tc-app: add missing 'function' annotations

Update the type-table with annotations for some identifiers
 that are handled specially by `tc-app`.

Add type table tests to `unit-tests/typecheck-tests.rkt`

Author: bennn

typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-apply.rkt

@@ -5,7 +5,7 @@
          "utils.rkt"
          syntax/parse racket/match
          (typecheck signatures)
-         (types abbrev utils)
+         (types abbrev type-table utils)
          (rep type-rep)
 
          (for-label
@@ -26,7 +26,9 @@
     (match (single-value #'e)
       [(tc-result1: (ListDots: dty dbound))
        (ret null null null dty dbound)]
-      [(tc-result1: (List: ts)) (ret ts)]
+      [(tc-result1: (List: ts))
+       (add-typeof-expr #'f (ret (->* ts (-values ts))))
+       (ret ts)]
       [_ (tc/apply #'f #'(e))]))
   (pattern ((~or apply k:apply) f . args)
     (tc/apply #'f #'args)))

typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt

@@ -49,76 +49,91 @@
 
 
 ;; FIXME - Do something with paths in the case that a structure/vector is not mutable
-(define (tc/hetero-ref i-e es-t vec-t name)
+(define (tc/hetero-ref i-e es-t vec-t name op)
   (define i-val (tc/index i-e))
   (define i-bound (length es-t))
   (cond
     [(valid-index? i-val i-bound)
-     (ret (list-ref es-t i-val))]
+     (define return-ty (list-ref es-t i-val))
+     (add-typeof-expr op (ret (-> vec-t -Fixnum return-ty)))
+     (ret return-ty)]
     [(not i-val)
-     (ret (apply Un es-t))]
+     (define return-ty (apply Un es-t))
+     (add-typeof-expr op (ret (-> vec-t -Fixnum return-ty)))
+     (ret return-ty)]
     [else
      (index-error i-val i-bound i-e vec-t name)]))
 
-(define (tc/hetero-set! i-e es-t val-e vec-t name)
+(define (tc/hetero-set! i-e es-t val-e vec-t name op)
   (define i-val (tc/index i-e))
   (define i-bound (length es-t))
-  (cond 
+  (cond
     [(valid-index? i-val i-bound)
-     (tc-expr/check val-e (ret (list-ref es-t i-val)))
+     (define val-t (list-ref es-t i-val))
+     (tc-expr/check val-e (ret val-t))
+     (add-typeof-expr op (ret (-> vec-t -Fixnum val-t -Void)))
      (ret -Void)]
     [(not i-val)
-     (define val-t (single-value val-e))
+     (define val-res (single-value val-e))
      (for ((es-type (in-list es-t)))
-       (check-below val-t (ret es-type)))
+       (check-below val-res (ret es-type)))
+     (define val-t
+       (match val-res [(tc-result1: t) t]))
+     (add-typeof-expr op (ret (-> vec-t -Fixnum val-t -Void)))
      (ret -Void)]
     [else
      (single-value val-e)
      (index-error i-val i-bound i-e vec-t name)]))
 
 (define-tc/app-syntax-class (tc/app-hetero expected)
   #:literal-sets (hetero-literals)
-  (pattern (~and form ((~or unsafe-struct-ref unsafe-struct*-ref) struct:expr index:expr))
+  (pattern (~and form ((~and op (~or unsafe-struct-ref unsafe-struct*-ref)) struct:expr index:expr))
     (match (single-value #'struct)
       [(tc-result1: (and struct-t (app resolve (Struct: _ _ (list (fld: flds _ _) ...) _ _ _))))
-       (tc/hetero-ref #'index flds struct-t "struct")]
+       (tc/hetero-ref #'index flds struct-t "struct" #'op)]
       [(tc-result1: (and struct-t (app resolve (Prefab: _ (list flds ...)))))
-       (tc/hetero-ref #'index flds struct-t "prefab struct")]
+       (tc/hetero-ref #'index flds struct-t "prefab struct" #'op)]
       [s-ty (tc/app-regular #'form expected)]))
   ;; vector-ref on het vectors
-  (pattern (~and form ((~or vector-ref unsafe-vector-ref unsafe-vector*-ref) vec:expr index:expr))
+  (pattern (~and form ((~and op (~or vector-ref unsafe-vector-ref unsafe-vector*-ref)) vec:expr index:expr))
     (match (single-value #'vec)
       [(tc-result1: (and vec-t (app resolve (Is-a: (HeterogeneousVector: es)))))
-       (tc/hetero-ref #'index es vec-t "vector")]
+       (tc/hetero-ref #'index es vec-t "vector" #'op)]
       [v-ty (tc/app-regular #'form expected)]))
-  ;; unsafe struct-set! 
-  (pattern (~and form ((~or unsafe-struct-set! unsafe-struct*-set!) s:expr index:expr val:expr))
+  ;; unsafe struct-set!
+  (pattern (~and form ((~and op (~or unsafe-struct-set! unsafe-struct*-set!)) s:expr index:expr val:expr))
     (match (single-value #'s)
       [(tc-result1: (and struct-t (app resolve (Struct: _ _ (list (fld: flds _ _) ...) _ _ _))))
-       (tc/hetero-set! #'index flds #'val struct-t "struct")]
+       (tc/hetero-set! #'index flds #'val struct-t "struct" #'op)]
       [s-ty (tc/app-regular #'form expected)]))
   ;; vector-set! on het vectors
-  (pattern (~and form ((~or vector-set! unsafe-vector-set! unsafe-vector*-set!) v:expr index:expr val:expr))
+  (pattern (~and form ((~and op (~or vector-set! unsafe-vector-set! unsafe-vector*-set!)) v:expr index:expr val:expr))
     (match (single-value #'v)
       [(tc-result1: (and vec-t (app resolve (Is-a: (HeterogeneousVector: es)))))
-       (tc/hetero-set! #'index es #'val vec-t "vector")]
+       (tc/hetero-set! #'index es #'val vec-t "vector" #'op)]
       [v-ty (tc/app-regular #'form expected)]))
-  (pattern (~and form ((~or vector-immutable vector) args:expr ...))
+  (pattern (~and form ((~and op (~or vector-immutable vector)) args:expr ...))
     (match expected
       [(tc-result1: (app resolve (Is-a: (Vector: t))))
-       (ret (make-HeterogeneousVector 
-              (for/list ([e (in-syntax #'(args ...))])
-                (tc-expr/check e (ret t))
-                t)))]
+       (define arg-tys
+         (for/list ([e (in-syntax #'(args ...))])
+           (tc-expr/check e (ret t))
+           t))
+       (define return-ty
+         (make-HeterogeneousVector arg-tys))
+       (add-typeof-expr #'op (ret (->* arg-tys return-ty)))
+       (ret return-ty)]
       [(tc-result1: (app resolve (Is-a: (HeterogeneousVector: ts))))
        (cond
          [(= (length ts) (syntax-length #'(args ...)))
-          (ret
-            (make-HeterogeneousVector
-              (for/list ([e (in-syntax #'(args ...))]
-                         [t (in-list ts)])
-                (tc-expr/check/t e (ret t))))
-            -true-propset)]
+          (define arg-tys
+            (for/list ([e (in-syntax #'(args ...))]
+                       [t (in-list ts)])
+              (tc-expr/check/t e (ret t))))
+          (define return-ty
+            (make-HeterogeneousVector arg-tys))
+          (add-typeof-expr #'op (ret (->* arg-tys return-ty)))
+          (ret return-ty -true-propset)]
          [else
           (tc-error/expr
             "expected vector with ~a elements, but got ~a"
@@ -136,7 +151,11 @@
          [_ (continue)])]
       ;; since vectors are mutable, if there is no expected type, we want to generalize the element type
       [(or #f (tc-any-results: _) (tc-result1: _))
-       (ret (make-HeterogeneousVector
-              (for/list ((e (in-syntax #'(args ...))))
-                (generalize (tc-expr/t e)))))]
+       (define arg-tys
+         (for/list ((e (in-syntax #'(args ...))))
+           (generalize (tc-expr/t e))))
+       (define return-ty
+         (make-HeterogeneousVector arg-tys))
+       (add-typeof-expr #'op (ret (->* arg-tys return-ty)))
+       (ret return-ty)]
       [_ (ret Err)])))

typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-list.rkt

@@ -6,7 +6,7 @@
          "utils.rkt"
          syntax/parse syntax/stx racket/match racket/sequence
          (typecheck signatures tc-funapp error-message)
-         (types abbrev utils substitute)
+         (types abbrev type-table utils substitute)
          (rep type-rep)
          (env tvar-env)
          (prefix-in i: (infer infer))
@@ -79,58 +79,79 @@
         [_ (tc/app-regular #'form expected)])))
   ;; special case for `list'
   (pattern
-   (list . args)
+   ((~and op-name list) . args)
    (let ([args-list (syntax->list #'args)])
-   (match expected
-     [(tc-result1: t)
-      (match t
-        [(List: ts)
-         (cond
-           [(= (length ts) (length args-list))
-            (for ([arg (in-list args-list)]
-                  [t (in-list ts)])
-              (tc-expr/check arg (ret t)))
-            (ret t)]
-           [else
-            (expected-but-got t (-Tuple (map tc-expr/t args-list)))
-            (ret t)])]
-        [_
-         (define vs (map (λ (_) (gensym)) args-list))
-         (define l-type (-Tuple (map make-F vs)))
-         ;; We want to infer the largest vs that are still under the element types
-         (define substs (i:infer vs null (list l-type) (list t) (-values (list (-> l-type Univ)))
-                                 #:multiple? #t))
-         (cond
-           [substs
-            (define result
-              (for*/first ([subst (in-list substs)]
-                           [argtys (in-value (for/list ([arg (in-list args-list)]
-                                                        [v (in-list vs)])
-                                               (tc-expr/check/t? arg (ret (subst-all subst (make-F v))))))]
-                           #:when (andmap values argtys))
-                (ret (-Tuple argtys))))
-            (or result
-                (begin (expected-but-got t (-Tuple (map tc-expr/t args-list)))
-                       (fix-results expected)))]
-           [else (ret (-Tuple (map tc-expr/t args-list)))])])]
-     [_ (ret (-Tuple (map tc-expr/t args-list)))])))
+     (match expected
+       [(tc-result1: t)
+        (match t
+          [(List: ts)
+           (cond
+             [(= (length ts) (length args-list))
+              (for ([arg (in-list args-list)]
+                    [t (in-list ts)])
+                (tc-expr/check arg (ret t)))
+              (add-typeof-expr #'op-name (ret (->* ts t)))
+              (ret t)]
+             [else
+              (expected-but-got t (-Tuple (map tc-expr/t args-list)))
+              (ret t)])]
+          [_
+           (define vs (map (λ (_) (gensym)) args-list))
+           (define l-type (-Tuple (map make-F vs)))
+           ;; We want to infer the largest vs that are still under the element types
+           (define substs (i:infer vs null (list l-type) (list t) (-values (list (-> l-type Univ)))
+                                   #:multiple? #t))
+           (cond
+             [substs
+              (define result
+                (for*/first ([subst (in-list substs)]
+                             [arg-tys (in-value (for/list ([arg (in-list args-list)]
+                                                           [v (in-list vs)])
+                                                  (tc-expr/check/t? arg (ret (subst-all subst (make-F v))))))]
+                             #:when (andmap values arg-tys))
+                  (define return-ty (-Tuple arg-tys))
+                  (add-typeof-expr #'op-name (ret (->* arg-tys return-ty)))
+                  (ret return-ty)))
+              (or result
+                  (begin (expected-but-got t (-Tuple (map tc-expr/t args-list)))
+                         (fix-results expected)))]
+             [else
+              (define arg-tys (map tc-expr/t args-list))
+              (define return-ty (-Tuple arg-tys))
+              (add-typeof-expr #'op-name (ret (->* arg-tys return-ty)))
+              (ret return-ty)])])]
+       [_
+        (define arg-tys (map tc-expr/t args-list))
+        (define return-ty (-Tuple arg-tys))
+        (add-typeof-expr #'op-name (ret (->* arg-tys return-ty)))
+        (ret return-ty)])))
   ;; special case for `list*'
-  (pattern (list* (~between args:expr 1 +inf.0) ...)
-    (match-let* ([(list tys ... last) (stx-map tc-expr/t #'(args ...))])
-      (ret (foldr -pair last tys))))
+  (pattern ((~and op-name list*) (~between args:expr 1 +inf.0) ...)
+    (match-let* ([(and arg-tys (list tys ... last)) (stx-map tc-expr/t #'(args ...))])
+      (define return-ty (foldr -pair last tys))
+      (add-typeof-expr #'op-name (ret (->* arg-tys return-ty)))
+      (ret return-ty)))
   ;; special case for `reverse' to propagate expected type info
   (pattern ((~and fun (~or reverse k:reverse)) arg)
     (match expected
-      [(tc-result1: (Listof: _))
-       (tc-expr/check #'arg expected)]
+      [(tc-result1: (and return-ty (Listof: _)))
+       (begin0
+         (tc-expr/check #'arg expected)
+         (add-typeof-expr #'fun (ret (-> return-ty return-ty))))]
       [(tc-result1: (List: ts))
-       (tc-expr/check #'arg (ret (-Tuple (reverse ts))))
-       (ret (-Tuple ts))]
+       (define arg-ty (-Tuple (reverse ts)))
+       (define return-ty (-Tuple ts))
+       (tc-expr/check #'arg (ret arg-ty))
+       (add-typeof-expr #'fun (ret (-> arg-ty return-ty)))
+       (ret return-ty)]
       [_
        (match (single-value #'arg)
-         [(tc-result1: (List: ts))
-          (ret (-Tuple (reverse ts)))]
+         [(tc-result1: (and arg-ty (List: ts)))
+          (define return-ty (-Tuple (reverse ts)))
+          (add-typeof-expr #'fun (ret (-> arg-ty return-ty)))
+          (ret return-ty)]
          [(tc-result1: (and r (Listof: t)))
+          (add-typeof-expr #'fun (ret (-> r r)))
           (ret r)]
          [arg-ty
           (tc/funapp #'fun #'(arg) (tc-expr/t #'fun) (list arg-ty) expected)])])))

typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-special.rkt

@@ -51,10 +51,12 @@
                     (list (ret Univ) (single-value #'arg))
                     expected)]))
   ;; special-case for not - flip the props
-  (pattern ((~or false? not) arg)
+  (pattern ((~and op-name (~or false? not)) arg)
     (match (single-value #'arg)
       [(tc-result1: t (PropSet: p+ p-) _)
-       (ret -Boolean (make-PropSet p- p+))]))
+       (define new-prop (make-PropSet p- p+))
+       (add-typeof-expr #'op-name (ret (-> Univ -Boolean)))
+       (ret -Boolean new-prop)]))
   ;; special case for (current-contract-region)'s default expansion
   ;; just let it through without any typechecking, since module-name-fixup
   ;; is a private function from syntax/location, so this must have been

typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-values.rkt

@@ -4,8 +4,9 @@
          "signatures.rkt"
          "utils.rkt"
          syntax/parse racket/match racket/sequence
-         (typecheck signatures tc-funapp)
-         (types base-abbrev utils)
+         (typecheck signatures tc-funapp tc-metafunctions)
+         (types base-abbrev abbrev type-table utils)
+         (rep values-rep)
 
          (for-label racket/base))
 
@@ -18,34 +19,51 @@
 (define-tc/app-syntax-class (tc/app-values expected)
   #:literal-sets (values-literals)
   ;; call-with-values
-  (pattern (call-with-values prod con)
-    (match (tc/funapp #'prod #'() (tc-expr/t #'prod) null #f)
+  (pattern ((~and op-name call-with-values) prod con)
+    #:do [(define prod-ty (tc-expr/t #'prod))]
+    (match (tc/funapp #'prod #'() prod-ty null #f)
       [(tc-results: tcrs #f)
-       (tc/funapp #'con #'(prod) (tc-expr/t #'con)
-                  (for/list ([tcr (in-list tcrs)])
-                    (-tc-results (list tcr) #f))
-                  expected)]
+       (define con-ty (tc-expr/t #'con))
+       (define r
+         (tc/funapp #'con #'(prod) con-ty
+                    (for/list ([tcr (in-list tcrs)])
+                      (-tc-results (list tcr) #f))
+                    expected))
+       (define return-ty (tc-results->values r))
+       (add-typeof-expr #'op-name (ret (-> prod-ty con-ty return-ty)))
+       r]
       [(tc-results: _ (? RestDots?))
        (tc-error/expr "`call-with-values` with ... is not supported")]
       [(tc-any-results: _)
        (tc/app-regular this-syntax expected)]))
   ;; special case for `values' with single argument
   ;; we just ignore the values, except that it forces arg to return one value
-  (pattern (values arg)
-    (match expected
-     [(or #f (tc-any-results: _)) (single-value #'arg)]
-     [(tc-result1: tp)
-      (single-value #'arg expected)]
-      ;; Type check the argument, to find other errors
-     [_ (single-value #'arg)]))
+  (pattern ((~and op-name values) arg)
+    (let ([tc-result
+           (match expected
+            [(or #f (tc-any-results: _))
+             (single-value #'arg)]
+            [(tc-result1: tp)
+             (single-value #'arg expected)]
+             ;; Type check the argument, to find other errors
+            [_ (single-value #'arg)])])
+      (define arg-ty
+        ;; match never fails; `single-value` always returns a tc-result1
+        (match tc-result [(tc-result1: t) t]))
+      (add-typeof-expr #'op-name (ret (-> arg-ty arg-ty)))
+      tc-result))
   ;; handle `values' specially
-  (pattern (values . args)
+  (pattern ((~and op-name values) . args)
     (match expected
       [(or (tc-results: tcrs #f)
            (bind tcrs '()))
-       (-tc-results
-        (for/list ([arg (in-syntax #'args)]
-                   [tcr (in-list/rest tcrs #f)])
-          (match (single-value arg (and tcr (-tc-results (list tcr) #f)))
-            [(tc-results: (list res) #f) res]))
-        #f)])))
+       (define res
+         (-tc-results
+           (for/list ([arg (in-syntax #'args)]
+                      [tcr (in-list/rest tcrs #f)])
+             (match (single-value arg (and tcr (-tc-results (list tcr) #f)))
+               [(tc-results: (list res) #f) res])) #f))
+       (define return-ty (tc-results->values res))
+       (define arg-tys (match return-ty [(Values: (list (Result: t* _ _) ...)) t*]))
+       (add-typeof-expr #'op-name (ret (->* arg-tys return-ty)))
+       res])))