diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
index 08fa5c82dd..b01e14cd81 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
@@ -8,7 +8,7 @@
          (infer-in infer)
          (rep type-rep filter-rep object-rep rep-utils)
          (utils tc-utils)
-         (types resolve subtype remove-intersect union filter-ops)
+         (types tc-result resolve subtype remove-intersect union filter-ops)
          (env type-env-structs lexical-env)
          (rename-in (types abbrev)
                     [-> -->]
@@ -18,9 +18,6 @@
 
 (provide
   with-lexical-env/extend-props)
-(provide/cond-contract
-  [env+ (([e env?] [fs (listof Filter/c)] [bx (box/c boolean?)])
-         #:pre (bx) (unbox bx) . ->i . [_ env?])])
 
 (define/cond-contract (update t ft pos? lo)
   (Type/c Type/c boolean? (listof PathElem?) . -> . Type/c)
@@ -63,29 +60,35 @@
      (int-err "update along ill-typed path: ~a ~a ~a" t t* lo)
      t]))
 
-;; sets the flag box to #f if anything becomes (U)
-(define (env+ env fs flag)
-  (define-values (props atoms) (combine-props fs (env-props env) flag))
-  (for/fold ([Γ (replace-props env (append atoms props))]) ([f (in-list atoms)])
-    (match f
-      [(Bot:) (set-box! flag #f) (env-map (lambda (k v) (Un)) Γ)]
-      [(or (TypeFilter: ft (Path: lo x)) (NotTypeFilter: ft (Path: lo x)))
-       (update-type/lexical
-         (lambda (x t) (let ([new-t (update t ft (TypeFilter? f) lo)])
-                         (when (type-equal? new-t -Bottom)
-                           (set-box! flag #f))
-                         new-t))
-         x Γ)]
-      [_ Γ])))
+;; Returns #f if anything becomes (U)
+(define (env+ env fs)
+  (let/ec exit
+    (define-values (props atoms) (combine-props fs (env-props env) exit))
+    (for/fold ([Γ (replace-props env (append atoms props))]) ([f (in-list atoms)])
+      (match f
+        [(or (TypeFilter: ft (Path: lo x)) (NotTypeFilter: ft (Path: lo x)))
+         (update-type/lexical
+           (lambda (x t)
+             (define new-t (update t ft (TypeFilter? f) lo))
+             (when (type-equal? new-t -Bottom)
+               (exit #f))
+             new-t)
+           x Γ)]
+        [_ Γ]))))
 
 ;; 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 filter.
 (define-syntax (with-lexical-env/extend-props stx)
-  (define-splicing-syntax-class flag
-    [pattern (~seq #:flag v:expr)]
-    [pattern (~seq) #:with v #'(box #t)])
+  (define-splicing-syntax-class unreachable?
+    (pattern (~seq #:unreachable form:expr))
+    (pattern (~seq) #:with form #'(begin)))
   (syntax-parse stx
-    [(_ ps flag:flag . b)
-     #'(with-lexical-env (env+ (lexical-env) ps flag.v)
-         (add-unconditional-prop (let () . b) (apply -and (env-props (lexical-env)))))]))
+    [(_ ps:expr u:unreachable? . b)
+     #'(let ([new-env (env+ (lexical-env) ps)])
+         (if new-env
+             (with-lexical-env new-env
+               (add-unconditional-prop (let () . b) (apply -and (env-props new-env))))
+             (let ()
+               u.form
+               (ret -Bottom))))]))
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-if.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-if.rkt
index 34fe39d4a3..60e8e1084a 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-if.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-if.rkt
@@ -13,28 +13,18 @@
 (export tc-if^)
 
 (define (tc/if-twoarm tst thn els [expected #f])
-  (define (tc expr reachable?)
-    (unless reachable? (warn-unreachable expr))
-    ;; If the code is unreachable, the resulting type should be Bottom.
-    (if reachable?
-        (tc-expr/check expr (and expected (erase-filter expected)))
-        (ret -Bottom)))
   (match (single-value tst)
-    [(tc-result1: _ (and f1 (FilterSet: fs+ fs-)) _)
-     (define flag+ (box #t))
-     (define flag- (box #t))
+    [(tc-result1: _ (FilterSet: fs+ fs-) _)
+     (define expected* (and expected (erase-filter expected)))
      (define results-t
-       (with-lexical-env/extend-props (list fs+) #:flag flag+
-         (add-unconditional-prop
-           (tc thn (unbox flag+)) fs+)))
+       (with-lexical-env/extend-props (list fs+)
+         #:unreachable (warn-unreachable thn)
+         (test-position-add-true tst)
+         (tc-expr/check thn expected*)))
      (define results-u
-       (with-lexical-env/extend-props (list fs-) #:flag flag-
-         (add-unconditional-prop
-           (tc els (unbox flag-)) fs-)))
+       (with-lexical-env/extend-props (list fs-)
+         #:unreachable (warn-unreachable els)
+         (test-position-add-false tst)
+         (tc-expr/check els expected*)))
 
-     ;; record reachability
-     (when (unbox flag+)
-       (test-position-add-true tst))
-     (when (unbox flag-)
-       (test-position-add-false tst))
      (merge-tc-results (list results-t results-u))]))
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
index e4cd3c89d5..3a6e1e2a49 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
@@ -55,8 +55,8 @@
       [(cons (AndFilter: ps*) ps) (loop (append ps* ps))]
       [(cons p ps) (cons p (loop ps))])))
 
-(define/cond-contract (combine-props new-props old-props flag)
-  ((listof Filter/c) (listof Filter/c) (box/c boolean?)
+(define/cond-contract (combine-props new-props old-props exit)
+  ((listof Filter/c) (listof Filter/c) (-> #f none/c)
    . -> .
    (values (listof (or/c ImpFilter? OrFilter?)) (listof (or/c TypeFilter? NotTypeFilter?))))
   (define (atomic-prop? p) (or (TypeFilter? p) (NotTypeFilter? p)))
@@ -93,7 +93,7 @@
 
             [(AndFilter: ps) (loop derived-formulas derived-atoms (append ps (cdr worklist)))]
             [(Top:) (loop derived-formulas derived-atoms (cdr worklist))]
-            [(Bot:) (set-box! flag #f) (values derived-formulas derived-atoms)])))))
+            [(Bot:) (exit #f)])))))
 
 
 (define (unconditional-prop res)
diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/metafunction-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/metafunction-tests.rkt
index ea57586057..dd2f696ab0 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/metafunction-tests.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/metafunction-tests.rkt
@@ -15,10 +15,12 @@
     [(_ new:expr existing:expr expected:expr box-v:expr)
      (quasisyntax/loc stx
        (test-case (~a '(new + existing = expected))
-         (define b (box #t))
-         (define-values (res-formulas res-props) (combine-props new existing b))
-         #,(syntax/loc stx (check-equal? (append res-formulas res-props) expected))
-         #,(syntax/loc stx (check-equal? (unbox b) box-v))))]))
+         (define success
+           (let/ec exit
+             (define-values (res-formulas res-props) (combine-props new existing exit))
+             #,(syntax/loc stx (check-equal? (append res-formulas res-props) expected))
+             #t))
+         #,(syntax/loc stx (check-equal? success box-v))))]))
 
 
 (define tests