Support polymorphism in both TR let and lambda

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/annotate-classes.rkt

@@ -147,3 +147,15 @@
 (define-splicing-syntax-class optional-standalone-annotation
   (pattern (~optional a:standalone-annotation)
            #:with ty (if (attribute a) #'a.ty #f)))
+
+(define-splicing-syntax-class lambda-type-vars
+  #:description "optional type parameters"
+  #:attributes (type-vars)
+  (pattern (~seq (~or #:forall #:∀) (var:id ...))
+           #:attr type-vars #'(var ...)))
+
+(define-splicing-syntax-class maybe-lambda-type-vars
+  #:description "optional type parameters"
+  #:attributes (type-vars)
+  (pattern :lambda-type-vars)
+  (pattern (~seq) #:attr type-vars #f))

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt

@@ -496,6 +496,15 @@ This file defines two sorts of primitives. All of them are provided into any mod
                                 (lambda (bs.ann-name ...) . #,(syntax/loc stx body)))])
                  #,(quasisyntax/loc stx nm)))])
         bs.rhs ...))]
+    [(-let ([bn:optionally-annotated-name e] ...)
+           vars:lambda-type-vars . rest)
+     (define/with-syntax (bn* ...)
+       ;; singleton names go to just the name
+       (for/list ([bn (in-syntax #'(bn ...))])
+         (if (empty? (stx-cdr bn))
+             (stx-car bn)
+             bn)))
+     (template ((-lambda (bn* ...) (?@ . vars) . rest) e ...))]
     [(-let . rest)
      (syntax/loc stx (-let-internal . rest))]))
 
@@ -1229,7 +1238,9 @@ This file defines two sorts of primitives. All of them are provided into any mod
 (define-syntax (-lambda stx)
   (syntax-parse stx
     #:literals (:)
-    [(_ formals:lambda-formals return:return-ann
+    [(_ formals:lambda-formals
+        vars:maybe-lambda-type-vars
+        return:return-ann
         (~describe "body expression or definition" e) ...
         (~describe "body expression" last-e))
      ;; Annotate the last expression with the return type. Should be correct
@@ -1240,9 +1251,16 @@ This file defines two sorts of primitives. All of them are provided into any mod
            #`(ann last-e #,(attribute return.type))
            #'last-e))
      (define d (syntax/loc stx (λ formals.erased e ... last-e*)))
+     (define d/prop
        (if (attribute formals.kw-property)
            (kw-lambda-property d (attribute formals.kw-property))
-         (opt-lambda-property d (attribute formals.opt-property)))]))
+           (opt-lambda-property d (attribute formals.opt-property))))
+     ;; attach a plambda property if necessary
+     (if (attribute vars.type-vars)
+         (quasisyntax/loc stx
+           (#%expression
+            #,(plambda-property d/prop (attribute vars.type-vars))))
+         d/prop)]))
 
 
 ;; do this ourselves so that we don't get the static bindings,

pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt

@@ -2137,6 +2137,17 @@
              (->key Univ #:y -String #t #:z -String #f -String)]
        [tc-e (tr:lambda (x #:y [y : String "y"] #:z [z : String "z"]) (string-append y z))
              (->key Univ #:y -String #f #:z -String #f -String)]
+       ;; for these next two tests, test the application instead of the
+       ;; type of the function because the precise filters are hard to
+       ;; get right in the expected result type.
+       [tc-e ((inst (tr:lambda (x [y : A]) #:forall (A) y) String) 'a "foo")
+             #:ret (ret -String (-FS -top -bot))]
+       [tc-e ((inst (tr:lambda (x [y : A]) #:∀ (A) y) String) 'a "foo")
+             #:ret (ret -String (-FS -top -bot))]
+       #| FIXME: does not work yet, TR thinks the type variable is unbound
+       [tc-e (inst (tr:lambda (x [y : A] [z : String "z"]) #:forall (A) y) String)
+             #:ret (ret (->opt Univ -String [-String] -String) (-FS -top -bot))]
+       |#
 
        ;; test new :-less forms that allow fewer annotations
        [tc-e (let ([x "foo"]) x) -String]
@@ -2148,6 +2159,10 @@
              -String]
        [tc-e (let ([y 'y] [x : String "foo"]) (string-append x "bar"))
              -String]
+       [tc-e (let ([x : A "foo"]) #:forall (A) x)
+             #:ret (ret -String (-FS -top -bot))]
+       [tc-e (let ([y 'y] [x : A "foo"]) #:forall (A) x)
+             #:ret (ret -String (-FS -top -bot))]
        [tc-e (let* ([x "foo"]) x) -String]
        [tc-e (let* ([x : String "foo"]) (string-append x "bar"))
              -String]