Instantiation appears to work.

collects/typed-scheme/private/base-env.ss

@@ -498,6 +498,20 @@
      [syntax? (make-pred-ty (-Syntax Univ))]
      [syntax-property (-poly (a) (cl->* (-> (-Syntax a) Univ Univ (-Syntax a))
                                         (-> (-Syntax Univ) Univ Univ)))]
+     
+     ;; experimental
+     
+     [map* (make-PolyDots 
+            (list 'a 'b 'c)
+            (make-Function 
+             (list 
+              (make-arr-dots 
+               (list (make-Function (list (make-arr-dots (list (-v b)) (-v a) (-v c) 'c)))
+                     (-lst (-v b)))
+               (-lst (-v a))
+               (-lst (-v c))
+               'c))))]
+     
      )))
 
 (begin-for-syntax 

collects/typed-scheme/private/extra-procs.ss

@@ -1,7 +1,11 @@
 #lang scheme/base
-(provide assert)    
+(provide assert map*)
 
 (define (assert v)
   (unless v
     (error "Assertion failed - value was #f"))
   v)
+
+(define map* map)
+
+

collects/typed-scheme/private/tc-expr-unit.ss

@@ -69,13 +69,20 @@
   (let* ([ty (lookup-type/lexical id)]
          [inst (syntax-property id 'type-inst)])
     (cond [(and inst
-                (not (Poly? ty)))
+                (not (or (Poly? ty) (PolyDots? ty))))
            (tc-error/expr #:return (ret (Un)) "Cannot instantiate non-polymorphic type ~a" ty)]
+          
           [(and inst
-               (not (= (length (syntax->list inst)) (Poly-n ty))))
+                (Poly? ty)
+                (not (= (length (syntax->list inst)) (Poly-n ty))))
            (tc-error/expr #:return (ret (Un)) 
                           "Wrong number of type arguments to polymorphic type ~a:~nexpected: ~a~ngot: ~a"
                           ty (Poly-n ty) (length (syntax->list inst)))]
+          [(and inst (PolyDots? ty) (not (>= (length (syntax->list inst)) (sub1 (PolyDots-n ty)))))
+           ;; we can provide 0 arguments for the ... var
+           (tc-error/expr #:return (ret (Un)) 
+                          "Wrong number of type arguments to polymorphic type ~a:~nexpected at least: ~a~ngot: ~a"
+                          ty (sub1 (PolyDots-n ty)) (length (syntax->list inst)))]
           [else
            (let ([ty* (if inst
                           (instantiate-poly ty (map parse-type (syntax->list inst)))

collects/typed-scheme/private/type-effect-printer.ss

@@ -52,7 +52,7 @@
        (when rest
          (fp "~a* " rest))
        (when drest
-         (fp "~a ..." 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))
@@ -115,6 +115,8 @@
     [(Poly-names: names body) 
      #;(fprintf (current-error-port) "POLY SEQ: ~a~n" (Type-seq body))
      (fp "(All ~a ~a)" names body)]
+    [(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

collects/typed-scheme/private/type-rep.ss

@@ -337,7 +337,7 @@
                     (if rest (sb rest) #f)
                     (if drest
                         (cons (sb (car drest))
-                              (if (= (cdr drest) (+ count outer)) (F-n image) (cdr drest)))
+                              (if (eqv? (cdr drest) (+ count outer)) (F-n image) (cdr drest)))
                         #f)
                     (map (lambda (e) (sub-eff sb e)) thn-eff)
                     (map (lambda (e) (sub-eff sb e)) els-eff))]
@@ -526,6 +526,7 @@
              [PolyDots:* PolyDots:]
              [Mu* make-Mu]
              [Poly* make-Poly]
+             [PolyDots* make-PolyDots]
              [Mu-body* Mu-body]
              [Poly-body* Poly-body]
              [PolyDots-body* PolyDots-body]))

collects/typed-scheme/private/type-utils.ss

@@ -33,7 +33,7 @@
                         (begin
                           (when (and (pair? drest)
                                      (eq? name (cdr drest)))
-                            (int-err "substitute used on ... variable ~a" name))
+                            (int-err "substitute used on ... variable ~a in type ~a" name target))
                           (make-arr (map sb dom)
                                     (sb rng)
                                     (and rest (sb rest))

collects/typed-scheme/private/utils.ss

@@ -99,7 +99,7 @@
       [(_ val)
        #'(? (lambda (x) (equal? val x)))])))
 
-(define-for-syntax printing? #f)
+(define-for-syntax printing? #t)
 
 (define print-type* (box (lambda _ (error "print-type* not yet defined"))))
 (define print-effect* (box (lambda _ (error "print-effect* not yet defined"))))