diff --git a/collects/typed-racket/base-env/base-env-indexing-abs.rkt b/collects/typed-racket/base-env/base-env-indexing-abs.rkt
index cf30bbe8..e9bf0878 100644
--- a/collects/typed-racket/base-env/base-env-indexing-abs.rkt
+++ b/collects/typed-racket/base-env/base-env-indexing-abs.rkt
@@ -4,7 +4,7 @@
  "../utils/utils.rkt"
  (for-template racket/base racket/list racket/unsafe/ops racket/flonum)
  (utils tc-utils) 
- (rename-in (types union convenience abbrev numeric-tower) [-Number N] [-Boolean B] [-Symbol Sym]))
+ (rename-in (types union convenience) [-Number N] [-Boolean B] [-Symbol Sym]))
 
 (provide indexing)
 
diff --git a/collects/typed-racket/base-env/base-env-indexing.rkt b/collects/typed-racket/base-env/base-env-indexing.rkt
index 87721351..cfb9a658 100644
--- a/collects/typed-racket/base-env/base-env-indexing.rkt
+++ b/collects/typed-racket/base-env/base-env-indexing.rkt
@@ -2,7 +2,7 @@
 
 (require
  (rename-in "../utils/utils.rkt" [infer r:infer])
- (types abbrev numeric-tower) (env init-envs) (r:infer infer-dummy infer)
+ (types convenience) (env init-envs) (r:infer infer-dummy infer)
  "base-env-indexing-abs.rkt")
 
 (define e (parameterize ([infer-param infer]) (indexing -Integer)))
diff --git a/collects/typed-racket/base-env/base-env-numeric.rkt b/collects/typed-racket/base-env/base-env-numeric.rkt
index b7856987..55b45852 100644
--- a/collects/typed-racket/base-env/base-env-numeric.rkt
+++ b/collects/typed-racket/base-env/base-env-numeric.rkt
@@ -5,7 +5,7 @@
    racket/list racket/math racket/flonum racket/unsafe/ops
    (for-template racket/flonum racket/fixnum racket/math racket/unsafe/ops racket/base
                  (only-in "../types/numeric-predicates.rkt" index?))
-   (only-in (types abbrev numeric-tower) [-Number N] [-Boolean B] [-Symbol Sym] [-Real R] [-PosInt -Pos]))
+   (only-in (types convenience) [-Number N] [-Boolean B] [-Symbol Sym] [-Real R] [-PosInt -Pos]))
 
   ;; TODO having definitions only at the top is really inconvenient.
 
diff --git a/collects/typed-racket/base-env/base-env.rkt b/collects/typed-racket/base-env/base-env.rkt
index fa54da50..fc987f35 100644
--- a/collects/typed-racket/base-env/base-env.rkt
+++ b/collects/typed-racket/base-env/base-env.rkt
@@ -25,7 +25,7 @@
   (only-in racket/match/runtime match:error matchable? match-equality-test))
  racket/file
  (only-in racket/private/pre-base new-apply-proc)
- (only-in (types abbrev numeric-tower) [-Number N] [-Boolean B] [-Symbol Sym])
+ (only-in (types convenience) [-Number N] [-Boolean B] [-Symbol Sym])
  (only-in (rep type-rep)
           make-MPairTop
           make-BoxTop make-ChannelTop make-VectorTop
diff --git a/collects/typed-racket/base-env/base-types.rkt b/collects/typed-racket/base-env/base-types.rkt
index bfc4d6e8..fec210c6 100644
--- a/collects/typed-racket/base-env/base-types.rkt
+++ b/collects/typed-racket/base-env/base-types.rkt
@@ -6,8 +6,7 @@
 ;; I don't understand this at all. :(
 ;; -- STH, 6/26/12
 (require (for-syntax "../env/global-env.rkt"))
-(require "../types/abbrev.rkt" "../types/convenience.rkt" "../types/numeric-tower.rkt"
-         "../rep/type-rep.rkt")
+(require "../types/convenience.rkt" "../rep/type-rep.rkt")
 
 [Complex -Number]
 [Number -Number]
diff --git a/collects/typed-racket/env/init-envs.rkt b/collects/typed-racket/env/init-envs.rkt
index 8882df5b..9c1125ee 100644
--- a/collects/typed-racket/env/init-envs.rkt
+++ b/collects/typed-racket/env/init-envs.rkt
@@ -3,15 +3,15 @@
 (require "../utils/utils.rkt"
          "../utils/tc-utils.rkt"
          "global-env.rkt"
-	 "type-name-env.rkt"
-	 "type-alias-env.rkt"
+         "type-name-env.rkt"
+         "type-alias-env.rkt"
          (rep type-rep object-rep filter-rep rep-utils)
-	 (for-template (rep type-rep object-rep filter-rep)
-		       (types union numeric-tower)
-		       racket/shared racket/base)
-	 (types union convenience)
+         (for-template (rep type-rep object-rep filter-rep)
+                       (types union convenience)
+                       racket/shared racket/base)
+         (types union convenience)
          racket/syntax
-	 mzlib/pconvert racket/match)
+         mzlib/pconvert racket/match)
 
 (define (initialize-type-name-env initial-type-names)
   (for-each (lambda (nm/ty) (register-resolved-type-alias (car nm/ty) (cadr nm/ty))) initial-type-names))
diff --git a/collects/typed-racket/infer/restrict.rkt b/collects/typed-racket/infer/restrict.rkt
index 27ec40ea..25c005c8 100644
--- a/collects/typed-racket/infer/restrict.rkt
+++ b/collects/typed-racket/infer/restrict.rkt
@@ -2,7 +2,7 @@
 
 (require "../utils/utils.rkt")
 (require (rep type-rep)
-	 (types utils union subtype remove-intersect resolve substitute abbrev)
+         (types utils union subtype remove-intersect resolve substitute)
          "signatures.rkt"
          racket/match)
 
@@ -19,7 +19,7 @@
 ;; NEW IMPL
 ;; restrict t1 to be a subtype of t2
 ;; if `f' is 'new, use t2 when giving up, otherwise use t1
-(define (restrict* t1 t2 [f 'new])  
+(define (restrict* t1 t2 [f 'new])
   (cond
     [(subtype t1 t2) t1] ;; already a subtype
     [(match t2 
@@ -34,5 +34,5 @@
     [(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 (if (eq? f 'new) t2 t1)])) ;; t2 and t1 have a complex relationship, so we punt
-    
+
 (define restrict restrict*)
diff --git a/collects/typed-racket/optimizer/list.rkt b/collects/typed-racket/optimizer/list.rkt
index e6965a58..04cbe827 100644
--- a/collects/typed-racket/optimizer/list.rkt
+++ b/collects/typed-racket/optimizer/list.rkt
@@ -4,7 +4,7 @@
          "../utils/utils.rkt"
          (utils tc-utils)
          (rep type-rep)
-         (types abbrev utils type-table)
+         (types convenience utils type-table)
          (optimizer utils logging)
          (for-template racket/base racket/unsafe/ops))
 
diff --git a/collects/typed-racket/optimizer/sequence.rkt b/collects/typed-racket/optimizer/sequence.rkt
index 08241833..841990a4 100644
--- a/collects/typed-racket/optimizer/sequence.rkt
+++ b/collects/typed-racket/optimizer/sequence.rkt
@@ -5,7 +5,7 @@
          (for-template racket/base racket/unsafe/ops)
          "../utils/utils.rkt" "../utils/tc-utils.rkt"
          (rep type-rep)
-         (types abbrev type-table utils)
+         (types convenience type-table utils)
          (optimizer utils logging string
                     float)) ; for int-expr
 
diff --git a/collects/typed-racket/optimizer/string.rkt b/collects/typed-racket/optimizer/string.rkt
index 04f2d259..0a6d3de2 100644
--- a/collects/typed-racket/optimizer/string.rkt
+++ b/collects/typed-racket/optimizer/string.rkt
@@ -4,7 +4,7 @@
          (for-template racket/base racket/unsafe/ops)
          "../utils/utils.rkt"
          (utils tc-utils)
-         (types abbrev)
+         (types convenience)
          (optimizer utils logging))
 
 (provide string-opt-expr string-expr bytes-expr)
diff --git a/collects/typed-racket/private/type-contract.rkt b/collects/typed-racket/private/type-contract.rkt
index 82ae6130..3e2463a2 100644
--- a/collects/typed-racket/private/type-contract.rkt
+++ b/collects/typed-racket/private/type-contract.rkt
@@ -10,7 +10,7 @@
  (utils tc-utils require-contract)
  (env type-name-env)
  (types resolve utils)
- (prefix-in t: (types convenience abbrev))
+ (prefix-in t: (types convenience))
  (private parse-type)
  racket/match unstable/match syntax/struct syntax/stx racket/syntax racket/list
  (only-in racket/contract -> ->* case-> cons/c flat-rec-contract provide/contract any/c)
diff --git a/collects/typed-racket/private/with-types.rkt b/collects/typed-racket/private/with-types.rkt
index 64b05235..4621ddf8 100644
--- a/collects/typed-racket/private/with-types.rkt
+++ b/collects/typed-racket/private/with-types.rkt
@@ -21,8 +21,7 @@
                              "infer/infer.rkt"
                              "utils/tc-utils.rkt"
                              "types/utils.rkt"
-                             "types/convenience.rkt"
-                             "types/abbrev.rkt")
+                             "types/convenience.rkt")
                     ->)
          (except-in (path-up "utils/utils.rkt") infer))
 
diff --git a/collects/typed-racket/typecheck/tc-app-helper.rkt b/collects/typed-racket/typecheck/tc-app-helper.rkt
index e7045f5a..bc4f0227 100644
--- a/collects/typed-racket/typecheck/tc-app-helper.rkt
+++ b/collects/typed-racket/typecheck/tc-app-helper.rkt
@@ -6,7 +6,7 @@
          "check-below.rkt" "tc-subst.rkt"
          (utils tc-utils)
          (rep type-rep object-rep)
-         (types utils union abbrev subtype))
+         (types utils union convenience subtype))
 
 (provide (all-defined-out))
 
diff --git a/collects/typed-racket/typecheck/tc-app.rkt b/collects/typed-racket/typecheck/tc-app.rkt
index 998dd345..79b5e9aa 100644
--- a/collects/typed-racket/typecheck/tc-app.rkt
+++ b/collects/typed-racket/typecheck/tc-app.rkt
@@ -15,10 +15,9 @@
          ;; end fixme
          (for-syntax syntax/parse racket/base (utils tc-utils))
          (private type-annotation)
-         (types utils abbrev union subtype resolve convenience 
+         (types utils union subtype resolve convenience
                 type-table substitute generalize)
          (utils tc-utils)
-         (only-in srfi/1 alist-delete)
          (except-in (env type-env-structs tvar-env index-env) extend)
          (rep type-rep filter-rep object-rep rep-utils)
          (r:infer infer)
diff --git a/collects/typed-racket/typecheck/tc-apply.rkt b/collects/typed-racket/typecheck/tc-apply.rkt
index a7dc3b20..8966a556 100644
--- a/collects/typed-racket/typecheck/tc-apply.rkt
+++ b/collects/typed-racket/typecheck/tc-apply.rkt
@@ -5,7 +5,7 @@
          racket/match racket/list
          (for-syntax (utils tc-utils))
          (private type-annotation)
-         (types utils abbrev union subtype resolve convenience type-table substitute)
+         (types utils union subtype resolve convenience type-table substitute)
          (utils tc-utils)
          (only-in srfi/1 alist-delete)
          (except-in (env type-env-structs tvar-env index-env) extend)
diff --git a/collects/typed-racket/typecheck/tc-funapp.rkt b/collects/typed-racket/typecheck/tc-funapp.rkt
index 2386b01f..ed306a43 100644
--- a/collects/typed-racket/typecheck/tc-funapp.rkt
+++ b/collects/typed-racket/typecheck/tc-funapp.rkt
@@ -13,7 +13,7 @@
          ;; end fixme
          (for-syntax syntax/parse racket/base (utils tc-utils))
          (private type-annotation)
-         (types utils abbrev union subtype resolve convenience type-table
+         (types utils union subtype resolve convenience type-table
                 substitute)
          (utils tc-utils)
          (except-in (env type-env-structs tvar-env index-env) extend)
diff --git a/collects/typed-racket/typecheck/tc-if.rkt b/collects/typed-racket/typecheck/tc-if.rkt
index a94019ae..cb107ed5 100644
--- a/collects/typed-racket/typecheck/tc-if.rkt
+++ b/collects/typed-racket/typecheck/tc-if.rkt
@@ -2,11 +2,10 @@
 (require (rename-in "../utils/utils.rkt" [infer r:infer])
          "signatures.rkt" "check-below.rkt"
          (rep type-rep filter-rep object-rep)
-         (rename-in (types convenience subtype union utils remove-intersect abbrev filter-ops)
-                    [remove *remove])
+         (types convenience subtype union utils filter-ops)
          (env lexical-env type-env-structs)
          (r:infer infer)
-	 (utils tc-utils)
+         (utils tc-utils)
          "tc-envops.rkt" "tc-metafunctions.rkt"
          (types type-table)
          syntax/kerncase
diff --git a/collects/typed-racket/typecheck/tc-lambda-unit.rkt b/collects/typed-racket/typecheck/tc-lambda-unit.rkt
index ef3b69e2..2199780e 100644
--- a/collects/typed-racket/typecheck/tc-lambda-unit.rkt
+++ b/collects/typed-racket/typecheck/tc-lambda-unit.rkt
@@ -12,9 +12,8 @@
          (rename-in (types convenience utils union)
                     [make-arr* make-arr])
          (private type-annotation)
-         (types abbrev utils)
-	 (env type-env-structs lexical-env tvar-env index-env)
-	 (utils tc-utils)
+         (env type-env-structs lexical-env tvar-env index-env)
+         (utils tc-utils)
 
          racket/match)
 (require (for-template racket/base "internal-forms.rkt"))
diff --git a/collects/typed-racket/typecheck/tc-structs.rkt b/collects/typed-racket/typecheck/tc-structs.rkt
index be1ac69a..dcb599ce 100644
--- a/collects/typed-racket/typecheck/tc-structs.rkt
+++ b/collects/typed-racket/typecheck/tc-structs.rkt
@@ -1,14 +1,14 @@
 #lang racket/base
 
 (require "../utils/utils.rkt"
-	 (except-in (rep type-rep free-variance) Dotted)
+         (except-in (rep type-rep free-variance) Dotted)
          (private parse-type)
-	 (types convenience utils union resolve abbrev substitute type-table)
-	 (env global-env type-env-structs type-name-env tvar-env)
-	 (utils tc-utils)
+         (types convenience utils union resolve substitute type-table)
+         (env global-env type-env-structs type-name-env tvar-env)
+         (utils tc-utils)
          "def-binding.rkt"
          syntax/kerncase
-         syntax/struct         
+         syntax/struct
          racket/function
          racket/match
          (only-in racket/contract
diff --git a/collects/typed-racket/types/abbrev.rkt b/collects/typed-racket/types/abbrev.rkt
index f305052d..64c15eaa 100644
--- a/collects/typed-racket/types/abbrev.rkt
+++ b/collects/typed-racket/types/abbrev.rkt
@@ -55,6 +55,7 @@
     [(Values: (list (Result: t _ _))) (list t)]
     [_ (list t)]))
 
+;; TODO make this file depend on union.rkt, and use the real Union constructor.
 ;; Simple union constructor.
 ;; Flattens nested unions and sorts types, but does not check for
 ;; overlapping subtypes.
diff --git a/collects/typed-racket/types/filter-ops.rkt b/collects/typed-racket/types/filter-ops.rkt
index 0c11b2a4..249339f3 100644
--- a/collects/typed-racket/types/filter-ops.rkt
+++ b/collects/typed-racket/types/filter-ops.rkt
@@ -3,8 +3,8 @@
 (require "../utils/utils.rkt"
          (rep type-rep filter-rep object-rep rep-utils)
          (utils tc-utils) (only-in (infer infer) restrict)
-         "abbrev.rkt" (only-in racket/contract current-blame-format [-> -->] listof)
-	 (types printer union subtype utils remove-intersect)
+         (only-in racket/contract [-> -->] listof)
+         (types union subtype utils remove-intersect convenience)
          racket/list racket/match
          (for-syntax syntax/parse racket/base)
          syntax/id-table racket/dict
diff --git a/collects/typed-racket/types/generalize.rkt b/collects/typed-racket/types/generalize.rkt
index 39bf8ad9..c03ba9f0 100644
--- a/collects/typed-racket/types/generalize.rkt
+++ b/collects/typed-racket/types/generalize.rkt
@@ -3,8 +3,7 @@
 (require "../utils/utils.rkt"
          (rep type-rep filter-rep object-rep rep-utils)
          (utils tc-utils)
-         (only-in racket/contract current-blame-format)
-         "abbrev.rkt" "numeric-tower.rkt" "subtype.rkt" "substitute.rkt" "union.rkt"
+         "convenience.rkt" "subtype.rkt" "substitute.rkt" "union.rkt"
          racket/match
          (for-syntax syntax/parse racket/base)
          syntax/id-table racket/dict)
@@ -18,7 +17,7 @@
     (let loop ([t* t])
       (match t*
         [(Value: '()) (-lst Univ)]
-	[(Value: 0) -Int]
+        [(Value: 0) -Int]
         [(List: ts) (-lst (apply Un ts))]
         [(? (lambda (t) (subtype t -Int))) -Int]
         [(? (lambda (t) (subtype t -Rat))) -Rat]
@@ -45,4 +44,4 @@
         [(ListDots: t bound) (-lst (substitute Univ bound t))]
         [(? (lambda (t) (subtype t -Symbol))) -Symbol]
         [(Value: #t) -Boolean]
-        [_ (exit t)]))))
\ No newline at end of file
+        [_ (exit t)]))))
diff --git a/collects/typed-racket/types/kw-types.rkt b/collects/typed-racket/types/kw-types.rkt
index 243bccb5..fe4140af 100644
--- a/collects/typed-racket/types/kw-types.rkt
+++ b/collects/typed-racket/types/kw-types.rkt
@@ -1,8 +1,8 @@
 #lang racket/base
 
 (require "convenience.rkt" "../rep/type-rep.rkt"
-         "union.rkt" "abbrev.rkt" "../utils/tc-utils.rkt"
-         racket/list racket/dict racket/set racket/match)
+         "union.rkt" "../utils/tc-utils.rkt"
+         racket/list racket/dict racket/match)
 
 ;; convert : [Listof Keyword] [Listof Type] [Listof Type] [Option Type] [Option Type] -> (values Type Type)
 (define (convert kw-t plain-t opt-t rng rest drest split?)
diff --git a/collects/typed-racket/types/printer.rkt b/collects/typed-racket/types/printer.rkt
index 98bba0ce..3243878f 100644
--- a/collects/typed-racket/types/printer.rkt
+++ b/collects/typed-racket/types/printer.rkt
@@ -3,8 +3,8 @@
 (require racket/require racket/match unstable/sequence racket/string racket/promise
          (prefix-in s: srfi/1)
          (path-up "rep/type-rep.rkt" "rep/filter-rep.rkt" "rep/object-rep.rkt"
-                  "rep/rep-utils.rkt" "types/abbrev.rkt" "types/subtype.rkt"
-                  "types/numeric-tower.rkt" "utils/utils.rkt"
+                  "rep/rep-utils.rkt" "types/convenience.rkt" "types/subtype.rkt"
+                  "utils/utils.rkt"
                   "utils/tc-utils.rkt"))
 
 ;; do we attempt to find instantiations of polymorphic types to print?
diff --git a/collects/typed-racket/types/subtype.rkt b/collects/typed-racket/types/subtype.rkt
index d78771f0..361c08ed 100644
--- a/collects/typed-racket/types/subtype.rkt
+++ b/collects/typed-racket/types/subtype.rkt
@@ -7,8 +7,7 @@
          (only-in (infer infer-dummy) unify)
          racket/match unstable/match
          racket/function
-         (rename-in racket/contract
-                    [-> c->] [->* c->*])
+         (prefix-in c: racket/contract)
          (for-syntax racket/base syntax/parse))
 
 ;; exn representing failure of subtyping
@@ -186,7 +185,7 @@
 ;(trace subtypes*/varargs)
 
 (define/cond-contract (combine-arrs arrs)
-  (c-> (listof arr?) (or/c #f arr?))
+  (c:-> (c:listof arr?) (c:or/c #f arr?))
   (match arrs
     [(list (and a1 (arr: dom1 rng1 #f #f '())) (arr: dom rng #f #f '()) ...)
      (cond
diff --git a/collects/typed-racket/types/union.rkt b/collects/typed-racket/types/union.rkt
index 5035161d..9cc399c6 100644
--- a/collects/typed-racket/types/union.rkt
+++ b/collects/typed-racket/types/union.rkt
@@ -4,7 +4,7 @@
          (rep type-rep rep-utils)
          (utils tc-utils)
          (prefix-in c: (contract-req))
-         (types utils subtype abbrev)
+         (types utils subtype)
          racket/match)
 
 
@@ -25,6 +25,13 @@
           [(ormap (lambda (t) (subtype (car ts*) t)) result) (loop (cdr ts*) result)]
           [else (loop (cdr ts*) (cons (car ts*) result))])))
 
+(define (flat t)
+  (match t
+    [(Union: es) es]
+    [(Values: (list (Result: (Union: es) _ _))) es]
+    [(Values: (list (Result: t _ _))) (list t)]
+    [_ (list t)]))
+
 ;; Union constructor
 ;; Normalizes representation by sorting types.
 (define Un