Add the forall Unicode symbol as an acceptable replacement for the

All type constructor.

svn: r10797

original commit: 91291ba2bc31e599ec703b5bdd091a6238ce6c71

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)))

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))

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))

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))

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))

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))

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")

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

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)))

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))
+

collects/tests/typed-scheme/succeed/batched-queue.scm

@@ -82,5 +82,5 @@
 
 ;; TESTS
 
-(= 0 (size (empty)))
+(= 0 (size ((inst empty Number))))
 

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))

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))))

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)}

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))))

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))

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)

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))

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))

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)

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))   
 
   

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")

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)

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)

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)
+
+|#

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)])

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))
 
 ; ---

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 +)

collects/tests/typed-scheme/succeed/string-const.ss

@@ -3,3 +3,5 @@
 (require string-constants/string-constant)
 
 (string-constant cancel)
+
+(this-language)

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 + - * /)

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)

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)

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 

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)                   

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)]

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))
 

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)
+

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))

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)))
    )

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 

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)

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))
           =>

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)]

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)
 

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)
 

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))]

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]))

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)
 
 

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

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))

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}

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