diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 4034d2ed..e6ce1de7 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,9 @@
 
 [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 a454714c..a3283d07 100644
--- a/collects/typed-scheme/private/parse-type.ss
+++ b/collects/typed-scheme/private/parse-type.ss
@@ -77,6 +77,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 +119,43 @@
            #: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-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  
+  #: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 +178,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 +188,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 d2be5958..ca2b264c 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 6526a428..28ec18a4 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 d0d6629b..4832711c 100644
--- a/collects/typed-scheme/private/subtype.ss
+++ b/collects/typed-scheme/private/subtype.ss
@@ -6,9 +6,10 @@
 	 "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)
 
 
@@ -302,3 +303,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 00000000..3a33b0f3
--- /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-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss
index 69c91f51..e8a8849f 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 f813a19e..567cdd56 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 make-Union)]
     [_ (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 d2235d65..e8830edc 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 (list (car types)) (remove-subtypes (cdr types))))]))]))
 
 #;(defintern (Un-intern args) (lambda (_ args) (apply Un args)) args)
 
diff --git a/collects/typed-scheme/rep/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss
index b5b54bf5..bd286cf8 100644
--- a/collects/typed-scheme/rep/type-rep.ss
+++ b/collects/typed-scheme/rep/type-rep.ss
@@ -158,7 +158,7 @@
 ;; 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))])
 
 (dt Univ () [#:frees #f] [#:fold-rhs #:base])
 
@@ -217,11 +217,12 @@
 
 ;; 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 3c75308f..36de510b 100644
--- a/collects/typed-scheme/typecheck/tc-app-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-app-unit.ss
@@ -544,13 +544,17 @@
 (define (find-annotation stx name)
   (define (find s) (find-annotation s name))
   (define (match? b)
+    (printf "match? 1 : ~a~n" (syntax->datum b))
     (syntax-parse b
       #:literals (#%plain-app reverse)
       [c:lv-clause
+       #:when (printf "match? 2 : ~a~n" (syntax->datum #'c.e))
        #: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]))
+  (printf "in find-ann~n")
   (syntax-parse stx
     #:literals (let-values)
     [(let-values cls:lv-clauses body)
@@ -760,7 +764,8 @@
     [((val acc ...)
       ((if (#%plain-app null? val*) thn els))
       (actual actuals ...))
-     (and (free-identifier=? #'val #'val*)
+     (and (printf "in match special case~n")
+          (free-identifier=? #'val #'val*)
           (ormap (lambda (a) (find-annotation #'(if (#%plain-app null? val*) thn els) a))
                  (syntax->list #'(acc ...))))
      (let* ([ts1 (generalize (tc-expr/t #'actual))]