diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-apply.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-apply.rkt
index bfd3ace3..d77dc3e0 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-apply.rkt
+++ b/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)))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt
index 5669740e..2191070f 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt
@@ -49,28 +49,37 @@
 
 
 ;; 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)
@@ -78,47 +87,53 @@
 
 (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)])))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-list.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-list.rkt
index 8fc941e0..67099033 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-list.rkt
+++ b/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)])])))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-special.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-special.rkt
index 9f83ccae..904f4dc2 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-special.rkt
+++ b/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
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-values.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-values.rkt
index 4601a8fd..5aa0b84e 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-values.rkt
+++ b/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])))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-apply.rkt b/typed-racket-lib/typed-racket/typecheck/tc-apply.rkt
index 7b81aff6..e51de097 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-apply.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-apply.rkt
@@ -3,7 +3,7 @@
 (require (rename-in "../utils/utils.rkt" [infer r:infer])
          racket/match racket/list
          (typecheck signatures tc-app-helper)
-         (types utils abbrev substitute)
+         (types utils abbrev substitute type-table)
          (utils tc-utils)
          (rep type-rep core-rep values-rep)
          (r:infer infer))
@@ -67,8 +67,9 @@
            ;; Takes a possible substitution and comuptes
            ;; the substituted range type if it is not #f
            (define (finish substitution)
-             (and substitution (do-ret (subst-all substitution rng))))
-
+             (begin0
+               (and substitution (do-ret (subst-all substitution rng)))
+               (add-typeof-expr f (ret (make-Fun (list arrow))))))
            (finish
             (infer vars dotted-vars
                    (list (-Tuple* arg-tys full-tail-ty))
diff --git a/typed-racket-test/unit-tests/typecheck-tests.rkt b/typed-racket-test/unit-tests/typecheck-tests.rkt
index 11b0a7cf..55a7e47f 100644
--- a/typed-racket-test/unit-tests/typecheck-tests.rkt
+++ b/typed-racket-test/unit-tests/typecheck-tests.rkt
@@ -42,14 +42,17 @@
     "test-utils.rkt"
     typed-racket/utils/utils
     racket/base racket/match
+    syntax/id-table
     (rep core-rep)
     (rename-in (types prop-ops tc-result printer subtype) [ret raw-ret])
+    (only-in (types type-table) type-of)
     syntax/parse
     (for-template (only-in typed-racket/typed-racket do-standard-inits))
     (typecheck typechecker check-below tc-metafunctions)
     (utils mutated-vars tc-utils)
     (env lexical-env mvar-env))
   (provide
+    test-type-table
     test-literal test-literal/fail
     test test/proc test/fail)
 
@@ -122,6 +125,38 @@
     (define golden (golden-fun expanded-expr))
     (check-tc-results result golden #:name "tc-expr"))
 
+  ;; test-type-table : syntax? (listof (cons/c identifier? tc-results?)) -> void?
+  ;; Typecheck the given expression
+  ;;  and assert that the type-table has an entry for every identifier
+  ;;  in the given association list.
+  ;;
+  ;; Example: `(test-type-table expr (list (cons f t)))` will
+  ;; 1. type-check `expr`
+  ;; 2. search `expr` for occurrences of `f`
+  ;; 3. check that the type-table entry for `f` matches `t`
+  (define (test-type-table expr assoc)
+    (define expanded-expr
+      (let ([expr+ (tr-expand expr)])
+        (begin (tc expr+ #f) expr+)))
+    (define expected-results
+      (make-free-id-table assoc))
+    (let loop ([x expanded-expr]) ;; loop : any/c -> void?
+      (cond
+       [(and (identifier? x)
+             (free-id-table-ref expected-results x #f))
+        => (λ (expected)
+             (define actual (type-of x))
+             (define test-name (format "(type-of ~a)" (syntax-e x)))
+             (check-tc-results actual expected #:name test-name))]
+       [(syntax? x)
+        (loop (syntax-e x))]
+       [(list? x)
+        (map loop x)]
+       [(pair? x)
+        (loop (car x))
+        (loop (cdr x))]
+       [else
+        (void)])))
 
   ;; test/fail syntax? tc-results? (or/c string? regexp?) (option/c tc-results?)
   ;;           [(listof (list id type))] -> void?
@@ -278,6 +313,15 @@
        (test-phase1 #,(syntax/loc #'lit (LITERAL/FAIL lit))
          (test-literal/fail (quote-syntax lit) msg.v ex.v)))]))
 
+(define-syntax (tc/type-table stx)
+  (syntax-parse stx
+    [(_ e:expr ([k v] ...))
+     (quasisyntax/loc stx
+       (test-phase1 e
+         (test-type-table
+           (quote-syntax e)
+           (list (cons (quote-syntax k) (ret v)) ...))))]))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -4490,4 +4534,99 @@
          (-prefab 'foo (-opt -String))
          #:expected (-prefab 'foo (-opt -String))]
    )
+
+   (test-suite
+    "type-table tests"
+    ;; tc-app-apply
+    (tc/type-table (apply values '(0))
+     ([values (t:-> (-val 0) (-val 0))]))
+    (tc/type-table (apply + '(0))
+     ([values (t:-> (-val 0) (-val 0))]))
+
+    ;; tc-app-hetero
+    (tc/type-table (void ;; vector-ref on heterogeneous vectors
+                     (vector-ref (ann '#(A B) (Vector 'A 'B)) 0)
+                     (unsafe-vector-ref (ann (vector 'A 'B) (Vector 'A 'B)) 0)
+                     (unsafe-vector*-ref (ann (vector 'A 'B) (Vector 'A 'B)) 1))
+     ([vector-ref (t:-> (-vec* (-val 'A) (-val 'B)) -Fixnum (-val 'A))]
+      [unsafe-vector-ref (t:-> (-vec* (-val 'A) (-val 'B)) -Fixnum (-val 'A))]
+      [unsafe-vector*-ref (t:-> (-vec* (-val 'A) (-val 'B)) -Fixnum (-val 'B))]))
+    (tc/type-table (void ;; vector-set! on heterogeneous vectors
+                     (vector-set! (ann (vector 'A 'B) (Vector Symbol 'B)) 0 'X)
+                     (unsafe-vector-set! (ann (vector 'C 'D) (Vector Symbol 'D)) 0 'X)
+                     (unsafe-vector*-set! (ann (vector 'E 'F) (Vector 'E Symbol)) 1 'X))
+     ([vector-set! (t:-> (-vec* -Symbol (-val 'B)) -Fixnum -Symbol -Void)]
+      [unsafe-vector-set! (t:-> (-vec* -Symbol (-val 'D)) -Fixnum -Symbol -Void)]
+      [unsafe-vector*-set! (t:-> (-vec* (-val 'E) -Symbol) -Fixnum -Symbol -Void)]))
+    (tc/type-table (vector-set! (ann (vector 'a 'b) (Vector Symbol Symbol)) (+ -1 2) 'c)
+     ;; test when the index for vector-set! isn't know
+     ([vector-set! (t:-> (-vec* -Symbol -Symbol) -Fixnum (-val 'c) -Void)]))
+    (tc/type-table (void ;; vector constructor, returning heterogeneous vector
+                     (ann (vector 'A 'B) (Vectorof Symbol))
+                     (ann (vector-immutable 'A 'B) (Vectorof Symbol)))
+     ([vector (t:-> -Symbol -Symbol (-vec* -Symbol -Symbol))]
+      [vector-immutable (t:-> -Symbol -Symbol (-vec* -Symbol -Symbol))]))
+    (tc/type-table (void ;; vector constructor, returning heterogeneous vector
+                     (ann (vector 'A 'B) (Vector 'A 'B))
+                     (ann (vector-immutable 'A 'B) (Vector 'A 'B)))
+     ([vector (t:-> (-val 'A) (-val 'B) (-vec* (-val 'A) (-val 'B)))]
+      [vector-immutable (t:-> (-val 'A) (-val 'B) (-vec* (-val 'A) (-val 'B)))]))
+    (tc/type-table (void ;; vector constructor, no expected type
+                     (vector 'A 'B)
+                     (vector-immutable 'A 'B))
+     ([vector (t:-> -Symbol -Symbol (-vec* -Symbol -Symbol))]
+      [vector-immutable (t:-> -Symbol -Symbol (-vec* -Symbol -Symbol))]))
+
+    ;; tc-app-list
+    ;;; list
+    (tc/type-table (ann (list 'A 'B) (List Symbol Symbol))
+     ([list (t:-> -Symbol -Symbol (-lst* -Symbol -Symbol))]))
+    (tc/type-table (ann (list 'A) Any)
+     ([list (t:-> Univ (-lst* Univ))]))
+    (tc/type-table (list 'A 'B)
+     ([list (t:-> (-val 'A) (-val 'B) (-lst* (-val 'A) (-val 'B)))]))
+    ;;; list*
+    (tc/type-table (list* #true #false)
+     ([list* (t:-> (-val #true) (-val #false) (-pair (-val #true) (-val #false)))]))
+    (tc/type-table (list* "A" "B" (list "C"))
+     ([list* (t:-> -String -String (-lst* -String) (-lst* -String -String -String))]))
+    ;;; reverse
+    (tc/type-table (ann (reverse '("A" "B")) (Listof String))
+     ([reverse (t:-> (-lst -String) (-lst -String))]))
+    (tc/type-table (ann (reverse '(A B)) (List 'B 'A))
+     ([reverse (t:-> (-lst* (-val 'A) (-val 'B)) (-lst* (-val 'B) (-val 'A)))]))
+    (tc/type-table (reverse (ann '(A B) (List 'A 'B)))
+     ([reverse (t:-> (-lst* (-val 'A) (-val 'B)) (-lst* (-val 'B) (-val 'A)))]))
+    (tc/type-table (reverse (ann '("A" "B") (Listof String)))
+     ([reverse (t:-> (-lst -String) (-lst -String))]))
+
+    ;; tc-app-special
+    (tc/type-table (false? #true)
+     ([false? (t:-> Univ -Boolean)]))
+    (tc/type-table (false? #false)
+     ([false? (t:-> Univ -Boolean)]))
+    (tc/type-table (not #true)
+     ([not (t:-> Univ -Boolean)]))
+    (tc/type-table (not #false)
+     ([not (t:-> Univ -Boolean)]))
+
+    ;; tc-app-values
+    (tc/type-table (values 0)
+     ([values (t:-> (-val 0) (-values (list (-val 0))))]))
+    ;; TODO tests fail because propsets are somehow different (2017-12-06)
+    ;(tc/type-table (values 0 0)
+    ; ([values (t:-> (-val 0) (-val 0) (-values (list (-val 0 ) (-val 0))))]))
+    ;(tc/type-table (call-with-values (λ () 'A) symbol->string)
+    ; ([call-with-values (->* (list (t:-> (-val 'A)) (t:-> -Symbol -String)) -String)]))
+    ;(tc/type-table (call-with-values (λ () "hello") (λ: ((x : String)) "world"))
+    ; ([call-with-values (t:-> (t:-> -String) (t:-> -String -String) -String)]))
+    ;(tc/type-table (call-with-values (λ () (values 0 0)) (λ: ((x : Zero) (y : Zero)) 0))
+    ; ([call-with-values (t:-> (t:-> (-values (list (-val 0) (-val 0))))
+    ;                          (t:-> (-val 0) (-val 0) (-val 0))
+    ;                          (-val 0))]))
+    ;(tc/type-table (call-with-values (λ () (values "a" "b")) (λ: ((x : String) (y : String)) (string-append x y)))
+    ; ([call-with-values (t:-> (t:-> (-values (list -String -String)))
+    ;                          (t:-> -String -String -String)
+    ;                          -String)]))
+   )
   ))