diff --git a/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
index e18ae4ee..8dfd31e0 100644
--- a/typed-racket-lib/typed-racket/infer/infer-unit.rkt
+++ b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
@@ -220,12 +220,12 @@
       (substitute (make-F var) v ty*))))
 
 
-(define/cond-contract (cgen/prop context s t)
+(define/cond-contract (cgen/prop context p q)
   (context? Prop? Prop? . -> . (or/c #f cset?))
-  (match* (s t)
-    [(e e) (empty-cset/context context)]
-    [(e (TrueProp:)) (empty-cset/context context)]
-    [((FalseProp:) e) (empty-cset/context context)]
+  (match* (p q)
+    [(p p) (empty-cset/context context)]
+    [(p (TrueProp:)) (empty-cset/context context)]
+    [((FalseProp:) q) (empty-cset/context context)]
     ;; FIXME - is there something to be said about the logical ones?
     [((TypeProp: o s) (TypeProp: o t)) (cgen/inv context s t)]
     [((NotTypeProp: o s) (NotTypeProp: o t)) (cgen/inv context s t)]
@@ -919,7 +919,7 @@
    (substs-gen m X (list dotted-var) R #f)))
 
 
-;(trace subst-gen)
+;(trace substs-gen)
 ;(trace cgen)
 ;(trace cgen/list)
 ;(trace cgen/arr)
diff --git a/typed-racket-lib/typed-racket/typecheck/check-below.rkt b/typed-racket-lib/typed-racket/typecheck/check-below.rkt
index a83587e6..1ff6e72a 100644
--- a/typed-racket-lib/typed-racket/typecheck/check-below.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/check-below.rkt
@@ -3,10 +3,11 @@
 (require "../utils/utils.rkt"
          racket/match (prefix-in - (contract-req))
          racket/format
-         (types utils subtype prop-ops abbrev)
+         (env lexical-env)
+         (types utils subtype prop-ops abbrev tc-result)
          (utils tc-utils)
          (rep type-rep object-rep prop-rep)
-         (typecheck error-message))
+         (typecheck error-message tc-envops))
 
 (provide/cond-contract
  [check-below (-->i ([s (-or/c Type? full-tc-results/c)]
@@ -14,8 +15,7 @@
                     [_ (s) (if (Type? s) Type? full-tc-results/c)])]
  [cond-check-below (-->i ([s (-or/c Type? full-tc-results/c)]
                           [t (s) (-or/c #f (if (Type? s) Type? tc-results/c))])
-                         [_ (s) (-or/c #f (if (Type? s) Type? full-tc-results/c))])]
- [fix-results (--> tc-results/c full-tc-results/c)])
+                         [_ (s) (-or/c #f (if (Type? s) Type? full-tc-results/c))])])
 
 (provide type-mismatch)
 
@@ -45,38 +45,6 @@
     (value-string expected) (value-string actual)
     "mismatch in number of values"))
 
-;; fix-props:
-;;  PropSet [PropSet] -> PropSet
-;;    or
-;;  Prop [Prop]       -> Prop
-;; Turns #f prop/propset into the actual prop; leaves other props alone.
-(define (fix-props p1 [p2 -tt-propset])
-  (or p1 p2))
-
-;; fix-object: Object [Object] -> Object
-;; Turns #f into the actual object; leaves other objects alone.
-(define (fix-object o1 [o2 -empty-obj])
-  (or o1 o2))
-
-;; fix-results: tc-results -> tc-results
-;; Turns #f Prop or Obj into the Empty/Trivial
-(define (fix-results r)
-  (match r
-    [(tc-any-results: f) (tc-any-results (fix-props f -tt))]
-    [(tc-results: ts ps os)
-     (ret ts (map fix-props ps) (map fix-object os))]
-    [(tc-results: ts ps os dty dbound)
-     (ret ts (map fix-props ps) (map fix-object os) dty dbound)]))
-
-(define (fix-results/bottom r)
-  (match r
-    [(tc-any-results: f) (tc-any-results (fix-props f -ff))]
-    [(tc-results: ts ps os)
-     (ret ts (for/list ([p ps]) (fix-props p -ff-propset)) (map fix-object os))]
-    [(tc-results: ts ps os dty dbound)
-     (ret ts (for/list ([p ps]) (fix-props p -ff-propset)) (map fix-object os) dty dbound)]))
-
-
 
 ;; check-below : (/\ (Results Type -> Result)
 ;;                   (Results Results -> Result)
@@ -88,8 +56,18 @@
       [(p p) #t]
       [(p #f) #t]
       [((PropSet: p1+ p1-) (PropSet: p2+ p2-))
-       (and (implies? p1+ p2+)
-            (implies? p1- p2-))]
+       (define positive-implies?
+         (or (TrueProp? p2+)
+             (FalseProp? p1+)
+             (let ([p1-and-not-p2 (-and p1+ (negate-prop p2+))])
+               (or (FalseProp? p1-and-not-p2)
+                   (impossible-in-lexical-env? p1-and-not-p2)))))
+       (and positive-implies?
+            (or (TrueProp? p2-)
+                (FalseProp? p1-)
+                (let ([p1-and-not-p2 (-and p1- (negate-prop p2-))])
+                  (or (FalseProp? p1-and-not-p2)
+                      (impossible-in-lexical-env? p1-and-not-p2)))))]
       [(_ _) #f]))
   (define (object-better? o1 o2)
     (match* (o1 o2)
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt b/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
index 6f230e74..0efdb596 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
@@ -6,6 +6,7 @@
          (contract-req)
          (rep type-rep prop-rep object-rep rep-utils)
          (utils tc-utils)
+         racket/set
          (types tc-result resolve subtype update prop-ops)
          (env type-env-structs lexical-env mvar-env)
          (rename-in (types abbrev)
@@ -14,64 +15,82 @@
                     [one-of/c -one-of/c])
          (typecheck tc-metafunctions))
 
-(provide with-lexical-env/extend-props)
+(provide with-lexical-env+props
+         impossible-in-lexical-env?)
+
+(define (impossible-in-lexical-env? p)
+  (not (env+ (lexical-env) (list p))))
 
 ;; Returns #f if anything becomes (U)
 (define (env+ env ps)
-  (define-values (props atoms) (combine-props ps (env-props env)))
   (cond
-    [props
-     (let loop ([ps atoms]
-                [negs '()]
-                [Γ (env-replace-props env props)])
-       (match ps
-         [(cons p ps)
-          (match p
-            [(TypeProp: (Path: lo x) pt)
-             #:when (and (not (is-var-mutated? x))
-                         (identifier-binding x))
-             (let* ([t (lookup-type/lexical x Γ #:fail (lambda _ Univ))]
-                    [new-t (update t pt #t lo)])
-               (if (Bottom? new-t)
-                   (values #f '())
-                   (loop ps negs (env-set-type Γ x new-t))))]
-            ;; process negative info _after_ positive info so we don't miss anything
-            [(NotTypeProp: (Path: _ x) _)
-             #:when (and (not (is-var-mutated? x))
-                         (identifier-binding x))
-             (loop ps (cons p negs) Γ)]
-            [_ (loop ps negs Γ)])]
-         [_ (let ([Γ (let loop ([negs negs]
-                                [Γ Γ])
-                       (match negs
-                         [(cons (NotTypeProp: (Path: lo x) pt) rst)
-                          (let* ([t (lookup-type/lexical x Γ #:fail (lambda _ Univ))]
-                                 [new-t (update t pt #f lo)])
-                            (if (Bottom? new-t)
-                                #f
-                                (loop rst (env-set-type Γ x new-t))))]
-                         [_ Γ]))])
-              (values Γ atoms))]))]
-    [else (values #f '())]))
+    [(null? ps) env]
+    [else
+     (define-values (props atoms) (combine-props ps (env-props env)))
+     (cond
+       [props
+        (let loop ([ps atoms]
+                   [negs '()]
+                   [Γ (env-replace-props env props)])
+          (match ps
+            [(cons p ps)
+             (match p
+               [(TypeProp: (Path: lo x) pt)
+                #:when (and (not (is-var-mutated? x))
+                            (identifier-binding x))
+                (let* ([t (lookup-type/lexical x Γ #:fail (λ (_) Univ))]
+                       [new-t (update t pt #t lo)])
+                  (and (not (Bottom? new-t))
+                       (loop ps negs (env-set-type Γ x new-t))))]
+               ;; process negative info _after_ positive info so we don't miss anything
+               [(NotTypeProp: (Path: _ x) _)
+                #:when (and (not (is-var-mutated? x))
+                            (identifier-binding x))
+                (loop ps (cons p negs) Γ)]
+               [_ (loop ps negs Γ)])]
+            [_ (let ([Γ (let loop ([negs negs]
+                                   [Γ Γ])
+                          (match negs
+                            [(cons (NotTypeProp: (Path: lo x) pt) rst)
+                             (let* ([t (lookup-type/lexical x Γ #:fail (λ (_) Univ))]
+                                    [new-t (update t pt #f lo)])
+                               (and (not (Bottom? new-t))
+                                    (loop rst (env-set-type Γ x new-t))))]
+                            [_ Γ]))])
+                 (and Γ (env-replace-props Γ (append atoms (env-props Γ)))))]))]
+       [else #f])]))
 
-;; run code in an extended env and with replaced props. Requires the body to return a tc-results.
-;; TODO make this only add the new prop instead of the entire environment once tc-id is fixed to
-;; include the interesting props in its prop.
-;; TODO figure out what the heck the above TODO means -amk
+
+;; run code in an extended env and with replaced props.
+;; Requires the body to return a tc-results.
 ;; WARNING: this may bail out when code is unreachable
-(define-syntax (with-lexical-env/extend-props stx)
+(define-syntax (with-lexical-env+props stx)
   (define-splicing-syntax-class unreachable?
     (pattern (~seq #:unreachable form:expr))
     (pattern (~seq) #:with form #'(begin)))
   (syntax-parse stx
-    [(_ ps:expr u:unreachable? . b)
-     #'(let-values ([(new-env atoms) (env+ (lexical-env) ps)])
+    [(_ ps:expr
+        #:expected expected
+        u:unreachable? . b)
+     (syntax/loc stx
+       (let ([old-props (env-props (lexical-env))]
+             [new-env (env+ (lexical-env) ps)])
          (cond
            [new-env
             (with-lexical-env
-             new-env
-             (add-unconditional-prop (let () . b) (apply -and (append atoms (env-props new-env)))))]
+              new-env
+              (let ([result (let () . b)])
+                (match expected
+                  ;; if there was not any expected results, then
+                  ;; return any new info that was learned while
+                  ;; extending the environment
+                  [(or #f (tc-any-results: #f))
+                   (define new-props
+                     (make-AndProp (set-subtract (env-props new-env) old-props)))
+                   (add-unconditional-prop result new-props)]
+                  ;; otherwise, just return the expected results
+                  [_ (fix-results expected)])))]
            [else
             ;; unreachable, bail out
             u.form
-            (ret -Bottom)]))]))
+            (ret -Bottom)])))]))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
index 262575d8..b8db950f 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
@@ -339,33 +339,29 @@
 ;; Body must be a non empty sequence of expressions to typecheck.
 ;; The final one will be checked against expected.
 (define (tc-body/check body expected)
-  (match (syntax->list body)
-    [(list es ... e-final)
-     ;; First, typecheck all the forms whose results are discarded.
-     ;; If any one those causes the rest to be unreachable (e.g. `exit' or `error`,
-     ;; then mark the rest as ignored.
-     (let loop ([es es])
-       (cond [(empty? es) ; Done, typecheck the return form.
-              (tc-expr/check e-final expected)]
-             [else
-              ;; Typecheck the first form.
-              (define e (first es))
-              (define results (tc-expr/check e (tc-any-results #f)))
-              (define props
-                (match results
-                  [(tc-any-results: f) (list f)]
-                  [(tc-results: _ (list (PropSet: p+ p-) ...) _)
-                   (map -or p+ p-)]
-                  [(tc-results: _ (list (PropSet: p+ p-) ...) _ _ _)
-                   (map -or p+ p-)]))
-              (with-lexical-env/extend-props
-               props
-               ;; If `e` bails out, mark the rest as ignored.
-               #:unreachable (for ([x (in-list (cons e-final (rest es)))])
-                               (register-ignored! x))
-               ;; Keep going with an environment extended with the propositions that are
-               ;; true if execution reaches this point.
-               (loop (rest es)))]))]))
+  (define any-res (tc-any-results #f))
+  (define exps (syntax->list body))
+  (let loop ([exps exps])
+    (match exps
+      [(list tail-exp) (tc-expr/check tail-exp expected)]
+      [(cons e rst)
+       (define results (tc-expr/check e any-res))
+       (define props
+         (match results
+           [(tc-any-results: p) (list p)]
+           [(tc-results: _ (list (PropSet: p+ p-) ...) _)
+            (map -or p+ p-)]
+           [(tc-results: _ (list (PropSet: p+ p-) ...) _ _ _)
+            (map -or p+ p-)]))
+       (with-lexical-env+props
+         props
+         #:expected any-res
+         ;; If `e` bails out, mark the rest as ignored.
+         #:unreachable (for-each register-ignored! rst)
+         ;; Keep going with an environment extended with the
+         ;; propositions that are true if execution reaches this
+         ;; point.
+         (loop rst))])))
 
 ;; find-stx-type : Any [(or/c Type? #f)] -> Type?
 ;; recursively find the type of either a syntax object or the result of syntax-e
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt b/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
index 255ec3d3..b5955c1e 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
@@ -8,7 +8,7 @@
          (for-syntax syntax/parse racket/base)
          (types utils subtype resolve abbrev
                 substitute classes prop-ops)
-         (typecheck tc-metafunctions tc-app-helper)
+         (typecheck tc-metafunctions tc-app-helper tc-subst)
          (rep type-rep)
          (r:infer infer))
 
@@ -35,8 +35,15 @@
                         #:name (and (identifier? f-stx) f-stx)
                         #:expected expected))))]))
 
+(define (subst-dom-objs argtys argobjs rng)
+  (subst-rep rng (for/list ([o (in-list argobjs)]
+                            [t (in-list argtys)]
+                            [idx (in-naturals)]
+                            #:when (not (Empty? o)))
+                   (list (cons 0 idx) o t))))
+
 (define (tc/funapp f-stx args-stx f-type args-res expected)
-  (match-define (list (tc-result1: argtys (PropSet: argps+ argps-) _) ...) args-res)
+  (match-define (list (tc-result1: argtys (PropSet: argps+ argps-) argobjs) ...) args-res)
   (define result
     (match f-type
       ;; we special-case this (no case-lambda) for improved error messages
@@ -74,18 +81,19 @@
         ;; Only try to infer the free vars of the rng (which includes the vars
         ;; in props/objects).
         (λ (dom rng rest drest a)
-          (extend-tvars fixed-vars
-                        (cond
-                          [drest
-                           (infer/dots
-                            fixed-vars dotted-var argtys dom (car drest) rng (fv rng)
-                            #:expected (and expected (tc-results->values expected)))]
-                          [rest
-                           (infer/vararg fixed-vars (list dotted-var) argtys dom rest rng
-                                         (and expected (tc-results->values expected)))]
-                          ;; no rest or drest
-                          [else (infer fixed-vars (list dotted-var) argtys dom rng
-                                       (and expected (tc-results->values expected)))])))
+          (let ([rng (subst-dom-objs argtys argobjs rng)])
+            (extend-tvars fixed-vars
+                          (cond
+                            [drest
+                             (infer/dots
+                              fixed-vars dotted-var argtys dom (car drest) rng (fv rng)
+                              #:expected (and expected (tc-results->values expected)))]
+                            [rest
+                             (infer/vararg fixed-vars (list dotted-var) argtys dom rest rng
+                                           (and expected (tc-results->values expected)))]
+                            ;; no rest or drest
+                            [else (infer fixed-vars (list dotted-var) argtys dom rng
+                                         (and expected (tc-results->values expected)))]))))
         f-type args-res expected)]
       ;; regular polymorphic functions without dotted rest, 
       ;; we do not choose any instantiations with mandatory keyword arguments
@@ -99,9 +107,10 @@
         ;; Only try to infer the free vars of the rng (which includes the vars
         ;; in props/objects).
         (λ (dom rng rest kw? a)
-          (extend-tvars vars
-                        (infer/vararg vars null argtys dom rest rng
-                                      (and expected (tc-results->values expected)))))
+          (let ([rng (subst-dom-objs argtys argobjs rng)])
+            (extend-tvars vars
+                          (infer/vararg vars null argtys dom rest rng
+                                        (and expected (tc-results->values expected))))))
         f-type args-res expected)]
       ;; Row polymorphism. For now we do really dumb inference that only works
       ;; in very restricted cases, but is probably enough for most cases in
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-if.rkt b/typed-racket-lib/typed-racket/typecheck/tc-if.rkt
index c5a211bd..057699b0 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-if.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-if.rkt
@@ -12,17 +12,26 @@
 
 (define (tc/if-twoarm tst thn els [expected #f])
   (match (single-value tst)
-    [(tc-result1: _ (PropSet: ps+ ps-) _)
-     (define expected* (and expected (erase-props expected)))
-     (define results-t
-       (with-lexical-env/extend-props (list ps+)
+    [(tc-result1: _ (PropSet: p+ p-) _)
+     (define thn-res
+       (with-lexical-env+props (list p+)
+         #:expected expected
          #:unreachable (warn-unreachable thn)
          (test-position-add-true tst)
-         (tc-expr/check thn expected*)))
-     (define results-u
-       (with-lexical-env/extend-props (list ps-)
+         (tc-expr/check thn expected)))
+     (define els-res
+       (with-lexical-env+props (list p-)
+         #:expected expected
          #:unreachable (warn-unreachable els)
          (test-position-add-false tst)
-         (tc-expr/check els expected*)))
+         (tc-expr/check els expected)))
 
-     (merge-tc-results (list results-t results-u))]))
+     (match expected
+       ;; if there was not any expected results, then merge the 'then'
+       ;; and 'else' results so we propogate the correct info upwards
+       [(or #f (tc-any-results: #f))
+        (merge-tc-results (list thn-res els-res))]
+       ;; otherwise, the subcomponents have already been checked and
+       ;; we just return the expected result 'fixed' to replace any
+       ;; missing fields (i.e. #f props or objects)
+       [_ (fix-results expected)])]))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
index e1820ad1..f9d584d3 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
@@ -120,8 +120,9 @@
      #:aliased-objects aliased-objs]
     (erase-names
      ids-to-erase
-     (with-lexical-env/extend-props
+     (with-lexical-env+props
        props
+       #:expected expected
        ;; if a let rhs does not return, the body isn't checked
        #:unreachable (for ([form (in-list (syntax->list body))])
                        (register-ignored! form))
@@ -129,7 +130,7 @@
        ;; before checking the body
        (pre-body-thunk)
        ;; typecheck the body
-       (tc-body/check body (and expected (erase-props expected)))))))
+       (tc-body/check body expected)))))
 
 (define (tc-expr/maybe-expected/t e names)
   (syntax-parse names
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt b/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
index 699a6e50..f19ff935 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
@@ -5,7 +5,7 @@
          (except-in (types abbrev utils prop-ops tc-result)
                     -> ->* one-of/c)
          (rep type-rep prop-rep object-rep values-rep rep-utils)
-         (typecheck tc-subst check-below)
+         (typecheck tc-subst)
          (contract-req))
 
 (provide abstract-results
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt b/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
index b367b229..5dacf72a 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
@@ -27,6 +27,7 @@
                   tc-results/c
                   tc-results/c)])
 
+(provide subst-rep)
 
 ;; Substitutes the given objects into the values and turns it into a
 ;; tc-result.  This matches up to the substitutions in the T-App rule
diff --git a/typed-racket-lib/typed-racket/types/prop-ops.rkt b/typed-racket-lib/typed-racket/types/prop-ops.rkt
index 5d1151ba..69d63610 100644
--- a/typed-racket-lib/typed-racket/types/prop-ops.rkt
+++ b/typed-racket-lib/typed-racket/types/prop-ops.rkt
@@ -298,7 +298,7 @@
 ;; Useful to express properties of the form: if this expressions returns at all, we learn this
 (define (add-unconditional-prop results prop)
   (match results
-    [(tc-any-results: f) (tc-any-results (-and prop f))]
+    [(tc-any-results: p) (tc-any-results (-and prop p))]
     [(tc-results: ts (list (PropSet: ps+ ps-) ...) os)
      (ret ts
           (for/list ([p+ (in-list ps+)]
diff --git a/typed-racket-lib/typed-racket/types/tc-result.rkt b/typed-racket-lib/typed-racket/types/tc-result.rkt
index f2aff49b..76b0239a 100644
--- a/typed-racket-lib/typed-racket/types/tc-result.rkt
+++ b/typed-racket-lib/typed-racket/types/tc-result.rkt
@@ -132,6 +132,38 @@
                      (list (-tc-result t pset o)))
                  (cons dty dbound))]))
 
+
+;; fix-props:
+;;  PropSet [PropSet] -> PropSet
+;;    or
+;;  Prop [Prop]       -> Prop
+;; Turns #f prop/propset into the actual prop; leaves other props alone.
+(define (fix-props p1 [p2 -tt-propset])
+  (or p1 p2))
+
+;; fix-object: Object [Object] -> Object
+;; Turns #f into the actual object; leaves other objects alone.
+(define (fix-object o1 [o2 -empty-obj])
+  (or o1 o2))
+
+;; fix-results: tc-results -> tc-results
+;; Turns #f Prop or Obj into the Empty/Trivial
+(define (fix-results r)
+  (match r
+    [(tc-any-results: f) (tc-any-results (fix-props f -tt))]
+    [(tc-results: ts ps os)
+     (ret ts (map fix-props ps) (map fix-object os))]
+    [(tc-results: ts ps os dty dbound)
+     (ret ts (map fix-props ps) (map fix-object os) dty dbound)]))
+
+(define (fix-results/bottom r)
+  (match r
+    [(tc-any-results: f) (tc-any-results (fix-props f -ff))]
+    [(tc-results: ts ps os)
+     (ret ts (for/list ([p ps]) (fix-props p -ff-propset)) (map fix-object os))]
+    [(tc-results: ts ps os dty dbound)
+     (ret ts (for/list ([p ps]) (fix-props p -ff-propset)) (map fix-object os) dty dbound)]))
+
 (provide/cond-contract
  [ret
   (c:->i ([t (c:or/c Type? (c:listof Type?))])
@@ -162,4 +194,11 @@
  [tc-results? (c:any/c . c:-> . boolean?)]
  [tc-results/c c:flat-contract?]
  [tc-results1/c c:flat-contract?]
- [full-tc-results/c c:flat-contract?])
+ [full-tc-results/c c:flat-contract?]
+ [fix-results (c:-> tc-results/c full-tc-results/c)]
+ [fix-results/bottom (c:-> tc-results/c full-tc-results/c)]
+ [fix-props
+  (c:->* ((c:or/c #f Prop? PropSet?))
+         ((c:or/c Prop? PropSet?))
+         (c:or/c Prop? PropSet?))]
+ [fix-object (c:->* ((c:or/c #f OptObject?)) (OptObject?) OptObject?)])
diff --git a/typed-racket-test/succeed/slow-parser.rkt b/typed-racket-test/succeed/slow-parser.rkt
new file mode 100644
index 00000000..96e1463d
--- /dev/null
+++ b/typed-racket-test/succeed/slow-parser.rkt
@@ -0,0 +1,105 @@
+#lang racket/base
+
+;; implied-atomic? was improved for disjunctions
+;; these tests make sure those improvements
+;; are still working (these used to take
+;; an astronomical amount of time)
+
+(require racket/sandbox)
+
+(call-with-limits
+ 120
+ 500
+ (λ () (eval '(begin (module a typed/racket
+                       (provide baz)
+                       (: baz : (Any -> Any))
+                       (define (baz v)
+                         (match v
+                           [`(VARREF ,(? symbol? x)) 'return]
+                           [`(Lambda ,(app baz fs) ,e ...) 'return]
+                           [`(CaseLambda ,lc ...) 'return]
+                           [`(If ,(app baz cond) ,(app baz then) ,(app baz else)) 'return]
+                           [`(Begin ,e ...) 'return]
+                           [`(Begin0 ,(app baz e1) ,e ...) 'return]
+                           [`(LetValues (,lvs ...) ,e ...) 'return]
+                           [`(LetrecValues (,lvs ...) ,e ...) 'return]
+                           [`(SetBang ,(? symbol? x) ,(app baz e)) 'return]
+                           [`(Quote ,(app baz d)) 'return]
+                           [`(QuoteSyntax ,(app baz d)) 'return]
+                           [`(WithContMark ,(app baz e1) ,(app baz e2) ,(app baz e3)) 'return]
+                           [`(App ,e ...) 'return]
+                           [`(Top ,(? symbol? x)) 'return]
+                           [`(VariableReference ,(? symbol? x)) 'return]
+                           [`(VariableReferenceTop ,(? symbol? x)) 'return]
+                           [`(VariableReference1 ,(? symbol? x)) 'return]
+                           [`(VariableReferenceTop2 ,(? symbol? x)) 'return]
+                           [`(Quote2 ,(app baz d)) 'return]
+                           [`(QuoteSyntax3 ,(app baz d)) 'return]
+                           [`(VARREF2 ,(? symbol? x)) 'return]
+                           [`(Lambda2 ,(app baz fs) ,e ...) 'return]
+                           [`(CaseLambda2 ,lc ...) 'return]
+                           [`(If2 ,(app baz cond) ,(app baz then) ,(app baz else)) 'return]
+                           [`(Begin2 ,e ...) 'return]
+                           [`(Begin02 ,(app baz e1) ,e ...) 'return]
+                           [`(VariableReference3 ,(? symbol? x)) 'return]
+                           [`(VariableReferenceTop3 ,(? symbol? x)) 'return]
+                           [`(Quote3 ,(app baz d)) 'return]
+                           [`(QuoteSyntax4 ,(app baz d)) 'return]
+                           [`(VARREF3 ,(? symbol? x)) 'return]
+                           [`(Lambda3 ,(app baz fs) ,e ...) 'return]
+                           [`(CaseLambda3 ,lc ...) 'return]
+                           [`(If3 ,(app baz cond) ,(app baz then) ,(app baz else)) 'return]
+                           [`(Begin3 ,e ...) 'return]
+                           [`(Begin03 ,(app baz e1) ,e ...) 'return]
+                           [`(Begin11 ,e ...) 'return]
+                           [`(Begin011 ,(app baz e1) ,e ...) 'return]
+                           [`(VariableReference11 ,(? symbol? x)) 'return]
+                           [`(VariableReferenceTop11 ,(? symbol? x)) 'return]
+                           [`(Quote11 ,(app baz d)) 'return]
+                           [`(QuoteSyntax11 ,(app baz d)) 'return]
+                           [`(VARREF11 ,(? symbol? x)) 'return]
+                           [`(Lambda11 ,(app baz fs) ,e ...) 'return]
+                           [`(CaseLambda11 ,lc ...) 'return]
+                           [`(If11 ,(app baz cond) ,(app baz then) ,(app baz else)) 'return]
+                           [`(Begin11 ,e ...) 'return]
+                           [`(Begin11 ,(app baz e1) ,e ...) 'return]
+                           [`(Begin12 ,e ...) 'return]
+                           [`(Begin012 ,(app baz e1) ,e ...) 'return]
+                           [`(VariableReference12 ,(? symbol? x)) 'return]
+                           [`(VariableReferenceTop12 ,(? symbol? x)) 'return]
+                           [`(Quote12 ,(app baz d)) 'return]
+                           [`(QuoteSyntax12 ,(app baz d)) 'return]
+                           [`(VARREF12 ,(? symbol? x)) 'return]
+                           [`(Lambda12 ,(app baz fs) ,e ...) 'return]
+                           [`(CaseLambda12 ,lc ...) 'return]
+                           [`(If12 ,(app baz cond) ,(app baz then) ,(app baz else)) 'return]
+                           [`(Begin12 ,e ...) 'return]
+                           [`(Begin12 ,(app baz e1) ,e ...) 'return]
+                           [`(Begin13 ,e ...) 'return]
+                           [`(Begin013 ,(app baz e1) ,e ...) 'return]
+                           [`(VariableReference13 ,(? symbol? x)) 'return]
+                           [`(VariableReferenceTop13 ,(? symbol? x)) 'return]
+                           [`(Quote13 ,(app baz d)) 'return]
+                           [`(QuoteSyntax13 ,(app baz d)) 'return]
+                           [`(VARREF13 ,(? symbol? x)) 'return]
+                           [`(Lambda13 ,(app baz fs) ,e ...) 'return]
+                           [`(CaseLambda13 ,lc ...) 'return]
+                           [`(If13 ,(app baz cond) ,(app baz then) ,(app baz else)) 'return]
+                           [`(Begin13 ,e ...) 'return]
+                           [`(Begin13 ,(app baz e1) ,e ...) 'return]
+                           [`(Begin14 ,e ...) 'return]
+                           [`(Begin014 ,(app baz e1) ,e ...) 'return]
+                           [`(VariableReference14 ,(? symbol? x)) 'return]
+                           [`(VariableReferenceTop14 ,(? symbol? x)) 'return]
+                           [`(Quote14 ,(app baz d)) 'return]
+                           [`(QuoteSyntax14 ,(app baz d)) 'return]
+                           [`(VARREF14 ,(? symbol? x)) 'return]
+                           [`(Lambda14 ,(app baz fs) ,e ...) 'return]
+                           [`(CaseLambda14 ,lc ...) 'return]
+                           [`(If14 ,(app baz cond) ,(app baz then) ,(app baz else)) 'return]
+                           [`(Begin14 ,e ...) 'return]
+                           [`(Begin14 ,(app baz e1) ,e ...) 'return]
+                           )))
+                     (require 'a)
+                     baz)
+             (make-base-namespace))))