From 69c730334293f6702a2b52de9f9ba359eab6bb33 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Mon, 9 Jun 2008 17:07:41 -0400
Subject: [PATCH 01/96] Add new datastructures for dots work.

original commit: a7c63840e4e2b80dd8007921334f7cbd245fe3de
---
 collects/typed-scheme/private/subtype.ss                 | 4 ++--
 collects/typed-scheme/private/type-effect-convenience.ss | 4 ++--
 collects/typed-scheme/private/type-effect-printer.ss     | 8 +++++---
 3 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/collects/typed-scheme/private/subtype.ss b/collects/typed-scheme/private/subtype.ss
index 91f0accf..5f7e3595 100644
--- a/collects/typed-scheme/private/subtype.ss
+++ b/collects/typed-scheme/private/subtype.ss
@@ -99,10 +99,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*)
diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss
index bbf60088..22317db1 100644
--- a/collects/typed-scheme/private/type-effect-convenience.ss
+++ b/collects/typed-scheme/private/type-effect-convenience.ss
@@ -68,8 +68,8 @@
 
 (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)]))
 
 (define (make-promise-ty t)
   (make-Struct (string->uninterned-symbol "Promise") #f (list t) #f #f #'promise? values))
diff --git a/collects/typed-scheme/private/type-effect-printer.ss b/collects/typed-scheme/private/type-effect-printer.ss
index 22cccaab..c2a2d940 100644
--- a/collects/typed-scheme/private/type-effect-printer.ss
+++ b/collects/typed-scheme/private/type-effect-printer.ss
@@ -46,11 +46,13 @@
     (match a
       [(top-arr:)
        (fp "Procedure")]
-      [(arr: dom rng rest thn-eff els-eff)
+      [(arr: dom rng rest drest thn-eff els-eff)
        (fp "(")
        (for-each (lambda (t) (fp "~a " t)) dom)
        (when rest
-         (fp "~a .. " rest))
+         (fp "~a* " rest))
+       (when drest
+         (fp "~a ..." drest))
        (fp "-> ~a" rng)
        (unless (and (null? thn-eff) (null? els-eff))
          (fp " : ~a ~a" thn-eff els-eff))
@@ -96,7 +98,7 @@
          [(list) (fp "(case-lambda)")]
          [(list a) (print-arr a)]
          [(list a ...) (fp "(case-lambda ") (for-each print-arr a) (fp ")")]))]
-    [(arr: _ _ _ _ _) (print-arr c)]
+    [(arr: _ _ _ _ _ _) (print-arr c)]
     [(Vector: e) (fp "(Vectorof ~a)" e)]
     [(Box: e) (fp "(Box ~a)" e)]
     [(Union: elems) (fp "~a" (cons 'U elems))]

From 583b6408338ce0de5f6ac41dfb49817967b655b8 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Tue, 10 Jun 2008 11:29:56 -0400
Subject: [PATCH 02/96] Fix instantiate and abstract to handle bounds properly.
 NEW INVARIANT - only use instantiate w/ names

original commit: 017f756c7735a0e6083fa2f52eaafc0f20b11912
---
 collects/typed-scheme/private/resolve-type.ss |  2 +-
 collects/typed-scheme/private/type-utils.ss   | 10 ++++++++--
 2 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/collects/typed-scheme/private/resolve-type.ss b/collects/typed-scheme/private/resolve-type.ss
index 28385b80..d68de692 100644
--- a/collects/typed-scheme/private/resolve-type.ss
+++ b/collects/typed-scheme/private/resolve-type.ss
@@ -1,7 +1,7 @@
 #lang scheme/base
 
 (require "type-rep.ss"  "type-name-env.ss" "tc-utils.ss"
-         "type-utils.ss" 
+         "type-utils.ss"
          mzlib/plt-match
          mzlib/trace)
 
diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index c4e1fa84..b82bf64a 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -17,7 +17,8 @@
          tc-result: 
          tc-result-equal? 
          effects-equal?
-         tc-result-t)
+         tc-result-t
+         unfold)
 
 
 ;; substitute : Type Name Type -> Type
@@ -35,7 +36,12 @@
   (foldr (lambda (e acc) (substitute (cadr e) (car e) acc)) t s))
 
 
-
+;; 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

From a93289aedde680542ed33089ebd128a69b108db3 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Tue, 10 Jun 2008 12:21:59 -0400
Subject: [PATCH 03/96] Substituion now works

original commit: a7f81d931d9bef247b9215cb1e6fdd3e616dd6a2
---
 collects/typed-scheme/private/subtype.ss      |  2 +-
 .../private/type-effect-convenience.ss        |  6 ++-
 collects/typed-scheme/private/type-utils.ss   | 41 ++++++++++++++++++-
 3 files changed, 46 insertions(+), 3 deletions(-)

diff --git a/collects/typed-scheme/private/subtype.ss b/collects/typed-scheme/private/subtype.ss
index 5f7e3595..04f3c89b 100644
--- a/collects/typed-scheme/private/subtype.ss
+++ b/collects/typed-scheme/private/subtype.ss
@@ -1,6 +1,6 @@
 #lang scheme/base
 
-(require "type-rep.ss" "unify.ss" "type-utils.ss"
+(require (except-in "type-rep.ss" sub-eff) "unify.ss" "type-utils.ss"
          "tc-utils.ss"
          "effect-rep.ss"
          "type-comparison.ss"
diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss
index 22317db1..73c11ef9 100644
--- a/collects/typed-scheme/private/type-effect-convenience.ss
+++ b/collects/typed-scheme/private/type-effect-convenience.ss
@@ -69,7 +69,11 @@
 (define make-arr*
   (case-lambda [(dom rng) (make-arr* dom rng #f (list) (list))]
                [(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 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))
diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index b82bf64a..a67bc677 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -10,6 +10,7 @@
 
 (provide fv fv/list
          substitute
+         substitute-dots
          subst-all
          subst 
          ret
@@ -26,7 +27,45 @@
   (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)))
+                            (int-err "substitute used on ... variable ~a" name))
+                          (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))
+
+;; substitute-dots : Listof[Type] Name Type -> Type
+(define (substitute-dots images name target)    
+  (define (sb t) (substitute-dots images name t))
+  (if (hash-ref (free-vars* target) name #f)
+      (type-case sb target
+                 [#:F name* (if (eq? name* name)
+                                (int-err "substitute-dots: got single variable ~a" name*)
+                                target)]
+                 [#:arr dom rng rest drest thn-eff els-eff
+                        (if (and (pair? drest)
+                                 (eq? name (cdr drest)))                            
+                            (make-arr (append 
+                                       (map sb dom)
+                                       (map (lambda (img) (substitute img name (car drest))) images))
+                                      (sb rng)
+                                      #f
+                                      #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))
 
 ;; substitute many variables

From d0711544383876ac24d0fc167999e9bb2e94859a Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Tue, 10 Jun 2008 12:29:53 -0400
Subject: [PATCH 04/96] Instantiate w/ dots

original commit: 5c8c2d3d96f02f4f8652b3c8e6fb70803ff85881
---
 collects/typed-scheme/private/type-utils.ss | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index a67bc677..ead27eea 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -6,6 +6,7 @@
          "rep-utils.ss"
          "free-variance.ss"
          mzlib/plt-match
+         scheme/list
          (for-syntax scheme/base))
 
 (provide fv fv/list
@@ -88,6 +89,13 @@
      (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)]
+    [(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 dotted body*))]
     [_ (int-err "instantiate-many: requires Poly type, got ~a" t)]))
 
 

From d6f8dfc983289f95245b17c7d1deb04f16b55d2c Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Tue, 10 Jun 2008 14:10:40 -0400
Subject: [PATCH 05/96] Instantiation appears to work.

original commit: e912818f866d6bcbeb43e4567ba9d0f1d58d6e3c
---
 collects/typed-scheme/private/base-env.ss          | 14 ++++++++++++++
 collects/typed-scheme/private/extra-procs.ss       |  6 +++++-
 .../typed-scheme/private/type-effect-printer.ss    |  4 +++-
 collects/typed-scheme/private/type-utils.ss        |  2 +-
 4 files changed, 23 insertions(+), 3 deletions(-)

diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 898796f6..0b8695a3 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/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 
diff --git a/collects/typed-scheme/private/extra-procs.ss b/collects/typed-scheme/private/extra-procs.ss
index b8b87b6c..428b5eaf 100644
--- a/collects/typed-scheme/private/extra-procs.ss
+++ b/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)
+
+
diff --git a/collects/typed-scheme/private/type-effect-printer.ss b/collects/typed-scheme/private/type-effect-printer.ss
index c2a2d940..2a5dac4d 100644
--- a/collects/typed-scheme/private/type-effect-printer.ss
+++ b/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
diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index ead27eea..621f6aab 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/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))

From f9708ff850058556cb7eadc1eb7f16ecb4c20f0e Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Tue, 10 Jun 2008 14:27:49 -0400
Subject: [PATCH 06/96] Remove infer.ss

original commit: 6afcb9aa9625376b1d634ed96ab96b8ae48b47f8
---
 collects/typed-scheme/private/remove-intersect.ss | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/collects/typed-scheme/private/remove-intersect.ss b/collects/typed-scheme/private/remove-intersect.ss
index 616fbb8e..afdb21bd 100644
--- a/collects/typed-scheme/private/remove-intersect.ss
+++ b/collects/typed-scheme/private/remove-intersect.ss
@@ -1,6 +1,6 @@
 #lang scheme/base
 
-(require "type-rep.ss" "unify.ss" "union.ss" "infer.ss" "subtype.ss"
+(require "type-rep.ss" "unify.ss" "union.ss" "subtype.ss"
          "type-utils.ss" "resolve-type.ss" "type-effect-convenience.ss"         
          mzlib/plt-match mzlib/trace)
 

From 9e78ce0847b3f8bda4bcdab8bb73a34c55740957 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Tue, 10 Jun 2008 15:05:13 -0400
Subject: [PATCH 07/96] Switch subtype to use infer.ss for unification.

original commit: 606ef69d205499ad6071d3a0e1d228938c5299b1
---
 collects/typed-scheme/private/remove-intersect.ss |  2 +-
 collects/typed-scheme/private/subtype.ss          |  5 +++--
 collects/typed-scheme/typed-scheme.ss             | 11 +++++++++--
 3 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/collects/typed-scheme/private/remove-intersect.ss b/collects/typed-scheme/private/remove-intersect.ss
index afdb21bd..f9b273e8 100644
--- a/collects/typed-scheme/private/remove-intersect.ss
+++ b/collects/typed-scheme/private/remove-intersect.ss
@@ -1,6 +1,6 @@
 #lang scheme/base
 
-(require "type-rep.ss" "unify.ss" "union.ss" "subtype.ss"
+(require "type-rep.ss" "union.ss" "subtype.ss"
          "type-utils.ss" "resolve-type.ss" "type-effect-convenience.ss"         
          mzlib/plt-match mzlib/trace)
 
diff --git a/collects/typed-scheme/private/subtype.ss b/collects/typed-scheme/private/subtype.ss
index 04f3c89b..5ba4a72c 100644
--- a/collects/typed-scheme/private/subtype.ss
+++ b/collects/typed-scheme/private/subtype.ss
@@ -1,11 +1,12 @@
 #lang scheme/base
 
-(require (except-in "type-rep.ss" sub-eff) "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)
 
@@ -197,7 +198,7 @@
               ;; use unification to see if we can use the polytype here
               [(list (Poly: vs b) s)
                (=> unmatch)
-               (if (unify1 s b) A0 (unmatch))]
+               (if (unify vs (list b) (list s)) A0 (unmatch))]
               [(list s (Poly: vs b))
                (=> unmatch)
                (if (null? (fv b)) (subtype* A0 s b) (unmatch))]
diff --git a/collects/typed-scheme/typed-scheme.ss b/collects/typed-scheme/typed-scheme.ss
index da552fea..939c49d5 100644
--- a/collects/typed-scheme/typed-scheme.ss
+++ b/collects/typed-scheme/typed-scheme.ss
@@ -13,6 +13,8 @@
           "private/type-name-env.ss"
           "private/type-alias-env.ss"
           "private/utils.ss"
+          (only-in "private/infer-dummy.ss" infer-param)
+          "private/infer.ss"
           "private/type-effect-convenience.ss"
           "private/type-contract.ss"
           scheme/nest
@@ -47,7 +49,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
@@ -93,7 +98,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

From ed9af8fdfd86dc10c87bbef4b95dd0eddba215a5 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Tue, 10 Jun 2008 15:41:56 -0400
Subject: [PATCH 08/96] Add syntax for ...

original commit: e29d4eb881b92a7f96ae1bbb248e311f7f8f90bc
---
 collects/typed-scheme/private/parse-type.ss   | 45 +++++++++++++++++--
 collects/typed-scheme/private/subtype.ss      |  2 +-
 .../private/type-effect-printer.ss            |  2 +-
 3 files changed, 43 insertions(+), 6 deletions(-)

diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss
index 72e51cd5..5565a9d9 100644
--- a/collects/typed-scheme/private/parse-type.ss
+++ b/collects/typed-scheme/private/parse-type.ss
@@ -24,6 +24,10 @@
 
 (define (stx-cadr stx) (stx-car (stx-cdr stx)))
 
+;; t is (make-F v)
+(define-struct Dotted (t))
+(define-struct (DottedBoth Dotted) ())
+
 
 (define (parse-type stx)    
   (parameterize ([current-orig-stx stx])
@@ -74,11 +78,28 @@
          (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 ...))))
+            (symbolic-identifier=? #'::: (quote-syntax *)))
        (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 #'->) '->)
@@ -129,6 +150,17 @@
       [(quot t)
        (eq? (syntax-e #'quot) 'quote)
        (-val (syntax-e #'t))]
+      [(All (vars ... v dd) t)
+       (and (eq? (syntax-e #'All) '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)
             (andmap identifier? (syntax->list #'(vars ...))))
@@ -136,7 +168,7 @@
               [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 +189,12 @@
        (identifier? #'id)
        (cond 
          ;; if it's a type variable, we just produce the corresponding reference (which is in the HT)
-         [(lookup (current-tvars) (syntax-e #'id) (lambda (_) #f))]
+         [(lookup (current-tvars) (syntax-e #'id) (lambda (_) #f))
+          =>
+          (lambda (e) (cond [(DottedBoth? e) (Dotted-t e)]
+                            [(Dotted? e)
+                             (tc-error "Type variable ~a must be used with ..." (syntax-e #'id))]
+                            [else e]))]
          ;; if it's a type alias, we expand it (the expanded type is stored in the HT)
          [(lookup-type-alias #'id parse-type (lambda () #f))
           =>
diff --git a/collects/typed-scheme/private/subtype.ss b/collects/typed-scheme/private/subtype.ss
index 5ba4a72c..01698ffb 100644
--- a/collects/typed-scheme/private/subtype.ss
+++ b/collects/typed-scheme/private/subtype.ss
@@ -198,7 +198,7 @@
               ;; use unification to see if we can use the polytype here
               [(list (Poly: vs b) s)
                (=> unmatch)
-               (if (unify vs (list b) (list s)) A0 (unmatch))]
+               (if (unify vs (list b) (list s)) A0 (unmatch))]              
               [(list s (Poly: vs b))
                (=> unmatch)
                (if (null? (fv b)) (subtype* A0 s b) (unmatch))]
diff --git a/collects/typed-scheme/private/type-effect-printer.ss b/collects/typed-scheme/private/type-effect-printer.ss
index 2a5dac4d..afe034df 100644
--- a/collects/typed-scheme/private/type-effect-printer.ss
+++ b/collects/typed-scheme/private/type-effect-printer.ss
@@ -103,7 +103,7 @@
     [(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))]
     [(Param: in out) 
      (if (equal? in out)

From 0085310b4f00a16590fe97b15087cae036bb5cf6 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Tue, 10 Jun 2008 16:38:14 -0400
Subject: [PATCH 09/96] Use new * syntax in prims. Handle extra tables in
 infer.

original commit: 975f26b93d9372f46960a42915d06702e9be9b49
---
 collects/typed-scheme/private/prims.ss | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/collects/typed-scheme/private/prims.ss b/collects/typed-scheme/private/prims.ss
index 862ad929..2390e0f5 100644
--- a/collects/typed-scheme/private/prims.ss
+++ b/collects/typed-scheme/private/prims.ss
@@ -96,7 +96,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
 (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 ..))]
+    [([var : ty] ... . [rest : rest-ty]) (syntax/loc stx (ty ... rest-ty *))]
     [_
      (let loop ([stx stx])
        (syntax-case stx ()

From 15f6c532e684d56ca0699b9c7983480e8528119b Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Tue, 10 Jun 2008 16:40:05 -0400
Subject: [PATCH 10/96] Changes to tests for ...

original commit: 4ae41412579f7c6daa1d2b527897a50d4f098ea7
---
 .../tests/typed-scheme/succeed/inst-dots.ss   |  7 ++++++
 .../tests/typed-scheme/succeed/metrics.ss     |  4 ++--
 .../typed-scheme/succeed/poly-subtype.ss      | 20 ++++++++++++++++
 .../tests/typed-scheme/succeed/random-bits.ss |  4 ++--
 .../typed-scheme/succeed/varargs-tests.ss     |  4 ++--
 .../typed-scheme/unit-tests/all-tests.ss      |  5 +++-
 .../typed-scheme/unit-tests/infer-tests.ss    |  4 +++-
 .../unit-tests/parse-type-tests.ss            |  2 +-
 .../unit-tests/remove-intersect-tests.ss      |  2 +-
 .../typed-scheme/unit-tests/subst-tests.ss    | 23 +++++++++++++++++++
 .../typed-scheme/unit-tests/subtype-tests.ss  |  2 +-
 11 files changed, 66 insertions(+), 11 deletions(-)
 create mode 100644 collects/tests/typed-scheme/succeed/inst-dots.ss
 create mode 100644 collects/tests/typed-scheme/succeed/poly-subtype.ss
 create mode 100644 collects/tests/typed-scheme/unit-tests/subst-tests.ss

diff --git a/collects/tests/typed-scheme/succeed/inst-dots.ss b/collects/tests/typed-scheme/succeed/inst-dots.ss
new file mode 100644
index 00000000..9e3f138b
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/inst-dots.ss
@@ -0,0 +1,7 @@
+#lang typed-scheme
+
+(require typed-scheme/private/extra-procs)
+
+((inst map* Number Number Number Number Number Number Number) 
+ + 
+ (list 1 2 3) (list 2 3 4) (list 1 2 3) (list 2 3 4) (list 1 2 3) (list 2 3 4))
diff --git a/collects/tests/typed-scheme/succeed/metrics.ss b/collects/tests/typed-scheme/succeed/metrics.ss
index 150261ab..f5d49d8a 100644
--- a/collects/tests/typed-scheme/succeed/metrics.ss
+++ b/collects/tests/typed-scheme/succeed/metrics.ss
@@ -14,9 +14,9 @@
 (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: (lib "48.ss" "srfi")))
+#;(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")
diff --git a/collects/tests/typed-scheme/succeed/poly-subtype.ss b/collects/tests/typed-scheme/succeed/poly-subtype.ss
new file mode 100644
index 00000000..39288d79
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/poly-subtype.ss
@@ -0,0 +1,20 @@
+#lang typed-scheme
+
+(: f (All (a) (a -> a)))
+(define (f x) x)
+
+(define: x : (Number -> Number) f)
+
+#;
+((lambda: ([f : (All (a ...) (a ... a -> Number))]) 12)
+ +)
+
+#;(Lambda (a ...)
+  ((lambda: ([f : (a .. a -> Number)]) 12) +))
+
+#|
+(: g (All (a ...) ((a ... a -> Number) -> Number)))
+
+(define (g x) 3)
+
+|#
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/random-bits.ss b/collects/tests/typed-scheme/succeed/random-bits.ss
index 094cb2f4..f926e07f 100644
--- a/collects/tests/typed-scheme/succeed/random-bits.ss
+++ b/collects/tests/typed-scheme/succeed/random-bits.ss
@@ -38,7 +38,7 @@
                                        [randomize! : ( -> Void)]
                                        [pseudo-randomize! : (Integer Integer -> Void)]
                                        [make-integers : (-> (Integer -> Integer)) ] 
-                                       [make-reals : ( Nb .. -> ( -> Number))])) 
+                                       [make-reals : ( Nb * -> ( -> Number))])) 
   (define-type-alias Random :random-source)
   (define: (:random-source-make 
             [state-ref : ( -> SpList)]
@@ -46,7 +46,7 @@
             [randomize! : ( -> Void)]
             [pseudo-randomize! : (Integer Integer -> Void)]
             [make-integers : (-> (Integer -> Integer)) ] 
-            [make-reals : (Nb .. -> (-> Number))])
+            [make-reals : (Nb * -> (-> Number))])
             : Random
     (make-:random-source state-ref state-set! randomize! pseudo-randomize! make-integers make-reals ))
   
diff --git a/collects/tests/typed-scheme/succeed/varargs-tests.ss b/collects/tests/typed-scheme/succeed/varargs-tests.ss
index 0ebacce8..2bb528aa 100644
--- a/collects/tests/typed-scheme/succeed/varargs-tests.ss
+++ b/collects/tests/typed-scheme/succeed/varargs-tests.ss
@@ -17,11 +17,11 @@
 (apply + '(2 3 4))
 
 
-(define: f : (number boolean .. -> number)
+(define: f : (number boolean * -> number)
   (lambda: ([x : number] . [y : boolean])
            (if (and (pair? y) (car y)) x (- x))))
 
-(define: f-cl : (number boolean .. -> number)
+(define: f-cl : (number boolean * -> number)
   (case-lambda: [([x : number] . [y : boolean])
 		 (if (and (pair? y) (car y)) x (- x))]))
 
diff --git a/collects/tests/typed-scheme/unit-tests/all-tests.ss b/collects/tests/typed-scheme/unit-tests/all-tests.ss
index 2e069f7f..aca0a4d1 100644
--- a/collects/tests/typed-scheme/unit-tests/all-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/all-tests.ss
@@ -9,14 +9,17 @@
  "parse-type-tests.ss" ;; done
  "type-annotation-test.ss" ;; done
  "module-tests.ss"
+ "subst-tests.ss"
  "infer-tests.ss")
 
-(require (private planet-requires))
+(require (private planet-requires infer infer-dummy))
 
 (require (schemeunit))
 
 (provide unit-tests)
 
+(infer-param infer)
+
 (define unit-tests
   (apply
    test-suite 
diff --git a/collects/tests/typed-scheme/unit-tests/infer-tests.ss b/collects/tests/typed-scheme/unit-tests/infer-tests.ss
index 27726a74..9dc58305 100644
--- a/collects/tests/typed-scheme/unit-tests/infer-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/infer-tests.ss
@@ -1,6 +1,6 @@
 #lang scheme/base
 (require "test-utils.ss" (for-syntax scheme/base))
-(require (private planet-requires type-effect-convenience type-rep unify union infer-ops type-utils)
+(require (private planet-requires type-effect-convenience type-rep unify union infer type-utils)
          (prefix-in table: (private tables)))
 (require (schemeunit)) 
 
@@ -25,6 +25,8 @@
               [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) ...)
diff --git a/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss b/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss
index cf8d0644..ded0c48f 100644
--- a/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss
@@ -69,7 +69,7 @@
    [(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)]
diff --git a/collects/tests/typed-scheme/unit-tests/remove-intersect-tests.ss b/collects/tests/typed-scheme/unit-tests/remove-intersect-tests.ss
index ea874f36..ca83402b 100644
--- a/collects/tests/typed-scheme/unit-tests/remove-intersect-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/remove-intersect-tests.ss
@@ -1,6 +1,6 @@
 #lang scheme/base
 (require "test-utils.ss" (for-syntax scheme/base))
-(require (private type-rep type-effect-convenience planet-requires remove-intersect unify subtype union infer-ops))
+(require (private type-rep type-effect-convenience planet-requires remove-intersect subtype union infer))
 
 (require (schemeunit))
 
diff --git a/collects/tests/typed-scheme/unit-tests/subst-tests.ss b/collects/tests/typed-scheme/unit-tests/subst-tests.ss
new file mode 100644
index 00000000..6c89d4ef
--- /dev/null
+++ b/collects/tests/typed-scheme/unit-tests/subst-tests.ss
@@ -0,0 +1,23 @@
+#lang scheme/base
+
+(require "test-utils.ss" (for-syntax scheme/base))
+(require (private planet-requires type-utils type-effect-convenience type-rep))
+(require (schemeunit))
+
+(define-syntax-rule (s img var tgt result)
+  (test-eq? "test" (substitute img 'var tgt) result))
+
+(define-syntax-rule (s... imgs var tgt result)
+  (test-eq? "test" (substitute-dots (list . imgs) 'var tgt) result))
+
+(define (subst-tests)
+  (test-suite "Tests for substitution"
+              (s N a (-v a) N)
+              (s... (N B) a (make-Function (list (make-arr-dots null N (-v a) 'a))) (N B . -> . N))
+              (s... (N B) a (make-Function (list (make-arr-dots (list -String) N (-v a) 'a))) (-String N B . -> . N))
+              (s... (N B) a (make-Function (list (make-arr-dots (list -String) N (-v b) 'a))) (-String (-v b) (-v b) . -> . N))
+              (s... (N B) a (make-Function (list (make-arr-dots (list -String) N (-v b) 'b))) 
+                    (make-Function (list (make-arr-dots (list -String) N (-v b) 'b))))))
+
+(define-go subst-tests)
+
diff --git a/collects/tests/typed-scheme/unit-tests/subtype-tests.ss b/collects/tests/typed-scheme/unit-tests/subtype-tests.ss
index 2f8f4506..f4bc9912 100644
--- a/collects/tests/typed-scheme/unit-tests/subtype-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/subtype-tests.ss
@@ -3,7 +3,7 @@
 (require "test-utils.ss")
 
 (require (private subtype type-rep type-effect-convenience 
-                  planet-requires init-envs type-environments union))
+                  planet-requires init-envs type-environments union infer infer-dummy))
 
 (require (schemeunit)
          (for-syntax scheme/base))

From f750b30c2f902f0caeeabef77332e2c51efd8c96 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Wed, 11 Jun 2008 11:41:46 -0400
Subject: [PATCH 11/96] Added new test for constraint solving on starred
 functions with different fixed arg lengths.

original commit: 97847c32c4dd3d55baa3ff2b7a5ac9f7ed0b83fe
---
 collects/tests/typed-scheme/succeed/star-sizes.ss     | 6 ++++++
 collects/tests/typed-scheme/unit-tests/infer-tests.ss | 2 +-
 2 files changed, 7 insertions(+), 1 deletion(-)
 create mode 100644 collects/tests/typed-scheme/succeed/star-sizes.ss

diff --git a/collects/tests/typed-scheme/succeed/star-sizes.ss b/collects/tests/typed-scheme/succeed/star-sizes.ss
new file mode 100644
index 00000000..6d04d748
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/star-sizes.ss
@@ -0,0 +1,6 @@
+#lang typed-scheme
+
+(: f (All (a) ((Integer a * -> Integer) -> Integer)))
+(define (f g) 0)
+
+(f +)
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/unit-tests/infer-tests.ss b/collects/tests/typed-scheme/unit-tests/infer-tests.ss
index 9dc58305..46a30545 100644
--- a/collects/tests/typed-scheme/unit-tests/infer-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/infer-tests.ss
@@ -1,6 +1,6 @@
 #lang scheme/base
 (require "test-utils.ss" (for-syntax scheme/base))
-(require (private planet-requires type-effect-convenience type-rep unify union infer type-utils)
+(require (private planet-requires type-effect-convenience type-rep union infer type-utils)
          (prefix-in table: (private tables)))
 (require (schemeunit)) 
 

From 4ec8076d0d6d78bb5329f228661bb0445dc28bd6 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Wed, 11 Jun 2008 17:16:40 -0400
Subject: [PATCH 12/96] Fix case-lambda type printing. Begin work on handling
 case-lambda/varargs in ... inference. Implement hash-union, and use to fix
 big bugs.

original commit: 457339d9a8876422153af0731d83bc93fdcc993a
---
 collects/typed-scheme/private/type-effect-printer.ss | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/collects/typed-scheme/private/type-effect-printer.ss b/collects/typed-scheme/private/type-effect-printer.ss
index afe034df..e7554d22 100644
--- a/collects/typed-scheme/private/type-effect-printer.ss
+++ b/collects/typed-scheme/private/type-effect-printer.ss
@@ -97,7 +97,12 @@
        (match arities
          [(list) (fp "(case-lambda)")]
          [(list a) (print-arr a)]
-         [(list a ...) (fp "(case-lambda ") (for-each print-arr a) (fp ")")]))]
+         [(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)]

From 87d8bc5bc8d73903b545b6be04595def12060c44 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Wed, 11 Jun 2008 17:16:58 -0400
Subject: [PATCH 13/96] Add new tests

original commit: eb9147a0fa4048647a328d994eddd979e4c3a7fa
---
 collects/tests/typed-scheme/fail/infer-dots.ss    | 10 ++++++++++
 collects/tests/typed-scheme/succeed/infer-dots.ss | 10 ++++++++++
 2 files changed, 20 insertions(+)
 create mode 100644 collects/tests/typed-scheme/fail/infer-dots.ss
 create mode 100644 collects/tests/typed-scheme/succeed/infer-dots.ss

diff --git a/collects/tests/typed-scheme/fail/infer-dots.ss b/collects/tests/typed-scheme/fail/infer-dots.ss
new file mode 100644
index 00000000..8ee72fb5
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/infer-dots.ss
@@ -0,0 +1,10 @@
+#lang typed-scheme
+
+(require typed-scheme/private/extra-procs)
+
+#;(map* + (list 1 2 3) (list 10 20 30) (list 'a 'b 'c))
+
+(: g (Integer Integer Integer  -> Integer))
+(define (g x y  z) 0)
+
+(map* g (list 1 2 3) (list 4 5 6))
diff --git a/collects/tests/typed-scheme/succeed/infer-dots.ss b/collects/tests/typed-scheme/succeed/infer-dots.ss
new file mode 100644
index 00000000..63ad19a5
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/infer-dots.ss
@@ -0,0 +1,10 @@
+#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))
\ No newline at end of file

From c5e99e9f54eff90920da224e1ce04b1d6468e597 Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Thu, 12 Jun 2008 14:08:23 -0400
Subject: [PATCH 14/96] Add fixed-args mismatch between starred/dotted
 functions.

original commit: 6da5171b2883610e2da221963926630814f5ad21
---
 collects/tests/typed-scheme/fail/infer-dots.ss | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/collects/tests/typed-scheme/fail/infer-dots.ss b/collects/tests/typed-scheme/fail/infer-dots.ss
index 8ee72fb5..6173f66b 100644
--- a/collects/tests/typed-scheme/fail/infer-dots.ss
+++ b/collects/tests/typed-scheme/fail/infer-dots.ss
@@ -4,7 +4,15 @@
 
 #;(map* + (list 1 2 3) (list 10 20 30) (list 'a 'b 'c))
 
-(: g (Integer Integer Integer  -> Integer))
-(define (g x y  z) 0)
+;; Arity mismatch.
+(: g (Integer Integer Integer -> Integer))
+(define (g x y z) 0)
 
 (map* g (list 1 2 3) (list 4 5 6))
+
+;; Can't use a starred function with more fixed args
+;; for a dotted function.
+(: h (Integer Integer Integer * -> Integer))
+(define (h x y . z) 0)
+
+(map* h (list 1 2 3) (list 4 5 6))

From 459a5f8f8e2004ad236c53e30fb1d714737b2023 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Thu, 12 Jun 2008 17:10:31 -0400
Subject: [PATCH 15/96] Implement dmap operations. Remove lots of unneeded
 requires. Add in-list-forever and extend to utils.ss Add optional variable
 argument to c-meet.

original commit: e2c0b4e6427ba184e2204f4f7be96f8a09b3430e
---
 collects/typed-scheme/typed-scheme.ss | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/collects/typed-scheme/typed-scheme.ss b/collects/typed-scheme/typed-scheme.ss
index 939c49d5..f01ba63b 100644
--- a/collects/typed-scheme/typed-scheme.ss
+++ b/collects/typed-scheme/typed-scheme.ss
@@ -12,7 +12,7 @@
           "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"

From f72b9f1e134306e5094d292da3f46685cbdc3a78 Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Fri, 13 Jun 2008 12:08:43 -0400
Subject: [PATCH 16/96] Test cases that should succeed and fail for star/dots
 mixes.

original commit: df91f204d21f1f345dd0fc9ee69004edd2eb7dc7
---
 collects/tests/typed-scheme/fail/infer-dots.ss    | 6 ++----
 collects/tests/typed-scheme/succeed/infer-dots.ss | 9 ++++++++-
 2 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/collects/tests/typed-scheme/fail/infer-dots.ss b/collects/tests/typed-scheme/fail/infer-dots.ss
index 6173f66b..7ef4ad21 100644
--- a/collects/tests/typed-scheme/fail/infer-dots.ss
+++ b/collects/tests/typed-scheme/fail/infer-dots.ss
@@ -2,7 +2,7 @@
 
 (require typed-scheme/private/extra-procs)
 
-#;(map* + (list 1 2 3) (list 10 20 30) (list 'a 'b 'c))
+(map* + (list 1 2 3) (list 10 20 30) (list 'a 'b 'c))
 
 ;; Arity mismatch.
 (: g (Integer Integer Integer -> Integer))
@@ -10,9 +10,7 @@
 
 (map* g (list 1 2 3) (list 4 5 6))
 
-;; Can't use a starred function with more fixed args
-;; for a dotted function.
 (: h (Integer Integer Integer * -> Integer))
 (define (h x y . z) 0)
 
-(map* h (list 1 2 3) (list 4 5 6))
+(map* h (list 1 2 3))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/infer-dots.ss b/collects/tests/typed-scheme/succeed/infer-dots.ss
index 63ad19a5..1e450452 100644
--- a/collects/tests/typed-scheme/succeed/infer-dots.ss
+++ b/collects/tests/typed-scheme/succeed/infer-dots.ss
@@ -7,4 +7,11 @@
 
 (map* f (list 1 2 3) (list 10 20 30))
 
-#;(map* + (list 1 2 3) (list 10 20 30) (list 10 20 30))
\ No newline at end of file
+(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) 0)
+
+(map* h (list 1 2 3) (list 4 5 6))
\ No newline at end of file

From 286e9b8510f5a6035785851ff2cb4d1a42c5d0f6 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Fri, 13 Jun 2008 17:04:22 -0400
Subject: [PATCH 17/96] More testing.

original commit: 27073e07fd8e48e74451937195867d5d134554c1
---
 collects/tests/typed-scheme/succeed/infer-dots.ss | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/collects/tests/typed-scheme/succeed/infer-dots.ss b/collects/tests/typed-scheme/succeed/infer-dots.ss
index 1e450452..be670b35 100644
--- a/collects/tests/typed-scheme/succeed/infer-dots.ss
+++ b/collects/tests/typed-scheme/succeed/infer-dots.ss
@@ -12,6 +12,7 @@
 (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) 0)
+(define (h x y . z) (apply + (cons x (cons y z))))
 
-(map* h (list 1 2 3) (list 4 5 6))
\ No newline at end of file
+(map* h (list 1 2 3) (list 4 5 6))
+(map* h (list 1 2 3) (list 4 5 6) (list 4 5 6))

From 1f15e359254e6cf33dfea689f38a9bf4110c8b37 Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Sun, 15 Jun 2008 15:56:44 -0400
Subject: [PATCH 18/96] I don't see how this isn't a bug.

original commit: 14da71b5c240b248d97be77ffd4c220af3ef6146
---
 collects/typed-scheme/private/type-effect-convenience.ss | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss
index 73c11ef9..22205b8d 100644
--- a/collects/typed-scheme/private/type-effect-convenience.ss
+++ b/collects/typed-scheme/private/type-effect-convenience.ss
@@ -41,7 +41,7 @@
     [(_ dom ... rng)
      (->* (list dom ...) rng)]
     [(_ dom ... rng : eff1 eff2)
-     (->* (list dom ...) : eff1 eff2)]))
+     (->* (list dom ...) rng : eff1 eff2)]))
 (define-syntax ->*
   (syntax-rules (:)
     [(_ dom rng)       

From b760e45d17fde49376bac987865186c56b795970 Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Mon, 16 Jun 2008 13:01:16 -0400
Subject: [PATCH 19/96] Change over some of the base environment over to dotted
 types.

original commit: c4e253d2d18020b428612227dac6bd789b59d43c
---
 collects/typed-scheme/private/base-env.ss     | 25 ++++++++-----------
 .../private/type-effect-convenience.ss        | 17 +++++++++++++
 2 files changed, 27 insertions(+), 15 deletions(-)

diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 0b8695a3..397aacef 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -1,9 +1,11 @@
+
 #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 rnrs/lists-6 fold-left)
  '#%paramz
  (only-in scheme/match/runtime match:error))
 
@@ -99,11 +101,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 b) (->... (list (->... (list a) (b b) B) (-lst a)) ((-lst b) b) B))]
+     [andmap (-polydots (a b) (->... (list (->... (list a) (b b) B) (-lst a)) ((-lst b) b) B))]
      [newline (cl-> [() -Void]
                     [(-Port) -Void])]
      [not (-> Univ B)]
@@ -122,16 +121,12 @@
      [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) . ->... . -Void) (-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))]
      [foldl
       (-poly (a b c)
              (cl-> [((a b . -> . b) b (make-lst a)) b]
diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss
index 22205b8d..2ceb2f13 100644
--- a/collects/typed-scheme/private/type-effect-convenience.ss
+++ b/collects/typed-scheme/private/type-effect-convenience.ss
@@ -52,6 +52,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] ...)
@@ -114,6 +124,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)

From 5f244e7f427e6f6c8cff2368992e41cfec1abccf Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Mon, 16 Jun 2008 13:26:15 -0400
Subject: [PATCH 20/96] Fix for-each type. Improve ... error messages.

original commit: 2ad440310828bc296223e23db3cdee84ad5fce34
---
 collects/typed-scheme/private/base-env.ss | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 397aacef..a671316e 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -123,7 +123,7 @@
      [procedure? (make-pred-ty (make-Function (list (make-top-arr))))]
      [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) . ->... . -Void) (-lst a))
+     [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))]

From 12aef5cc7e913f5d91d3b7fd2a316d72c81f6264 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Mon, 16 Jun 2008 13:27:59 -0400
Subject: [PATCH 21/96] Remove map*

original commit: fdb780fb00cb13fbdd1bd08c544af092f75aeb44
---
 collects/typed-scheme/private/base-env.ss    | 16 +---------------
 collects/typed-scheme/private/extra-procs.ss |  3 +--
 2 files changed, 2 insertions(+), 17 deletions(-)

diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index a671316e..d11d5a64 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -492,21 +492,7 @@
      [identifier? (make-pred-ty (-Syntax Sym))]
      [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))))]
-     
+                                        (-> (-Syntax Univ) Univ Univ)))]     
      )))
 
 (begin-for-syntax 
diff --git a/collects/typed-scheme/private/extra-procs.ss b/collects/typed-scheme/private/extra-procs.ss
index 428b5eaf..e2c6b97b 100644
--- a/collects/typed-scheme/private/extra-procs.ss
+++ b/collects/typed-scheme/private/extra-procs.ss
@@ -1,11 +1,10 @@
 #lang scheme/base
-(provide assert map*)
+(provide assert)
 
 (define (assert v)
   (unless v
     (error "Assertion failed - value was #f"))
   v)
 
-(define map* map)
 
 

From 2afa0ac8f1b17a24bfca69634deb5f08187ef8fb Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Mon, 16 Jun 2008 13:28:27 -0400
Subject: [PATCH 22/96] Change map* to map.

original commit: a43b2f5681c576e9b22ff7926ca48ddacfcbcfc2
---
 collects/tests/typed-scheme/fail/infer-dots.ss    |  6 +++---
 collects/tests/typed-scheme/succeed/infer-dots.ss | 10 +++++-----
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/collects/tests/typed-scheme/fail/infer-dots.ss b/collects/tests/typed-scheme/fail/infer-dots.ss
index 7ef4ad21..40dea049 100644
--- a/collects/tests/typed-scheme/fail/infer-dots.ss
+++ b/collects/tests/typed-scheme/fail/infer-dots.ss
@@ -2,15 +2,15 @@
 
 (require typed-scheme/private/extra-procs)
 
-(map* + (list 1 2 3) (list 10 20 30) (list 'a 'b 'c))
+(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))
+(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))
\ No newline at end of file
+(map h (list 1 2 3))
diff --git a/collects/tests/typed-scheme/succeed/infer-dots.ss b/collects/tests/typed-scheme/succeed/infer-dots.ss
index be670b35..89892336 100644
--- a/collects/tests/typed-scheme/succeed/infer-dots.ss
+++ b/collects/tests/typed-scheme/succeed/infer-dots.ss
@@ -5,14 +5,14 @@
 (: f (Integer Integer -> Integer))
 (define (f x y) (+ x y))
 
-(map* f (list 1 2 3) (list 10 20 30))
+(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))
 
-(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))
+(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))
+(map h (list 1 2 3) (list 4 5 6))
+(map h (list 1 2 3) (list 4 5 6) (list 4 5 6))

From 8d9ca01cf51cbe139960fbb83aaeed2a72db8db3 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Mon, 16 Jun 2008 16:34:09 -0400
Subject: [PATCH 23/96] Source location in synthetic module begin.

original commit: 055eb3cd0b2b1f57d79808c40e3dc5566b94d65b
---
 collects/typed-scheme/typed-scheme.ss | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/collects/typed-scheme/typed-scheme.ss b/collects/typed-scheme/typed-scheme.ss
index f01ba63b..63fc8ba7 100644
--- a/collects/typed-scheme/typed-scheme.ss
+++ b/collects/typed-scheme/typed-scheme.ss
@@ -70,8 +70,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])]

From 31f40113879387b7e43c6507913b10036b566ac7 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Mon, 16 Jun 2008 16:47:08 -0400
Subject: [PATCH 24/96] Definition (but not use) of ... vars

original commit: 1b998d7eb8b2f35d5daf0f991bf33fc45bd4e06d
---
 collects/typed-scheme/private/base-env.ss     |  2 +-
 collects/typed-scheme/private/parse-type.ss   |  5 -----
 collects/typed-scheme/private/prims.ss        | 22 ++++++++++++++++---
 .../typed-scheme/private/type-annotation.ss   | 16 +++++++++-----
 collects/typed-scheme/private/type-utils.ss   | 10 +++++++--
 5 files changed, 38 insertions(+), 17 deletions(-)

diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index d11d5a64..95df2174 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -492,7 +492,7 @@
      [identifier? (make-pred-ty (-Syntax Sym))]
      [syntax? (make-pred-ty (-Syntax Univ))]
      [syntax-property (-poly (a) (cl->* (-> (-Syntax a) Univ Univ (-Syntax a))
-                                        (-> (-Syntax Univ) Univ Univ)))]     
+                                        (-> (-Syntax Univ) Univ Univ)))]
      )))
 
 (begin-for-syntax 
diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss
index 5565a9d9..686bd2b1 100644
--- a/collects/typed-scheme/private/parse-type.ss
+++ b/collects/typed-scheme/private/parse-type.ss
@@ -24,11 +24,6 @@
 
 (define (stx-cadr stx) (stx-car (stx-cdr stx)))
 
-;; t is (make-F v)
-(define-struct Dotted (t))
-(define-struct (DottedBoth Dotted) ())
-
-
 (define (parse-type stx)    
   (parameterize ([current-orig-stx stx])
     (syntax-case* stx ()
diff --git a/collects/typed-scheme/private/prims.ss b/collects/typed-scheme/private/prims.ss
index 2390e0f5..80facd1e 100644
--- a/collects/typed-scheme/private/prims.ss
+++ b/collects/typed-scheme/private/prims.ss
@@ -96,7 +96,11 @@ This file defines two sorts of primitives. All of them are provided into any mod
 (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 *))]
+    [([var : ty] ... . [rest : rest-ty]) 
+     (syntax/loc stx (ty ... rest-ty *))]
+    [([var : ty] ... . [rest : rest-ty ddd bound])
+     (eq? '... (syntax-e #'ddd))
+     (syntax/loc stx (ty ... rest-ty ddd bound))]
     [_
      (let loop ([stx stx])
        (syntax-case stx ()
@@ -139,7 +143,12 @@ This file defines two sorts of primitives. All of them are provided into any mod
     [(_ arg : ty)
      (syntax-property #'arg 'type-ascription #'ty)]
     [(_ arg ty)
-     (syntax-property #'arg 'type-ascription #'ty)]))
+     (syntax-property #'arg 'type-ascription #'ty)]
+    [(_ arg ty ddd bound)
+     (eq? '... (syntax-e #'ddd))
+     (syntax-property (syntax-property #'arg 'type-ascription #'ty)
+                      'type-dotted 
+                      #'bound)]))
 
 (define-syntax (: stx)
   (let ([stx*
@@ -198,12 +207,19 @@ This file defines two sorts of primitives. All of them are provided into any mod
     (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))]))       
+     (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))]))
 
 (define-syntax-rule (λ: . args) (lambda: . args))
 
diff --git a/collects/typed-scheme/private/type-annotation.ss b/collects/typed-scheme/private/type-annotation.ss
index d9875ef4..ec214068 100644
--- a/collects/typed-scheme/private/type-annotation.ss
+++ b/collects/typed-scheme/private/type-annotation.ss
@@ -8,11 +8,14 @@
          get-type/infer
          type-label-symbol
          type-ascrip-symbol
+         type-dotted-symbol
          type-ascription
-         check-type)
+         check-type
+         dotted?)
 
 (define type-label-symbol 'type-label)
-(define type-ascrip-symbol 'type-ascription)    
+(define type-ascrip-symbol 'type-ascription)
+(define type-dotted-symbol 'type-dotted)
 
 (define (print-size stx)
   (syntax-case stx ()
@@ -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
@@ -121,3 +121,7 @@
       (unless (subtype e-type ty)
         ;(printf "orig-stx: ~a" (syntax->datum stx*))
         (tc-error "Body had type:~n~a~nVariable had type:~n~a~n" e-type ty)))))
+
+(define (dotted? stx)
+  (cond [(syntax-property stx type-dotted-symbol) => syntax-e]
+        [else #f]))
\ No newline at end of file
diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index 621f6aab..21b4c5f5 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -4,7 +4,7 @@
          "effect-rep.ss"
          "tc-utils.ss"
          "rep-utils.ss"
-         "free-variance.ss"
+         (only-in "free-variance.ss" combine-frees)
          mzlib/plt-match
          scheme/list
          (for-syntax scheme/base))
@@ -20,7 +20,9 @@
          tc-result-equal? 
          effects-equal?
          tc-result-t
-         unfold)
+         unfold
+         (struct-out Dotted)
+         (struct-out DottedBoth))
 
 
 ;; substitute : Type Name Type -> Type
@@ -129,3 +131,7 @@
 
 ;; 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) ())
\ No newline at end of file

From e3734750dbdaeca776710447ea76b73c1493f311 Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Mon, 16 Jun 2008 19:02:45 -0400
Subject: [PATCH 25/96] Add examples of each.

original commit: bcb205a9303bdda29c94f5239e919ceef90145bb
---
 collects/tests/typed-scheme/succeed/dot-intro.ss | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 collects/tests/typed-scheme/succeed/dot-intro.ss

diff --git a/collects/tests/typed-scheme/succeed/dot-intro.ss b/collects/tests/typed-scheme/succeed/dot-intro.ss
new file mode 100644
index 00000000..7afb8c1a
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/dot-intro.ss
@@ -0,0 +1,9 @@
+#lang typed-scheme
+
+(define x
+  (plambda: (a ...) ([x : Number] . [y : Number ... a])
+    (ormap zero? (map add1 y))))
+
+(define y
+  (plambda: (a ...) ([x : Number] . [y : a ... a])
+    (ormap null? (map list y))))
\ No newline at end of file

From ca3e58f3a69aac6a1d0b94a6b1f69b76cb8024b2 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Tue, 17 Jun 2008 10:46:39 -0400
Subject: [PATCH 26/96] Use map instead of map*

original commit: c7733e5e34dfb6f22d7ddb07c5e17192a5679b91
---
 collects/tests/typed-scheme/succeed/inst-dots.ss | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/collects/tests/typed-scheme/succeed/inst-dots.ss b/collects/tests/typed-scheme/succeed/inst-dots.ss
index 9e3f138b..51bf3223 100644
--- a/collects/tests/typed-scheme/succeed/inst-dots.ss
+++ b/collects/tests/typed-scheme/succeed/inst-dots.ss
@@ -2,6 +2,6 @@
 
 (require typed-scheme/private/extra-procs)
 
-((inst map* Number Number Number Number Number Number Number) 
+((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))

From a313b99999ed1221beecd1ab92436665561697dc Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Tue, 17 Jun 2008 12:57:29 -0400
Subject: [PATCH 27/96] Add handling of dotted functions when not wrapped with
 a big lambda.

original commit: 1bef5f9d0b7af964d904575dc6976d132ba76b5c
---
 collects/typed-scheme/private/type-effect-convenience.ss | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss
index 2ceb2f13..b18e8bd1 100644
--- a/collects/typed-scheme/private/type-effect-convenience.ss
+++ b/collects/typed-scheme/private/type-effect-convenience.ss
@@ -164,9 +164,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))))

From 265f9c900988e2d3d4d96f072ee7e7c81ef3a373 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Tue, 17 Jun 2008 12:58:15 -0400
Subject: [PATCH 28/96] Adding testcases for dotted function application to
 rest args via apply.

original commit: 93c937f909b431fa64c49515ae66d87f42711e2b
---
 .../tests/typed-scheme/fail/apply-dots.ss     | 11 +++++++++++
 .../tests/typed-scheme/succeed/apply-dots.ss  | 19 +++++++++++++++++++
 2 files changed, 30 insertions(+)
 create mode 100644 collects/tests/typed-scheme/fail/apply-dots.ss
 create mode 100644 collects/tests/typed-scheme/succeed/apply-dots.ss

diff --git a/collects/tests/typed-scheme/fail/apply-dots.ss b/collects/tests/typed-scheme/fail/apply-dots.ss
new file mode 100644
index 00000000..6dde0cf9
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/apply-dots.ss
@@ -0,0 +1,11 @@
+#lang typed-scheme
+
+(plambda: (a ...) ([z : String] . [w : Number])
+          (apply (case-lambda: (([x : Number] . [y : Number ... a]) x))
+                 w))
+
+(plambda: (a ...) ([z : String] . [w : Number])
+          (apply (case-lambda: (([x : Number] . [y : Number ... a]) x)
+                               (([x : String] [y : String] . [z : String]) 0)
+                               ([y : String] 0))
+                 w))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/apply-dots.ss b/collects/tests/typed-scheme/succeed/apply-dots.ss
new file mode 100644
index 00000000..506f11a7
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/apply-dots.ss
@@ -0,0 +1,19 @@
+#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))
\ No newline at end of file

From 64c709bbb70b2bf67c453921143d5da493369a00 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Tue, 17 Jun 2008 14:28:41 -0400
Subject: [PATCH 29/96] New tests

original commit: 59e2dc4dea772cae5af0a2c7b72b1737864afb20
---
 collects/tests/typed-scheme/unit-tests/typecheck-tests.ss | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
index a3fe2ffe..139956cc 100644
--- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
@@ -544,6 +544,10 @@
         
         [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))]
+        
         ;; error tests
         [tc-err (#%variable-reference number?)]
         [tc-err (+ 3 #f)]

From 2a935208e9ff3dec02f5051b1d33731ab79aa339 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Tue, 17 Jun 2008 16:24:30 -0400
Subject: [PATCH 30/96] New tests

original commit: 3f180f88daf777504d1d210cb9115118cab629b8
---
 collects/tests/typed-scheme/unit-tests/typecheck-tests.ss | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
index 139956cc..11047522 100644
--- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
@@ -547,6 +547,9 @@
         [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)))]
         
         ;; error tests
         [tc-err (#%variable-reference number?)]

From 4853428482138ac4d61b268ac367c417cde7b956 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Tue, 17 Jun 2008 16:28:34 -0400
Subject: [PATCH 31/96] Don't produce extra errors for top-level defines. Lots
 more error message improvements for application. Work on polydots apply.
 Extend environment only in the proper place in plambda. Don't let a variable
 unify with a dotted variable.

original commit: c8a2810742514c9f78b006930e6f327794af0228
---
 collects/typed-scheme/private/type-utils.ss | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index 21b4c5f5..42bf4788 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -22,7 +22,8 @@
          tc-result-t
          unfold
          (struct-out Dotted)
-         (struct-out DottedBoth))
+         (struct-out DottedBoth)
+         just-Dotted?)
 
 
 ;; substitute : Type Name Type -> Type
@@ -134,4 +135,8 @@
 
 ;; t is (make-F v)
 (define-struct Dotted (t))
-(define-struct (DottedBoth Dotted) ())
\ No newline at end of file
+(define-struct (DottedBoth Dotted) ())
+
+(define (just-Dotted? S)
+    (and (Dotted? S)
+         (not (DottedBoth? S))))
\ No newline at end of file

From 4271f734a687b7eb903a2bc99607ff83449d1fca Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Tue, 17 Jun 2008 18:10:17 -0400
Subject: [PATCH 32/96] Checkpoint.

original commit: dfdfae95d7d16ef3fa97503cfa0156101dc275b3
---
 collects/typed-scheme/private/parse-type.ss   | 19 +++++++------------
 .../private/type-effect-convenience.ss        |  3 ---
 collects/typed-scheme/private/type-utils.ss   | 13 +++++++++++--
 3 files changed, 18 insertions(+), 17 deletions(-)

diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss
index 686bd2b1..a5f61ed0 100644
--- a/collects/typed-scheme/private/parse-type.ss
+++ b/collects/typed-scheme/private/parse-type.ss
@@ -73,7 +73,7 @@
          (make-pred-ty (list (parse-type #'dom)) (parse-type #'rng) (parse-type #'pred-ty)))]
       [(dom ... rest ::: -> rng)
        (and (eq? (syntax-e #'->) '->) 
-            (symbolic-identifier=? #'::: (quote-syntax *)))
+            (eq? (syntax-e #':::) '*))
        (begin
          (add-type-name-reference #'->)
          (->* (map parse-type (syntax->list #'(dom ...))) (parse-type #'rest) (parse-type #'rng)))]
@@ -106,17 +106,12 @@
        (-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
diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss
index b18e8bd1..8a1c95ef 100644
--- a/collects/typed-scheme/private/type-effect-convenience.ss
+++ b/collects/typed-scheme/private/type-effect-convenience.ss
@@ -249,8 +249,5 @@
                (exit t)))]
         [_ (exit t)]))))
 
-(define (tc-error/expr msg #:return [return (Un)] #:stx [stx (current-orig-stx)] . rest)
-  (tc-error/delayed #:stx stx (apply format msg rest))
-  return)
 
 
diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index 42bf4788..6d182581 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -23,7 +23,9 @@
          unfold
          (struct-out Dotted)
          (struct-out DottedBoth)
-         just-Dotted?)
+         just-Dotted?
+         tc-error/expr
+         lookup-fail)
 
 
 ;; substitute : Type Name Type -> Type
@@ -139,4 +141,11 @@
 
 (define (just-Dotted? S)
     (and (Dotted? S)
-         (not (DottedBoth? S))))
\ No newline at end of file
+         (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))

From f8ed6299c4cfa13c22de5810d31996fa68fa98b7 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Tue, 17 Jun 2008 18:10:41 -0400
Subject: [PATCH 33/96] More tests.  Not all of them pass yet, but we are
 hopeful.

original commit: 8e498458aa635b201db6c005241d436f644c940d
---
 .../tests/typed-scheme/succeed/apply-dots.ss  | 48 ++++++++++++++++++-
 collects/tests/typed-scheme/succeed/cl-bug.ss | 15 ++++++
 .../tests/typed-scheme/succeed/fold-left.ss   | 19 ++++++++
 .../tests/typed-scheme/succeed/lots-o-bugs.ss | 23 +++++++++
 .../typed-scheme/succeed/unholy-terror.ss     | 30 ++++++++++++
 .../unit-tests/typecheck-tests.ss             | 12 +++++
 6 files changed, 146 insertions(+), 1 deletion(-)
 create mode 100644 collects/tests/typed-scheme/succeed/cl-bug.ss
 create mode 100644 collects/tests/typed-scheme/succeed/fold-left.ss
 create mode 100644 collects/tests/typed-scheme/succeed/lots-o-bugs.ss
 create mode 100644 collects/tests/typed-scheme/succeed/unholy-terror.ss

diff --git a/collects/tests/typed-scheme/succeed/apply-dots.ss b/collects/tests/typed-scheme/succeed/apply-dots.ss
index 506f11a7..4d13e0d9 100644
--- a/collects/tests/typed-scheme/succeed/apply-dots.ss
+++ b/collects/tests/typed-scheme/succeed/apply-dots.ss
@@ -16,4 +16,50 @@
           (apply (case-lambda: (([x : Number] . [y : Number ... a]) x)
                                (([x : String] [y : String] . [z : String]) 0)
                                ([y : Number] 0))
-                 w))
\ No newline at end of file
+                 w))
+
+;; */*/poly
+(plambda: (a ...) ([z : String] . [w : Number])
+          (apply (plambda: (b) ([x : b] . [y : Number]) x)
+                 1 w))
+
+(plambda: (a ...) ([z : String] . [w : Number])
+          (apply (plambda: (b) ([x : b] . [y : Number]) x)
+                 1 2 3 w))
+
+;; */*/polydots
+(plambda: (a ...) ([z : String] . [w : Number])
+          (apply (plambda: (b ...) ([x : Number] . [y : Number]) x)
+                 1 w))
+
+(plambda: (a ...) ([z : String] . [w : Number])
+          (apply (plambda: (b ...) ([x : Number] . [y : Number]) x)
+                 1 1 1 w))
+
+;; */.../poly
+(plambda: (a ...) ([z : String] . [w : Number ... a])
+          (apply (plambda: (b) ([x : Number] . [y : Number]) x)
+                 1 w))
+
+(plambda: (a ...) ([z : String] . [w : Number ... a])
+          (apply (plambda: (b) ([x : Number] . [y : Number]) x)
+                 1 1 1 1 w))
+
+;; */.../polydots
+#;(plambda: (a ...) ([z : String] . [w : Number ... a])
+          (apply (plambda: (b ...) ([x : Number] . [y : Number]) x)
+                 1 w))
+
+#;(plambda: (a ...) ([z : String] . [w : Number ... a])
+          (apply (plambda: (b ...) ([x : Number] . [y : Number]) x)
+                 1 1 1 1 w))
+
+;; .../.../poly
+(plambda: (a ...) ([z : String] . [w : Number ... a])
+          (apply (plambda: (b) ([x : Number] . [y : Number ... a]) x)
+                 1 w))
+
+#;(plambda: (a ...) ([z : String] . [w : Number ... a])
+          (apply (plambda: (b ...) ([x : Number] . [y : Number ... a]) x)
+                 1 w))
+
diff --git a/collects/tests/typed-scheme/succeed/cl-bug.ss b/collects/tests/typed-scheme/succeed/cl-bug.ss
new file mode 100644
index 00000000..6b5a61c6
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/cl-bug.ss
@@ -0,0 +1,15 @@
+#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))
+
+(: f3 (case-lambda (Integer * -> Integer) (Number * -> Number)))
+(define (f3 x y) (+ x y))
+
+(+ 1 'foo)
+
+(: f2 (case-lambda (Number * -> Number)))
+(define (f2 x y) (+ x y))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/fold-left.ss b/collects/tests/typed-scheme/succeed/fold-left.ss
new file mode 100644
index 00000000..5b8c6e73
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/fold-left.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? a)
+          (ormap null? bss))
+      c
+      (apply fold-left f 
+             (apply f c (car as) (map car bss))
+             (cdr as) (map cdr bs))))
+
+(: 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? a)
+          (ormap null? bss))
+      c
+      (apply f
+             (apply fold-left f c (cdr as) (map cdr bs))
+             (car as) (map car bss))))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/lots-o-bugs.ss b/collects/tests/typed-scheme/succeed/lots-o-bugs.ss
new file mode 100644
index 00000000..21e5dd9c
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/lots-o-bugs.ss
@@ -0,0 +1,23 @@
+#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)
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/unholy-terror.ss b/collects/tests/typed-scheme/succeed/unholy-terror.ss
new file mode 100644
index 00000000..4802241a
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/unholy-terror.ss
@@ -0,0 +1,30 @@
+#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 + - * /))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
index 11047522..80afadc0 100644
--- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
@@ -551,6 +551,18 @@
         [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-err (plambda: (a ...) ([z : String] . [w : Number ... a])
+                          (apply (plambda: (b ...) ([x : Number] . [y : Number ... b]) x)
+                                 1 w))]
+        
         ;; error tests
         [tc-err (#%variable-reference number?)]
         [tc-err (+ 3 #f)]

From 9d55a9e5924e74f70b7689aaa1cf952768f9a5c0 Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Wed, 18 Jun 2008 12:31:08 -0400
Subject: [PATCH 34/96]  * Enforce the use of a '*' in list-like rest args.  *
 Abstract out annotation errors so that we can report it in the other case   
 where it's useful.

original commit: c2a53b316be90d81b1af0afd4acb4f22b5dc57c9
---
 collects/typed-scheme/private/prims.ss | 50 ++++++++++++++++----------
 1 file changed, 31 insertions(+), 19 deletions(-)

diff --git a/collects/typed-scheme/private/prims.ss b/collects/typed-scheme/private/prims.ss
index 80facd1e..929430bf 100644
--- a/collects/typed-scheme/private/prims.ss
+++ b/collects/typed-scheme/private/prims.ss
@@ -93,26 +93,32 @@ 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]) 
+    [([var : ty] ... . [rest : rest-ty star])
+     (eq? '* (syntax-e #'star))
      (syntax/loc stx (ty ... rest-ty *))]
     [([var : ty] ... . [rest : rest-ty ddd bound])
      (eq? '... (syntax-e #'ddd))
      (syntax/loc stx (ty ... rest-ty ddd bound))]
-    [_
-     (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)]))]))
+    [_ (formal-annotation-error stx src)]))
 
 
 (define-syntax (plambda: stx)
@@ -144,6 +150,9 @@ This file defines two sorts of primitives. All of them are provided into any mod
      (syntax-property #'arg 'type-ascription #'ty)]
     [(_ arg ty)
      (syntax-property #'arg 'type-ascription #'ty)]
+    [(_ arg ty star)
+     (eq? '* (syntax-e #'star))
+     (syntax-property #'arg 'type-ascription #'ty)]
     [(_ arg ty ddd bound)
      (eq? '... (syntax-e #'ddd))
      (syntax-property (syntax-property #'arg 'type-ascription #'ty)
@@ -200,7 +209,7 @@ 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)
@@ -215,24 +224,27 @@ This file defines two sorts of primitives. All of them are provided into any mod
     [[var : ty] (label-one #'var #'ty)]
     [([var : ty] ...)
      (label #'(var ...) #'(ty ...))]
-    [([var : ty] ... . [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))]))
+     (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:)
@@ -240,7 +252,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 ...))

From 978e6acffa1590c02abcfba3fb5a41aadac292bb Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Wed, 18 Jun 2008 12:45:08 -0400
Subject: [PATCH 35/96] No need for this, it's handled by a case lower down
 (and correctly, so why force changes in two positions?)

original commit: 6a30c9dec99921e7ffff058bbb130b72a2695f55
---
 collects/typed-scheme/private/prims.ss | 1 -
 1 file changed, 1 deletion(-)

diff --git a/collects/typed-scheme/private/prims.ss b/collects/typed-scheme/private/prims.ss
index 929430bf..983ec78e 100644
--- a/collects/typed-scheme/private/prims.ss
+++ b/collects/typed-scheme/private/prims.ss
@@ -221,7 +221,6 @@ This file defines two sorts of primitives. All of them are provided into any mod
                       'type-dotted 
                       bound))
   (syntax-case stx (:)
-    [[var : ty] (label-one #'var #'ty)]
     [([var : ty] ...)
      (label #'(var ...) #'(ty ...))]
     [([var : ty] ... . [rest : rest-ty star])

From a8a55f440a70250b6ec594326fa4a6f6076eb392 Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Wed, 18 Jun 2008 12:57:52 -0400
Subject: [PATCH 36/96]  * Should have used star (bound in syntax-case), not
 just * in type-of-formals  * I'm pretty sure ann should never get a starred
 or dotted type, since those    can't appear outside of an arrow context.

original commit: 4010a39c2d177f56c79ca561f02b00bc082d9bdd
---
 collects/typed-scheme/private/prims.ss | 12 ++----------
 1 file changed, 2 insertions(+), 10 deletions(-)

diff --git a/collects/typed-scheme/private/prims.ss b/collects/typed-scheme/private/prims.ss
index 983ec78e..b9fdfe2e 100644
--- a/collects/typed-scheme/private/prims.ss
+++ b/collects/typed-scheme/private/prims.ss
@@ -114,7 +114,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
     [([var : ty] ...) (quasisyntax/loc stx (ty ...))]
     [([var : ty] ... . [rest : rest-ty star])
      (eq? '* (syntax-e #'star))
-     (syntax/loc stx (ty ... rest-ty *))]
+     (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))]
@@ -149,15 +149,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
     [(_ arg : ty)
      (syntax-property #'arg 'type-ascription #'ty)]
     [(_ arg ty)
-     (syntax-property #'arg 'type-ascription #'ty)]
-    [(_ arg ty star)
-     (eq? '* (syntax-e #'star))
-     (syntax-property #'arg 'type-ascription #'ty)]
-    [(_ arg ty ddd bound)
-     (eq? '... (syntax-e #'ddd))
-     (syntax-property (syntax-property #'arg 'type-ascription #'ty)
-                      'type-dotted 
-                      #'bound)]))
+     (syntax-property #'arg 'type-ascription #'ty)]))
 
 (define-syntax (: stx)
   (let ([stx*

From 9544bcbd1fe6fcb453d316e357e13964d3822596 Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Wed, 18 Jun 2008 13:01:43 -0400
Subject: [PATCH 37/96] Add * where appropriate.

original commit: 4b3508a89004c5334e856ad0f5b6988881097775
---
 .../tests/typed-scheme/succeed/apply-dots.ss  | 36 +++++++++----------
 .../typed-scheme/succeed/leftist-heap.ss      |  2 +-
 .../tests/typed-scheme/succeed/random-bits.ss |  4 +--
 .../typed-scheme/succeed/varargs-tests.ss     |  6 ++--
 .../unit-tests/typecheck-tests.ss             | 26 +++++++-------
 5 files changed, 37 insertions(+), 37 deletions(-)

diff --git a/collects/tests/typed-scheme/succeed/apply-dots.ss b/collects/tests/typed-scheme/succeed/apply-dots.ss
index 4d13e0d9..d7ad17a0 100644
--- a/collects/tests/typed-scheme/succeed/apply-dots.ss
+++ b/collects/tests/typed-scheme/succeed/apply-dots.ss
@@ -5,53 +5,53 @@
                  1 w))
 
 (plambda: (a ...) ([z : String] . [w : Number ... a])
-          (apply (lambda: ([x : Number] . [y : Number]) x)
+          (apply (lambda: ([x : Number] . [y : Number *]) x)
                  1 w))
 
-(plambda: (a ...) ([z : String] . [w : Number])
-          (apply (lambda: ([x : Number] . [y : Number]) x)
+(plambda: (a ...) ([z : String] . [w : Number *])
+          (apply (lambda: ([x : Number] . [y : Number *]) x)
                  1 w))
 
-(plambda: (a ...) ([z : String] . [w : Number])
+(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))
+                               (([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)
+(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)
+(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)
+(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)
+(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)
+          (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)
+          (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)
+          (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)
+          (apply (plambda: (b ...) ([x : Number] . [y : Number *]) x)
                  1 1 1 1 w))
 
 ;; .../.../poly
diff --git a/collects/tests/typed-scheme/succeed/leftist-heap.ss b/collects/tests/typed-scheme/succeed/leftist-heap.ss
index 81651f7c..da493318 100644
--- a/collects/tests/typed-scheme/succeed/leftist-heap.ss
+++ b/collects/tests/typed-scheme/succeed/leftist-heap.ss
@@ -205,7 +205,7 @@
                     s))
             0 h)))
   
-  (pdefine: (a) (-heap . [xs : a]) : (Heap a)
+  (pdefine: (a) (-heap . [xs : a *]) : (Heap a)
     (list->heap xs))   
 
   
diff --git a/collects/tests/typed-scheme/succeed/random-bits.ss b/collects/tests/typed-scheme/succeed/random-bits.ss
index f926e07f..7d0c8b9a 100644
--- a/collects/tests/typed-scheme/succeed/random-bits.ss
+++ b/collects/tests/typed-scheme/succeed/random-bits.ss
@@ -564,7 +564,7 @@
            (mrg32k3a-random-integer state n))
           (else
            (mrg32k3a-random-large state n)))))
-     (lambda: [args : Nb] 
+     (lambda: [args : Nb *] 
        (cond
         ((null? args)
          (lambda () 
@@ -603,7 +603,7 @@
 (define: (random-source-make-integers [s : Random]): (Nb -> Nb)
   ((:random-source-make-integers s)))
 
-(define: (random-source-make-reals [s : Random] . [unit : Nb]) : ( -> Flt)
+(define: (random-source-make-reals [s : Random] . [unit : Nb *]) : ( -> Flt)
   (apply (:random-source-make-reals s)  unit))
 
 ; ---
diff --git a/collects/tests/typed-scheme/succeed/varargs-tests.ss b/collects/tests/typed-scheme/succeed/varargs-tests.ss
index 2bb528aa..ccf4ec59 100644
--- a/collects/tests/typed-scheme/succeed/varargs-tests.ss
+++ b/collects/tests/typed-scheme/succeed/varargs-tests.ss
@@ -18,14 +18,14 @@
 
 
 (define: f : (number boolean * -> number)
-  (lambda: ([x : number] . [y : boolean])
+  (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])
+  (case-lambda: [([x : number] . [y : boolean *])
 		 (if (and (pair? y) (car y)) x (- x))]))
 
-(define: (f* [x : number] . [y : boolean]) : number
+(define: (f* [x : number] . [y : boolean *]) : number
   (if (and (pair? y) (car y)) x (- x)))
 
 (f 3)
diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
index 80afadc0..6036a47d 100644
--- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
@@ -157,17 +157,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 +222,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 +471,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 +527,7 @@
                   1)]
         
         [tc-e ((case-lambda:
-                [[x : Number] (+ 1 (car x))])
+                [[x : Number *] (+ 1 (car x))])
                5)
               N]
         #;

From 1bbdcf1ccf9d9753a0439be0042abc01b95e843c Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Wed, 18 Jun 2008 15:03:12 -0400
Subject: [PATCH 38/96] New test for lambda formal list mismatches.

original commit: 467b138cdacde26bcad3bbb9955fc62cfa9f1536
---
 .../typed-scheme/fail/formal-len-mismatches.ss  | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 collects/tests/typed-scheme/fail/formal-len-mismatches.ss

diff --git a/collects/tests/typed-scheme/fail/formal-len-mismatches.ss b/collects/tests/typed-scheme/fail/formal-len-mismatches.ss
new file mode 100644
index 00000000..bd640a06
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/formal-len-mismatches.ss
@@ -0,0 +1,17 @@
+#lang typed-scheme
+
+(: f (Integer Integer Integer * -> Integer))
+(define (f x)
+  (+ #\c x))
+
+(: f2 (Integer Integer * -> Integer))
+(define (f2 x y . z)
+  (apply + #\c x y z))
+
+(: f4 (Integer Integer -> Integer))
+(define (f4 x y w . z)
+  (apply + #\c x y w z))
+
+(: f3 (Integer Integer -> Integer))
+(define (f3 x . z)
+  (apply + #\c x z))
\ No newline at end of file

From 0af62b0c588bd98738d9dc22ab21cc93acbd2029 Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Wed, 18 Jun 2008 15:06:48 -0400
Subject: [PATCH 39/96] Forgot to add stars here.

original commit: 0c6ad7f08be86584eea8daab5c96728dbbd7e982
---
 collects/tests/typed-scheme/fail/apply-dots.ss | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/collects/tests/typed-scheme/fail/apply-dots.ss b/collects/tests/typed-scheme/fail/apply-dots.ss
index 6dde0cf9..69d6a129 100644
--- a/collects/tests/typed-scheme/fail/apply-dots.ss
+++ b/collects/tests/typed-scheme/fail/apply-dots.ss
@@ -1,11 +1,11 @@
 #lang typed-scheme
 
-(plambda: (a ...) ([z : String] . [w : Number])
+(plambda: (a ...) ([z : String] . [w : Number *])
           (apply (case-lambda: (([x : Number] . [y : Number ... a]) x))
                  w))
 
-(plambda: (a ...) ([z : String] . [w : Number])
+(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))
+                               (([x : String] [y : String] . [z : String *]) 0)
+                               ([y : String *] 0))
                  w))
\ No newline at end of file

From b59b032342aebd380028e6675bbce71be360bbbe Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Wed, 18 Jun 2008 15:07:00 -0400
Subject: [PATCH 40/96] Split this out into what should succeed and what should
 fail.

original commit: f80711bc9e3eb33aae1b9bb52d7f9033a1d83936
---
 collects/tests/typed-scheme/fail/cl-bug.ss    |  9 +++++++++
 collects/tests/typed-scheme/succeed/cl-bug.ss | 10 +---------
 2 files changed, 10 insertions(+), 9 deletions(-)
 create mode 100644 collects/tests/typed-scheme/fail/cl-bug.ss

diff --git a/collects/tests/typed-scheme/fail/cl-bug.ss b/collects/tests/typed-scheme/fail/cl-bug.ss
new file mode 100644
index 00000000..123d82e4
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/cl-bug.ss
@@ -0,0 +1,9 @@
+#lang typed-scheme
+
+(: f3 (case-lambda (Integer * -> Integer) (Number * -> Number)))
+(define (f3 x y) (+ x y))
+
+(+ 1 'foo)
+
+(: f2 (case-lambda (Number * -> Number)))
+(define (f2 x y) (+ x y))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/cl-bug.ss b/collects/tests/typed-scheme/succeed/cl-bug.ss
index 6b5a61c6..09b9327f 100644
--- a/collects/tests/typed-scheme/succeed/cl-bug.ss
+++ b/collects/tests/typed-scheme/succeed/cl-bug.ss
@@ -4,12 +4,4 @@
 (define (f . x) (+ 1 2))
 
 (: f4 (case-lambda (Integer * -> Integer) (Number * -> Number)))
-(define (f4 . x) (apply + x))
-
-(: f3 (case-lambda (Integer * -> Integer) (Number * -> Number)))
-(define (f3 x y) (+ x y))
-
-(+ 1 'foo)
-
-(: f2 (case-lambda (Number * -> Number)))
-(define (f2 x y) (+ x y))
\ No newline at end of file
+(define (f4 . x) (apply + x))
\ No newline at end of file

From b6fda17f3af30aa6a51ab460f230c0da696673c3 Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Wed, 18 Jun 2008 16:03:45 -0400
Subject: [PATCH 41/96] Remove this, as it isn't needed.

original commit: 449a784c1da3a658b84cf53b7ebead5909bd4fa0
---
 collects/tests/typed-scheme/fail/cl-bug.ss | 2 --
 1 file changed, 2 deletions(-)

diff --git a/collects/tests/typed-scheme/fail/cl-bug.ss b/collects/tests/typed-scheme/fail/cl-bug.ss
index 123d82e4..44300184 100644
--- a/collects/tests/typed-scheme/fail/cl-bug.ss
+++ b/collects/tests/typed-scheme/fail/cl-bug.ss
@@ -3,7 +3,5 @@
 (: f3 (case-lambda (Integer * -> Integer) (Number * -> Number)))
 (define (f3 x y) (+ x y))
 
-(+ 1 'foo)
-
 (: f2 (case-lambda (Number * -> Number)))
 (define (f2 x y) (+ x y))
\ No newline at end of file

From 5c8a9dfc5d7b19b048b20f43cb14865e654d87ea Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Wed, 18 Jun 2008 16:16:11 -0400
Subject: [PATCH 42/96] I don't know why this wasn't caught before, but with
 recent changes, it's now caught correctly.

original commit: f1211df156a37c709bc6f13077bc0430cd901617
---
 collects/tests/typed-scheme/succeed/int-def-colon.ss | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/collects/tests/typed-scheme/succeed/int-def-colon.ss b/collects/tests/typed-scheme/succeed/int-def-colon.ss
index 991b709c..2ac8856b 100644
--- a/collects/tests/typed-scheme/succeed/int-def-colon.ss
+++ b/collects/tests/typed-scheme/succeed/int-def-colon.ss
@@ -2,7 +2,7 @@
 
 (define-type-alias Int Integer)
 
-(: foo (Int -> Int))
+(: foo ( -> Int))
 (define (foo)
  (: loop (Int -> Int))
  (define (loop x)

From 385809eca896ee35cac60caab0cdb9ebdd24f151 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Wed, 18 Jun 2008 17:22:16 -0400
Subject: [PATCH 43/96] Tests in here that now succeed

original commit: b5bfb189610fed971b4a37f5a4191d72dc66548e
---
 collects/tests/typed-scheme/succeed/lots-o-bugs.ss | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/collects/tests/typed-scheme/succeed/lots-o-bugs.ss b/collects/tests/typed-scheme/succeed/lots-o-bugs.ss
index 21e5dd9c..98e4711c 100644
--- a/collects/tests/typed-scheme/succeed/lots-o-bugs.ss
+++ b/collects/tests/typed-scheme/succeed/lots-o-bugs.ss
@@ -1,23 +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 ...) () (lambda: [ys : a ... a] 3)))
 
-#;
-((plambda: (a ...) [xs : a ... a] (lambda: [ys : a ... a] 3))
- 1 2 3)
\ No newline at end of file
+#;((plambda: (a ...) [xs : a ... a] (lambda: [ys : a ... a] 3))
+   1 2 3 "foo")
\ No newline at end of file

From a2902970050c01528024afb488f7f84e08ba1746 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Wed, 18 Jun 2008 17:36:12 -0400
Subject: [PATCH 44/96] Fix identifier issues in fold-left/fold-right.

original commit: 8a66c759dc293fb822d89c99b8ec56dd3289c80d
---
 collects/tests/typed-scheme/succeed/fold-left.ss | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/collects/tests/typed-scheme/succeed/fold-left.ss b/collects/tests/typed-scheme/succeed/fold-left.ss
index 5b8c6e73..8b035175 100644
--- a/collects/tests/typed-scheme/succeed/fold-left.ss
+++ b/collects/tests/typed-scheme/succeed/fold-left.ss
@@ -2,18 +2,18 @@
 
 (: 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? a)
+  (if (or (null? as)
           (ormap null? bss))
       c
       (apply fold-left f 
              (apply f c (car as) (map car bss))
-             (cdr as) (map cdr bs))))
+             (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? a)
+  (if (or (null? as)
           (ormap null? bss))
       c
       (apply f
-             (apply fold-left f c (cdr as) (map cdr bs))
+             (apply fold-left f c (cdr as) (map cdr bss))
              (car as) (map car bss))))
\ No newline at end of file

From 395e0fc733de65803b556179095d9029348cd58e Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Wed, 18 Jun 2008 18:09:50 -0400
Subject: [PATCH 45/96] Otherwise we don't handle nesting.

original commit: 052849c1bbca03cd4aa778665da87f919959c48f
---
 collects/typed-scheme/private/type-utils.ss | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index 6d182581..0e55ff58 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -60,7 +60,8 @@
                                  (eq? name (cdr drest)))                            
                             (make-arr (append 
                                        (map sb dom)
-                                       (map (lambda (img) (substitute img name (car drest))) images))
+                                       ;; We need to recur first, just to expand out any dotted usages of this.
+                                       (map (lambda (img) (substitute img name (sb (car drest)))) images))
                                       (sb rng)
                                       #f
                                       #f

From 8cc53d8936b98b0debb9cbd23efa64c813b45af2 Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Wed, 18 Jun 2008 18:22:16 -0400
Subject: [PATCH 46/96] Instantiation... seems to be broken.  Adding unit tests
 to alert us to that fact.

original commit: 8256f922f9c9cd2e24261b4309700c7e896c4454
---
 .../typed-scheme/unit-tests/typecheck-tests.ss    | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
index 6036a47d..a3714212 100644
--- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
@@ -563,6 +563,21 @@
                           (apply (plambda: (b ...) ([x : Number] . [y : Number ... b]) x)
                                  1 w))]
         
+        ;; instantiating non-dotted terms
+        [tc-e (inst (plambda: (a) ([x : a]) x) Integer)
+              (-Integer . -> . -Integer)]
+        [tc-e (inst (plambda: (a) [x : a *] (apply + x)) Integer)
+              ((list) -Integer . ->* . -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)]
+        
         ;; error tests
         [tc-err (#%variable-reference number?)]
         [tc-err (+ 3 #f)]

From 156c0d0d38861c37d542957bcffb2031ed594278 Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Wed, 18 Jun 2008 18:53:46 -0400
Subject: [PATCH 47/96] I'm not sure what to do about this, given the recursive
 sb call.

original commit: 51ec643172e3893701b2a68ca7a5430ddac7ee8c
---
 collects/typed-scheme/private/type-utils.ss | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index 0e55ff58..dcc02ed9 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -52,9 +52,11 @@
   (define (sb t) (substitute-dots images name t))
   (if (hash-ref (free-vars* target) name #f)
       (type-case sb target
-                 [#:F name* (if (eq? name* name)
+                 ;; The way I handled this in my type system is via type validity checking.  Hrmm.
+                 #;[#:F name* (if (eq? name* name)
                                 (int-err "substitute-dots: got single variable ~a" name*)
                                 target)]
+                 [#:F name* target]
                  [#:arr dom rng rest drest thn-eff els-eff
                         (if (and (pair? drest)
                                  (eq? name (cdr drest)))                            

From f939f616f523a855f0ef766c39a8b39cf765d8d0 Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Wed, 18 Jun 2008 23:48:31 -0400
Subject: [PATCH 48/96] Lift out the recursive call, since that'll be shared
 across all substitutions.

original commit: f68efe9e317a53de87a4acb7e15875f4364044b7
---
 collects/typed-scheme/private/type-utils.ss | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index dcc02ed9..e32f735f 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -63,7 +63,8 @@
                             (make-arr (append 
                                        (map sb dom)
                                        ;; We need to recur first, just to expand out any dotted usages of this.
-                                       (map (lambda (img) (substitute img name (sb (car drest)))) images))
+                                       (let ([expanded (sb (car drest))])
+					 (map (lambda (img) (substitute img name expanded)) images)))
                                       (sb rng)
                                       #f
                                       #f

From 7f4b1a5cd129065deda1b7cf1b9136875ca7eb7c Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Thu, 19 Jun 2008 11:12:32 -0400
Subject: [PATCH 49/96] Fix macro impl.

original commit: 23aeff8c3bdc57442164d9865411f867917b7448
---
 collects/typed-scheme/private/type-effect-convenience.ss | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss
index 8a1c95ef..a0c6c815 100644
--- a/collects/typed-scheme/private/type-effect-convenience.ss
+++ b/collects/typed-scheme/private/type-effect-convenience.ss
@@ -13,7 +13,6 @@
 
 (provide (all-defined-out))
 
-
 (define (-vet id) (make-Var-True-Effect id))
 (define (-vef id) (make-Var-False-Effect id))
 
@@ -38,10 +37,11 @@
 
 (define-syntax ->
   (syntax-rules (:)
-    [(_ dom ... rng)
-     (->* (list dom ...) rng)]
     [(_ dom ... rng : eff1 eff2)
-     (->* (list dom ...) rng : eff1 eff2)]))
+     (->* (list dom ...) rng : eff1 eff2)]
+    [(_ dom ... rng)
+     (->* (list dom ...) rng)]))
+
 (define-syntax ->*
   (syntax-rules (:)
     [(_ dom rng)       

From 3ea5cf0e613decf13610c64cd455fb60f63009a2 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Thu, 19 Jun 2008 11:57:07 -0400
Subject: [PATCH 50/96] Fix type of filter, and inference w/ effects.

original commit: 3fd969651fbb7c90983ae76542c80391624e1f39
---
 collects/typed-scheme/private/base-env.ss   | 13 ++++++++++++-
 collects/typed-scheme/private/subtype.ss    |  7 +++++--
 collects/typed-scheme/private/type-utils.ss |  5 ++++-
 3 files changed, 21 insertions(+), 4 deletions(-)

diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 95df2174..115f7838 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -9,10 +9,13 @@
  '#%paramz
  (only-in scheme/match/runtime match:error))
 
+
+
 ;; these are all for constructing the types given to variables
 (require (for-syntax
           scheme/base
           "init-envs.ss"
+          "effect-rep.ss"
           (except-in "type-rep.ss" make-arr)
           "type-effect-convenience.ss"
           (only-in "type-effect-convenience.ss" [make-arr* make-arr])
@@ -132,7 +135,15 @@
              (cl-> [((a b . -> . b) b (make-lst a)) b]
                    [((a b c . -> . c) c (make-lst a) (make-lst b)) c]))]
      [foldr  (-poly (a b c) ((a b . -> . b) b (-lst a) . -> . b))]
-     [filter (-poly (a) ((a . -> . B) (-lst a) . -> . (-lst a)))]
+     [filter (-poly (a b) (cl->*
+                           ((a . -> . B
+                               :
+                               (list (make-Latent-Restrict-Effect b))
+                               (list (make-Latent-Remove-Effect b)))
+                            (-lst a)
+                            . -> .
+                            (-lst b))
+                           ((a . -> . B) (-lst a) . -> . (-lst a))))]
      [take   (-poly (a) ((-lst a) -Integer . -> . (-lst a)))]
      [drop   (-poly (a) ((-lst a) -Integer . -> . (-lst a)))]
      [last   (-poly (a) ((-lst a) . -> . a))]
diff --git a/collects/typed-scheme/private/subtype.ss b/collects/typed-scheme/private/subtype.ss
index 01698ffb..398fe7b2 100644
--- a/collects/typed-scheme/private/subtype.ss
+++ b/collects/typed-scheme/private/subtype.ss
@@ -108,8 +108,11 @@
            (or (and (null? thn-eff*) (null? els-eff*))
                (and (effects-equal? thn-eff thn-eff*)
                     (effects-equal? els-eff els-eff*))
-               (and (andmap sub-eff thn-eff thn-eff*)
-                    (andmap sub-eff els-eff els-eff*)))
+               (and 
+                (= (length thn-eff) (length thn-eff*))
+                (= (length els-eff) (length els-eff*))
+                (andmap sub-eff thn-eff thn-eff*)
+                (andmap sub-eff els-eff els-eff*)))
          (fail! s t))
        ;; either the effects have to be the same, or the supertype can't have effects
        (let ([A (subtypes*/varargs A0 t1 s1 s3)])
diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index e32f735f..9da1fe36 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -130,7 +130,10 @@
 ;; equality - good
 
 (define tc-result-equal? equal?)
-(define (effects-equal? fs1 fs2) (andmap eq? fs1 fs2))
+(define (effects-equal? fs1 fs2) 
+  (and 
+   (= (length fs1) (length fs2))
+   (andmap eq? fs1 fs2)))
 
 
 ;; fv : Type -> Listof[Name]

From b3223cab41d2cb52d952be1ce70ed0d3876a85a3 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Thu, 19 Jun 2008 12:41:06 -0400
Subject: [PATCH 51/96] Fix tests, add filter tests.

original commit: 1af866586ec8e5497e4d4564ac1b129f4c0a02e4
---
 .../tests/typed-scheme/unit-tests/typecheck-tests.ss   | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
index a3714212..eb1ca5ca 100644
--- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
@@ -566,8 +566,8 @@
         ;; instantiating non-dotted terms
         [tc-e (inst (plambda: (a) ([x : a]) x) Integer)
               (-Integer . -> . -Integer)]
-        [tc-e (inst (plambda: (a) [x : a *] (apply + x)) Integer)
-              ((list) -Integer . ->* . -Integer)]
+        [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)
@@ -602,6 +602,12 @@
                              (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 (let: ([fact : (Number -> Number) (lambda: ([n : Number]) (if (zero? n) 1 (* n (fact (- n 1)))))])
                         (fact 20))]
         

From 8e48f421847f1c2dd6cdb0d193ad7147e5a2a3af Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Thu, 19 Jun 2008 13:23:27 -0400
Subject: [PATCH 52/96] Fix test to expecte effects. Remove useless annotation.

original commit: 36408a32d5526038ecda7c8b05ba844868a0ac5e
---
 collects/tests/typed-scheme/succeed/priority-queue.scm    | 2 +-
 collects/tests/typed-scheme/unit-tests/typecheck-tests.ss | 3 +--
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/collects/tests/typed-scheme/succeed/priority-queue.scm b/collects/tests/typed-scheme/succeed/priority-queue.scm
index bf04a2e4..e2d7e57c 100644
--- a/collects/tests/typed-scheme/succeed/priority-queue.scm
+++ b/collects/tests/typed-scheme/succeed/priority-queue.scm
@@ -80,7 +80,7 @@
 
 ;; FIXME -- too many annotations needed on cons
 (pdefine: (a) (insert* [xs : (list-of a)] [ps : (list-of number)] [pq : (priority-queue a)]) : (priority-queue a)
-          (make (heap:insert* (map #{#{cons @ number a} :: (number a -> (cons number a))} ps xs) (heap pq))))
+          (make (heap:insert* (map #{cons @ number a} ps xs) (heap pq))))
 
 (pdefine: (a) (delete-min [pq : (priority-queue a)]) : (priority-queue a)
 	  (let ([h (heap pq)])
diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
index eb1ca5ca..ea2444a3 100644
--- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
@@ -562,10 +562,9 @@
         [tc-err (plambda: (a ...) ([z : String] . [w : Number ... a])
                           (apply (plambda: (b ...) ([x : Number] . [y : Number ... b]) x)
                                  1 w))]
-        
         ;; instantiating non-dotted terms
         [tc-e (inst (plambda: (a) ([x : a]) x) Integer)
-              (-Integer . -> . -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))]
         

From da03725d19bcc851bcd927ea6a0313eeef8aa496 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Thu, 19 Jun 2008 14:57:35 -0400
Subject: [PATCH 53/96]  * Split apart identifier typechecking and type
 instantiation  * Add dotted instantiation (replacing bounds with different
 bounds)  * Fix some macro issues, including syntax locations  * Fix more
 effect inference

original commit: bb8d8e23d81c7f1324d1bfc8b33882fc71f94503
---
 collects/typed-scheme/private/prims.ss        | 23 ++++++++----
 .../private/type-effect-convenience.ss        |  8 ++--
 collects/typed-scheme/private/type-utils.ss   | 37 ++++++++++++++++---
 3 files changed, 51 insertions(+), 17 deletions(-)

diff --git a/collects/typed-scheme/private/prims.ss b/collects/typed-scheme/private/prims.ss
index b9fdfe2e..2414b552 100644
--- a/collects/typed-scheme/private/prims.ss
+++ b/collects/typed-scheme/private/prims.ss
@@ -124,16 +124,20 @@ This file defines two sorts of primitives. All of them are provided into any mod
 (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 (:)
@@ -173,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 ...))]))
 
diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss
index a0c6c815..cf76cb55 100644
--- a/collects/typed-scheme/private/type-effect-convenience.ss
+++ b/collects/typed-scheme/private/type-effect-convenience.ss
@@ -35,12 +35,12 @@
     [(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)
-     (->* (list dom ...) rng)]))
+     #'(->* (list dom ...) rng)]))
 
 (define-syntax ->*
   (syntax-rules (:)
diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index 9da1fe36..5987266e 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -16,6 +16,7 @@
          subst 
          ret
          instantiate-poly
+         instantiate-poly-dotted
          tc-result: 
          tc-result-equal? 
          effects-equal?
@@ -52,10 +53,6 @@
   (define (sb t) (substitute-dots images name t))
   (if (hash-ref (free-vars* target) name #f)
       (type-case sb target
-                 ;; The way I handled this in my type system is via type validity checking.  Hrmm.
-                 #;[#:F name* (if (eq? name* name)
-                                (int-err "substitute-dots: got single variable ~a" name*)
-                                target)]
                  [#:F name* target]
                  [#:arr dom rng rest drest thn-eff els-eff
                         (if (and (pair? drest)
@@ -78,6 +75,27 @@
                                       (map (lambda (e) (sub-eff sb e)) els-eff)))])
       target))
 
+;; implements sd from the formalism
+;; substitute-dotted : Type Name Type Name -> 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
+                 [#: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]]
 ;; subst-all : substition Type -> Type
@@ -105,7 +123,16 @@
             [rest-tys (drop types (length fixed))]
             [body* (subst-all (map list fixed fixed-tys) body)])
        (substitute-dots rest-tys dotted body*))]
-    [_ (int-err "instantiate-many: requires Poly type, got ~a" t)]))
+    [_ (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

From 8be54e9a3b264d7b9a20d9fb80ea40ccdf0151f6 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Thu, 19 Jun 2008 14:59:19 -0400
Subject: [PATCH 54/96] Add unit test for dotted instantiation, and add version
 of fold-left/fold-right that explicitly instantiates the recursive call.

original commit: 2a7dbe2a80d34abc5097e144b80bda9965546703
---
 .../typed-scheme/succeed/fold-left-inst.ss    | 19 +++++++++++++++++++
 .../unit-tests/typecheck-tests.ss             |  3 +++
 2 files changed, 22 insertions(+)
 create mode 100644 collects/tests/typed-scheme/succeed/fold-left-inst.ss

diff --git a/collects/tests/typed-scheme/succeed/fold-left-inst.ss b/collects/tests/typed-scheme/succeed/fold-left-inst.ss
new file mode 100644
index 00000000..100ecbba
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/fold-left-inst.ss
@@ -0,0 +1,19 @@
+#lang typed-scheme
+
+(: fold-left (All (c a b ...) ((c a b ... b -> c) c (Listof a) (Listof b) ... b -> c)))
+(define (fold-left f c as . bss)
+  (if (or (null? as)
+          (ormap null? bss))
+      c
+      (apply (inst fold-left c a b ... b) f 
+             (apply f c (car as) (map car bss))
+             (cdr as) (map cdr bss))))
+
+(: fold-right (All (c a b ...) ((c a b ... b -> c) c (Listof a) (Listof b) ... b -> c)))
+(define (fold-right f c as . bss)
+  (if (or (null? as)
+          (ormap null? bss))
+      c
+      (apply f
+             (apply (inst fold-left c a b ... b) f c (cdr as) (map cdr bss))
+             (car as) (map car bss))))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
index ea2444a3..1f5b1d1f 100644
--- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
@@ -577,6 +577,9 @@
                (-Integer B -Integer . -> . -Integer)
                . -> . -Integer)]
         
+        [tc-e (plambda: (z x y ...) () (inst map z x y ... y))
+              (-polydots (z x y) ((list ((list z x) (y y) . ->... . z) z (-lst x)) ((-lst y) y) . ->... . (-lst z)))]
+        
         ;; error tests
         [tc-err (#%variable-reference number?)]
         [tc-err (+ 3 #f)]

From 8338ee8756f1382f43d2a73d4c72ec866d524081 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Thu, 19 Jun 2008 16:55:06 -0400
Subject: [PATCH 55/96]  * Add constraints when matching t1...a to t2...b  * Do
 inference when you have (apply f ... xs), f and xs are dotted,    and on
 different bounds.  * Add fold-right to extra-procs and its type to base-env

original commit: b9e1676a55ab3f8d454a58aa290a0dcb0ecce414
---
 collects/typed-scheme/private/base-env.ss    | 2 ++
 collects/typed-scheme/private/extra-procs.ss | 9 +++++++--
 collects/typed-scheme/private/type-utils.ss  | 3 ++-
 3 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 115f7838..07999859 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -130,6 +130,8 @@
                                    ((-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]
diff --git a/collects/typed-scheme/private/extra-procs.ss b/collects/typed-scheme/private/extra-procs.ss
index e2c6b97b..7c793ccf 100644
--- a/collects/typed-scheme/private/extra-procs.ss
+++ b/collects/typed-scheme/private/extra-procs.ss
@@ -6,5 +6,10 @@
     (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))))
\ No newline at end of file
diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index 5987266e..4022514d 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -12,6 +12,7 @@
 (provide fv fv/list
          substitute
          substitute-dots
+         substitute-dotted
          subst-all
          subst 
          ret
@@ -76,7 +77,7 @@
       target))
 
 ;; implements sd from the formalism
-;; substitute-dotted : Type Name Type Name -> Type
+;; 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)

From 2e4d817391e5fa75a69180a3ca3dc460246ebf21 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Thu, 19 Jun 2008 16:55:26 -0400
Subject: [PATCH 56/96] More tests!

original commit: e62598ef08326c3a0f20a57c5b8370d0319473a5
---
 .../tests/typed-scheme/succeed/fold-left.ss   | 26 ++++++++++++-
 .../unit-tests/typecheck-tests.ss             | 39 +++++++++++++++++--
 2 files changed, 59 insertions(+), 6 deletions(-)

diff --git a/collects/tests/typed-scheme/succeed/fold-left.ss b/collects/tests/typed-scheme/succeed/fold-left.ss
index 8b035175..ca1364da 100644
--- a/collects/tests/typed-scheme/succeed/fold-left.ss
+++ b/collects/tests/typed-scheme/succeed/fold-left.ss
@@ -15,5 +15,27 @@
           (ormap null? bss))
       c
       (apply f
-             (apply fold-left f c (cdr as) (map cdr bss))
-             (car as) (map car bss))))
\ No newline at end of file
+             (apply fold-right f c (cdr as) (map cdr bss))
+             (car as) (map car bss))))
+
+;; Matthias -- tell me why this returns 4.
+((plambda: (x ...) [xs : x ... x] 
+    (apply fold-left 
+           (lambda: ([a : Integer] [b : Integer] . [xs : x ... x])
+             (+ a b))
+           3 
+           (list 1 2 3) 
+           (map list xs)))
+ 3 4 5)
+
+((plambda: (x ...) [xs : x ... x] 
+    (apply fold-right
+           (lambda: ([a : Integer] [b : Integer] . [xs : x ... x])
+             (+ a b))
+           3 
+           (list 1 2 3) 
+           (map list xs)))
+ 3 4 5)
+
+(fold-left  (lambda: ([a : (Listof Integer)] [c : Integer]) (cons c a)) null (list 3 4 5 6))
+(fold-right (lambda: ([a : (Listof Integer)] [c : Integer]) (cons c a)) null (list 3 4 5 6))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
index 1f5b1d1f..bb0c8dcb 100644
--- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
@@ -559,9 +559,10 @@
                           (apply (plambda: (b) ([x : Number] . [y : Number ... a]) x)
                                  1 w))]
         
-        [tc-err (plambda: (a ...) ([z : String] . [w : Number ... a])
-                          (apply (plambda: (b ...) ([x : Number] . [y : Number ... b]) 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)))]
@@ -578,7 +579,7 @@
                . -> . -Integer)]
         
         [tc-e (plambda: (z x y ...) () (inst map z x y ... y))
-              (-polydots (z x y) ((list ((list z x) (y y) . ->... . z) z (-lst x)) ((-lst y) y) . ->... . (-lst z)))]
+              (-polydots (z x y) (-> ((list ((list x) (y y) . ->... . z) (-lst x)) ((-lst y) y) . ->... . (-lst z))))]
         
         ;; error tests
         [tc-err (#%variable-reference number?)]
@@ -610,6 +611,36 @@
         [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))))]
+        
         #;[tc-err (let: ([fact : (Number -> Number) (lambda: ([n : Number]) (if (zero? n) 1 (* n (fact (- n 1)))))])
                         (fact 20))]
         

From 6a3dbebd0771692e05cb96c4d891d11433bf2d31 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Thu, 19 Jun 2008 18:04:19 -0400
Subject: [PATCH 57/96] Do substitution properly from dmap.

original commit: 0f142d97e3d2d995fa18f694e211cbdabf814bbf
---
 collects/typed-scheme/private/type-utils.ss | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index 4022514d..c78ea3ea 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -54,7 +54,6 @@
   (define (sb t) (substitute-dots images name t))
   (if (hash-ref (free-vars* target) name #f)
       (type-case sb target
-                 [#:F name* target]
                  [#:arr dom rng rest drest thn-eff els-eff
                         (if (and (pair? drest)
                                  (eq? name (cdr drest)))                            
@@ -101,7 +100,14 @@
 ;; substitution = Listof[List[Name,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 ...) #f)
+       (substitute-dots imgs v t)]
+      [(list v (list ts) starred)
+       (int-err "subst-all: nyi")]
+      [(list v img)
+       (substitute img v t)])))
 
 
 ;; unfold : Type -> Type

From ffc0331fa7c4788445a54b51154c1020a2331e44 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Thu, 19 Jun 2008 18:04:30 -0400
Subject: [PATCH 58/96] New test

original commit: 2bf691991c2c7316cb2f4b30677a7fd424f7e4dc
---
 collects/tests/typed-scheme/succeed/dotted-identity.ss | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 collects/tests/typed-scheme/succeed/dotted-identity.ss

diff --git a/collects/tests/typed-scheme/succeed/dotted-identity.ss b/collects/tests/typed-scheme/succeed/dotted-identity.ss
new file mode 100644
index 00000000..0ff8aedc
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/dotted-identity.ss
@@ -0,0 +1,10 @@
+#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)}
+

From 20fdbea0313808b7c7de37b66e2736d0a29fc028 Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Thu, 19 Jun 2008 19:10:05 -0400
Subject: [PATCH 59/96] Another example, putting in starred for dots.

original commit: af12feb72972ca9f5c0ae71573be43101c93dc76
---
 collects/tests/typed-scheme/succeed/dotted-identity.ss | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/collects/tests/typed-scheme/succeed/dotted-identity.ss b/collects/tests/typed-scheme/succeed/dotted-identity.ss
index 0ff8aedc..7ea9391d 100644
--- a/collects/tests/typed-scheme/succeed/dotted-identity.ss
+++ b/collects/tests/typed-scheme/succeed/dotted-identity.ss
@@ -8,3 +8,9 @@
 
 #{(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) :: (Integer * -> Integer)}
\ No newline at end of file

From 8a6adc82da01b2d0b0eeb360316cafd5d84131fb Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Thu, 19 Jun 2008 19:12:39 -0400
Subject: [PATCH 60/96] Another change.

original commit: a1f078fb591d87b572864f80b152a9f1e462b10a
---
 .../tests/typed-scheme/succeed/dotted-identity.ss     | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/collects/tests/typed-scheme/succeed/dotted-identity.ss b/collects/tests/typed-scheme/succeed/dotted-identity.ss
index 7ea9391d..df07474f 100644
--- a/collects/tests/typed-scheme/succeed/dotted-identity.ss
+++ b/collects/tests/typed-scheme/succeed/dotted-identity.ss
@@ -12,5 +12,12 @@
 (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) :: (Integer * -> Integer)}
\ No newline at end of file
+
+#; #{(f z) :: (Integer * -> Integer)}
+
+;; I don't believe the below should work, but it points out where that internal error is coming from.
+
+(: g (All (b ...) ( -> (b ... b -> Integer))))
+(define (g) (lambda xs 0))
+
+(f (g))
\ No newline at end of file

From ee044ee4c4f607d19a829b86998d051417f813b2 Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Thu, 19 Jun 2008 19:14:32 -0400
Subject: [PATCH 61/96]  * Add the ability to substitute in starred types for
 dotted when    we've inferred it.  * Try and consolidate a lot of the error
 printing with domain mismatches.

original commit: 654d7e2f4683f65ba7d0a12491d4b3b834bd70f3
---
 collects/typed-scheme/private/type-utils.ss | 16 +++++++---------
 1 file changed, 7 insertions(+), 9 deletions(-)

diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index c78ea3ea..3eab1382 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -49,9 +49,9 @@
                                     (map (lambda (e) (sub-eff sb e)) els-eff)))])
       target))
 
-;; substitute-dots : Listof[Type] Name Type -> Type
-(define (substitute-dots images name target)    
-  (define (sb t) (substitute-dots images name t))
+;; 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
                  [#:arr dom rng rest drest thn-eff els-eff
@@ -63,7 +63,7 @@
                                        (let ([expanded (sb (car drest))])
 					 (map (lambda (img) (substitute img name expanded)) images)))
                                       (sb rng)
-                                      #f
+                                      rimage
                                       #f
                                       (map (lambda (e) (sub-eff sb e)) thn-eff)
                                       (map (lambda (e) (sub-eff sb e)) els-eff))
@@ -102,10 +102,8 @@
 (define (subst-all s t)
   (for/fold ([t t]) ([e s])
     (match e
-      [(list v (list imgs ...) #f)
-       (substitute-dots imgs v t)]
-      [(list v (list ts) starred)
-       (int-err "subst-all: nyi")]
+      [(list v (list imgs ...) starred)
+       (substitute-dots imgs starred v t)]
       [(list v img)
        (substitute img v t)])))
 
@@ -129,7 +127,7 @@
      (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 dotted 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)

From 53200d23db819232262b006f239986993b80d8f7 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Fri, 20 Jun 2008 13:07:08 -0400
Subject: [PATCH 62/96]  * Added code to check that substitution gets rid of
 all appropriate    variables (and fails if not)  * Added weird dotted as
 subtype of * case (dcon-exact)

original commit: 6296ffbfcf85a624227f11f486fb195954e4479b
---
 collects/typed-scheme/private/type-utils.ss | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index 3eab1382..d6e191f1 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -97,7 +97,7 @@
       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)
   (for/fold ([t t]) ([e s])

From f2b3eadd88319373b90c7ea3f3b0748bdfc83b33 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Fri, 20 Jun 2008 13:07:42 -0400
Subject: [PATCH 63/96] Correct and incorrect uses of dotted identity

original commit: bec9c11fd4d61bceb966b06e5a9517d286af9ca4
---
 collects/tests/typed-scheme/fail/dotted-identity.ss | 11 +++++++++++
 .../tests/typed-scheme/succeed/dotted-identity.ss   |  9 ++-------
 .../tests/typed-scheme/succeed/unholy-terror.ss     | 13 +++++++++----
 3 files changed, 22 insertions(+), 11 deletions(-)
 create mode 100644 collects/tests/typed-scheme/fail/dotted-identity.ss

diff --git a/collects/tests/typed-scheme/fail/dotted-identity.ss b/collects/tests/typed-scheme/fail/dotted-identity.ss
new file mode 100644
index 00000000..543f46c3
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/dotted-identity.ss
@@ -0,0 +1,11 @@
+#lang typed-scheme
+
+;; I don't believe the below should work, but it points out where that internal error is coming from.
+
+(: f (All (a ...) ((a ... a -> Integer) -> (a ... a -> Integer))))
+(define (f x) x)
+
+(: g (All (b ...) ( -> (b ... b -> Integer))))
+(define (g) (lambda xs 0))
+
+(f (g))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/dotted-identity.ss b/collects/tests/typed-scheme/succeed/dotted-identity.ss
index df07474f..78a83976 100644
--- a/collects/tests/typed-scheme/succeed/dotted-identity.ss
+++ b/collects/tests/typed-scheme/succeed/dotted-identity.ss
@@ -13,11 +13,6 @@
 
 ((f z) 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18)
 
-#; #{(f z) :: (Integer * -> Integer)}
+(f z)
 
-;; I don't believe the below should work, but it points out where that internal error is coming from.
-
-(: g (All (b ...) ( -> (b ... b -> Integer))))
-(define (g) (lambda xs 0))
-
-(f (g))
\ No newline at end of file
+#{(f z) :: (Integer * -> Integer)}
diff --git a/collects/tests/typed-scheme/succeed/unholy-terror.ss b/collects/tests/typed-scheme/succeed/unholy-terror.ss
index 4802241a..93aa200f 100644
--- a/collects/tests/typed-scheme/succeed/unholy-terror.ss
+++ b/collects/tests/typed-scheme/succeed/unholy-terror.ss
@@ -1,5 +1,6 @@
 #lang typed-scheme
 
+#;
 (apply (plambda: (a ...) [ys : (a ... a -> Number) *]
          (lambda: [zs : a ... a]
             (map (lambda: ([y : (a ... a -> Number)])
@@ -9,7 +10,7 @@
              (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)])
@@ -21,10 +22,14 @@
               (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 + - * /))
 
 (apply (plambda: (a ...) [ys : (a ... a -> Number) *]
          (lambda: [zs : a ... a]
-            (map (lambda: ([y : (a ... a -> Number)])
-                   (apply y zs))
-                 ys)))
+            #{(error 'foo) :: (Listof Number)}))
        (list + - * /))
\ No newline at end of file

From b133c45645014037d9a75f0abb37962627e20aca Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Fri, 20 Jun 2008 14:46:24 -0400
Subject: [PATCH 64/96] Small changes needed after changes to infer.

original commit: 89cb3a4b09243dcc3bf292cfd682f226e1f2d326
---
 collects/tests/typed-scheme/succeed/batched-queue.scm |  2 +-
 collects/tests/typed-scheme/succeed/unholy-terror.ss  | 10 ++++++++--
 collects/tests/typed-scheme/unit-tests/infer-tests.ss |  6 +++---
 3 files changed, 12 insertions(+), 6 deletions(-)

diff --git a/collects/tests/typed-scheme/succeed/batched-queue.scm b/collects/tests/typed-scheme/succeed/batched-queue.scm
index 71e1db34..7c2ae9e9 100644
--- a/collects/tests/typed-scheme/succeed/batched-queue.scm
+++ b/collects/tests/typed-scheme/succeed/batched-queue.scm
@@ -82,5 +82,5 @@
 
 ;; TESTS
 
-(= 0 (size (empty)))
+(= 0 (size ((inst empty Number))))
 
diff --git a/collects/tests/typed-scheme/succeed/unholy-terror.ss b/collects/tests/typed-scheme/succeed/unholy-terror.ss
index 93aa200f..34aaa19b 100644
--- a/collects/tests/typed-scheme/succeed/unholy-terror.ss
+++ b/collects/tests/typed-scheme/succeed/unholy-terror.ss
@@ -1,6 +1,6 @@
 #lang typed-scheme
 
-#;
+
 (apply (plambda: (a ...) [ys : (a ... a -> Number) *]
          (lambda: [zs : a ... a]
             (map (lambda: ([y : (a ... a -> Number)])
@@ -10,7 +10,7 @@
              (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)])
@@ -22,6 +22,12 @@
               (lambda: ([x : Number] [y : Number]) (/ x y))))
  3 4)
 
+(plambda: (a ...) [ys : (a ... a -> Number) *]
+          ((inst map Number (a ... a -> Number)) (ann (error 'fail) ((a ... a -> Number) -> Number)) ys))
+
+(plambda: (a ...) [ys : (a ... a -> Number) *]
+          (map (ann (error 'fail) ((a ... a -> Number) -> Number)) ys))
+
 (apply (plambda: (a ...) [ys : (a ... a -> Number) *]
          (lambda: [zs : a ... a]
                   (map (lambda: ([y : (a ... a -> Number)])
diff --git a/collects/tests/typed-scheme/unit-tests/infer-tests.ss b/collects/tests/typed-scheme/unit-tests/infer-tests.ss
index 46a30545..f1d5e22b 100644
--- a/collects/tests/typed-scheme/unit-tests/infer-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/infer-tests.ss
@@ -32,16 +32,16 @@
 (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)                   

From 34df17ddb4f71f8c7b7b1e16444f18e946e68408 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Fri, 20 Jun 2008 15:27:46 -0400
Subject: [PATCH 65/96] Use the X from cgen/list to create the empty cmap. This
 allows (vector) to have type (Vectorof (U))

original commit: 0366745cbf3e8308b9700305c7e187aa260119ba
---
 collects/typed-scheme/private/base-env.ss | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 07999859..22644307 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -196,7 +196,7 @@
      (min (->* (list N) N N))
      [values  (make-Poly '(a) (-> (-v a) (-v a)))]
      [vector-ref 
-      (make-Poly (list 'a) ((make-Vector (-v a)) N . -> . (-v a)))]
+      (make-Poly (list 'a) ((make-Vector (-v a)) -Integer . -> . (-v a)))]
      [build-vector (-poly (a) (-Integer (-Integer . -> . a) . -> . (make-Vector a)))]
      [build-list (-poly (a) (-Integer (-Integer . -> . a) . -> . (-lst a)))]
      [reverse (make-Poly '(a) (-> (make-lst (-v a)) (make-lst (-v a))))]
@@ -323,7 +323,7 @@
      
      [match:error ((list) Univ . ->* . (Un))]
      
-     [vector-set! (-poly (a) (-> (make-Vector a) N a -Void))]
+     [vector-set! (-poly (a) (-> (make-Vector a) -Integer a -Void))]
      
      [vector->list (-poly (a) (-> (make-Vector a) (-lst a)))]
      [list->vector (-poly (a) (-> (-lst a) (make-Vector a)))]
@@ -353,13 +353,13 @@
      [make-vector
       (-poly (a)
              (cl->
-              [(N) (make-Vector N)]
-              [(N a) (make-Vector a)]))]
+              [(-Integer) (make-Vector -Integer)]
+              [(-Integer a) (make-Vector a)]))]
      
      [file-exists? (-Pathlike . -> . B)]
      [string->symbol (-String . -> . Sym)]
      [symbol->string (Sym . -> . -String)]
-     [vector-length (-poly (a) ((make-Vector a) . -> . N))]
+     [vector-length (-poly (a) ((make-Vector a) . -> . -Integer))]
      
      [call-with-input-file (-poly (a) 
                                   (cl->

From 9810d79ec55c40ff2e1553606c9bbb1042587e64 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Fri, 20 Jun 2008 15:27:59 -0400
Subject: [PATCH 66/96] Remove no-longer-needed inst.

original commit: b2edd9d19754b1297ce02eb04d591ccc7f29e46a
---
 collects/tests/typed-scheme/succeed/batched-queue.scm | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/collects/tests/typed-scheme/succeed/batched-queue.scm b/collects/tests/typed-scheme/succeed/batched-queue.scm
index 7c2ae9e9..71e1db34 100644
--- a/collects/tests/typed-scheme/succeed/batched-queue.scm
+++ b/collects/tests/typed-scheme/succeed/batched-queue.scm
@@ -82,5 +82,5 @@
 
 ;; TESTS
 
-(= 0 (size ((inst empty Number))))
+(= 0 (size (empty)))
 

From eb320ad75d690c9bc5cdedfd9a556a87dcf32c79 Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Fri, 20 Jun 2008 15:47:22 -0400
Subject: [PATCH 67/96] Revert last change.

original commit: ce58c4c6763f6ee31604f38660e3165f29096931
---
 collects/tests/typed-scheme/succeed/batched-queue.scm | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/collects/tests/typed-scheme/succeed/batched-queue.scm b/collects/tests/typed-scheme/succeed/batched-queue.scm
index 71e1db34..7c2ae9e9 100644
--- a/collects/tests/typed-scheme/succeed/batched-queue.scm
+++ b/collects/tests/typed-scheme/succeed/batched-queue.scm
@@ -82,5 +82,5 @@
 
 ;; TESTS
 
-(= 0 (size (empty)))
+(= 0 (size ((inst empty Number))))
 

From 028aeadc4b8a6fad99c95e28cf4774e368aa3a07 Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Fri, 20 Jun 2008 15:47:56 -0400
Subject: [PATCH 68/96] Revert last change.

original commit: a6ea8d79543ba3db69a859700dde9c78d583dd8b
---
 collects/typed-scheme/private/base-env.ss | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 22644307..07999859 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -196,7 +196,7 @@
      (min (->* (list N) N N))
      [values  (make-Poly '(a) (-> (-v a) (-v a)))]
      [vector-ref 
-      (make-Poly (list 'a) ((make-Vector (-v a)) -Integer . -> . (-v a)))]
+      (make-Poly (list 'a) ((make-Vector (-v a)) N . -> . (-v a)))]
      [build-vector (-poly (a) (-Integer (-Integer . -> . a) . -> . (make-Vector a)))]
      [build-list (-poly (a) (-Integer (-Integer . -> . a) . -> . (-lst a)))]
      [reverse (make-Poly '(a) (-> (make-lst (-v a)) (make-lst (-v a))))]
@@ -323,7 +323,7 @@
      
      [match:error ((list) Univ . ->* . (Un))]
      
-     [vector-set! (-poly (a) (-> (make-Vector a) -Integer a -Void))]
+     [vector-set! (-poly (a) (-> (make-Vector a) N a -Void))]
      
      [vector->list (-poly (a) (-> (make-Vector a) (-lst a)))]
      [list->vector (-poly (a) (-> (-lst a) (make-Vector a)))]
@@ -353,13 +353,13 @@
      [make-vector
       (-poly (a)
              (cl->
-              [(-Integer) (make-Vector -Integer)]
-              [(-Integer a) (make-Vector a)]))]
+              [(N) (make-Vector N)]
+              [(N a) (make-Vector a)]))]
      
      [file-exists? (-Pathlike . -> . B)]
      [string->symbol (-String . -> . Sym)]
      [symbol->string (Sym . -> . -String)]
-     [vector-length (-poly (a) ((make-Vector a) . -> . -Integer))]
+     [vector-length (-poly (a) ((make-Vector a) . -> . N))]
      
      [call-with-input-file (-poly (a) 
                                   (cl->

From 16df4ac649549cbeece24435acb21fdff408ed4c Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Fri, 20 Jun 2008 17:50:15 -0400
Subject: [PATCH 69/96] Remove the bits and pieces used to diagnose the
 original file, and add the non-outer-apply versions (that have no reason not
 to work).

original commit: 48961eb5519b86de55b100fa98ab8c526c9dd699
---
 .../typed-scheme/succeed/unholy-terror.ss     | 37 ++++++++++++++-----
 1 file changed, 27 insertions(+), 10 deletions(-)

diff --git a/collects/tests/typed-scheme/succeed/unholy-terror.ss b/collects/tests/typed-scheme/succeed/unholy-terror.ss
index 34aaa19b..04de86c2 100644
--- a/collects/tests/typed-scheme/succeed/unholy-terror.ss
+++ b/collects/tests/typed-scheme/succeed/unholy-terror.ss
@@ -22,12 +22,6 @@
               (lambda: ([x : Number] [y : Number]) (/ x y))))
  3 4)
 
-(plambda: (a ...) [ys : (a ... a -> Number) *]
-          ((inst map Number (a ... a -> Number)) (ann (error 'fail) ((a ... a -> Number) -> Number)) ys))
-
-(plambda: (a ...) [ys : (a ... a -> Number) *]
-          (map (ann (error 'fail) ((a ... a -> Number) -> Number)) ys))
-
 (apply (plambda: (a ...) [ys : (a ... a -> Number) *]
          (lambda: [zs : a ... a]
                   (map (lambda: ([y : (a ... a -> Number)])
@@ -35,7 +29,30 @@
                        ys)))
        (list + - * /))
 
-(apply (plambda: (a ...) [ys : (a ... a -> Number) *]
-         (lambda: [zs : a ... a]
-            #{(error 'foo) :: (Listof Number)}))
-       (list + - * /))
\ No newline at end of file
+((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)))
+ + - * /)
\ No newline at end of file

From de9142f4bae5a3d1c1324097937e82cd01429045 Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Sat, 21 Jun 2008 21:09:03 -0400
Subject: [PATCH 70/96] Let's also try out the abstracted version of this
 function.

original commit: e4a0dc82b3753641b0da838e393d7ff453ca37c9
---
 collects/tests/typed-scheme/succeed/unholy-terror.ss | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/collects/tests/typed-scheme/succeed/unholy-terror.ss b/collects/tests/typed-scheme/succeed/unholy-terror.ss
index 04de86c2..1abdcc3a 100644
--- a/collects/tests/typed-scheme/succeed/unholy-terror.ss
+++ b/collects/tests/typed-scheme/succeed/unholy-terror.ss
@@ -1,6 +1,5 @@
 #lang typed-scheme
 
-
 (apply (plambda: (a ...) [ys : (a ... a -> Number) *]
          (lambda: [zs : a ... a]
             (map (lambda: ([y : (a ... a -> Number)])
@@ -55,4 +54,12 @@
      (map (lambda: ([y : (a ... a -> Number)])
             (apply y zs))
           ys)))
- + - * /)
\ No newline at end of file
+ + - * /)
+
+(: map-with-funcs (All (b a ...) ((a ... a -> b) * -> (a ... a -> (Listof b)))))
+(define (map-with-funcs . fs)
+  (lambda as
+    (map (lambda: ([f : (a ... a -> b)])
+           (apply f as))
+         fs)))
+(map-with-funcs + - * /)
\ No newline at end of file

From d229e895b4862f76e3d81fe99a1dd72a057adc57 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Tue, 24 Jun 2008 11:43:06 -0400
Subject: [PATCH 71/96] new test

original commit: d7cf0a10c06ea231812e29a3f480ebe6ec7f15de
---
 collects/tests/typed-scheme/succeed/ann-map-funcs.ss | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 collects/tests/typed-scheme/succeed/ann-map-funcs.ss

diff --git a/collects/tests/typed-scheme/succeed/ann-map-funcs.ss b/collects/tests/typed-scheme/succeed/ann-map-funcs.ss
new file mode 100644
index 00000000..d5784431
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/ann-map-funcs.ss
@@ -0,0 +1,11 @@
+#lang typed-scheme
+
+(: map-with-funcs (All (b a ...) ((a ... a -> b) * -> (a ... a -> (Listof b)))))
+
+(define (map-with-funcs . fs)
+ (lambda as
+   (map (lambda: ([f : (a ... a -> b)])
+          (apply f as))
+        fs)))
+
+(ann (map-with-funcs + - * /) (Integer Integer * -> (Listof Number)))
\ No newline at end of file

From 02f34aa0fd3c4c2dfe657f75a9555243ed80e94e Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Tue, 24 Jun 2008 14:05:24 -0400
Subject: [PATCH 72/96] Check number of type errors.

original commit: 97c5444b88b79c70c1e7625361e6c6ea48284621
---
 .../tests/typed-scheme/fail/ann-map-funcs.ss    | 17 +++++++++++++++++
 collects/tests/typed-scheme/fail/apply-dots.ss  |  2 ++
 collects/tests/typed-scheme/main.ss             | 10 ++++++----
 .../tests/typed-scheme/succeed/ann-map-funcs.ss |  2 +-
 4 files changed, 26 insertions(+), 5 deletions(-)
 create mode 100644 collects/tests/typed-scheme/fail/ann-map-funcs.ss

diff --git a/collects/tests/typed-scheme/fail/ann-map-funcs.ss b/collects/tests/typed-scheme/fail/ann-map-funcs.ss
new file mode 100644
index 00000000..f8ba9fb4
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/ann-map-funcs.ss
@@ -0,0 +1,17 @@
+#;
+(exn-pred 3)
+#lang typed-scheme
+
+(: map-with-funcs (All (b a ...) ((a ... a -> b) * -> (a ... a -> (Listof b)))))
+
+(define (map-with-funcs . fs)
+ (lambda as
+   (map (lambda: ([f : (a ... a -> b)])
+          (apply f as))
+        fs)))
+
+(ann (map-with-funcs + - * /) (Number Number * -> (Listof Integer)))
+
+(ann (map-with-funcs + - * /) (Number * -> (Listof Number)))
+
+(ann (map-with-funcs + - * /) (Integer * -> (Listof Number)))
diff --git a/collects/tests/typed-scheme/fail/apply-dots.ss b/collects/tests/typed-scheme/fail/apply-dots.ss
index 69d6a129..d798f8c3 100644
--- a/collects/tests/typed-scheme/fail/apply-dots.ss
+++ b/collects/tests/typed-scheme/fail/apply-dots.ss
@@ -1,3 +1,5 @@
+#;
+(exn-pred 2)
 #lang typed-scheme
 
 (plambda: (a ...) ([z : String] . [w : Number *])
diff --git a/collects/tests/typed-scheme/main.ss b/collects/tests/typed-scheme/main.ss
index d7dfca88..81726da0 100644
--- a/collects/tests/typed-scheme/main.ss
+++ b/collects/tests/typed-scheme/main.ss
@@ -20,10 +20,12 @@
    (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))))]
+                         [(or (string? e) (regexp? e) (bytes? e))
+                          (regexp-match e (exn-message val))]))))
    args))
   
 (define (exn-pred p)
diff --git a/collects/tests/typed-scheme/succeed/ann-map-funcs.ss b/collects/tests/typed-scheme/succeed/ann-map-funcs.ss
index d5784431..a7835a36 100644
--- a/collects/tests/typed-scheme/succeed/ann-map-funcs.ss
+++ b/collects/tests/typed-scheme/succeed/ann-map-funcs.ss
@@ -8,4 +8,4 @@
           (apply f as))
         fs)))
 
-(ann (map-with-funcs + - * /) (Integer Integer * -> (Listof Number)))
\ No newline at end of file
+(ann (map-with-funcs + - * /) (Number Number * -> (Listof Number)))

From f84545ceefbe0d21d0cc6674d1e63a3da16629d6 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Tue, 1 Jul 2008 11:27:05 -0400
Subject: [PATCH 73/96] Extra require. Compile files first.

original commit: bbae1112294a6f92342af3d3ca77a139b3b1c729
---
 collects/tests/typed-scheme/main.ss           | 26 ++++++++++---------
 .../unit-tests/typecheck-tests.ss             |  2 +-
 2 files changed, 15 insertions(+), 13 deletions(-)

diff --git a/collects/tests/typed-scheme/main.ss b/collects/tests/typed-scheme/main.ss
index 81726da0..520ac6a2 100644
--- a/collects/tests/typed-scheme/main.ss
+++ b/collects/tests/typed-scheme/main.ss
@@ -4,8 +4,8 @@
 
 (require (planet schematics/schemeunit/test)
          (planet schematics/schemeunit/text-ui)
-         #;(planet schematics/schemeunit/graphical-ui)
          mzlib/etc
+         compiler/compiler
          scheme/match
          "unit-tests/all-tests.ss"
          "unit-tests/test-utils.ss")
@@ -30,11 +30,10 @@
   
 (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)])
+                (with-input-from-file p
+                  (lambda () 
+                    (read-line 'any) (read))))])
     (match sexp
       [(list-rest 'exn-pred e)
        (eval `(exn-matches . ,e) (namespace-anchor->namespace a))]
@@ -52,20 +51,23 @@
           (build-path path p)
           (lambda ()
             (parameterize ([read-accept-reader #t]
-                           [current-load-relative-directory 
-                            path])
+                           [current-load-relative-directory path]
+                           [current-directory path])
               (with-output-to-file "/dev/null" #:exists 'append
                 (lambda () (loader p)))))))))
     (apply test-suite dir
            tests)))
 
+(define (dr p)
+  ((compile-zos #f) (list p) 'auto)
+  (parameterize ([current-namespace (make-base-empty-namespace)])    
+    (dynamic-require `(file ,(path->string p)) #f)))
+
 (define succ-tests (mk-tests "succeed" 
-                             (lambda (p) (parameterize ([current-namespace (make-base-empty-namespace)])
-                                           (dynamic-require `(file ,(path->string p)) #f)))
+                             dr
                              (lambda (p thnk) (check-not-exn thnk))))
 (define fail-tests (mk-tests "fail"
-                             (lambda (p) (parameterize ([current-namespace (make-base-empty-namespace)])
-                                           (dynamic-require `(file ,(path->string p)) #f)))
+                             dr
                              (lambda (p thnk)
                                (define-values (pred info) (exn-pred p))
                                (with-check-info
diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
index bb0c8dcb..91d8d5f7 100644
--- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
@@ -11,7 +11,7 @@
                   type-name-env init-envs mutated-vars
                   effect-rep type-annotation type-utils)
          (for-syntax (private tc-utils typechecker base-env type-env))
-         (for-template (private base-env)))
+         (for-template (private base-env base-types)))
 (require (schemeunit))
 
 

From 19b45b32c4d212092c581dcbb9e6b9db256efc73 Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Tue, 1 Jul 2008 14:43:44 -0400
Subject: [PATCH 74/96] Example of nested polydots.

original commit: b90e1505d35e695f13cd81417ced00fae709223b
---
 collects/tests/typed-scheme/succeed/nested-poly.ss | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 collects/tests/typed-scheme/succeed/nested-poly.ss

diff --git a/collects/tests/typed-scheme/succeed/nested-poly.ss b/collects/tests/typed-scheme/succeed/nested-poly.ss
new file mode 100644
index 00000000..14830465
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/nested-poly.ss
@@ -0,0 +1,5 @@
+#lang typed-scheme
+
+(: f (All (A ...) (All (B ...) (A ... A -> Int))))
+
+(define (f . xs) 5)
\ No newline at end of file

From 70d1b6b4979b3429872fadc08dafe2e912d12c78 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Mon, 7 Jul 2008 11:01:42 -0400
Subject: [PATCH 75/96] values with dots

original commit: c43c3baa67512954b0f2e477aafde6f8461bd99a
---
 collects/typed-scheme/private/base-env.ss     |  3 +++
 collects/typed-scheme/private/extra-procs.ss  |  7 ++++--
 collects/typed-scheme/private/parse-type.ss   | 13 ++++++++++
 .../private/type-effect-printer.ss            |  1 +
 collects/typed-scheme/private/type-utils.ss   | 25 +++++++++++++++++--
 5 files changed, 45 insertions(+), 4 deletions(-)

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

From 6fac649e7a0a89412b20b6d937df50d8583dde15 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Mon, 7 Jul 2008 12:27:08 -0400
Subject: [PATCH 76/96] remove trace

original commit: e06a22c29b3e36cc4f51822b3d4b8ddcff6d682e
---
 collects/typed-scheme/private/type-utils.ss | 2 --
 1 file changed, 2 deletions(-)

diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index 08a022b6..e6ba3654 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -115,8 +115,6 @@
                                   (map (lambda (e) (sub-eff sb e)) els-eff))])
        target))
 
-(trace substitute-dots)
-
 ;; substitute many variables
 ;; substitution = Listof[U List[Name,Type] List[Name,Listof[Type]]]
 ;; subst-all : substition Type -> Type

From 782a227c354f138c010ec1bcb9992f2202f222bb Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Mon, 7 Jul 2008 12:54:45 -0400
Subject: [PATCH 77/96] Adding Sam's test for value dots.

original commit: 3dbf0f7ccc9ed8e2686f577ece004ad718c6982b
---
 .../tests/typed-scheme/succeed/values-dots.ss | 29 +++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 collects/tests/typed-scheme/succeed/values-dots.ss

diff --git a/collects/tests/typed-scheme/succeed/values-dots.ss b/collects/tests/typed-scheme/succeed/values-dots.ss
new file mode 100644
index 00000000..18be39f3
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/values-dots.ss
@@ -0,0 +1,29 @@
+#lang typed-scheme
+
+(require "private/extra-procs.ss")
+
+
+(call-with-values (lambda () (values 1 2)) (lambda: ([x : Number] [y : Number]) (+ x y)))
+
+(#{call-with-values* @ Integer Integer Integer} (lambda () (values 1 2)) (lambda: ([x : Integer] [y : Integer]) (+ x y)))
+
+
+(call-with-values* (lambda () (values 1 2)) (lambda: ([x : Integer] [y : Integer]) (+ x y)))
+
+(: map-with-funcs (All (b ...) ((b ... b -> b) ... b -> (b ... b -> (values b ... b)))))
+(define (map-with-funcs . fs)
+  (lambda bs
+    (apply values* (map (lambda: ([f : (b ... b -> b)])
+                          (apply f bs)) fs))))
+
+#;(map-with-funcs + - * /)
+
+(inst map-with-funcs Integer Integer)
+
+#;(map-with-funcs (lambda: ([x : Integer] [y : Integer]) (+ x y))
+                  (lambda: ([x : Integer] [y : Integer]) (- x y)))
+
+(((inst map-with-funcs Integer Integer)
+    (lambda: ([x : Integer] [y : Integer]) (+ x y))
+    (lambda: ([x : Integer] [y : Integer]) (- x y)))
+   3 4)
\ No newline at end of file

From cc2b39add337a4cede7ffed25c619e5d3eccfdaa Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Mon, 7 Jul 2008 12:56:19 -0400
Subject: [PATCH 78/96] Since this is now in a different loc, need to fix up
 the require.

original commit: 2714b3a84ac5c44af205c1a2460146e64d878daa
---
 collects/tests/typed-scheme/succeed/values-dots.ss | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/collects/tests/typed-scheme/succeed/values-dots.ss b/collects/tests/typed-scheme/succeed/values-dots.ss
index 18be39f3..25cf3496 100644
--- a/collects/tests/typed-scheme/succeed/values-dots.ss
+++ b/collects/tests/typed-scheme/succeed/values-dots.ss
@@ -1,6 +1,6 @@
 #lang typed-scheme
 
-(require "private/extra-procs.ss")
+(require typed-scheme/private/extra-procs)
 
 
 (call-with-values (lambda () (values 1 2)) (lambda: ([x : Number] [y : Number]) (+ x y)))

From bbb3e251f8c24fbe31a7144a618482356470651e Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Mon, 7 Jul 2008 14:25:15 -0400
Subject: [PATCH 79/96] More info in internal errors. Fix substitution in
 nested ... case.

original commit: 61cefef89c8120ffc46d9cc9095637d8337c924e
---
 collects/typed-scheme/private/type-utils.ss | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index e6ba3654..80d7a5ff 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -40,7 +40,8 @@
                  [#:arr dom rng rest drest thn-eff els-eff
                         (begin
                           (when (and (pair? drest)
-                                     (eq? name (cdr 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)

From 760559a6db133afb57d36769ec6358d1a38c0a55 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Mon, 7 Jul 2008 14:49:19 -0400
Subject: [PATCH 80/96] Add failure cases.

original commit: 88cbe6387952e9da5e57c46c9977a15702e41b82
---
 collects/tests/typed-scheme/fail/values-dots.ss  | 16 ++++++++++++++++
 .../tests/typed-scheme/succeed/values-dots.ss    |  7 ++++---
 2 files changed, 20 insertions(+), 3 deletions(-)
 create mode 100644 collects/tests/typed-scheme/fail/values-dots.ss

diff --git a/collects/tests/typed-scheme/fail/values-dots.ss b/collects/tests/typed-scheme/fail/values-dots.ss
new file mode 100644
index 00000000..148a2815
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/values-dots.ss
@@ -0,0 +1,16 @@
+#;
+(exn-pred 2)
+#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)))
diff --git a/collects/tests/typed-scheme/succeed/values-dots.ss b/collects/tests/typed-scheme/succeed/values-dots.ss
index 25cf3496..0078526f 100644
--- a/collects/tests/typed-scheme/succeed/values-dots.ss
+++ b/collects/tests/typed-scheme/succeed/values-dots.ss
@@ -16,12 +16,13 @@
     (apply values* (map (lambda: ([f : (b ... b -> b)])
                           (apply f bs)) fs))))
 
-#;(map-with-funcs + - * /)
+(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)))
+(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))

From e8621eecf0674be268d786e9be6d095ccebfa5cf Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Mon, 7 Jul 2008 14:49:46 -0400
Subject: [PATCH 81/96] Fix up singleton values

original commit: d0939ffa1e57894a076bfd6326c4d977cfdf3e2e
---
 collects/typed-scheme/private/type-utils.ss | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index 80d7a5ff..f17a7626 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -56,6 +56,12 @@
                                  (make-ValuesDots (map sb types) (sb dty) dbound))])
       target))
 
+;; the other definition is not accessible here
+(define (-values args)
+  (if (= (length args) 1)
+      (car args)
+      (make-Values args)))
+
 ;; 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))
@@ -63,7 +69,7 @@
       (type-case sb target
                  [#:ValuesDots types dty dbound
                                (if (eq? name dbound)
-                                   (make-Values
+                                   (-values
                                     (append 
                                      (map sb types)
                                      ;; We need to recur first, just to expand out any dotted usages of this.

From 13384db457f13ff0127c5e675285d27f3a5a68d0 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Mon, 7 Jul 2008 14:58:22 -0400
Subject: [PATCH 82/96] make-Values now checks its argument for having only 1
 element

original commit: 2844dec0a109157a05db51e8494d3f317c96c379
---
 collects/typed-scheme/private/type-effect-convenience.ss | 6 ------
 collects/typed-scheme/private/type-utils.ss              | 8 +-------
 2 files changed, 1 insertion(+), 13 deletions(-)

diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss
index cf76cb55..6f166791 100644
--- a/collects/typed-scheme/private/type-effect-convenience.ss
+++ b/collects/typed-scheme/private/type-effect-convenience.ss
@@ -140,12 +140,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))]))
diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index f17a7626..80d7a5ff 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -56,12 +56,6 @@
                                  (make-ValuesDots (map sb types) (sb dty) dbound))])
       target))
 
-;; the other definition is not accessible here
-(define (-values args)
-  (if (= (length args) 1)
-      (car args)
-      (make-Values args)))
-
 ;; 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))
@@ -69,7 +63,7 @@
       (type-case sb target
                  [#:ValuesDots types dty dbound
                                (if (eq? name dbound)
-                                   (-values
+                                   (make-Values
                                     (append 
                                      (map sb types)
                                      ;; We need to recur first, just to expand out any dotted usages of this.

From 4a8331d129c99d617f804518ceb6b022086dc927 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Mon, 7 Jul 2008 15:06:21 -0400
Subject: [PATCH 83/96] More failure tests.

original commit: 477cba1b0bdf8595b2c434fe731d29a1d5f5abda
---
 collects/tests/typed-scheme/fail/values-dots.ss | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/collects/tests/typed-scheme/fail/values-dots.ss b/collects/tests/typed-scheme/fail/values-dots.ss
index 148a2815..6c08fff5 100644
--- a/collects/tests/typed-scheme/fail/values-dots.ss
+++ b/collects/tests/typed-scheme/fail/values-dots.ss
@@ -1,5 +1,5 @@
 #;
-(exn-pred 2)
+(exn-pred 7)
 #lang typed-scheme
 
 (require typed-scheme/private/extra-procs)
@@ -14,3 +14,12 @@
 
 (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")

From ae6caf476570328826c875e05010d688c7a47c4b Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Mon, 7 Jul 2008 15:19:50 -0400
Subject: [PATCH 84/96] Fix exn-pred handling.

original commit: 41c9a2eaf17825f3af06ae16232cdd827f2864ea
---
 collects/tests/typed-scheme/main.ss | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/collects/tests/typed-scheme/main.ss b/collects/tests/typed-scheme/main.ss
index 520ac6a2..3a3d2fc7 100644
--- a/collects/tests/typed-scheme/main.ss
+++ b/collects/tests/typed-scheme/main.ss
@@ -24,20 +24,22 @@
                          [(number? e)
                           (and (exn:fail:syntax? val)
                                (= e (length (exn:fail:syntax-exprs val))))]
-                         [(or (string? e) (regexp? e) (bytes? e))
+                         [else                          
                           (regexp-match e (exn-message val))]))))
    args))
   
 (define (exn-pred p)
   (let ([sexp (with-handlers
                   ([exn:fail? (lambda _ #f)])
-                (with-input-from-file p
-                  (lambda () 
-                    (read-line 'any) (read))))])
+                (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 ()

From 6cd98e19ef8d5da2f094c33faf5b2c77237e984f Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Mon, 7 Jul 2008 15:36:45 -0400
Subject: [PATCH 85/96] Int is not a type

original commit: f2699abe6539da6e44e9a8e19fe481b26a2fa8ec
---
 collects/tests/typed-scheme/succeed/nested-poly.ss | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/collects/tests/typed-scheme/succeed/nested-poly.ss b/collects/tests/typed-scheme/succeed/nested-poly.ss
index 14830465..8b67fab8 100644
--- a/collects/tests/typed-scheme/succeed/nested-poly.ss
+++ b/collects/tests/typed-scheme/succeed/nested-poly.ss
@@ -1,5 +1,5 @@
 #lang typed-scheme
 
-(: f (All (A ...) (All (B ...) (A ... A -> Int))))
+(: f (All (A ...) (All (B ...) (A ... A -> Integer))))
 
 (define (f . xs) 5)
\ No newline at end of file

From ea5d2b8f5f75579a6a09276c832180acdda0cd13 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Mon, 7 Jul 2008 16:43:12 -0400
Subject: [PATCH 86/96] Add require of scheme/promise for force. Handle
 call-with-values more appropriately.

original commit: 589ba9d77a6d120f5cf0ebcc926518db69d391bf
---
 collects/typed-scheme/private/base-env.ss     | 10 ++++----
 .../private/type-effect-convenience.ss        | 24 ++++++++++---------
 2 files changed, 18 insertions(+), 16 deletions(-)

diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 88b2e8fb..00c6d8e7 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -7,7 +7,8 @@
  (only-in scheme/list cons? take drop add-between last)
  (only-in rnrs/lists-6 fold-left)
  '#%paramz
- (only-in scheme/match/runtime match:error))
+ (only-in scheme/match/runtime match:error)
+ scheme/promise)
 
 
 
@@ -415,17 +416,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->*
diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss
index 6f166791..9c9e1130 100644
--- a/collects/typed-scheme/private/type-effect-convenience.ss
+++ b/collects/typed-scheme/private/type-effect-convenience.ss
@@ -213,17 +213,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*)))

From dbca8c34e47113777caa5eceb164652f14c31a33 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Mon, 7 Jul 2008 17:15:10 -0400
Subject: [PATCH 87/96] Add new test for force/delay. Fix tests that have
 errors to have appropriate parameters.

original commit: 717a81283582694de7508f6251e2d880da78d8cc
---
 collects/tests/typed-scheme/succeed/force-delay.ss       | 9 +++++++++
 collects/tests/typed-scheme/succeed/string-const.ss      | 4 +++-
 .../tests/typed-scheme/unit-tests/typecheck-tests.ss     | 6 ++++--
 3 files changed, 16 insertions(+), 3 deletions(-)
 create mode 100644 collects/tests/typed-scheme/succeed/force-delay.ss

diff --git a/collects/tests/typed-scheme/succeed/force-delay.ss b/collects/tests/typed-scheme/succeed/force-delay.ss
new file mode 100644
index 00000000..fd411d55
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/force-delay.ss
@@ -0,0 +1,9 @@
+#lang typed-scheme
+
+(require scheme/promise)
+
+;((plambda: (a) ([x : a]) x) (error 'foo))
+
+(force (delay 3))
+
+(call-with-values (lambda () 3) list)
diff --git a/collects/tests/typed-scheme/succeed/string-const.ss b/collects/tests/typed-scheme/succeed/string-const.ss
index 39354bc7..8512f3c7 100644
--- a/collects/tests/typed-scheme/succeed/string-const.ss
+++ b/collects/tests/typed-scheme/succeed/string-const.ss
@@ -2,4 +2,6 @@
 
 (require string-constants/string-constant)
 
-(string-constant cancel)
\ No newline at end of file
+(string-constant cancel)
+
+(this-language)
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
index 91d8d5f7..75445e57 100644
--- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
@@ -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)))]))
@@ -648,7 +649,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)))
    )

From 89696cbcd46b7227be33f3079ada746b15b5981f Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Mon, 7 Jul 2008 19:21:42 -0400
Subject: [PATCH 88/96] Finally found a nasty bug involving variables not
 appearing in the hash table.

original commit: b835002d72e06f13991ea4adbc6d052fa6fe0c0e
---
 collects/typed-scheme/private/type-effect-printer.ss | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/collects/typed-scheme/private/type-effect-printer.ss b/collects/typed-scheme/private/type-effect-printer.ss
index 1f301705..b4fbcc44 100644
--- a/collects/typed-scheme/private/type-effect-printer.ss
+++ b/collects/typed-scheme/private/type-effect-printer.ss
@@ -66,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))]
@@ -116,12 +115,13 @@
          (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-names: (list names ... dotted) 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)]

From 0278f71d93a560a62e984a4d9c17da7ca62f564c Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Sun, 13 Jul 2008 04:35:54 -0400
Subject: [PATCH 89/96] I thought I checked this in, but apparently not!  Oops.

original commit: 05e54f0dfe619a491d7c337e4562f60f8dbdb7e9
---
 collects/tests/typed-scheme/unit-tests/typecheck-tests.ss | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
index 75445e57..a5263dd3 100644
--- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
@@ -642,6 +642,13 @@
                        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))]
         

From c9a76891bcd62bf17671bd89f7b21a1ebe1cfadc Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Sun, 13 Jul 2008 16:07:29 -0400
Subject: [PATCH 90/96] Starting to expand out the documentation in preparation
 of merging this branch back to trunk.

original commit: d6f527a96f05fe949ef032c471e2abca9bc89da9
---
 collects/typed-scheme/typed-scheme.scrbl | 50 ++++++++++++++++++++++++
 1 file changed, 50 insertions(+)

diff --git a/collects/typed-scheme/typed-scheme.scrbl b/collects/typed-scheme/typed-scheme.scrbl
index fd52f6ca..bdc2d63c 100644
--- a/collects/typed-scheme/typed-scheme.scrbl
+++ b/collects/typed-scheme/typed-scheme.scrbl
@@ -185,6 +185,10 @@ process of elimination we can determine that @scheme[t] must be a
 
 @section{Polymorphism}
 
+Typed Scheme offers abstraction over types as well as values.
+
+@subsection{Polymorphic Data Structures}
+
 Virtually every Scheme program uses lists and sexpressions.  Fortunately, Typed
 Scheme can handle these as well.  A simple list processing program can be
 written like this:
@@ -246,6 +250,52 @@ 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}
+
+@subsection{Uniform Variable-Arity Functions}
+
+@subsection{Non-Uniform Variable-Arity Functions}
+
 @section[#:tag "type-ref"]{Type Reference}
 
 @subsubsub*section{Base Types}

From 5a2792932fa0c14b02dffe12d6114ce2c2754c88 Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Sun, 13 Jul 2008 16:50:05 -0400
Subject: [PATCH 91/96] Put the beginnings of documentation here.

original commit: 4e7f527cb8ad3c2bdfc872c4da8d8e8d6725df1f
---
 collects/typed-scheme/typed-scheme.scrbl | 88 ++++++++++++++++++++++++
 1 file changed, 88 insertions(+)

diff --git a/collects/typed-scheme/typed-scheme.scrbl b/collects/typed-scheme/typed-scheme.scrbl
index bdc2d63c..74ef6cca 100644
--- a/collects/typed-scheme/typed-scheme.scrbl
+++ b/collects/typed-scheme/typed-scheme.scrbl
@@ -292,10 +292,98 @@ appear free in the body of the @scheme[All] form.
 
 @section{Variable-Arity Functions}
 
+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}

From d77d7ba57f9e2abb1e00c0cd42b45a0669c50611 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Sun, 13 Jul 2008 17:31:58 -0400
Subject: [PATCH 92/96] Fix handling of mutable structs (setters != getters)
 Allow use of #:mutable as define-typed-struct arg Fix types of random andmap
 ormap

original commit: 2456dcc18b10a10a7bad3b1f9af8e33fad03231f
---
 collects/typed-scheme/private/base-env.ss |  8 ++++----
 collects/typed-scheme/private/prims.ss    | 11 +++++++----
 2 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 00c6d8e7..348d36af 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -105,8 +105,8 @@
      [read (cl-> 
             [(-Port) -Sexp]
             [() -Sexp])]
-     [ormap (-polydots (a b) (->... (list (->... (list a) (b b) B) (-lst a)) ((-lst b) b) B))]
-     [andmap (-polydots (a b) (->... (list (->... (list a) (b b) B) (-lst a)) ((-lst b) b) B))]
+     [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)]
@@ -256,8 +256,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)
diff --git a/collects/typed-scheme/private/prims.ss b/collects/typed-scheme/private/prims.ss
index 2414b552..5c838d63 100644
--- a/collects/typed-scheme/private/prims.ss
+++ b/collects/typed-scheme/private/prims.ss
@@ -305,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)]

From 8a0c61069971d407e3877c4b313afb8947d065f7 Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Sun, 13 Jul 2008 22:33:37 -0400
Subject: [PATCH 93/96] I'm not sure how best to add this as a hit for "rest
 argument(s)" without actually putting that in the section title -- and
 truthfully, maybe it should be, for those who aren't deeply versed in PL but
 know enough Lisp/Scheme to ask for this.

original commit: e92c35d90c6558ef54f5d81191eb4c1eaf88249c
---
 collects/typed-scheme/typed-scheme.scrbl | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/collects/typed-scheme/typed-scheme.scrbl b/collects/typed-scheme/typed-scheme.scrbl
index 74ef6cca..bf85f9ee 100644
--- a/collects/typed-scheme/typed-scheme.scrbl
+++ b/collects/typed-scheme/typed-scheme.scrbl
@@ -290,7 +290,7 @@ 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}
+@section{Variable-Arity Functions: Programming with Rest Arguments}
 
 Typed Scheme can handle some uses of rest arguments.
 

From 18810e108ad5a0e519944c094074422beec5375b Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Mon, 14 Jul 2008 08:48:14 -0400
Subject: [PATCH 94/96] logging

original commit: 2866efd3485b19c98dd858b1db7e09928f0213c6
---
 collects/typed-scheme/private/base-env.ss        | 9 +++++----
 collects/typed-scheme/private/type-annotation.ss | 8 ++++----
 collects/typed-scheme/typed-scheme.ss            | 4 +++-
 3 files changed, 12 insertions(+), 9 deletions(-)

diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 348d36af..6c34b14f 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -337,15 +337,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])]
@@ -375,7 +375,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)]       
@@ -482,6 +482,7 @@
      [delete-file (-> -Pathlike -Void)]
      [make-namespace (cl->* (-> -Namespace)
                             (-> (*Un (-val 'empty) (-val 'initial)) -Namespace))]
+     [make-base-namespace (-> -Namespace)]
      [eval (-> -Sexp Univ)]
      
      [exit (-> (Un))]
diff --git a/collects/typed-scheme/private/type-annotation.ss b/collects/typed-scheme/private/type-annotation.ss
index ec214068..1a72e73b 100644
--- a/collects/typed-scheme/private/type-annotation.ss
+++ b/collects/typed-scheme/private/type-annotation.ss
@@ -30,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)))
@@ -51,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)))
@@ -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 "
diff --git a/collects/typed-scheme/typed-scheme.ss b/collects/typed-scheme/typed-scheme.ss
index 63fc8ba7..1a0d5023 100644
--- a/collects/typed-scheme/typed-scheme.ss
+++ b/collects/typed-scheme/typed-scheme.ss
@@ -40,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

From b6fc5b6d3658a68ad130e8be8930668654a9214e Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Tue, 15 Jul 2008 00:10:04 -0400
Subject: [PATCH 95/96] This is too long for the paragraph, just separate it.

original commit: 1fd8f6c2c315a6ab1b374091bc8f3511b36d934c
---
 collects/typed-scheme/typed-scheme.scrbl | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/collects/typed-scheme/typed-scheme.scrbl b/collects/typed-scheme/typed-scheme.scrbl
index bf85f9ee..43afa16c 100644
--- a/collects/typed-scheme/typed-scheme.scrbl
+++ b/collects/typed-scheme/typed-scheme.scrbl
@@ -381,8 +381,12 @@ 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))].
+is
+
+@scheme[((Boolean String Number -> Integer)
+         (Listof Boolean) (Listof String) (Listof Number)
+         ->
+         (Listof Integer))].
 
 @section[#:tag "type-ref"]{Type Reference}
 

From a42d2b6dd949e63a54af1e445a887ca95612b6a0 Mon Sep 17 00:00:00 2001
From: Stevie Strickland <sstrickl@racket-lang.org>
Date: Tue, 15 Jul 2008 00:33:14 -0400
Subject: [PATCH 96/96] Add filter-map to base-env.ss

original commit: 39c343ec18dc9a850e1461869979a7c06e8d05b4
---
 collects/typed-scheme/private/base-env.ss | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 6c34b14f..6faf49bf 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -4,7 +4,7 @@
 ;; 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)
@@ -147,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))]