fix issue #169

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]

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))))])))
 

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))]

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)]))
 

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

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)

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

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

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))))
+