type constrs: improve type app and variances.

1. type applications are not resolved until the results are used
closes #1234

2. streamline the handling of variances

Author: capfredf

typed-racket-lib/typed-racket/base-env/top-interaction.rkt

@@ -47,6 +47,7 @@
     "../types/utils.rkt"
     "../types/abbrev.rkt"
     "../types/printer.rkt"
+    "../types/resolve.rkt"
     "../typecheck/possible-domains.rkt"
     "../typecheck/typechecker.rkt"
     "../rep/type-rep.rkt"
@@ -70,7 +71,9 @@
                       [current-type-names
                        (if (attribute verbose-kw) '() (current-type-names))]
                       [current-print-unexpanded (box '())])
-         (define type (pretty-format-rep (parse-type #'ty)))
+         (define type (pretty-format-rep (match (parse-type #'ty)
+                                           [(? App? ty) (resolve ty)]
+                                           [ty ty])))
          (define unexpanded
            (remove-duplicates (unbox (current-print-unexpanded))))
          (define cue (if (null? unexpanded)

typed-racket-lib/typed-racket/env/init-envs.rkt

@@ -12,7 +12,6 @@
          "signature-env.rkt"
          "struct-name-env.rkt"
          "../private/user-defined-type-constr.rkt"
-         "../typecheck/struct-type-constr.rkt"
          "../rep/core-rep.rkt"
          "../rep/type-rep.rkt"
          "../rep/type-constr.rkt"
@@ -364,9 +363,11 @@
     ;; Most Top types are in the predefined table, the ones here
     ;; are not
     [(StructTop: name) `(make-StructTop ,(type->sexp name))]
-    [(TypeConstructor constr arity kind*? productive?)
+    [(TypeConstructor constr arity kind*? productive? variances)
      (define constr^ (gen-serialize-type-rep constr type->sexp))
-     `(make-type-constr ,constr^ ,arity ,productive? #:kind*? ,kind*?)]))
+     `(make-type-constr ,constr^ ,arity ,productive? #:kind*? ,kind*?
+                        #:variances
+                        (list #,@(map variance->binding variances)))]))
 
 ;; Helper for class/row clauses
 (define (convert-row-clause members [inits? #f])
@@ -459,10 +460,6 @@
     type-name-env-map
     (λ (id ty) #`(register-type-name #'#,id #,(quote-type ty)))))
 
-(define (tvariance-env-init-code)
-  (make-init-code
-    type-variance-env-map
-    (λ (id var) #`(register-type-variance! #'#,id (list #,@(map variance->binding var))))))
 
 (define (talias-env-init-code)
   (make-init-code
@@ -489,10 +486,11 @@
    kind-env-map
    (lambda (id v)
      ;; TODO: turn this into a function
-     (match-define (TypeConstructor constr arity kind*? productive?) v)
+     (match-define (TypeConstructor constr arity kind*? productive? variances) v)
      (define constr^ (gen-serialize-type-rep constr type->sexp))
      #`(register-type-constructor! #'#,id
-                                   (make-type-constr #,constr^ #,arity #,productive? #:kind*? #,kind*?)))))
+                                   (make-type-constr #,constr^ #,arity #,productive? #:kind*? #,kind*?
+                                                     #:variances (list #,@(map variance->binding variances)))))))
 
 ;; see 'finalize-signatures!' in 'env/signature-env.rkt',
 ;; which forces these delays after all the signatures are parsed
@@ -519,7 +517,6 @@
     (list (env-init-code)
           (talias-env-init-code)
           (tname-env-init-code)
-          (tvariance-env-init-code)
           (mvar-env-init-code mvar-env)
           (signature-env-init-code)
           (make-struct-table-code)

typed-racket-lib/typed-racket/env/type-alias-helper.rkt

@@ -8,10 +8,12 @@
          "type-alias-env.rkt"
          "type-name-env.rkt"
          "../rep/type-rep.rkt"
+         "../rep/free-variance.rkt"
          "../rep/type-constr.rkt"
          "tvar-env.rkt"
          "type-constr-env.rkt"
          "../private/parse-type.rkt"
+         "../private/user-defined-type-constr.rkt"
          "../typecheck/internal-forms.rkt"
          "../types/resolve.rkt"
          "../types/base-abbrev.rkt"
@@ -70,11 +72,13 @@
         ;; start registering type alias names
         (start-type-alias-registration! id (make-Name id (length args) #f))
         (values id (list id type-stx args))))
-    (register-all-type-alias-info type-alias-names type-alias-map)
-    (unless (zero? (free-id-table-count (incomplete-name-alias-map)))
-      (define names (free-id-table-keys (incomplete-name-alias-map)))
-      (int-err "not all type alias names are fully registered: ~n ~a"
-               names))))
+
+    (begin0
+      (register-all-type-alias-info type-alias-names type-alias-map)
+      (unless (zero? (free-id-table-count (incomplete-name-alias-map)))
+        (define names (free-id-table-keys (incomplete-name-alias-map)))
+        (int-err "not all type alias names are fully registered: ~n ~a"
+                 names)))))
 
 ;; Identifier -> Type
 ;; Construct a fresh placeholder type
@@ -198,20 +202,31 @@
   ;; Note that the connected component algorithm returns results
   ;; in topologically sorted order, so we want to go through in the
   ;; reverse order of that to avoid unbound type aliases.
-  (for ([id (in-list acyclic-singletons)])
-    (match-define (list _ type-stx args) (free-id-table-ref type-alias-map id))
-    (cond
-      [(not (null? args))
-       (define ty-op (parse-type-operator-abstraction id args type-stx #f
-                                                      type-alias-productivity-map))
-       (register-type-constructor! id ty-op)]
-      [else
-       ;; id can be a simple abbreviation for another type constructor
-       (define rv (parse-type-or-type-constructor type-stx))
-       ((if (TypeConstructor? rv)
-            register-type-constructor!
-            register-resolved-type-alias) id rv)])
-    (complete-type-alias-registration! id))
+  (define acyclic-constr-names
+    (for/fold ([acc '()])
+              ([id (in-list acyclic-singletons)])
+      (match-define (list _ type-stx args) (free-id-table-ref type-alias-map id))
+      (define acc^
+        (cond
+          [(not (null? args))
+           (define ty-op (parse-type-operator-abstraction id args type-stx #f
+                                                          type-alias-productivity-map))
+
+           (register-type-constructor! id ty-op)
+           (cons id acc)]
+          [else
+           ;; id can be a simple abbreviation for another type constructor
+           (define rv (parse-type-or-type-constructor type-stx))
+           (match rv
+             [(? TypeConstructor?)
+              (register-type-constructor! id rv)
+              (if (user-defined-type-constr? rv)
+                  (cons id acc)
+                  acc)]
+             [else (register-resolved-type-alias id rv)
+                   acc])]))
+      (complete-type-alias-registration! id)
+      acc^))
 
   ;; Clear the resolver cache of Name types from this block
 
@@ -250,41 +265,40 @@
     (for/lists (_1 _2 _3)
                ([record (in-list type-records)])
       (match-define (list id type-stx args) record)
-      ;; TODO try parse-type
       (define type (parse-type type-stx type-alias-productivity-map))
       (reset-resolver-cache!)
       (register-type-name id type)
       (complete-type-alias-registration! id)
-      (add-constant-variance! id args)
       (values id type (map syntax-e args))))
 
-  ;; do a pass to refine the variance
-  (refine-variance! names-to-refine types-to-refine tvarss)
-
   (define-values (productive unproductive)
     (partition (match-lambda
                  [(cons a _)
                   (equal? (free-id-table-ref type-alias-productivity-map a #f) #t)])
                type-op-records))
 
-  (let (;; sort unproductive constructors by the number of dependent
-        ;; user-defined constructors in increasing order
-        [unproductive (sort unproductive <
+  ;; sort unproductive constructors by the number of dependent
+  ;; user-defined constructors in increasing order
+  (let ([unproductive (sort unproductive <
                             #:key
                              (match-lambda
                                [(cons a _)
                                 (length (free-id-table-ref type-alias-dependency-map a #f))]))])
-    (for/list ([record (in-list (append productive unproductive))])
-      (match-define (list id type-stx args) record)
-      (define ty-op (parse-type-operator-abstraction id args type-stx
-                                                     (lambda (x)
-                                                       (define res (in-same-component? id x))
-                                                       res)
-                                                     type-alias-productivity-map))
-      (register-type-constructor! id ty-op)
-      (complete-type-alias-registration! id)
-      (reset-resolver-cache!)
-      (add-constant-variance! id args))))
+    (define constr-names
+      (for/list ([record (in-list (append productive unproductive))])
+        (match-define (list id type-stx args) record)
+        (define ty-op (parse-type-operator-abstraction id args type-stx
+                                                       (lambda (x)
+                                                         (define res (in-same-component? id x))
+                                                         res)
+                                                       type-alias-productivity-map
+                                                       #:delay-variances? #t))
+        (register-type-constructor! id ty-op)
+        (complete-type-alias-registration! id)
+        (reset-resolver-cache!)
+        id))
+    (refine-user-defined-constructor-variances! constr-names)
+    (append acyclic-constr-names constr-names)))
 
 ;; Syntax -> Syntax Syntax (Listof Syntax)
 ;; Parse a type alias internal declaration

typed-racket-lib/typed-racket/env/type-name-env.rkt

@@ -21,25 +21,10 @@
                        [add-alias (-> identifier? identifier? any)]
                        [type-name-env-map
                         (-> (-> identifier? (or/c #t Type?) any) any)]
-                       [type-variance-env-map
-                        (-> (-> identifier? (listof variance?) any) any)]
                        [type-name-env-for-each
                         (-> (-> identifier? (or/c #t Type?) any) void?)]
-                       [type-variance-env-for-each
-                        (-> (-> identifier? (listof variance?) any) void?)]
                        [lookup-type-name
-                        (->* (identifier?) (procedure?) (or/c #t Type?))]
-                       [register-type-variance!
-                        (-> identifier? (listof variance?) any)]
-                       [lookup-type-variance
-                        (-> identifier? (listof variance?))]
-                       [add-constant-variance!
-                        (-> identifier? (or/c #f (listof identifier?)) any)]
-                       [refine-variance!
-                        (-> (listof identifier?)
-                            (listof Type?)
-                            (listof (or/c #f (listof symbol?)))
-                            any)])
+                        (->* (identifier?) (procedure?) (or/c #t Type?))])
 
 ;; a mapping from id -> type (where id is the name of the type)
 (define the-mapping
@@ -82,46 +67,3 @@
        (register-type-constructor! from v))]))
 
 
-;; a mapping from id -> listof[Variance] (where id is the name of the type)
-(define variance-mapping
-  (make-free-id-table))
-
-;; add a name to the mapping
-(define (register-type-variance! id variance)
-  (free-id-table-set! variance-mapping id variance))
-
-(define (lookup-type-variance id)
-  (free-id-table-ref
-   variance-mapping id
-   (lambda () (lookup-variance-fail id))))
-
-;; map over the-mapping, producing a list
-;; (id variance -> T) -> listof[T]
-(define (type-variance-env-map f)
-  (sorted-free-id-table-map variance-mapping f))
-
-(define (type-variance-env-for-each f)
-  (sorted-free-id-table-for-each variance-mapping f))
-
-;; Refines the variance of a type in the name environment
-(define (refine-variance! names types tvarss)
-  (let loop ()
-    (define sames?
-      (for/and ([name (in-list names)]
-                [type (in-list types)]
-                [tvars (in-list tvarss)])
-        (cond
-          [(or (not tvars) (null? tvars)) #t]
-          [else
-            (define free-vars (free-vars-hash (free-vars* type)))
-            (define variance (map (λ (v) (hash-ref free-vars v variance:const)) tvars))
-            (define old-variance (lookup-type-variance name))
-
-            (register-type-variance! name variance)
-            (equal? variance old-variance)])))
-    (unless sames? (loop))))
-
-;; Initialize variance of the given id to Constant for all type vars
-(define (add-constant-variance! name vars)
-  (unless (or (not vars) (null? vars))
-    (register-type-variance! name (map (lambda (_) variance:const) vars))))

typed-racket-lib/typed-racket/private/parse-type.rkt

@@ -10,6 +10,7 @@
          "../rep/free-ids.rkt"
          "../rep/rep-utils.rkt"
          "../rep/type-constr.rkt"
+         "../rep/free-variance.rkt"
          "../types/abbrev.rkt"
          "user-defined-type-constr.rkt"
          "../types/utils.rkt"
@@ -43,6 +44,7 @@
          racket/format
          racket/match
          syntax/id-table
+         syntax/id-set
          "parse-classes.rkt"
          (for-template "../base-env/base-types-extra.rkt"
                        racket/base)
@@ -63,7 +65,8 @@
                     Type?)]
  [parse-type-operator-abstraction (c:->* (identifier? (c:listof identifier?) syntax?)
                                          ((c:or/c (c:-> identifier? boolean?) #f)
-                                          (free-id-table/c identifier? boolean?))
+                                          (free-id-table/c identifier? boolean?)
+                                          #:delay-variances? boolean?)
                                          TypeConstructor?)]
  [parse-for-effects (c:-> identifier? (c:cons/c (c:listof identifier?) syntax?)
                           (values (c:listof identifier?)
@@ -646,7 +649,9 @@
 ;; type-op-productivity-map: maps names of constructors to their productivity.
 
 (define (parse-type-operator-abstraction name arg-names stx [opt-in-same-component? #f]
-                                         [type-op-productivity-map (make-immutable-free-id-table)])
+                                         [type-op-productivity-map (make-immutable-free-id-table)]
+                                         #:delay-variances?
+                                         [delay-variances? #f])
   (define syms (map syntax-e arg-names))
   (define mode (synth-mode name syms opt-in-same-component?))
   (define var-kind-level-env
@@ -664,9 +669,14 @@
                             (parse stx INIT-LEVEL
                                    var-kind-level-env
                                    #:mode mode)))
+
   (make-type-constr (user-defined-type-op syms res)
                     (length syms)
-                    (free-id-table-ref type-op-productivity-map name #f)))
+                    (free-id-table-ref type-op-productivity-map name #f)
+                    #:variances
+                    (if delay-variances?
+                        (build-default-variances syms)
+                        (variances-in-type res syms))))
 
 (define (parse-type-or-type-constructor stx)
   (parse stx 0 (make-immutable-free-id-table) #:mode #f #:ret-type-op? #t))
@@ -1357,16 +1367,25 @@
                       [var (in-list (synth-mode-args mode))])
                   (check-argument rand var))))
             (match rator
-              [(? TypeConstructor?)
+              [(struct* TypeConstructor ([arity arity]))
+               (define (err expected given)
+                 (tc-error (~a "wrong number of arguments to type constructor"
+                               "\n  type: " #'id
+                               "\n  expected: " expected
+                               "\n  given: " given
+                               "\n  arguments...: " #'(args ...))))
+
                (with-handlers ([exn:fail:contract:arity:type-constructor?
                                 (lambda (e)
                                   (match-define (exn:fail:contract:arity:type-constructor _ _ expected given) e)
-                                  (tc-error (~a "wrong number of arguments to type constructor"
-                                                "\n  type: " #'id
-                                                "\n  expected: " expected
-                                                "\n  given: " given
-                                                "\n  arguments...: " #'(args ...))))])
-                 (apply rator args^))]
+                                  (err expected given))])
+                 (define alias (lookup-type-alias #'id (lambda (x) x) (lambda () #f)))
+                 (match alias
+                   [(? Name?)
+                    (if (equal? arity (length args^))
+                        (make-App alias args^)
+                        (err arity (length args^)))]
+                   [_ (apply rator args^)]))]
               [(? Name?)
                (resolve-app-check-error rator args^ stx)
                (define app (make-App rator args^))