diff --git a/collects/tests/typed-scheme/succeed/for.rkt b/collects/tests/typed-scheme/succeed/for.rkt
index cdd22c1c0a..5569e2681d 100644
--- a/collects/tests/typed-scheme/succeed/for.rkt
+++ b/collects/tests/typed-scheme/succeed/for.rkt
@@ -18,7 +18,7 @@
        (with-output-to-string
          (lambda ()
            (for: : Void
-                 ((i : Exact-Positive-Integer '(1 2 3))
+                 ((i : Integer '(1 2 3))
                   (j : Char "abc")
                   #:when (odd? i)
                   (k : True #(#t #t))
@@ -32,22 +32,22 @@
 
 (check equal?
        (for/list: : (Listof Integer)
-                  ((i : Exact-Positive-Integer '(1 2 3))
-                   (j : Exact-Positive-Integer '(10 20 30))
+                  ((i : Integer '(1 2 3))
+                   (j : Integer '(10 20 30))
                    #:when (odd? i))
                   (+ i j 10))
        '(21 43))
 
 (check equal?
        (for/or: : Boolean
-                ((i : Exact-Positive-Integer '(1 2 3)))
+                ((i : Integer '(1 2 3)))
                 (>= i 3))
        #t)
 
 (check equal?
        (for/or: : Boolean
-                ((i : Exact-Positive-Integer '(1 2 3))
-                 (j : Exact-Positive-Integer '(2 1 3)))
+                ((i : Integer '(1 2 3))
+                 (j : Integer '(2 1 3)))
                 (>= i j))
        #t)
 
@@ -56,9 +56,9 @@
                       (for/lists: : (values (Listof Integer) (Listof Integer))
                                   ((x : (Listof Integer))
                                    (y : (Listof Integer)))
-                                  ((i : Exact-Positive-Integer '(1 2 3))
+                                  ((i : Integer '(1 2 3))
                                    #:when #t
-                                   (j : Exact-Positive-Integer '(10 20 30))
+                                   (j : Integer '(10 20 30))
                                    #:when (> j 12))
                                   (values i j))])
                     (append x y))
@@ -67,19 +67,19 @@
 (check =
        (for/fold: : Integer
                   ((acc : Integer 0))
-                  ((i : Exact-Positive-Integer '(1 2 3))
-                   (j : Exact-Positive-Integer '(10 20 30)))
+                  ((i : Integer '(1 2 3))
+                   (j : Integer '(10 20 30)))
                   (+ acc i j))
        66)
 
 (check =
        (for/fold: : Integer
                   ((acc : Integer 0))
-                  ((i : Exact-Positive-Integer '(1 2 3))
+                  ((i : Integer '(1 2 3))
                    #:when (even? i)
-                   (j : Exact-Positive-Integer '(10 20 30))
+                   (j : Integer '(10 20 30))
                    #:when #t
-                   (k : Exact-Positive-Integer '(100 200 300)))
+                   (k : Integer '(100 200 300)))
                   (+ acc i j k))
        1998)
 
@@ -87,8 +87,8 @@
        (with-output-to-string
          (lambda ()
            (for*: : Void
-                  ((i : Exact-Positive-Integer '(1 2 3))
-                   (j : Exact-Positive-Integer '(10 20 30)))
+                  ((i : Integer '(1 2 3))
+                   (j : Integer '(10 20 30)))
                   (display (list i j)))))
        "(1 10)(1 20)(1 30)(2 10)(2 20)(2 30)(3 10)(3 20)(3 30)")
 
@@ -97,8 +97,8 @@
                       (for*/lists: : (values (Listof Integer) (Listof Integer))
                                    ((x : (Listof Integer))
                                     (y : (Listof Integer)))
-                                   ((i : Exact-Positive-Integer '(1 2 3))
-                                    (j : Exact-Positive-Integer '(10 20 30))
+                                   ((i : Integer '(1 2 3))
+                                    (j : Integer '(10 20 30))
                                     #:when (> j 12))
                                    (values i j))])
                     (append x y))
@@ -107,9 +107,9 @@
 (check =
        (for*/fold: : Integer
                    ((acc : Integer 0))
-                   ((i : Exact-Positive-Integer '(1 2 3))
+                   ((i : Integer '(1 2 3))
                     #:when (even? i)
-                    (j : Exact-Positive-Integer '(10 20 30))
-                    (k : Exact-Positive-Integer '(100 200 300)))
+                    (j : Integer '(10 20 30))
+                    (k : Integer '(100 200 300)))
                    (+ acc i j k))
        1998)
diff --git a/collects/tests/typed-scheme/xfail/for-inference.rkt b/collects/tests/typed-scheme/xfail/for-inference.rkt
index faa0154bee..14a3a70d89 100644
--- a/collects/tests/typed-scheme/xfail/for-inference.rkt
+++ b/collects/tests/typed-scheme/xfail/for-inference.rkt
@@ -59,3 +59,23 @@
 (for/last: : (Option Integer)
            ((i : Exact-Positive-Integer '(1 2 3)))
            i)
+
+;; unlike the usual cases with #:when clauses, inference does something, but does it wrong
+(for/list: : (Listof Integer)
+           (#:when #t
+            (i : Exact-Positive-Integer '(1 2 3))
+            (j : Exact-Positive-Integer '(10 20 30)))
+           (+ i j 10))
+
+;; that same bug makes for/hash:, for/hasheq: and for/hasheqv: unusable
+;; this infers Nothing for the type of the elements of the HashTable
+;; since they don't work, these functions are not currently documented
+(for/hash: : (HashTable Integer Char)
+           ((i : Exact-Positive-Integer '(1 2 3))
+            (j : Char "abc"))
+           (values i j))
+
+;; same thing for for/and:
+(for/and: : Boolean
+          ((i : Exact-Positive-Integer '(1 2 3)))
+          (< i 3))
diff --git a/collects/tests/typed-scheme/xfail/for-type-precision.rkt b/collects/tests/typed-scheme/xfail/for-type-precision.rkt
deleted file mode 100644
index 187907699f..0000000000
--- a/collects/tests/typed-scheme/xfail/for-type-precision.rkt
+++ /dev/null
@@ -1,37 +0,0 @@
-#lang typed/scheme
-
-;; I would have to be annotated with its most precise type (Exact-Positive-Integer) for this to work
-(for: : Void ((i : Integer '(1 2 3)))
-      (display i))
-
-;; same here, would need type (U (List 'a 't) (List 'c 'g))
-(for: : Void
-      ([from-to : (List Symbol Symbol)
-                '([a t]
-                  [c g])])
-      #t)
-
-;; wants (U False True), which should be the same as Boolean, but apparently isn't
-(for: : Void
-      ((k : Boolean #(#t #f))
-       #:when k)
-      (display k))
-
-;; unlike the usual cases with #:when clauses (see for-inference.rkt), inference does something, but does it wrong
-(for/list: : (Listof Integer)
-           (#:when #t
-            (i : Exact-Positive-Integer '(1 2 3))
-            (j : Exact-Positive-Integer '(10 20 30)))
-           (+ i j 10))
-
-;; that same bug makes for/hash:, for/hasheq: and for/hasheqv: unusable
-;; this infers Nothing for the type of the elements of the HashTable
-;; since they don't work, these functions are not currently documented
-(for/hash: : (HashTable Integer Char)
-           ((i : Exact-Positive-Integer '(1 2 3))
-            (j : Char "abc"))
-           (values i j))
-;; same thing for for/and:
-(for/and: : Boolean
-          ((i : Exact-Positive-Integer '(1 2 3)))
-          (< i 3))
diff --git a/collects/typed-scheme/private/for-clauses.rkt b/collects/typed-scheme/private/for-clauses.rkt
index 83c7f36b0f..5401352277 100644
--- a/collects/typed-scheme/private/for-clauses.rkt
+++ b/collects/typed-scheme/private/for-clauses.rkt
@@ -2,18 +2,25 @@
 
 (require syntax/parse
          "annotate-classes.rkt"
-         (for-template racket/base))
+         (for-template racket/base
+                       "base-types-new.rkt"))
 
 (provide (all-defined-out))
 
 (define-splicing-syntax-class for-clause
     ;; single-valued seq-expr
     (pattern (var:annotated-name seq-expr:expr)
-             #:with (expand ...) (list #'(var.ann-name seq-expr)))
+             #:with (expand ...) (list #`(var.ann-name
+                                          #,(syntax-property #'seq-expr
+                                                             'type-ascription
+                                                             #'(Sequenceof var.ty)))))
     ;; multi-valued seq-expr
     ;; currently disabled because it triggers an internal error in the typechecker
     #;(pattern (((v:annotated-name) ...) seq-expr:expr)
-             #:with (expand ...) (list #'((v.ann-name ...) seq-expr)))
+             #:with (expand ...) (list #`((v.ann-name ...)
+                                          #,(syntax-property #'seq-expr
+                                                             'type-ascription
+                                                             #'(Sequenceof (values v.ty ...))))))
     ;; when clause
     (pattern (~seq #:when guard:expr)
              #:with (expand ...) (list #'#:when #'guard)))
@@ -22,11 +29,19 @@
 (define-splicing-syntax-class for*-clause
   ;; single-valued seq-expr
     (pattern (var:annotated-name seq-expr:expr)
-             #:with (expand ...) (list #'(var.ann-name seq-expr) #'#:when #'#t))
+             #:with (expand ...) (list #`(var.ann-name
+                                          #,(syntax-property #'seq-expr
+                                                             'type-ascription
+                                                             #'(Sequenceof var.ty)))
+                                       #'#:when #'#t))
     ;; multi-valued seq-expr
     ;; currently disabled because it triggers an internal error in the typechecker
     #;(pattern (((v:annotated-name) ...) seq-expr:expr)
-             #:with (expand ...) (list #'((v.ann-name ...) seq-expr) #'#:when #'#t))
+             #:with (expand ...) (list #`((v.ann-name ...)
+                                          #,(syntax-property #'seq-expr
+                                                             'type-ascription
+                                                             #'(Sequenceof (values v.ty ...))))
+                                       #'#:when #'#t))
     ;; when clause
     (pattern (~seq #:when guard:expr)
              #:with (expand ...) (list #'#:when #'guard)))
diff --git a/collects/typed-scheme/private/prims.rkt b/collects/typed-scheme/private/prims.rkt
index dd08d722e1..d226360505 100644
--- a/collects/typed-scheme/private/prims.rkt
+++ b/collects/typed-scheme/private/prims.rkt
@@ -392,11 +392,20 @@ This file defines two sorts of primitives. All of them are provided into any mod
        (let loop ((clauses #'clauses))
          (define-syntax-class for-clause
            ;; single-valued seq-expr
+           ;; unlike the definitions in for-clauses.rkt, this does not include
+           ;; #:when clauses, which are handled separately here
            (pattern (var:annotated-name seq-expr:expr)
-                    #:with expand #'(var.ann-name seq-expr))
+                    #:with expand #`(var.ann-name
+                                     #,(syntax-property #'seq-expr
+                                                        'type-ascription
+                                                        #'(Sequenceof var.ty))))
            ;; multi-valued seq-expr
-           (pattern ((v:annotated-name ...) seq-expr:expr)
-                    #:with expand #'((v.ann-name ...) seq-expr)))
+           ;; currently disabled because it triggers an internal error in the typechecker
+           #;(pattern ((v:annotated-name ...) seq-expr:expr)
+                    #:with expand #`((v.ann-name ...)
+                                     #,(syntax-property #'seq-expr
+                                                        'type-ascription
+                                                        #'(Sequenceof (values v.ty ...))))))
          (syntax-parse clauses
            [(head:for-clause next:for-clause ... #:when rest ...)
             (syntax-property