Don't let map introduce type variables.

Closes PR 13581.

collects/math/private/array/typed-array-pointwise.rkt

@@ -25,11 +25,11 @@
                                               (map array-shape arrs))))
      (let ([arr0  (array-broadcast arr0 ds)]
            [arr1  (array-broadcast arr1 ds)]
-           [arrs  (map (λ: ([arr : (Array T)]) (array-broadcast arr ds)) arrs)])
+           [arrs  (map (plambda: (S) ([arr : (Array S)]) (array-broadcast arr ds)) arrs)])
        (define g0 (unsafe-array-proc arr0))
        (define g1 (unsafe-array-proc arr1))
        (define gs (map unsafe-array-proc arrs))
        (array-default-strict
         (unsafe-build-array
          ds (λ: ([js : Indexes]) (apply f (g0 js) (g1 js)
-                                        (map (λ: ([g : (Indexes -> T)]) (g js)) gs))))))]))
+                                        (map (plambda: (S) ([g : (Indexes -> S)]) (g js)) gs))))))]))

collects/math/private/matrix/typed-matrix-arithmetic.rkt

@@ -35,7 +35,7 @@
       (unsafe-build-array
        ((inst vector Index) m n)
        (λ: ([js : Indexes]) (apply f (g0 js) (g1 js)
-                                   (map (λ: ([g : (Indexes -> T)]) (g js)) gs)))))]))
+                                   (map (plambda: (S) ([g : (Indexes -> S)]) (g js)) gs)))))]))
 
 (: matrix=? ((Matrix Number) (Matrix Number) -> Boolean))
 (define (matrix=? arr0 arr1)

collects/tests/typed-racket/fail/pr13581.rkt

@@ -0,0 +1,14 @@
+#lang typed/racket
+(: g (All (a ...) (a ... a -> (List a ... a))))
+(define (g . rst)
+  (map
+   ;; 'a' is in scope due to map rule
+   (lambda: ([y : a]) 
+     (map
+      ;; in scope again
+      (lambda: ([z : a])
+        (set! y z)
+        z)
+      rst)
+     y)
+   rst))

collects/tests/typed-racket/fail/values-dots.rkt

@@ -7,7 +7,7 @@
 (: map-with-funcs (All (b ...) ((b ... b -> b) ... b -> (b ... b -> (values b ... b)))))
 (define (map-with-funcs . fs)
   (lambda bs
-    (apply values (map (lambda: ([f : (b ... b -> b)])
+    (apply values (map (plambda: (c) ([f : (b ... b -> c)])
                          (apply f bs)) fs))))
 
 (map-with-funcs (lambda () 1))

collects/tests/typed-racket/succeed/nested-poly.rkt

@@ -13,7 +13,7 @@
               (B ... B -> (values A ... A))))))
 (define (map-with-funcs . fs)
   (lambda as
-    (apply values (map (lambda: ([f : (B ... B -> A)])
+    (apply values (map (plambda: (C) ([f : (B ... B -> C)])
                                  (apply f as))
                         fs))))
 

collects/tests/typed-racket/succeed/values-dots.rkt

@@ -13,7 +13,7 @@
 (: map-with-funcs (All (b ...) ((b ... b -> b) ... b -> (b ... b -> (values b ... b)))))
 (define (map-with-funcs . fs)
   (lambda bs
-    (apply values (map (lambda: ([f : (b ... b -> b)])
+    (apply values (map (plambda: (c) ([f : (b ... b -> c)])
                          (apply f bs)) fs))))
 
 (map-with-funcs + - * /)

collects/typed-racket/typecheck/check-below.rkt

@@ -95,9 +95,13 @@
      (unless (for/and ([t t1] [s t2]) (subtype t s))
        (tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
      expected]
-    [((tc-results: t1 f o dty dbound) (tc-results: t2 f o dty dbound))
+    [((tc-results: t1 f o dty1 dbound) (tc-results: t2 f o dty2 dbound))
+     (unless (= (length t1) (length t2))
+       (tc-error/expr "Expected ~a non dotted values, but got ~a" (length t2) (length t1)))
      (unless (andmap subtype t1 t2)
        (tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
+     (unless (subtype dty1 dty2)
+       (tc-error/expr "Expected ~a in ..., but got ~a" dty2 dty1))
      expected]
     [((tc-results: t1 fs os) (tc-results: t2 fs os))
      (unless (= (length t1) (length t2))
@@ -136,5 +140,5 @@
        (tc-error/expr "Expected ~a, but got ~a" t2 t1))
      expected]
     [((tc-results: ts fs os dty dbound) (tc-results: ts* fs* os* dty* dbound*))
-     (int-err "dotted types in check-below nyi: ~a ~a" dty dty*)]
+     (int-err "dotted types with different bounds/filters/objects in check-below nyi: ~a ~a" tr1 expected)]
     [(a b) (int-err "unexpected input for check-below: ~a ~a" a b)]))

collects/typed-racket/typecheck/tc-app/tc-app-list.rkt

@@ -42,9 +42,12 @@
               ...))
        (=> fail)
        (unless (for/and ([b bound]) (or (not b) (eq? bound0 b))) (fail))
+       ;; Do not check this in an environment where bound0 is a type variable.
+       (define f-type (tc-expr #'f))
+       ;; Check that the function applies successfully to the element type
+       ;; We need the bound to be considered a type var here so that inference works
        (match (extend-tvars (list bound0)
-                ;; just check that the function applies successfully to the element type
+                (tc/funapp #'f #'(arg0 arg ...) f-type (cons (ret t0) (map ret t)) expected))
-                (tc/funapp #'f #'(arg0 arg ...) (tc-expr #'f) (cons (ret t0) (map ret t)) expected))
          [(tc-result1: t) (ret (make-ListDots t bound0))]
          [(tc-results: ts)
           (tc-error/expr #:return (ret (Un))