diff --git a/collects/tests/typed-racket/fail/pr13581.rkt b/collects/tests/typed-racket/fail/pr13581.rkt
new file mode 100644
index 00000000..42844435
--- /dev/null
+++ b/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))
diff --git a/collects/tests/typed-racket/fail/values-dots.rkt b/collects/tests/typed-racket/fail/values-dots.rkt
index 9ef8a78a..bbf8c2b5 100644
--- a/collects/tests/typed-racket/fail/values-dots.rkt
+++ b/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))
diff --git a/collects/tests/typed-racket/succeed/nested-poly.rkt b/collects/tests/typed-racket/succeed/nested-poly.rkt
index 27620d07..5e51e835 100644
--- a/collects/tests/typed-racket/succeed/nested-poly.rkt
+++ b/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))))
 
diff --git a/collects/tests/typed-racket/succeed/values-dots.rkt b/collects/tests/typed-racket/succeed/values-dots.rkt
index efe5f3d1..5d10bb6e 100644
--- a/collects/tests/typed-racket/succeed/values-dots.rkt
+++ b/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 + - * /)
diff --git a/collects/typed-racket/typecheck/check-below.rkt b/collects/typed-racket/typecheck/check-below.rkt
index dbaf9cdf..8cae5261 100644
--- a/collects/typed-racket/typecheck/check-below.rkt
+++ b/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)]))
diff --git a/collects/typed-racket/typecheck/tc-app/tc-app-list.rkt b/collects/typed-racket/typecheck/tc-app/tc-app-list.rkt
index 5408ffbb..7c6fbcb3 100644
--- a/collects/typed-racket/typecheck/tc-app/tc-app-list.rkt
+++ 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 ...) (tc-expr #'f) (cons (ret t0) (map ret t)) expected))
+                (tc/funapp #'f #'(arg0 arg ...) f-type (cons (ret t0) (map ret t)) expected))
          [(tc-result1: t) (ret (make-ListDots t bound0))]
          [(tc-results: ts)
           (tc-error/expr #:return (ret (Un))