diff --git a/typed-racket-lib/typed-racket/base-env/base-types-extra.rkt b/typed-racket-lib/typed-racket/base-env/base-types-extra.rkt index ed415397..8087f5d2 100644 --- a/typed-racket-lib/typed-racket/base-env/base-types-extra.rkt +++ b/typed-racket-lib/typed-racket/base-env/base-types-extra.rkt @@ -17,7 +17,7 @@ (define-other-types -> ->* case-> U Rec All Opaque Vector Parameterof List List* Class Object Values Instance Refinement - pred Struct Struct-Type Prefab Top Bot) + pred Struct Struct-Type Prefab Top Bot Distinction) (provide (rename-out [All ∀] [U Un] diff --git a/typed-racket-lib/typed-racket/base-env/prims-struct.rkt b/typed-racket-lib/typed-racket/base-env/prims-struct.rkt index 50ec5d05..940b0320 100644 --- a/typed-racket-lib/typed-racket/base-env/prims-struct.rkt +++ b/typed-racket-lib/typed-racket/base-env/prims-struct.rkt @@ -206,10 +206,9 @@ stx (and (stx-pair? stx) (stx-car stx)))) #`(begin + (define-type-alias ty (Distinction ty gen-id rep-ty)) #,(ignore - #'(begin - (define-syntax ty stx-err-fun) - (define constructor (lambda (x) x)))) + #'(define constructor (lambda (x) x))) #,(internal (syntax/loc stx (define-new-subtype-internal ty (constructor rep-ty) #:gen-id gen-id))))]))) diff --git a/typed-racket-lib/typed-racket/private/parse-type.rkt b/typed-racket-lib/typed-racket/private/parse-type.rkt index 45297811..c5b2201c 100644 --- a/typed-racket-lib/typed-racket/private/parse-type.rkt +++ b/typed-racket-lib/typed-racket/private/parse-type.rkt @@ -100,6 +100,7 @@ (define-literal-syntax-class #:for-label values) (define-literal-syntax-class #:for-label Top) (define-literal-syntax-class #:for-label Bot) +(define-literal-syntax-class #:for-label Distinction) ;; (Syntax -> Type) -> Syntax Any -> Syntax ;; See `parse-type/id`. This is a curried generalization. @@ -427,6 +428,8 @@ (parse-all-type stx)] [(:Opaque^ p?:id) (make-Opaque #'p?)] + [(:Distinction^ name:id unique-id:id rep-ty:expr) + (-Distinction (syntax-e #'name) (syntax-e #'unique-id) (parse-type #'rep-ty))] [(:Parameter^ t) (let ([ty (parse-type #'t)]) (-Param ty ty))] diff --git a/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt b/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt index aa6db55b..76d8e4f7 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt @@ -69,8 +69,7 @@ ;; define-new-subtype [form:new-subtype-def - ;; also handled by an earlier pass - (list)] + (handle-define-new-subtype/pass1 #'form)] ;; declare-refinement ;; FIXME - this sucks and should die @@ -290,12 +289,11 @@ (define (type-check forms0) (define forms (syntax->list forms0)) (do-time "before form splitting") - (define-values (type-aliases struct-defs new-subtype-defs stx-defs0 val-defs0 provs) + (define-values (type-aliases struct-defs stx-defs0 val-defs0 provs) (filter-multiple forms type-alias? (lambda (e) (or (typed-struct? e) (typed-struct/exec? e))) - new-subtype-def? parse-syntax-def parse-def provide?)) @@ -314,8 +312,6 @@ (for-each add-constant-variance! names type-vars)) (do-time "after adding type names") - (for-each handle-define-new-subtype new-subtype-defs) - (register-all-type-aliases type-alias-names type-alias-map) (do-time "starting struct handling") @@ -548,17 +544,13 @@ (begin0 (tc-toplevel/pass2 form #f) (report-all-errors))) -;; handle-define-new-subtype : Syntax -> Void -(define (handle-define-new-subtype form) +;; handle-define-new-subtype/pass1 : Syntax -> Empty +(define (handle-define-new-subtype/pass1 form) (syntax-parse form - ;; define-new-subtype [form:new-subtype-def ;; (define-new-subtype-internal name (constructor rep-type) #:gen-id gen-id) - (define name (syntax-e (attribute form.name))) - (define sym (syntax-e (attribute form.gen-id))) + (define ty (parse-type (attribute form.name))) (define rep-ty (parse-type (attribute form.rep-type))) - (define new-ty (-Distinction name sym rep-ty)) - (register-type (attribute form.constructor) (-> rep-ty new-ty)) - (register-type-alias (attribute form.name) new-ty) - (void)])) + (register-type (attribute form.constructor) (-> rep-ty ty)) + (list)])) diff --git a/typed-racket-lib/typed-racket/types/subtype.rkt b/typed-racket-lib/typed-racket/types/subtype.rkt index 1e5412fa..6bf66c57 100644 --- a/typed-racket-lib/typed-racket/types/subtype.rkt +++ b/typed-racket-lib/typed-racket/types/subtype.rkt @@ -293,6 +293,9 @@ [((or (? Struct? s1) (NameStruct: s1)) (Value: (? (negate struct?) _))) #f] ;; from define-new-subtype + [((Distinction: nm1 id1 t1) (app resolve (Distinction: nm2 id2 t2))) + #:when (and (equal? nm1 nm2) (equal? id1 id2)) + (subtype* A0 t1 t2)] [((Distinction: _ _ t1) t2) (subtype* A0 t1 t2)] ;; sequences are covariant diff --git a/typed-racket-lib/typed/racket/base.rkt b/typed-racket-lib/typed/racket/base.rkt index 77349992..37014066 100644 --- a/typed-racket-lib/typed/racket/base.rkt +++ b/typed-racket-lib/typed/racket/base.rkt @@ -18,7 +18,7 @@ require-typed-struct-legacy require/typed-legacy) typed-racket/base-env/base-types - typed-racket/base-env/base-types-extra) + (except-in typed-racket/base-env/base-types-extra Distinction)) (provide (rename-out [define-type-alias define-type]) (all-from-out typed-racket/base-env/prims) (all-from-out typed-racket/base-env/base-types) diff --git a/typed-racket-test/fail/issue-169-1.rkt b/typed-racket-test/fail/issue-169-1.rkt new file mode 100644 index 00000000..3827741b --- /dev/null +++ b/typed-racket-test/fail/issue-169-1.rkt @@ -0,0 +1,7 @@ +#lang typed/racket +(define-type Pos Integer) +(define-new-subtype Pos* (p Pos)) +(define lst + (for*/list ([x (in-range 3)]) : (Listof Pos*) + (p x))) +(ann lst (Listof Nothing)) ; this should fail diff --git a/typed-racket-test/fail/issue-169-2.rkt b/typed-racket-test/fail/issue-169-2.rkt new file mode 100644 index 00000000..08b7f4bd --- /dev/null +++ b/typed-racket-test/fail/issue-169-2.rkt @@ -0,0 +1,8 @@ +#lang typed/racket +(define-type Pos Integer) +(define-new-subtype Pos* (p Pos)) +(define lst : (Listof Pos*) + '()) +(define lst* + (reverse lst)) +(ann lst* (Listof Nothing)) ; this should fail diff --git a/typed-racket-test/succeed/define-new-subtype-mu-rec.rkt b/typed-racket-test/succeed/define-new-subtype-mu-rec.rkt new file mode 100644 index 00000000..9c32405d --- /dev/null +++ b/typed-racket-test/succeed/define-new-subtype-mu-rec.rkt @@ -0,0 +1,10 @@ +#lang typed/racket/base + +(define-new-subtype Lst (make-Lst (U Null (Pairof Elt Lst)))) +(define-new-subtype Elt (make-Elt (U Symbol Lst))) + +(: lst : [Elt * -> Lst]) +(define (lst . args) + (for/fold ([lst (make-Lst '())]) ([elt (in-list (reverse args))]) + (make-Lst (cons elt lst)))) +