diff --git a/collects/tests/typed-scheme/succeed/for-over-hash.rkt b/collects/tests/typed-scheme/succeed/for-over-hash.rkt
new file mode 100644
index 00000000..be9e007b
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/for-over-hash.rkt
@@ -0,0 +1,5 @@
+#lang typed/racket
+
+(: v : (Listof Number))
+(define v (for/list ([(k v) (make-hash (list (cons 1 2) (cons 3 4)))])
+            (+ k v)))
diff --git a/collects/typed-scheme/private/base-env.rkt b/collects/typed-scheme/private/base-env.rkt
index 58f09fd2..a8e248cd 100644
--- a/collects/typed-scheme/private/base-env.rkt
+++ b/collects/typed-scheme/private/base-env.rkt
@@ -579,6 +579,10 @@
 [hash-map (-poly (a b c) ((-HT a b) (a b . -> . c) . -> . (-lst c)))]
 [hash-for-each (-poly (a b c) (-> (-HT a b) (-> a b c) -Void))]
 [hash-count (-poly (a b) (-> (-HT a b) -NonnegativeFixnum))]
+[hash-keys (-poly (a b) ((-HT a b) . -> . (-lst a)))]
+[hash-values (-poly (a b) ((-HT a b) . -> . (-lst b)))]
+[hash->list (-poly (a b) ((-HT a b) . -> . (-lst (-pair a b))))]
+
 [hash-copy (-poly (a b) (-> (-HT a b) (-HT a b)))]
 [eq-hash-code (-poly (a) (-> a -Integer))]
 [eqv-hash-code (-poly (a) (-> a -Integer))]
diff --git a/collects/typed-scheme/private/base-special-env.rkt b/collects/typed-scheme/private/base-special-env.rkt
index 2140c4fa..2c9c5a7f 100644
--- a/collects/typed-scheme/private/base-special-env.rkt
+++ b/collects/typed-scheme/private/base-special-env.rkt
@@ -52,23 +52,19 @@
      #:literals (let-values quote)
      [(let-values ([_ (m-s '(_) '())]) . _)
       #'m-s])
-   (-poly (a) 
+   (-poly (a b)
           (let ([seq-vals 
-                 (lambda ([a a])
+                 (lambda (a)
                    (-values (list 
-                             (-> Univ a)
+                             (-> Univ (-values a))
                              (-> Univ Univ)
                              Univ
                              (-> Univ Univ)
-                             (-> a Univ)
-                             (-> Univ a Univ))))])
-            (-> Univ (-seq a) (seq-vals))
-            #;
-            (cl->* (-> Univ (-lst a) (seq-vals))
-                   (-> Univ (-vec a) (seq-vals))
-                   (-> Univ -String (seq-vals -Char))
-                   (-> Univ -Bytes (seq-vals -Nat))
-                   (-> Univ -Input-Port (seq-vals -Nat)))))]
+                             (->* a Univ)
+                             (->* (cons Univ a) Univ))))])
+            (cl->*
+             (-> Univ (-seq a) (seq-vals (list a)))
+             (-> Univ (-seq a b) (seq-vals (list a b))))))]
   ;; in-range
   [(syntax-parse (local-expand #'(in-range 1) 'expression #f)
      [(i-n _ ...)
diff --git a/collects/typed-scheme/rep/type-rep.rkt b/collects/typed-scheme/rep/type-rep.rkt
index 4a7ca8b7..4cddd134 100644
--- a/collects/typed-scheme/rep/type-rep.rkt
+++ b/collects/typed-scheme/rep/type-rep.rkt
@@ -196,7 +196,8 @@
                  (hash-remove (combine-frees (map free-vars* (cons dty rs))) dbound)
                  (combine-frees (map free-vars* (cons dty rs))))
              (if (symbol? dbound)
-                 (combine-frees (cons (make-immutable-hasheq (list (cons dbound Covariant))) (map free-idxs* (cons dty rs))))
+                 (combine-frees (cons (make-immutable-hasheq (list (cons dbound Covariant))) 
+                                      (map free-idxs* (cons dty rs))))
                  (combine-frees (map free-idxs* (cons dty rs))))]
     [#:fold-rhs (*ValuesDots (map type-rec-id rs) (type-rec-id dty) dbound)])
 
diff --git a/collects/typed-scheme/typecheck/tc-app.rkt b/collects/typed-scheme/typecheck/tc-app.rkt
index 96d546e7..a2a6b1df 100644
--- a/collects/typed-scheme/typecheck/tc-app.rkt
+++ b/collects/typed-scheme/typecheck/tc-app.rkt
@@ -5,7 +5,7 @@
          "tc-app-helper.rkt" "find-annotation.rkt" "tc-funapp.rkt"
          "tc-subst.rkt" (prefix-in c: racket/contract)
          syntax/parse racket/match racket/trace scheme/list 
-	 unstable/sequence unstable/debug
+	 unstable/sequence unstable/debug unstable/list
          ;; fixme - don't need to be bound in this phase - only to make tests work
          scheme/bool
          racket/unsafe/ops
@@ -281,13 +281,15 @@
                 (tc-error/expr #:return (or expected (ret Univ)) "expected Parameter, but got ~a" t)
                 (loop (cddr args))]))))]
     ;; use the additional but normally ignored first argument to make-sequence to provide a better instantiation
-    [(#%plain-app (~var op (id-from 'make-sequence 'racket/private/for)) (~and quo ((~literal quote) (i:id))) arg:expr)
-     #:when (type-annotation #'i)     
+    [(#%plain-app (~var op (id-from 'make-sequence 'racket/private/for)) (~and quo ((~literal quote) (i:id ...))) arg:expr)
+     #:when (andmap type-annotation (syntax->list #'(i ...)))
      (match (single-value #'op)
          [(tc-result1: (and t Poly?))
           (tc-expr/check #'quo (ret Univ))
           (tc/funapp #'op #'(quo arg) 
-                     (ret (instantiate-poly t (list (type-annotation #'i))))
+                     (ret (instantiate-poly t (extend (list Univ Univ)
+                                                      (map type-annotation (syntax->list #'(i ...)))
+                                                      Univ)))
                      (list (ret Univ) (single-value #'arg))
                      expected)])]
     ;; unsafe struct operations