diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-lambda.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-lambda.rkt
index 661fca83..4afe32bd 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-lambda.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-lambda.rkt
@@ -3,6 +3,7 @@
 (require "../../utils/utils.rkt"
          "signatures.rkt"
          "utils.rkt"
+         (prefix-in - (contract-req))
          syntax/parse racket/match racket/list
          unstable/sequence unstable/syntax
          (typecheck signatures find-annotation)
@@ -53,7 +54,9 @@
                       expected)))))
 
 
-(define (let-loop-check lam lp actuals args body expected)
+(define/cond-contract
+  (let-loop-check lam lp actuals args body expected)
+  (syntax? syntax? syntax? syntax? syntax? tc-results/c . --> . tc-results/c)
   (syntax-parse #`(#,args #,body #,actuals)
     #:literal-sets (kernel-literals lambda-literals)
     [((val acc ...)
@@ -76,8 +79,10 @@
                   [t (in-list ann-ts)])
          (tc-expr/check a (ret t)))
        ;; then check that the function typechecks with the inferred types
-       (add-typeof-expr lam (tc/rec-lambda/check args body lp ts expected))
-       expected)]
+       (define-values (fun-results body-results)
+         (tc/rec-lambda/check args body lp ts expected))
+       (add-typeof-expr lam fun-results)
+       body-results)]
     ;; special case `for/list'
     [((val acc ...)
       ((~and inner-body (if e1 e2 e3:id)))
@@ -95,8 +100,10 @@
                       [(tc-result1: (and t (Listof: _))) t]
                       [_ #f])
                     (generalize (-val '())))])
-       (add-typeof-expr lam (tc/rec-lambda/check args body lp (cons acc-ty ts) expected))
-       expected)]
+       (define-values (fun-results body-results)
+         (tc/rec-lambda/check args body lp (cons acc-ty ts) expected))
+       (add-typeof-expr lam fun-results)
+       body-results)]
     ;; special case when argument needs inference
     [(_ body* _)
      (let ([ts (for/list ([ac (in-syntax actuals)]
@@ -106,6 +113,8 @@
                    (if infer-t
                        (tc-expr/check/t ac (ret infer-t))
                        (generalize (tc-expr/t ac)))))])
-       (add-typeof-expr lam (tc/rec-lambda/check args body lp ts expected))
-       expected)]))
+       (define-values (fun-results body-results)
+         (tc/rec-lambda/check args body lp ts expected))
+       (add-typeof-expr lam fun-results)
+       body-results)]))
 
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
index e2afa1b6..94bc4592 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
@@ -520,12 +520,16 @@
 ;; name : the name of the loop
 ;; args : the types of the actual arguments to the loop
 ;; ret : the expected return type of the whole expression
-(define (tc/rec-lambda/check formals body name args return)
+;; Returns both the tc-results of the function and of the body
+(define (tc/rec-lambda/check formals* body name args return)
+  (define formals (syntax->list formals*))
   (with-lexical-env/extend
-   (syntax->list formals) args
+   formals args
    (let* ([r (tc-results->values return)]
           [t (make-arr args r)]
           [ft (make-Function (list t))])
      (with-lexical-env/extend
       (list name) (list ft)
-      (begin (tc-body/check body return) (ret ft))))))
+      (values
+        (erase-names/results formals (ret ft))
+        (erase-names/results formals (tc-body/check body return)))))))
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 6e2d5851..ccc1d990 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
@@ -8,7 +8,7 @@
               global-env type-env-structs scoped-tvar-env)
          (rep type-rep filter-rep)
          syntax/free-vars
-         (typecheck signatures tc-metafunctions tc-subst internal-forms)
+         (typecheck signatures tc-metafunctions internal-forms)
          (utils tarjan)
          racket/match (contract-req)
          syntax/parse syntax/stx
@@ -64,31 +64,19 @@
              clauses
              exprs
              expected-results)
-   (let ([subber (lambda (proc lst)
-                   (for/list ([i (in-list lst)])
-                     (for/fold ([s i])
-                       ([nm (in-list (apply append abstract namess))])
-                       (proc s nm -empty-obj #t))))])
-     (define (run res)
-       (match res
-         [(tc-any-results:) res]
-         [(tc-results: ts fs os)
-          (ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os))]
-         [(tc-results: ts fs os dt db)
-          (ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os) dt db)]))
-     (with-lexical-env/extend/props
-      ;; we typechecked the rhss with the lhss having types that potentially contain undefined
-      ;; if undefined can actually show up, a type error will have been triggered
-      ;; it is therefore safe to typecheck the body with the original types the user gave us
-      ;; any undefined-related problems have been caught already
-      namess
-      expected-types ; types w/o undefined
-      (append p1 p2)
-      ;; typecheck the body
-      (run
-        (if expected
-          (tc-body/check body (erase-filter expected))
-          (tc-body body)))))))
+   (with-lexical-env/extend/props
+    ;; we typechecked the rhss with the lhss having types that potentially contain undefined
+    ;; if undefined can actually show up, a type error will have been triggered
+    ;; it is therefore safe to typecheck the body with the original types the user gave us
+    ;; any undefined-related problems have been caught already
+    namess
+    expected-types ; types w/o undefined
+    (append p1 p2)
+    ;; typecheck the body
+    (erase-names/results (apply append abstract namess)
+      (if expected
+        (tc-body/check body (erase-filter expected))
+        (tc-body body))))))
 
 (define (tc-expr/maybe-expected/t e names)
   (syntax-parse names
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 9037f618..13cb9aa7 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
@@ -5,9 +5,11 @@
          (except-in (types abbrev union utils filter-ops)
                     -> ->* one-of/c)
          (rep type-rep filter-rep object-rep rep-utils)
+         (typecheck tc-subst)
          (contract-req))
 
 (provide abstract-results
+         erase-names/results
          combine-props
          tc-results->values)
 
@@ -100,20 +102,13 @@
            ;; the scope count in the keys so that names are
            ;; substituted with the correct level of nesting
            (λ (type)
-             (abstract-type ids (add-scope keys) type))])
+             (abstract-type ids (map add-scope keys) type))])
       (make-arr (map at dom)
                 (at* rng) ; only increase scope in range
                 (and rest (at rest))
                 (and drest (cons (at (car drest)) (cdr drest)))
                 (map at kws)))]))
 
-;; add-scope : Listof<name-ref/c> -> Listof<name-ref/c>
-;; Add a scope to the index object
-(define (add-scope keys)
-  (for/list ([depth+arg keys])
-    (match-define (list depth arg) depth+arg)
-    (list (+ 1 depth) arg)))
-
 ;; Abstract all given id objects into index objects (keys) in
 ;; the given object
 (define/cond-contract (abstract-object ids keys o)
@@ -246,3 +241,19 @@
             [(Bot:) (set-box! flag #f) (values derived-props derived-atoms)]
             [_ (loop (cons p derived-props) derived-atoms (cdr worklist))])))))
 
+;; erase-names/results: (listof identifier?) tc-results? -> tc-results?
+;; Maps all of the given names in the results to the empty object.
+;; This is used so that names do not escape the scope of their definitions
+;; TODO support mapping names to other objects.
+(define (erase-names/results names res)
+  (define (subber proc lst)
+    (for/list ([i (in-list lst)])
+      (for/fold ([s i])
+        ([nm (in-list names)])
+        (proc s nm -empty-obj #t))))
+  (match res
+    [(tc-any-results:) res]
+    [(tc-results: ts fs os)
+     (ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os))]
+    [(tc-results: ts fs os dt db)
+     (ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os) dt db)]))
diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
index 4c017f08..7c28d1f6 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
@@ -933,7 +933,7 @@
            (do: : Number ((x : (Listof Number) x (cdr x))
                           (sum : Number 0 (+ sum (car x))))
                 ((null? x) sum)))
-         #:ret (ret -Number -top-filter -no-obj)]
+         #:ret (ret -Number -top-filter -empty-obj)]
 
         [tc-e/t (if #f 1 'foo) (-val 'foo)]
 
@@ -1179,7 +1179,7 @@
                      ([j : Natural (+ i 'a) (+ j i)])
                      ((>= j 10))
                      #f)
-          #:ret (ret -Void -no-filter -no-obj)]
+          #:ret (ret -Void -top-filter -empty-obj)]
         [tc-err (apply +)]
         [tc-e/t
          (let ([x eof])
@@ -1748,7 +1748,7 @@
         [tc-e (let ([my-pred (λ () #f)])
                 (for/and: : Any ([i (in-range 4)])
                           (my-pred)))
-              #:ret (ret Univ -top-filter -no-obj)]
+              #:ret (ret Univ -top-filter -empty-obj)]
         [tc-e
          (let ()
            (define: long : (List 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 Integer)
@@ -1864,7 +1864,7 @@
           (ann
             ((letrec ((x (lambda (acc #{ v : Symbol}) (if v (list v) acc)))) x) null (list 'bad 'prog))
             (Listof Symbol))
-          #:ret (ret (-lst -Symbol) -no-filter -no-obj)]
+          #:ret (ret (-lst -Symbol) -top-filter -empty-obj)]
         [tc-e (filter values empty)
               (-lst -Bottom)]
         [tc-e (lambda lst (map (plambda: (b) ([x : b]) x) lst))
@@ -2150,7 +2150,7 @@
                (values x y))
              #:ret (ret (-HT -Symbol -String)
                         (-FS -top -top)
-                        -no-obj)]
+                        -empty-obj)]
        [tc-e (for*/hash: : (HashTable Symbol String)
                ([k (in-list '(x y z))]
                 [v (in-list '("a" "b"))]
@@ -2158,7 +2158,7 @@
                (values k v))
              #:ret (ret (-HT -Symbol -String)
                         (-FS -top -top)
-                        -no-obj)]
+                        -empty-obj)]
 
        ;; PR 13937
        [tc-e (let ()
@@ -2399,9 +2399,9 @@
        [tc-e (let/ec k : String (k "foo")) -String]
        [tc-e (ann (do ([x : Integer 0 (add1 x)]) ((> x 10) x) (displayln x))
                   Integer)
-             #:ret (ret -Integer -no-filter -no-obj)]
+             #:ret (ret -Integer -top-filter -empty-obj)]
        [tc-e (do : Integer ([x : Integer 0 (add1 x)]) ((> x 10) x) (displayln x))
-             #:ret (ret -Integer -no-filter -no-obj)]
+             #:ret (ret -Integer -top-filter -empty-obj)]
        [tc-e (tr:case-lambda [(x [y : String]) x])
              #:ret (ret (t:-> Univ -String Univ
                               : (-FS (-not-filter (-val #f) (list 0 0))