diff --git a/collects/tests/typed-scheme/fail/ann-map-funcs.ss b/collects/tests/typed-scheme/fail/ann-map-funcs.ss
new file mode 100644
index 00000000..f8ba9fb4
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/ann-map-funcs.ss
@@ -0,0 +1,17 @@
+#;
+(exn-pred 3)
+#lang typed-scheme
+
+(: map-with-funcs (All (b a ...) ((a ... a -> b) * -> (a ... a -> (Listof b)))))
+
+(define (map-with-funcs . fs)
+ (lambda as
+   (map (lambda: ([f : (a ... a -> b)])
+          (apply f as))
+        fs)))
+
+(ann (map-with-funcs + - * /) (Number Number * -> (Listof Integer)))
+
+(ann (map-with-funcs + - * /) (Number * -> (Listof Number)))
+
+(ann (map-with-funcs + - * /) (Integer * -> (Listof Number)))
diff --git a/collects/tests/typed-scheme/fail/apply-dots.ss b/collects/tests/typed-scheme/fail/apply-dots.ss
new file mode 100644
index 00000000..d798f8c3
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/apply-dots.ss
@@ -0,0 +1,13 @@
+#;
+(exn-pred 2)
+#lang typed-scheme
+
+(plambda: (a ...) ([z : String] . [w : Number *])
+          (apply (case-lambda: (([x : Number] . [y : Number ... a]) x))
+                 w))
+
+(plambda: (a ...) ([z : String] . [w : Number *])
+          (apply (case-lambda: (([x : Number] . [y : Number ... a]) x)
+                               (([x : String] [y : String] . [z : String *]) 0)
+                               ([y : String *] 0))
+                 w))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/fail/cl-bug.ss b/collects/tests/typed-scheme/fail/cl-bug.ss
new file mode 100644
index 00000000..44300184
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/cl-bug.ss
@@ -0,0 +1,7 @@
+#lang typed-scheme
+
+(: f3 (case-lambda (Integer * -> Integer) (Number * -> Number)))
+(define (f3 x y) (+ x y))
+
+(: f2 (case-lambda (Number * -> Number)))
+(define (f2 x y) (+ x y))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/fail/dotted-identity.ss b/collects/tests/typed-scheme/fail/dotted-identity.ss
new file mode 100644
index 00000000..543f46c3
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/dotted-identity.ss
@@ -0,0 +1,11 @@
+#lang typed-scheme
+
+;; I don't believe the below should work, but it points out where that internal error is coming from.
+
+(: f (All (a ...) ((a ... a -> Integer) -> (a ... a -> Integer))))
+(define (f x) x)
+
+(: g (All (b ...) ( -> (b ... b -> Integer))))
+(define (g) (lambda xs 0))
+
+(f (g))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/fail/formal-len-mismatches.ss b/collects/tests/typed-scheme/fail/formal-len-mismatches.ss
new file mode 100644
index 00000000..bd640a06
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/formal-len-mismatches.ss
@@ -0,0 +1,17 @@
+#lang typed-scheme
+
+(: f (Integer Integer Integer * -> Integer))
+(define (f x)
+  (+ #\c x))
+
+(: f2 (Integer Integer * -> Integer))
+(define (f2 x y . z)
+  (apply + #\c x y z))
+
+(: f4 (Integer Integer -> Integer))
+(define (f4 x y w . z)
+  (apply + #\c x y w z))
+
+(: f3 (Integer Integer -> Integer))
+(define (f3 x . z)
+  (apply + #\c x z))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/fail/infer-dots.ss b/collects/tests/typed-scheme/fail/infer-dots.ss
new file mode 100644
index 00000000..40dea049
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/infer-dots.ss
@@ -0,0 +1,16 @@
+#lang typed-scheme
+
+(require typed-scheme/private/extra-procs)
+
+(map + (list 1 2 3) (list 10 20 30) (list 'a 'b 'c))
+
+;; Arity mismatch.
+(: g (Integer Integer Integer -> Integer))
+(define (g x y z) 0)
+
+(map g (list 1 2 3) (list 4 5 6))
+
+(: h (Integer Integer Integer * -> Integer))
+(define (h x y . z) 0)
+
+(map h (list 1 2 3))
diff --git a/collects/tests/typed-scheme/fail/values-dots.ss b/collects/tests/typed-scheme/fail/values-dots.ss
new file mode 100644
index 00000000..6c08fff5
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/values-dots.ss
@@ -0,0 +1,25 @@
+#;
+(exn-pred 7)
+#lang typed-scheme
+
+(require typed-scheme/private/extra-procs)
+
+(: 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 f bs)) fs))))
+
+(map-with-funcs (lambda () 1))
+
+(map-with-funcs (lambda: ([x : Integer] [y : Integer] . [z : Integer *])
+                         (+ x y)))
+
+(map-with-funcs (lambda: ([x : Integer] [y : Integer])
+                         (+ x y)))
+
+(map-with-funcs + - * / string-append)
+
+((map-with-funcs + - * /) 1 2 3)
+((map-with-funcs + - * /) 1 2 3 4 5)
+((map-with-funcs + - * /) 1 2 3 "foo")
diff --git a/collects/tests/typed-scheme/main.ss b/collects/tests/typed-scheme/main.ss
index d7dfca88..3a3d2fc7 100644
--- a/collects/tests/typed-scheme/main.ss
+++ b/collects/tests/typed-scheme/main.ss
@@ -4,8 +4,8 @@
 
 (require (planet schematics/schemeunit/test)
          (planet schematics/schemeunit/text-ui)
-         #;(planet schematics/schemeunit/graphical-ui)
          mzlib/etc
+         compiler/compiler
          scheme/match
          "unit-tests/all-tests.ss"
          "unit-tests/test-utils.ss")
@@ -20,23 +20,26 @@
    (lambda (val)
      (and (exn? val)
           (for/and ([e args])
-                   (if (procedure? e)
-                       (e val)
-                       (begin
-                         (regexp-match e (exn-message val)))))))
+                   (cond [(procedure? e) (e val)]
+                         [(number? e)
+                          (and (exn:fail:syntax? val)
+                               (= e (length (exn:fail:syntax-exprs val))))]
+                         [else                          
+                          (regexp-match e (exn-message val))]))))
    args))
   
 (define (exn-pred p)
   (let ([sexp (with-handlers
-                  ([values (lambda _ #f)])
-                (let ([prt (open-input-file p)])
-                  (begin0 (begin (read-line prt 'any) 
-                                 (read prt))
-                          (close-input-port prt))))])   
+                  ([exn:fail? (lambda _ #f)])
+                (call-with-input-file
+                 p
+                 (lambda (prt) 
+                   (read-line prt 'any) (read prt))))])
     (match sexp
       [(list-rest 'exn-pred e)
        (eval `(exn-matches . ,e) (namespace-anchor->namespace a))]
-      [_ (exn-matches ".*typecheck.*" exn:fail:syntax?)])))
+      [_ 
+       (exn-matches ".*typecheck.*" exn:fail:syntax?)])))
 
 (define (mk-tests dir loader test)
   (lambda ()
@@ -50,20 +53,23 @@
           (build-path path p)
           (lambda ()
             (parameterize ([read-accept-reader #t]
-                           [current-load-relative-directory 
-                            path])
+                           [current-load-relative-directory path]
+                           [current-directory path])
               (with-output-to-file "/dev/null" #:exists 'append
                 (lambda () (loader p)))))))))
     (apply test-suite dir
            tests)))
 
+(define (dr p)
+  ((compile-zos #f) (list p) 'auto)
+  (parameterize ([current-namespace (make-base-empty-namespace)])    
+    (dynamic-require `(file ,(path->string p)) #f)))
+
 (define succ-tests (mk-tests "succeed" 
-                             (lambda (p) (parameterize ([current-namespace (make-base-empty-namespace)])
-                                           (dynamic-require `(file ,(path->string p)) #f)))
+                             dr
                              (lambda (p thnk) (check-not-exn thnk))))
 (define fail-tests (mk-tests "fail"
-                             (lambda (p) (parameterize ([current-namespace (make-base-empty-namespace)])
-                                           (dynamic-require `(file ,(path->string p)) #f)))
+                             dr
                              (lambda (p thnk)
                                (define-values (pred info) (exn-pred p))
                                (with-check-info
diff --git a/collects/tests/typed-scheme/succeed/ann-map-funcs.ss b/collects/tests/typed-scheme/succeed/ann-map-funcs.ss
new file mode 100644
index 00000000..a7835a36
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/ann-map-funcs.ss
@@ -0,0 +1,11 @@
+#lang typed-scheme
+
+(: map-with-funcs (All (b a ...) ((a ... a -> b) * -> (a ... a -> (Listof b)))))
+
+(define (map-with-funcs . fs)
+ (lambda as
+   (map (lambda: ([f : (a ... a -> b)])
+          (apply f as))
+        fs)))
+
+(ann (map-with-funcs + - * /) (Number Number * -> (Listof Number)))
diff --git a/collects/tests/typed-scheme/succeed/apply-dots.ss b/collects/tests/typed-scheme/succeed/apply-dots.ss
new file mode 100644
index 00000000..d7ad17a0
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/apply-dots.ss
@@ -0,0 +1,65 @@
+#lang typed-scheme
+
+(plambda: (a ...) ([z : String] . [w : Number ... a])
+          (apply (lambda: ([x : Number] . [y : Number ... a]) x)
+                 1 w))
+
+(plambda: (a ...) ([z : String] . [w : Number ... a])
+          (apply (lambda: ([x : Number] . [y : Number *]) x)
+                 1 w))
+
+(plambda: (a ...) ([z : String] . [w : Number *])
+          (apply (lambda: ([x : Number] . [y : Number *]) x)
+                 1 w))
+
+(plambda: (a ...) ([z : String] . [w : Number *])
+          (apply (case-lambda: (([x : Number] . [y : Number ... a]) x)
+                               (([x : String] [y : String] . [z : String *]) 0)
+                               ([y : Number *] 0))
+                 w))
+
+;; */*/poly
+(plambda: (a ...) ([z : String] . [w : Number *])
+          (apply (plambda: (b) ([x : b] . [y : Number *]) x)
+                 1 w))
+
+(plambda: (a ...) ([z : String] . [w : Number *])
+          (apply (plambda: (b) ([x : b] . [y : Number *]) x)
+                 1 2 3 w))
+
+;; */*/polydots
+(plambda: (a ...) ([z : String] . [w : Number *])
+          (apply (plambda: (b ...) ([x : Number] . [y : Number *]) x)
+                 1 w))
+
+(plambda: (a ...) ([z : String] . [w : Number *])
+          (apply (plambda: (b ...) ([x : Number] . [y : Number *]) x)
+                 1 1 1 w))
+
+;; */.../poly
+(plambda: (a ...) ([z : String] . [w : Number ... a])
+          (apply (plambda: (b) ([x : Number] . [y : Number *]) x)
+                 1 w))
+
+(plambda: (a ...) ([z : String] . [w : Number ... a])
+          (apply (plambda: (b) ([x : Number] . [y : Number *]) x)
+                 1 1 1 1 w))
+
+;; */.../polydots
+#;(plambda: (a ...) ([z : String] . [w : Number ... a])
+          (apply (plambda: (b ...) ([x : Number] . [y : Number *]) x)
+                 1 w))
+
+#;(plambda: (a ...) ([z : String] . [w : Number ... a])
+          (apply (plambda: (b ...) ([x : Number] . [y : Number *]) x)
+                 1 1 1 1 w))
+
+;; .../.../poly
+(plambda: (a ...) ([z : String] . [w : Number ... a])
+          (apply (plambda: (b) ([x : Number] . [y : Number ... a]) x)
+                 1 w))
+
+#;(plambda: (a ...) ([z : String] . [w : Number ... a])
+          (apply (plambda: (b ...) ([x : Number] . [y : Number ... a]) x)
+                 1 w))
+
diff --git a/collects/tests/typed-scheme/succeed/batched-queue.scm b/collects/tests/typed-scheme/succeed/batched-queue.scm
index 71e1db34..7c2ae9e9 100644
--- a/collects/tests/typed-scheme/succeed/batched-queue.scm
+++ b/collects/tests/typed-scheme/succeed/batched-queue.scm
@@ -82,5 +82,5 @@
 
 ;; TESTS
 
-(= 0 (size (empty)))
+(= 0 (size ((inst empty Number))))
 
diff --git a/collects/tests/typed-scheme/succeed/cl-bug.ss b/collects/tests/typed-scheme/succeed/cl-bug.ss
new file mode 100644
index 00000000..09b9327f
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/cl-bug.ss
@@ -0,0 +1,7 @@
+#lang typed-scheme
+
+(: f (case-lambda (Integer * -> Integer) (Number * -> Number)))
+(define (f . x) (+ 1 2))
+
+(: f4 (case-lambda (Integer * -> Integer) (Number * -> Number)))
+(define (f4 . x) (apply + x))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/dot-intro.ss b/collects/tests/typed-scheme/succeed/dot-intro.ss
new file mode 100644
index 00000000..7afb8c1a
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/dot-intro.ss
@@ -0,0 +1,9 @@
+#lang typed-scheme
+
+(define x
+  (plambda: (a ...) ([x : Number] . [y : Number ... a])
+    (ormap zero? (map add1 y))))
+
+(define y
+  (plambda: (a ...) ([x : Number] . [y : a ... a])
+    (ormap null? (map list y))))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/dotted-identity.ss b/collects/tests/typed-scheme/succeed/dotted-identity.ss
new file mode 100644
index 00000000..78a83976
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/dotted-identity.ss
@@ -0,0 +1,18 @@
+#lang typed-scheme
+
+(: f (All (a ...) ((a ... a -> Integer) -> (a ... a -> Integer))))
+(define (f x) x)
+
+(: y (Integer Integer -> Integer))
+(define (y a b) (+ a b))
+
+#{(f y) :: (Integer Integer -> Integer)}
+
+(: z (Integer * -> Integer))
+(define (z . xs) (apply + xs))
+
+((f z) 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18)
+
+(f z)
+
+#{(f z) :: (Integer * -> Integer)}
diff --git a/collects/tests/typed-scheme/succeed/fold-left-inst.ss b/collects/tests/typed-scheme/succeed/fold-left-inst.ss
new file mode 100644
index 00000000..100ecbba
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/fold-left-inst.ss
@@ -0,0 +1,19 @@
+#lang typed-scheme
+
+(: fold-left (All (c a b ...) ((c a b ... b -> c) c (Listof a) (Listof b) ... b -> c)))
+(define (fold-left f c as . bss)
+  (if (or (null? as)
+          (ormap null? bss))
+      c
+      (apply (inst fold-left c a b ... b) f 
+             (apply f c (car as) (map car bss))
+             (cdr as) (map cdr bss))))
+
+(: fold-right (All (c a b ...) ((c a b ... b -> c) c (Listof a) (Listof b) ... b -> c)))
+(define (fold-right f c as . bss)
+  (if (or (null? as)
+          (ormap null? bss))
+      c
+      (apply f
+             (apply (inst fold-left c a b ... b) f c (cdr as) (map cdr bss))
+             (car as) (map car bss))))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/fold-left.ss b/collects/tests/typed-scheme/succeed/fold-left.ss
new file mode 100644
index 00000000..ca1364da
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/fold-left.ss
@@ -0,0 +1,41 @@
+#lang typed-scheme
+
+(: fold-left (All (c a b ...) ((c a b ... b -> c) c (Listof a) (Listof b) ... b -> c)))
+(define (fold-left f c as . bss)
+  (if (or (null? as)
+          (ormap null? bss))
+      c
+      (apply fold-left f 
+             (apply f c (car as) (map car bss))
+             (cdr as) (map cdr bss))))
+
+(: fold-right (All (c a b ...) ((c a b ... b -> c) c (Listof a) (Listof b) ... b -> c)))
+(define (fold-right f c as . bss)
+  (if (or (null? as)
+          (ormap null? bss))
+      c
+      (apply f
+             (apply fold-right f c (cdr as) (map cdr bss))
+             (car as) (map car bss))))
+
+;; Matthias -- tell me why this returns 4.
+((plambda: (x ...) [xs : x ... x] 
+    (apply fold-left 
+           (lambda: ([a : Integer] [b : Integer] . [xs : x ... x])
+             (+ a b))
+           3 
+           (list 1 2 3) 
+           (map list xs)))
+ 3 4 5)
+
+((plambda: (x ...) [xs : x ... x] 
+    (apply fold-right
+           (lambda: ([a : Integer] [b : Integer] . [xs : x ... x])
+             (+ a b))
+           3 
+           (list 1 2 3) 
+           (map list xs)))
+ 3 4 5)
+
+(fold-left  (lambda: ([a : (Listof Integer)] [c : Integer]) (cons c a)) null (list 3 4 5 6))
+(fold-right (lambda: ([a : (Listof Integer)] [c : Integer]) (cons c a)) null (list 3 4 5 6))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/force-delay.ss b/collects/tests/typed-scheme/succeed/force-delay.ss
new file mode 100644
index 00000000..fd411d55
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/force-delay.ss
@@ -0,0 +1,9 @@
+#lang typed-scheme
+
+(require scheme/promise)
+
+;((plambda: (a) ([x : a]) x) (error 'foo))
+
+(force (delay 3))
+
+(call-with-values (lambda () 3) list)
diff --git a/collects/tests/typed-scheme/succeed/infer-dots.ss b/collects/tests/typed-scheme/succeed/infer-dots.ss
new file mode 100644
index 00000000..89892336
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/infer-dots.ss
@@ -0,0 +1,18 @@
+#lang typed-scheme
+
+(require typed-scheme/private/extra-procs)
+
+(: f (Integer Integer -> Integer))
+(define (f x y) (+ x y))
+
+(map f (list 1 2 3) (list 10 20 30))
+
+(map + (list 1 2 3) (list 10 20 30) (list 10 20 30))
+
+(map + (list 1 2 3) (list 10 20 30) (list 10 20 30) (list 10 20 30) (list 10 20 30) (list 10 20 30) (list 10 20 30) (list 10 20 30) (list 10 20 30) (list 10 20 30) (list 10 20 30) (list 10 20 30) (list 10 20 30) (list 10 20 30) (list 10 20 30) (list 10 20 30))
+
+(: h (Integer Integer Integer * -> Integer))
+(define (h x y . z) (apply + (cons x (cons y z))))
+
+(map h (list 1 2 3) (list 4 5 6))
+(map h (list 1 2 3) (list 4 5 6) (list 4 5 6))
diff --git a/collects/tests/typed-scheme/succeed/inst-dots.ss b/collects/tests/typed-scheme/succeed/inst-dots.ss
new file mode 100644
index 00000000..51bf3223
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/inst-dots.ss
@@ -0,0 +1,7 @@
+#lang typed-scheme
+
+(require typed-scheme/private/extra-procs)
+
+((inst map Number Number Number Number Number Number Number) 
+ + 
+ (list 1 2 3) (list 2 3 4) (list 1 2 3) (list 2 3 4) (list 1 2 3) (list 2 3 4))
diff --git a/collects/tests/typed-scheme/succeed/int-def-colon.ss b/collects/tests/typed-scheme/succeed/int-def-colon.ss
index b74ff402..3372f8cf 100644
--- a/collects/tests/typed-scheme/succeed/int-def-colon.ss
+++ b/collects/tests/typed-scheme/succeed/int-def-colon.ss
@@ -2,7 +2,7 @@
 
 (define-type-alias Int Integer)
 
-(: foo (Int -> Int))
+(: foo ( -> Int))
 (define (foo)
  (: loop (Int -> Int))
  (define (loop x)
diff --git a/collects/tests/typed-scheme/succeed/leftist-heap.ss b/collects/tests/typed-scheme/succeed/leftist-heap.ss
index 0423a4a3..ff9f43b3 100644
--- a/collects/tests/typed-scheme/succeed/leftist-heap.ss
+++ b/collects/tests/typed-scheme/succeed/leftist-heap.ss
@@ -205,7 +205,7 @@
                     s))
             0 h)))
   
-  (pdefine: (a) (-heap . [xs : a]) : (Heap a)
+  (pdefine: (a) (-heap . [xs : a *]) : (Heap a)
     (list->heap xs))   
 
   
diff --git a/collects/tests/typed-scheme/succeed/lots-o-bugs.ss b/collects/tests/typed-scheme/succeed/lots-o-bugs.ss
new file mode 100644
index 00000000..98e4711c
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/lots-o-bugs.ss
@@ -0,0 +1,21 @@
+#lang typed-scheme
+
+;; (All (a ...) ( -> (a ... a -> Integer)))
+
+(plambda: (a ...) ()
+          (lambda: [ys : a ... a] 3))
+
+(define x (plambda: (a ...) () (lambda: [ys : a ... a] 3)))
+
+
+
+(: y (All (a ...) ( -> (a ... a -> Integer))))
+(define y (plambda: (a ...) () (lambda: [ys : a ... a] 3)))
+
+(: z (All (a ...) ( -> (a ... a -> Integer))))
+(define z (lambda () (lambda ys 3)))
+
+#;((plambda: (a ...) () (lambda: [ys : a ... a] 3)))
+
+#;((plambda: (a ...) [xs : a ... a] (lambda: [ys : a ... a] 3))
+   1 2 3 "foo")
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/metrics.ss b/collects/tests/typed-scheme/succeed/metrics.ss
index 5e6d2eb0..f5d49d8a 100644
--- a/collects/tests/typed-scheme/succeed/metrics.ss
+++ b/collects/tests/typed-scheme/succeed/metrics.ss
@@ -14,15 +14,15 @@
 (require/typed filename-extension (Path -> (U #f Bytes)) (lib "file.ss"))
 (require/typed normalize-path (Path Path -> Path) (lib "file.ss"))
 (require/typed explode-path (Path -> (Listof Path)) (lib "file.ss"))
-(require/typed srfi48::format (Port String String top .. -> top)  "patch.ss")
+(require/typed srfi48::format (Port String String top * -> top)  "patch.ss")
 ;; FIXME - prefix
-#;(require/typed srfi48:format ( Port String String top .. -> top) (prefix-in srfi48: srfi/48))
-(require mzlib/match
-         ;mzlib/file
-         ;mzlib/list
-         ;mzlib/etc
-         (prefix-in srfi13: srfi/13)
-         ;(prefix srfi48: srfi/48)
+#;(require/typed srfi48:format ( Port String String top * -> top) (prefix-in srfi48: (lib "48.ss" "srfi")))
+(require (lib "match.ss")
+         ;(lib "file.ss")
+         ;(lib "list.ss")
+         ;(lib "etc.ss")
+         (prefix-in srfi13: (lib "13.ss" "srfi"))
+         ;(prefix srfi48: (lib "48.ss" "srfi"))
          )
 
 (define-type-alias Sexpr Any)
diff --git a/collects/tests/typed-scheme/succeed/nested-poly.ss b/collects/tests/typed-scheme/succeed/nested-poly.ss
new file mode 100644
index 00000000..8b67fab8
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/nested-poly.ss
@@ -0,0 +1,5 @@
+#lang typed-scheme
+
+(: f (All (A ...) (All (B ...) (A ... A -> Integer))))
+
+(define (f . xs) 5)
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/poly-subtype.ss b/collects/tests/typed-scheme/succeed/poly-subtype.ss
new file mode 100644
index 00000000..39288d79
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/poly-subtype.ss
@@ -0,0 +1,20 @@
+#lang typed-scheme
+
+(: f (All (a) (a -> a)))
+(define (f x) x)
+
+(define: x : (Number -> Number) f)
+
+#;
+((lambda: ([f : (All (a ...) (a ... a -> Number))]) 12)
+ +)
+
+#;(Lambda (a ...)
+  ((lambda: ([f : (a .. a -> Number)]) 12) +))
+
+#|
+(: g (All (a ...) ((a ... a -> Number) -> Number)))
+
+(define (g x) 3)
+
+|#
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/priority-queue.scm b/collects/tests/typed-scheme/succeed/priority-queue.scm
index bf04a2e4..e2d7e57c 100644
--- a/collects/tests/typed-scheme/succeed/priority-queue.scm
+++ b/collects/tests/typed-scheme/succeed/priority-queue.scm
@@ -80,7 +80,7 @@
 
 ;; FIXME -- too many annotations needed on cons
 (pdefine: (a) (insert* [xs : (list-of a)] [ps : (list-of number)] [pq : (priority-queue a)]) : (priority-queue a)
-          (make (heap:insert* (map #{#{cons @ number a} :: (number a -> (cons number a))} ps xs) (heap pq))))
+          (make (heap:insert* (map #{cons @ number a} ps xs) (heap pq))))
 
 (pdefine: (a) (delete-min [pq : (priority-queue a)]) : (priority-queue a)
 	  (let ([h (heap pq)])
diff --git a/collects/tests/typed-scheme/succeed/random-bits.ss b/collects/tests/typed-scheme/succeed/random-bits.ss
index 725d7e5a..eea51558 100644
--- a/collects/tests/typed-scheme/succeed/random-bits.ss
+++ b/collects/tests/typed-scheme/succeed/random-bits.ss
@@ -38,7 +38,7 @@
                                        [randomize! : ( -> Void)]
                                        [pseudo-randomize! : (Integer Integer -> Void)]
                                        [make-integers : (-> (Integer -> Integer)) ] 
-                                       [make-reals : ( Nb .. -> ( -> Number))])) 
+                                       [make-reals : ( Nb * -> ( -> Number))])) 
   (define-type-alias Random :random-source)
   (define: (:random-source-make 
             [state-ref : ( -> SpList)]
@@ -46,7 +46,7 @@
             [randomize! : ( -> Void)]
             [pseudo-randomize! : (Integer Integer -> Void)]
             [make-integers : (-> (Integer -> Integer)) ] 
-            [make-reals : (Nb .. -> (-> Number))])
+            [make-reals : (Nb * -> (-> Number))])
             : Random
     (make-:random-source state-ref state-set! randomize! pseudo-randomize! make-integers make-reals ))
   
@@ -564,7 +564,7 @@
            (mrg32k3a-random-integer state n))
           (else
            (mrg32k3a-random-large state n)))))
-     (lambda: [args : Nb] 
+     (lambda: [args : Nb *] 
        (cond
         ((null? args)
          (lambda () 
@@ -603,7 +603,7 @@
 (define: (random-source-make-integers [s : Random]): (Nb -> Nb)
   ((:random-source-make-integers s)))
 
-(define: (random-source-make-reals [s : Random] . [unit : Nb]) : ( -> Flt)
+(define: (random-source-make-reals [s : Random] . [unit : Nb *]) : ( -> Flt)
   (apply (:random-source-make-reals s)  unit))
 
 ; ---
diff --git a/collects/tests/typed-scheme/succeed/star-sizes.ss b/collects/tests/typed-scheme/succeed/star-sizes.ss
new file mode 100644
index 00000000..6d04d748
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/star-sizes.ss
@@ -0,0 +1,6 @@
+#lang typed-scheme
+
+(: f (All (a) ((Integer a * -> Integer) -> Integer)))
+(define (f g) 0)
+
+(f +)
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/string-const.ss b/collects/tests/typed-scheme/succeed/string-const.ss
index 9437ae14..77e0ca02 100644
--- a/collects/tests/typed-scheme/succeed/string-const.ss
+++ b/collects/tests/typed-scheme/succeed/string-const.ss
@@ -3,3 +3,5 @@
 (require string-constants/string-constant)
 
 (string-constant cancel)
+
+(this-language)
diff --git a/collects/tests/typed-scheme/succeed/unholy-terror.ss b/collects/tests/typed-scheme/succeed/unholy-terror.ss
new file mode 100644
index 00000000..1abdcc3a
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/unholy-terror.ss
@@ -0,0 +1,65 @@
+#lang typed-scheme
+
+(apply (plambda: (a ...) [ys : (a ... a -> Number) *]
+         (lambda: [zs : a ... a]
+            (map (lambda: ([y : (a ... a -> Number)])
+                   (apply y zs))
+                 ys)))
+       (list (lambda: ([x : Number] [y : Number]) (+ x y))
+             (lambda: ([x : Number] [y : Number]) (- x y))
+             (lambda: ([x : Number] [y : Number]) (* x y))
+             (lambda: ([x : Number] [y : Number]) (/ x y))))
+
+((apply (plambda: (a ...) [ys : (a ... a -> Number) *]
+          (lambda: [zs : a ... a]
+            (map (lambda: ([y : (a ... a -> Number)])
+                   (apply y zs))
+                 ys)))
+        (list (lambda: ([x : Number] [y : Number]) (+ x y))
+              (lambda: ([x : Number] [y : Number]) (- x y))
+              (lambda: ([x : Number] [y : Number]) (* x y))
+              (lambda: ([x : Number] [y : Number]) (/ x y))))
+ 3 4)
+
+(apply (plambda: (a ...) [ys : (a ... a -> Number) *]
+         (lambda: [zs : a ... a]
+                  (map (lambda: ([y : (a ... a -> Number)])
+                                (apply y zs))
+                       ys)))
+       (list + - * /))
+
+((plambda: (a ...) [ys : (a ... a -> Number) *]
+   (lambda: [zs : a ... a]
+     (map (lambda: ([y : (a ... a -> Number)])
+            (apply y zs))
+          ys)))
+ (lambda: ([x : Number] [y : Number]) (+ x y))
+ (lambda: ([x : Number] [y : Number]) (- x y))
+ (lambda: ([x : Number] [y : Number]) (* x y))
+ (lambda: ([x : Number] [y : Number]) (/ x y)))
+
+(((plambda: (a ...) [ys : (a ... a -> Number) *]
+    (lambda: [zs : a ... a]
+      (map (lambda: ([y : (a ... a -> Number)])
+             (apply y zs))
+           ys)))
+  (lambda: ([x : Number] [y : Number]) (+ x y))
+  (lambda: ([x : Number] [y : Number]) (- x y))
+  (lambda: ([x : Number] [y : Number]) (* x y))
+  (lambda: ([x : Number] [y : Number]) (/ x y)))
+ 3 4)
+
+((plambda: (a ...) [ys : (a ... a -> Number) *]
+   (lambda: [zs : a ... a]
+     (map (lambda: ([y : (a ... a -> Number)])
+            (apply y zs))
+          ys)))
+ + - * /)
+
+(: map-with-funcs (All (b a ...) ((a ... a -> b) * -> (a ... a -> (Listof b)))))
+(define (map-with-funcs . fs)
+  (lambda as
+    (map (lambda: ([f : (a ... a -> b)])
+           (apply f as))
+         fs)))
+(map-with-funcs + - * /)
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/values-dots.ss b/collects/tests/typed-scheme/succeed/values-dots.ss
new file mode 100644
index 00000000..0078526f
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/values-dots.ss
@@ -0,0 +1,30 @@
+#lang typed-scheme
+
+(require typed-scheme/private/extra-procs)
+
+
+(call-with-values (lambda () (values 1 2)) (lambda: ([x : Number] [y : Number]) (+ x y)))
+
+(#{call-with-values* @ Integer Integer Integer} (lambda () (values 1 2)) (lambda: ([x : Integer] [y : Integer]) (+ x y)))
+
+
+(call-with-values* (lambda () (values 1 2)) (lambda: ([x : Integer] [y : Integer]) (+ x y)))
+
+(: 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 f bs)) fs))))
+
+(map-with-funcs + - * /)
+
+(inst map-with-funcs Integer Integer)
+
+(map-with-funcs 
+ (lambda: ([x : Integer] [y : Integer]) (+ x y))
+ (lambda: ([x : Integer] [y : Integer]) (- x y)) )
+
+(((inst map-with-funcs Integer Integer)
+    (lambda: ([x : Integer] [y : Integer]) (+ x y))
+    (lambda: ([x : Integer] [y : Integer]) (- x y)))
+   3 4)
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/varargs-tests.ss b/collects/tests/typed-scheme/succeed/varargs-tests.ss
index 0ebacce8..ccf4ec59 100644
--- a/collects/tests/typed-scheme/succeed/varargs-tests.ss
+++ b/collects/tests/typed-scheme/succeed/varargs-tests.ss
@@ -17,15 +17,15 @@
 (apply + '(2 3 4))
 
 
-(define: f : (number boolean .. -> number)
-  (lambda: ([x : number] . [y : boolean])
+(define: f : (number boolean * -> number)
+  (lambda: ([x : number] . [y : boolean *])
            (if (and (pair? y) (car y)) x (- x))))
 
-(define: f-cl : (number boolean .. -> number)
-  (case-lambda: [([x : number] . [y : boolean])
+(define: f-cl : (number boolean * -> number)
+  (case-lambda: [([x : number] . [y : boolean *])
 		 (if (and (pair? y) (car y)) x (- x))]))
 
-(define: (f* [x : number] . [y : boolean]) : number
+(define: (f* [x : number] . [y : boolean *]) : number
   (if (and (pair? y) (car y)) x (- x)))
 
 (f 3)
diff --git a/collects/tests/typed-scheme/unit-tests/all-tests.ss b/collects/tests/typed-scheme/unit-tests/all-tests.ss
index 2e069f7f..aca0a4d1 100644
--- a/collects/tests/typed-scheme/unit-tests/all-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/all-tests.ss
@@ -9,14 +9,17 @@
  "parse-type-tests.ss" ;; done
  "type-annotation-test.ss" ;; done
  "module-tests.ss"
+ "subst-tests.ss"
  "infer-tests.ss")
 
-(require (private planet-requires))
+(require (private planet-requires infer infer-dummy))
 
 (require (schemeunit))
 
 (provide unit-tests)
 
+(infer-param infer)
+
 (define unit-tests
   (apply
    test-suite 
diff --git a/collects/tests/typed-scheme/unit-tests/infer-tests.ss b/collects/tests/typed-scheme/unit-tests/infer-tests.ss
index 27726a74..f1d5e22b 100644
--- a/collects/tests/typed-scheme/unit-tests/infer-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/infer-tests.ss
@@ -1,6 +1,6 @@
 #lang scheme/base
 (require "test-utils.ss" (for-syntax scheme/base))
-(require (private planet-requires type-effect-convenience type-rep unify union infer-ops type-utils)
+(require (private planet-requires type-effect-convenience type-rep union infer type-utils)
          (prefix-in table: (private tables)))
 (require (schemeunit)) 
 
@@ -25,21 +25,23 @@
               [fv-t (-poly (b c d e) (-v a)) a]
               [fv-t (-mu a (-lst a))]
               [fv-t (-mu a (-lst (-pair a (-v b)))) b]
+              
+              [fv-t (->* null (-v a) N) a] ;; check that a is CONTRAVARIANT
               ))
 
 (define-syntax-rule (i2-t t1 t2 (a b) ...)
   (test-check (format "~a ~a" t1 t2)
               equal?
-              (infer t1 t2 (fv t1))
+              (infer t1 t2 (fv t1) (fv t1))
               (list (list a b) ...)))
 
 (define-syntax-rule (i2-l t1 t2 fv (a b) ...)
   (test-check (format "~a ~a" t1 t2)
               equal?
-              (infer/list t1 t2 fv)
+              (infer/list t1 t2 fv fv)
               (list (list a b) ...)))
 
-(define (f t1 t2) (infer t1 t2 (fv t1)))
+(define (f t1 t2) (infer t1 t2 (fv t1) (fv t1)))
 
 (define-syntax-rule (i2-f t1 t2)
   (test-false (format "~a ~a" t1 t2)                   
diff --git a/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss b/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss
index cf8d0644..aa3882fd 100644
--- a/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss
@@ -69,12 +69,15 @@
    [(Number -> Number) (t:-> N N)]
    [(Number -> Number) (t:-> N N)]
    [(Number Number Number Boolean -> Number) (N N N B . t:-> . N)]
-   [(Number Number Number .. -> Boolean) ((list N N) N . ->* . B)]
+   [(Number Number Number * -> Boolean) ((list N N) N . ->* . B)]
    ;[((. Number) -> Number) (->* (list) N N)] ;; not legal syntax
    [(U Number Boolean) (Un N B)]
    [(U Number Boolean Number) (Un N B)]
    [(U Number Boolean 1) (Un N B)]
    [(All (a) (Listof a)) (-poly (a) (make-Listof  a))]
+   [(All (a ...) (a ... a -> Integer)) (-polydots (a) ( (list) (a a) . ->... . -Integer))]
+   [(∀ (a) (Listof a)) (-poly (a) (make-Listof  a))]
+   [(∀ (a ...) (a ... a -> Integer)) (-polydots (a) ( (list) (a a) . ->... . -Integer))]
    [(case-lambda (Number -> Boolean) (Number Number -> Number)) (cl-> [(N) B]
                                                                       [(N N) N])]
    [1 (-val 1)]
diff --git a/collects/tests/typed-scheme/unit-tests/remove-intersect-tests.ss b/collects/tests/typed-scheme/unit-tests/remove-intersect-tests.ss
index ea874f36..ca83402b 100644
--- a/collects/tests/typed-scheme/unit-tests/remove-intersect-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/remove-intersect-tests.ss
@@ -1,6 +1,6 @@
 #lang scheme/base
 (require "test-utils.ss" (for-syntax scheme/base))
-(require (private type-rep type-effect-convenience planet-requires remove-intersect unify subtype union infer-ops))
+(require (private type-rep type-effect-convenience planet-requires remove-intersect subtype union infer))
 
 (require (schemeunit))
 
diff --git a/collects/tests/typed-scheme/unit-tests/subst-tests.ss b/collects/tests/typed-scheme/unit-tests/subst-tests.ss
new file mode 100644
index 00000000..6c89d4ef
--- /dev/null
+++ b/collects/tests/typed-scheme/unit-tests/subst-tests.ss
@@ -0,0 +1,23 @@
+#lang scheme/base
+
+(require "test-utils.ss" (for-syntax scheme/base))
+(require (private planet-requires type-utils type-effect-convenience type-rep))
+(require (schemeunit))
+
+(define-syntax-rule (s img var tgt result)
+  (test-eq? "test" (substitute img 'var tgt) result))
+
+(define-syntax-rule (s... imgs var tgt result)
+  (test-eq? "test" (substitute-dots (list . imgs) 'var tgt) result))
+
+(define (subst-tests)
+  (test-suite "Tests for substitution"
+              (s N a (-v a) N)
+              (s... (N B) a (make-Function (list (make-arr-dots null N (-v a) 'a))) (N B . -> . N))
+              (s... (N B) a (make-Function (list (make-arr-dots (list -String) N (-v a) 'a))) (-String N B . -> . N))
+              (s... (N B) a (make-Function (list (make-arr-dots (list -String) N (-v b) 'a))) (-String (-v b) (-v b) . -> . N))
+              (s... (N B) a (make-Function (list (make-arr-dots (list -String) N (-v b) 'b))) 
+                    (make-Function (list (make-arr-dots (list -String) N (-v b) 'b))))))
+
+(define-go subst-tests)
+
diff --git a/collects/tests/typed-scheme/unit-tests/subtype-tests.ss b/collects/tests/typed-scheme/unit-tests/subtype-tests.ss
index 2f8f4506..f4bc9912 100644
--- a/collects/tests/typed-scheme/unit-tests/subtype-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/subtype-tests.ss
@@ -3,7 +3,7 @@
 (require "test-utils.ss")
 
 (require (private subtype type-rep type-effect-convenience 
-                  planet-requires init-envs type-environments union))
+                  planet-requires init-envs type-environments union infer infer-dummy))
 
 (require (schemeunit)
          (for-syntax scheme/base))
diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
index a3fe2ffe..a5263dd3 100644
--- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
@@ -11,7 +11,7 @@
                   type-name-env init-envs mutated-vars
                   effect-rep type-annotation type-utils)
          (for-syntax (private tc-utils typechecker base-env type-env))
-         (for-template (private base-env)))
+         (for-template (private base-env base-types)))
 (require (schemeunit))
 
 
@@ -35,7 +35,8 @@
   (syntax-case stx ()
     [(_ e)
      #`(parameterize ([delay-errors? #f]
-                      [current-namespace (namespace-anchor->namespace anch)])
+                      [current-namespace (namespace-anchor->namespace anch)]
+                      [orig-module-stx (quote-syntax e)])
          (let ([ex (expand 'e)])
            (find-mutated-vars ex)
            (tc-expr ex)))]))
@@ -157,17 +158,17 @@
                     (cond [(pair? x) 1]
                           [(null? x) 1]))
               -Integer]
-        [tc-e (lambda: ([x : Number] . [y : Number]) (car y)) (->* (list N) N N)]
-        [tc-e ((lambda: ([x : Number] . [y : Number]) (car y)) 3) N]
-        [tc-e ((lambda: ([x : Number] . [y : Number]) (car y)) 3 4 5) N]
-        [tc-e ((lambda: ([x : Number] . [y : Number]) (car y)) 3 4) N]
-        [tc-e (apply (lambda: ([x : Number] . [y : Number]) (car y)) 3 '(4)) N]
-        [tc-e (apply (lambda: ([x : Number] . [y : Number]) (car y)) 3 '(4 6 7)) N]
-        [tc-e (apply (lambda: ([x : Number] . [y : Number]) (car y)) 3 '()) N]
+        [tc-e (lambda: ([x : Number] . [y : Number *]) (car y)) (->* (list N) N N)]
+        [tc-e ((lambda: ([x : Number] . [y : Number *]) (car y)) 3) N]
+        [tc-e ((lambda: ([x : Number] . [y : Number *]) (car y)) 3 4 5) N]
+        [tc-e ((lambda: ([x : Number] . [y : Number *]) (car y)) 3 4) N]
+        [tc-e (apply (lambda: ([x : Number] . [y : Number *]) (car y)) 3 '(4)) N]
+        [tc-e (apply (lambda: ([x : Number] . [y : Number *]) (car y)) 3 '(4 6 7)) N]
+        [tc-e (apply (lambda: ([x : Number] . [y : Number *]) (car y)) 3 '()) N]
         
-        [tc-e (lambda: ([x : Number] . [y : Boolean]) (car y)) (->* (list N) B B)]
-        [tc-e ((lambda: ([x : Number] . [y : Boolean]) (car y)) 3) B]
-        [tc-e (apply (lambda: ([x : Number] . [y : Boolean]) (car y)) 3 '(#f)) B]
+        [tc-e (lambda: ([x : Number] . [y : Boolean *]) (car y)) (->* (list N) B B)]
+        [tc-e ((lambda: ([x : Number] . [y : Boolean *]) (car y)) 3) B]
+        [tc-e (apply (lambda: ([x : Number] . [y : Boolean *]) (car y)) 3 '(#f)) B]
         
         [tc-e (let: ([x : Number 3])
                     (when (number? x) #t))
@@ -222,7 +223,7 @@
                  (string-append "foo" (a v))))
          -String]
         
-        [tc-e (apply (plambda: (a) [x : a] x) '(5)) (-lst -Integer)]
+        [tc-e (apply (plambda: (a) [x : a *] x) '(5)) (-lst -Integer)]
         [tc-e (apply append (list '(1 2 3) '(4 5 6))) (-lst -Integer)]
         
         [tc-err ((case-lambda: [([x : Number]) x]
@@ -471,7 +472,7 @@
         
         ;; testing some primitives
         [tc-e (let ([app apply]
-                    [f (lambda: [x : Number] 3)])
+                    [f (lambda: [x : Number *] 3)])
                 (app f (list 1 2 3)))
               -Integer]
         [tc-e ((lambda () (call/cc (lambda: ([k : (Number -> (U))]) (if (read) 5 (k 10))))))
@@ -527,7 +528,7 @@
                   1)]
         
         [tc-e ((case-lambda:
-                [[x : Number] (+ 1 (car x))])
+                [[x : Number *] (+ 1 (car x))])
                5)
               N]
         #;
@@ -544,6 +545,43 @@
         
         [tc-e (list* 1 2 3) (-pair -Integer (-pair -Integer -Integer))]
         
+        [tc-err (apply append (list 1) (list 2) (list 3) (list (list 1) "foo"))]
+        [tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list 1))) (-lst -Integer)]
+        [tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list "foo"))) (-lst (Un -String -Integer))]
+        [tc-err (plambda: (b ...) [y : b ... b] (apply append (map list y)))]
+        [tc-e (plambda: (b ...) [y : (Listof Integer) ... b] (apply append y))
+              (-polydots (b) (->... (list) ((-lst -Integer) b) (-lst -Integer)))]
+        
+        [tc-err (plambda: (a ...) ([z : String] . [w : Number ... a])
+                          (apply (plambda: (b) ([x : Number] . [y : Number ... a]) x)
+                                 1 1 1 1 w))]
+        
+        [tc-err (plambda: (a ...) ([z : String] . [w : Number])
+                          (apply (plambda: (b) ([x : Number] . [y : Number ... a]) x)
+                                 1 w))]
+        
+        [tc-e (plambda: (a ...) ([z : String] . [w : Number ... a])
+                        (apply (plambda: (b ...) ([x : Number] . [y : Number ... b]) x)
+                               1 w))
+              (-polydots (a) ((list -String) (N a) . ->... . N))]
+        ;; instantiating non-dotted terms
+        [tc-e (inst (plambda: (a) ([x : a]) x) Integer)
+              (-Integer . -> . -Integer : (list (make-Latent-Var-True-Effect)) (list (make-Latent-Var-False-Effect)))]
+        [tc-e (inst (plambda: (a) [x : a *] (apply list x)) Integer)
+              ((list) -Integer . ->* . (-lst -Integer))]
+        
+        ;; instantiating dotted terms
+        [tc-e (inst (plambda: (a ...) [xs : a ... a] 3) Integer Boolean Integer)
+              (-Integer B -Integer . -> . -Integer)]
+        [tc-e (inst (plambda: (a ...) [xs : (a ... a -> Integer) ... a] 3) Integer Boolean Integer)
+              ((-Integer B -Integer . -> . -Integer)
+               (-Integer B -Integer . -> . -Integer)
+               (-Integer B -Integer . -> . -Integer)
+               . -> . -Integer)]
+        
+        [tc-e (plambda: (z x y ...) () (inst map z x y ... y))
+              (-polydots (z x y) (-> ((list ((list x) (y y) . ->... . z) (-lst x)) ((-lst y) y) . ->... . (-lst z))))]
+        
         ;; error tests
         [tc-err (#%variable-reference number?)]
         [tc-err (+ 3 #f)]
@@ -568,6 +606,49 @@
                              (add1 x)
                              12))]
         
+        [tc-e (filter integer? (list 1 2 3 'foo))
+              (-lst -Integer)]
+        
+        [tc-e (filter even? (filter integer? (list 1 2 3 'foo)))
+              (-lst -Integer)]
+        
+        [tc-err (plambda: (a ...) [as : a ... a]
+                          (apply fold-left (lambda: ([c : Integer] [a : Char] . [xs : a ... a]) c)
+                                 3 (list #\c) as))]
+        [tc-err (plambda: (a ...) [as : a ... a]
+                          (apply fold-left (lambda: ([c : Integer] [a : String] . [xs : a ... a]) c)
+                                 3 (list #\c) (map list as)))]
+        [tc-err (plambda: (a ...) [as : a ... a]
+                          (apply fold-left (lambda: ([c : Integer] [a : Char] . [xs : a ... a]) c)
+                                 3 (list #\c) (map list (map list as))))]
+        
+        [tc-e (plambda: (a ...) [as : a ... a]
+                        (apply fold-left (lambda: ([c : Integer] [a : Char] . [xs : a ... a]) c)
+                               3 (list #\c) (map list as)))
+              (-polydots (a) ((list) (a a) . ->... . -Integer))]
+        
+        ;; First is same as second, but with map explicitly instantiated.
+        [tc-e (plambda: (a ...) [ys : (a ... a -> Number) *]
+                (lambda: [zs : a ... a]
+                  ((inst map Number (a ... a -> Number))
+                   (lambda: ([y : (a ... a -> Number)])
+                     (apply y zs))
+                   ys)))
+              (-polydots (a) ((list) ((list) (a a) . ->... . N) . ->* . ((list) (a a) . ->... . (-lst N))))]
+        [tc-e (plambda: (a ...) [ys : (a ... a -> Number) *]
+                (lambda: [zs : a ... a]
+                  (map (lambda: ([y : (a ... a -> Number)])
+                         (apply y zs))
+                       ys)))
+              (-polydots (a) ((list) ((list) (a a) . ->... . N) . ->* . ((list) (a a) . ->... . (-lst N))))]
+        
+        ;; We need to make sure that even if a isn't free in the dotted type, that it gets replicated
+        ;; appropriately.
+        [tc-e (inst (plambda: (a ...) [ys : Number ... a]
+                              (apply + ys))
+                    Boolean String Number)
+              (N N N . -> . N)]
+        
         #;[tc-err (let: ([fact : (Number -> Number) (lambda: ([n : Number]) (if (zero? n) 1 (* n (fact (- n 1)))))])
                         (fact 20))]
         
@@ -575,7 +656,8 @@
         ))
   (test-suite
    "check-type tests"
-   (test-exn "Fails correctly" exn:fail:syntax? (lambda () (check-type #'here N B)))
+   (test-exn "Fails correctly" exn:fail:syntax? (lambda () (parameterize ([orig-module-stx #'here])
+                                                             (check-type #'here N B))))
    (test-not-exn "Doesn't fail on subtypes" (lambda () (check-type #'here N Univ)))
    (test-not-exn "Doesn't fail on equal types" (lambda () (check-type #'here N N)))
    )
diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 255b01f1..6faf49bf 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -1,11 +1,14 @@
+
 #lang scheme/base
 
 ;; these are libraries providing functions we add types to that are not in scheme/base
 (require
  "extra-procs.ss"
- (only-in scheme/list cons? take drop add-between last)
+ (only-in scheme/list cons? take drop add-between last filter-map)
+ (only-in rnrs/lists-6 fold-left)
  '#%paramz
- (only-in scheme/match/runtime match:error))
+ (only-in scheme/match/runtime match:error)
+ scheme/promise)
 
 
 
@@ -102,11 +105,8 @@
      [read (cl-> 
             [(-Port) -Sexp]
             [() -Sexp])]
-     [ormap (-poly (a b) ((-> a b) (-lst a) . -> . b))]
-     [andmap (-poly (a b c d e) 
-                    (cl->*
-                     ((-> a b) (-lst a) . -> . b)
-                     ((-> c d e) (-lst c) (-lst d) . -> . e)))]
+     [ormap (-polydots (a c b) (->... (list (->... (list a) (b b) c) (-lst a)) ((-lst b) b) c))]
+     [andmap (-polydots (a c b) (->... (list (->... (list a) (b b) c) (-lst a)) ((-lst b) b) c))]
      [newline (cl-> [() -Void]
                     [(-Port) -Void])]
      [not (-> Univ B)]
@@ -125,16 +125,14 @@
      [list? (make-pred-ty (-lst Univ))]
      [list (-poly (a) (->* '() a (-lst a)))]
      [procedure? (make-pred-ty (make-Function (list (make-top-arr))))]
-     [map 
-      (-poly (a b c d)
-             (cl-> [((-> a b) (-lst a)) (-lst b)]
-                   [((-> a b c) (-lst a) (-lst b)) (-lst c)]
-                   [((-> a b c d) (-lst a) (-lst b) (-lst c)) (-lst d)]))]
-     [for-each 
-      (-poly (a b c d)
-             (cl-> [((-> a b) (-lst a)) -Void]
-                   [((-> a b c) (-lst a) (-lst b)) -Void]
-                   [((-> a b c d) (-lst a) (-lst b) (-lst c)) -Void]))]
+     [map (-polydots (c a b) ((list ((list a) (b b) . ->... . c) (-lst a))
+                              ((-lst b) b) . ->... .(-lst c)))]
+     [for-each (-polydots (c a b) ((list ((list a) (b b) . ->... . Univ) (-lst a))
+                                   ((-lst b) b) . ->... . -Void))]
+     [fold-left (-polydots (c a b) ((list ((list c a) (b b) . ->... . c) c (-lst a))
+                                    ((-lst b) b) . ->... . c))]
+     [fold-right (-polydots (c a b) ((list ((list c a) (b b) . ->... . c) c (-lst a))
+                                     ((-lst b) b) . ->... . c))]
      [foldl
       (-poly (a b c)
              (cl-> [((a b . -> . b) b (make-lst a)) b]
@@ -149,6 +147,11 @@
                             . -> .
                             (-lst b))
                            ((a . -> . B) (-lst a) . -> . (-lst a))))]
+     [filter-map (-polydots (c a b)
+                            ((list
+                              ((list a) (b b) . ->... . (-opt c))
+                              (-lst a))
+                             ((-lst b) b) . ->... . (-lst c)))]
      [take   (-poly (a) ((-lst a) -Integer . -> . (-lst a)))]
      [drop   (-poly (a) ((-lst a) -Integer . -> . (-lst a)))]
      [last   (-poly (a) ((-lst a) . -> . a))]
@@ -258,8 +261,8 @@
                  [(-Pathlike (-> a) Sym) a]))]
      
      [random (cl->
-              [(N) N]
-              [() N])]
+              [(-Integer) -Integer]
+              [() -Integer])]
      
      [assoc (-poly (a b) (a (-lst (-pair a b)) . -> . (-opt (-pair a b))))]
      [assf  (-poly (a b)
@@ -339,15 +342,15 @@
      [imag-part (N . -> . N)]
      [magnitude (N . -> . N)]
      [angle (N . -> . N)]
-     [numerator (N . -> . N)]
-     [denominator (N . -> . N)]
+     [numerator (N . -> . -Integer)]
+     [denominator (N . -> . -Integer)]
      [exact->inexact (N . -> . N)]
      [inexact->exact (N . -> . N)]
      [make-string
       (cl->
        [(N) -String]
        [(N -Char) -String])]
-     [arithmetic-shift (N N . -> . N)]
+     [arithmetic-shift (-Integer -Integer . -> . -Integer)]
      [abs (N . -> . N)]
      [substring (cl-> [(-String N) -String]
                       [(-String N N) -String])]
@@ -377,7 +380,7 @@
      [current-error-port (-Param -Output-Port -Output-Port)]
      [current-input-port (-Param -Input-Port -Input-Port)]
      [round (N . -> . N)]
-     [seconds->date (N . -> . (make-Struct 'date #f (list N N N N N N N N B N) #f #f #'date? values))]
+     [seconds->date (N . -> . (make-Name #'date))]
      [current-seconds (-> N)]
      [sqrt (-> N N)]
      [path->string (-> -Path -String)]       
@@ -418,17 +421,16 @@
                  [(-Input-Port Sym) -String])]
      [copy-file (-> -Pathlike -Pathlike -Void)]  
      [bytes->string/utf-8 (-> -Bytes -String)]
+     
      ;; language
      [(expand '(this-language))
       Sym
       string-constants/string-constant]
-     ;; make-promise 
-     
+     ;; make-promise      
      [(cadr (syntax->list (expand '(delay 3))))
       (-poly (a) (-> (-> a) (-Promise a)))
       scheme/promise]
-     ;; qq-append
-     
+     ;; qq-append     
      [(cadr (syntax->list (expand '`(,@'() 1)))) 
       (-poly (a b) 
              (cl->*
@@ -485,6 +487,7 @@
      [delete-file (-> -Pathlike -Void)]
      [make-namespace (cl->* (-> -Namespace)
                             (-> (*Un (-val 'empty) (-val 'initial)) -Namespace))]
+     [make-base-namespace (-> -Namespace)]
      [eval (-> -Sexp Univ)]
      
      [exit (-> (Un))]
@@ -509,6 +512,9 @@
      [syntax? (make-pred-ty (-Syntax Univ))]
      [syntax-property (-poly (a) (cl->* (-> (-Syntax a) Univ Univ (-Syntax a))
                                         (-> (-Syntax Univ) Univ Univ)))]
+     
+     [values* (-polydots (a) (null (a a) . ->... . (make-ValuesDots null a 'a)))]
+     [call-with-values* (-polydots (b a) ((-> (make-ValuesDots null a 'a)) (null (a a) . ->... . b) . -> .  b))]
      )))
 
 (begin-for-syntax 
diff --git a/collects/typed-scheme/private/extra-procs.ss b/collects/typed-scheme/private/extra-procs.ss
index b8b87b6c..83aa9c40 100644
--- a/collects/typed-scheme/private/extra-procs.ss
+++ b/collects/typed-scheme/private/extra-procs.ss
@@ -1,7 +1,18 @@
 #lang scheme/base
-(provide assert)    
+(provide assert call-with-values* values*)
 
 (define (assert v)
   (unless v
     (error "Assertion failed - value was #f"))
   v)
+
+(define (fold-right f c as . bss)
+  (if (or (null? as)
+          (ormap null? bss))
+      c
+      (apply f
+             (apply fold-right f c (cdr as) (map cdr bss))
+             (car as) (map car bss))))
+
+(define call-with-values* call-with-values)
+(define values* values)
\ No newline at end of file
diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss
index 72e51cd5..b8e08515 100644
--- a/collects/typed-scheme/private/parse-type.ss
+++ b/collects/typed-scheme/private/parse-type.ss
@@ -24,7 +24,6 @@
 
 (define (stx-cadr stx) (stx-car (stx-cdr stx)))
 
-
 (define (parse-type stx)    
   (parameterize ([current-orig-stx stx])
     (syntax-case* stx ()
@@ -74,33 +73,58 @@
          (make-pred-ty (list (parse-type #'dom)) (parse-type #'rng) (parse-type #'pred-ty)))]
       [(dom ... rest ::: -> rng)
        (and (eq? (syntax-e #'->) '->) 
-            (or (symbolic-identifier=? #'::: (quote-syntax ..))
-                (symbolic-identifier=? #'::: (quote-syntax ...))))
+            (eq? (syntax-e #':::) '*))
        (begin
          (add-type-name-reference #'->)
          (->* (map parse-type (syntax->list #'(dom ...))) (parse-type #'rest) (parse-type #'rng)))]
+      [(dom ... rest ::: bound -> rng)
+       (and (eq? (syntax-e #'->) '->) 
+            (eq? (syntax-e #':::) '...)
+            (identifier? #'bound))
+       (begin
+         (add-type-name-reference #'->)
+         (let ([var (lookup (current-tvars) (syntax-e #'bound) (lambda (_) #f))])
+           (if (not (Dotted? var))
+               (tc-error/stx #'bound "Used a type variable (~a) not bound with ... as a bound on a ..." (syntax-e #'bound))
+               (make-Function
+                (list
+                 (make-arr-dots (map parse-type (syntax->list #'(dom ...)))
+                                (parse-type #'rng)
+                                (parameterize ([current-tvars (extend-env (list (syntax-e #'bound)) 
+                                                                          (list (make-DottedBoth (make-F (syntax-e #'bound))))
+                                                                          (current-tvars))])
+                                  (parse-type #'rest))
+                                (syntax-e #'bound)))))))]
       ;; has to be below the previous one
       [(dom ... -> rng) 
        (eq? (syntax-e #'->) '->)
        (begin
          (add-type-name-reference #'->)
          (->* (map parse-type (syntax->list #'(dom ...))) (parse-type #'rng)))]
+      [(values tys ... dty dd bound)
+       (and (eq? (syntax-e #'dd) '...)
+            (identifier? #'bound)
+            (eq? (syntax-e #'values) 'values))
+       (let ([var (lookup (current-tvars) (syntax-e #'bound) (lambda (_) #f))])
+         (if (not (Dotted? var))
+             (tc-error/stx #'bound "Used a type variable (~a) not bound with ... as a bound on a ..." (syntax-e #'bound))             
+             (make-ValuesDots (map parse-type (syntax->list #'(tys ...)))
+                              (parameterize ([current-tvars (extend-env (list (syntax-e #'bound)) 
+                                                                        (list (make-DottedBoth (make-F (syntax-e #'bound))))
+                                                                        (current-tvars))])
+                                (parse-type #'dty))
+                              (syntax-e #'bound))))]
       [(values tys ...) 
        (eq? (syntax-e #'values) 'values)
        (-values (map parse-type (syntax->list #'(tys ...))))]
       [(case-lambda tys ...) 
        (eq? (syntax-e #'case-lambda) 'case-lambda)
-       (make-Function (map (lambda (ty) 
-                             (syntax-case* ty (->) symbolic-identifier=?
-                               [(dom ... -> rng)
-                                (make-arr 
-                                 (map parse-type (syntax->list #'(dom ...))) 
-                                 (parse-type #'rng))]))
-                           (syntax->list #'(tys ...))))]
-      ;; I wish I could write this
-      #;[(case-lambda ([dom ... -> rng] ...)) (make-funty (list (make-arr (list (parse-type #'dom) ...) (parse-type #'rng)) ...))]
-      #;[(list-of t) (make-lst (parse-type #'t))]
-      #;[(Listof t) (make-lst (parse-type #'t))]
+       (make-Function 
+        (for/list ([ty (syntax->list #'(tys ...))])
+          (let ([t (parse-type ty)])
+            (match t
+              [(Function: (list arr)) arr]
+              [_ (tc-error/stx ty "Component of case-lambda type was not a function clause")]))))]
       [(Vectorof t) 
        (eq? (syntax-e #'Vectorof) 'Vectorof)
        (begin
@@ -129,14 +153,27 @@
       [(quot t)
        (eq? (syntax-e #'quot) 'quote)
        (-val (syntax-e #'t))]
+      [(All (vars ... v dd) t)
+       (and (or (eq? (syntax-e #'All) 'All)
+                (eq? (syntax-e #'All) '∀))
+            (eq? (syntax-e #'dd) '...)
+            (andmap identifier? (syntax->list #'(v vars ...))))
+       (let* ([vars (map syntax-e (syntax->list #'(vars ...)))]
+              [tvars (map make-F vars)]
+              [v (syntax-e #'v)]
+              [tv (make-Dotted (make-F v))])
+         (add-type-name-reference #'All)
+         (parameterize ([current-tvars (extend-env (cons v vars) (cons tv tvars) (current-tvars))])
+           (make-PolyDots (append vars (list v)) (parse-type #'t))))]
       [(All (vars ...) t) 
-       (and (eq? (syntax-e #'All) 'All)
+       (and (or (eq? (syntax-e #'All) 'All)
+                (eq? (syntax-e #'All) '∀))
             (andmap identifier? (syntax->list #'(vars ...))))
        (let* ([vars (map syntax-e (syntax->list #'(vars ...)))]
               [tvars (map make-F vars)])
          (add-type-name-reference #'All)
          (parameterize ([current-tvars (extend-env vars tvars (current-tvars))])
-           (make-Poly vars (parse-type #'t))))]        
+           (make-Poly vars (parse-type #'t))))]
       [(Opaque p?) 
        (eq? (syntax-e #'Opaque) 'Opaque)
        (begin
@@ -157,7 +194,12 @@
        (identifier? #'id)
        (cond 
          ;; if it's a type variable, we just produce the corresponding reference (which is in the HT)
-         [(lookup (current-tvars) (syntax-e #'id) (lambda (_) #f))]
+         [(lookup (current-tvars) (syntax-e #'id) (lambda (_) #f))
+          =>
+          (lambda (e) (cond [(DottedBoth? e) (Dotted-t e)]
+                            [(Dotted? e)
+                             (tc-error "Type variable ~a must be used with ..." (syntax-e #'id))]
+                            [else e]))]
          ;; if it's a type alias, we expand it (the expanded type is stored in the HT)
          [(lookup-type-alias #'id parse-type (lambda () #f))
           =>
diff --git a/collects/typed-scheme/private/prims.ss b/collects/typed-scheme/private/prims.ss
index 7d051062..f94b97b5 100644
--- a/collects/typed-scheme/private/prims.ss
+++ b/collects/typed-scheme/private/prims.ss
@@ -93,37 +93,51 @@ This file defines two sorts of primitives. All of them are provided into any mod
            #,(syntax-property #'(require/contract pred pred-cnt lib)
                               'typechecker:ignore #t))))]))
 
+(define-for-syntax (formal-annotation-error stx src)
+  (let loop ([stx stx])
+    (syntax-case stx ()
+      ;; should never happen
+      [() (raise-syntax-error #f "bad annotation syntax" src stx)]
+      [[var : ty]
+       (identifier? #'var)
+       (raise-syntax-error #f "expected dotted or starred type" src #'ty)]
+      [([var : ty] . rest)
+       (identifier? #'var)
+       (loop #'rest)]
+      [([var : ty] . rest)
+       (raise-syntax-error #f "not a variable" src #'var)]
+      [(e . rest)
+       (raise-syntax-error #f "expected annotated variable of the form [x : T], got something else" src #'e)])))
+
 (define-for-syntax (types-of-formals stx src)
   (syntax-case stx (:)
     [([var : ty] ...) (quasisyntax/loc stx (ty ...))]
-    [([var : ty] ... . [rest : rest-ty]) (syntax/loc stx (ty ... rest-ty ..))]
-    [_
-     (let loop ([stx stx])
-       (syntax-case stx ()
-         ;; should never happen
-         [() (raise-syntax-error #f "bad annotation syntax" src stx)]
-         [([var : ty] . rest)
-          (identifier? #'var)
-          (loop #'rest)]
-         [([var : ty] . rest)
-          (raise-syntax-error #f "not a variable" src #'var)]
-         [(e . rest)
-          (raise-syntax-error #f "expected annotated variable of the form [x : T], got something else" src #'e)]))]))
+    [([var : ty] ... . [rest : rest-ty star])
+     (eq? '* (syntax-e #'star))
+     (syntax/loc stx (ty ... rest-ty star))]
+    [([var : ty] ... . [rest : rest-ty ddd bound])
+     (eq? '... (syntax-e #'ddd))
+     (syntax/loc stx (ty ... rest-ty ddd bound))]
+    [_ (formal-annotation-error stx src)]))
 
 
 (define-syntax (plambda: stx)
   (syntax-case stx ()
     [(plambda: (tvars ...) formals . body)
-     (syntax-property #'(lambda: formals . body)
-                      'typechecker:plambda
-                      #'(tvars ...))]))
+     (quasisyntax/loc stx
+       (#%expression
+        #,(syntax-property (syntax/loc stx (lambda: formals . body))
+                           'typechecker:plambda
+                           #'(tvars ...))))]))
 
 (define-syntax (pcase-lambda: stx)
   (syntax-case stx ()
     [(pcase-lambda: (tvars ...) cl ...)
-     (syntax-property #'(case-lambda: cl ...)
-                      'typechecker:plambda
-                      #'(tvars ...))]))
+     (quasisyntax/loc stx
+       (#%expression
+        #,(syntax-property (syntax/loc stx (case-lambda: cl ...))
+                           'typechecker:plambda
+                           #'(tvars ...))))]))
 
 (define-syntax (pdefine: stx)
   (syntax-case stx (:)
@@ -163,8 +177,11 @@ This file defines two sorts of primitives. All of them are provided into any mod
 
 (define-syntax (inst stx)
   (syntax-case stx (:)
-    [(_ arg : tys ...)
-     (syntax-property #'arg 'type-inst #'(tys ...))]
+    [(_ arg : . tys)
+     (syntax/loc stx (inst arg . tys))]    
+    [(_ arg tys ... ty ddd b)
+     (eq? (syntax-e #'ddd) '...)
+     (syntax-property #'arg 'type-inst #'(tys ... (ty . b)))]
     [(_ arg tys ...)
      (syntax-property #'arg 'type-inst #'(tys ...))]))
 
@@ -191,32 +208,41 @@ This file defines two sorts of primitives. All of them are provided into any mod
 
 
 ;; helper function for annoating the bound names
-(define-for-syntax (annotate-names stx)
+(define-for-syntax (annotate-names stx src)
   (define (label-one var ty)
     (syntax-property var 'type-label ty))
   (define (label vars tys)
     (map label-one
          (syntax->list vars)
          (syntax->list tys)))
+  (define (label-dotted var ty bound)
+    (syntax-property (syntax-property var 'type-ascription ty)
+                      'type-dotted 
+                      bound))
   (syntax-case stx (:)
-    [[var : ty] (label-one #'var #'ty)]
     [([var : ty] ...)
      (label #'(var ...) #'(ty ...))]
-    [([var : ty] ... . [rest : rest-ty])
-     (append (label #'(var ...) #'(ty ...)) (label-one #'rest #'rest-ty))]))       
+    [([var : ty] ... . [rest : rest-ty star])
+     (eq? '* (syntax-e #'star))
+     (append (label #'(var ...) #'(ty ...)) (label-one #'rest #'rest-ty))]
+    [([var : ty] ... . [rest : rest-ty ddd bound])
+     (eq? '... (syntax-e #'ddd))
+     (append (label #'(var ...) #'(ty ...)) (label-dotted #'rest #'rest-ty #'bound))]
+    [_ (formal-annotation-error stx src)]))
 
 (define-syntax-rule (λ: . args) (lambda: . args))
 
 (define-syntax (lambda: stx)
   (syntax-case stx (:)
     [(lambda: formals . body)
-     (with-syntax ([labeled-formals (annotate-names #'formals)])
+     (with-syntax ([labeled-formals (annotate-names #'formals stx)])
        (syntax/loc stx (lambda labeled-formals . body)))]))
 
 (define-syntax (case-lambda: stx)
   (syntax-case stx (:)
     [(case-lambda: [formals . body] ...)
-     (with-syntax ([(lab-formals ...) (map annotate-names (syntax->list #'(formals ...)))])
+     (with-syntax ([(lab-formals ...) (map (lambda (s) (annotate-names s stx))
+                                           (syntax->list #'(formals ...)))])
        (syntax/loc stx (case-lambda [lab-formals . body] ...)))]))
 
 (define-syntaxes (let-internal: let*: letrec:)
@@ -224,7 +250,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
               (lambda (stx)
                 (syntax-case stx (:)
                   [(_ ([nm : ty . exprs] ...) . body)
-                   (with-syntax* ([(vars ...) (annotate-names #'([nm : ty] ...))]
+                   (with-syntax* ([(vars ...) (annotate-names #'([nm : ty] ...) stx)]
                                   [bindings (map (lambda (v e loc)
                                                    (quasisyntax/loc loc [#,v . #,e]))
                                                  (syntax->list #'(vars ...))
@@ -279,10 +305,13 @@ This file defines two sorts of primitives. All of them are provided into any mod
 (define-syntax (define-typed-struct stx)
   (syntax-case stx (:)
     [(_ nm ([fld : ty] ...) . opts)
-     (with-syntax ([d-s (syntax-property (syntax/loc stx (define-struct nm (fld ...) . opts))
-                                         'typechecker:ignore #t)]
-                   [dtsi (internal (syntax/loc stx (define-typed-struct-internal nm ([fld : ty] ...))))])
-       #'(begin d-s dtsi))]
+     (let ([mutable (if (memq '#:mutable (syntax->datum #'opts))
+                        '(#:mutable)
+                        '())])
+       (with-syntax ([d-s (syntax-property (syntax/loc stx (define-struct nm (fld ...) . opts))
+                                           'typechecker:ignore #t)]
+                     [dtsi (internal (quasisyntax/loc stx (define-typed-struct-internal nm ([fld : ty] ...) #,@mutable)))])
+         #'(begin d-s dtsi)))]
     [(_ (vars ...) nm ([fld : ty] ...) . opts)
      (with-syntax ([d-s (syntax-property (syntax/loc stx (define-struct nm (fld ...) . opts))
                                          'typechecker:ignore #t)]
diff --git a/collects/typed-scheme/private/remove-intersect.ss b/collects/typed-scheme/private/remove-intersect.ss
index 616fbb8e..f9b273e8 100644
--- a/collects/typed-scheme/private/remove-intersect.ss
+++ b/collects/typed-scheme/private/remove-intersect.ss
@@ -1,6 +1,6 @@
 #lang scheme/base
 
-(require "type-rep.ss" "unify.ss" "union.ss" "infer.ss" "subtype.ss"
+(require "type-rep.ss" "union.ss" "subtype.ss"
          "type-utils.ss" "resolve-type.ss" "type-effect-convenience.ss"         
          mzlib/plt-match mzlib/trace)
 
diff --git a/collects/typed-scheme/private/resolve-type.ss b/collects/typed-scheme/private/resolve-type.ss
index 28385b80..d68de692 100644
--- a/collects/typed-scheme/private/resolve-type.ss
+++ b/collects/typed-scheme/private/resolve-type.ss
@@ -1,7 +1,7 @@
 #lang scheme/base
 
 (require "type-rep.ss"  "type-name-env.ss" "tc-utils.ss"
-         "type-utils.ss" 
+         "type-utils.ss"
          mzlib/plt-match
          mzlib/trace)
 
diff --git a/collects/typed-scheme/private/subtype.ss b/collects/typed-scheme/private/subtype.ss
index f2114838..398fe7b2 100644
--- a/collects/typed-scheme/private/subtype.ss
+++ b/collects/typed-scheme/private/subtype.ss
@@ -1,11 +1,12 @@
 #lang scheme/base
 
-(require "type-rep.ss" "unify.ss" "type-utils.ss"
+(require (except-in "type-rep.ss" sub-eff) "type-utils.ss"
          "tc-utils.ss"
          "effect-rep.ss"
          "type-comparison.ss"
          "resolve-type.ss"
          "type-name-env.ss"
+         (only-in "infer-dummy.ss" unify)
          mzlib/plt-match
          mzlib/trace)
 
@@ -99,10 +100,10 @@
     (match (list s t)
       ;; top for functions is above everything
       [(list _ (top-arr:)) A0]
-      [(list (arr: s1 s2 #f thn-eff els-eff) (arr: t1 t2 #f thn-eff  els-eff))
+      [(list (arr: s1 s2 #f #f thn-eff els-eff) (arr: t1 t2 #f #f thn-eff  els-eff))
        (let ([A1 (subtypes* A0 t1 s1)])
          (subtype* A1 s2 t2))]
-      [(list (arr: s1 s2 s3 thn-eff els-eff) (arr: t1 t2 t3 thn-eff* els-eff*))
+      [(list (arr: s1 s2 s3 #f thn-eff els-eff) (arr: t1 t2 t3 #f thn-eff* els-eff*))
        (unless 
            (or (and (null? thn-eff*) (null? els-eff*))
                (and (effects-equal? thn-eff thn-eff*)
@@ -200,7 +201,7 @@
               ;; use unification to see if we can use the polytype here
               [(list (Poly: vs b) s)
                (=> unmatch)
-               (if (unify1 s b) A0 (unmatch))]
+               (if (unify vs (list b) (list s)) A0 (unmatch))]              
               [(list s (Poly: vs b))
                (=> unmatch)
                (if (null? (fv b)) (subtype* A0 s b) (unmatch))]
diff --git a/collects/typed-scheme/private/type-annotation.ss b/collects/typed-scheme/private/type-annotation.ss
index d9875ef4..1a72e73b 100644
--- a/collects/typed-scheme/private/type-annotation.ss
+++ b/collects/typed-scheme/private/type-annotation.ss
@@ -8,11 +8,14 @@
          get-type/infer
          type-label-symbol
          type-ascrip-symbol
+         type-dotted-symbol
          type-ascription
-         check-type)
+         check-type
+         dotted?)
 
 (define type-label-symbol 'type-label)
-(define type-ascrip-symbol 'type-ascription)    
+(define type-ascrip-symbol 'type-ascription)
+(define type-dotted-symbol 'type-dotted)
 
 (define (print-size stx)
   (syntax-case stx ()
@@ -27,7 +30,7 @@
 ;; is let-binding really necessary? - remember to record the bugs!
 (define (type-annotation stx #:infer [let-binding #f])
   (define (pt prop)
-    (print-size prop)
+    #;(print-size prop)
     (if (syntax? prop)
         (parse-type prop)
         (parse-type/id stx prop)))
@@ -48,7 +51,7 @@
 
 (define (type-ascription stx)
   (define (pt prop)
-    (print-size prop)
+    #;(print-size prop)
     (if (syntax? prop)
         (parse-type prop)
         (parse-type/id stx prop)))
@@ -69,10 +72,7 @@
   (parameterize
       ([current-orig-stx stx])
     (cond
-      [(type-annotation stx #:infer #t)
-       => (lambda (x) 
-            (log/ann stx x)
-            x)]
+      [(type-annotation stx #:infer #t)]
       [(not (syntax-original? stx))
        (tc-error "untyped var: ~a" (syntax-e stx))]
       [else
@@ -103,8 +103,8 @@
                                       "Expression should produce ~a values, but produces ~a values of types ~a"
                                       (length stxs) (length tys) (stringify tys))
                     (map (lambda (stx ty a)
-                           (cond [a => (lambda (ann) (check-type stx ty ann) (log/extra stx ty ann) ann)]
-                                 [else (log/noann stx ty) ty]))
+                           (cond [a => (lambda (ann) (check-type stx ty ann) #;(log/extra stx ty ann) ann)]
+                                 [else #;(log/noann stx ty) ty]))
                          stxs tys anns))]
                [ty (tc-error/delayed #:ret (map (lambda _ (Un)) stxs) 
                                      "Expression should produce ~a values, but produces one values of type "
@@ -121,3 +121,7 @@
       (unless (subtype e-type ty)
         ;(printf "orig-stx: ~a" (syntax->datum stx*))
         (tc-error "Body had type:~n~a~nVariable had type:~n~a~n" e-type ty)))))
+
+(define (dotted? stx)
+  (cond [(syntax-property stx type-dotted-symbol) => syntax-e]
+        [else #f]))
\ No newline at end of file
diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss
index e09caee9..9ae26d54 100644
--- a/collects/typed-scheme/private/type-effect-convenience.ss
+++ b/collects/typed-scheme/private/type-effect-convenience.ss
@@ -13,7 +13,6 @@
 
 (provide (all-defined-out))
 
-
 (define (-vet id) (make-Var-True-Effect id))
 (define (-vef id) (make-Var-False-Effect id))
 
@@ -36,12 +35,15 @@
     [(False-Effect:) eff]
     [_ (error 'internal-tc-error "can't add var to effect ~a" eff)]))
 
-(define-syntax ->
-  (syntax-rules (:)
+(define-syntax (-> stx)
+  (syntax-case* stx (:) (lambda (a b) (eq? (syntax-e a) (syntax-e b)))
     [(_ dom ... rng : eff1 eff2)
-     (->* (list dom ...) rng : eff1 eff2)]
+     #'(->* (list dom ...) rng : eff1 eff2)]
+    [(_ dom ... rng : eff1 eff2)
+     #'(->* (list dom ...) rng : eff1 eff2)]
     [(_ dom ... rng)
-     (->* (list dom ...) rng)]))
+     #'(->* (list dom ...) rng)]))
+
 (define-syntax ->*
   (syntax-rules (:)
     [(_ dom rng)       
@@ -52,6 +54,16 @@
      (make-Function (list (make-arr* dom rng #f eff1 eff2)))]
     [(_ dom rst rng : eff1 eff2)
      (make-Function (list (make-arr* dom rng rst eff1 eff2)))]))
+(define-syntax ->...
+  (syntax-rules (:)
+    [(_ dom rng)
+     (->* dom rng)]
+    [(_ dom (dty dbound) rng)
+     (make-Function (list (make-arr* dom rng #f (cons dty 'dbound) (list) (list))))]
+    [(_ dom rng : eff1 eff2)
+     (->* dom rng : eff1 eff2)]
+    [(_ dom (dty dbound) rng : eff1 eff2)
+     (make-Function (list (make-arr* dom rng #f (cons dty 'dbound) eff1 eff2)))]))
 (define-syntax cl->
   (syntax-rules (:)
     [(_ [(dom ...) rng] ...)
@@ -68,8 +80,12 @@
 
 (define make-arr*
   (case-lambda [(dom rng) (make-arr* dom rng #f (list) (list))]
-               [(dom rng rest) (make-arr dom rng rest (list) (list))]
-               [(dom rng rest eff1 eff2) (make-arr dom rng rest eff1 eff2)]))
+               [(dom rng rest) (make-arr dom rng rest #f (list) (list))]
+               [(dom rng rest eff1 eff2) (make-arr dom rng rest #f eff1 eff2)]
+               [(dom rng rest drest eff1 eff2) (make-arr dom rng rest drest eff1 eff2)]))
+
+(define (make-arr-dots dom rng dty dbound)
+  (make-arr* dom rng #f (cons dty dbound) null null))
 
 (define (make-promise-ty t)
   (make-Struct (string->uninterned-symbol "Promise") #f (list t) #f #f #'promise? values))
@@ -110,6 +126,13 @@
      (let ([vars (-v vars)] ...)
        (make-Poly (list 'vars ...) ty))]))
 
+(define-syntax -polydots
+  (syntax-rules ()
+    [(_ (vars ... dotted) ty)
+     (let ([dotted (-v dotted)]
+           [vars (-v vars)] ...)
+       (make-PolyDots (list 'vars ... 'dotted) ty))]))
+
 (define-syntax -mu
   (syntax-rules ()
     [(_ var ty)
@@ -119,12 +142,6 @@
 
 (define -values make-Values)
 
-;; produce the appropriate type of a list of types
-;; that is - if there is exactly one type, just produce it, otherwise produce a values-ty
-;; list[type] -> type
-(define (list->values-ty l)
-  (if (= 1 (length l)) (car l) (-values l)))
-
 (define-syntax *Un
   (syntax-rules ()
     [(_ . args) (make-Union (list . args))]))
@@ -143,9 +160,10 @@
 (define -Sexp (-mu x (*Un Sym N B -String (-val null) (-pair x x))))
 (define -Port (*Un -Input-Port -Output-Port))
 
-(define (-lst* . args) (if (null? args)
-                           (-val null)
-                           (-pair (car args) (apply -lst* (cdr args)))))
+(define (-lst* #:tail [tail (-val null)] . args)
+  (if (null? args)
+      tail
+      (-pair (car args) (apply -lst* #:tail tail (cdr args)))))
 
 
 #;(define NE (-mu x (Un N (make-Listof x))))
@@ -197,17 +215,19 @@
                      (identifier? #'nm)
                      #`(list  #'nm ty)]
                     [(e ty extra-mods ...)
-                     #'(list (let ([new-ns
-                                    (let* ([ns (make-empty-namespace)])
-                                      (namespace-attach-module (current-namespace)
-                                                               'scheme/base
-                                                               ns)
-                                      ns)])
-                               (parameterize ([current-namespace new-ns])
-                                 (namespace-require 'scheme/base)
-                                 (namespace-require 'extra-mods) ...
-                                 e))
-                             ty)]))
+                     #'(let ([x (list (let ([new-ns
+                                             (let* ([ns (make-empty-namespace)])
+                                               (namespace-attach-module (current-namespace)
+                                                                        'scheme/base
+                                                                        ns)
+                                               ns)])
+                                        (parameterize ([current-namespace new-ns])
+                                          (namespace-require 'scheme/base)
+                                          (namespace-require 'extra-mods) ...
+                                          e))
+                                      ty)])
+                         ;(display x) (newline)
+                         x)]))
                 (syntax->list #'(e ...))))]))
 
 ;; if t is of the form (Pair t* (Pair t* ... (Listof t*)))
@@ -227,8 +247,5 @@
                (exit t)))]
         [_ (exit t)]))))
 
-(define (tc-error/expr msg #:return [return (Un)] #:stx [stx (current-orig-stx)] . rest)
-  (tc-error/delayed #:stx stx (apply format msg rest))
-  return)
 
 
diff --git a/collects/typed-scheme/private/type-effect-printer.ss b/collects/typed-scheme/private/type-effect-printer.ss
index 22cccaab..b4fbcc44 100644
--- a/collects/typed-scheme/private/type-effect-printer.ss
+++ b/collects/typed-scheme/private/type-effect-printer.ss
@@ -46,11 +46,13 @@
     (match a
       [(top-arr:)
        (fp "Procedure")]
-      [(arr: dom rng rest thn-eff els-eff)
+      [(arr: dom rng rest drest thn-eff els-eff)
        (fp "(")
        (for-each (lambda (t) (fp "~a " t)) dom)
        (when rest
-         (fp "~a .. " rest))
+         (fp "~a* " rest))
+       (when drest
+         (fp "~a ... ~a " (car drest) (cdr drest)))
        (fp "-> ~a" rng)
        (unless (and (null? thn-eff) (null? els-eff))
          (fp " : ~a ~a" thn-eff els-eff))
@@ -64,7 +66,6 @@
     (match t
       [(Pair: a e) (cons a (tuple-elems e))]
       [(Value: '()) null]))
-  ;(fp "~a~n" (Type-seq c))
   (match c 
     [(Univ:) (fp "Any")]
     [(? has-name?) (fp "~a" (has-name? c))]
@@ -95,24 +96,33 @@
        (match arities
          [(list) (fp "(case-lambda)")]
          [(list a) (print-arr a)]
-         [(list a ...) (fp "(case-lambda ") (for-each print-arr a) (fp ")")]))]
-    [(arr: _ _ _ _ _) (print-arr c)]
+         [(list a b ...) (fp "(case-lambda ")
+                         (print-arr a) 
+                         (for-each 
+                          (lambda (e) (fp " ") (print-arr e))
+                          b)
+                         (fp ")")]))]
+    [(arr: _ _ _ _ _ _) (print-arr c)]
     [(Vector: e) (fp "(Vectorof ~a)" e)]
     [(Box: e) (fp "(Box ~a)" e)]
     [(Union: elems) (fp "~a" (cons 'U elems))]
     [(Pair: l r) (fp "(Pair ~a ~a)" l r)]
-    [(F: nm) (fp "<~a>" nm)]      
+    [(F: nm) (fp "~a" nm)]      
     [(Values: (list v ...)) (fp "~a" (cons 'values v))]
+    [(ValuesDots: v dty dbound) (fp "~a" (cons 'values (append v (list dty '... dbound))))]
     [(Param: in out) 
      (if (equal? in out)
          (fp "(Parameter ~a)" in)           
          (fp "(Parameter ~a ~a)" in out))]
     [(Hashtable: k v) (fp "(HashTable ~a ~a)" k v)]
-    #;
-    [(Poly-unsafe: n b) (fp "(unsafe-poly ~a ~a ~a)" (Type-seq c) n b)]
+    
+    #;[(Poly-unsafe: n b) (fp "(unsafe-poly ~a ~a ~a)" (Type-seq c) n b)]
     [(Poly-names: names body) 
      #;(fprintf (current-error-port) "POLY SEQ: ~a~n" (Type-seq body))
      (fp "(All ~a ~a)" names body)]
+    #;[(PolyDots-unsafe: n b) (fp "(unsafe-polydots ~a ~a ~a)" (Type-seq c) n b)]
+    [(PolyDots-names: (list names ... dotted) body)
+     (fp "(All ~a ~a)" (append names (list dotted '...)) body)]
     #;
     [(Mu-unsafe: b) (fp "(unsafe-mu ~a ~a)" (Type-seq c) b)]
     [(Mu: x (Syntax: (Union: (list
diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index 2d402e11..80d7a5ff 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -4,20 +4,31 @@
          "effect-rep.ss"
          "tc-utils.ss"
          "rep-utils.ss"
-         "free-variance.ss"
+         (only-in "free-variance.ss" combine-frees)
          mzlib/plt-match
+         scheme/list
+         mzlib/trace
          (for-syntax scheme/base))
 
 (provide fv fv/list
          substitute
+         substitute-dots
+         substitute-dotted
          subst-all
          subst 
          ret
          instantiate-poly
+         instantiate-poly-dotted
          tc-result: 
          tc-result-equal? 
          effects-equal?
-         tc-result-t)
+         tc-result-t
+         unfold
+         (struct-out Dotted)
+         (struct-out DottedBoth)
+         just-Dotted?
+         tc-error/expr
+         lookup-fail)
 
 
 ;; substitute : Type Name Type -> Type
@@ -25,17 +36,104 @@
   (define (sb t) (substitute image name t))
   (if (hash-ref (free-vars* target) name #f)
       (type-case sb target
-                 [#:F name* (if (eq? name* name) image target)])
+                 [#:F name* (if (eq? name* name) image target)]
+                 [#:arr dom rng rest drest thn-eff els-eff
+                        (begin
+                          (when (and (pair? drest)
+                                     (eq? name (cdr drest))
+                                     (just-Dotted? name))
+                            (int-err "substitute used on ... variable ~a in type ~a" name target))
+                          (make-arr (map sb dom)
+                                    (sb rng)
+                                    (and rest (sb rest))
+                                    (and drest (cons (sb (car drest)) (cdr drest)))
+                                    (map (lambda (e) (sub-eff sb e)) thn-eff)
+                                    (map (lambda (e) (sub-eff sb e)) els-eff)))]
+                 [#:ValuesDots types dty dbound
+                               (begin
+                                 (when (eq? name dbound)
+                                   (int-err "substitute used on ... variable ~a in type ~a" name target))
+                                 (make-ValuesDots (map sb types) (sb dty) dbound))])
       target))
 
+;; substitute-dots : Listof[Type] Option[type] Name Type -> Type
+(define (substitute-dots images rimage name target)    
+  (define (sb t) (substitute-dots images rimage name t))
+  (if (hash-ref (free-vars* target) name #f)
+      (type-case sb target
+                 [#:ValuesDots types dty dbound
+                               (if (eq? name dbound)
+                                   (make-Values
+                                    (append 
+                                     (map sb types)
+                                     ;; We need to recur first, just to expand out any dotted usages of this.
+                                     (let ([expanded (sb dty)])
+                                       (map (lambda (img) (substitute img name expanded)) images))))
+                                   (make-ValuesDots (map sb types) (sb dty) dbound))]
+                 [#:arr dom rng rest drest thn-eff els-eff
+                        (if (and (pair? drest)
+                                 (eq? name (cdr drest)))                            
+                            (make-arr (append 
+                                       (map sb dom)
+                                       ;; We need to recur first, just to expand out any dotted usages of this.
+                                       (let ([expanded (sb (car drest))])
+					 (map (lambda (img) (substitute img name expanded)) images)))
+                                      (sb rng)
+                                      rimage
+                                      #f
+                                      (map (lambda (e) (sub-eff sb e)) thn-eff)
+                                      (map (lambda (e) (sub-eff sb e)) els-eff))
+                            (make-arr (map sb dom)
+                                      (sb rng)
+                                      (and rest (sb rest))
+                                      (and drest (cons (sb (car drest)) (cdr drest)))
+                                      (map (lambda (e) (sub-eff sb e)) thn-eff)
+                                      (map (lambda (e) (sub-eff sb e)) els-eff)))])
+      target))
+
+;; implements sd from the formalism
+;; substitute-dotted : Type Name Name Type -> Type
+(define (substitute-dotted image image-bound name target)
+  (define (sb t) (substitute-dotted image image-bound name t))
+  (if (hash-ref (free-vars* target) name #f)
+      (type-case sb target
+                 [#:ValuesDots types dty dbound
+                               (make-ValuesDots (map sb types)
+                                                (sb dty)
+                                                (if (eq? name dbound) image-bound dbound))]
+                 [#:F name*
+                      (if (eq? name* name)
+                          image
+                          target)]
+                 [#:arr dom rng rest drest thn-eff els-eff
+                        (make-arr (map sb dom)
+                                  (sb rng)
+                                  (and rest (sb rest))
+                                  (and drest
+                                       (cons (sb (car drest))
+                                             (if (eq? name (cdr drest)) image-bound (cdr drest))))
+                                  (map (lambda (e) (sub-eff sb e)) thn-eff)
+                                  (map (lambda (e) (sub-eff sb e)) els-eff))])
+       target))
+
 ;; substitute many variables
-;; substitution = Listof[List[Name,Type]]
+;; substitution = Listof[U List[Name,Type] List[Name,Listof[Type]]]
 ;; subst-all : substition Type -> Type
 (define (subst-all s t)
-  (foldr (lambda (e acc) (substitute (cadr e) (car e) acc)) t s))
-
+  (for/fold ([t t]) ([e s])
+    (match e
+      [(list v (list imgs ...) starred)
+       (substitute-dots imgs starred v t)]
+      [(list v img)
+       (substitute img v t)])))
 
 
+;; unfold : Type -> Type
+;; must be applied to a Mu
+(define (unfold t)
+  (match t
+    [(Mu: name b) (substitute t name b)]
+    [_ (int-err "unfold: requires Mu type, got ~a" t)]))
 
 (define (instantiate-poly t types)
   (match t
@@ -43,7 +141,23 @@
      (unless (= (length types) (length ns))
        (int-err "instantiate-poly: wrong number of types: expected ~a, got ~a" (length ns) (length types)))
      (subst-all (map list ns types) body)]
-    [_ (int-err "instantiate-many: requires Poly type, got ~a" t)]))
+    [(PolyDots: (list fixed ... dotted) body)
+     (unless (>= (length types) (length fixed))
+       (int-err "instantiate-poly: wrong number of types: expected at least ~a, got ~a" (length fixed) (length types)))
+     (let* ([fixed-tys (take types (length fixed))]
+            [rest-tys (drop types (length fixed))]
+            [body* (subst-all (map list fixed fixed-tys) body)])
+       (substitute-dots rest-tys #f dotted body*))]
+    [_ (int-err "instantiate-poly: requires Poly type, got ~a" t)]))
+
+(define (instantiate-poly-dotted t types image var)
+  (match t
+    [(PolyDots: (list fixed ... dotted) body)
+     (unless (= (length fixed) (length types))
+       (int-err "instantiate-poly-dotted: wrong number of types: expected ~a, got ~a" (length fixed) (length types)))
+     (let ([body* (subst-all (map list fixed types) body)])
+       (substitute-dotted image var dotted body*))]
+    [_ (int-err "instantiate-poly-dotted: requires PolyDots type, got ~a" t)]))
 
 
 ;; this structure represents the result of typechecking an expression
@@ -79,3 +193,18 @@
 
 ;; fv/list : Listof[Type] -> Listof[Name]
 (define (fv/list ts) (hash-map (combine-frees (map free-vars* ts)) (lambda (k v) k)))
+
+;; t is (make-F v)
+(define-struct Dotted (t))
+(define-struct (DottedBoth Dotted) ())
+
+(define (just-Dotted? S)
+    (and (Dotted? S)
+         (not (DottedBoth? S))))
+
+(define (tc-error/expr msg #:return [return (make-Union null)] #:stx [stx (current-orig-stx)] . rest)
+  (tc-error/delayed #:stx stx (apply format msg rest))
+  return)
+
+;; error for unbound variables
+(define (lookup-fail e) (tc-error/expr "unbound identifier ~a" e))
diff --git a/collects/typed-scheme/typed-scheme.scrbl b/collects/typed-scheme/typed-scheme.scrbl
index fd52f6ca..43afa16c 100644
--- a/collects/typed-scheme/typed-scheme.scrbl
+++ b/collects/typed-scheme/typed-scheme.scrbl
@@ -185,6 +185,10 @@ process of elimination we can determine that @scheme[t] must be a
 
 @section{Polymorphism}
 
+Typed Scheme offers abstraction over types as well as values.
+
+@subsection{Polymorphic Data Structures}
+
 Virtually every Scheme program uses lists and sexpressions.  Fortunately, Typed
 Scheme can handle these as well.  A simple list processing program can be
 written like this:
@@ -246,6 +250,144 @@ produces @scheme[(make-Just v)] when the number is found in the list,
 and @scheme[(make-Nothing)] otherwise.  Therefore, it produces a
 @scheme[(Maybe Number)], just as the annotation specified.  
 
+@subsection{Polymorphic Functions}
+
+Sometimes functions over polymorphic data structures only concern
+themselves with the form of the structure.  For example, one might
+write a function that takes the length of a list of numbers:
+
+@schememod[typed-scheme
+(: list-number-length ((Listof Number) -> Integer))
+(define (list-number-length l)
+  (if (null? l)
+      0
+      (add1 (list-number-length (cdr l)))))]
+
+and also a function that takes the length of a list of strings:
+
+@schememod[typed-scheme
+(: list-string-length ((Listof String) -> Integer))
+(define (list-string-length l)
+  (if (null? l)
+      0
+      (add1 (list-string-length (cdr l)))))]
+
+Notice that both of these functions have almost exactly the same
+definition; the only difference is the name of the function.  This
+is because neither function uses the type of the elements in the
+definition.
+
+We can abstract over the type of the element as follows:
+
+@schememod[typed-scheme
+(: list-length (All (A) ((Listof A) -> Integer)))
+(define (list-length l)
+  (if (null? l)
+      0
+      (add1 (list-length (cdr l)))))]
+
+The new type constructor @scheme[All] takes a list of type
+variables and a body type.  The type variables are allowed to
+appear free in the body of the @scheme[All] form.
+
+@section{Variable-Arity Functions: Programming with Rest Arguments}
+
+Typed Scheme can handle some uses of rest arguments.
+
+@subsection{Uniform Variable-Arity Functions}
+
+In Scheme, one can write a function that takes an arbitrary
+number of arguments as follows:
+
+@schememod[scheme
+(define (sum . xs)
+  (if (null? xs)
+      0
+      (+ (car xs) (apply sum (cdr xs)))))
+
+(sum)
+(sum 1 2 3 4)
+(sum 1 3)]
+
+The arguments to the function that are in excess to the
+non-rest arguments are converted to a list which is assigned
+to the rest parameter.  So the examples above evaluate to
+@schemeresult[0], @schemeresult[10], and @schemeresult[4].
+
+We can define such functions in Typed Scheme as well:
+
+@schememod[typed-scheme
+(: sum (Number * -> Number))
+(define (sum . xs)
+  (if (null? xs)
+      0
+      (+ (car xs) (apply sum (cdr xs)))))]
+
+This type can be assigned to the function when each element
+of the rest parameter is used at the same type.
+
+@subsection{Non-Uniform Variable-Arity Functions}
+
+However, the rest argument may be used as a heterogeneous list.
+Take this (simplified) definition of the Scheme function @scheme[map]:
+
+@schememod[scheme
+(define (map f as . bss)
+  (if (or (null? as)
+          (ormap null? bss))
+      null
+      (cons (apply f (car as) (map car bss))
+            (apply map f (cdr as) (map cdr bss)))))
+
+(map add1 (list 1 2 3 4))
+(map cons (list 1 2 3) (list (list 4) (list 5) (list 6)))
+(map + (list 1 2 3) (list 2 3 4) (list 3 4 5) (list 4 5 6))]
+
+Here the different lists that make up the rest argument @scheme[bss]
+can be of different types, but the type of each list in @scheme[bss]
+corresponds to the type of the corresponding argument of @scheme[f].
+We also know that, in order to avoid arity errors, the length of
+@scheme[bss] must be one less than the arity of @scheme[f] (as
+@scheme[as] corresponds to the first argument of @scheme[f]).
+                                                            
+The example uses of @scheme[map] evaluate to @schemeresult[(list 2 3 4 5)],
+@schemeresult[(list (list 1 4) (list 2 5) (list 3 6))], and
+@schemeresult[(list 10 14 18)].
+
+In Typed Scheme, we can define @scheme[map] as follows:
+
+@schememod[typed-scheme
+(: map 
+   (All (C A B ...)
+        ((A B ... B -> C) (Listof A) (Listof B) ... B
+         ->
+         (Listof C))))
+(define (map f as . bss)
+  (if (or (null? as)
+          (ormap null? bss))
+      null
+      (cons (apply f (car as) (map car bss))
+            (apply map f (cdr as) (map cdr bss)))))]
+
+Note that the type variable @scheme[B] is followed by an
+ellipsis.  This denotes that B is a dotted type variable
+which corresponds to a list of types, much as a rest
+argument corresponds to a list of values.  When the type
+of @scheme[map] is instantiated at a list of types, then
+each type @scheme[t] which is bound by @scheme[B] (notated by
+the dotted pre-type @scheme[t ... B]) is expanded to a number
+of copies of @scheme[t] equal to the length of the sequence
+assigned to @scheme[B].  Then @scheme[B] in each copy is
+replaced with the corresponding type from the sequence.
+
+So the type of @scheme[(inst map Integer Boolean String Number)]
+is
+
+@scheme[((Boolean String Number -> Integer)
+         (Listof Boolean) (Listof String) (Listof Number)
+         ->
+         (Listof Integer))].
+
 @section[#:tag "type-ref"]{Type Reference}
 
 @subsubsub*section{Base Types}
diff --git a/collects/typed-scheme/typed-scheme.ss b/collects/typed-scheme/typed-scheme.ss
index da552fea..1a0d5023 100644
--- a/collects/typed-scheme/typed-scheme.ss
+++ b/collects/typed-scheme/typed-scheme.ss
@@ -12,7 +12,9 @@
           "private/tc-utils.ss"
           "private/type-name-env.ss"
           "private/type-alias-env.ss"
-          "private/utils.ss"
+          (except-in "private/utils.ss" extend)
+          (only-in "private/infer-dummy.ss" infer-param)
+          "private/infer.ss"
           "private/type-effect-convenience.ss"
           "private/type-contract.ss"
           scheme/nest
@@ -38,7 +40,9 @@
   (define module-name (syntax-property stx 'enclosing-module-name))
   ;(printf "BEGIN: ~a~n" (syntax->datum stx))
   (with-logging-to-file 
-   (log-file-name (syntax-src stx) module-name)
+   "/tmp/ts-poly.log"
+   #;
+   (log-file-name (syntax-source stx) module-name)
    (syntax-case stx ()
      [(mb forms ...)
       (nest
@@ -47,7 +51,10 @@
            [with-handlers
                ([(lambda (e) (and catch-errors? (exn:fail? e) (not (exn:fail:syntax? e))))
                  (lambda (e) (tc-error "Internal error: ~a" e))])]
-           [parameterize ([delay-errors? #t]
+           [parameterize (;; a cheat to avoid units
+                          [infer-param infer]
+                          ;; do we report multiple errors
+                          [delay-errors? #t]
                           ;; this parameter is for parsing types
                           [current-tvars initial-tvar-env]
                           ;; this parameter is just for printing types
@@ -65,8 +72,9 @@
            ;; local-expand the module
            ;; pmb = #%plain-module-begin                            
            [with-syntax ([new-mod 
-                          (local-expand #`(#%plain-module-begin 
-                                           forms ...)
+                          (local-expand (syntax/loc stx
+                                          (#%plain-module-begin 
+                                           forms ...))
                                         'module-begin 
                                         null)])]
            [with-syntax ([(pmb body2 ...) #'new-mod])]
@@ -93,7 +101,9 @@
     [(_ . form)     
      (nest
          ([begin (set-box! typed-context? #t)]
-          [parameterize (;; this paramter is for parsing types
+          [parameterize (;; a cheat to avoid units
+                         [infer-param infer]
+                         ;; this paramter is for parsing types
                          [current-tvars initial-tvar-env]
                          ;; this parameter is just for printing types
                          ;; this is a parameter to avoid dependency issues