diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 07999859..88b2e8fb 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -506,6 +506,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 7c793ccf..83aa9c40 100644
--- a/collects/typed-scheme/private/extra-procs.ss
+++ b/collects/typed-scheme/private/extra-procs.ss
@@ -1,5 +1,5 @@
 #lang scheme/base
-(provide assert)
+(provide assert call-with-values* values*)
 
 (define (assert v)
   (unless v
@@ -12,4 +12,7 @@
       c
       (apply f
              (apply fold-right f c (cdr as) (map cdr bss))
-             (car as) (map car bss))))
\ No newline at end of file
+             (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 a5f61ed0..88da572e 100644
--- a/collects/typed-scheme/private/parse-type.ss
+++ b/collects/typed-scheme/private/parse-type.ss
@@ -101,6 +101,19 @@
        (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 ...))))]
diff --git a/collects/typed-scheme/private/type-effect-printer.ss b/collects/typed-scheme/private/type-effect-printer.ss
index e7554d22..1f301705 100644
--- a/collects/typed-scheme/private/type-effect-printer.ss
+++ b/collects/typed-scheme/private/type-effect-printer.ss
@@ -110,6 +110,7 @@
     [(Pair: l r) (fp "(Pair ~a ~a)" l r)]
     [(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)           
diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index d6e191f1..08a022b6 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -7,6 +7,7 @@
          (only-in "free-variance.ss" combine-frees)
          mzlib/plt-match
          scheme/list
+         mzlib/trace
          (for-syntax scheme/base))
 
 (provide fv fv/list
@@ -46,7 +47,12 @@
                                     (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)))])
+                                    (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
@@ -54,6 +60,15 @@
   (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)))                            
@@ -81,6 +96,10 @@
   (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
@@ -94,7 +113,9 @@
                                              (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))
+       target))
+
+(trace substitute-dots)
 
 ;; substitute many variables
 ;; substitution = Listof[U List[Name,Type] List[Name,Listof[Type]]]