Definition (but not use) of ... vars

original commit: 1b998d7eb8b2f35d5daf0f991bf33fc45bd4e06d

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 

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

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

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

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