diff --git a/collects/typed-scheme/env/init-envs.ss b/collects/typed-scheme/env/init-envs.ss
index 4b87fadc..73d1a9a1 100644
--- a/collects/typed-scheme/env/init-envs.ss
+++ b/collects/typed-scheme/env/init-envs.ss
@@ -22,7 +22,7 @@
   (define (gen-constructor sym)
     (string->symbol (string-append "make-" (substring (symbol->string sym) 7))))
   (match v
-    [(Union: elems) `(make-Union (list ,@(map sub elems)))]
+    [(Union: elems) `(make-Union (sort (list ,@(map sub elems)) < #:key Type-seq))]
     [(Base: n cnt) `(make-Base ',n (quote-syntax ,cnt))]
     [(Name: stx) `(make-Name (quote-syntax ,stx))]
     [(Struct: name parent flds proc poly? pred-id cert)
diff --git a/collects/typed-scheme/infer/infer-unit.ss b/collects/typed-scheme/infer/infer-unit.ss
index ee36c67c..8888f0b7 100644
--- a/collects/typed-scheme/infer/infer-unit.ss
+++ b/collects/typed-scheme/infer/infer-unit.ss
@@ -2,7 +2,7 @@
 
 (require (except-in "../utils/utils.ss"))
 (require (rep free-variance type-rep filter-rep rep-utils)
-	 (types convenience union subtype remove-intersect)
+	 (types convenience union subtype remove-intersect resolve)
 	 (except-in (utils tc-utils) make-env)
 	 (env type-name-env)
          (except-in (types utils) Dotted)
@@ -347,9 +347,9 @@
             (App: (Name: n*) args* _))
            (unless (free-identifier=? n n*)
              (fail! S T))
-           (let ([x (instantiate-poly (lookup-type-name n) args)]
-                 [y (instantiate-poly (lookup-type-name n) args*)])
-             (cg x y))]
+             (cg (resolve-once S) (resolve-once T))]
+          [((App: _ _ _) _) (cg (resolve-once S) T)]
+          [(_ (App: _ _ _)) (cg S (resolve-once T))]
           [((Values: ss) (Values: ts))
            (unless (= (length ss) (length ts))
              (fail! ss ts))
@@ -471,7 +471,7 @@
 (define (infer X S T R must-vars [expected #f])
   (with-handlers ([exn:infer? (lambda _ #f)])  
     (let ([cs (cgen/list null X S T)])
-      ;(printf "cs: ~a~n" cs)
+      (printf "cs: ~a~n" cs)
       (if (not expected)
           (subst-gen cs R must-vars)
           (subst-gen (cset-meet cs (cgen null X R expected)) R must-vars)))))
@@ -480,6 +480,7 @@
 (define (infer/vararg X S T T-var R must-vars [expected #f])
   (define new-T (if T-var (extend S T T-var) T))
   (and ((length S) . >= . (length T))
+       (printf "calling infer~n")
        (infer X S new-T R must-vars expected)))
 
 ;; like infer, but dotted-var is the bound on the ...
@@ -506,4 +507,4 @@
 (define (i s t r)
   (infer/simple (list s) (list t) r))
 
-;(trace cgen cgen/filters cgen/filter)
+(trace subst-gen cgen)
diff --git a/collects/typed-scheme/infer/infer.ss b/collects/typed-scheme/infer/infer.ss
index c660783e..8222f69f 100644
--- a/collects/typed-scheme/infer/infer.ss
+++ b/collects/typed-scheme/infer/infer.ss
@@ -3,6 +3,7 @@
 (require (except-in "../utils/utils.ss" infer))
 (require "infer-unit.ss" "constraints.ss" "dmap.ss" "signatures.ss"
          "restrict.ss" "promote-demote.ss"
+         mzlib/trace
          (only-in scheme/unit provide-signature-elements
                   define-values/invoke-unit/infer link)
          (utils unit-utils))
diff --git a/collects/typed-scheme/infer/restrict.ss b/collects/typed-scheme/infer/restrict.ss
index 140e276d..587bbe7d 100644
--- a/collects/typed-scheme/infer/restrict.ss
+++ b/collects/typed-scheme/infer/restrict.ss
@@ -2,9 +2,9 @@
 
 (require "../utils/utils.ss")
 (require (rep type-rep)
-	 (types utils union subtype remove-intersect)
+	 (types utils union subtype remove-intersect resolve)
          "signatures.ss"
-         scheme/match)
+         scheme/match mzlib/trace)
 
 (import infer^)
 (export restrict^)
@@ -12,26 +12,27 @@
 
 ;; NEW IMPL
 ;; restrict t1 to be a subtype of t2
-(define (restrict t1 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)
+         (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 vars)])
-          (and subst (restrict t1 (subst-all subst 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))]
+    [(Union? t1) (union-map (lambda (e) (restrict* e t2)) t1)]
+    [(needs-resolving? t1) (restrict* (resolve-once t1) t2)]
+    [(needs-resolving? t2) (restrict* t1 (resolve-once 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*)
+(define restrict restrict*)
diff --git a/collects/typed-scheme/rep/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss
index bcebb693..1ad80fd3 100644
--- a/collects/typed-scheme/rep/type-rep.ss
+++ b/collects/typed-scheme/rep/type-rep.ss
@@ -224,7 +224,7 @@
 							    [else #f])])
 
 ;; elems : Listof[Type]
-(dt Union ([elems (and/c (listof Type/c)
+(dt Union ([elems (and/c (listof Type/c)                         
                          (lambda (es)
                            (let-values ([(sorted? k)
                                          (for/fold ([sorted? #t]
diff --git a/collects/typed-scheme/typecheck/tc-app.ss b/collects/typed-scheme/typecheck/tc-app.ss
index aa983616..d7b175b3 100644
--- a/collects/typed-scheme/typecheck/tc-app.ss
+++ b/collects/typed-scheme/typecheck/tc-app.ss
@@ -538,6 +538,7 @@
                           (PolyDots: vars
                                      (Function: (list (and arrs (arr: doms rngs rests (and drests #f) '())) ...))))))
       (list (tc-result1: argtys-t) ...))
+     (printf "simple poly case: ~a~n" t)
      (handle-clauses (doms rngs rests arrs) f-stx args-stx
                      ;; only try inference if the argument lengths are appropriate
                      (lambda (dom _ rest a) ((if rest <= =) (length dom) (length argtys)))
diff --git a/collects/typed-scheme/types/remove-intersect.ss b/collects/typed-scheme/types/remove-intersect.ss
index 0d76e51b..f9420703 100644
--- a/collects/typed-scheme/types/remove-intersect.ss
+++ b/collects/typed-scheme/types/remove-intersect.ss
@@ -1,7 +1,7 @@
 #lang scheme/base
 
 (require (except-in "../utils/utils.ss" extend))
-(require (rep type-rep)
+(require (rep type-rep rep-utils)
 	 (types union subtype resolve convenience utils)
          scheme/match mzlib/trace)
 
@@ -9,41 +9,62 @@
 
 
 (define (overlap t1 t2)
-  (match (list t1 t2)        
-    [(list (Univ:) _) #t]
-    [(list _ (Univ:)) #t]
-    [(list (F: _) _) #t]
-    [(list _ (F: _)) #t]
-    [(list (Name: n) (Name: n*)) (free-identifier=? n n*)]
-    [(list (? Mu?) _) (overlap (unfold t1) t2)]
-    [(list _ (? Mu?)) (overlap t1 (unfold t2))]
-    [(list (Union: e) t)
-     (ormap (lambda (t*) (overlap t* t)) e)]
-    [(list t (Union: e))
-     (ormap (lambda (t*) (overlap t t*)) e)]
-    [(or (list _ (? Poly?)) (list (? Poly?) _))
-     #t] ;; these can have overlap, conservatively
-    [(list (Base: s1 _) (Base: s2 _)) (or (subtype t1 t2) (subtype t2 t1))]
-    [(list (Base: _ _) (Value: _)) (subtype t2 t1)] ;; conservative
-    [(list (Value: _) (Base: _ _)) (subtype t1 t2)] ;; conservative
-    [(list (Syntax: t) (Syntax: t*))
-     (overlap t t*)]
-    [(or (list (Syntax: _) _)
-         (list _ (Syntax: _)))
-     #f]    
-    [(list (Base: _ _) _) #f]
-    [(list _ (Base: _ _)) #f]
-    [(list (Value: (? pair? v)) (Pair: _ _)) #t]
-    [(list (Pair: _ _) (Value: (? pair? v))) #t]
-    [(list (Pair: a b) (Pair: a* b*))
-     (and (overlap a a*)
-          (overlap b b*))]
-    [(or (list (Pair: _ _) _)
-         (list _ (Pair: _ _)))
-     #f]
-    [else #t]))
+  (let ([ks (Type-key t1)] [kt (Type-key t2)])
+    (cond 
+      [(and (symbol? ks) (symbol? kt) (not (eq? ks kt))) #f]
+      [(and (symbol? ks) (pair? kt) (not (memq ks kt))) #f]
+      [(and (symbol? kt) (pair? ks) (not (memq kt ks))) #f]
+      [(and (pair? ks) (pair? kt)
+            (for/and ([i (in-list ks)]) (not (memq i kt))))
+       #f]
+      [else
+       (match (list t1 t2)        
+         [(list (Univ:) _) #t]
+         [(list _ (Univ:)) #t]
+         [(list (F: _) _) #t]
+         [(list _ (F: _)) #t]
+         [(list (Name: n) (Name: n*)) (free-identifier=? n n*)]
+         [(list (? Mu?) _) (overlap (unfold t1) t2)]
+         [(list _ (? Mu?)) (overlap t1 (unfold t2))]
+         [(list (Union: e) t)
+          (ormap (lambda (t*) (overlap t* t)) e)]
+         [(list t (Union: e))
+          (ormap (lambda (t*) (overlap t t*)) e)]
+         [(or (list _ (? Poly?)) (list (? Poly?) _))
+          #t] ;; these can have overlap, conservatively
+         [(list (Base: s1 _) (Base: s2 _)) (or (subtype t1 t2) (subtype t2 t1))]
+         [(list (Base: _ _) (Value: _)) (subtype t2 t1)] ;; conservative
+         [(list (Value: _) (Base: _ _)) (subtype t1 t2)] ;; conservative
+         [(list (Syntax: t) (Syntax: t*))
+          (overlap t t*)]
+         [(or (list (Syntax: _) _)
+              (list _ (Syntax: _)))
+          #f]    
+         [(list (Base: _ _) _) #f]
+         [(list _ (Base: _ _)) #f]
+         [(list (Value: (? pair? v)) (Pair: _ _)) #t]
+         [(list (Pair: _ _) (Value: (? pair? v))) #t]
+         [(list (Pair: a b) (Pair: a* b*))
+          (and (overlap a a*)
+               (overlap b b*))]
+         [(or (list (Pair: _ _) _)
+              (list _ (Pair: _ _)))
+          #f]
+         [(list (Struct: n _ flds _ _ _ _)
+                (Struct: n _ flds* _ _ _ _))
+          (for/and ([f flds] [f* flds*]) (overlap f f*))]
+         ;; n and n* must be different, so there's no overlap
+         [(list (Struct: n #f flds _ _ _ _)
+                (Struct: n* #f flds* _ _ _ _))
+          #f]
+         [(list (Struct: n p flds _ _ _ _)
+                (Struct: n* p* flds* _ _ _ _))
+          (and (= (length flds) (length flds*)) (for/and ([f flds] [f* flds*]) (overlap f f*)))]
+         [else #t])])))
 
 
+(trace overlap)
+
 
 ;(trace restrict)
 
diff --git a/collects/typed-scheme/types/subtype.ss b/collects/typed-scheme/types/subtype.ss
index 0a1e4768..5a700507 100644
--- a/collects/typed-scheme/types/subtype.ss
+++ b/collects/typed-scheme/types/subtype.ss
@@ -260,15 +260,6 @@
 	      ;; for unions, we check the cross-product
 	      [(list (Union: es) t) (and (andmap (lambda (elem) (subtype* A0 elem t)) es) A0)]
 	      [(list s (Union: es)) (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0)]
-	      ;; subtyping on immutable structs is covariant
-	      [(list (Struct: nm _ flds #f _ _ _) (Struct: nm _ flds* #f _ _ _))
-	       (subtypes* A0 flds flds*)]
-	      [(list (Struct: nm _ flds proc _ _ _) (Struct: nm _ flds* proc* _ _ _))
-	       (subtypes* A0 (cons proc flds) (cons proc* flds*))]
-	      ;; subtyping on structs follows the declared hierarchy
-	      [(list (Struct: nm (? Type? parent) flds proc _ _ _) other) 
-					;(printf "subtype - hierarchy : ~a ~a ~a~n" nm parent other)
-	       (subtype* A0 parent other)]
 	      ;; applications and names are structs too
 	      [(list (App: (Name: n) args stx) other)
 	       (let ([t (lookup-type-name n)])
@@ -311,6 +302,16 @@
 		 (if (Type? t)                     
 		     (subtype* A0 other t)
 		     (fail! t s)))]
+	      ;; subtyping on immutable structs is covariant
+	      [(list (Struct: nm _ flds #f _ _ _) (Struct: nm _ flds* #f _ _ _))
+               (printf "subtyping on structs: ~a ~a~n" flds flds*)
+	       (subtypes* A0 flds flds*)]
+	      [(list (Struct: nm _ flds proc _ _ _) (Struct: nm _ flds* proc* _ _ _))
+	       (subtypes* A0 (cons proc flds) (cons proc* flds*))]
+	      ;; subtyping on structs follows the declared hierarchy
+	      [(list (Struct: nm (? Type? parent) flds proc _ _ _) other) 
+					;(printf "subtype - hierarchy : ~a ~a ~a~n" nm parent other)
+	       (subtype* A0 parent other)]
 	      ;; Promises are covariant
 	      [(list (Struct: 'Promise _ (list t) _ _ _ _) (Struct: 'Promise _ (list t*) _ _ _ _)) (subtype* A0 t t*)]
 	      ;; subtyping on values is pointwise