diff --git a/collects/typed-scheme/private/infer-unit.ss b/collects/typed-scheme/private/infer-unit.ss
index 4994d50e37..9def9e8c0a 100644
--- a/collects/typed-scheme/private/infer-unit.ss
+++ b/collects/typed-scheme/private/infer-unit.ss
@@ -6,6 +6,7 @@
          "union.ss" "tc-utils.ss" "type-name-env.ss"
          "subtype.ss" "remove-intersect.ss" "signatures.ss" "utils.ss"
          "constraint-structs.ss"
+         (only-in "type-environments.ss" lookup current-tvars)
          scheme/match
          mzlib/etc
          mzlib/trace
@@ -185,8 +186,18 @@
          [(_ (Univ:)) empty]
          
          [((F: (? (lambda (e) (memq e X)) v)) S)
+          (when (match S
+                  [(F: v*)
+                   (just-Dotted? (lookup (current-tvars) v* (lambda _ #f)))]
+                  [_ #f])
+            (fail! S T))
           (singleton (Un) v (var-demote S V))]
          [(S (F: (? (lambda (e) (memq e X)) v)))
+          (when (match S
+                  [(F: v*)
+                   (just-Dotted? (lookup (current-tvars) v* (lambda _ #f)))]
+                  [_ #f])
+            (fail! S T))
           (singleton (var-promote S V) v Univ)]
          
          
diff --git a/collects/typed-scheme/private/tc-app-unit.ss b/collects/typed-scheme/private/tc-app-unit.ss
index 7762bfbce9..b8f4d9da1a 100644
--- a/collects/typed-scheme/private/tc-app-unit.ss
+++ b/collects/typed-scheme/private/tc-app-unit.ss
@@ -126,14 +126,18 @@
     (let loop ([l l] [acc '()])
       (if (null? (cdr l))
           (values (reverse acc) (car l))
-          (loop (cdr l) (cons (car l) acc)))))   
-  (define (printable dom rst drst)
+          (loop (cdr l) (cons (car l) acc)))))
+  (define (printable-h dom r-ty r-bound)
     (let ([doms-string (if (null? dom) "" (string-append (stringify dom) " "))])
-      (cond [rst
-             (format "~a~a *" doms-string rst)]
-            [drst
-             (format "~a~a ... ~a" doms-string (car drst) (cdr drst))]
+      (cond [r-bound
+             (format "~a~a ... ~a" doms-string r-ty r-bound)]
+            [r-ty
+             (format "~a~a *" doms-string r-ty)]
             [else (stringify dom)])))
+  (define (printable dom rst drst)
+    (cond [rst (printable-h dom rst #f)]
+          [drst (printable-h dom (car drst) (cdr drst))]
+          [else (printable-h dom #f #f)]))
   (define-values (fixed-args tail) (split (syntax->list args)))
   (define (apply-error doms rests drests arg-tys tail-ty tail-bound)
     (if (and (not (null? doms)) (null? (cdr doms)))
@@ -172,11 +176,9 @@
        (let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests])
          (cond [(null? doms*)
                 (let-values ([(tail-ty tail-bound)
-                              (with-handlers ([exn:fail? (lambda _ (values #f #f))])
+                              (with-handlers ([exn:fail? (lambda _ (values (tc-expr/t tail) #f))])
                                 (tc/dots tail))])
-                  (if tail-ty
-                      (apply-error doms rests drests arg-tys tail-ty tail-bound)
-                      (apply-error doms rests drests arg-tys (tc-expr/t tail) #f)))]
+                      (apply-error doms rests drests arg-tys tail-ty tail-bound))]
                [(and (car rests*)
                      (let-values ([(tail-ty tail-bound) 
                                    (with-handlers ([exn:fail? (lambda _ (values #f #f))])
@@ -203,9 +205,9 @@
                 (ret (car rngs*))]
                [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))]
     [(tc-result: (Poly: vars (Function: (list (arr: doms rngs rests #f thn-effs els-effs) ..1))))
-     (let*-values ([(arg-tys tail-ty) (values (map tc-expr/t fixed-args)
-                                              (tc-expr/t tail))]
-                   [(arg-tys0) (append arg-tys (list tail-ty))])
+     (let*-values ([(arg-tys) (map tc-expr/t fixed-args)]
+                   [(tail-ty tail-bound) (with-handlers ([exn:fail:syntax? (lambda _ (values (tc-expr/t tail) #f))])
+                                           (tc/dots tail))])
        (for-each (lambda (x) (unless (not (Poly? x))                                      
                                (tc-error "Polymorphic argument ~a to polymorphic function in apply not allowed" x)))
                  (cons tail-ty arg-tys))
@@ -220,11 +222,11 @@
                           (tc-error/expr
                            #:return (ret (Un))
                            "polymorphic function domain did not match -~ndomain was: ~a~nrest argument was: ~a~narguments were ~a~n" 
-                           (car doms) (car rests) (stringify arg-tys0))
+                           (car doms) (car rests) (printable-h arg-tys tail-ty tail-bound))
                           (tc-error/expr
                            #:return (ret (Un))
                            "polymorphic function domain did not match -~ndomain was: ~a~narguments were ~a~n" 
-                           (car doms) (stringify arg-tys0)))]
+                           (car doms) (printable-h arg-tys tail-ty tail-bound)))]
                      [else 
                       (tc-error/expr
                        #:return (ret (Un))
@@ -235,8 +237,11 @@
                               (format "~a rest argument: " (stringify dom) rest)
                               (stringify dom)))
                         "\n")
-                       (stringify arg-tys0))])])]
-               [(and (<= (length (car doms*))
+                       (printable-h arg-tys tail-ty tail-bound))])])]
+               ;; the actual work, when we have a * function and a list final argument
+               [(and (car rests*)
+                     (not tail-bound)
+                     (<= (length (car doms*))
                          (length arg-tys))
                      (infer/vararg vars
                                    (cons tail-ty arg-tys) 
@@ -244,12 +249,18 @@
                                          (car doms*))
                                    (car rests*)
                                    (car rngs*)))
-                => (lambda (substitution) 
-                     #;(let* ([s (lambda (t) (subst-all substitution t))]
-                            [new-doms* (append (map s (car doms*)) (list (make-Listof (s (car rests*)))))])
-                         (unless (andmap subtype arg-tys0 new-doms*)
-                           (int-err "Inconsistent substitution - arguments not subtypes: ~n~a~n~a~n" arg-tys0 new-doms*)))
-                     (ret (subst-all substitution (car rngs*))))]
+                => (lambda (substitution) (ret (subst-all substitution (car rngs*))))]
+               [(and (car rests*)
+                     tail-bound                     
+                     (<= (length (car doms*))
+                         (length arg-tys))
+                     (infer/vararg vars
+                                   (cons (make-Listof tail-ty) arg-tys)
+                                   (cons (make-Listof (car rests*))
+                                         (car doms*))
+                                   (car rests*)
+                                   (car rngs*)))
+                => (lambda (substitution) (ret (subst-all substitution (car rngs*))))]
                [else (loop (cdr doms*) (cdr rngs*) (cdr rests*))])))]
     [(tc-result: (Poly: vars (Function: '())))
      (tc-error/expr #:return (ret (Un))
diff --git a/collects/typed-scheme/private/tc-dots-unit.ss b/collects/typed-scheme/private/tc-dots-unit.ss
index 26c2436960..674d9d9b3e 100644
--- a/collects/typed-scheme/private/tc-dots-unit.ss
+++ b/collects/typed-scheme/private/tc-dots-unit.ss
@@ -25,6 +25,8 @@
           (values dty dbound)])]
       [(#%plain-app map f l)
        (let-values ([(lty lbound) (tc/dots #'l)])
+         (unless (Dotted? (lookup (current-tvars) lbound (lambda _ #f)))
+           (int-err "tc/dots: ~a was not dotted" lbound))
          (parameterize ([current-tvars (extend-env (list lbound)
                                                    (list (make-DottedBoth (make-F lbound)))
                                                    (current-tvars))])
diff --git a/collects/typed-scheme/private/tc-lambda-unit.ss b/collects/typed-scheme/private/tc-lambda-unit.ss
index 9efbb6710e..cd3ff60608 100644
--- a/collects/typed-scheme/private/tc-lambda-unit.ss
+++ b/collects/typed-scheme/private/tc-lambda-unit.ss
@@ -116,18 +116,19 @@
                                      (lambda _ (tc-error/stx #'rest
                                                              "Bound on ... type (~a) was not in scope" bound))))
               (tc-error "Bound on ... type (~a) is not an appropriate type variable" bound))
-            (parameterize ([current-tvars (extend-env (list bound) 
-                                                      (list (make-DottedBoth (make-F bound)))
-                                                      (current-tvars))])
-              (let ([rest-type (get-type #'rest)])
-                (with-lexical-env/extend 
-                 arg-list
-                 arg-types
-                 (parameterize ([dotted-env (extend-env (list #'rest)
-                                                        (list (cons rest-type bound))
-                                                        (dotted-env))])
-                   (match-let ([(tc-result: t thn els) (tc-exprs (syntax->list body))])
-                     (make-arr-dots arg-types t rest-type bound)))))))]
+            (let ([rest-type (parameterize ([current-tvars 
+                                             (extend-env (list bound) 
+                                                         (list (make-DottedBoth (make-F bound)))
+                                                         (current-tvars))])
+                               (get-type #'rest))])
+              (with-lexical-env/extend 
+               arg-list
+               arg-types
+               (parameterize ([dotted-env (extend-env (list #'rest)
+                                                      (list (cons rest-type bound))
+                                                      (dotted-env))])
+                 (match-let ([(tc-result: t thn els) (tc-exprs (syntax->list body))])
+                   (make-arr-dots arg-types t rest-type bound))))))]
          [else
           (let ([rest-type (get-type #'rest)])
             (with-lexical-env/extend 
diff --git a/collects/typed-scheme/private/tc-toplevel.ss b/collects/typed-scheme/private/tc-toplevel.ss
index 5cc6cf1302..63e2a82b2d 100644
--- a/collects/typed-scheme/private/tc-toplevel.ss
+++ b/collects/typed-scheme/private/tc-toplevel.ss
@@ -90,7 +90,10 @@
             (map (lambda (s) (make-def-binding s (lookup-type s))) vars)]
            ;; special case to infer types for top level defines - should handle the multiple values case here
            [(and (= 1 (length vars)) 
-                 (with-handlers ([exn:fail? (lambda _ #f)]) (tc-expr #'expr)))
+                 (with-handlers ([exn:fail? (lambda _ #f)])
+                   (save-errors!)
+                   (begin0 (tc-expr #'expr)
+                           (restore-errors!))))
             => (match-lambda 
                  [(tc-result: t)
                   (register-type (car vars) t)
diff --git a/collects/typed-scheme/private/tc-utils.ss b/collects/typed-scheme/private/tc-utils.ss
index 00919fe3c2..59e65f6fc1 100644
--- a/collects/typed-scheme/private/tc-utils.ss
+++ b/collects/typed-scheme/private/tc-utils.ss
@@ -49,6 +49,11 @@
 
 (define-struct err (msg stx) #:prefab)
 
+(define-values (save-errors! restore-errors!)
+  (let ([v (box #f)])
+    (values (lambda () (set-box! v delayed-errors))
+            (lambda () (set! delayed-errors (unbox v))))))
+
 (define (report-all-errors)
   (define (reset!) (set! delayed-errors null))
   (match (reverse delayed-errors)
diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index 21b4c5f532..42bf4788a0 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -22,7 +22,8 @@
          tc-result-t
          unfold
          (struct-out Dotted)
-         (struct-out DottedBoth))
+         (struct-out DottedBoth)
+         just-Dotted?)
 
 
 ;; substitute : Type Name Type -> Type
@@ -134,4 +135,8 @@
 
 ;; t is (make-F v)
 (define-struct Dotted (t))
-(define-struct (DottedBoth Dotted) ())
\ No newline at end of file
+(define-struct (DottedBoth Dotted) ())
+
+(define (just-Dotted? S)
+    (and (Dotted? S)
+         (not (DottedBoth? S))))
\ No newline at end of file