From c2fafe90e076a9ab0d306fcf976bad51a9f630f7 Mon Sep 17 00:00:00 2001
From: Eric Dobson <eric.n.dobson@gmail.com>
Date: Sat, 15 Mar 2014 10:07:18 -0700
Subject: [PATCH] Make version of tc-err that checks return types.

original commit: bbec6422840bcd6c11530de441b851801eb4d974
---
 .../typed-racket/utils/tc-utils.rkt           |  16 +-
 .../typed-racket/unit-tests/class-tests.rkt   |  99 +++++++--
 .../unit-tests/typecheck-tests.rkt            | 188 ++++++++++++------
 3 files changed, 226 insertions(+), 77 deletions(-)

diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/tc-utils.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/tc-utils.rkt
index f41dc8a1..4e793c27 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/tc-utils.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/tc-utils.rkt
@@ -24,6 +24,8 @@ don't depend on any other portion of the system
          locate-stx
          warn-unreachable
 
+         reset-errors!
+         report-first-error
          report-all-errors
          tc-error/fields
          tc-error/delayed
@@ -102,13 +104,21 @@ don't depend on any other portion of the system
     (values (lambda () (set-box! v delayed-errors))
             (lambda () (set! delayed-errors (unbox v))))))
 
+(define (reset-errors!) (set! delayed-errors null))
+
+(define (report-first-error)
+  (match (reverse delayed-errors)
+    [(list) (void)]
+    [(cons (struct err (msg stx)) _)
+     (reset-errors!)
+     (raise-typecheck-error msg stx)]))
+
 (define (report-all-errors)
-  (define (reset!) (set! delayed-errors null))
   (match (reverse delayed-errors)
     [(list) (void)]
     ;; if there's only one, we don't need multiple-error handling
     [(list (struct err (msg stx)))
-     (reset!)
+     (reset-errors!)
      (raise-typecheck-error msg stx)]
     [l
      (let ([stxs
@@ -117,7 +127,7 @@ don't depend on any other portion of the system
                                (λ (e) ((error-display-handler) (exn-message e) e))])
                 (raise-typecheck-error (err-msg e) (err-stx e)))
               (err-stx e))])
-       (reset!)
+       (reset-errors!)
        (unless (null? stxs)
          (raise-typecheck-error (format "Summary: ~a errors encountered"
                                         (length stxs))
diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/class-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/class-tests.rkt
index 9b2455c0..a1d5710b 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/class-tests.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/class-tests.rkt
@@ -51,6 +51,7 @@
                           (init x)
                           (define/public (m x) 0)))
              (void))
+           #:ret (ret -Void)
            #:msg #rx"superclass expression should produce a class"]
    ;; Method using argument type
    [tc-e (let ()
@@ -81,6 +82,7 @@
                           (init [x 0])
                           (define/public (m x) (send this z))))
              (void))
+           #:ret (ret -Void)
            #:msg #rx"method not understood.*method name: z"]
    ;; Send to other methods
    [tc-e (let ()
@@ -125,11 +127,13 @@
                     (super-new)
                     (field [x : String "foo"])))
              'not-string)
+           #:ret (ret -Void)
            #:msg #rx"set-field! only allowed with"]
    ;; fails, field's default value has wrong type
    [tc-err (class object% (super-new)
              (: x Symbol)
              (field [x "foo"]))
+           #:ret (ret (-class #:field ([x -Symbol])))
            #:msg #rx"expected: Symbol.*given: String"]
    ;; Fail, field access to missing field
    [tc-err (let ()
@@ -138,6 +142,7 @@
                           (super-new)
                           (define/public (m) (get-field n this))))
              (void))
+           #:ret (ret -Void)
            #:msg #rx"missing an expected field.*field: n"]
    ;; Fail, conflict with parent field
    [tc-err (let ()
@@ -153,6 +158,7 @@
                           (field [n 17])
                           (super-new)))
              (void))
+           #:ret (ret -Void)
            #:msg #rx"defines conflicting public field n"]
    ;; Fail, conflict with parent method
    [tc-err (let ()
@@ -165,6 +171,7 @@
                           (super-new)
                           (define/public (m) 17)))
              (void))
+           #:ret (ret -Void)
            #:msg #rx"defines conflicting public method m"]
    ;; Inheritance
    [tc-e (let ()
@@ -181,6 +188,7 @@
          -Void]
    ;; fail, superclass expression is not a class with no expected type
    [tc-err (class "foo" (super-new))
+           #:ret (ret (-class))
            #:msg "expected: a class"]
    ;; should fail, too many methods
    [tc-err (let ()
@@ -189,6 +197,7 @@
                           (super-new)
                           (define/public (m) 0)))
              (void))
+           #:ret (ret -Void)
            #:msg #rx"public method m that is not in the expected type"]
    ;; same as previous
    [tc-err (let ()
@@ -197,6 +206,7 @@
                           (define/public (m x) (add1 x))
                           (define/public (n) 0)))
              (void))
+           #:ret (ret -Void)
            #:msg #rx"public method n that is not in the expected type"]
    ;; fails, too many inits
    [tc-err (let ()
@@ -204,6 +214,7 @@
              (define c% (class object% (super-new)
                           (init x)))
              (void))
+           #:ret (ret -Void)
            #:msg #rx"initialization argument x that is not in the expected type"]
    ;; fails, init should be optional but is mandatory
    [tc-err (let ()
@@ -211,6 +222,7 @@
              (define c% (class object% (super-new)
                           (init str)))
              (void))
+           #:ret (ret -Void)
            #:msg #rx"missing optional init argument str"]
    ;; fails, too many fields
    [tc-err (let ()
@@ -218,6 +230,7 @@
              (define c% (class object% (super-new)
                           (field [str "foo"] [x 0])))
              (void))
+           #:ret (ret -Void)
            #:msg #rx"public field x that is not in the expected type"]
    ;; test that an init with no annotation still type-checks
    ;; (though it will have the Any type)
@@ -262,6 +275,7 @@
                  (define/public (m) 0)))
 
              (mixin arg-class%))
+           #:ret (ret (-class #:method ([m (t:-> -Integer)] [n (t:-> -String)])))
            #:msg #rx"missing public method n"]
    ;; Fail, bad mixin argument
    [tc-err (let ()
@@ -282,6 +296,7 @@
 
              (mixin arg-class%)
              (void))
+           #:ret (ret -Void)
            #:msg #rx"expected: \\(Class \\(m \\(-> Symbol\\)\\)\\)"]
    ;; classes that don't use define/public directly
    [tc-e (let ()
@@ -316,6 +331,7 @@
              (: c% (Class (init [x Integer])))
              (define c% (class object% (init x)))
              (void))
+           #:ret (ret -Void)
            #:msg #rx"typed classes must call super-new"]
    ;; fails, non-top-level super-new
    ;; FIXME: this case also spits out additional untyped identifier
@@ -324,6 +340,7 @@
              (: c% (Class (init [x Integer])))
              (define c% (class object% (let () (super-new)) (init x)))
              (void))
+           #:ret (ret -Void)
            #:msg #rx"typed classes must call super-new"]
    ;; fails, bad super-new argument
    [tc-err (let ()
@@ -332,6 +349,7 @@
              (: d% (Class))
              (define d% (class c% (super-new [x "bad"])))
              (void))
+           #:ret (ret -Void)
            #:msg #rx"expected: Symbol.*given: String"]
    ;; test override
    [tc-e (let ()
@@ -361,7 +379,8 @@
              (define d% (class object% (super-new)
                           (define/override (m y)
                             (string-append (assert y string?) "foo"))))
-             (void))]
+             (void))
+           #:ret (ret -Void)]
    ;; local field access and set!
    [tc-e (let ()
            (: c% (Class (field [x Integer])
@@ -403,6 +422,7 @@
                           (define/public (m y) 'a)
                           (string-append (string->symbol "a") "a")))
              (void))
+           #:ret (ret -Void)
            #:msg #rx"expected: String.*given: Symbol"]
    ;; fails, ill-typed method call
    [tc-err (let ()
@@ -411,6 +431,7 @@
                           (define/public (m y) 'a)
                           (m "foo")))
              (void))
+           #:ret (ret -Void)
            #:msg #rx"expected: Symbol.*given: String"]
    ;; fails, ill-typed field access
    [tc-err (let ()
@@ -419,6 +440,7 @@
                           (field [f "foo"])
                           (set! f 'a)))
              (void))
+           #:ret (ret -Void)
            #:msg #rx"expected: String.*given: 'a"]
    ;; test private field
    [tc-e (let ()
@@ -444,12 +466,14 @@
              (: x Symbol)
              (define x 'a)
              (set! x "foo"))
+           #:ret (ret (-class))
            #:msg #rx"expected: Symbol.*given: String"]
    ;; fails, bad private field default
    [tc-err (class object%
              (super-new)
              (: x Symbol)
              (define x "foo"))
+           #:ret (ret (-class))
            #:msg #rx"expected: Symbol.*given: String"]
    ;; ok, synthesis works on private fields
    [tc-e (class object% (super-new)
@@ -470,17 +494,20 @@
              (define/private (x) 'a)
              (: m (-> String))
              (define/public (m) (x)))
+           #:ret (ret (-class #:method ([m (t:-> -String)])))
            #:msg #rx"expected: String.*given: Symbol"]
    ;; fails, not enough annotation on private
    [tc-err (class object% (super-new)
              (define/private (x) 3)
              (: m (-> Integer))
              (define/public (m) (x)))
+           #:ret (ret (-class #:method ([m (t:-> -Integer)])))
            #:msg #rx"Cannot apply expression of type Any"]
    ;; fails, ill-typed private method implementation
    [tc-err (class object% (super-new)
              (: x (-> Symbol))
              (define/private (x) "bad result"))
+           #:ret (ret (-class))
            #:msg #rx"expected: Symbol.*given: String"]
    ;; test optional init arg
    [tc-e (let ()
@@ -508,6 +535,7 @@
                           (: x Integer)
                           (init [x 0])))
              (void))
+           #:ret (ret -Void)
            #:msg #rx"optional init argument x that is not in the expected type"]
    ;; fails, mandatory init not provided
    [tc-err (let ()
@@ -515,6 +543,7 @@
                           (: x Integer)
                           (init x)))
              (new d%))
+           #:ret (ret (-object #:init ([x -Integer #f])))
            #:msg #rx"value not provided for named init arg x"]
    ;; test that provided super-class inits don't count
    ;; towards the type of current class
@@ -532,9 +561,11 @@
                                  (: x Integer)
                                  (init x))
                           (super-new [x 3])))
-             (new c% [x 5]))]
+             (new c% [x 5]))
+           #:ret (ret (-object))]
    ;; fails, super-new can only be called once per class
-   [tc-err (class object% (super-new) (super-new))]
+   [tc-err (class object% (super-new) (super-new))
+           #:ret (ret (-class))]
    ;; test passing an init arg to super-new
    [tc-e (let ()
            (define c% (class (class object% (super-new)
@@ -552,9 +583,11 @@
                     (init x))
              (: x String)
              (init x)
-             (super-new [x x]))]
+             (super-new [x x]))
+           #:ret (ret (-class #:init ([x -String #f])))]
    ;; fails, superclass does not accept this init arg
    [tc-err (class object% (super-new [x 3]))
+           #:ret (ret (-class))
            #:msg "not accepted by superclass"]
    ;; test inherit method
    [tc-e (let ()
@@ -597,16 +630,19 @@
    [tc-err (class (class object% (super-new))
              (super-new)
              (inherit-field [y x]))
+           #:ret (ret (-class))
            #:msg #rx"superclass missing field"]
    ;; fails, missing super method for inherit
-   [tc-err (class (class object% (super-new)) (super-new) (inherit z))]
+   [tc-err (class (class object% (super-new)) (super-new) (inherit z))
+           #:ret (ret (-class))]
    ;; fails, bad argument type to inherited method
    [tc-err (class (class object% (super-new)
                     (: m (Integer -> Integer))
                     (define/public (m x) (add1 x)))
              (super-new)
              (inherit m)
-             (m "foo"))]
+             (m "foo"))
+           #:ret (ret (-class #:method ([m (t:-> -Integer -Integer)])))]
    ;; test that keyword methods type-check
    ;; FIXME: send with keywords does not work yet
    [tc-e (let ()
@@ -745,7 +781,8 @@
              (define c% (class object% (super-new)
                           (: i Integer)
                           (init ([i j]))))
-             (new c% [i 5]))]
+             (new c% [i 5]))
+           #:ret (ret (-object #:init ([j -Integer #f])))]
    ;; test init default values
    [tc-e (let ()
            (class object% (super-new)
@@ -756,7 +793,8 @@
    ;; fails, bad default init value
    [tc-err (class object% (super-new)
              (: z Integer)
-             (init [z "foo"]))]
+             (init [z "foo"]))
+           #:ret (ret (-class #:init ([z -Integer #t])))]
    ;; test init field default value
    [tc-e (let ()
            (define c% (class object% (super-new)
@@ -767,7 +805,8 @@
    ;; fails, wrong init-field default
    [tc-err (class object% (super-new)
              (: x Integer)
-             (init-field ([x y] "foo")))]
+             (init-field ([x y] "foo")))
+           #:ret (ret (-class #:init ([y -Integer #t]) #:field ([y -Integer])))]
    ;; test type-checking method with internal/external
    [tc-err (let ()
              (: c% (Class [n (Integer -> Integer)]))
@@ -786,6 +825,7 @@
    [tc-err (class object% (super-new)
              (define/public (m) (n))
              (define/public (n x) 0))
+           #:ret (ret (-class #:method ([m (t:-> -Bottom)] [n (t:-> Univ -Zero : -true-filter)])))
            #:msg #rx"since it is not a function type"]
    ;; test type-checking for classes without any
    ;; internal type annotations on methods
@@ -834,7 +874,12 @@
              (define (f cls)
                (class cls (super-new)
                  (field [x 5])))
-             (inst f #:row (field [x Integer])))]
+             (inst f #:row (field [x Integer])))
+           #:ret (ret (t:-> (-class 
+                              #:row (make-Row null `([x ,-Integer]) null null #f))
+                            (-class
+                              #:row (make-Row null `([x ,-Integer]) null null #f)
+                              #:field ([x -Integer]))))]
    ;; fails, mixin argument is missing required field
    [tc-err (let ()
              (: f (All (A #:row (field x))
@@ -847,7 +892,10 @@
              (define instantiated
                (inst f #:row (field [y Integer])))
              (instantiated
-              (class object% (super-new))))]
+              (class object% (super-new))))
+           #:ret (ret (-class
+                        #:row (make-Row null (list (list 'y -Integer)) null null #f)
+                        #:field ([x -Integer])))]
    ;; fails, the argument object lacks required fields (with inference)
    [tc-err (let ()
              (: mixin (All (r #:row)
@@ -855,6 +903,8 @@
                              (Class (field [x Any]) #:row-var r))))
              (define (mixin cls) cls)
              (mixin object%))
+           #:ret (ret (-class #:row (make-Row null null null null #f)
+                              #:field ([x Univ])))
            #:msg (regexp-quote "expected: (Class (field (x Any)))")]
    ;; mixin application succeeds
    [tc-e (let ()
@@ -894,7 +944,12 @@
              (define (f cls)
                (class cls (super-new)
                  (field [x 5])))
-             (inst f #:row (field [x Integer])))]
+             (inst f #:row (field [x Integer])))
+           #:ret (ret (t:-> (-class 
+                              #:row (make-Row null `([x ,-Integer]) null null #f))
+                            (-class
+                              #:row (make-Row null `([x ,-Integer]) null null #f)
+                              #:field ([x -Integer]))))]
    ;; Check simple use of pubment
    [tc-e (let ()
            (define c%
@@ -985,6 +1040,7 @@
                  (define/augment (m x)
                    (string-append x "bar"))))
              (send (new c%) m 'b))
+           #:ret (ret -Symbol)
            #:msg #rx"expected: String.*given: Symbol"]
    ;; Fail, bad inner default
    [tc-err (class object%
@@ -992,6 +1048,8 @@
              (: m (Symbol -> Symbol))
              (define/pubment (m x)
                (inner "foo" m x)))
+           #:ret (ret (-class #:method ([m (t:-> -Symbol -Symbol)])
+                              #:augment ([m (t:-> -Symbol -Symbol)])))
            #:msg #rx"expected: Symbol.*given: String"]
    ;; Fail, wrong number of arguments to inner
    [tc-err (class object%
@@ -999,6 +1057,8 @@
              (: m (Integer -> Integer))
              (define/pubment (m x)
                (inner 3 m)))
+           #:ret (ret (-class #:method ([m (t:-> -Integer -Integer)])
+                              #:augment ([m (t:-> -Integer -Integer)])))
            #:msg #rx"wrong number of arguments provided.*expected: 2"]
    ;; Fail, bad augment type
    [tc-err (let ()
@@ -1013,6 +1073,7 @@
                  (super-new)
                  (define/augment (m x) "bad type")))
              (void))
+           #:ret (ret -Void)
            #:msg #rx"expected: Symbol.*given: String"]
    ;; Fail, cannot augment non-augmentable method
    [tc-err (let ()
@@ -1026,6 +1087,7 @@
                  (super-new)
                  (define/augment (m x) 1)))
              (void))
+           #:ret (ret -Void)
            #:msg #rx"superclass missing augmentable method m"]
    ;; Pubment with separate internal/external names
    ;; FIXME: broken right now due to : macro changes
@@ -1059,6 +1121,7 @@
                  (: x Symbol)
                  (init-field x)))
              (void))
+           #:ret (ret -Void)
            #:msg #rx"expected: String"]
    ;; test polymorphic class
    [tc-e (let ()
@@ -1079,6 +1142,7 @@
                  (init-field x)
                  (set! x "a")))
              (void))
+           #:ret (ret -Void)
            #:msg #rx"expected: A.*given: String"]
    ;; test polymorphism with keyword
    [tc-e (let ()
@@ -1118,18 +1182,21 @@
              (super-new)
              (: m (X -> X))
              (define/public (m x) "a"))
+           #:ret (ret (-poly (X) (-class #:method ([m (t:-> X X)]))))
            #:msg #rx"expected: X.*given: String"]
    ;; fails because default init value cannot be polymorphic
    [tc-err (class object%
              #:forall (Z)
              (super-new)
              (init-field [x : Z] [y : Z 0]))
+           #:ret (ret (-poly (Z) (-class #:init-field ([x Z #f] [y Z #t]))))
            #:msg #rx"Default init value has wrong type"]
    ;; fails because default field value cannot be polymorphic
    [tc-err (class object%
              #:forall (Z)
              (super-new)
              (field [x : Z "a"]))
+           #:ret (ret (-poly (Z) (-class #:field ([x Z]))))
            #:msg #rx"expected: Z.*given: String"]
    ;; test in-clause type annotations (next several tests)
    [tc-e (let ()
@@ -1174,6 +1241,7 @@
              (super-new)
              (: x String)
              (field [x : Symbol 0]))
+           #:ret (ret (-class #:field ([x -Symbol])))
            #:msg #rx"duplicate type annotation.*new type: String"]
    ;; fails, expected type and annotation don't match
    [tc-err (let ()
@@ -1181,11 +1249,15 @@
              (define c% (class object% (super-new)
                           (field [x : Symbol 'a])))
              (void))
+           #:ret (ret -Void)
            #:msg #rx"expected: \\(Class \\(field \\(x String"]
    ;; fails, but make sure it's not an internal error
    [tc-err (class object% (super-new)
              (define/pubment (foo x) 0)
              (define/public (g x) (foo 3)))
+           #:ret (ret (-class #:method ([g (t:-> Univ -Bottom)]
+                                        [foo (t:-> Univ -Zero : -true-filter)])
+                              #:augment ([foo top-func])))
            #:msg #rx"Cannot apply expression of type Any"]
    ;; the next several tests are for positional init arguments
    [tc-e (let ()
@@ -1250,6 +1322,7 @@
                           (super-new)
                           (init-rest [rst : (List Symbol)])))
              (make-object c% "wrong"))
+           #:ret (ret (make-Instance (make-Class #f null null null null (-Tuple (list -Symbol)))))
            #:msg #rx"expected: Symbol.*given: String"]
    ;; PR 14408, test init-field order
    [tc-e (let ()
@@ -1272,6 +1345,7 @@
          -Void]
    ;; fail, too many positional arguments to superclass
    [tc-err (class object% (super-make-object "foo"))
+           #:ret (ret (-class))
            #:msg #rx"too many positional init arguments"]
    ;; check that case-lambda methods work
    [tc-e (let ()
@@ -1295,6 +1369,7 @@
              (: m (case-> (Any -> Integer)))
              (public m)
              (define m (case-lambda [(x) "bad"])))
+           #:ret (ret (-class #:method [(m (t:-> Univ -Integer))]))
            #:msg #rx"expected: Integer.*given: String"]
    ;; test that rest args work
    [tc-e (let ()
diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
index a7dec8b1..4f0157e1 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
@@ -37,7 +37,7 @@
     syntax/parse
     (for-template (only-in typed-racket/typed-racket do-standard-inits))
     (typecheck typechecker)
-    (utils mutated-vars)
+    (utils mutated-vars tc-utils)
     (env mvar-env))
   (provide
     test-literal test-literal/fail
@@ -79,21 +79,34 @@
                #:expected golden
                "tc-expr did not return the expected value"))))
 
-  ;; test/fail syntax? (or/c string? regexp?) (option/c tc-results?) -> void?
-  ;; Checks that the expression doesn't typecheck using the expected type and the golden message
-  (define (test/fail code message expected)
-    (with-handlers ([exn:fail:syntax?
-                     (lambda (exn)
-                       (when message
-                         (unless (regexp-match? message (exn-message exn))
-                           (raise (cross-phase-failure
-                                    #:actual (exn-message exn)
-                                    #:expected message
-                                    "tc-expr raised the wrong error message")))))])
-      (define result (tc (tr-expand code) expected))
-      (raise (cross-phase-failure
-               #:actual result
-               "tc-expr did not raise an error"))))
+  ;; test/fail syntax? tc-results? (or/c string? regexp?) (option/c tc-results?) -> void?
+  ;; Checks that the expression doesn't typecheck using the expected type, returns the golden type,
+  ;; and raises an error message matching the golden message
+  (define (test/fail code golden message expected)
+    (dynamic-wind
+      void
+      (λ ()
+        (with-handlers ([exn:fail:syntax?
+                         (lambda (exn)
+                           (when message
+                             (unless (regexp-match? message (exn-message exn))
+                               (raise (cross-phase-failure
+                                        #:actual (exn-message exn)
+                                        #:expected message
+                                        "tc-expr raised the wrong error message")))))])
+          (define result
+            (parameterize ([delay-errors? #t])
+              (tc (tr-expand code) expected)))
+          (unless (equal? golden result)
+            (raise (cross-phase-failure
+                     #:actual result
+                     #:expected golden
+                     "tc-expr did not return the expected value")))
+          (report-first-error)
+          (raise (cross-phase-failure
+                   #:actual result
+                   "tc-expr did not raise an error"))))
+      (λ () (reset-errors!))))
 
 
   ;; test-literal syntax? tc-results? (option/c tc-results?) -> void?
@@ -153,6 +166,10 @@
     (pattern ty:expr #:attr v #'(ret ty))
     (pattern (~seq #:ret r:expr) #:attr v #'r))
 
+  (define-splicing-syntax-class err-return
+    (pattern (~seq #:ret r:expr) #:attr v #'r)
+    (pattern (~seq) #:attr v #'(ret -Bottom)))
+
   (define-splicing-syntax-class expected
     (pattern (~seq #:expected v:expr))
     (pattern (~seq) #:attr v #'#f))
@@ -205,10 +222,10 @@
 ;; check that typechecking this expression fails
 (define-syntax (tc-err stx)
   (syntax-parse stx
-    [(_ code:expr ex:expected msg:expected-msg)
+    [(_ code:expr ret:err-return ex:expected msg:expected-msg)
      (quasisyntax/loc stx
         (test-phase1 #,(syntax/loc #'code (FAIL code))
-           (test/fail (quote-syntax code) msg.v ex.v)))]))
+           (test/fail (quote-syntax code) ret.v msg.v ex.v)))]))
 
 (define-syntax (tc-l/err stx)
   (syntax-parse stx
@@ -256,7 +273,7 @@
   ;; Needed for constructing TR types in expected values
   (for-syntax
     (rep type-rep filter-rep object-rep)
-    (rename-in (types abbrev union numeric-tower filter-ops utils)
+    (rename-in (types abbrev union numeric-tower filter-ops utils resolve)
                [Un t:Un]
                [-> t:->])))
 
@@ -392,8 +409,12 @@
         [tc-e (void 3 4) -Void]
         [tc-e (void #t #f '(1 2 3)) -Void]
         [tc-e/t #() (make-HeterogeneousVector (list))]
-        [tc-err #(3) #:expected (ret (make-HeterogeneousVector (list -Integer -Integer)))]
-        [tc-err #(3 4 5) #:expected (ret (make-HeterogeneousVector (list -Integer -Integer)))]
+        [tc-err #(3)
+           #:ret (ret (make-HeterogeneousVector (list -Integer -Integer)))
+           #:expected (ret (make-HeterogeneousVector (list -Integer -Integer)))]
+        [tc-err #(3 4 5)
+           #:ret (ret (make-HeterogeneousVector (list -Integer -Integer)))
+           #:expected (ret (make-HeterogeneousVector (list -Integer -Integer)))]
         [tc-e/t #(3 4 5) (make-HeterogeneousVector (list -Integer -Integer -Integer))]
         [tc-e/t '(2 3 4) (-lst* -PosByte -PosByte -PosByte)]
         [tc-e/t '(2 3 #t) (-lst* -PosByte -PosByte (-val #t))]
@@ -401,7 +422,9 @@
         [tc-e (vector 2 "3" #t) (make-HeterogeneousVector (list -Integer -String -Boolean))]
         [tc-e (vector) (make-HeterogeneousVector (list))]
         [tc-e (vector) (make-HeterogeneousVector (list)) #:expected tc-any-results]
-        [tc-err (vector) #:expected (ret -Integer)]
+        [tc-err (vector)
+           #:ret (ret -Integer)
+           #:expected (ret -Integer)]
         [tc-e (vector-immutable 2 "3" #t) (make-HeterogeneousVector (list -Integer -String -Boolean))]
         [tc-e (make-vector 4 1) (-vec -Integer)]
         [tc-e (build-vector 4 (lambda (x) 1)) (-vec -Integer)]
@@ -619,7 +642,8 @@
         [tc-err (let: ([x : (U String 'foo) 'foo])
                       (if (string=? x 'foo)
                           "foo"
-                          x))]
+                          x))
+          #:ret (ret (t:Un -String (-val 'foo)))]
 
         [tc-e (let: ([x : (U String 5) 5])
                       (if (eq? x 5)
@@ -764,15 +788,19 @@
                   (lambda: ([x : Any]) (if (p? x) x 12)))
                 (t:-> Univ Univ)]
 
-        [tc-e (not 1) #:ret (ret -Boolean -false-filter)]
+        [tc-e (not 1)
+          #:ret (ret -Boolean -false-filter)]
 
-        [tc-err ((lambda () 1) 2)]
+        [tc-err ((lambda () 1) 2)
+          #:ret (ret (-val 1) -true-filter)]
         [tc-err (apply (lambda () 1) '(2))]
-        [tc-err ((lambda: ([x : Any] [y : Any]) 1) 2)]
+        [tc-err ((lambda: ([x : Any] [y : Any]) 1) 2)
+          #:ret (ret (-val 1) -true-filter)]
         [tc-err (map map '(2))]
         [tc-err ((plambda: (a) ([x : (a -> a)] [y : a]) (x y)) 5)]
         [tc-err ((plambda: (a) ([x : a] [y : a]) x) 5)]
-        [tc-err (ann 5 : String)]
+        [tc-err (ann 5 : String)
+          #:ret (ret -String -true-filter)]
 
         ;; these don't work because the type annotation gets lost in marshalling
         #|
@@ -795,7 +823,8 @@
 
         [tc-err (let ([x (add1 5)])
                   (set! x "foo")
-                  x)]
+                  x)
+          #:ret (ret -Integer)]
         ;; w-c-m
         [tc-e/t (with-continuation-mark
                   ((inst make-continuation-mark-key Symbol)) 'mark
@@ -818,12 +847,15 @@
                                 (lambda: ([x : Number]) (+ x 1)))
               -Number]
         [tc-err (call-with-values (lambda () 1)
-                                  (lambda: () 2))]
+                                  (lambda: () 2))
+          #:ret (ret -PosByte -true-filter)]
 
         [tc-err (call-with-values (lambda () (values 2))
-                                  (lambda: ([x : Number] [y : Number]) (+ x y)))]
+                                  (lambda: ([x : Number] [y : Number]) (+ x y)))
+          #:ret (ret -Number)]
         [tc-err (call-with-values 5
-                                  (lambda: ([x : Number] [y : Number]) (+ x y)))]
+                                  (lambda: ([x : Number] [y : Number]) (+ x y)))
+          #:ret (ret -Number)]
         [tc-err (call-with-values (lambda () (values 2))
                                   5)]
         [tc-err (call-with-values (lambda () (values 2 1))
@@ -910,13 +942,15 @@
         [tc-err (apply append (list 1) (list 2) (list 3) (list (list 1) "foo"))]
         [tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list 1))) (-lst -PosByte)]
         [tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list "foo"))) (-lst (t:Un -String -PosByte))]
-        [tc-err (plambda: (b ...) [y : b ... b] (apply append (map list y)))]
+        [tc-err (plambda: (b ...) [y : b ... b] (apply append (map list y)))
+         #:ret (ret (-polydots (b) (->... (list) (b b) -Bottom)) -true-filter)]
         [tc-e/t (plambda: (b ...) [y : (Listof Integer) ... b] (apply append y))
                 (-polydots (b) (->... (list) ((-lst -Integer) b) (-lst -Integer)))]
 
         [tc-err (plambda: (a ...) ([z : String] . [w : Number ... a])
                           (apply (plambda: (b) ([x : Number] . [y : Number ... a]) x)
-                                 1 1 1 1 w))]
+                                 1 1 1 1 w))
+         #:ret (ret (-polydots (a) (->... (list -String) (-Number a) -Bottom)) -true-filter)]
 
         [tc-err (plambda: (a ...) ([z : String] . [w : Number])
                           (apply (plambda: (b) ([x : Number] . [y : Number ... a]) x)
@@ -956,21 +990,25 @@
 
         ;; error tests
         [tc-err (+ 3 #f)]
-        [tc-err (let: ([x : Number #f]) x)]
-        [tc-err (let: ([x : Number #f]) (+ 1 x))]
+        [tc-err (let: ([x : Number #f]) x)
+          #:ret (ret -Number)]
+        [tc-err (let: ([x : Number #f]) (+ 1 x))
+          #:ret (ret -Number)]
 
         [tc-err
          (let: ([x : Any '(foo)])
                (if (null? x) 1
                    (if (list? x)
                        (add1 x)
-                       12)))]
+                       12)))
+         #:ret (ret -PosByte)]
 
         [tc-err (let*: ([x : Any 1]
                         [f : (-> Void) (lambda () (set! x 'foo))])
                        (if (number? x)
                            (begin (f) (add1 x))
-                           12))]
+                           12))
+          #:ret (ret -PosByte)]
 
         [tc-err (ann 3 (Rec a a))]
         [tc-err (ann 3 (Rec a (U a 3)))]
@@ -1071,9 +1109,11 @@
         [tc-e (hash-has-key? (make-hash '((1 . 2))) 1) -Boolean]
 
         [tc-err (let: ([fact : (Number -> Number) (lambda: ([n : Number]) (if (zero? n) 1 (* n (fact (- n 1)))))])
-                        (fact 20))]
+                        (fact 20))
+          #:ret (ret -Number)]
 
-        [tc-err (ann (lambda: ([x : Any]) #f) (Any -> Boolean : String))]
+        [tc-err (ann (lambda: ([x : Any]) #f) (Any -> Boolean : String))
+          #:ret (ret (make-pred-ty -String) -true-filter)]
 
 
         [tc-e (time (+ 3 4)) -PosIndex]
@@ -1133,11 +1173,13 @@
                 (vector-ref #("a" "b") (sub1 x))
                 (vector-ref #("a" "b") (- x 1)))
               -String]
-        [tc-err (string-append "bar" (if (zero? (ann 0.0 Float)) #f "foo"))]
+        [tc-err (string-append "bar" (if (zero? (ann 0.0 Float)) #f "foo"))
+          #:ret (ret -String)]
         [tc-err (do: : Void
                      ([j : Natural (+ i 'a) (+ j i)])
                      ((>= j 10))
-                     #f)]
+                     #f)
+          #:ret (ret -Void -no-filter -no-obj)]
         [tc-err (apply +)]
         [tc-e/t
          (let ([x eof])
@@ -1147,7 +1189,8 @@
          (make-pred-ty (-val eof))]
         [tc-e ((inst map Number (Pairof Number Number)) car (ann (list (cons 1 2) (cons 2 3) (cons 4 5)) (Listof (Pairof Number Number))))
               (-lst -Number)]
-        [tc-err (list (values 1 2))]
+        [tc-err (list (values 1 2))
+          #:ret (ret (-Tuple (list -Bottom)))]
 
 
         ;;Path tests
@@ -1292,13 +1335,16 @@
         (tc-e (regexp-match "foo" (open-input-string "tmp")) (-opt (-pair -Bytes (-lst (-opt -Bytes)))))
         (tc-e (regexp-match #"foo" (open-input-string "tmp")) (-opt (-pair -Bytes (-lst (-opt -Bytes)))))
 
-        (tc-err (regexp-try-match "foo" "foobar"))
+        (tc-err (regexp-try-match "foo" "foobar")
+          #:ret (ret (t:Un (-val #f) (-pair -Bytes (-lst (t:Un (-val #f) -Bytes))))))
         (tc-e (regexp-try-match "foo" (open-input-string "foobar")) (-opt (-pair -Bytes (-lst (-opt -Bytes)))))
 
-        (tc-err (regexp-match-peek "foo" "foobar"))
+        (tc-err (regexp-match-peek "foo" "foobar")
+          #:ret (ret (t:Un (-val #f) (-pair -Bytes (-lst (t:Un (-val #f) -Bytes))))))
         (tc-e (regexp-match-peek "foo" (open-input-string "foobar")) (-opt (-pair -Bytes (-lst (-opt -Bytes)))))
 
-        (tc-err (regexp-match-peek-immediate "foo" "foobar"))
+        (tc-err (regexp-match-peek-immediate "foo" "foobar")
+          #:ret (ret (t:Un (-val #f) (-pair -Bytes (-lst (t:Un (-val #f) -Bytes))))))
         (tc-e (regexp-match-peek-immediate "foo" (open-input-string "foobar")) (-opt (-pair -Bytes (-lst (-opt -Bytes)))))
 
 
@@ -1310,7 +1356,8 @@
         (tc-e (regexp-split #"foo" "foobar") (-pair -Bytes (-lst -Bytes)))
         (tc-e (regexp-split #"foo" #"foobar") (-pair -Bytes (-lst -Bytes)))
 
-        (tc-err (regexp-split "foo" (path->string "foobar")))
+        (tc-err (regexp-split "foo" (path->string "foobar"))
+          #:ret (ret (-pair -String (-lst -String))))
 
         (tc-e (regexp-replace "foo" "foobar" "rep") -String)
         (tc-e (regexp-replace #"foo" "foobar" "rep") -Bytes)
@@ -1613,11 +1660,14 @@
         (tc-e (guard-evt (inst make-channel String))
               (make-Evt -String))
         (tc-err (let: ([a : (U (Evtof Any) String) always-evt])
-                  (if (handle-evt? a) a (string->symbol a))))
+                  (if (handle-evt? a) a (string->symbol a)))
+          #:ret (ret (t:Un -Symbol (make-Evt Univ))))
         (tc-err (let: ([a : (U (Evtof Any) String) always-evt])
-                  (if (channel-put-evt? a) a (string->symbol a))))
+                  (if (channel-put-evt? a) a (string->symbol a)))
+          #:ret (ret (t:Un -Symbol (make-Evt (-mu x (make-Evt x))))))
         (tc-err (let: ([a : (U (Evtof Any) String) always-evt])
-                  (if (semaphore-peek-evt? a) a (string->symbol a))))
+                  (if (semaphore-peek-evt? a) a (string->symbol a)))
+          #:ret (ret (t:Un -Symbol (make-Evt (-mu x (make-Evt x))))))
 
         ;Semaphores
         (tc-e (make-semaphore) -Semaphore)
@@ -1680,7 +1730,8 @@
                     srcloc)
               -Void)
         [tc-e (raise (exn:fail:contract "1" (current-continuation-marks))) (t:Un)]
-        [tc-err (exn:fail:contract)]
+        [tc-err (exn:fail:contract)
+          #:ret (ret (resolve (make-Name #'exn:fail:contract null #f #t)))]
         [tc-e (#%variable-reference) -Variable-Reference]
         [tc-e (#%variable-reference x) -Variable-Reference]
         [tc-e (#%variable-reference +) -Variable-Reference]
@@ -1771,7 +1822,8 @@
               Univ]
         [tc-e ((inst vector Index) 0)
               (-vec -Index)]
-        [tc-err ((inst list Void) 1 2 3)]
+        [tc-err ((inst list Void) 1 2 3)
+          #:ret (ret (-lst -Void))]
         [tc-e ((inst list Any) 1 2 3)
               (-lst Univ)]
 
@@ -1789,7 +1841,8 @@
                   (define (g x) 2))]
         [tc-err
           (let ((s (ann (set 2) Any)))
-            (if (set? s) (ann s (Setof String)) ((inst set String))))]
+            (if (set? s) (ann s (Setof String)) ((inst set String))))
+          #:ret (ret (-set -String))]
 
         [tc-e (split-at (list 0 2 3 4 5 6) 3)
               (list (-lst -Byte) (-lst -Byte))]
@@ -1810,7 +1863,8 @@
         [tc-err
           (ann
             ((letrec ((x (lambda (acc #{ v : Symbol}) (if v (list v) acc)))) x) null (list 'bad 'prog))
-            (Listof Symbol))]
+            (Listof Symbol))
+          #:ret (ret (-lst -Symbol) -no-filter -no-obj)]
         [tc-e (filter values empty)
               (-lst -Bottom)]
         [tc-e (lambda lst (map (plambda: (b) ([x : b]) x) lst))
@@ -1829,9 +1883,11 @@
         [tc-e/t (ann (ann 'x Symbol) Symbol) -Symbol]
 
         [tc-err (lambda (x) x)
-                #:expected (ret (-poly (a) (cl->* (t:-> a a) (t:-> a a a))))]
+          #:ret (ret (-poly (a) (cl->* (t:-> a a) (t:-> a a a))))
+          #:expected (ret (-poly (a) (cl->* (t:-> a a) (t:-> a a a))))]
         [tc-err (plambda: (A) ((x : A)) x)
-                #:expected (ret (list -Symbol -Symbol))]
+          #:ret (ret (list -Symbol -Symbol))
+          #:expected (ret (list -Symbol -Symbol))]
 
         [tc-e/t
           (case-lambda
@@ -2027,8 +2083,10 @@
              (make-StructTypeTop)]
        [tc-err (let-values ([(name _1 _2 getter setter _3 _4 _5)
                              (struct-type-info struct:arity-at-least)])
-                 (getter 'bad 0))]
-       [tc-err (struct-type-make-constructor 'bad)]
+                 (getter 'bad 0))
+         #:ret (ret Univ)]
+       [tc-err (struct-type-make-constructor 'bad)
+         #:ret (ret top-func)]
        [tc-err (struct-type-make-predicate 'bad)]
 
        [tc-e
@@ -2170,9 +2228,11 @@
        [tc-e ((tr:lambda (x #:y y . args) y) 'a #:y 'b) Univ]
        [tc-e ((tr:lambda (x #:y [y 'y] . args) y) 'a #:y 'b) Univ]
        [tc-err (let () (tr:define (f x #:y y) (string-append x "foo")) (void))
-               #:msg #rx"expected: String.*given: Any"]
+         #:ret (ret -Void)
+         #:msg #rx"expected: String.*given: Any"]
        [tc-err (let () (tr:define (f x #:y y) y) (f "a"))
-               #:msg #rx"required keyword was not supplied"]
+         #:ret (ret Univ)
+         #:msg #rx"required keyword was not supplied"]
 
        ;; test lambdas with mixed type expressions, typed keywords, typed
        ;; optional arguments
@@ -2193,7 +2253,8 @@
        [tc-e (tr:lambda (x z [y : String]) : String (string-append y "b"))
              #:ret (ret (t:-> Univ Univ -String -String) -true-filter)]
        [tc-err (tr:lambda (x [y : String]) : Symbol (string-append y "b"))
-               #:msg "expected: Symbol.*given: String"]
+         #:ret (ret (t:-> Univ -String -Symbol) -true-filter)
+         #:msg "expected: Symbol.*given: String"]
        [tc-err (tr:lambda (x [y : String "a"] z) (string-append y "b"))
                #:msg "expected optional lambda argument"]
        [tc-e (tr:lambda (x [y : String "a"]) (string-append y "b"))
@@ -2515,10 +2576,13 @@
                #:msg "type information"]
        ;; make sure no-binding cases like the middle expression are checked
        [tc-err (let () (define r "r") (string-append r 'foo) (define x "x") "y")
-               #:msg "expected: String.*given: 'foo"]
+         #:ret (ret -String -true-filter)
+         #:msg "expected: String.*given: 'foo"]
 
+       ;; Polydotted types are not checking equality correctly
        [tc-err (ann (lambda () (let ([my-values values]) (my-values)))
-                 (All (A ...) (-> (Values Symbol ... A))))]
+                 (All (A ...) (-> (Values Symbol ... A))))
+         #:ret (ret (-polydots (A) (t:-> (-values-dots null -Symbol 'A))) -true-filter)]
 
        [tc-e (list 'x)
              #:ret (ret (-Tuple (list -Symbol)))