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 5ef586df..bc920ac5 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
@@ -531,5 +531,5 @@
      (with-lexical-env/extend
       (list name) (list ft)
       (values
-        (erase-names/results formals (ret ft))
-        (erase-names/results formals (tc-body/check body return)))))))
+        (replace-names (map (λ (f) (list f -empty-obj)) formals) (ret ft))
+        (replace-names (map (λ (f) (list f -empty-obj)) 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 40490a83..90880105 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
@@ -11,6 +11,7 @@
          (typecheck signatures tc-metafunctions internal-forms)
          (utils tarjan)
          racket/match (contract-req)
+         racket/list
          syntax/parse syntax/stx
          syntax/id-table
          ;; For internal type forms
@@ -20,12 +21,25 @@
 (import tc-expr^)
 (export tc-let^)
 
-(define/cond-contract (do-check expr->type namess results expected-results exprs body expected #:abstract [abstract null])
-     (((syntax? tc-results/c . -> . any/c)
-       (listof (listof identifier?)) (listof tc-results/c) (listof tc-results/c)
-       (listof syntax?) (listof syntax?) (or/c #f tc-results/c))
-      (#:abstract any/c)
-      . ->* .
+;; get-names+objects (listof (listof identifier?)) (listof tc-results?) -> (listof (list/c identifier Object?))
+;; Given a list of bindings and the tc-results for the corresponding expressions, return a list of
+;; tuples of the binding-name and corresponding objects from the results.
+;; This is used to replace the names with the objects after the names go out of scope.
+(define (get-names+objects namess results)
+  (append*
+    (for/list ([names namess] [results results])
+      (match results
+        [(tc-results: _ _ os)
+         (map list names os)]))))
+
+;; Checks that the body has the expected type when names are bound to the types spcified by results.
+;; The exprs are also typechecked by using expr->type.
+;; TODO: make this function sane.
+(define/cond-contract (do-check expr->type namess results expected-results exprs body expected)
+     ((syntax? tc-results/c . -> . any/c)
+      (listof (listof identifier?)) (listof tc-results/c) (listof tc-results/c)
+      (listof syntax?) syntax? (or/c #f tc-results/c)
+      . -> .
       tc-results/c)
      (with-cond-contract t/p ([types          (listof (listof Type/c))] ; types that may contain undefined (letrec)
                               [expected-types (listof (listof Type/c))] ; types that may not contain undefined (what we got from the user)
@@ -74,7 +88,7 @@
     expected-types ; types w/o undefined
     (append p1 p2)
     ;; typecheck the body
-    (erase-names/results (apply append abstract namess)
+    (replace-names (get-names+objects namess expected-results)
       (if expected
         (tc-body/check body (erase-filter expected))
         (tc-body body))))))
@@ -130,44 +144,47 @@
         (values name expr)))
 
     ;; Check those and gather an environment for use below
-    (define-values (env-names env-types)
+    (define-values (env-names env-results)
       (check-non-recursive-clauses ordered-clauses))
 
-    (with-lexical-env/extend env-names env-types
-      (cond
-        ;; after everything, check the body expressions
-        [(null? remaining-names)
-         (do-check void null null null null body expected #:abstract orig-flat-names)]
-        [else
-         (define flat-names (apply append remaining-names))
-         (do-check tc-expr/check
-                   remaining-names
-                   ;; compute set of variables that can't be undefined. see below.
-                   (let-values
-                    ([(safe-bindings _)
-                      (for/fold ([safe-bindings              '()] ; includes transitively-safe
-                                 [transitively-safe-bindings '()])
-                          ([names  (in-list remaining-names)]
-                           [expr (in-list remaining-exprs)])
-                        (case (safe-letrec-values-clause? expr transitively-safe-bindings flat-names)
-                          ;; transitively safe -> safe to mention in a subsequent rhs
-                          [(transitively-safe) (values (append names safe-bindings)
-                                                       (append names transitively-safe-bindings))]
-                          ;; safe -> safe by itself, but may not be safe to use in a subsequent rhs
-                          [(safe)              (values (append names safe-bindings)
-                                                       transitively-safe-bindings)]
-                          ;; unsafe -> could be undefined
-                          [(unsafe)            (values safe-bindings transitively-safe-bindings)]))])
-                    (map (λ (l) (let ([types-from-user (map get-type l)])
-                                  (ret (if (andmap (λ (x) ; are all the lhs vars safe?
-                                                      (member x safe-bindings bound-identifier=?))
-                                                   l)
-                                           types-from-user
-                                           (map (λ (x) (Un x -Undefined)) types-from-user)))))
-                         remaining-names))
-                   ;; types the user gave. check against that to error if we could get undefined
-                   (map (λ (l) (ret (map get-type l))) remaining-names)
-                   remaining-exprs body expected)]))))
+    (replace-names (get-names+objects env-names env-results)
+      (with-lexical-env/extend env-names (map tc-results-ts env-results)
+        (cond
+          ;; after everything, check the body expressions
+          [(null? remaining-names)
+             (if expected
+               (tc-body/check body (erase-filter expected))
+               (tc-body body))]
+          [else
+           (define flat-names (apply append remaining-names))
+           (do-check tc-expr/check
+                     remaining-names
+                     ;; compute set of variables that can't be undefined. see below.
+                     (let-values
+                      ([(safe-bindings _)
+                        (for/fold ([safe-bindings              '()] ; includes transitively-safe
+                                   [transitively-safe-bindings '()])
+                            ([names  (in-list remaining-names)]
+                             [expr (in-list remaining-exprs)])
+                          (case (safe-letrec-values-clause? expr transitively-safe-bindings flat-names)
+                            ;; transitively safe -> safe to mention in a subsequent rhs
+                            [(transitively-safe) (values (append names safe-bindings)
+                                                         (append names transitively-safe-bindings))]
+                            ;; safe -> safe by itself, but may not be safe to use in a subsequent rhs
+                            [(safe)              (values (append names safe-bindings)
+                                                         transitively-safe-bindings)]
+                            ;; unsafe -> could be undefined
+                            [(unsafe)            (values safe-bindings transitively-safe-bindings)]))])
+                      (map (λ (l) (let ([types-from-user (map get-type l)])
+                                    (ret (if (andmap (λ (x) ; are all the lhs vars safe?
+                                                        (member x safe-bindings bound-identifier=?))
+                                                     l)
+                                             types-from-user
+                                             (map (λ (x) (Un x -Undefined)) types-from-user)))))
+                           remaining-names))
+                     ;; types the user gave. check against that to error if we could get undefined
+                     (map (λ (l) (ret (map get-type l))) remaining-names)
+                     remaining-exprs body expected)])))))
 
 ;; An lr-clause is a
 ;;   (lr-clause (Listof Identifier) Syntax)
@@ -233,7 +250,7 @@
           remaining))
 
 ;; check-non-recursive-clauses : (Listof lr-clause) ->
-;;                               (Listof Identifier) (Listof Type)
+;;                               (Listof (Listof Identifier)) (Listof tc-results)
 ;; Given a list of non-recursive clauses, check the clauses in order and
 ;; build up a type environment for use in the second pass.
 (define (check-non-recursive-clauses clauses)
@@ -245,11 +262,10 @@
              (get-type/infer names expr
                              (lambda (e) (tc-expr/maybe-expected/t e names))
                              tc-expr/check))
-           (match-define (tc-results: types) results)
-           (with-lexical-env/extend names types
+           (with-lexical-env/extend names (tc-results-ts results)
              (loop (cdr clauses)
                    (cons names env-ids)
-                   (cons types env-types)))])))
+                   (cons results env-types)))])))
 
 ;; determines whether any of the variables bound in the given clause can have an undefined value
 ;; in this case, we cannot trust the type the user gave us and must union it with undefined
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 ee83207a..c66a9728 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
@@ -9,10 +9,13 @@
          (contract-req))
 
 (provide abstract-results
-         erase-names/results
          combine-props
          tc-results->values)
 
+(provide/cond-contract
+  [replace-names (-> (listof (list/c identifier? Object?)) tc-results/c tc-results/c)])
+
+
 ;; abstract-results
 ;;
 ;; Given results from the range of a lambda, abstract any
@@ -236,16 +239,14 @@
             [(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.
+;; replace-names: (listof (list/c identifier? Object?) tc-results? -> tc-results?
+;; For each name replaces all uses of it in res with the corresponding 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 (replace-names names+objects 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))))
+      (for/fold ([s i]) ([name/object (in-list names+objects)])
+        (proc s (first name/object) (second name/object) #t))))
   (match res
     [(tc-any-results:) res]
     [(tc-results: ts fs os)
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/kw-types.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/kw-types.rkt
index cb045f35..3c03b316 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/kw-types.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/kw-types.rkt
@@ -2,6 +2,7 @@
 
 (require "abbrev.rkt" "../rep/type-rep.rkt"
          "../utils/tc-utils.rkt"
+         "tc-result.rkt"
          racket/list racket/set racket/dict racket/match
          syntax/parse)
 
@@ -68,6 +69,20 @@
                 (make-arr* ts/false rng #:drest drest)))
         (list (make-arr* ts rng #:rest rest #:drest drest)))))
 
+
+;; This is used to fix the filters of keyword types.
+;; TODO: This should also explore deeper into the actual types and remove filters in there as well.
+;; TODO: This should not remove the filters but instead make them refer to the actual arguments after
+;; keyword conversion.
+(define (erase-filter/Values values)
+  (match values
+    [(AnyValues:) values]
+    [(Results: ts fs os)
+     (-values ts)]
+    [(Results: ts fs os dty dbound)
+     (-values-dots ts dty dbound)]))
+
+
 (define (prefix-of a b)
   (define (rest-equal? a b)
     (match* (a b)
@@ -176,7 +191,7 @@
               (and rest? (last other-args)))
             (make-Function
              (list (make-arr* (take other-args non-kw-argc)
-                              rng
+                              (erase-filter/Values rng)
                               #:kws actual-kws
                               #:rest rest-type)))]
            [(and (even? (length arrs)) ; had optional args
@@ -198,7 +213,7 @@
             (make-Function
              (for/list ([to-take (in-range (add1 (length opt-types)))])
                (make-arr* (append mand-args (take opt-types to-take))
-                          rng
+                          (erase-filter/Values rng)
                           #:kws actual-kws
                           #:rest rest-type)))]
            [else (int-err "unsupported arrs in keyword function type")])]
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/tc-result.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/tc-result.rkt
index 68afc433..1fa38103 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/tc-result.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/tc-result.rkt
@@ -51,7 +51,7 @@
    [(_ tp) (struct tc-results ((list (struct tc-result (tp _ _)))
                                  #f))]))
 
-(define (tc-results-t tc)
+(define (tc-results-ts* tc)
   (match tc
     [(tc-results: t) t]))
 
@@ -63,7 +63,8 @@
 (define-match-expander Results:
   (syntax-rules ()
    [(_ tp) (Values: (list (Result: tp _ _) (... ...)))]
-   [(_ tp fp op) (Values: (list (Result: tp fp op) (... ...)))]))
+   [(_ tp fp op) (Values: (list (Result: tp fp op) (... ...)))]
+   [(_ tp fp op dty dbound) (ValuesDots: (list (Result: tp fp op) (... ...)) dty dbound)]))
 
 ;; convenience function for returning the result of typechecking an expression
 (define ret
@@ -125,6 +126,7 @@
 (provide/cond-contract
  [combine-results ((c:listof tc-results?) . c:-> . tc-results?)]
  [tc-result-t (tc-result? . c:-> . Type/c)]
+ [rename tc-results-ts* tc-results-ts (tc-results? . c:-> . (c:listof Type/c))]
  [tc-result-equal? (tc-result? tc-result? . c:-> . boolean?)]
  [tc-results? (c:any/c . c:-> . boolean?)]
  [tc-results/c c:flat-contract?])
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 ecadbbd1..d25ec2ff 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
@@ -1205,12 +1205,12 @@
                      #f)
           #:ret (ret -Void -top-filter -empty-obj)]
         [tc-err (apply +)]
-        [tc-e/t
+        [tc-e
          (let ([x eof])
            (if (procedure? x)
                x
                (lambda (z) (eq? x z))))
-         (make-pred-ty (-val eof))]
+         #:ret (ret (make-pred-ty (-val eof)) (-FS (-not-filter top-func #'eof) -bot))]
         [tc-e ((inst map Number (Pairof Number Number)) car (ann (list (cons 1 2) (cons 2 3) (cons 4 5)) (Listof (Pairof Number Number))))
               (-lst -Number)]
         [tc-err (list (values 1 2))
@@ -2651,6 +2651,22 @@
                0))
          #:ret (ret -Bottom)]
 
+       [tc-e
+         (let: ([x : Any 4])
+           (if (let: ([y x]) (number? y))
+               (add1 x)
+               4))
+         -Number]
+
+       [tc-e
+         (let ()
+           (: g (-> Boolean))
+           (define (g) (g))
+           (: x Any)
+           (define x 0)
+           (number? x))
+         -Boolean]
+
         )
   (test-suite
    "tc-literal tests"