Make let correctly implement the TC-Let rule from the paper.

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))
+        (replace-names (map (λ (f) (list f -empty-obj)) formals) (ret ft))
-        (erase-names/results formals (tc-body/check body return)))))))
+        (replace-names (map (λ (f) (list f -empty-obj)) formals) (tc-body/check body return)))))))

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])
+;; get-names+objects (listof (listof identifier?)) (listof tc-results?) -> (listof (list/c identifier Object?))
-     (((syntax? tc-results/c . -> . any/c)
+;; 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?) (listof syntax?) (or/c #f tc-results/c))
+      (listof syntax?) syntax? (or/c #f tc-results/c)
-      (#:abstract any/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,14 +144,17 @@
         (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
+    (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)
-         (do-check void null null null null body expected #:abstract orig-flat-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
@@ -167,7 +184,7 @@
                            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)]))))
+                     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 (tc-results-ts results)
-           (with-lexical-env/extend names types
              (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

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?
+;; replace-names: (listof (list/c identifier? Object?) tc-results? -> tc-results?
-;; Maps all of the given names in the results to the empty object.
+;; 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 (replace-names names+objects res)
-(define (erase-names/results names res)
   (define (subber proc lst)
     (for/list ([i (in-list lst)])
-      (for/fold ([s i])
+      (for/fold ([s i]) ([name/object (in-list names+objects)])
-        ([nm (in-list names)])
+        (proc s (first name/object) (second name/object) #t))))
-        (proc s nm -empty-obj #t))))
   (match res
     [(tc-any-results:) res]
     [(tc-results: ts fs os)

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")])]

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?])

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"