annotated eta works

collects/typed-scheme/env/init-envs.ss

@@ -42,11 +42,18 @@
     [(arr: dom rng rest drest kws)
      `(make-arr ,(sub dom) ,(sub rng) ,(sub rest) ,(sub drest) ,(sub kws))]
     [(TypeFilter: t p i)
-     `(make-TypeFilter ,(sub t) ,(sub p) (quote-syntax ,i))]
+     `(make-TypeFilter ,(sub t) ,(sub p) ,(if (identifier? i)
+                                              `(quote-syntax ,i)
+                                              i))]
     [(NotTypeFilter: t p i)
-     `(make-NotTypeFilter ,(sub t) ,(sub p) (quote-syntax ,i))]
+     `(make-NotTypeFilter ,(sub t) ,(sub p) 
+                          ,(if (identifier? i)
+                               `(quote-syntax ,i)
+                               i))]
     [(Path: p i)
-     `(make-Path ,(sub p) (quote-syntax ,i))]
+     `(make-Path ,(sub p) ,(if (identifier? i)
+                               `(quote-syntax ,i)
+                               i))]
     [(? (lambda (e) (or (Filter? e)
                         (Object? e)
                         (PathElem? e)))

collects/typed-scheme/typecheck/tc-lambda-unit.ss

@@ -3,6 +3,7 @@
 (require (rename-in "../utils/utils.ss" [infer r:infer])
          "signatures.ss"
          "tc-metafunctions.ss"
+         "tc-subst.ss"
          mzlib/trace
          scheme/list
          syntax/private/util syntax/stx
@@ -201,9 +202,10 @@
        (match expected          
          [(tc-result1: (and t (Mu: _ _))) (loop (ret (unfold t)))]
          [(tc-result1: (Function: (list (arr: argss rets rests drests '()) ...)))
+          (let ([fmls (car (syntax->list formals))])            
             (for/list ([args argss] [ret rets] [rest rests] [drest drests])
-            (tc/lambda-clause/check (car (syntax->list formals)) (car (syntax->list bodies))
+              (tc/lambda-clause/check fmls (car (syntax->list bodies))
-                                    args (values->tc-results ret) rest drest))]
+                                      args (values->tc-results ret (syntax->list fmls)) rest drest)))]
          [_ (go (syntax->list formals) (syntax->list bodies) null null null)]))]
     ;; otherwise
     [else (go (syntax->list formals) (syntax->list bodies) null null null)]))

collects/typed-scheme/typecheck/tc-metafunctions.ss

@@ -72,9 +72,11 @@
   (define (rec f) (abo xs idxs f))
   (define (sb-t t) t)
   (filter-case (#:Type sb-t #:Filter rec) f
-               [#:TypeFilter t p (lookup: idx)
+               [#:TypeFilter 
+                t p (lookup: idx)
                 (make-TypeFilter t p idx)]
-               [#:NotTypeFilter t p (lookup: idx)
+               [#:NotTypeFilter
+                t p (lookup: idx)
                 (make-NotTypeFilter t p idx)]))
 
 (define (merge-filter-sets fs)
@@ -82,18 +84,6 @@
     [(list (FilterSet: f+ f-) ...)
      (make-FilterSet (make-AndFilter f+) (make-AndFilter f-))]))
 
-
-
-
-;; (or/c Values? ValuesDots?) listof[identifier] -> tc-results?
-(d/c/p (values->tc-results tc)
-  ((or/c Values? ValuesDots?) . -> . tc-results?)
-  (match tc
-    [(ValuesDots: (list (Result: ts fs os) ...) dty dbound)
-     (ret ts fs os dty dbound)]
-    [(Values: (list (Result: ts fs os) ...))
-     (ret ts fs os)]))
-
 (define (tc-results->values tc)
   (match tc
     [(tc-results: ts) (-values ts)]))

collects/typed-scheme/typecheck/tc-subst.ss

@@ -129,3 +129,17 @@
                                    (and drest (cons (for-type (car drest)) (cdr drest)))
                                    (map for-type kws)))]))
    (for-type type)))
+
+;; (or/c Values? ValuesDots?) listof[identifier] -> tc-results?
+(d/c/p (values->tc-results tc formals)
+  ((or/c Values? ValuesDots?) (listof identifier?) . -> . tc-results?)
+  (match tc
+    [(ValuesDots: (list rs ...) dty dbound)
+     (let-values ([(ts fs os) (for/lists (ts fs os) ([r (in-list rs)]) (open-Result r (map (lambda (i) (make-Path null i)) formals)))])
+       (ret ts fs os
+            (for/fold ([dty dty]) ([(o k) (in-indexed (in-list formals))])
+              (subst-type dty k (make-Path null o) #t))
+            dbound))]
+    [(Values: (list rs ...))
+     (let-values ([(ts fs os) (for/lists (ts fs os) ([r (in-list rs)]) (open-Result r (map (lambda (i) (make-Path null i)) formals)))])
+       (ret ts fs os))]))