* 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

collects/typed-scheme/private/infer-unit.ss

@@ -127,7 +127,10 @@
                          (cgen/list X V (extend ts ss s-rest) ts)]
                         [else (fail! S T)])]
                  [ret-mapping (cg t s)])
-             (cset-meet arg-mapping ret-mapping))]
+             (cset-meet*
+              (list arg-mapping ret-mapping
+                    (cgen/eff/list V X t-thn-eff s-thn-eff)
+                    (cgen/eff/list V X t-els-eff s-els-eff))))]
           [((arr: ts t #f (cons dty dbound) t-thn-eff t-els-eff)
             (arr: ss s #f #f                s-thn-eff s-els-eff))
            (unless (memq dbound X)
@@ -164,7 +167,10 @@
            (let* ([arg-mapping (cgen/list X V ss ts)]
                   [darg-mapping (cgen (cons dbound V) X s-dty t-dty)]
                   [ret-mapping (cg t s)])
-             (cset-meet* (list arg-mapping darg-mapping ret-mapping)))]
+             (cset-meet* 
+              (list arg-mapping darg-mapping ret-mapping
+                    (cgen/eff/list V X t-thn-eff s-thn-eff)
+                    (cgen/eff/list V X t-els-eff s-els-eff))))]
           [((arr: ts t t-rest #f                  t-thn-eff t-els-eff)
             (arr: ss s #f     (cons s-dty dbound) s-thn-eff s-els-eff))
            (unless (memq dbound X)
@@ -174,7 +180,9 @@
                (let* ([arg-mapping (cgen/list X V ss (extend ss ts t-rest))]
                       [darg-mapping (move-rest-to-dmap (cgen (cons dbound V) X s-dty t-rest) dbound)]
                       [ret-mapping (cg t s)])
-                 (cset-meet* (list arg-mapping darg-mapping ret-mapping)))
+                 (cset-meet* (list arg-mapping darg-mapping ret-mapping
+                                   (cgen/eff/list V X t-thn-eff s-thn-eff)
+                                   (cgen/eff/list V X t-els-eff s-els-eff))))
                ;; the hard case
                (let* ([num-vars (- (length ts) (length ss))]
                       [vars     (for/list ([n (in-range num-vars)])

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

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

@@ -15,7 +15,9 @@
          "lexical-env.ss" ;; maybe needs tests
          "type-annotation.ss" ;; has tests
          "effect-rep.ss"
-         scheme/private/class-internal)
+         (only-in "type-environments.ss" lookup current-tvars extend-env)
+         scheme/private/class-internal
+         (only-in srfi/1 split-at))
 
 (require (for-template scheme/base scheme/private/class-internal))
 
@@ -49,32 +51,52 @@
     [(regexp? v) -Regexp]
     [else Univ]))
 
+
+(define (do-inst stx ty)
+  (define inst (syntax-property stx 'type-inst))
+  (define (split-last l)
+    (let-values ([(all-but last-list) (split-at l (sub1 (length l)))])
+      (values all-but (car last-list))))
+  (cond [(not inst) ty]
+        [(not (or (Poly? ty) (PolyDots? ty)))
+         (tc-error/expr #:return (ret (Un)) "Cannot instantiate non-polymorphic type ~a" ty)]
+        
+        [(and (Poly? ty)
+              (not (= (length (syntax->list inst)) (Poly-n ty))))
+         (tc-error/expr #:return (ret (Un)) 
+                        "Wrong number of type arguments to polymorphic type ~a:~nexpected: ~a~ngot: ~a"
+                        ty (Poly-n ty) (length (syntax->list inst)))]
+        [(and (PolyDots? ty) (not (>= (length (syntax->list inst)) (sub1 (PolyDots-n ty)))))
+         ;; we can provide 0 arguments for the ... var
+         (tc-error/expr #:return (ret (Un)) 
+                        "Wrong number of type arguments to polymorphic type ~a:~nexpected at least: ~a~ngot: ~a"
+                        ty (sub1 (PolyDots-n ty)) (length (syntax->list inst)))]
+        [(and (PolyDots? ty) (= (length (syntax->list inst)) (PolyDots-n ty)))
+         ;; In this case, we need to check the last thing.  If it's a dotted var, then we need to
+         ;; use instantiate-poly-dotted, otherwise we do the normal thing.
+         (let-values ([(all-but-last last-stx) (split-last (syntax->list inst))])
+           (match (syntax-e last-stx)
+             [(cons last-ty-stx last-id-stx)
+              (unless (Dotted? (lookup (current-tvars) (syntax-e last-id-stx) (lambda _ #f)))
+                (tc-error/stx last-id-stx "~a is not a type variable bound with ..." (syntax-e last-id-stx)))
+              (let* ([last-id (syntax-e last-id-stx)]
+                     [last-ty
+                      (parameterize ([current-tvars (extend-env (list last-id)
+                                                                (list (make-DottedBoth (make-F last-id)))
+                                                                (current-tvars))])
+                        (parse-type last-ty-stx))])
+                (instantiate-poly-dotted ty (map parse-type all-but-last) last-ty last-id))]
+             [_
+              (instantiate-poly ty (map parse-type (syntax->list inst)))]))]
+        [else
+         (instantiate-poly ty (map parse-type (syntax->list inst)))]))
+
 ;; typecheck an identifier
 ;; the identifier has variable effect
 ;; tc-id : identifier -> tc-result
 (define (tc-id id)
-  (let* ([ty (lookup-type/lexical id)]
-         [inst (syntax-property id 'type-inst)])
-    (cond [(and inst
-                (not (or (Poly? ty) (PolyDots? ty))))
-           (tc-error/expr #:return (ret (Un)) "Cannot instantiate non-polymorphic type ~a" ty)]
-          
-          [(and inst
-                (Poly? ty)
-                (not (= (length (syntax->list inst)) (Poly-n ty))))
-           (tc-error/expr #:return (ret (Un)) 
-                          "Wrong number of type arguments to polymorphic type ~a:~nexpected: ~a~ngot: ~a"
-                          ty (Poly-n ty) (length (syntax->list inst)))]
-          [(and inst (PolyDots? ty) (not (>= (length (syntax->list inst)) (sub1 (PolyDots-n ty)))))
-           ;; we can provide 0 arguments for the ... var
-           (tc-error/expr #:return (ret (Un)) 
-                          "Wrong number of type arguments to polymorphic type ~a:~nexpected at least: ~a~ngot: ~a"
-                          ty (sub1 (PolyDots-n ty)) (length (syntax->list inst)))]
-          [else
-           (let ([ty* (if inst
-                          (instantiate-poly ty (map parse-type (syntax->list inst)))
-                          ty)])
-             (ret ty* (list (make-Var-True-Effect id)) (list (make-Var-False-Effect id))))])))
+  (let* ([ty (lookup-type/lexical id)])
+    (ret ty (list (make-Var-True-Effect id)) (list (make-Var-False-Effect id)))))
 
 ;; typecheck an expression, but throw away the effect
 ;; tc-expr/t : Expr -> Type
@@ -129,7 +151,7 @@
         [(quote-syntax datum) (ret Any-Syntax)]
         ;; mutation!
         [(set! id val)
-         (match-let* ([(tc-result: id-t) (tc-id #'id)]
+         (match-let* ([(tc-result: id-t) (tc-expr #'id)]
                       [(tc-result: val-t) (tc-expr #'val)])
            (unless (subtype val-t id-t)
              (tc-error/expr "Mutation only allowed with compatible types:~n~a is not a subtype of ~a" val-t id-t))
@@ -235,7 +257,7 @@
        (tc/letrec-values #'((name ...) ...) #'(expr ...) #'body form)]        
       ;; mutation!
       [(set! id val)
-       (match-let* ([(tc-result: id-t) (tc-id #'id)]
+       (match-let* ([(tc-result: id-t) (tc-expr #'id)]
                     [(tc-result: val-t) (tc-expr #'val)])
          (unless (subtype val-t id-t)
            (tc-error/expr "Mutation only allowed with compatible types:~n~a is not a subtype of ~a" val-t id-t))
@@ -276,9 +298,13 @@
     (unless (syntax? form) 
       (int-err "bad form input to tc-expr: ~a" form))
     ;; typecheck form
-    (cond [(type-ascription form) => (lambda (ann)
-                                       (tc-expr/check form ann))]
-          [else (internal-tc-expr form)])))
+    (let ([ty (cond [(type-ascription form) => (lambda (ann)
+                                                 (tc-expr/check form ann))]
+                    [else (internal-tc-expr form)])])
+      (match ty
+        [(tc-result: t eff1 eff2)
+         (let ([ty* (do-inst form t)])
+           (ret ty* eff1 eff2))]))))
 
 (define (tc/send rcvr method args [expected #f])
   (match (tc-expr rcvr)

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

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