diff --git a/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss b/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss
index caf3dda7c2..cfe775ea65 100644
--- a/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss
@@ -3,13 +3,14 @@
 (require (utils tc-utils)
 	 (env type-alias-env type-environments type-name-env init-envs)
 	 (rep type-rep)
-	 (private type-comparison parse-type subtype
-		  union type-utils)
+	 (rename-in (private type-comparison parse-type subtype
+                             union type-utils)
+                    [Un t:Un])
          (schemeunit))
 
 (require (rename-in (private type-effect-convenience) [-> t:->])
-         (private base-types)
-         (for-template (private base-types)))
+         (private base-types base-types-extra)
+         (for-template (private base-types base-types-extra)))
 
 (provide parse-type-tests)
 
@@ -72,9 +73,9 @@
    [(Number Number Number Boolean -> Number) (N N N B . t:-> . N)]
    [(Number Number Number * -> Boolean) ((list N N) N . ->* . B)]
    ;[((. Number) -> Number) (->* (list) N N)] ;; not legal syntax
-   [(U Number Boolean) (Un N B)]
-   [(U Number Boolean Number) (Un N B)]
-   [(U Number Boolean 1) (Un N B)]
+   [(U Number Boolean) (t:Un N B)]
+   [(U Number Boolean Number) (t:Un N B)]
+   [(U Number Boolean 1) (t:Un N B)]
    [(All (a) (Listof a)) (-poly (a) (make-Listof  a))]
    [(All (a ...) (a ... a -> Integer)) (-polydots (a) ( (list) (a a) . ->... . -Integer))]
    [(∀ (a) (Listof a)) (-poly (a) (make-Listof  a))]
diff --git a/collects/typed-scheme/env/init-envs.ss b/collects/typed-scheme/env/init-envs.ss
index e087666bfa..0b64510527 100644
--- a/collects/typed-scheme/env/init-envs.ss
+++ b/collects/typed-scheme/env/init-envs.ss
@@ -32,9 +32,9 @@
     [(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b))]
     [(Poly-names: ns b) `(make-Poly (list ,@(map sub ns)) ,(sub b))]
     [(PolyDots-names: ns b) `(make-PolyDots (list ,@(map sub ns)) ,(sub b))]
-    [(? Type? (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq vals))) 
+    [(? Type? (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag key seq vals))) 
      `(,(gen-constructor tag) ,@(map sub vals))]
-    [(? Effect? (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq vals))) 
+    [(? Effect? (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag key seq vals))) 
      `(,(gen-constructor tag) ,@(map sub vals))]
     [_ (basic v)]))
 
diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 4034d2ed70..c8e9b69a41 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -517,8 +517,8 @@
 [expand (-> (-Syntax Univ) (-Syntax Univ))]
 [expand-once (-> (-Syntax Univ) (-Syntax Univ))]
 
-[syntax-source (-poly (a) (-> (-Syntax a) Univ))]
-[syntax-position (-poly (a) (-> (-Syntax a) (-opt N)))]
+[syntax-source (-> (-Syntax Univ) Univ)]
+[syntax-position (-> (-Syntax Univ) (-opt N))]
 [datum->syntax (cl->*
                 (-> (-opt (-Syntax Univ)) Sym (-Syntax Sym))
                 (-> (-opt (-Syntax Univ)) Univ (-Syntax Univ)))]
@@ -538,6 +538,11 @@
 
 [maybe-print-message (-String . -> . -Void)]
 
+;; scheme/list
+[last-pair (-poly (a) ((-mu x (Un a (-val '()) (-pair a x)))
+                       . -> . 
+                       (Un (-pair a a) (-pair a (-val '())))))]
+
 ;; scheme/tcp
 [tcp-listener? (make-pred-ty -TCP-Listener)]
 [tcp-abandon-port (-Port . -> . -Void)]
diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss
index a454714ca9..526d91843e 100644
--- a/collects/typed-scheme/private/parse-type.ss
+++ b/collects/typed-scheme/private/parse-type.ss
@@ -28,10 +28,12 @@
 (define (stx-cadr stx) (stx-car (stx-cdr stx)))
 
 (define-syntax-class star
+  #:description "*"
   (pattern star:id
            #:when (eq? '* #'star.datum)))
 
 (define-syntax-class ddd
+  #:description "..."
   (pattern ddd:id
            #:when (eq? '... #'ddd.datum)))
 
@@ -77,6 +79,7 @@
 
 (define-syntax-class fun-ty
   #:literals (t:-> :)
+  #:transparent
   #:description "function type"
   ;; FIXME - shouldn't have to use syntax->datum  
   (pattern (dom*:type t:-> rng:type : pred:type)
@@ -118,31 +121,44 @@
            #:with t (-values (syntax->datum #'(ts.t ...)))))
 
 (define-syntax-class type-name
+  #:description "type name"
  (pattern i:id
           #:when (lookup-type-name #'i (lambda () #f))
           #:with t #'(make-Name #'i)
           #:when (add-type-name-reference #'i)))
 
 (define-syntax-class type-alias
+  #:description "type alias"
   (pattern i:id
            #:with t (lookup-type-alias #'i parse-type* (lambda () #f))
            #:when #'t
            #:when (add-type-name-reference #'i)))
 
-(define-syntax-class all-type  
+(define-syntax-class all-ddd-formals
+  #:description "\na sequence of identifiers with a ... after the last identifier\n"
+  (pattern (v:id ... v-last:id _:ddd)))
+
+(define-syntax-class all-formals
+  #:description "\na sequence of identifiers\n"
+  (pattern (v:id ...)))
+
+(define-syntax-class all-type 
+  #:description "All type"
+  #:transparent
   #:literals (t:All)
-  (pattern (t:All (v:id ... v-last:id _:ddd) b)  
+  (pattern (t:All :all-ddd-formals b)  
            #:with b.t (parse/get #'b t (type/tvars (cons #'v-last.datum (syntax->datum #'(v ...)))
                                                    (cons (make-Dotted (make-F #'v-last.datum))
                                                          (map make-F (syntax->datum #'(v ...))))))
            #:when (add-type-name-reference #'All)
            #:with t (make-PolyDots (syntax->datum #'(v ... v-last)) #'b.t))
-  (pattern (t:All (v:id ...) b)
+  (pattern (t:All :all-formals b)
            #:with b.t (parse/get #'b t (type/tvars (syntax->datum #'(v ...)) (map make-F (syntax->datum #'(v ...)))))
            #:when (add-type-name-reference #'All)
            #:with t (make-Poly (syntax->datum #'(v ...)) #'b.t)))
 
 (define-syntax-class type-app
+  #:attributes (t)
   (pattern (i arg:type args:type ...)
            #:declare i type
            #:when (identifier? #'i)
@@ -165,6 +181,7 @@
                   Err]))))
 
 (define-syntax-class not-kw-id
+  #:attributes (datum)
   (pattern i:id
            #:when (not (for/or ([e (syntax->list 
                                     #'(quote t:pred t:Tuple case-lambda t:U t:Rec t:Opaque t:Parameter t:Class t:Instance
@@ -174,6 +191,8 @@
            #:with datum #'i.datum))
 
 (define-syntax-class type
+  #:transparent
+  #:attributes (t)
   #:literals (quote t:pred t:Tuple case-lambda t:U t:Rec t:Opaque t:Parameter t:Class t:Instance)  
   (pattern ty
            #:declare ty (3d Type?)
diff --git a/collects/typed-scheme/private/remove-intersect.ss b/collects/typed-scheme/private/remove-intersect.ss
index d2be5958a0..ca2b264c01 100644
--- a/collects/typed-scheme/private/remove-intersect.ss
+++ b/collects/typed-scheme/private/remove-intersect.ss
@@ -3,7 +3,7 @@
 (require (except-in "../utils/utils.ss" extend))
 (require (rep type-rep)
 	 (private union subtype resolve-type type-effect-convenience type-utils)
-         mzlib/plt-match mzlib/trace)
+         scheme/match mzlib/trace)
 
 (provide (rename-out [*remove remove]) overlap)
 
diff --git a/collects/typed-scheme/private/resolve-type.ss b/collects/typed-scheme/private/resolve-type.ss
index 6526a42819..28ec18a488 100644
--- a/collects/typed-scheme/private/resolve-type.ss
+++ b/collects/typed-scheme/private/resolve-type.ss
@@ -3,7 +3,7 @@
 
 (require (rep type-rep)  (env type-name-env) (utils tc-utils)
          "type-utils.ss"
-         mzlib/plt-match
+         scheme/match
          mzlib/trace)
 
 (provide resolve-name resolve-app needs-resolving? resolve-once)
diff --git a/collects/typed-scheme/private/subtype.ss b/collects/typed-scheme/private/subtype.ss
index d0d6629bc7..0c2ffdb722 100644
--- a/collects/typed-scheme/private/subtype.ss
+++ b/collects/typed-scheme/private/subtype.ss
@@ -1,14 +1,15 @@
 #lang scheme/base
 (require "../utils/utils.ss")
 
-(require (except-in (rep type-rep effect-rep) sub-eff)
+(require (except-in (rep type-rep effect-rep rep-utils) sub-eff)
          (utils tc-utils)
 	 "type-utils.ss"
          "type-comparison.ss"
          "resolve-type.ss"
+         "type-abbrev.ss"
          (env type-name-env)
          (only-in (infer infer-dummy) unify)
-         mzlib/plt-match
+         scheme/match
          mzlib/trace)
 
 
@@ -39,13 +40,26 @@
 (define (remember s t A) (cons (seen-before s t) A))
 (define (seen? s t) (member (seen-before s t) (current-seen)))
 
+(define subtype-cache (make-hash))
+(define (cache-types s t)
+  (cache-keys (Type-seq s) (Type-seq t)))
+(define (cache-keys ks kt)
+  (hash-set! subtype-cache (cons ks kt) #t))
+(define (cached? s t)
+  (hash-ref subtype-cache (cons (Type-seq s) (Type-seq t)) #f))
 
 ;; is s a subtype of t?
 ;; type type -> boolean
 (define (subtype s t)
-  (with-handlers
-      ([exn:subtype? (lambda _ #f)])
-    (subtype* (current-seen) s t)))
+  (define k (cons (Type-seq s) (Type-seq t)))
+  (define lookup? (hash-ref subtype-cache k 'no))
+  (if (eq? 'no lookup?)
+      (let ([result (with-handlers
+                        ([exn:subtype? (lambda _ #f)])
+                      (subtype* (current-seen) s t))])
+        (hash-set! subtype-cache k result)
+        result)
+      lookup?))
 
 ;; are all the s's subtypes of all the t's?
 ;; [type] [type] -> boolean
@@ -155,139 +169,139 @@
 (define (subtype* A s t)
   (parameterize ([match-equality-test type-equal?]
                  [current-seen A])
-    (if (seen? s t)
-        A
-        (let* ([A0 (remember s t A)])
-          (parameterize ([current-seen A0])
-            #;(match t
-              [(Name: n) (when (eq? 'heap (syntax-e n))
-                             (trace subtype*))]
-              [_ #f])
+    (let ([ks (Type-key s)] [kt (Type-key t)])
+      (cond 
+       [(or (seen? s t) (type-equal? s t)) A]
+       [(and (symbol? ks) (symbol? kt) (not (eq? ks kt))) (fail! s t)]
+       [(and (symbol? ks) (pair? kt) (not (memq ks kt))) (fail! s t)]
+       [(and (pair? ks) (pair? kt)
+	     (for/and ([i (in-list ks)]) (not (memq i kt))))
+	(fail! s t)]
+       [else
+	(let* ([A0 (remember s t A)])
+	  (parameterize ([current-seen A0])
             (match (list s t)
-              ;; subtyping is reflexive
-              [(list t t) A0]              
-              ;; univ is top
-              [(list _ (Univ:)) A0]
-              ;; error is top and bot
-              [(list _ (Error:)) A0]
-              [(list (Error:) _) A0]
-              ;; (Un) is bot
-              [(list _ (Union: (list))) (fail! s t)]
-              [(list (Union: (list)) _) A0]
-              ;; value types              
-              [(list (Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))]
-              ;; integers are numbers too
-              [(list (Base: 'Integer _) (Base: 'Number _)) A0]
-              ;; values are subtypes of their "type"
-              [(list (Value: (? integer? n)) (Base: 'Integer _)) A0]
-              [(list (Value: (? number? n)) (Base: 'Number _)) A0]
-              [(list (Value: (? boolean? n)) (Base: 'Boolean _)) A0]
-              [(list (Value: (? symbol? n)) (Base: 'Symbol _)) A0]
-              [(list (Value: (? string? n)) (Base: 'String _)) A0]
-              ;; tvars are equal if they are the same variable
-              [(list (F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))]
-              ;; case-lambda
-              [(list (Function: arr1) (Function: arr2))
-               (when (null? arr1) (fail! s t))
-               (let loop-arities ([A* A0]
-                                  [arr2 arr2])
-                 (cond 
-                   [(null? arr2) A*]
-                   [(supertype-of-one/arr A* (car arr2) arr1) => (lambda (A) (loop-arities A (cdr arr2)))]
-                   [else (fail! s t)]))]
-              ;; recur structurally on pairs
-              [(list (Pair: a d) (Pair: a* d*))
-               (let ([A1 (subtype* A0 a a*)])
-                 (and A1 (subtype* A1 d d*)))]
-              ;; quantification over two types preserves subtyping
-              [(list (Poly: ns b1) (Poly: ms b2)) 
-               (=> unmatch)
-               (unless (= (length ns) (length ms)) 
-                 (unmatch))
-               ;(printf "Poly: ~n~a ~n~a~n" b1 (subst-all (map list ms (map make-F ns)) b2))
-               (subtype* A0 b1 (subst-all (map list ms (map make-F ns)) b2))]
-              ;; use unification to see if we can use the polytype here
-              [(list (Poly: vs b) s)
-               (=> unmatch)
-               (if (unify vs (list b) (list s)) A0 (unmatch))]              
-              [(list s (Poly: vs b))
-               (=> unmatch)
-               (if (null? (fv b)) (subtype* A0 s b) (unmatch))]
-              ;; names are compared for equality:
-              [(list (Name: n) (Name: n*))
-               (=> unmatch)
-               (if (free-identifier=? n n*)
-                   A0
-                   (unmatch))]
-              ;; just unfold the recursive types
-              [(list _ (? Mu?)) (subtype* A0 s (unfold t))]
-              [(list (? Mu?) _) (subtype* A0 (unfold s) t)]
-              ;; 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)])
-                 (unless (Type? t)                     
-                   (fail! s t))
-                 #;(printf "subtype: app-name: name: ~a type: ~a other: ~a ~ninst: ~a~n" (syntax-e n) t other 
-                         (instantiate-poly t args))
-                 (unless (Poly? t)
-                   (tc-error/stx stx "cannot apply non-polymorphic type ~a" t))                 
-                 (match t [(Poly-unsafe: n _)
-                           (unless (= n (length args))
-                             (tc-error/stx stx "wrong number of arguments to polymorphic type: expected ~a and got ~a"
-                                           n (length args)))])
-                 (let ([v (subtype* A0 (instantiate-poly t args) other)])
-                   #;(printf "val: ~a~n"  v)
-                   v))]
-              [(list other (App: (Name: n) args stx))
-               (let ([t (lookup-type-name n)])
-                 (unless (Type? t)                     
-                   (fail! s t))
-                 #;(printf "subtype: 2 app-name: name: ~a type: ~a other: ~a ~ninst: ~a~n" (syntax-e n) t other 
-                         (instantiate-poly t args))
-                 (unless (Poly? t)
-                   (tc-error/stx stx "cannot apply non-polymorphic type ~a" t))                 
-                 (match t [(Poly-unsafe: n _)
-                           (unless (= n (length args))
-                             (tc-error/stx stx "wrong number of arguments to polymorphic type: expected ~a and got ~a"
-                                           n (length args)))])
-                 ;(printf "about to call subtype with: ~a ~a ~n" other (instantiate-poly t args))
-                 (let ([v (subtype* A0 other (instantiate-poly t args))])
-                   #;(printf "2 val: ~a~n"  v)
-                   v))]
-              [(list (Name: n) other)
-               (let ([t (lookup-type-name n)])
-                 ;(printf "subtype: name: ~a ~a ~a~n" (syntax-e n) t other)
-                 (if (Type? t)                     
-                     (subtype* A0 t other)
-                     (fail! s t)))]
-              ;; Promises are covariant
-              [(list (Struct: 'Promise _ (list t) _ _ _ _) (Struct: 'Promise _ (list t*) _ _ _ _)) (subtype* A0 t t*)]
-              ;; subtyping on values is pointwise
-              [(list (Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)]
-              ;; single values shouldn't actually happen, but they're just like the type
-              [(list t (Values: (list t*))) (int-err "BUG - singleton values type~a" (make-Values (list t*)))]
-              [(list (Values: (list t)) t*) (int-err "BUG - singleton values type~a" (make-Values (list t)))]
-              ;; subtyping on other stuff
-              [(list (Syntax: t) (Syntax: t*))
-               (subtype* A0 t t*)]
-              [(list (Instance: t) (Instance: t*))
-               (subtype* A0 t t*)]
-              ;; otherwise, not a subtype
-              [_ (fail! s t) #;(printf "failed")]))))))
+	      [(list _ (Univ:)) A0]
+	      ;; error is top and bot
+	      [(list _ (Error:)) A0]
+	      [(list (Error:) _) A0]
+	      ;; (Un) is bot
+	      [(list _ (Union: (list))) (fail! s t)]
+	      [(list (Union: (list)) _) A0]
+	      ;; value types              
+	      [(list (Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))]
+	      ;; integers are numbers too
+	      [(list (Base: 'Integer _) (Base: 'Number _)) A0]
+	      ;; values are subtypes of their "type"
+	      [(list (Value: (? integer? n)) (Base: 'Integer _)) A0]
+	      [(list (Value: (? number? n)) (Base: 'Number _)) A0]
+	      [(list (Value: (? boolean? n)) (Base: 'Boolean _)) A0]
+	      [(list (Value: (? symbol? n)) (Base: 'Symbol _)) A0]
+	      [(list (Value: (? string? n)) (Base: 'String _)) A0]
+	      ;; tvars are equal if they are the same variable
+	      [(list (F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))]
+	      ;; case-lambda
+	      [(list (Function: arr1) (Function: arr2))
+	       (when (null? arr1) (fail! s t))
+	       (let loop-arities ([A* A0]
+				  [arr2 arr2])
+		 (cond 
+		  [(null? arr2) A*]
+		  [(supertype-of-one/arr A* (car arr2) arr1) => (lambda (A) (loop-arities A (cdr arr2)))]
+		  [else (fail! s t)]))]
+	      ;; recur structurally on pairs
+	      [(list (Pair: a d) (Pair: a* d*))
+	       (let ([A1 (subtype* A0 a a*)])
+		 (and A1 (subtype* A1 d d*)))]
+	      ;; quantification over two types preserves subtyping
+	      [(list (Poly: ns b1) (Poly: ms b2)) 
+	       (=> unmatch)
+	       (unless (= (length ns) (length ms)) 
+		       (unmatch))
+					;(printf "Poly: ~n~a ~n~a~n" b1 (subst-all (map list ms (map make-F ns)) b2))
+	       (subtype* A0 b1 (subst-all (map list ms (map make-F ns)) b2))]
+	      ;; use unification to see if we can use the polytype here
+	      [(list (Poly: vs b) s)
+	       (=> unmatch)
+	       (if (unify vs (list b) (list s)) A0 (unmatch))]              
+	      [(list s (Poly: vs b))
+	       (=> unmatch)
+	       (if (null? (fv b)) (subtype* A0 s b) (unmatch))]
+	      ;; names are compared for equality:
+	      [(list (Name: n) (Name: n*))
+	       (=> unmatch)
+	       (if (free-identifier=? n n*)
+		   A0
+		   (unmatch))]
+	      ;; just unfold the recursive types
+	      [(list _ (? Mu?)) (subtype* A0 s (unfold t))]
+	      [(list (? Mu?) _) (subtype* A0 (unfold s) t)]
+	      ;; 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)])
+		 (unless (Type? t)                     
+			 (fail! s t))
+		 #;(printf "subtype: app-name: name: ~a type: ~a other: ~a ~ninst: ~a~n" (syntax-e n) t other 
+		 (instantiate-poly t args))
+		 (unless (Poly? t)
+			 (tc-error/stx stx "cannot apply non-polymorphic type ~a" t))                 
+		 (match t [(Poly-unsafe: n _)
+			   (unless (= n (length args))
+				   (tc-error/stx stx "wrong number of arguments to polymorphic type: expected ~a and got ~a"
+						 n (length args)))])
+		 (let ([v (subtype* A0 (instantiate-poly t args) other)])
+		   #;(printf "val: ~a~n"  v)
+		   v))]
+	      [(list other (App: (Name: n) args stx))
+	       (let ([t (lookup-type-name n)])
+		 (unless (Type? t)                     
+			 (fail! s t))
+		 #;(printf "subtype: 2 app-name: name: ~a type: ~a other: ~a ~ninst: ~a~n" (syntax-e n) t other 
+		 (instantiate-poly t args))
+		 (unless (Poly? t)
+			 (tc-error/stx stx "cannot apply non-polymorphic type ~a" t))                 
+		 (match t [(Poly-unsafe: n _)
+			   (unless (= n (length args))
+				   (tc-error/stx stx "wrong number of arguments to polymorphic type: expected ~a and got ~a"
+						 n (length args)))])
+					;(printf "about to call subtype with: ~a ~a ~n" other (instantiate-poly t args))
+		 (let ([v (subtype* A0 other (instantiate-poly t args))])
+		   #;(printf "2 val: ~a~n"  v)
+		   v))]
+	      [(list (Name: n) other)
+	       (let ([t (lookup-type-name n)])
+					;(printf "subtype: name: ~a ~a ~a~n" (syntax-e n) t other)
+		 (if (Type? t)                     
+		     (subtype* A0 t other)
+		     (fail! s t)))]
+	      ;; Promises are covariant
+	      [(list (Struct: 'Promise _ (list t) _ _ _ _) (Struct: 'Promise _ (list t*) _ _ _ _)) (subtype* A0 t t*)]
+	      ;; subtyping on values is pointwise
+	      [(list (Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)]
+	      ;; single values shouldn't actually happen, but they're just like the type
+	      [(list t (Values: (list t*))) (int-err "BUG - singleton values type~a" (make-Values (list t*)))]
+	      [(list (Values: (list t)) t*) (int-err "BUG - singleton values type~a" (make-Values (list t)))]
+	      ;; subtyping on other stuff
+	      [(list (Syntax: t) (Syntax: t*))
+	       (subtype* A0 t t*)]
+	      [(list (Instance: t) (Instance: t*))
+	       (subtype* A0 t t*)]
+	      ;; otherwise, not a subtype
+	      [_ (fail! s t) #;(printf "failed")])))]))))
 
-(define (type-compare? a b)
+  (define (type-compare? a b)
   (and (subtype a b) (subtype b a)))
 
 (provide subtype type-compare? subtypes/varargs subtypes)
@@ -302,3 +316,6 @@
 
 ;(subtype (-> Univ B) (-> Univ Univ))
 ;(subtype (make-poly '(a) (make-tvar 'a)) (make-lst N))
+
+;;problem:
+;; (subtype (make-Mu 'x (make-Syntax (make-Union (list (make-Base 'Number #'number?) (make-F 'x))))) (make-Syntax (make-Univ)))
\ No newline at end of file
diff --git a/collects/typed-scheme/private/type-abbrev.ss b/collects/typed-scheme/private/type-abbrev.ss
new file mode 100644
index 0000000000..3a33b0f34d
--- /dev/null
+++ b/collects/typed-scheme/private/type-abbrev.ss
@@ -0,0 +1,235 @@
+#lang scheme
+
+(require "../utils/utils.ss")
+
+(require (rep type-rep effect-rep)
+         (utils tc-utils)
+         scheme/list
+         scheme/match
+         "type-effect-printer.ss"
+         scheme/promise
+         (for-syntax scheme/base stxclass)
+	 (for-template scheme/base scheme/contract scheme/tcp))
+
+(provide (all-defined-out))
+
+(define top-func (make-Function (list (make-top-arr))))
+
+(define (-vet id) (make-Var-True-Effect id))
+(define (-vef id) (make-Var-False-Effect id))
+
+(define -rem make-Remove-Effect)
+(define -rest make-Restrict-Effect)
+
+(define (var->type-eff eff)
+  (match eff
+    [(Var-True-Effect: v) (make-Remove-Effect (make-Value #f) v)]
+    [(Var-False-Effect: v) (make-Restrict-Effect (make-Value #f) v)]
+    [_ eff]))
+
+(define ((add-var v) eff)
+  (match eff
+    [(Latent-Var-True-Effect:) (-vet v)]
+    [(Latent-Var-False-Effect:) (-vef v)]
+    [(Latent-Restrict-Effect: t) (make-Restrict-Effect t v)]
+    [(Latent-Remove-Effect: t) (make-Remove-Effect t v)]
+    [(True-Effect:) eff]
+    [(False-Effect:) eff]
+    [_ (int-err "can't add var ~a to effect ~a" v eff)]))
+
+(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)]
+    [(_ dom ... rng : eff1 eff2)
+     #'(->* (list dom ...) rng : eff1 eff2)]
+    [(_ dom ... rng)
+     #'(->* (list dom ...) rng)]))
+
+(define-syntax ->*
+  (syntax-rules (:)
+    [(_ dom rng)       
+     (make-Function (list (make-arr* dom rng)))]
+    [(_ dom rst rng)
+     (make-Function (list (make-arr* dom rng rst)))]
+    [(_ dom rng : eff1 eff2)
+     (make-Function (list (make-arr* dom rng #f eff1 eff2)))]
+    [(_ dom rst rng : eff1 eff2)
+     (make-Function (list (make-arr* dom rng rst eff1 eff2)))]))
+(define-syntax ->...
+  (syntax-rules (:)
+    [(_ dom rng)
+     (->* dom rng)]
+    [(_ dom (dty dbound) rng)
+     (make-Function (list (make-arr* dom rng #f (cons dty 'dbound) (list) (list))))]
+    [(_ dom rng : eff1 eff2)
+     (->* dom rng : eff1 eff2)]
+    [(_ dom (dty dbound) rng : eff1 eff2)
+     (make-Function (list (make-arr* dom rng #f (cons dty 'dbound) eff1 eff2)))]))
+(define-syntax cl->
+  (syntax-rules (:)
+    [(_ [(dom ...) rng] ...)
+     (make-Function (list (make-arr* (list dom ...) rng) ...))]
+    [(_ [(dom ...) rng : eff1 eff2] ...)
+     (make-Function (list (make-arr* (list dom ...) rng #f eff1 eff2) ...))]
+    [(_ [(dom ...) rng rst : eff1 eff2] ...)
+     (make-Function (list (make-arr* (list dom ...) rng rst eff1 eff2) ...))]))
+(define (cl->* . args)
+  (define (funty-arities f)
+    (match f
+      [(Function: as) as]))
+  (make-Function (apply append (map funty-arities args))))
+
+(define-syntax (->key stx)
+  (syntax-parse stx
+                [(_ ty:expr ... ((k:keyword kty:expr opt:boolean)) ...* rng)
+                 #'(make-Function
+                    (list
+                     (make-arr* (list ty ...)
+                                rng
+                                #f
+                                #f
+                                (list (make-Keyword 'k kty opt) ...)
+                                null
+                                null)))]))
+
+(define make-arr*
+  (case-lambda [(dom rng) (make-arr dom rng #f #f null (list) (list))]
+               [(dom rng rest) (make-arr dom rng rest #f null (list) (list))]
+               [(dom rng rest eff1 eff2) (make-arr dom rng rest #f null eff1 eff2)]
+               [(dom rng rest drest eff1 eff2) (make-arr dom rng rest drest null eff1 eff2)]
+               [(dom rng rest drest kws eff1 eff2)
+                (make-arr dom rng rest drest (sort #:key Keyword-kw kws keyword<?) eff1 eff2)]))
+
+(define (make-arr-dots dom rng dty dbound)
+  (make-arr* dom rng #f (cons dty dbound) null null))
+
+(define make-promise-ty
+  (let ([s (string->uninterned-symbol "Promise")])
+    (lambda (t)
+      (make-Struct s #f (list t) #f #f #'promise? values))))
+
+(define N (make-Base 'Number #'number?))
+(define -Integer (make-Base 'Integer #'exact-integer?))
+(define B (make-Base 'Boolean #'boolean?))
+(define Sym (make-Base 'Symbol #'symbol?))
+(define -Void (make-Base 'Void #'void?))
+(define -Bytes (make-Base 'Bytes #'bytes?))
+(define -Regexp (make-Base 'Regexp #'(and/c regexp? (not/c pregexp?) (not/c byte-regexp?))))
+(define -PRegexp (make-Base 'PRegexp #'(and/c pregexp? (not/c byte-pregexp?))))
+(define -Byte-Regexp (make-Base 'Byte-Regexp #'(and/c byte-regexp? (not/c byte-pregexp?))))
+(define -Byte-PRegexp (make-Base 'Byte-PRegexp #'byte-pregexp?))
+(define -String (make-Base 'String #'string?))
+(define -Keyword (make-Base 'Keyword #'keyword?))
+(define -Char (make-Base 'Char #'char?))
+(define -Prompt-Tag (make-Base 'Prompt-Tag #'continuation-prompt-tag?))
+(define -Cont-Mark-Set (make-Base 'Continuation-Mark-Set #'continuation-mark-set?))
+(define -Path (make-Base 'Path #'path?))
+(define -Namespace (make-Base 'Namespace #'namespace?))
+(define -Output-Port (make-Base 'Output-Port #'output-port?))
+(define -Input-Port (make-Base 'Input-Port #'input-port?))
+(define -TCP-Listener (make-Base 'TCP-Listener #'tcp-listener?))
+
+(define -Syntax make-Syntax)
+(define -HT make-Hashtable)
+(define -Promise make-promise-ty)
+
+(define Univ (make-Univ))
+(define Err (make-Error))
+
+(define -Nat -Integer)
+
+(define-syntax -v 
+  (syntax-rules ()
+    [(_ x) (make-F 'x)]))
+
+(define-syntax -poly
+  (syntax-rules ()
+    [(_ (vars ...) ty)
+     (let ([vars (-v vars)] ...)
+       (make-Poly (list 'vars ...) ty))]))
+
+(define-syntax -polydots
+  (syntax-rules ()
+    [(_ (vars ... dotted) ty)
+     (let ([dotted (-v dotted)]
+           [vars (-v vars)] ...)
+       (make-PolyDots (list 'vars ... 'dotted) ty))]))
+
+(define-syntax -mu
+  (syntax-rules ()
+    [(_ var ty)
+     (let ([var (-v var)])
+       (make-Mu 'var ty))]))
+
+
+(define -values make-Values)
+
+(define-syntax *Un
+  (syntax-rules ()
+    [(_ . args) (make-Union (list . args))]))
+
+
+(define -pair make-Pair)
+
+(define -struct make-Struct)
+(define -val make-Value)
+
+(define (make-Listof elem) (-mu list-rec (*Un (-val null) (-pair elem list-rec))))
+(define -Listof (-poly (list-elem) (make-Listof list-elem)))
+
+(define -lst make-Listof)
+(define -Sexp (-mu x (*Un Sym N B -String (-val null) (-pair x x))))
+(define -Port (*Un -Input-Port -Output-Port))
+
+(define (-lst* #:tail [tail (-val null)] . args)
+  (if (null? args)
+      tail
+      (-pair (car args) (apply -lst* #:tail tail (cdr args)))))
+
+
+#;(define NE (-mu x (Un N (make-Listof x))))
+(define -NE (-mu x (*Un N (-pair x (-pair Sym (-pair x (-val null)))))))
+
+(define -Param make-Param)
+
+(define make-pred-ty
+  (case-lambda 
+    [(in out t)
+     (->* in out : (list (make-Latent-Restrict-Effect t)) (list (make-Latent-Remove-Effect t)))]
+    [(t) (make-pred-ty (list Univ) B t)]))
+
+(define -Pathlike (*Un -Path -String))
+(define -Pathlike* (*Un (-val 'up) (-val 'same) -Path -String))
+(define -Pattern (*Un -String -Bytes -Regexp -Byte-Regexp -PRegexp -Byte-PRegexp))
+(define -Byte N)
+
+(define (-Tuple l)
+  (foldr -pair (-val '()) l))
+
+(define (untuple t)
+  (match t
+    [(Value: '()) null]
+    [(Pair: a b) (cond [(untuple b) => (lambda (l) (cons a l))]
+                       [else #f])]
+    [_ #f]))
+
+(define -box make-Box)
+(define -vec make-Vector)
+
+(define Any-Syntax ;(-Syntax Univ)
+  (-mu x
+       (-Syntax (*Un 
+                 (-mu y (*Un (-pair x (*Un x y)) (-val '())))
+                 (make-Vector x)
+                 (make-Box x)
+                 N
+                 B
+		 -Keyword
+                 -String
+                 Sym))))
+
+(define Ident (-Syntax Sym))
+
+;; DO NOT USE if t contains #f
+(define (-opt t) (*Un (-val #f) t))
\ No newline at end of file
diff --git a/collects/typed-scheme/private/type-contract.ss b/collects/typed-scheme/private/type-contract.ss
index 9e1366ab36..da0990418e 100644
--- a/collects/typed-scheme/private/type-contract.ss
+++ b/collects/typed-scheme/private/type-contract.ss
@@ -121,6 +121,7 @@
              #`(syntax/c #,(t->c t)))]
         [(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))]
         [(Param: in out) #`(parameter/c #,(t->c out))]
+	[(Hashtable: k v) #`hash?]
         [else          
          (exit (fail))]))))
 
diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss
index 69c91f5196..e8a8849f61 100644
--- a/collects/typed-scheme/private/type-effect-convenience.ss
+++ b/collects/typed-scheme/private/type-effect-convenience.ss
@@ -10,241 +10,23 @@
          "union.ss"
          "subtype.ss"
          "type-utils.ss" 
+         "type-abbrev.ss"
          scheme/promise
          (for-syntax stxclass)
          (for-syntax scheme/base)
          (for-template scheme/base scheme/contract scheme/tcp))
 
-(provide (all-defined-out) 
+(provide (all-defined-out)
+         (all-from-out "type-abbrev.ss")
          ;; these should all eventually go away
          make-Name make-ValuesDots make-Function make-Latent-Restrict-Effect make-Latent-Remove-Effect)
 
 (define (one-of/c . args)
   (apply Un (map -val args)))
 
-(define top-func (make-Function (list (make-top-arr))))
-
-(define (-vet id) (make-Var-True-Effect id))
-(define (-vef id) (make-Var-False-Effect id))
-
-(define -rem make-Remove-Effect)
-(define -rest make-Restrict-Effect)
-
-(define (var->type-eff eff)
-  (match eff
-    [(Var-True-Effect: v) (make-Remove-Effect (make-Value #f) v)]
-    [(Var-False-Effect: v) (make-Restrict-Effect (make-Value #f) v)]
-    [_ eff]))
-
-(define ((add-var v) eff)
-  (match eff
-    [(Latent-Var-True-Effect:) (-vet v)]
-    [(Latent-Var-False-Effect:) (-vef v)]
-    [(Latent-Restrict-Effect: t) (make-Restrict-Effect t v)]
-    [(Latent-Remove-Effect: t) (make-Remove-Effect t v)]
-    [(True-Effect:) eff]
-    [(False-Effect:) eff]
-    [_ (int-err "can't add var ~a to effect ~a" v eff)]))
-
-(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)]
-    [(_ dom ... rng : eff1 eff2)
-     #'(->* (list dom ...) rng : eff1 eff2)]
-    [(_ dom ... rng)
-     #'(->* (list dom ...) rng)]))
-
-(define-syntax ->*
-  (syntax-rules (:)
-    [(_ dom rng)       
-     (make-Function (list (make-arr* dom rng)))]
-    [(_ dom rst rng)
-     (make-Function (list (make-arr* dom rng rst)))]
-    [(_ dom rng : eff1 eff2)
-     (make-Function (list (make-arr* dom rng #f eff1 eff2)))]
-    [(_ dom rst rng : eff1 eff2)
-     (make-Function (list (make-arr* dom rng rst eff1 eff2)))]))
-(define-syntax ->...
-  (syntax-rules (:)
-    [(_ dom rng)
-     (->* dom rng)]
-    [(_ dom (dty dbound) rng)
-     (make-Function (list (make-arr* dom rng #f (cons dty 'dbound) (list) (list))))]
-    [(_ dom rng : eff1 eff2)
-     (->* dom rng : eff1 eff2)]
-    [(_ dom (dty dbound) rng : eff1 eff2)
-     (make-Function (list (make-arr* dom rng #f (cons dty 'dbound) eff1 eff2)))]))
-(define-syntax cl->
-  (syntax-rules (:)
-    [(_ [(dom ...) rng] ...)
-     (make-Function (list (make-arr* (list dom ...) rng) ...))]
-    [(_ [(dom ...) rng : eff1 eff2] ...)
-     (make-Function (list (make-arr* (list dom ...) rng #f eff1 eff2) ...))]
-    [(_ [(dom ...) rng rst : eff1 eff2] ...)
-     (make-Function (list (make-arr* (list dom ...) rng rst eff1 eff2) ...))]))
-(define (cl->* . args)
-  (define (funty-arities f)
-    (match f
-      [(Function: as) as]))
-  (make-Function (apply append (map funty-arities args))))
-
-(define-syntax (->key stx)
-  (syntax-parse stx
-                [(_ ty:expr ... ((k:keyword kty:expr opt:boolean)) ...* rng)
-                 #'(make-Function
-                    (list
-                     (make-arr* (list ty ...)
-                                rng
-                                #f
-                                #f
-                                (list (make-Keyword 'k kty opt) ...)
-                                null
-                                null)))]))
-
-(define make-arr*
-  (case-lambda [(dom rng) (make-arr dom rng #f #f null (list) (list))]
-               [(dom rng rest) (make-arr dom rng rest #f null (list) (list))]
-               [(dom rng rest eff1 eff2) (make-arr dom rng rest #f null eff1 eff2)]
-               [(dom rng rest drest eff1 eff2) (make-arr dom rng rest drest null eff1 eff2)]
-               [(dom rng rest drest kws eff1 eff2)
-                (make-arr dom rng rest drest (sort #:key Keyword-kw kws keyword<?) eff1 eff2)]))
-
-(define (make-arr-dots dom rng dty dbound)
-  (make-arr* dom rng #f (cons dty dbound) null null))
-
-(define make-promise-ty
-  (let ([s (string->uninterned-symbol "Promise")])
-    (lambda (t)
-      (make-Struct s #f (list t) #f #f #'promise? values))))
-
-(define N (make-Base 'Number #'number?))
-(define -Integer (make-Base 'Integer #'exact-integer?))
-(define B (make-Base 'Boolean #'boolean?))
-(define Sym (make-Base 'Symbol #'symbol?))
-(define -Void (make-Base 'Void #'void?))
-(define -Bytes (make-Base 'Bytes #'bytes?))
-(define -Regexp (make-Base 'Regexp #'(and/c regexp? (not/c pregexp?) (not/c byte-regexp?))))
-(define -PRegexp (make-Base 'PRegexp #'(and/c pregexp? (not/c byte-pregexp?))))
-(define -Byte-Regexp (make-Base 'Byte-Regexp #'(and/c byte-regexp? (not/c byte-pregexp?))))
-(define -Byte-PRegexp (make-Base 'Byte-PRegexp #'byte-pregexp?))
-(define -String (make-Base 'String #'string?))
-(define -Keyword (make-Base 'Keyword #'keyword?))
-(define -Char (make-Base 'Char #'char?))
-(define -Prompt-Tag (make-Base 'Prompt-Tag #'continuation-prompt-tag?))
-(define -Cont-Mark-Set (make-Base 'Continuation-Mark-Set #'continuation-mark-set?))
-(define -Path (make-Base 'Path #'path?))
-(define -Namespace (make-Base 'Namespace #'namespace?))
-(define -Output-Port (make-Base 'Output-Port #'output-port?))
-(define -Input-Port (make-Base 'Input-Port #'input-port?))
-(define -TCP-Listener (make-Base 'TCP-Listener #'tcp-listener?))
-
-(define -Syntax make-Syntax)
-(define -HT make-Hashtable)
-(define -Promise make-promise-ty)
-
-(define Univ (make-Univ))
-(define Err (make-Error))
-
-(define -Nat -Integer)
-
-(define-syntax -v 
-  (syntax-rules ()
-    [(_ x) (make-F 'x)]))
-
-(define-syntax -poly
-  (syntax-rules ()
-    [(_ (vars ...) ty)
-     (let ([vars (-v vars)] ...)
-       (make-Poly (list 'vars ...) ty))]))
-
-(define-syntax -polydots
-  (syntax-rules ()
-    [(_ (vars ... dotted) ty)
-     (let ([dotted (-v dotted)]
-           [vars (-v vars)] ...)
-       (make-PolyDots (list 'vars ... 'dotted) ty))]))
-
-(define-syntax -mu
-  (syntax-rules ()
-    [(_ var ty)
-     (let ([var (-v var)])
-       (make-Mu 'var ty))]))
-
-
-(define -values make-Values)
-
-(define-syntax *Un
-  (syntax-rules ()
-    [(_ . args) (make-Union (list . args))]))
-
-
-(define -pair make-Pair)
-
-(define -struct make-Struct)
-(define -val make-Value)
-
-(define (make-Listof elem) (-mu list-rec (*Un (-val null) (-pair elem list-rec))))
-(define -Listof (-poly (list-elem) (make-Listof list-elem)))
-
-(define -lst make-Listof)
-(define -Sexp (-mu x (*Un Sym N B -String (-val null) (-pair x x))))
-(define -Port (*Un -Input-Port -Output-Port))
-
-(define (-lst* #:tail [tail (-val null)] . args)
-  (if (null? args)
-      tail
-      (-pair (car args) (apply -lst* #:tail tail (cdr args)))))
-
-
-#;(define NE (-mu x (Un N (make-Listof x))))
-(define -NE (-mu x (*Un N (-pair x (-pair Sym (-pair x (-val null)))))))
-
 (define (Un/eff . args)
   (apply Un (map tc-result-t args)))
 
-(define -Param make-Param)
-
-(define make-pred-ty
-  (case-lambda 
-    [(in out t)
-     (->* in out : (list (make-Latent-Restrict-Effect t)) (list (make-Latent-Remove-Effect t)))]
-    [(t) (make-pred-ty (list Univ) B t)]))
-
-(define -Pathlike (*Un -Path -String))
-(define -Pathlike* (*Un (-val 'up) (-val 'same) -Path -String))
-(define -Pattern (*Un -String -Bytes -Regexp -Byte-Regexp -PRegexp -Byte-PRegexp))
-(define -Byte N)
-
-(define (-Tuple l)
-  (foldr -pair (-val '()) l))
-
-(define (untuple t)
-  (match t
-    [(Value: '()) null]
-    [(Pair: a b) (cond [(untuple b) => (lambda (l) (cons a l))]
-                       [else #f])]
-    [_ #f]))
-
-(define -box make-Box)
-(define -vec make-Vector)
-
-(define Any-Syntax 
-  (-mu x
-       (-Syntax (*Un 
-                 (-lst x)                       
-                 (-mu y (*Un x (-pair x y)))
-                 (make-Vector x)
-                 (make-Box x)
-                 N
-                 B
-                 -String
-                 Sym))))
-
-(define Ident (-Syntax Sym))
-
-;; DO NOT USE if t contains #f
-(define (-opt t) (*Un (-val #f) t))
 
 (define-syntax (make-env stx)
   (syntax-case stx ()
diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss
index f813a19ef6..0617aa0f86 100644
--- a/collects/typed-scheme/private/type-utils.ss
+++ b/collects/typed-scheme/private/type-utils.ss
@@ -5,7 +5,7 @@
 (require (rep type-rep effect-rep rep-utils)
          (utils tc-utils)
          (only-in (rep free-variance) combine-frees)
-         mzlib/plt-match
+         scheme/match
          scheme/list
          mzlib/trace
          (for-syntax scheme/base))
@@ -33,10 +33,11 @@
 
 
 ;; substitute : Type Name Type -> Type
-(define (substitute image name target)    
+(define (substitute image name target #:Un [Un (get-union-maker)])
   (define (sb t) (substitute image name t))
   (if (hash-ref (free-vars* target) name #f)
       (type-case sb target
+		 [#:Union tys (Un (map sb tys))]
                  [#:F name* (if (eq? name* name) image target)]
                  [#:arr dom rng rest drest kws thn-eff els-eff
                         (begin
@@ -141,7 +142,7 @@
 ;; must be applied to a Mu
 (define (unfold t)
   (match t
-    [(Mu: name b) (substitute t name b)]
+    [(Mu: name b) (substitute t name b #:Un (lambda (tys) (make-Union (sort tys < #:key Type-seq))))]
     [_ (int-err "unfold: requires Mu type, got ~a" t)]))
 
 (define (instantiate-poly t types)
diff --git a/collects/typed-scheme/private/union.ss b/collects/typed-scheme/private/union.ss
index d2235d658f..816dbe7eb9 100644
--- a/collects/typed-scheme/private/union.ss
+++ b/collects/typed-scheme/private/union.ss
@@ -4,7 +4,9 @@
 
 (require (rep type-rep rep-utils)
 	 (utils tc-utils)
+	 "type-utils.ss"
 	 "subtype.ss" 
+         "type-abbrev.ss"
          "type-effect-printer.ss" 
          "type-comparison.ss"
          scheme/match mzlib/trace)
@@ -32,6 +34,7 @@
 (define Un
   (case-lambda 
     [() empty-union]
+    [(t) t]
     [args
      ;; a is a Type (not a union type)
      ;; b is a List[Type]
@@ -50,7 +53,7 @@
           (if (andmap Values? types)
               (make-Values (apply map Un (map Values-types types)))
               (int-err "Un: should not take the union of multiple values with some other type: ~a" types))]
-         [else (make-union* #;(remove-subtypes types) (foldr union2 null (remove-subtypes types)))]))]))
+         [else (make-union* #;(remove-subtypes types) (foldr union2 '() (remove-subtypes types)))]))]))
 
 #;(defintern (Un-intern args) (lambda (_ args) (apply Un args)) args)
 
diff --git a/collects/typed-scheme/rep/interning.ss b/collects/typed-scheme/rep/interning.ss
index d9eb6ff41d..2430ee4af9 100644
--- a/collects/typed-scheme/rep/interning.ss
+++ b/collects/typed-scheme/rep/interning.ss
@@ -1,25 +1,25 @@
 #lang scheme/base
 
-(require syntax/boundmap)
+(require syntax/boundmap (for-syntax scheme/base stxclass))
 
 (provide defintern hash-id)
 
 
-(define-syntax defintern
-  (syntax-rules ()
-    [(_ name+args make-name key) 
-     (defintern name+args (lambda () (make-hash #;'weak)) make-name key)]
-    [(_ (*name arg ...) make-ht make-name key-expr)
-     (define *name
-       (let ([table (make-ht)])
-         (lambda (arg ...)
-           #;(all-count!)
-           (let ([key key-expr])
-             (hash-ref table key
-                       (lambda ()
-                         (let ([new (make-name (count!) arg ...)])
-                           (hash-set! table key new)
-                           new)))))))]))
+(define-syntax (defintern stx)
+  (syntax-parse stx
+    [(_ name+args make-name key ([#:extra-arg e:expr]) ...*) 
+     #'(defintern name+args (lambda () (make-hash #;'weak)) make-name key #:extra-arg e ...)]
+    [(_ (*name:id arg:id ...) make-ht make-name key-expr ([#:extra-arg e:expr]) ...*)
+     #'(define *name
+	 (let ([table (make-ht)])
+	   (lambda (arg ...)
+	     #;(all-count!)
+	     (let ([key key-expr])
+	       (hash-ref table key
+			 (lambda ()
+			   (let ([new (make-name (count!) e ... arg ...)])
+			     (hash-set! table key new)
+			     new)))))))]))
 
 (define (make-count!)
   
diff --git a/collects/typed-scheme/rep/rep-utils.ss b/collects/typed-scheme/rep/rep-utils.ss
index 14e39c96a9..2d2ecc7d98 100644
--- a/collects/typed-scheme/rep/rep-utils.ss
+++ b/collects/typed-scheme/rep/rep-utils.ss
@@ -8,12 +8,13 @@
          "interning.ss"
          mzlib/etc
          (for-syntax 
+          stxclass
           scheme/base
           syntax/struct
           syntax/stx
-	  (utils utils)))
+	  (rename-in (utils utils) [id mk-id])))
 
-(provide == dt de print-type* print-effect* Type Type? Effect Effect? defintern hash-id Type-seq Effect-seq)
+(provide == dt de print-type* print-effect* Type Type? Effect Effect? defintern hash-id Type-seq Effect-seq Type-key)
 
 
 
@@ -25,9 +26,9 @@
 
 
 ;; all types are Type?
-(define-struct/printer Type (seq) (lambda (a b c) ((unbox print-type*) a b c)))
+(define-struct/printer Type (seq key) (lambda (a b c) ((unbox print-type*) a b c)))
 
-(define-struct/printer Effect (seq) (lambda (a b c) ((unbox print-effect*) a b c)))
+(define-struct/printer Effect (seq key) (lambda (a b c) ((unbox print-effect*) a b c)))
 
 
 
@@ -43,119 +44,88 @@
 
 (define-syntaxes (dt de)
   (let ()
-    (define (parse-opts opts stx)
-      (let loop ([provide? #t] [intern? #f] [frees #t] [fold-rhs #f] [opts opts])
-        (cond 
-          [(null? opts) (values provide? intern? frees fold-rhs)]
-          [(eq? '#:no-provide (syntax-e (stx-car opts)))
-           (loop #f intern? frees fold-rhs (cdr opts))]
-          [(eq? '#:no-frees (syntax-e (stx-car opts)))
-           (loop #f intern? #f fold-rhs (cdr opts))]
-          [(not (and (stx-pair? opts) (stx-pair? (stx-car opts))))
-           (raise-syntax-error #f "bad options" stx)]
-          [(eq? '#:intern (syntax-e (stx-car (car opts))))
-           (loop provide? (stx-car (stx-cdr (car opts))) frees fold-rhs (cdr opts))]
-          [(eq? '#:frees (syntax-e (stx-car (car opts))))
-           (loop provide? intern? (stx-cdr (car opts)) fold-rhs (cdr opts))]
-          [(eq? '#:fold-rhs (syntax-e (stx-car (car opts))))
-           (loop provide? intern? frees (stx-cdr (car opts)) (cdr opts))]
-          [else (raise-syntax-error #f "bad options" stx)])))
+    (define-syntax-class no-provide-kw
+      (pattern #:no-provide))
+    (define-syntax-class idlist
+      (pattern (i:id ...)))
+    (define (combiner f flds)
+      (syntax-parse flds
+        [() #'empty-hash-table]
+        [(e) #`(#,f e)]
+        [(e ...) #`(combine-frees (list (#,f e) ...))]))
+    (define-syntax-class frees-pat
+      #:transparent
+      #:attributes (f1 f2)
+      (pattern (f1:expr f2:expr))
+      (pattern (#f)
+               #:with f1 #'empty-hash-table
+               #:with f2 #'empty-hash-table))
+    (define-syntax-class fold-pat
+      #:transparent
+      #:attributes (e)
+      (pattern #:base
+               #:with e fold-target)
+      (pattern ex:expr
+	       #:with e #'#'ex))
     (define (mk par ht-stx)        
       (lambda (stx)          
-        (syntax-case stx ()
-          [(dform nm flds . opts)
-           (let*-values ([(provide? intern? frees fold-rhs) (parse-opts (syntax->list #'opts) #'opts)]
-                         [(kw) (string->keyword (symbol->string (syntax-e #'nm)))])
-             (with-syntax* 
-                 ([ex (id #'nm #'nm ":")]
-                  [kw-stx kw]
-                  [parent par]
-                  [(s:ty maker pred acc ...) (build-struct-names #'nm (syntax->list #'flds) #f #t #'nm)]
-                  [(flds* ...) #'flds]
-                  [*maker (id #'nm "*" #'nm)]
-                  [**maker (id #'nm "**" #'nm)]
-                  [ht-stx ht-stx]
-                  [bfs-fold-rhs (cond [(and fold-rhs (eq? (syntax-e (stx-car fold-rhs)) '#:base))
-                                       #`(lambda (tr er) #,fold-target)]
-                                      [(and fold-rhs (stx-pair? fold-rhs))
-                                       (with-syntax ([fr (stx-car fold-rhs)])
-                                         #'(lambda (tr er) 
-                                             #'fr))]
-                                      [fold-rhs (raise-syntax-error fold-rhs "something went wrong")]
-                                      [else #'(lambda (type-rec-id effect-rec-id) #`(*maker (#,type-rec-id flds*) ...))])]
-                  [provides (if provide? 
-                                #`(begin 
-                                    (provide ex pred acc ...)
-                                    (provide (rename-out [*maker maker])))
-                                #'(begin))]
-                  [intern (cond 
-                            [(syntax? intern?)
-                             #`(defintern (**maker . flds) maker #,intern?)]                                        
-                            [(null? (syntax-e #'flds))
-                             #'(defintern (**maker . flds) maker #f)]
-                            [(stx-null? (stx-cdr #'flds)) #'(defintern (**maker . flds) maker . flds)]
-                            [else #'(defintern (**maker . flds) maker (list . flds))])]
-                  [frees (cond
-                           [(not frees) #'(begin)]
-                           ;; we know that this has no free vars
-                           [(and (pair? frees) (syntax? (car frees)) (not (syntax-e (car frees))))
-                            (syntax/loc stx
-                              (define (*maker . flds)
-                                (define v (**maker . flds)) 
-                                #;(printf  "~a entered in #f case~n" '*maker)
-                                (unless-in-table 
-                                 var-table v
-                                 (hash-set! var-table v empty-hash-table)
-                                 (hash-set! index-table v empty-hash-table))
-                                v))]
-                           ;; we provided an expression each for calculating the free vars and free idxs
-                           ;; this should really be 2 expressions, one for each kind
-                           [(and (pair? frees) (pair? (cdr frees)))
-                            (quasisyntax/loc
-                                stx
-                              (define (*maker . flds)
-                                (define v (**maker . flds))
-                                #;(printf  "~a entered in expr case ~n~a~n~a ~n" '*maker '#,(car frees) '#,(cadr frees))
-                                #,
-                                (quasisyntax/loc (car frees)
-                                  (unless-in-table 
-                                   var-table v
-                                   (hash-set! var-table v #,(car frees))
-                                   (hash-set! index-table v #,(cadr frees))))
-                                #;(printf  "~a exited in expr case~n" '*maker)
-                                v))]                                       
-                           [else 
-                            (let 
-                                ([combiner 
-                                  (lambda (f flds)
-                                    (syntax-case flds ()
-                                      [() #'empty-hash-table]
-                                      [(e) #`(#,f e)]
-                                      [(e ...) #`(combine-frees (list (#,f e) ...))]))])
-                              (quasisyntax/loc stx
-                                (define (*maker . flds)
-                                  (define v (**maker . flds))
-                                  #;(printf  "~a entered in default case~n" '*maker)
-                                  (unless-in-table 
-                                   var-table v
-                                   (define fvs #,(combiner #'free-vars* #'flds))
-                                   (define fis #,(combiner #'free-idxs* #'flds))
-                                   (hash-set! var-table v fvs)
-                                   (hash-set! index-table v fis))
-                                  v)))])])
-               #`(begin
-                   (define-struct (nm parent) flds #:inspector #f)
-                   (define-match-expander ex
-                     (lambda (s)
-                       (... 
-                        (syntax-case s ()
-                          [(__ . fs) 
-                           (with-syntax ([flds** (syntax/loc s (_ . fs))])
-                             (quasisyntax/loc s (struct nm flds**)))]))))
-                   (begin-for-syntax
-                     (hash-set! ht-stx 'kw-stx (list #'ex #'flds bfs-fold-rhs #'#,stx)))
-                   intern
-                   provides
-                   frees)))])))
-    (values (mk #'Type #'type-name-ht) (mk #'Effect #'effect-name-ht))))
+        (syntax-parse stx 
+          [(dform nm:id flds:idlist ([[#:key key-expr:expr]] #:opt 
+				     [[#:intern intern?:expr]] #:opt
+				     [[#:frees . frees:frees-pat]] #:opt
+				     [[#:fold-rhs fold-rhs:fold-pat]] #:opt
+				     [no-provide?:no-provide-kw] #:opt) ...*)
+	   (with-syntax* 
+	     ([ex (mk-id #'nm #'nm ":")]
+	      [kw-stx (string->keyword (symbol->string #'nm.datum))]
+	      [parent par]
+	      [(s:ty maker pred acc ...) (build-struct-names #'nm (syntax->list #'flds) #f #t #'nm)]
+	      [*maker (mk-id #'nm "*" #'nm)]
+	      [**maker (mk-id #'nm "**" #'nm)]
+	      [ht-stx ht-stx]
+	      [bfs-fold-rhs (cond [#'fold-rhs #`(lambda (tr er) #,#'fold-rhs.e)]
+				  [else #'(lambda (type-rec-id effect-rec-id) 
+					    #`(*maker (#,type-rec-id flds.i) ...))])]
+	      [provides (if #'no-provide?
+			    #'(begin)                                 
+			    #`(begin 
+				(provide ex pred acc ...)
+				(provide (rename-out [*maker maker]))))]
+	      [intern 
+	       (let ([mk (lambda (int) #`(defintern (**maker . flds) maker #,int #:extra-arg key-expr))])
+		 (syntax-parse #'flds
+		   [_ #:when #'intern?
+		    (mk #'intern?)]
+		   [() (mk #'#f)]
+		   [(f) (mk #'f)]
+		   [_ (mk #'(list . flds))]))]
+	      [frees 
+	       (with-syntax ([(f1 f2) (if #'frees
+					  #'(frees.f1 frees.f2)
+					  (list (combiner #'free-vars* #'flds)
+						(combiner #'free-idxs* #'flds)))])
+			    (quasisyntax/loc stx
+					     (define (*maker . flds)
+					       (define v (**maker . flds))
+					       (unless-in-table 
+						var-table v
+						(define fvs f1)
+						(define fis f2)
+						(hash-set! var-table v fvs)
+						(hash-set! index-table v fis))
+					       v)))])
+	     #`(begin
+		 (define-struct (nm parent) flds #:inspector #f)
+		 (define-match-expander ex
+		   (lambda (s)
+		     (syntax-parse s 
+		       [(_ . fs) 
+			#:with pat (syntax/loc s (_ _ . fs))
+			(syntax/loc s (struct nm pat))])))
+		 (begin-for-syntax
+		  (hash-set! ht-stx 'kw-stx (list #'ex #'flds bfs-fold-rhs #'#,stx)))
+		 intern
+		 provides
+		 frees))])))
+  (values (mk #'Type #'type-name-ht) (mk #'Effect #'effect-name-ht))))
 
diff --git a/collects/typed-scheme/rep/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss
index b5b54bf5ea..ea2d2017bb 100644
--- a/collects/typed-scheme/rep/type-rep.ss
+++ b/collects/typed-scheme/rep/type-rep.ss
@@ -13,7 +13,7 @@
 ;; Type is defined in rep-utils.ss
 
 ;; t must be a Type
-(dt Scope (t))
+(dt Scope (t) [#:key (Type-key t)])
 
 ;; this is ONLY used when a type error ocurrs
 (dt Error () [#:frees #f] [#:fold-rhs #:base])
@@ -41,39 +41,52 @@
                       stx)])
 
 ;; left and right are Types
-(dt Pair (left right))
+(dt Pair (left right) [#:key 'pair])
 
 ;; elem is a Type
-(dt Vector (elem) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))])
+(dt Vector (elem) 
+    [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))]
+    [#:key 'vector])
 
 ;; elem is a Type
-(dt Box (elem) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))])  
+(dt Box (elem) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))]
+    [#:key 'box])  
 
 ;; name is a Symbol (not a Name)
-(dt Base (name contract) [#:frees #f] [#:fold-rhs #:base] [#:intern name])
+(dt Base (name contract) [#:frees #f] [#:fold-rhs #:base] [#:intern name]
+    [#:key (case name
+	     [(Number Integer) 'number]
+	     [(Boolean) 'boolean]
+	     [(String) 'string]
+	     [(Symbol) 'symbol]
+             [(Keyword) 'keyword]
+	     [else #f])])
 
 ;; body is a Scope
 (dt Mu (body) #:no-provide [#:frees (free-vars* body) (without-below 1 (free-idxs* body))]
-    [#:fold-rhs (*Mu (*Scope (type-rec-id (Scope-t body))))])    
+    [#:fold-rhs (*Mu (*Scope (type-rec-id (Scope-t body))))]
+    [#:key (Type-key body)])    
 
 ;; n is how many variables are bound here
 ;; body is a Scope
 (dt Poly (n body) #:no-provide 
     [#:frees (free-vars* body) (without-below n (free-idxs* body))]
     [#:fold-rhs (let ([body* (remove-scopes n body)])
-                  (*Poly n (add-scopes n (type-rec-id body*))))])
+                  (*Poly n (add-scopes n (type-rec-id body*))))]
+    [#:key (Type-key body)])
 
 ;; n is how many variables are bound here
 ;; there are n-1 'normal' vars and 1 ... var
 ;; body is a Scope
 (dt PolyDots (n body) #:no-provide
+    [#:key (Type-key body)]
     [#:frees (free-vars* body) (without-below n (free-idxs* body))]
     [#:fold-rhs (let ([body* (remove-scopes n body)])
                   (*PolyDots n (add-scopes n (type-rec-id body*))))])
 
 ;; pred : identifier
 ;; cert : syntax certifier
-(dt Opaque (pred cert) [#:intern (hash-id pred)] [#:frees #f] [#:fold-rhs #:base])
+(dt Opaque (pred cert) [#:intern (hash-id pred)] [#:frees #f] [#:fold-rhs #:base] [#:key pred])
 
 ;; name : symbol
 ;; parent : Struct
@@ -92,7 +105,8 @@
                          (and proc (type-rec-id proc))
                          poly?
                          pred-id
-                         cert)])
+                         cert)]
+    [#:key (gensym)])
 
 ;; kw : keyword?
 ;; ty : Type
@@ -100,7 +114,8 @@
 (dt Keyword (kw ty required?)
     [#:frees (free-vars* ty)
              (free-idxs* ty)]
-    [#:fold-rhs (*Keyword kw (type-rec-id ty) required?)])
+    [#:fold-rhs (*Keyword kw (type-rec-id ty) required?)]
+    [#:key 'keyword])
 
 ;; dom : Listof[Type]
 ;; rng : Type
@@ -112,6 +127,7 @@
 ;; els-eff : Effect
 ;; arr is NOT a Type
 (dt arr (dom rng rest drest kws thn-eff els-eff)
+    [#:key 'procedure]
     [#:frees (combine-frees (append (map flip-variances (map free-vars* (append (if rest (list rest) null)
                                                                                 (map Keyword-ty kws)
                                                                                 dom)))
@@ -153,13 +169,22 @@
     [#:fold-rhs (*Function (map type-rec-id arities))])
 
 ;; v : Scheme Value
-(dt Value (v) [#:frees #f] [#:fold-rhs #:base])
+(dt Value (v) [#:frees #f] [#:fold-rhs #:base] [#:key (cond [(number? v) 'number]
+							    [(boolean? v) 'boolean]
+							    [(null? v) 'null]
+							    [else #f])])
 
 ;; elems : Listof[Type]
 (dt Union (elems) [#:frees (combine-frees (map free-vars* elems))
                            (combine-frees (map free-idxs* elems))]
-    [#:fold-rhs ((unbox union-maker) (map type-rec-id elems))])
-
+    [#:fold-rhs ((get-union-maker) (map type-rec-id elems))]
+    [#:key (let loop ([res null] [ts elems])
+	     (if (null? ts) res
+		 (let ([k (Type-key (car ts))])
+		   (cond [(pair? k) (loop (append k res) (cdr ts))]
+			 [k (loop (cons k res) (cdr ts))]
+			 [else #f]))))])
+    
 (dt Univ () [#:frees #f] [#:fold-rhs #:base])
 
 ;; types : Listof[Type]
@@ -167,23 +192,25 @@
     #:no-provide
     [#:frees (combine-frees (map free-vars* types))
              (combine-frees (map free-idxs* types))]
-    [#:fold-rhs (*Values (map type-rec-id types))])
+    [#:fold-rhs (*Values (map type-rec-id types))]
+    [#:key 'values])
 
 (dt ValuesDots (types dty dbound) 
     [#:frees (combine-frees (map free-vars* (cons dty types)))
              (combine-frees (map free-idxs* (cons dty types)))]
-    [#:fold-rhs (*ValuesDots (map type-rec-id types) (type-rec-id dty) dbound)])
+    [#:fold-rhs (*ValuesDots (map type-rec-id types) (type-rec-id dty) dbound)]
+    [#:key 'values])
 
 ;; in : Type
 ;; out : Type
-(dt Param (in out))
+(dt Param (in out) [#:key 'parameter])
 
 ;; key : Type
 ;; value : Type
-(dt Hashtable (key value))
+(dt Hashtable (key value) [#:key 'hash])
 
 ;; t : Type
-(dt Syntax (t))
+(dt Syntax (t) [#:key 'syntax])
 
 ;; pos-flds  : (Listof Type)
 ;; name-flds : (Listof (Tuple Symbol Type Boolean))
@@ -197,7 +224,7 @@
               (map free-idxs* (append pos-flds 
                                       (map cadr name-flds)
                                       (map cadr methods))))]
-    
+    [#:key 'class]
     [#:fold-rhs (match (list pos-flds name-flds methods)
                   [(list
                     pos-tys 
@@ -211,17 +238,18 @@
                     (map list mname (map type-rec-id mty)))])])
 
 ;; cls : Class
-(dt Instance (cls))
+(dt Instance (cls) [#:key 'instance])
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 ;; Ugly hack - should use units
 
-(define union-maker (box #f))
+(define union-maker (box (lambda args (int-err "Union not yet available"))))
 
 (define (set-union-maker! v) (set-box! union-maker v))
+(define (get-union-maker) (unbox union-maker))
 
-(provide set-union-maker!)
+(provide set-union-maker! get-union-maker)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
diff --git a/collects/typed-scheme/typecheck/tc-app-unit.ss b/collects/typed-scheme/typecheck/tc-app-unit.ss
index 3c75308f3d..ee815cbc61 100644
--- a/collects/typed-scheme/typecheck/tc-app-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-app-unit.ss
@@ -548,7 +548,8 @@
       #:literals (#%plain-app reverse)
       [c:lv-clause
        #:with (#%plain-app reverse n:id) #'c.e
-       #:when (free-identifier=? name #'n)
+       #:with (v) #'(c.v ...) 
+       #:when (free-identifier=? name #'v)
        (type-annotation #'v)]
       [_ #f]))
   (syntax-parse stx
diff --git a/collects/typed-scheme/utils/utils.ss b/collects/typed-scheme/utils/utils.ss
index f08a44ff90..485bc20b7f 100644
--- a/collects/typed-scheme/utils/utils.ss
+++ b/collects/typed-scheme/utils/utils.ss
@@ -171,11 +171,22 @@
 (define print-type* (box (lambda _ (error "print-type* not yet defined"))))
 (define print-effect* (box (lambda _ (error "print-effect* not yet defined"))))
 
+(require scheme/pretty mzlib/pconvert)
+
 (define-syntax (define-struct/printer stx)
   (syntax-case stx ()
     [(form name (flds ...) printer)
      #`(define-struct/properties name (flds ...) 
-         #,(if printing? #'([prop:custom-write printer]) #'())
+         #,(if printing?
+               #'([prop:custom-write printer]) 
+               #'([prop:custom-write (lambda (s port mode)
+                                       (parameterize ([current-output-port port]
+                                                      [show-sharing #f]
+                                                      [booleans-as-true/false #f]
+                                                      [constructor-style-printing #t])
+                                         (newline)
+                                         (pretty-print (print-convert s))
+                                         (newline)))]))
          #f)]))
 
 (define (id kw . args)