diff --git a/collects/typed-scheme/private/infer-ops.ss b/collects/typed-scheme/private/infer-ops.ss
index b328a08285..17590cf259 100644
--- a/collects/typed-scheme/private/infer-ops.ss
+++ b/collects/typed-scheme/private/infer-ops.ss
@@ -2,13 +2,13 @@
 
 (require "type-effect-convenience.ss" "type-rep.ss" "effect-rep.ss" "rep-utils.ss"
          "free-variance.ss" "type-utils.ss" "union.ss" "tc-utils.ss"
-         "remove-intersect.ss" "subtype.ss"
+         "subtype.ss" "remove-intersect.ss"
          scheme/match
          mzlib/etc
          mzlib/trace
          scheme/list)
 
-(provide (all-defined-out))
+(provide infer infer/vararg restrict)
 
 (define-values (fail-sym exn:infer?)
   (let ([sym (gensym)])
@@ -115,8 +115,13 @@
     ([a args])
     (cset-meet a c)))
 
-
-
+;; ss and ts have the same length
+(define (cgen-union V X ss ts)
+  ;; first, we remove common elements of ss and ts
+  (let-values ([(ss* ts*)
+                (values (filter (lambda (se) (not (ormap (lambda (t) (type-equal? t se)) ts))) ss)
+                        (filter (lambda (te) (not (ormap (lambda (s) (type-equal? s te)) ss))) ts))])
+    (cgen/list V X ss* ts*)))
 
 (define (cgen V X S T)
   (define empty (empty-cset X))
@@ -127,6 +132,15 @@
      (S T)
      [(a a) empty]
      [(_ (Univ:)) empty]
+     
+     ;; two unions with the same number of elements, so we just try to unify them pairwise
+     #;[((Union: l1) (Union: l2))
+      (=> unmatch)
+      (unless (= (length l1) (length l2))
+        (unmatch))
+      (cgen-union V X l1 l2)]
+     
+     
      [((Union: es) S) (cset-meet* X (for/list ([e es]) (cgen V X e S)))]
      [(S (Union: es)) (or
                        (for/or 
@@ -146,8 +160,11 @@
                           [(or proc proc*)
                            (fail! S T)]
                           [else (values flds flds*)])])
-        (cset-meet* X (for/list ([f flds] [f* flds*])
-                        (cgen V X f f*))))]
+        (cgen/list X V flds flds*))]
+     [((Name: n) (Name: n*))
+      (if (free-identifier=? n n*)
+          null
+          (fail! S T))]
      [((Pair: a b) (Pair: a* b*))
       (cset-meet (cgen V X a a*) (cgen V X b b*))]
      ;; if we have two mu's, we rename them to have the same variable
@@ -162,9 +179,19 @@
        (App: (Name: n*) args* _))
       (unless (free-identifier=? n n*)
         (fail! S T))
-      (cset-meet* X (for/list ([a args] [a* args*]) (cgen V X a a*)))]
+      (cgen/list X V args args*)]
      [((Vector: e) (Vector: e*))
       (cset-meet (cgen V X e e*) (cgen V X e* e))]
+     [((Box: e) (Box: e*))
+      (cset-meet (cgen V X e e*) (cgen V X e* e))]
+     [((Hashtable: s1 s2) (Hashtable: t1 t2))
+      ;; the key is covariant, the value is invariant
+      (cset-meet* X (list (cgen V X s1 t1) (cgen V X t2 s2) (cgen V X s2 t2)))]
+     [((Syntax: s1) (Syntax: s2))
+      (cgen V X s1 s2)]
+     ;; parameters are just like one-arg functions
+     [((Param: in1 out1) (Param: in2 out2))
+      (cset-meet (cgen V X in2 in1) (cgen V X out1 out2))]
      [((Function: (list t-arr ...))
        (Function: (list s-arr ...)))
       (=> unmatch)
@@ -175,17 +202,13 @@
                       [(list (arr: ts t t-rest t-thn-eff t-els-eff) (arr: ss s s-rest s-thn-eff s-els-eff))
                        (let ([arg-mapping 
                               (cond [(and t-rest s-rest (= (length ts) (length ss)))
-                                     (cset-meet* X (for/list ([t (cons t-rest ts)] [s (cons s-rest ss)])
-                                                     (cgen V X s t)))]
+                                     (cgen/list X V (cons s-rest ss) (cons t-rest ts))]
                                     [(and (not t-rest) (not s-rest) (= (length ts) (length ss)))
-                                     (cset-meet* X (for/list ([t ts] [s ss])
-                                                     (cgen V X s t)))]
+                                     (cgen/list X V ss ts)]
                                     [(and t-rest (not s-rest) (<= (length ts) (length ss)))
-                                     (cset-meet* X (for/list ([s ss] [t (extend ss ts t-rest)])
-                                                             (cgen V X s t)))]
+                                     (cgen/list X V ss (extend ss ts t-rest))]
                                     [(and s-rest (not t-rest) (>= (length ts) (length ss)))
-                                     (cset-meet* X (for/list ([s (extend ts ss s-rest)] [t ts])
-                                                             (cgen V X s t)))]
+                                     (cgen/list X V (extend ts ss s-rest) ts)]
                                     [else (unmatch)])]
                              [ret-mapping (cgen V X t s)])
                          (loop (cdr t-arr) (cdr s-arr)
@@ -209,6 +232,10 @@
                  [Invariant (unless (type-equal? S T)
                               (fail! S T))
                             S])))])))
+
+(define (cgen/list X V S T)
+  (cset-meet* X (for/list ([s S] [t T]) (cgen V X s t))))
+
 ;; X : variables to infer
 ;; S : actual argument types
 ;; T : formal argument types
@@ -218,7 +245,7 @@
 ;; just return a boolean result
 (define (infer X S T R)
   (with-handlers ([exn:infer? (lambda _ #f)])
-    (let ([cs (cset-meet* X (for/list ([s S] [t T]) (cgen null X s t)))])
+    (let ([cs (cgen/list X null S T)])
     (if R
         (subst-gen cs R)
         #t))))
@@ -243,3 +270,31 @@
 
 (define (i s t r)
   (infer/simple (list s) (list t) r))
+
+;; this is *definitely* not yet correct
+
+;; NEW IMPL
+;; restrict t1 to be a subtype of t2
+(define (restrict t1 t2)     
+  ;; we don't use union map directly, since that might produce too many elements
+  (define (union-map f l)
+    (match l
+      [(Union: es) 
+       (let ([l (map f es)])
+         ;(printf "l is ~a~n" l)
+         (apply Un l))]))
+  (cond
+    [(subtype t1 t2) t1] ;; already a subtype          
+    [(match t2
+       [(Poly: vars t)
+        (let ([subst (infer vars (list t1) (list t) t1)])
+          (and subst (restrict t1 (subst-all subst t1))))]
+       [_ #f])]           
+    [(Union? t1) (union-map (lambda (e) (restrict e t2)) t1)]
+    [(Mu? t1)
+     (restrict (unfold t1) t2)]
+    [(Mu? t2) (restrict t1 (unfold t2))]
+    [(subtype t2 t1) t2] ;; we don't actually want this - want something that's a part of t1
+    [(not (overlap t1 t2)) (Un)] ;; there's no overlap, so the restriction is empty
+    [else t2] ;; t2 and t1 have a complex relationship, so we punt
+    ))
diff --git a/collects/typed-scheme/private/infer.ss b/collects/typed-scheme/private/infer.ss
index b0c5628c48..3d4c1465ad 100644
--- a/collects/typed-scheme/private/infer.ss
+++ b/collects/typed-scheme/private/infer.ss
@@ -1,5 +1,8 @@
 #lang scheme/base
 
+;; NO LONGER USED
+;; NOT YET REMOVED AS DOCUMENTATION
+
 (require "unify.ss" "type-comparison.ss" "type-rep.ss" "effect-rep.ss" "subtype.ss"
          "planet-requires.ss" "tc-utils.ss" "union.ss"
          "resolve-type.ss"
@@ -9,7 +12,7 @@
          (lib "list.ss"))
 (require (galore))
 
-(provide infer infer/list infer/list/vararg combine table:un exn:infer?)
+#;(provide infer infer/list infer/list/vararg combine table:un exn:infer?)
 
 ;; exn representing failure of inference
 ;; s,t both types
diff --git a/collects/typed-scheme/private/remove-intersect.ss b/collects/typed-scheme/private/remove-intersect.ss
index 4ad904313b..616fbb8e40 100644
--- a/collects/typed-scheme/private/remove-intersect.ss
+++ b/collects/typed-scheme/private/remove-intersect.ss
@@ -1,10 +1,10 @@
 #lang scheme/base
 
 (require "type-rep.ss" "unify.ss" "union.ss" "infer.ss" "subtype.ss"
-         "type-utils.ss" "resolve-type.ss" "type-effect-convenience.ss"
+         "type-utils.ss" "resolve-type.ss" "type-effect-convenience.ss"         
          mzlib/plt-match mzlib/trace)
 
-(provide restrict (rename-out [*remove remove]) overlap)
+(provide (rename-out [*remove remove]) overlap)
 
 
 (define (overlap t1 t2)
@@ -42,33 +42,7 @@
      #f]
     [else #t]))
 
-;; this is *definitely* not yet correct
 
-;; NEW IMPL
-;; restrict t1 to be a subtype of t2
-(define (restrict t1 t2)     
-  ;; we don't use union map directly, since that might produce too many elements
-  (define (union-map f l)
-    (match l
-      [(Union: es) 
-       (let ([l (map f es)])
-         ;(printf "l is ~a~n" l)
-         (apply Un l))]))
-  (cond
-    [(subtype t1 t2) t1] ;; already a subtype          
-    [(match t2
-       [(Poly: vars t)
-        (let ([subst (infer t t1 vars)])
-          (and subst (restrict t1 (subst-all subst t1))))]
-       [_ #f])]           
-    [(Union? t1) (union-map (lambda (e) (restrict e t2)) t1)]
-    [(Mu? t1)
-     (restrict (unfold t1) t2)]
-    [(Mu? t2) (restrict t1 (unfold t2))]
-    [(subtype t2 t1) t2] ;; we don't actually want this - want something that's a part of t1
-    [(not (overlap t1 t2)) (Un)] ;; there's no overlap, so the restriction is empty
-    [else t2] ;; t2 and t1 have a complex relationship, so we punt
-    ))
 
 ;(trace restrict)
 
diff --git a/collects/typed-scheme/private/tc-if-unit.ss b/collects/typed-scheme/private/tc-if-unit.ss
index 2de7a5289d..de8e8b6807 100644
--- a/collects/typed-scheme/private/tc-if-unit.ss
+++ b/collects/typed-scheme/private/tc-if-unit.ss
@@ -9,8 +9,8 @@
          "mutated-vars.ss"
          "subtype.ss"
          (only-in "remove-intersect.ss" 
-                  [remove *remove]
-                  restrict)
+                  [remove *remove])
+         "infer-ops.ss"
          "union.ss"
          "type-utils.ss"
          "tc-utils.ss"