diff --git a/collects/typed-scheme/typecheck/tc-app.ss b/collects/typed-scheme/typecheck/tc-app.ss
index c2531d1d..09919656 100644
--- a/collects/typed-scheme/typecheck/tc-app.ss
+++ b/collects/typed-scheme/typecheck/tc-app.ss
@@ -3,6 +3,7 @@
 (require (rename-in "../utils/utils.ss" [infer r:infer])
          "signatures.ss" "tc-metafunctions.ss"
          "tc-app-helper.ss" "find-annotation.ss"
+         "tc-subst.ss"
          syntax/parse scheme/match mzlib/trace scheme/list 
 	 unstable/sequence
          ;; fixme - don't need to be bound in this phase - only to make syntax/parse happy
@@ -731,7 +732,7 @@
   ;(printf "got to here 0~a~n" args-stx)
   (match* (ftype0 argtys)
     ;; we check that all kw args are optional
-    [((arr: dom (Values: (list (Result: t-r f-r o-r) ...)) rest #f (list (Keyword: _ _ #f) ...))
+    [((arr: dom (Values: (and results (list (Result: t-r f-r o-r) ...))) rest #f (and kws (list (Keyword: _ _ #f) ...)))
       (list (tc-result1: t-a phi-a o-a) ...))
      ;(printf "got to here 1~a~n" args-stx)
      (when check?
@@ -746,21 +747,16 @@
              [arg-t (in-list t-a)])
          (parameterize ([current-orig-stx a]) (check-below arg-t dom-t))))
      ;(printf "got to here 2 ~a ~a ~a ~n" dom names o-a)
-     (let-values ([(names o-a)
-                   (for/lists (n o) ([(d nm) (in-indexed (in-list dom))]
-                                     [oa (in-list o-a)])
-                     (values nm oa))])
-       ;(printf "got to here 3~a~n" args-stx)
-       (let* (;; Listof[FilterSet]
-              [f-r (for/list ([f f-r])
-                     (apply-filter f names o-a))]
-              ;; Listof[Object]
-              [o-r (for/list ([o o-r])
-                     (apply-object o names o-a))]
-              ;; Listof[Type]
-              [t-r (for/list ([t t-r])
-                     (apply-type t names o-a))])
-         (ret t-r f-r o-r)))]
+     (let* ([dom-count (length dom)]
+            [arg-count (+ dom-count (if rest 1 0) (length kws))]
+            [o-a (for/list ([nm (in-range arg-count)]
+                            [oa (in-sequence-forever (in-list o-a) (make-Empty))])
+                   (if (>= nm dom-count) (make-Empty) oa))])
+       (define-values (t-r f-r o-r)
+         (for/lists (t-r f-r o-r) 
+           ([r (in-list results)])
+           (open-Result r o-a)))
+       (ret t-r f-r o-r))]
     [((arr: _ _ _ drest '()) _)
      (int-err "funapp with drest args NYI")]
     [((arr: _ _ _ _ kws) _)
diff --git a/collects/typed-scheme/typecheck/tc-metafunctions.ss b/collects/typed-scheme/typecheck/tc-metafunctions.ss
index 4d193635..66f5cb61 100644
--- a/collects/typed-scheme/typecheck/tc-metafunctions.ss
+++ b/collects/typed-scheme/typecheck/tc-metafunctions.ss
@@ -30,6 +30,9 @@
           [((Bot:) _) (-FS -bot -top)]
           [(_ _) (-FS l1 l2)]))
 
+(provide combine)
+
+
 (d/c/p (abstract-filters results)
      (tc-results? . -> . (or/c Values? ValuesDots?))     
      (match results
@@ -83,111 +86,7 @@
     [(list (FilterSet: f+ f-) ...)
      (make-FilterSet (make-AndFilter f+) (make-AndFilter f-))]))
 
-(d/c/p (apply-filter fs ids os [polarity #t])
-  (->* (FilterSet/c (listof identifier?) (listof Object?)) (boolean?) FilterSet/c)
-  (match fs
-    [(FilterSet: f+ f-)
-     (combine (subst-filter* f+ ids os polarity) 
-	      (subst-filter* f- ids os polarity))]))
 
-(d/c/p (apply-type t ids os [polarity #t])
-  (->* (Type/c (listof identifier?) (listof Object?)) (boolean?) Type/c)
-  (for/fold ([t t]) ([i (in-list ids)] [o (in-list os)])
-    (subst-type t i o polarity)))
-
-(d/c/p (apply-object t ids os [polarity #t])
-  (->* (Object? (listof identifier?) (listof Object?)) (boolean?) Object?)
-  (for/fold ([t t]) ([i (in-list ids)] [o (in-list os)])
-    (subst-object t i o polarity)))
-
-(define (subst-filter* f ids os polarity)
-  (-> Filter/c (listof identifier?) (listof Object?) boolean? Filter/c)
-  (for/fold ([f f]) ([i (in-list ids)] [o (in-list os)])
-    (subst-filter f i o polarity)))
-
-(d/c/p (subst-filter-set fs id o polarity)
-       (-> FilterSet? identifier? Object? boolean? FilterSet?)
-  (match fs
-    [(FilterSet: f+ f-)
-     (combine (subst-filter f+ id o polarity) 
-	      (subst-filter f- id o polarity))]))
-
-(define (subst-type t id o polarity)
-  (define (st t) (subst-type t id o polarity))
-  (d/c (sf fs) (FilterSet? . -> . FilterSet?) (subst-filter-set fs id o polarity))
-  (type-case (#:Type st 
-	      #:Filter sf
-	      #:Object (lambda (f) (subst-object f id o polarity)))
-	      t))
-
-(define (subst-object t id o polarity)
-  (match t
-    [(NoObject:) t]
-    [(Empty:) t]
-    [(Path: p i)
-     (if (free-identifier=? i id)
-	 (match o
-	   [(Empty:) (make-Empty)]
-	   ;; the result is not from an annotation, so it isn't a NoObject
-	   [(NoObject:) (make-Empty)]
-	   [(Path: p* i*) (make-Path (append p p*) i*)])
-	 t)]))
-
-;; this is the substitution metafunction 
-(d/c/p (subst-filter f id o polarity)
-  (-> Filter/c identifier? Object? boolean? Filter/c)
-  (define (ap f) (subst-filter f o polarity))
-  (define (tf-matcher t p i id o polarity maker)
-    (match o
-      [(or (Empty:) (NoObject:)) (if polarity -top -bot)]
-      [(Path: p* i*)
-       (cond [(free-identifier=? i id)
-	      (maker
-	       (subst-type t id o polarity)
-	       (append p p*) 
-	       i*)]
-	     [(id-free-in? id t) (if polarity -top -bot)]
-	     [else f])]))
-  (match f
-    [(ImpFilter: ant consq)
-     (make-ImpFilter (subst-filter ant id o (not polarity)) (ap consq))]
-    [(AndFilter: fs) (make-AndFilter (map ap fs))]
-    [(OrFilter: fs) (make-OrFilter (map ap fs))]
-    [(Bot:) -bot]
-    [(Top:) -top]
-    [(TypeFilter: t p i)
-     (tf-matcher t p i id o polarity make-TypeFilter)]
-    [(NotTypeFilter: t p i)
-     (tf-matcher t p i id o polarity make-NotTypeFilter)]))
-
-(define (id-free-in? id type)
-  (let/ec 
-   return
-   (define (for-object o)
-     (object-case (#:Type for-type)
-		  o
-		  [#:Path p i
-			  (if (free-identifier=? i id)
-			      (return #t)
-			      o)]))
-   (define (for-filter o)
-     (filter-case (#:Type for-type
-		   #:Filter for-filter)
-		  o
-		  [#:NotTypeFilter t p i
-				   (if (free-identifier=? i id)
-				       (return #t)
-				       o)]
-		  [#:TypeFilter t p i
-				(if (free-identifier=? i id)
-				    (return #t)
-				    o)]))
-   (define (for-type t)
-     (type-case (#:Type for-type
-		 #:Filter for-filter
-		 #:Object for-object)
-		t))
-   (for-type type)))
 
 #|
 #;
@@ -253,7 +152,7 @@
   (match tc
     [(tc-results: ts) (-values ts)]))
 
-(provide combine-props tc-results->values subst-object subst-type)
+(provide combine-props tc-results->values)
 
 (define (combine-props new-props old-props)
   (define-values (new-atoms new-formulas) 
diff --git a/collects/typed-scheme/typecheck/tc-subst.ss b/collects/typed-scheme/typecheck/tc-subst.ss
new file mode 100644
index 00000000..f90fbffb
--- /dev/null
+++ b/collects/typed-scheme/typecheck/tc-subst.ss
@@ -0,0 +1,131 @@
+#lang scheme/base
+
+(require "../utils/utils.ss")
+(require (rename-in (types subtype convenience remove-intersect union utils)                   
+                    [-> -->]
+                    [->* -->*]
+                    [one-of/c -one-of/c])
+         (rep type-rep filter-rep rep-utils) scheme/list
+         scheme/contract scheme/match unstable/match
+         (for-syntax scheme/base)
+         "tc-metafunctions.ss")
+
+;(provide (all-defined-out))
+
+(define-syntax-rule (d/c/p (name . args) c . body)
+  (begin (d/c (name . args) c . body)
+         (p/c [name c])))
+
+(d/c/p (open-Result r objs)
+       (-> Result? (listof Object?) Result?)
+       (for/fold ([r r])
+         ([(o k) (in-indexed (in-list objs))])
+         (match r
+           [(Result: t fs old-obj)
+            (make-Result (subst-type t k o #t)
+                         (subst-filter-set t fs o #t)
+                         (subst-object t old-obj o #t))])))
+
+(d/c/p (subst-filter-set fs k o polarity)
+       (-> FilterSet? integer? Object? boolean? FilterSet?)
+  (match fs
+    [(FilterSet: f+ f-)
+     (combine (subst-filter f+ k o polarity) 
+	      (subst-filter f- k o polarity))]))
+
+(d/c (subst-type t k o polarity)
+     (-> Type/c integer? Object? boolean? Type/c)
+  (define (st t) (subst-type t k o polarity))
+  (d/c (sf fs) (FilterSet? . -> . FilterSet?) (subst-filter-set fs k o polarity))
+  (type-case (#:Type st 
+	      #:Filter sf
+	      #:Object (lambda (f) (subst-object f k o polarity)))
+	      t
+              [#:arr dom rng rest drest kws
+                     ;; here we have to increment the count for the domain, where the new bindings are in scope
+                     (let* ([arg-count (+ (length dom) (if rest 1 0) (if drest 1 0) (length kws))]
+                            [st* (lambda (t) (subst-type t (+ arg-count k) o polarity))])
+                       (make-arr (map st dom)
+                                 (st* rng)
+                                 (and rest (st rest))
+                                 (and drest (cons (st (car drest)) (cdr drest)))
+                                 (map st kws)))]))
+
+(d/c (subst-object t k o polarity)
+     (-> Object? integer? Object? boolean? Object?)
+  (match t
+    [(NoObject:) t]
+    [(Empty:) t]
+    [(Path: p i)
+     (if (eq? i k)
+	 (match o
+	   [(Empty:) (make-Empty)]
+	   ;; the result is not from an annotation, so it isn't a NoObject
+	   [(NoObject:) (make-Empty)]
+	   [(Path: p* i*) (make-Path (append p p*) i*)])
+	 t)]))
+
+;; this is the substitution metafunction 
+(d/c/p (subst-filter f k o polarity)
+  (-> Filter/c integer? Object? boolean? Filter/c)
+  (define (ap f) (subst-filter f o polarity))
+  (define (tf-matcher t p i k o polarity maker)
+    (match o
+      [(or (Empty:) (NoObject:)) (if polarity -top -bot)]
+      [(Path: p* i*)
+       (cond [(eq? i k)
+	      (maker
+	       (subst-type t k o polarity)
+	       (append p p*) 
+	       i*)]
+	     [(index-free-in? k t) (if polarity -top -bot)]
+	     [else f])]))
+  (match f
+    [(ImpFilter: ant consq)
+     (make-ImpFilter (subst-filter ant k o (not polarity)) (ap consq))]
+    [(AndFilter: fs) (make-AndFilter (map ap fs))]
+    [(OrFilter: fs) (make-OrFilter (map ap fs))]
+    [(Bot:) -bot]
+    [(Top:) -top]
+    [(TypeFilter: t p i)
+     (tf-matcher t p i k o polarity make-TypeFilter)]
+    [(NotTypeFilter: t p i)
+     (tf-matcher t p i k o polarity make-NotTypeFilter)]))
+
+(define (index-free-in? k type)
+  (let/ec 
+   return
+   (define (for-object o)
+     (object-case (#:Type for-type)
+		  o
+		  [#:Path p i
+			  (if (eq? i k)
+			      (return #t)
+			      o)]))
+   (define (for-filter o)
+     (filter-case (#:Type for-type
+		   #:Filter for-filter)
+		  o
+		  [#:NotTypeFilter t p i
+				   (if (eq? i k)
+				       (return #t)
+				       o)]
+		  [#:TypeFilter t p i
+				(if (eq? i k)
+				    (return #t)
+				    o)]))
+   (define (for-type t)
+     (type-case (#:Type for-type
+		 #:Filter for-filter
+		 #:Object for-object)
+		t
+                [#:arr dom rng rest drest kws
+                       ;; here we have to increment the count for the domain, where the new bindings are in scope
+                       (let* ([arg-count (+ (length dom) (if rest 1 0) (if drest 1 0) (length kws))]
+                              [st* (lambda (t) (for-type (+ arg-count k) t))])
+                         (make-arr (map for-type dom)
+                                   (st* rng)
+                                   (and rest (for-type rest))
+                                   (and drest (cons (for-type (car drest)) (cdr drest)))
+                                   (map for-type kws)))]))
+   (for-type type)))