diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/constraints.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/constraints.rkt
index 319bfdaa11..44c11ca25a 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/constraints.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/constraints.rkt
@@ -4,25 +4,13 @@
 	 (types abbrev union subtype)
 	 (utils tc-utils)
 	 unstable/sequence unstable/hash
-         "signatures.rkt" "constraint-structs.rkt"
+         "fail.rkt" "signatures.rkt" "constraint-structs.rkt"
          racket/match
          racket/list)
 
 (import restrict^ dmap^)
 (export constraints^)
 
-;; It's hard to remove this use of exceptions
-;; because there's no monadic version of `hash-union` etc
-(define-values (fail-sym exn:infer?)
-  (let ([sym (gensym 'infer-fail)])
-    (values sym (λ (s) (and (pair? s) (eq? (car s) sym))))))
-
-;; why does this have to be duplicated?
-;; inference failure - masked before it gets to the user program
-(define-syntaxes (fail!)
-  (syntax-rules ()
-    [(_ s t) (raise (list fail-sym s t))]))
-
 ;; Widest constraint possible
 (define (no-constraint v)
   (make-c (Un) v Univ))
@@ -31,10 +19,12 @@
 ;; index variables Y.  For now, we add the widest constraints for
 ;; variables in X to the cmap and create an empty dmap.
 (define (empty-cset X Y)
-  (make-cset (list (cons (for/hash ([x (in-list X)]) (values x (no-constraint x)))
+  (make-cset (list (cons (for/hash ([x (in-list X)])
+                           (values x (no-constraint x)))
                          (make-dmap (make-immutable-hash null))))))
 
 
+;; add the constraints S <: var <: T to every map in cs
 (define (insert cs var S T)
   (match cs
     [(struct cset (maps))
@@ -42,7 +32,9 @@
                   (cons (hash-set map var (make-c S var T))
                         dmap)))]))
 
-;; a stupid impl
+;; meet: Type Type -> Type
+;; intersect the given types. produces a lower bound on both, but
+;; perhaps not the GLB
 (define (meet S T)
   (let ([s* (restrict S T)])
     (if (and (subtype s* S)
@@ -50,41 +42,54 @@
         s*
         (Un))))
 
+;; join: Type Type -> Type
+;; union the given types
 (define (join T U) (Un T U))
 
 
+;; meet of two variable constraints
+;; never fails
+;; if var is provided, the resulting constraint uses it, otherwise it
+;; uses the variable from `c1` (which must be the same as the one from
+;; `c2`)
 (define (c-meet c1 c2 [var #f])
-  (match* (c1 c2)
+  (match*/early (c1 c2)
     [((struct c (S X T)) (struct c (S* X* T*)))
      (unless (or var (eq? X X*))
        (int-err "Non-matching vars in c-meet: ~a ~a" X X*))
      (let ([S (join S S*)] [T (meet T T*)])
-       (unless (subtype S T)
-         (fail! S T))
-       (make-c S (or var X) T))]))
-
+       (and (subtype S T)  
+            (make-c S (or var X) T)))]))
+  
+;; compute the meet of two constraint sets
+;; returns #f for failure
 (define (cset-meet x y)
   (match* (x y)
    [((struct cset (maps1)) (struct cset (maps2)))
-    (let ([maps (filter values
-                        (for*/list
-                         ([(map1 dmap1) (in-pairs (remove-duplicates maps1))]
-                          [(map2 dmap2) (in-pairs (remove-duplicates maps2))])
-                         (with-handlers ([exn:infer? (lambda (_) #f)])
-                           (cons
-                            (hash-union map1 map2 #:combine c-meet)
-                            (dmap-meet dmap1 dmap2)))))])
-      (when (null? maps)
-        (fail! maps1 maps2))
-      (make-cset maps))]
+    (define maps (for*/list ([(map1 dmap1) (in-pairs (remove-duplicates maps1))]
+                             [(map2 dmap2) (in-pairs (remove-duplicates maps2))]
+                             [v (in-value (% cons
+                                             (hash-union/fail map1 map2 #:combine c-meet)
+                                             (dmap-meet dmap1 dmap2)))]
+                             #:when v)
+                   v))
+    (cond [(null? maps)
+           #f]
+          [else (make-cset maps)])]
    [(_ _) (int-err "Got non-cset: ~a ~a" x y)]))
 
+;; combines a list of csets using cset-meet individually
+;; returns #f for failure
 (define (cset-meet* args)
-  (for/fold ([c (make-cset (list (cons (make-immutable-hash null)
-                                       (make-dmap (make-immutable-hash null)))))])
-    ([a (in-list args)])
+  (for/fold ([c (make-cset (list (cons
+                                  (make-immutable-hash null)
+                                  (make-dmap (make-immutable-hash null)))))])
+    ([a (in-list args)]
+     #:break (not c))
     (cset-meet a c)))
 
-(define (cset-combine l)
+;; produces a cset of all of the maps in all of the given csets
+;; FIXME: should this call `remove-duplicates`?
+(define (cset-join l)
   (let ([mapss (map cset-maps l)])
     (make-cset (apply append mapss))))
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/dmap.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/dmap.rkt
index 74c3e00844..3034b73caf 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/dmap.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/dmap.rkt
@@ -1,6 +1,6 @@
 #lang racket/unit
 
-(require "../utils/utils.rkt"
+(require "../utils/utils.rkt" "fail.rkt"
          "signatures.rkt" "constraint-structs.rkt"
          (utils tc-utils) 
          (contract-req)
@@ -9,38 +9,40 @@
 (import constraints^)
 (export dmap^)
 
-;; dcon-meet : dcon dcon -> dcon
+
+;; dcon-meet : dcon dcon -> dcon or #f
 (define/cond-contract (dcon-meet dc1 dc2)
-  (dcon/c dcon/c . -> . dcon/c)
-  (match* (dc1 dc2)
+  (dcon/c dcon/c . -> . (or/c #f dcon/c))
+  (match*/early (dc1 dc2)
     [((struct dcon-exact (fixed1 rest1)) (or (struct dcon (fixed2 rest2))
                                              (struct dcon-exact (fixed2 rest2))))
-     (unless (and rest2 (= (length fixed1) (length fixed2)))
-       (fail! fixed1 fixed2))
-     (make-dcon-exact
-      (for/list ([c1 (in-list fixed1)]
-                 [c2 (in-list fixed2)])
-        (c-meet c1 c2 (c-X c1)))
-      (c-meet rest1 rest2 (c-X rest1)))]
-    ;; redo in the other order to call the first case
+     #:return-unless (and rest2 (= (length fixed1) (length fixed2)))
+     #f
+     (% make-dcon-exact
+        (for/list/fail ([c1 (in-list fixed1)]
+                        [c2 (in-list fixed2)])
+           (c-meet c1 c2 (c-X c1)))
+        (c-meet rest1 rest2 (c-X rest1)))]
+    ;; redo in the other order to call the previous case
     [((struct dcon (fixed1 rest1)) (struct dcon-exact (fixed2 rest2)))
      (dcon-meet dc2 dc1)]
     [((struct dcon (fixed1 #f)) (struct dcon (fixed2 #f)))
-     (unless (= (length fixed1) (length fixed2))
-       (fail! fixed1 fixed2))
-     (make-dcon
-      (for/list ([c1 (in-list fixed1)]
-                 [c2 (in-list fixed2)])
-        (c-meet c1 c2 (c-X c1)))
-      #f)]
+     #:return-unless (= (length fixed1) (length fixed2))
+     #f
+     (%1 make-dcon
+         (for/list/fail ([c1 (in-list fixed1)]
+                         [c2 (in-list fixed2)])
+           (c-meet c1 c2 (c-X c1)))
+         #f)]
     [((struct dcon (fixed1 #f)) (struct dcon (fixed2 rest)))
-     (unless (>= (length fixed1) (length fixed2))
-       (fail! fixed1 fixed2))
-     (make-dcon
-      (for/list ([c1 (in-list fixed1)]
-                 [c2 (in-sequence-forever fixed2 rest)])
+     #:return-unless (>= (length fixed1) (length fixed2))
+     #f
+     (%1 make-dcon
+      (for/list/fail ([c1 (in-list fixed1)]
+                      [c2 (in-sequence-forever fixed2 rest)])
         (c-meet c1 c2 (c-X c1)))
       #f)]
+    ;; redo in the other order to call the previous case
     [((struct dcon (fixed1 rest)) (struct dcon (fixed2 #f)))
      (dcon-meet dc2 dc1)]
     [((struct dcon (fixed1 rest1)) (struct dcon (fixed2 rest2)))
@@ -48,24 +50,25 @@
                    (if (< (length fixed1) (length fixed2))
                        (values fixed1 fixed2 rest1 rest2)
                        (values fixed2 fixed1 rest2 rest1))])
-       (make-dcon
-        (for/list ([c1 (in-list longer)]
+       (% make-dcon
+        (for/list/fail ([c1 (in-list longer)]
                    [c2 (in-sequence-forever shorter srest)])
           (c-meet c1 c2 (c-X c1)))
         (c-meet lrest srest (c-X lrest))))]
     [((struct dcon-dotted (fixed1 c1 bound1)) (struct dcon-dotted (fixed2 c2 bound2)))
-     (unless (and (= (length fixed1) (length fixed2))
-                  (eq? bound1 bound2))
-       (fail! bound1 bound2))
-     (make-dcon-dotted (for/list ([c1 (in-list fixed1)] [c2 (in-list fixed2)])
-                         (c-meet c1 c2 (c-X c1)))
+     #:return-unless (and (= (length fixed1) (length fixed2))
+                          (eq? bound1 bound2))
+     #f
+     (% make-dcon-dotted (for/list/fail ([c1 (in-list fixed1)] [c2 (in-list fixed2)])
+                           (c-meet c1 c2 (c-X c1)))
                        (c-meet c1 c2 bound1) bound1)]
     [((struct dcon _) (struct dcon-dotted _))
-     (fail! dc1 dc2)]
+     #f]
     [((struct dcon-dotted _) (struct dcon _))
-     (fail! dc1 dc2)]
+     #f]
     [(_ _) (int-err "Got non-dcons: ~a ~a" dc1 dc2)]))
 
+;; dmap dmap -> dmap or #f
 (define (dmap-meet dm1 dm2)
-  (make-dmap
-   (hash-union (dmap-map dm1) (dmap-map dm2) #:combine dcon-meet)))
+  (% make-dmap
+   (hash-union/fail (dmap-map dm1) (dmap-map dm2) #:combine dcon-meet)))
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/fail.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/fail.rkt
new file mode 100644
index 0000000000..aaf22007fa
--- /dev/null
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/fail.rkt
@@ -0,0 +1,59 @@
+#lang racket/base
+(provide (all-defined-out) early-return)
+(require (for-syntax racket/base syntax/parse racket/syntax) "../utils/early-return.rkt"
+         racket/match)
+
+;; like `match*`, but with `early-return` around the rhss
+(define-syntax (match*/early stx)
+  (define-syntax-class rhs
+    (pattern (#:when e rhs ...)
+             #:with r
+             #'(#:when e (early-return rhs ...)))
+    (pattern (rhs ...)
+             #:with r
+             #'((early-return rhs ...))))
+ (syntax-parse stx
+  [(_ e [c . r:rhs] ...)
+   #'(match* e [c . r.r] ...)]))
+
+;; (% f e ...) == (and e ... (f e ...)) but without repeated evaluation
+(define-syntax (% stx)
+  (syntax-parse stx 
+    [(_ f e ...)
+     (define/with-syntax (a ...) (generate-temporaries #'(e ...)))
+     #'(let/fail ([a e] ...)
+         (f a ...))]))
+
+;; (%1 f e0 e ...) == (and e0 (f e0 e ...)) but without repeated evaluation
+(define-syntax (%1 stx)
+  (syntax-parse stx 
+    [(_ f e0 e ...)
+     (define/with-syntax (a0 a ...) (generate-temporaries #'(e0 e ...)))
+     #'(let/fail ([a0 e0]) 
+         (let ([a e] ...)
+           (f a0 a ...)))]))
+
+;; like `let`, but if any bindings are #f, the whole expression produces #f
+(define-syntax (let/fail stx)
+  (syntax-parse stx
+    [(let/fail () e ...) #'(let () e ...)]
+    [(let/fail ([x rhs ...] . rest) body ...)
+     #'(let ([x rhs ...])
+         (and x
+              (let/fail rest body ...)))]))
+
+;; (for/list/fail e ...) == (and (andmap values (for/list e ...)) (for/list e ...)
+;; but without wasted work
+(define-syntax-rule (for/list/fail (cl ...) body ...)
+  (% reverse
+     (for/fold ([result null]) (cl ... #:break (not result))
+       (let ([e (let () body ...)])
+         (and e (cons e result))))))
+
+;; like hash-union, but if combine ever produces #f, the overall result is #f
+(define (hash-union/fail #:combine combine one two)
+  (for/fold ([one one]) ([(k v) (in-hash two)] #:break (not one))
+    (define d (if (hash-has-key? one k)
+                  (combine (hash-ref one k) v)
+                  v))
+    (and d (hash-set one k d))))
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt
index 217cf5d24c..2b06d7788c 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt
@@ -17,7 +17,7 @@
            (env index-env tvar-env))
           make-env -> ->* one-of/c)
          "constraint-structs.rkt"
-         "signatures.rkt"
+         "signatures.rkt" "fail.rkt"
          racket/match
          mzlib/etc
          (contract-req)
@@ -52,16 +52,18 @@
 
 ;; Type Type -> Boolean
 ;; Check if a given type pair have been seen before
-(define/cond-contract (seen? s t)
+(define/cond-contract (seen? s t cs)
   ((or/c AnyValues? Values/c ValuesDots?) (or/c AnyValues? Values/c ValuesDots?)
+   (listof (cons/c exact-nonnegative-integer?
+                   exact-nonnegative-integer?))
    . -> . any/c)
- (member (seen-before s t) (current-seen)))
+ (member (seen-before s t) cs))
 
 ;; (CMap DMap -> Pair<CMap, DMap>) CSet -> CSet
 ;; Map a function over a constraint set
 (define (map/cset f cset)
-  (make-cset (for/list ([(cmap dmap) (in-pairs (cset-maps cset))])
-               (f cmap dmap))))
+  (% make-cset (for/list/fail ([(cmap dmap) (in-pairs (cset-maps cset))])
+                 (f cmap dmap))))
 
 ;; Symbol DCon -> DMap
 ;; Construct a dmap containing only a single mapping
@@ -76,12 +78,13 @@
 (define (mover cset dbound vars f)
   (map/cset
    (lambda (cmap dmap)
-     (cons (hash-remove* cmap (cons dbound vars))
-           (dmap-meet
-            (singleton-dmap
-             dbound
-             (f cmap dmap))
-            (make-dmap (hash-remove (dmap-map dmap) dbound)))))
+     (% cons
+        (hash-remove* cmap (cons dbound vars))
+        (dmap-meet
+         (singleton-dmap
+          dbound
+          (f cmap dmap))
+         (make-dmap (hash-remove (dmap-map dmap) dbound)))))
    cset))
 
 ;; dbound : index variable
@@ -168,44 +171,46 @@
           all))))
 
 (define/cond-contract (cgen/filter V X Y s t)
-  ((listof symbol?) (listof symbol?) (listof symbol?) Filter? Filter? . -> . cset?)
+  ((listof symbol?) (listof symbol?) (listof symbol?) Filter? Filter? . -> . (or/c #f cset?))
   (match* (s t)
     [(e e) (empty-cset X Y)]
     [(e (Top:)) (empty-cset X Y)]
     ;; FIXME - is there something to be said about the logical ones?
-    [((TypeFilter: s p i) (TypeFilter: t p i)) (cset-meet (cgen V X Y s t) (cgen V X Y t s))]
-    [((NotTypeFilter: s p i) (NotTypeFilter: t p i)) (cset-meet (cgen V X Y s t) (cgen V X Y t s))]
-    [(_ _) (fail! s t)]))
+    [((TypeFilter: s p i) (TypeFilter: t p i))
+     (% cset-meet (cgen V X Y s t) (cgen V X Y t s))]
+    [((NotTypeFilter: s p i) (NotTypeFilter: t p i))
+     (% cset-meet (cgen V X Y s t) (cgen V X Y t s))]
+    [(_ _) #f]))
 
 ;; s and t must be *latent* filter sets
 (define/cond-contract (cgen/filter-set V X Y s t)
-  ((listof symbol?) (listof symbol?) (listof symbol?) FilterSet? FilterSet? . -> . cset?)
+  ((listof symbol?) (listof symbol?) (listof symbol?) FilterSet? FilterSet? . -> . (or/c #f cset?))
   (match* (s t)
     [(e e) (empty-cset X Y)]
     [((FilterSet: s+ s-) (FilterSet: t+ t-))
-     (cset-meet (cgen/filter V X Y s+ t+) (cgen/filter V X Y s- t-))]
-    [(_ _) (fail! s t)]))
+     (% cset-meet (cgen/filter V X Y s+ t+) (cgen/filter V X Y s- t-))]
+    [(_ _) #f]))
 
 (define/cond-contract (cgen/object V X Y s t)
-  ((listof symbol?) (listof symbol?) (listof symbol?) Object? Object? . -> . cset?)
+  ((listof symbol?) (listof symbol?) (listof symbol?) Object? Object? . -> . (or/c #f cset?))
   (match* (s t)
     [(e e) (empty-cset X Y)]
     [(e (Empty:)) (empty-cset X Y)]
     ;; FIXME - do something here
-    [(_ _) (fail! s t)]))
+    [(_ _) #f]))
 
 (define/cond-contract (cgen/arr V X Y s-arr t-arr)
-  ((listof symbol?) (listof symbol?) (listof symbol?) arr? arr? . -> . cset?)
+  ((listof symbol?) (listof symbol?) (listof symbol?) arr? arr? . -> . (or/c #f cset?))
   (define (cg S T) (cgen V X Y S T))
-  (match* (s-arr t-arr)
+  (match*/early (s-arr t-arr)
     ;; the simplest case - no rests, drests, keywords
     [((arr: ss s #f #f '())
       (arr: ts t #f #f '()))
-     (cset-meet* (list
-                  ;; contravariant
-                  (cgen/list V X Y ts ss)
-                  ;; covariant
-                  (cg s t)))]
+     (% cset-meet* (% list
+                      ;; contravariant
+                      (cgen/list V X Y ts ss)
+                      ;; covariant
+                      (cg s t)))]
     ;; just a rest arg, no drest, no keywords
     [((arr: ss s s-rest #f '())
       (arr: ts t t-rest #f '()))
@@ -213,96 +218,100 @@
             (cond
               ;; both rest args are present, so make them the same length
               [(and s-rest t-rest)
-               (cgen/list V X Y (cons t-rest (extend ss ts t-rest)) (cons s-rest (extend ts ss s-rest)))]
+               (cgen/list V X Y
+                          (cons t-rest (extend ss ts t-rest))
+                          (cons s-rest (extend ts ss s-rest)))]
               ;; no rest arg on the right, so just pad the left and forget the rest arg
               [(and s-rest (not t-rest) (<= (length ss) (length ts)))
                (cgen/list V X Y ts (extend ts ss s-rest))]
               ;; no rest arg on the left, or wrong number = fail
-              [else (fail! s-arr t-arr)])]
+              [else #f])]
            [ret-mapping (cg s t)])
-       (cset-meet* (list arg-mapping ret-mapping)))]
+       (% cset-meet* (% list arg-mapping ret-mapping)))]
     ;; dotted on the left, nothing on the right
     [((arr: ss s #f (cons dty dbound) '())
       (arr: ts t #f #f                '()))
-     (unless (memq dbound Y)
-       (fail! s-arr t-arr))
-     (unless (<= (length ss) (length ts))
-       (fail! ss ts))
+     #:return-unless (memq dbound Y)
+     #f
+     #:return-unless (<= (length ss) (length ts))
+     #f
      (let* ([vars      (var-store-take dbound dty (- (length ts) (length ss)))]
             [new-tys   (for/list ([var (in-list vars)])
                          (substitute (make-F var) dbound dty))]
             [new-s-arr (make-arr (append ss new-tys) s #f #f null)]
             [new-cset  (cgen/arr V (append vars X) Y new-s-arr t-arr)])
-       (move-vars-to-dmap new-cset dbound vars))]
+       (% move-vars-to-dmap new-cset dbound vars))]
     ;; dotted on the right, nothing on the left
     [((arr: ss s #f #f                '())
       (arr: ts t #f (cons dty dbound) '()))
-     (unless (memq dbound Y)
-       (fail! s-arr t-arr))
-     (unless (<= (length ts) (length ss))
-       (fail! ss ts))
+     #:return-unless (memq dbound Y)
+     #f
+     #:return-unless (<= (length ts) (length ss))
+     #f
      (let* ([vars     (var-store-take dbound dty (- (length ss) (length ts)))]
             [new-tys  (for/list ([var (in-list vars)])
                         (substitute (make-F var) dbound dty))]
             [new-t-arr (make-arr (append ts new-tys) t #f #f null)]
             [new-cset (cgen/arr V (append vars X) Y s-arr new-t-arr)])
-       (move-vars-to-dmap new-cset dbound vars))]
+       (% move-vars-to-dmap new-cset dbound vars))]
     ;; this case is just for constrainting other variables, not dbound
     [((arr: ss s #f (cons s-dty dbound) '())
       (arr: ts t #f (cons t-dty dbound) '()))
-     (unless (= (length ss) (length ts))
-       (fail! ss ts))
+     #:return-unless (= (length ss) (length ts))
+     #f
      ;; If we want to infer the dotted bound, then why is it in both types?
-     (when (memq dbound Y)
-       (fail! s-arr t-arr))
+     #:return-when (memq dbound Y)
+     #f
      (let* ([arg-mapping (cgen/list V X Y ts ss)]
             [darg-mapping (cgen V X Y t-dty s-dty)]
             [ret-mapping (cg s t)])
-       (cset-meet*
-        (list arg-mapping darg-mapping ret-mapping)))]
+       (% cset-meet*
+          (% list arg-mapping darg-mapping ret-mapping)))]
     ;; bounds are different
     [((arr: ss s #f (cons s-dty (? (λ (db) (memq db Y)) dbound))  '())
       (arr: ts t #f (cons t-dty dbound*) '()))
-     (unless (= (length ss) (length ts)) (fail! ss ts))
-     (when (memq dbound* Y) (fail! s-arr t-arr))
+     #:return-unless (= (length ss) (length ts)) #f
+     #:return-when (memq dbound* Y) #f
      (let* ([arg-mapping (cgen/list V X Y ts ss)]
             ;; just add dbound as something that can be constrained
-            [darg-mapping (move-dotted-rest-to-dmap (cgen V (cons dbound X) Y t-dty s-dty) dbound)]
+            [darg-mapping (% move-dotted-rest-to-dmap (cgen V (cons dbound X) Y t-dty s-dty) dbound)]
             [ret-mapping (cg s t)])
-       (cset-meet*
-        (list arg-mapping darg-mapping ret-mapping)))]
+       (% cset-meet*
+        (% list arg-mapping darg-mapping ret-mapping)))]
     [((arr: ss s #f (cons s-dty dbound)  '())
       (arr: ts t #f (cons t-dty (? (λ (db) (memq db Y)) dbound*)) '()))
-     (unless (= (length ss) (length ts)) (fail! ss ts))
+     #:return-unless (= (length ss) (length ts)) #f
      (let* ([arg-mapping (cgen/list V X Y ts ss)]
             ;; just add dbound as something that can be constrained
-            [darg-mapping (move-dotted-rest-to-dmap (cgen V (cons dbound* X) Y t-dty s-dty) dbound*)]
+            [darg-mapping (% move-dotted-rest-to-dmap
+                             (cgen V (cons dbound* X) Y t-dty s-dty) dbound*)]
             [ret-mapping (cg s t)])
-       (cset-meet*
-        (list arg-mapping darg-mapping ret-mapping)))]
+       (% cset-meet*
+        (% list arg-mapping darg-mapping ret-mapping)))]
     ;; * <: ...
     [((arr: ss s s-rest #f                  '())
       (arr: ts t #f     (cons t-dty dbound) '()))
-     (unless (memq dbound Y)
-       (fail! s-arr t-arr))
+     #:return-unless (memq dbound Y)
+     #f
      (if (<= (length ss) (length ts))
          ;; the simple case
          (let* ([arg-mapping (cgen/list V X Y ts (extend ts ss s-rest))]
-                [darg-mapping (move-rest-to-dmap (cgen V (cons dbound X) Y t-dty s-rest) dbound)]
+                [darg-mapping (% move-rest-to-dmap
+                                 (cgen V (cons dbound X) Y t-dty s-rest) dbound)]
                 [ret-mapping (cg s t)])
-           (cset-meet* (list arg-mapping darg-mapping ret-mapping)))
+           (% cset-meet* (% list arg-mapping darg-mapping ret-mapping)))
          ;; the hard case
          (let* ([vars     (var-store-take dbound t-dty (- (length ss) (length ts)))]
                 [new-tys  (for/list ([var (in-list vars)])
                             (substitute (make-F var) dbound t-dty))]
                 [new-t-arr (make-arr (append ts new-tys) t #f (cons t-dty dbound) null)]
                 [new-cset (cgen/arr V (append vars X) Y s-arr new-t-arr)])
-           (move-vars+rest-to-dmap new-cset dbound vars)))]
+           (% move-vars+rest-to-dmap new-cset dbound vars)))]
     ;; If dotted <: starred is correct, add it below.  Not sure it is.
     [((arr: ss s #f     (cons s-dty dbound) '())
       (arr: ts t t-rest #f                  '()))
-     (unless (memq dbound Y)
-       (fail! s-arr t-arr))
+     #:return-unless (memq dbound Y)
+     #f
      (cond [(< (length ss) (length ts))
             ;; the hard case
             (let* ([vars     (var-store-take dbound s-dty (- (length ts) (length ss)))]
@@ -310,21 +319,25 @@
                                (substitute (make-F var) dbound s-dty))]
                    [new-s-arr (make-arr (append ss new-tys) s #f (cons s-dty dbound) null)]
                    [new-cset (cgen/arr V (append vars X) Y new-s-arr t-arr)])
-              (move-vars+rest-to-dmap new-cset dbound vars #:exact #t))]
+              (and new-cset vars
+                   (move-vars+rest-to-dmap new-cset dbound vars #:exact #t)))]
            [(= (length ss) (length ts))
             ;; the simple case
             (let* ([arg-mapping (cgen/list V X Y (extend ss ts t-rest) ss)]
-                   [darg-mapping (move-rest-to-dmap (cgen V (cons dbound X) Y t-rest s-dty) dbound #:exact #t)]
+                   [rest-mapping (cgen V (cons dbound X) Y t-rest s-dty)]
+                   [darg-mapping (and rest-mapping 
+                                      (move-rest-to-dmap
+                                       rest-mapping dbound #:exact #t))]
                    [ret-mapping (cg s t)])
-              (cset-meet* (list arg-mapping darg-mapping ret-mapping)))]
-           [else
-             (fail! s-arr t-arr)])]
-    [(_ _) (fail! s-arr t-arr)]))
+              (% cset-meet* (% list arg-mapping darg-mapping ret-mapping)))]
+           [else #f])]
+    [(_ _) #f]))
 
 (define/cond-contract (cgen/flds V X Y flds-s flds-t)
-  ((listof symbol?) (listof symbol?) (listof symbol?) (listof fld?) (listof fld?)  . -> . cset?)
-  (cset-meet*
-   (for/list ([s (in-list flds-s)] [t (in-list flds-t)])
+  ((listof symbol?) (listof symbol?) (listof symbol?) (listof fld?) (listof fld?)  
+   . -> . (or/c #f cset?))
+  (% cset-meet*
+   (for/list/fail ([s (in-list flds-s)] [t (in-list flds-t)])
      (match* (s t)
        ;; mutable - invariant
        [((fld: s _ #t) (fld: t _ #t)) (cset-meet (cgen V X Y s t) (cgen V X Y t s))]
@@ -341,26 +354,30 @@
 ;; the index variables from the TOPLAS paper
 (define/cond-contract (cgen V X Y S T)
   ((listof symbol?) (listof symbol?) (listof symbol?)
-   (or/c Values/c ValuesDots? AnyValues?) (or/c Values/c ValuesDots? AnyValues?) . -> . cset?)
+   (or/c Values/c ValuesDots? AnyValues?) (or/c Values/c ValuesDots? AnyValues?)
+   . -> . (or/c #F cset?))
   ;; useful quick loop
   (define/cond-contract (cg S T)
-   (Type/c Type/c . -> . cset?)
+   (Type/c Type/c . -> . (or/c #f cset?))
    (cgen V X Y S T))
   ;; this places no constraints on any variables in X
   (define empty (empty-cset X Y))
   ;; this constrains just x (which is a single var)
   (define (singleton S x T)
     (insert empty x S T))
+  ;; FIXME -- figure out how to use parameters less here
+  ;;          subtyping doesn't need to use it quite as much
+  (define cs (current-seen))
   ;; if we've been around this loop before, we're done (for rec types)
-  (if (seen? S T)
+  (if (seen? S T cs)
       empty
-      (parameterize ([match-equality-test (lambda (a b) (if (and (Rep? a) (Rep? b)) (type-equal? a b) (equal? a b)))]
-                     ;; remember S and T, and obtain everything we've seen from the context
-                     ;; we can't make this an argument since we may call back and forth with subtyping, for example
-                     [current-seen (remember S T (current-seen))])
-        (match* (S T)
+      (parameterize (;; remember S and T, and obtain everything we've seen from the context
+                     ;; we can't make this an argument since we may call back and forth with
+                     ;; subtyping, for example
+                     [current-seen (remember S T cs)])
+        (match*/early (S T)
           ;; if they're equal, no constraints are necessary (CG-Refl)
-          [(a a) empty]
+          [(a b) #:when (type-equal? a b) empty]
           ;; CG-Top
           [(_ (Univ:)) empty]
           [(_ (AnyValues:)) empty]
@@ -370,23 +387,25 @@
           ;; check each element
           [((Result: s f-s o-s)
             (Result: t f-t o-t))
-           (cset-meet* (list (cg s t)
-                             (cgen/filter-set V X Y f-s f-t)
-                             (cgen/object V X Y o-s o-t)))]
+           (% cset-meet* (% list
+                            (cg s t)
+                            (cgen/filter-set V X Y f-s f-t)
+                            (cgen/object V X Y o-s o-t)))]
 
           ;; values are covariant
           [((Values: ss) (Values: ts))
-           (unless (= (length ss) (length ts))
-             (fail! ss ts))
+           #:return-unless (= (length ss) (length ts))
+           #f
            (cgen/list V X Y ss ts)]
 
           ;; this constrains `dbound' to be |ts| - |ss|
           [((ValuesDots: ss s-dty dbound) (Values: ts))
-           (unless (>= (length ts) (length ss)) (fail! ss ts))
-           (unless (memq dbound Y) (fail! S T))
+           #:return-unless (>= (length ts) (length ss)) #f
+           #:return-unless (memq dbound Y) #f
 
            (let* ([vars     (var-store-take dbound s-dty (- (length ts) (length ss)))]
-                  ;; new-tys are dummy plain type variables, standing in for the elements of dbound that need to be generated
+                  ;; new-tys are dummy plain type variables, 
+                  ;; standing in for the elements of dbound that need to be generated
                   [new-tys  (for/list ([var (in-list vars)])
                               ;; must be a Result since we are matching these against
                               ;; the contents of the `Values`, which are Results
@@ -394,12 +413,12 @@
                   ;; generate constraints on the prefixes, and on the dummy types
                   [new-cset (cgen/list V (append vars X) Y (append ss new-tys) ts)])
              ;; now take all the dummy types, and use them to constrain dbound appropriately
-             (move-vars-to-dmap new-cset dbound vars))]
+             (% move-vars-to-dmap new-cset dbound vars))]
 
           ;; like the case above, but constrains `dbound' to be |ss| - |ts|
           [((Values: ss) (ValuesDots: ts t-dty dbound))
-           (unless (>= (length ss) (length ts)) (fail! ss ts))
-           (unless (memq dbound Y) (fail! S T))
+           #:return-unless (>= (length ss) (length ts)) #f
+           #:return-unless (memq dbound Y) #f
 
            ;; see comments for last case, this case swaps `s` and `t` order
            (let* ([vars     (var-store-take dbound t-dty (- (length ss) (length ts)))]
@@ -410,25 +429,27 @@
 
           ;; identical bounds - just unify pairwise
           [((ValuesDots: ss s-dty dbound) (ValuesDots: ts t-dty dbound))
-           (when (memq dbound Y) (fail! ss ts))
+           #:return-when (memq dbound Y) #f
            (cgen/list V X Y (cons s-dty ss) (cons t-dty ts))]
-          [((ValuesDots: ss s-dty (? (λ (db) (memq db Y)) s-dbound)) (ValuesDots: ts t-dty t-dbound))
+          [((ValuesDots: ss s-dty (? (λ (db) (memq db Y)) s-dbound))
+            (ValuesDots: ts t-dty t-dbound))
            ;; What should we do if both are in Y?
-           (when (memq t-dbound Y) (fail! S T))
-           (cset-meet
-            (cgen/list V X Y ss ts)
-            (move-dotted-rest-to-dmap (cgen V (cons s-dbound X) Y s-dty t-dty) s-dbound))]
-          [((ValuesDots: ss s-dty s-dbound) (ValuesDots: ts t-dty (? (λ (db) (memq db Y)) t-dbound)))
+           #:return-when (memq t-dbound Y) #f
+           (% cset-meet
+              (cgen/list V X Y ss ts)
+              (% move-dotted-rest-to-dmap 
+                 (cgen V (cons s-dbound X) Y s-dty t-dty) s-dbound))]
+          [((ValuesDots: ss s-dty s-dbound)
+            (ValuesDots: ts t-dty (? (λ (db) (memq db Y)) t-dbound)))
            ;; s-dbound can't be in Y, due to previous rule
-           (cset-meet
-            (cgen/list V X Y ss ts)
-            (move-dotted-rest-to-dmap (cgen V (cons t-dbound X) Y s-dty t-dty) t-dbound))]
+           (% cset-meet
+              (cgen/list V X Y ss ts)
+              (% move-dotted-rest-to-dmap (cgen V (cons t-dbound X) Y s-dty t-dty) t-dbound))]
 
           ;; they're subtypes. easy.
-          [(a b) (=> nevermind)
-           (if (subtype a b)
-               empty
-               (nevermind))]
+          [(a b) 
+           #:when (subtype a b)
+           empty]
 
           ;; refinements are erased to their bound
           [((Refinement: S _) T)
@@ -437,18 +458,21 @@
           ;; variables that are in X and should be constrained
           ;; all other variables are compatible only with themselves
           [((F: (? (λ (e) (memq e X)) v)) T)
+           #:return-when
            (match T
              ;; fail when v* is an index variable
-             [(F: v*) (when (and (bound-index? v*) (not (bound-tvar? v*)))
-                        (fail! S T))]
-             [_ (void)])
+             [(F: v*) (and (bound-index? v*) (not (bound-tvar? v*)))]
+             [_ #f])
+           #f
            ;; constrain v to be below T (but don't mention V)
            (singleton (Un) v (var-demote T V))]
+
           [(S (F: (? (lambda (e) (memq e X)) v)))
+           #:return-when
            (match S
-             [(F: v*) (when (and (bound-index? v*) (not (bound-tvar? v*)))
-                        (fail! S T))]
-             [_ (void)])
+             [(F: v*) (and (bound-index? v*) (not (bound-tvar? v*)))]
+             [_ #f])
+           #f
            ;; constrain v to be above S (but don't mention V)
            (singleton (var-promote S V) v Univ)]
 
@@ -462,61 +486,63 @@
           [((Poly: v1 b1) T) (cgen (append v1 V) X Y b1 T)]
 
           ;; constrain *each* element of es to be below T, and then combine the constraints
-          [((Union: es) T) (cset-meet* (cons empty (for/list ([e (in-list es)]) (cg e T))))]
+          [((Union: es) T)
+           (define cs (for/list/fail ([e (in-list es)]) (cg e T)))
+           (and cs (cset-meet* (cons empty cs)))]
 
           ;; find *an* element of es which can be made to be a supertype of S
           ;; FIXME: we're using multiple csets here, but I don't think it makes a difference
           ;; not using multiple csets will break for: ???
           [(S (Union: es))
-           (cset-combine
-            (filter values
-                    (for/list ([e (in-list es)])
-                      (with-handlers ([exn:infer? (λ _ #f)]) (cg S e)))))]
+           (cset-join
+            (for*/list ([e (in-list es)]
+                        [v (in-value (cg S e))]
+                        #:when v)
+              v))]
 
           ;; two structs with the same name
           ;; just check pairwise on the fields
-          [((Struct: nm _ flds proc _ _) (Struct: nm* _ flds* proc* _ _)) (=> nevermind)
-           (unless (free-identifier=? nm nm*) (nevermind))
+          [((Struct: nm _ flds proc _ _) (Struct: nm* _ flds* proc* _ _))
+           #:when (free-identifier=? nm nm*)
            (let ([proc-c
                   (cond [(and proc proc*)
                          (cg proc proc*)]
-                        [proc* (fail! S T)]
+                        [proc* #f]
                         [else empty])])
-             (cset-meet proc-c (cgen/flds V X Y flds flds*)))]
+             (% cset-meet proc-c (cgen/flds V X Y flds flds*)))]
 
           ;; two struct names, need to resolve b/c one could be a parent
           [((Name: n _ _ #t) (Name: n* _ _ #t))
            (if (free-identifier=? n n*)
-               null
-               (let ((rn (resolve-once S)) (rn* (resolve-once T)))
-                (if (and rn rn*) (cg rn rn*) (fail! S T))))]
+               empty ;; just succeed now
+               (% cg (resolve-once S) (resolve-once T)))]
           ;; pairs are pointwise
           [((Pair: a b) (Pair: a* b*))
-           (cset-meet (cg a a*) (cg b b*))]
+           (% cset-meet (cg a a*) (cg b b*))]
           ;; sequences are covariant
           [((Sequence: ts) (Sequence: ts*))
            (cgen/list V X Y ts ts*)]
           [((Listof: t) (Sequence: (list t*)))
            (cg t t*)]
           [((Pair: t1 t2) (Sequence: (list t*)))
-           (cset-meet (cg t1 t*) (cg t2 (-lst t*)))]
+           (% cset-meet (cg t1 t*) (cg t2 (-lst t*)))]
           [((MListof: t) (Sequence: (list t*)))
            (cg t t*)]
           ;; To check that mutable pair is a sequence we check that the cdr is
           ;; both an mutable list and a sequence
           [((MPair: t1 t2) (Sequence: (list t*)))
-           (cset-meet* (list (cg t1 t*) (cg t2 T) (cg t2 (Un (-val null) (make-MPairTop)))))]
+           (% cset-meet* (% list (cg t1 t*) (cg t2 T) (cg t2 (Un (-val null) (make-MPairTop)))))]
           [((List: ts) (Sequence: (list t*)))
-           (cset-meet* (for/list ([t (in-list ts)])
-                         (cg t t*)))]
+           (% cset-meet* (for/list/fail ([t (in-list ts)])
+                           (cg t t*)))]
           [((HeterogeneousVector: ts) (HeterogeneousVector: ts*))
-           (cset-meet (cgen/list V X Y ts ts*) (cgen/list V X Y ts* ts))]
+           (% cset-meet (cgen/list V X Y ts ts*) (cgen/list V X Y ts* ts))]
           [((HeterogeneousVector: ts) (Vector: s))
            (define ts* (map (λ _ s) ts)) ;; invariant, everything has to match
-           (cset-meet (cgen/list V X Y ts ts*) (cgen/list V X Y ts* ts))]
+           (% cset-meet (cgen/list V X Y ts ts*) (cgen/list V X Y ts* ts))]
           [((HeterogeneousVector: ts) (Sequence: (list t*)))
-           (cset-meet* (for/list ([t (in-list ts)])
-                         (cg t t*)))]
+           (% cset-meet* (for/list/fail ([t (in-list ts)])
+                           (cg t t*)))]
           [((Vector: t) (Sequence: (list t*)))
            (cg t t*)]
           [((Base: 'String _ _ _) (Sequence: (list t*)))
@@ -542,9 +568,7 @@
            (define type
              (for/or ([t (in-list (list -Byte -Index -NonNegFixnum -Nat))])
                (and (subtype S t) t)))
-           (if type
-               (cg type t*)
-               (fail! S T))]
+           (% cg type t*)]
           [((Vector: t) (Sequence: (list t*)))
            (cg t t*)]
           [((Hashtable: k v) (Sequence: (list k* v*)))
@@ -554,7 +578,7 @@
           ;; ListDots can be below a Listof
           ;; must be above mu unfolding
           [((ListDots: s-dty dbound) (Listof: t-elem))
-           (when (memq dbound Y) (fail! S T))
+           #:return-when (memq dbound Y) #f
            (cgen V X Y (substitute Univ dbound s-dty) t-elem)]
           ;; two ListDots with the same bound, just check the element type
           ;; This is conservative because we don't try to infer a constraint on dbound.
@@ -562,7 +586,7 @@
            (cgen V X Y s-dty t-dty)]
           [((ListDots: s-dty (? (λ (db) (memq db Y)) s-dbound)) (ListDots: t-dty t-dbound))
            ;; What should we do if both are in Y?
-           (when (memq t-dbound Y) (fail! S T))
+           #:return-when (memq t-dbound Y) #f
            (move-dotted-rest-to-dmap (cgen V (cons s-dbound X) Y s-dty t-dty) s-dbound)]
           [((ListDots: s-dty s-dbound) (ListDots: t-dty (? (λ (db) (memq db Y)) t-dbound)))
            ;; s-dbound can't be in Y, due to previous rule
@@ -570,20 +594,20 @@
 
           ;; this constrains `dbound' to be |ts| - |ss|
           [((ListDots: s-dty dbound) (List: ts))
-           (unless (memq dbound Y) (fail! S T))
-
+           #:return-unless (memq dbound Y) #f
            (let* ([vars     (var-store-take dbound s-dty (length ts))]
-                  ;; new-tys are dummy plain type variables, standing in for the elements of dbound that need to be generated
+                  ;; new-tys are dummy plain type variables, 
+                  ;; standing in for the elements of dbound that need to be generated
                   [new-tys  (for/list ([var (in-list vars)])
                               (substitute (make-F var) dbound s-dty))]
                   ;; generate constraints on the prefixes, and on the dummy types
                   [new-cset (cgen/list V (append vars X) Y new-tys ts)])
              ;; now take all the dummy types, and use them to constrain dbound appropriately
-             (move-vars-to-dmap new-cset dbound vars))]
+             (% move-vars-to-dmap new-cset dbound vars))]
 
           ;; same as above, constrains `dbound' to be |ss| - |ts|
           [((List: ss) (ListDots: t-dty dbound))
-           (unless (memq dbound Y) (fail! S T))
+           #:return-unless (memq dbound Y) #f
 
            ;; see comments for last case, we flip s and t though
            (let* ([vars     (var-store-take dbound t-dty (length ss))]
@@ -594,7 +618,8 @@
 
           ;; if we have two mu's, we rename them to have the same variable
           ;; and then compare the bodies
-          ;; This relies on (B 0) only unifying with itself, and thus only hitting the first case of this `match'
+          ;; This relies on (B 0) only unifying with itself, 
+          ;; and thus only hitting the first case of this `match'
           [((Mu-unsafe: s) (Mu-unsafe: t))
            (cg s t)]
 
@@ -604,11 +629,9 @@
 
           ;; resolve applications
           [((App: _ _ _) _)
-           (let ((S* (resolve-once S)))
-            (if S* (cg S* T) (fail! S T)))]
+           (% cg (resolve-once S) T)]
           [(_ (App: _ _ _))
-           (let ((T* (resolve-once T)))
-            (if T* (cg S T*) (fail! S T)))]
+           (% cg S (resolve-once T))]
 
           ;; If the struct names don't match, try the parent of S
           ;; Needs to be done after App and Mu in case T is actually the current struct
@@ -619,24 +642,24 @@
           ;; Invariant here because struct types aren't subtypes just because the
           ;; structs are (since you can make a constructor from the type).
           [((StructType: s) (StructType: t))
-           (cset-meet (cg s t) (cg t s))]
+           (% cset-meet (cg s t) (cg t s))]
 
           ;; vectors are invariant - generate constraints *both* ways
           [((Vector: e) (Vector: e*))
-           (cset-meet (cg e e*) (cg e* e))]
+           (% cset-meet (cg e e*) (cg e* e))]
           ;; boxes are invariant - generate constraints *both* ways
           [((Box: e) (Box: e*))
-           (cset-meet (cg e e*) (cg e* e))]
+           (% cset-meet (cg e e*) (cg e* e))]
           [((MPair: s t) (MPair: s* t*))
-           (cset-meet* (list (cg s s*) (cg s* s) (cg t t*) (cg t* t)))]
+           (% cset-meet* (% list (cg s s*) (cg s* s) (cg t t*) (cg t* t)))]
           [((Channel: e) (Channel: e*))
-           (cset-meet (cg e e*) (cg e* e))]
+           (% cset-meet (cg e e*) (cg e* e))]
           [((ThreadCell: e) (ThreadCell: e*))
-           (cset-meet (cg e e*) (cg e* e))]
+           (% cset-meet (cg e e*) (cg e* e))]
           [((Continuation-Mark-Keyof: e) (Continuation-Mark-Keyof: e*))
-           (cset-meet (cg e e*) (cg e* e))]
+           (% cset-meet (cg e e*) (cg e* e))]
           [((Prompt-Tagof: s t) (Prompt-Tagof: s* t*))
-           (cset-meet* (list (cg s s*) (cg s* s) (cg t t*) (cg t* t)))]
+           (% cset-meet* (% list (cg s s*) (cg s* s) (cg t t*) (cg t* t)))]
           [((Promise: e) (Promise: e*))
            (cg e e*)]
           [((Ephemeron: e) (Ephemeron: e*))
@@ -671,7 +694,7 @@
           ;; we assume all HTs are mutable at the moment
           [((Hashtable: s1 s2) (Hashtable: t1 t2))
            ;; for mutable hash tables, both are invariant
-           (cset-meet* (list (cg t1 s1) (cg s1 t1) (cg t2 s2) (cg s2 t2)))]
+           (% cset-meet* (% list (cg t1 s1) (cg s1 t1) (cg t2 s2) (cg s2 t2)))]
           ;; syntax is covariant
           [((Syntax: s1) (Syntax: s2))
            (cg s1 s2)]
@@ -680,26 +703,26 @@
            (cg s1 s2)]
           ;; parameters are just like one-arg functions
           [((Param: in1 out1) (Param: in2 out2))
-           (cset-meet (cg in2 in1) (cg out1 out2))]
+           (% cset-meet (cg in2 in1) (cg out1 out2))]
           ;; every function is trivially below top-arr
           [((Function: _)
             (Function: (list (top-arr:))))
            empty]
           [((Function: (list s-arr ...))
             (Function: (list t-arr ...)))
-           (cset-meet*
-            (for/list ([t-arr (in-list t-arr)])
+           (% cset-meet*
+            (for/list/fail ([t-arr (in-list t-arr)])
               ;; for each element of t-arr, we need to get at least one element of s-arr that works
-              (let ([results (filter values
-                                     (for/list ([s-arr (in-list s-arr)])
-                                       (with-handlers ([exn:infer? (lambda (_) #f)])
-                                         (cgen/arr V X Y s-arr t-arr))))])
+              (let ([results (for*/list ([s-arr (in-list s-arr)]
+                                         [v (in-value (cgen/arr V X Y s-arr t-arr))]
+                                         #:when v)
+                               v)])
                 ;; ensure that something produces a constraint set
-                (when (null? results) (fail! S T))
-                (cset-combine results))))]
+                (and (not (null? results))
+                     (cset-join results)))))]
           [(_ _)
            ;; nothing worked, and we fail
-           (fail! S T)]))))
+           #f]))))
 
 ;; C : cset? - set of constraints found by the inference engine
 ;; Y : (listof symbol?) - index variables that must have entries
@@ -813,15 +836,14 @@
 (define/cond-contract (cgen/list V X Y S T
                                  #:expected-cset [expected-cset (empty-cset '() '())])
   (((listof symbol?) (listof symbol?) (listof symbol?) (listof Values/c) (listof Values/c))
-   (#:expected-cset cset?) . ->* . cset?)
-  (unless (= (length S) (length T))
-    (fail! S T))
-  (cset-meet*
-   (for/list ([s (in-list S)] [t (in-list T)])
-             ;; We meet early to prune the csets to a reasonable size.
-             ;; This weakens the inference a bit, but sometimes avoids
-             ;; constraint explosion.
-             (cset-meet (cgen V X Y s t) expected-cset))))
+   (#:expected-cset cset?) . ->* . (or/c cset? #f))
+  (and (= (length S) (length T))
+       (% cset-meet*
+          (for/list/fail ([s (in-list S)] [t (in-list T)])
+                         ;; We meet early to prune the csets to a reasonable size.
+                         ;; This weakens the inference a bit, but sometimes avoids
+                         ;; constraint explosion.
+            (% cset-meet (cgen V X Y s t) expected-cset)))))
 
 
 
@@ -841,13 +863,13 @@
       (or/c #f Values/c ValuesDots?))
      ((or/c #f Values/c AnyValues? ValuesDots?))
      . ->* . (or/c boolean? substitution/c))
-    (with-handlers ([exn:infer? (lambda _ #f)])
-      (let* ([expected-cset (if expected
-                                (cgen null X Y R expected)
-                                (empty-cset '() '()))]
-             [cs  (cgen/list null X Y S T #:expected-cset expected-cset)]
-             [cs* (cset-meet cs expected-cset)])
-            (if R (subst-gen cs* Y R) #t))))
+    (let* ([expected-cset (if expected
+                              (cgen null X Y R expected)
+                              (empty-cset '() '()))]
+           [cs  (and expected-cset
+                     (cgen/list null X Y S T #:expected-cset expected-cset))]
+           [cs* (% cset-meet cs expected-cset)])
+      (and cs* (if R (subst-gen cs* Y R) #t))))
    infer)) ;to export a variable binding and not syntax
 
 ;; like infer, but T-var is the vararg type:
@@ -859,22 +881,30 @@
 ;; like infer, but dotted-var is the bound on the ...
 ;; and T-dotted is the repeated type
 (define (infer/dots X dotted-var S T T-dotted R must-vars #:expected [expected #f])
-  (with-handlers ([exn:infer? (lambda _ #f)])
-    (let* ([short-S (take S (length T))]
-           [rest-S (drop S (length T))]
-           [expected-cset (if expected
-                              (cgen null X (list dotted-var) R expected)
-                              (empty-cset '() '()))]
-           [cs-short (cgen/list null X (list dotted-var) short-S T
-                                #:expected-cset expected-cset)]
-           [new-vars (var-store-take dotted-var T-dotted (length rest-S))]
-           [new-Ts (for/list ([v (in-list new-vars)])
-                     (substitute (make-F v) dotted-var
-                                 (substitute-dots (map make-F new-vars) #f dotted-var T-dotted)))]
-           [cs-dotted (cgen/list null (append new-vars X) (list dotted-var) rest-S new-Ts
-                                 #:expected-cset expected-cset)]
-           [cs-dotted* (move-vars-to-dmap cs-dotted dotted-var new-vars)]
-           [cs (cset-meet cs-short cs-dotted*)])
-      (subst-gen (cset-meet cs expected-cset) (list dotted-var) R))))
+  (early-return
+   (define short-S (take S (length T)))
+   (define rest-S (drop S (length T)))
+   (define expected-cset (if expected
+                             (cgen null X (list dotted-var) R expected)
+                             (empty-cset '() '())))
+   #:return-unless expected-cset #f
+   (define cs-short (cgen/list null X (list dotted-var) short-S T
+                               #:expected-cset expected-cset))
+   #:return-unless cs-short #f
+   (define new-vars (var-store-take dotted-var T-dotted (length rest-S)))
+   (define new-Ts (for/list ([v (in-list new-vars)])
+                            (substitute (make-F v) dotted-var
+                                        (substitute-dots (map make-F new-vars)
+                                                         #f dotted-var T-dotted))))
+   (define cs-dotted (cgen/list null (append new-vars X) (list dotted-var) rest-S new-Ts
+                                #:expected-cset expected-cset))
+   #:return-unless cs-dotted #f
+   (define cs-dotted* (move-vars-to-dmap cs-dotted dotted-var new-vars))
+   #:return-unless cs-dotted* #f
+   (define cs (cset-meet cs-short cs-dotted*))
+   #:return-unless cs #f
+   (define m (cset-meet cs expected-cset))
+   #:return-unless m #f
+   (subst-gen m (list dotted-var) R)))
+
 
-;(trace cgen)
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/signatures.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/signatures.rkt
index 3d0606d62e..86168f8c3f 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/signatures.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/signatures.rkt
@@ -7,26 +7,20 @@
 (provide (all-defined-out))
 
 (define-signature dmap^
-  ([cond-contracted dmap-meet (dmap? dmap? . -> . dmap?)]))
+  ([cond-contracted dmap-meet (dmap? dmap? . -> . (or/c #f dmap?))]))
 
 (define-signature promote-demote^
   ([cond-contracted var-promote (Type/c (listof symbol?) . -> . Type/c)]
    [cond-contracted var-demote  (Type/c (listof symbol?) . -> . Type/c)]))
 
 (define-signature constraints^
-  ([cond-contracted exn:infer? (any/c . -> . boolean?)]
-   [cond-contracted fail-sym symbol?]
-   ;; inference failure - masked before it gets to the user program
-   (define-syntaxes (fail!)
-     (syntax-rules ()
-       [(_ s t) (raise (list fail-sym s t))]))
-   [cond-contracted cset-meet (cset? cset? . -> . cset?)]
-   [cond-contracted cset-meet* ((listof cset?) . -> . cset?)]
+  ([cond-contracted cset-meet (cset? cset? . -> . (or/c #f cset?))]
+   [cond-contracted cset-meet* ((listof cset?) . -> . (or/c #f cset?))]
    no-constraint
    [cond-contracted empty-cset ((listof symbol?) (listof symbol?) . -> . cset?)]
    [cond-contracted insert (cset? symbol? Type/c Type/c . -> . cset?)]
-   [cond-contracted cset-combine ((listof cset?) . -> . cset?)]
-   [cond-contracted c-meet ((c? c?) (symbol?) . ->* . c?)]))
+   [cond-contracted cset-join ((listof cset?) . -> . cset?)]
+   [cond-contracted c-meet ((c? c?) (symbol?) . ->* . (or/c #f c?))]))
 
 (define-signature restrict^
   ([cond-contracted restrict ((Type/c Type/c) ((or/c 'new 'orig)) . ->* . Type/c)]))
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/check-below.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/check-below.rkt
index dcf6f40fab..cc4df2a55b 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/check-below.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/check-below.rkt
@@ -9,9 +9,9 @@
          (only-in (types printer) pretty-format-type))
 
 (provide/cond-contract
- [check-below (-->i ([s (-or/c Type/c full-tc-results/c)]
+ [check-below (-->i ([s (-or/c Type/c tc-results/c)]
                      [t (s) (if (Type/c? s) Type/c tc-results/c)])
-                    [_ (s) (if (Type/c? s) Type/c full-tc-results/c)])]
+                    [_ (s) (if (Type/c? s) Type/c tc-results/c)])]
  [cond-check-below (-->i ([s (-or/c Type/c full-tc-results/c)]
                           [t (s) (-or/c #f (if (Type/c? s) Type/c tc-results/c))])
                          [_ (s) (-or/c #f (if (Type/c? s) Type/c full-tc-results/c))])]
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/signatures.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/signatures.rkt
index c1e5953cad..cae827b74e 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/signatures.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/signatures.rkt
@@ -7,7 +7,7 @@
 
 (define-signature tc-expr^
   ([cond-contracted tc-expr (syntax? . -> . full-tc-results/c)]
-   [cond-contracted tc-expr/check (syntax? tc-results/c . -> . full-tc-results/c)]
+   [cond-contracted tc-expr/check (syntax? tc-results/c . -> . tc-results/c)]
    [cond-contracted tc-expr/check/t (syntax? tc-results/c . -> . Type/c)]
    [cond-contracted tc-body (syntax? . -> . full-tc-results/c)]
    [cond-contracted tc-body/check (syntax? tc-results/c . -> . full-tc-results/c)]
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
index 97cbf3f9ca..0021030071 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
@@ -86,7 +86,7 @@
 
 ;; tc-expr/check : syntax tc-results -> tc-results
 (define/cond-contract (tc-expr/check/internal form expected)
-  (--> syntax? tc-results/c full-tc-results/c)
+  (--> syntax? tc-results/c tc-results/c)
   (parameterize ([current-orig-stx form])
     ;(printf "form: ~a\n" (syntax-object->datum form))
     ;; the argument must be syntax
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
index 8338b6da52..ea3a56121e 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
@@ -37,7 +37,7 @@
 ;; TODO: make this function sane.
 (define/cond-contract (do-check expr->type namess expected-results exprs body expected)
   ((syntax? tc-results/c . -> . any/c)
-   (listof (listof identifier?)) (listof tc-results/c) (listof tc-results/c)
+   (listof (listof identifier?)) (listof tc-results/c)
    (listof syntax?) syntax? (or/c #f tc-results/c)
    . -> .
    tc-results/c)
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt
index ab9c5498e4..9d3c977b71 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt
@@ -65,8 +65,8 @@
 		 #:when (and (Type? t*) (type-equal? t t*)))
 	 n))
     (if (null? candidates)
-	#f
-	(sort candidates string>? #:key symbol->string))]
+        #f
+        (sort candidates string>? #:key symbol->string))]
    [else #f]))
 
 ;; print-<thing> : <thing> Output-Port Boolean -> Void
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt
index 581cc9dc0d..578a82cde6 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt
@@ -3,7 +3,7 @@
          racket/match racket/function racket/lazy-require racket/list
          (prefix-in c: (contract-req))
          (rep type-rep filter-rep object-rep rep-utils)
-         (utils tc-utils)
+         (utils tc-utils early-return)
          (types utils resolve base-abbrev match-expanders
                 numeric-tower substitute current-seen)
          (for-syntax racket/base syntax/parse unstable/sequence))
@@ -226,16 +226,6 @@
 	       (subtype* s t)
 	       (subtype* t s)))
 
-(define-syntax (early-return stx)
-  (syntax-parse stx
-    [(_ e:expr ... #:return-when e0:expr e1:expr rest ...)
-     #'(let ()
-         e ...
-         (if e0 e1
-             (early-return rest ...)))]
-    [(_ e:expr ...) #'(let () e ...)]))
-
-
 (define bottom-key (Rep-seq -Bottom))
 (define top-key (Rep-seq Univ))
 
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/early-return.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/early-return.rkt
new file mode 100644
index 0000000000..91705830df
--- /dev/null
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/early-return.rkt
@@ -0,0 +1,24 @@
+#lang racket/base
+
+(require (for-syntax racket/base syntax/parse))
+(provide early-return)
+
+(define-syntax (early-return stx)
+  (syntax-parse stx
+    [(_ e:expr ... #:return-when e0:expr e1:expr rest ...)
+     (syntax/loc stx
+       (let ()
+         e ...
+         (if e0 e1
+             (early-return rest ...))))]
+    [(_ e:expr ... #:return-unless e0:expr e1:expr rest ...)
+     (syntax/loc stx
+       (let ()
+         e ...
+         (if e0
+             (early-return rest ...)
+             e1)))]
+    [(_ e:expr ...) (syntax/loc stx (let () e ...))]))
+
+
+
diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/values-dots2.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/values-dots2.rkt
new file mode 100644
index 0000000000..91abc3124d
--- /dev/null
+++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/values-dots2.rkt
@@ -0,0 +1,16 @@
+#lang typed/racket/base
+
+(: map-with-funcs (All (b c d e ) ((b c d e -> b)
+                                  (b c d e -> c) 
+                                  (b c d e -> d) 
+                                  (b c d e -> e) 
+                                  -> 
+                                  (b c d e -> (List b c d e)))))
+(define (map-with-funcs f1 f2 f3 f4)
+  (lambda (b0 c0 d0 e0 )
+    (list (f1 b0 c0 d0 e0 )
+          (f2 b0 c0 d0 e0 )
+          (f3 b0 c0 d0 e0 )
+          (f4 b0 c0 d0 e0 ))))
+
+(map-with-funcs + - * /)
diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/infer-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/infer-tests.rkt
index a6419ffca5..a84e8ee193 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/infer-tests.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/infer-tests.rkt
@@ -7,7 +7,7 @@
   (rep type-rep)
   (r:infer infer)
 
-  (types numeric-tower utils abbrev))
+  (types union substitute numeric-tower utils abbrev))
 
 (provide tests)
 (gen-test-main)
@@ -19,7 +19,7 @@
                 (fv ty*)
                 (list (quote elems) ...))))
 
-(define-syntax (infer-t stx)
+(begin-for-syntax
   (define-splicing-syntax-class vars
     (pattern (~seq) #:with vars #'empty)
     (pattern (~seq #:vars vars:expr) ))
@@ -29,14 +29,44 @@
   (define-splicing-syntax-class pass
     (pattern (~seq) #:with pass #'#t)
     (pattern #:pass #:with pass #'#t)
-    (pattern #:fail #:with pass #'#f))
+    (pattern #:fail #:with pass #'#f)))
+
+(define-syntax (infer-t stx)
   (syntax-parse stx
     ([_ S:expr T:expr :vars :indices :pass]
-     #'(test-case "foobar"
+     (syntax/loc stx
+       (test-case (format "~a ~a~a" S T (if pass "" " should fail"))
          (define result (infer vars indices (list S) (list T) #f))
          (unless (equal? result pass)
-           (fail-check "Could not infer a substitution"))))))
+           (fail-check "Could not infer a substitution")))))))
 
+(define-syntax (infer-l stx)
+  (syntax-parse stx
+    ([_ S:expr T:expr :vars :indices :pass]
+     (syntax/loc stx
+       (test-case (format "~a ~a~a" S T (if pass "" " should fail"))
+         (define result (infer vars indices S T #f))
+         (unless (equal? result pass)
+           (fail-check "Could not infer a substitution")))))))
+
+
+(define-syntax-rule (i2-t t1 t2 (a b) ...)
+  (test-equal? (format "~a ~a" t1 t2)
+               (infer (fv t1) null (list t2) (list t1) (-lst* (make-F a) ...) #f)
+               (make-immutable-hash (list (cons a (t-subst b)) ...))))
+
+(define-syntax-rule (i2-l t1 t2 fv (a b) ...)
+  (test-equal? (format "~a ~a" t2 t1)
+               (infer fv null t2 t1 (-lst* (make-F a) ...) #f)
+               (make-immutable-hash (list (cons a (t-subst b)) ...))))
+
+(define (f t1 t2) (infer (fv t1) null (list t1) (list t2) #f))
+
+(define-syntax-rule (i2-f t1 t2)
+  (infer-t t2 t1 #:vars (fv t2) #:fail))
+
+(define N -Number)
+(define B -Boolean)
 
 
 (define fv-tests
@@ -72,13 +102,47 @@
     (infer-t (make-ListDots (-v b) 'b) (make-ListDots (-v b) 'b) #:indices '(b))
     (infer-t (make-ListDots (-v b) 'b) (make-ListDots Univ 'b) #:indices '(b))
 
+    [infer-t (->... null ((-v a) a) (-v b)) (-> -Symbol -String) #:vars '(b) #:indices '(a)]
+    [infer-t (->... null ((-v a) a) (make-ListDots (-v a) 'a)) (-> -String -Symbol  (-lst* -String -Symbol)) #:indices '(a)]
+    [infer-t (->... (list (-v b)) ((-v a) a) (-v b)) (-> -String -Symbol -String) #:vars '(b) #:indices '(a)]
+
+    [infer-l (list (->... null ((-v b) b) (-v a)) (-> (-v a) -Boolean))
+             (list (-> -String -Symbol) (-> Univ -Boolean) -String)
+             #:vars '(a)
+             #:indices '(b)]
+    [infer-l (list (->... null ((-v a) a) (-v b)) (make-ListDots (-v a) 'a))
+             (list (-> -Symbol -Symbol -String) (-lst* -Symbol -Symbol))
+             #:vars '(b)
+             #:indices '(a)]
     ;; Currently Broken
     ;(infer-t (make-ListDots (-v b) 'b) (-lst -Symbol) #:indices '(b))
     ;(infer-t (-lst -Symbol) (make-ListDots -Symbol 'b) #:indices '(b))
     ;(infer-t (make-ListDots (-v b) 'b) (make-ListDots -Symbol 'b) #:indices '(b))
     ;(infer-t (make-ListDots -Symbol 'b) (make-ListDots (-v b) 'b) #:indices '(b))
     ;(infer-t (make-ListDots -Symbol 'b) (-pair -Symbol (-lst -Symbol)) #:indices '(b))
-  ))
+    [i2-t (-v a) N ('a N)]
+    [i2-t (-pair (-v a) (-v a)) (-pair N (Un N B)) ('a (Un N B))]
+    [i2-t (-lst (-v a)) (-pair N (-pair N (-val null))) ('a N)]
+    [i2-t (-lst (-v a)) (-pair N (-pair B (-val null))) ('a (Un N B))]
+    [i2-t Univ (Un N B)]
+    [i2-t ((-v a) . -> . (-v b)) (-> N N) ('b N) ('a (Un))]
+
+
+    [i2-l (list (-v a) (-v a) (-v b)) 
+          (list (Un (-val 1) (-val 2)) N N)
+          '(a b) ('b N) ('a N)]
+    [i2-l (list (-> (-v a) Univ) (-lst (-v a)))
+          (list (-> N (Un N B)) (-lst N))
+          '(a) ('a N)]
+    [i2-l (list (-> (-v a) (-v b)) (-lst (-v a)))
+          (list (-> N N) (-lst (Un (-val 1) (-val 2))))
+          '(a b) ('b N) ('a (Un (-val 1) (-val 2)))]
+    [i2-l (list  (-lst (-v a)))
+          (list  (-lst (Un B N)))
+          '(a) ('a (Un N B))]
+    ;; error tests
+    [i2-f (-lst (-v a)) Univ]
+    ))
 
 
 (define tests