remove type anns for parameters in λs generated from kw/opt plambdas

an optional or keyword lambda is expanded to more than two lambdas where
syntax objects for the original paramaters are reused. This is problematic when
those parameters are typed with bound type variables in polymorphic functions,
because in generated lambdas those variables would become unbound.

This patch fixes the problem by throwing the types away before typechecking
the generated lambdas.

closes #940

Author: capfredf

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

@@ -684,7 +684,22 @@ the typed racket language.
        (if (attribute return.type)
            #`(ann last-e #,(attribute return.type))
            #'last-e))
-     (define d (syntax/loc stx (λ formals.erased e ... last-e*)))
+
+     ;; if the lambda form being checked is a polymorphic function, tag its
+     ;; parameters with property `from-lambda'. 
+     (define (maybe-set-from-lambda type-vars formals)
+       (cond
+         [(and type-vars (stx-list? formals))
+          (stx-map (lambda (x)
+                     (from-plambda-property x #t))
+                   formals)]
+         [type-vars (from-plambda-property formals #t)]
+         [else formals]))
+
+     (define d (with-syntax ([erase-formals (maybe-set-from-lambda
+                                             (attribute vars.type-vars)
+                                             (attribute formals.erased))])
+                 (syntax/loc stx (λ erase-formals e ... last-e*))))
      (define d/prop
        (if (attribute formals.kw-property)
            (kw-lambda-property d (attribute formals.kw-property))

typed-racket-lib/typed-racket/private/syntax-properties.rkt

@@ -69,6 +69,8 @@
   (struct-info struct-info)
   (opt-lambda opt-lambda)
   (kw-lambda kw-lambda)
+  ; mark syntax objects for formal parameters in polymorphic lambdas forms.
+  (from-plambda from-plambda)
   (tail-position typechecker:called-in-tail-position #:mark)
   (tr:class tr:class #:mark)
   (tr:class:top-level tr:class:top-level)

typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt

@@ -43,14 +43,28 @@
 ;; (i.e. (append positional (or id '())) but syntax)
 (struct formals (positional rest syntax) #:transparent)
 
-(define (make-formals stx)
+
+;; When expanding a keyword or optional lambda, Racket adds into the expanded
+;; code more lambdas, where syntax objects for the original lambda's parameters
+;; are reused. Since Typed Racket stores type information stored in the syntax
+;; objects, when the orginal lambda is a polymorphic function, that information
+;; might carry out-of-scope type variables. In this case, we need to remove it
+;; from parameter syntax objects.
+;;
+;; not-in-poly is #t if the original TR function is polymorphic. 
+(define (make-formals stx [not-in-poly #t])
+  (define (maybe-remove a)
+    (if (and not-in-poly (from-plambda-property a))
+        (syntax-property-remove a 'type-label)
+        a))
+
   (let loop ([s stx] [acc null])
     (cond
-      [(pair? s) (loop (cdr s) (cons (car s) acc))]
+      [(pair? s) (loop (cdr s) (cons (maybe-remove (car s)) acc))]
       [(null? s) (formals (reverse acc) #f stx)]
-      [(pair? (syntax-e s)) (loop (stx-cdr s) (cons (stx-car s) acc))]
+      [(pair? (syntax-e s)) (loop (stx-cdr s) (cons (maybe-remove (stx-car s)) acc))]
       [(null? (syntax-e s)) (formals (reverse acc) #f stx)]
-      [else (formals (reverse acc) s stx)])))
+      [else (formals (reverse acc) (maybe-remove s) stx)])))
 
 ;; Currently no support for objects representing the rest argument
 (define (formals->objects f)
@@ -621,15 +635,15 @@
        (tc-error/expr #:return dep-fun-ty
                       "Dependent functions must have a single arity.")])))
 
-(define (tc/mono-lambda/type formalss bodies expected)
+(define (tc/mono-lambda/type formalss bodies expected [not-in-poly #t])
   (match expected
     [(tc-result1:(? DepFun? dep-fun-ty))
      (tc/dep-lambda formalss bodies dep-fun-ty)]
     [_ (make-Fun
         (tc/mono-lambda
          (for/list ([f (in-syntax formalss)]
                     [b (in-syntax bodies)])
-           (cons (make-formals f) b))
+           (cons (make-formals f not-in-poly) b))
          expected))]))
 
 (define (plambda-prop stx)
@@ -678,7 +692,7 @@
       [_
         (define remaining-layers (remove-poly-layer tvarss-list))
         (if (null? remaining-layers)
-            (tc/mono-lambda/type formals bodies expected)
+            (tc/mono-lambda/type formals bodies expected #f)
             (tc/plambda form remaining-layers formals bodies expected))]))
   ;; check the bodies appropriately
   ;; and make both annotated and declared type variables point to the

typed-racket-test/succeed/gh-issue-940.rkt

@@ -0,0 +1,7 @@
+#lang typed/racket
+(lambda #:forall (A) ([a : A] #:mand mand) 10)
+
+(lambda #:forall (A) ([a : A] #:mand [mand : (Listof A)]) 10)
+
+(define #:forall (A) (bar [a : (Listof A)] #:mand [mand : Integer]) : Integer
+  0)