diff --git a/typed-racket-lib/typed-racket/env/init-envs.rkt b/typed-racket-lib/typed-racket/env/init-envs.rkt
index 70eb1d5e..7a5f4f6e 100644
--- a/typed-racket-lib/typed-racket/env/init-envs.rkt
+++ b/typed-racket-lib/typed-racket/env/init-envs.rkt
@@ -3,7 +3,7 @@
 ;; Support for defining the initial TR environment
 
 (require "../utils/utils.rkt"
-         (utils tc-utils hset)
+         (utils tc-utils)
          "global-env.rkt"
          "type-name-env.rkt"
          "type-alias-env.rkt"
@@ -95,22 +95,13 @@
 
 ;; Helper for type->sexp
 (define (recur ty)
-  (define (numeric? t) (match t [(Base: _ _ _ b) b] [(Value: (? number?)) #t] [_ #f]))
-  (define (split-union ts)
-    (let ([ts (hset->list ts)])
-      (define-values (nums others) (partition numeric? ts))
-      (cond [(or (null? nums) (null? others))
-             ;; nothing interesting to do in this case
-             `(Un ,@(map type->sexp ts))]
-            [else
-             ;; we do a little more work to hopefully save a bunch in serialization space
-             ;; if we get a hit in the predefined-type-table
-             `(Un ,(type->sexp (apply Un nums)) ,(type->sexp (apply Un others)))])))
-
+  (define (numeric? t) (match t
+                         [(Base-bits: num? _) num?]
+                         [(Value: (? number?)) #t]
+                         [_ #f]))
   (match ty
     [(In-Predefined-Table: id) id]
-    [(Base: n cnt pred _)
-     (int-err "Base type ~a not in predefined-type-table" n)]
+    [(? Base?) (int-err "Base type ~a not in predefined-type-table" ty)]
     [(B: nat) `(make-B ,nat)]
     [(F: sym) `(make-F (quote ,sym))]
     [(Pair: ty (Listof: ty))
@@ -214,12 +205,16 @@
                    ,(object->sexp obj))]
     [(AnyValues: prop)
      `(make-AnyValues ,(prop->sexp prop))]
-    [(Union: (app hset->list (list (Value: vs) ...)))
-     `(one-of/c ,@(for/list ([v (in-list vs)])
-                    `(quote ,v)))]
-    [(Union: elems) (split-union elems)]
+    [(Union: (? Bottom?) ts)
+     #:when (andmap Value? ts)
+     `(one-of/c ,@(for/list ([t (in-list ts)])
+                    `(quote ,(Value-val t))))]
+    
+    [(BaseUnion: bbits nbits) `(make-BaseUnion ,bbits ,nbits)]
+    [(Union: base elems) `(Un . ,(append (if (Bottom? base) '() (list (type->sexp base)))
+                                         (map type->sexp elems)))]
     [(Intersection: elems)
-     `(make-Intersection (hset ,@(hset-map elems type->sexp)))]
+     `(make-Intersection (list ,@(map type->sexp elems)))]
     [(Name: stx 0 #t)
      `(-struct-name (quote-syntax ,stx))]
     [(Name: stx args struct?)
diff --git a/typed-racket-lib/typed-racket/env/type-alias-helper.rkt b/typed-racket-lib/typed-racket/env/type-alias-helper.rkt
index 05f23edb..d2c584cd 100644
--- a/typed-racket-lib/typed-racket/env/type-alias-helper.rkt
+++ b/typed-racket-lib/typed-racket/env/type-alias-helper.rkt
@@ -3,7 +3,7 @@
 ;; This module provides helper functions for type aliases
 
 (require "../utils/utils.rkt"
-         (utils tarjan tc-utils hset)
+         (utils tarjan tc-utils)
          (env type-alias-env type-name-env)
          (rep type-rep)
          (private parse-type)
@@ -57,8 +57,8 @@
 ;;
 (define (check-type-alias-contractive id type)
   (define/match (check type)
-    [((Union: elems)) (for/and ([elem (in-hset elems)]) (check elem))]
-    [((Intersection: elems)) (for/and ([elem (in-hset elems)]) (check elem))]
+    [((Union: _ ts)) (andmap check ts)]
+    [((Intersection: elems)) (andmap check elems)]
     [((Name/simple: name-id))
      (and (not (free-identifier=? name-id id))
           (check (resolve-once type)))]
@@ -90,11 +90,7 @@
 ;; Identifier -> Type
 ;; Construct a fresh placeholder type
 (define (make-placeholder-type id)
-  (make-Base ;; the uninterned symbol here ensures that no two type
-             ;; aliases get the same placeholder type
-             (string->uninterned-symbol (symbol->string (syntax-e id)))
-             #'(int-err "Encountered unresolved alias placeholder")
-             (lambda _ #f) #f))
+  (make-Opaque id))
 
 ;; register-all-type-aliases : Listof<Id> Dict<Id, TypeAliasInfo> -> Void
 ;;
diff --git a/typed-racket-lib/typed-racket/infer/constraint-structs.rkt b/typed-racket-lib/typed-racket/infer/constraint-structs.rkt
index 0577ea3f..1e8e1212 100644
--- a/typed-racket-lib/typed-racket/infer/constraint-structs.rkt
+++ b/typed-racket-lib/typed-racket/infer/constraint-structs.rkt
@@ -37,11 +37,14 @@
 ;; don't want to rule them out too early
 (define-struct/cond-contract cset ([maps (listof (cons/c (hash/c symbol? c? #:immutable #t) dmap?))]) #:transparent)
 
+(define no-cset (make-cset '()))
+
 (provide-for-cond-contract dcon/c)
 (provide
-  (struct-out cset)
-  (struct-out dmap)
-  (struct-out dcon)
-  (struct-out dcon-dotted)
-  (struct-out dcon-exact)
-  (struct-out c))
+ no-cset
+ (struct-out cset)
+ (struct-out dmap)
+ (struct-out dcon)
+ (struct-out dcon-dotted)
+ (struct-out dcon-exact)
+ (struct-out c))
diff --git a/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
index a8b1ca31..96bf79fd 100644
--- a/typed-racket-lib/typed-racket/infer/infer-unit.rkt
+++ b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
@@ -10,7 +10,7 @@
 (require "../utils/utils.rkt"
          (except-in
           (combine-in
-           (utils tc-utils hset)
+           (utils tc-utils)
            (rep free-variance type-rep prop-rep object-rep
                 values-rep rep-utils type-mask)
            (types utils abbrev numeric-tower subtype resolve
@@ -397,7 +397,6 @@
 (define (cgen/inv context s t)
   (% cset-meet (cgen context s t) (cgen context t s)))
 
-
 ;; context : the context of what to infer/not infer
 ;; S : a type to be the subtype of T
 ;; T : a type
@@ -527,28 +526,32 @@
         ;; find *an* element of elems which can be made a subtype of T
         [((Intersection: ts) T)
          (cset-join
-          (for*/list ([t (in-hset ts)]
+          (for*/list ([t (in-list ts)]
                       [v (in-value (cg t T))]
                       #:when v)
             v))]
         
         ;; constrain S to be below *each* element of elems, and then combine the constraints
         [(S (Intersection: ts))
-         (define cs (for/list/fail ([ts (in-hset ts)]) (cg S ts)))
+         (define cs (for/list/fail ([ts (in-list ts)]) (cg S ts)))
          (and cs (cset-meet* (cons empty cs)))]
         
         ;; constrain *each* element of es to be below T, and then combine the constraints
-        [((Union: es) T)
-         (define cs (for/list/fail ([e (in-hset es)]) (cg e T)))
+        [((BaseUnion-bases: es) T)
+         (define cs (for/list/fail ([e (in-list es)]) (cg e T)))
+         (and cs (cset-meet* (cons empty cs)))]
+        [((Union-all: es) T)
+         (define cs (for/list/fail ([e (in-list es)]) (cg e T)))
          (and cs (cset-meet* (cons empty cs)))]
 
+        [(_ (Bottom:)) no-cset]
+        
         ;; find *an* element of es which can be made to be a supertype of S
         ;; FIXME: we're using multiple csets here, but I don't think it makes a difference
         ;; not using multiple csets will break for: ???
-        [(S (or (Union: es)
-                (and (Bottom:) (bind es (hset)))))
+        [(S (Union-all: es))
          (cset-join
-          (for*/list ([e (in-hset es)]
+          (for*/list ([e (in-list es)]
                       [v (in-value (cg S e))]
                       #:when v)
             v))]
@@ -617,11 +620,11 @@
                                       (cg t t*)))]
         [((Vector: t) (Sequence: (list t*)))
          (cg t t*)]
-        [((Base: 'String _ _ _) (Sequence: (list t*)))
+        [((? Base:String?) (Sequence: (list t*)))
          (cg -Char t*)]
-        [((Base: 'Bytes _ _ _) (Sequence: (list t*)))
+        [((? Base:Bytes?) (Sequence: (list t*)))
          (cg -Nat t*)]
-        [((Base: 'Input-Port _ _ _) (Sequence: (list t*)))
+        [((? Base:Input-Port?) (Sequence: (list t*)))
          (cg -Nat t*)]
         [((Value: (? exact-nonnegative-integer? n)) (Sequence: (list t*)))
          (define possibilities
@@ -636,7 +639,8 @@
                [(list pred? type)
                 (and (pred? n) type)])))
          (cg type t*)]
-        [((Base: _ _ _ #t) (Sequence: (list t*)))
+        ;; numeric? == #true
+        [((Base-bits: #t _) (Sequence: (list t*)))
          (define type
            (for/or ([t (in-list (list -Byte -Index -NonNegFixnum -Nat))])
              (and (subtype S t) t)))
@@ -694,28 +698,28 @@
          (cg a a*)]
         [((Evt: a) (Evt: a*))
          (cg a a*)]
-        [((Base: 'Semaphore _ _ _) (Evt: t))
+        [((? Base:Semaphore?) (Evt: t))
          (cg S t)]
-        [((Base: 'Output-Port _ _ _) (Evt: t))
+        [((? Base:Output-Port?) (Evt: t))
          (cg S t)]
-        [((Base: 'Input-Port _ _ _) (Evt: t))
+        [((? Base:Input-Port?) (Evt: t))
          (cg S t)]
-        [((Base: 'TCP-Listener _ _ _) (Evt: t))
+        [((? Base:TCP-Listener?) (Evt: t))
          (cg S t)]
-        [((Base: 'Thread _ _ _) (Evt: t))
+        [((? Base:Thread?) (Evt: t))
          (cg S t)]
-        [((Base: 'Subprocess _ _ _) (Evt: t))
+        [((? Base:Subprocess?) (Evt: t))
          (cg S t)]
-        [((Base: 'Will-Executor _ _ _) (Evt: t))
+        [((? Base:Will-Executor?) (Evt: t))
          (cg S t)]
-        [((Base: 'LogReceiver _ _ _) (Evt: t ))
+        [((? Base:Log-Receiver?) (Evt: t ))
          (cg (make-HeterogeneousVector
               (list -Symbol -String Univ
                     (Un (-val #f) -Symbol)))
              t)]
-        [((Base: 'Place _ _ _) (Evt: t))
+        [((? Base:Place?) (Evt: t))
          (cg Univ t)]
-        [((Base: 'Base-Place-Channel _ _ _) (Evt: t))
+        [((? Base:Base-Place-Channel?) (Evt: t))
          (cg Univ t)]
         [((CustodianBox: t) (Evt: t*)) (cg S t*)]
         [((Channel: t) (Evt: t*)) (cg t t*)]
@@ -864,26 +868,26 @@
 ;; just return a boolean result
 (define infer
  (let ()
-  (define/cond-contract (infer X Y S T R [expected #f] #:multiple? [multiple-substitutions? #f])
-    (((listof symbol?) (listof symbol?) (listof Type?) (listof Type?)
-      (or/c #f Values/c ValuesDots?))
-     ((or/c #f Values/c AnyValues? ValuesDots?)
-      #:multiple? boolean?)
-     . ->* . (or/c boolean?
-                   substitution/c
-                   (cons/c substitution/c
-                           (listof substitution/c))))
-    (define ctx (context null X Y ))
-    (define expected-cset
-      (if expected
-          (cgen ctx R expected)
-          (empty-cset '() '())))
-    (and expected-cset
-         (let* ([cs (cgen/list ctx S T #:expected-cset expected-cset)]
-                [cs* (% cset-meet cs expected-cset)])
-           (and cs* (cond
-                      [R (substs-gen cs* X Y R multiple-substitutions?)]
-                      [else #t])))))
+   (define/cond-contract (infer X Y S T R [expected #f] #:multiple? [multiple-substitutions? #f])
+     (((listof symbol?) (listof symbol?) (listof Type?) (listof Type?)
+       (or/c #f Values/c ValuesDots?))
+      ((or/c #f Values/c AnyValues? ValuesDots?)
+       #:multiple? boolean?)
+      . ->* . (or/c boolean?
+                    substitution/c
+                    (cons/c substitution/c
+                            (listof substitution/c))))
+     (define ctx (context null X Y ))
+     (define expected-cset
+       (if expected
+           (cgen ctx R expected)
+           (empty-cset '() '())))
+     (and expected-cset
+          (let* ([cs (cgen/list ctx S T #:expected-cset expected-cset)]
+                 [cs* (% cset-meet cs expected-cset)])
+            (and cs* (cond
+                       [R (substs-gen cs* X Y R multiple-substitutions?)]
+                       [else #t])))))
   ;(trace infer)
   infer)) ;to export a variable binding and not syntax
 
diff --git a/typed-racket-lib/typed-racket/infer/intersect.rkt b/typed-racket-lib/typed-racket/infer/intersect.rkt
index f3be5875..faa44356 100644
--- a/typed-racket-lib/typed-racket/infer/intersect.rkt
+++ b/typed-racket-lib/typed-racket/infer/intersect.rkt
@@ -1,9 +1,8 @@
 #lang racket/unit
 
 (require "../utils/utils.rkt"
-         (utils hset)
          (rep type-rep type-mask rep-utils)
-         (types abbrev base-abbrev subtype resolve overlap)
+         (types abbrev subtype resolve overlap)
          "signatures.rkt"
          racket/match
          racket/set)
@@ -11,19 +10,15 @@
 (import infer^)
 (export intersect^)
 
-;; compute the intersection of two types
-;; (note: previously called restrict, however now restrict is
-;;  a non-additive intersection computation defined below
-;; (i.e. only parts of t1 will remain, no parts from t2 are added))
-(define (intersect t1 t2)
+
+(define ((intersect-types additive?) t1 t2)
   (cond
     ;; we dispatch w/ Error first, because it behaves in
     ;; strange ways (e.g. it is ⊤ and ⊥ w.r.t subtyping) and
     ;; mucks up what might otherwise be commutative behavior
     [(or (Error? t1) (Error? t2)) Err]
     [else
-     (let intersect
-       ([t1 t2] [t2 t1] [seen '()])
+     (let intersect ([t1 t1] [t2 t2] [seen '()])
        ;; t1   : Type?
        ;; t2   : Type?
        ;; seen : (listof (cons/c (cons/c Type? Type?) symbol?))
@@ -34,7 +29,7 @@
        (define (rec t1 t2) (intersect t1 t2 seen))
        (match* (t1 t2)
          ;; quick overlap check
-         [(_ _) #:when (disjoint-masks? (mask t1) (mask t2)) -Bottom]
+         [(_ _) #:when (not (overlap? t1 t2)) -Bottom]
       
          ;; already a subtype
          [(_ _) #:when (subtype t1 t2) t1]
@@ -61,22 +56,26 @@
          [((Promise: t1*) (Promise: t2*))
           (rebuild -Promise (rec t1* t2*))]
 
-         [((Union: t1s) t2)
+         [((Union: base1 t1s) t2)
           (match t2
             ;; let's be consistent in slamming together unions
             ;; (i.e. if we don't do this dual traversal, the order the
             ;; unions are passed to 'intersect' can produces different
             ;; (albeit equivalent modulo subtyping, we believe) answers)
-            [(Union: t2s) (make-Union (for*/hset ([t1 (in-hset t1s)]
-                                                  [t2 (in-hset t2s)])
-                                                 (rec t1 t2)))]
-            [_ (Union-map t1s (λ (t1) (rec t1 t2)))])]
-         [(t1 (Union: t2s)) (Union-map t2s (λ (t2) (rec t1 t2)))]
+            [(Union-all: t2s)
+             (let ([t1s (if (Bottom? base1) t1s (cons base1 t1s))])
+               (apply Un (for*/list ([t1 (in-list t1s)]
+                                     [t2 (in-list t2s)]
+                                     [t* (in-value (rec t1 t2))]
+                                     #:unless (Bottom? t*))
+                           t*)))]
+            [_ (Union-fmap (λ (t1) (rec t1 t2)) base1 t1s)])]
+         [(t1 (Union: base2 t2s)) (Union-fmap (λ (t2) (rec t1 t2)) base2 t2s)]
 
          [((Intersection: t1s) t2)
-          (apply -unsafe-intersect (hset-map t1s (λ (t1) (rec t1 t2))))]
+          (apply -unsafe-intersect (map (λ (t1) (rec t1 t2)) t1s))]
          [(t1 (Intersection: t2s))
-          (apply -unsafe-intersect (hset-map t2s (λ (t2) (rec t1 t2))))]
+          (apply -unsafe-intersect (map (λ (t2) (rec t1 t2)) t2s))]
 
          ;; For resolvable types, we record the occurrence and save a back pointer
          ;; in 'seen'. Then, if this pair of types emerges again, we know that we are
@@ -115,10 +114,49 @@
                ;; otherwise just return the result
                [else t])])]
 
-         ;; t2 and t1 have a complex relationship, so we build an intersection
-         ;; (note: intersection checks for overlap)
-         [(t1 t2) (-unsafe-intersect t1 t2)]))]))
+         ;; Base Unions
+         [((BaseUnion: bbits1 nbits1)
+           (BaseUnion: bbits2 nbits2))
+          (make-BaseUnion (bbits-intersect bbits1 bbits2)
+                          (nbits-intersect nbits1 nbits2))]
+         [((BaseUnion: bbits nbits)
+           (Base-bits: numeric? bits))
+          (cond [numeric? (if (nbits-overlap? nbits bits)
+                              t2
+                              -Bottom)]
+                [else (if (bbits-overlap? bbits bits)
+                          t2
+                          -Bottom)])]
+         [((Base-bits: numeric? bits)
+           (BaseUnion: bbits nbits))
+          (cond [numeric? (if (nbits-overlap? nbits bits)
+                              t1
+                              -Bottom)]
+                [else (if (bbits-overlap? bbits bits)
+                          t1
+                          -Bottom)])]
+         [((BaseUnion-bases: bases1) t2)
+          (apply Un (for/list ([b (in-list bases1)])
+                      (rec b t2)))]
+         [(t1 (BaseUnion-bases: bases2))
+          (apply Un (for/list ([b (in-list bases2)])
+                      (rec t1 b)))]
 
+         ;; t2 and t1 have a complex relationship, so we build an intersection
+         ;; if additive, otherwise t1 remains unchanged
+         [(t1 t2) (if additive?
+                      (-unsafe-intersect t1 t2)
+                      t1)]))]))
+
+
+;; intersect
+;; Type Type -> Type
+;;
+;; compute the intersection of two types
+;; (note: previously called restrict, however now restrict is
+;;  a non-additive intersection computation defined below
+;; (i.e. only parts of t1 will remain, no parts from t2 are added))
+(define intersect (intersect-types #t))
 
 ;; restrict
 ;; Type Type -> Type
@@ -129,66 +167,4 @@
 ;; will create an intersection type if the intersection is not obvious,
 ;; and sometimes we want to make sure and _not_ add t2 to the result
 ;; we just want to keep the parts of t1 consistent with t2)
-(define (restrict t1 t2)
-  ;; resolved is a set tracking previously seen restrict cases
-  ;; (i.e. pairs of t1 t2) to prevent infinite unfolding.
-  ;; subtyping performs a similar check for the same
-  ;; reason
-  (let restrict
-    ([t1 t1] [t2 t2] [resolved '()])
-    (match* (t1 t2)
-      ;; no overlap
-      [(_ _) #:when (not (overlap? t1 t2)) -Bottom]
-      ;; already a subtype
-      [(t1 t2) #:when (subtype t1 t2) t1]
-      
-      ;; polymorphic restrict
-      [(t1 (Poly: vars t)) #:when (infer vars null (list t1) (list t) #f) t1]
-      
-      ;; structural recursion on types
-      [((Pair: a1 d1) (Pair: a2 d2)) 
-       (rebuild -pair
-                (restrict a1 a2 resolved)
-                (restrict d1 d2 resolved))]
-      ;; FIXME: support structural updating for structs when structs are updated to
-      ;; contain not only *if* they are polymorphic, but *which* fields are too  
-      ;;[((Struct: _ _ _ _ _ _)
-      ;; (Struct: _ _ _ _ _ _))]
-      [((Syntax: t1*) (Syntax: t2*))
-       (rebuild -Syntax (restrict t1* t2* resolved))]
-      [((Promise: t1*) (Promise: t2*))
-       (rebuild -Promise (restrict t1* t2* resolved))]
-      
-      ;; unions
-      [((Union: t1s) t2)
-       (Union-map  t1s (λ (t1) (restrict t1 t2 resolved)))]
-
-      [(t1 (Union: t2s))
-       (Union-map t2s (λ (t2) (restrict t1 t2 resolved)))]
-      
-      ;; restrictions
-      [((Intersection: t1s) t2)
-       (apply -unsafe-intersect (for/list ([t1 (in-list t1s)])
-                                  (restrict t1 t2 resolved)))]
-
-      [(t1 (Intersection: t2s))
-       (apply -unsafe-intersect (for/list ([t2 (in-list t2s)])
-                                  (restrict t1 t2 resolved)))]
-      
-      ;; resolve resolvable types if we haven't already done so
-      [((? resolvable? t1) t2)
-       #:when (not (member (cons t1 t2) resolved))
-       (restrict (resolve t1) t2 (cons (cons t1 t2) resolved))]
-
-      [(t1 (? resolvable? t2))
-       #:when (not (member (cons t1 t2) resolved))
-       (restrict t1 (resolve t2) (cons (cons t1 t2) resolved))]
-      
-      ;; if we're intersecting two recursive types, intersect their body
-      ;; and have their recursive references point back to the result
-      [((? Mu?) (? Mu?))
-       (define name (gensym))
-       (make-Mu name (restrict (Mu-body name t1) (Mu-body name t2) resolved))]
-
-      ;; else it's complicated and t1 remains unchanged
-      [(_ _) t1])))
+(define restrict (intersect-types #f))
diff --git a/typed-racket-lib/typed-racket/optimizer/utils.rkt b/typed-racket-lib/typed-racket/optimizer/utils.rkt
index a5fc8046..2b4162cb 100644
--- a/typed-racket-lib/typed-racket/optimizer/utils.rkt
+++ b/typed-racket-lib/typed-racket/optimizer/utils.rkt
@@ -10,7 +10,7 @@
          (only-in (utils literal-syntax-class)
            [define-literal-syntax-class define-literal-syntax-class*])
          (for-template racket/base)
-         (types type-table utils subtype)
+         (types type-table utils subtype match-expanders)
          (rep type-rep))
 
 (provide *show-optimized-code*
@@ -130,10 +130,11 @@
     #:with opt this-syntax)
   (pattern (~and e :opt-expr)
     #:when (match (type-of #'e)
-             [(tc-result1: (Value: _)) #t]
+             [(tc-result1: (Val-able: _))
+              #t]
              [_ #f])
     #:attr val (match (type-of #'e)
-                 [(tc-result1: (Value: v)) v]
+                 [(tc-result1: (Val-able: v)) v]
                  [_ #f])))
 
 (define-syntax-class kernel-expression
diff --git a/typed-racket-lib/typed-racket/private/parse-type.rkt b/typed-racket-lib/typed-racket/private/parse-type.rkt
index cae03333..98132da1 100644
--- a/typed-racket-lib/typed-racket/private/parse-type.rkt
+++ b/typed-racket-lib/typed-racket/private/parse-type.rkt
@@ -8,7 +8,7 @@
                            classes prefab signatures)
                     [make-arr* make-arr])
          (only-in (infer-in infer) intersect)
-         (utils tc-utils stxclass-util literal-syntax-class hset)
+         (utils tc-utils stxclass-util literal-syntax-class)
          syntax/stx (prefix-in c: (contract-req))
          syntax/parse racket/sequence
          (env tvar-env type-alias-env mvar-env
@@ -453,10 +453,10 @@
                        (let ([t* (parse-type #'t)])
                          ;; is t in a productive position?
                          (define productive
-                           (let loop ((ty t*))
+                           (let loop ([ty t*])
                              (match ty
-                               [(Union: elems) (for/and ([elem (in-hset elems)]) (loop elem))]
-                               [(Intersection: elems) (for/and ([elem (in-hset elems)]) (loop elem))]
+                               [(Union: _ elems) (andmap loop elems)]
+                               [(Intersection: elems) (andmap loop elems)]
                                [(F: _) (not (equal? ty tvar))]
                                [(App: rator rands)
                                 (loop (resolve-app rator rands stx))]
diff --git a/typed-racket-lib/typed-racket/private/type-contract.rkt b/typed-racket-lib/typed-racket/private/type-contract.rkt
index 736da947..37c0605d 100644
--- a/typed-racket-lib/typed-racket/private/type-contract.rkt
+++ b/typed-racket-lib/typed-racket/private/type-contract.rkt
@@ -6,9 +6,9 @@
  "../utils/utils.rkt"
  syntax/parse
  (rep type-rep prop-rep object-rep)
- (utils tc-utils hset)
+ (utils tc-utils)
  (env type-name-env row-constraint-env)
- (rep core-rep rep-utils type-mask values-rep)
+ (rep core-rep rep-utils type-mask values-rep base-types numeric-base-types)
  (types resolve utils printer match-expanders union)
  (prefix-in t: (types abbrev numeric-tower subtype))
  (private parse-type syntax-properties)
@@ -352,298 +352,304 @@
         (if (from-typed? typed-side)
             (and/sc sc any-wrap/sc)
             sc))
-      (cached-match sc-cache type typed-side
-        ;; Applications of implicit recursive type aliases
-        ;;
-        ;; We special case this rather than just resorting to standard
-        ;; App resolution (see case below) because the resolution process
-        ;; will make type->static-contract infinite loop.
-        [(App: (Name: name _ #f) _)
-         ;; Key with (cons name 'app) instead of just name because the
-         ;; application of the Name is not necessarily the same as the
-         ;; Name type alone
-         (cond [(hash-ref recursive-values (cons name 'app) #f)]
-               [else
-                (define name* (generate-temporary name))
-                (recursive-sc (list name*)
-                              (list
-                               (t->sc (resolve-once type)
-                                      #:recursive-values
-                                      (hash-set recursive-values
-                                                (cons name 'app)
-                                                (recursive-sc-use name*))))
-                              (recursive-sc-use name*))])]
-        ;; Implicit recursive aliases
-        [(Name: name-id args #f)
-         (cond [;; recursive references are looked up in a special table
-                ;; that's handled differently by sc instantiation
-                (lookup-name-sc type typed-side)]
-               [else
-                (define rv recursive-values)
-                (define resolved-name (resolve-once type))
-                (register-name-sc type
-                                  (λ () (loop resolved-name 'untyped rv))
-                                  (λ () (loop resolved-name 'typed rv))
-                                  (λ () (loop resolved-name 'both rv)))
-                (lookup-name-sc type typed-side)])]
-        ;; Ordinary type applications or struct type names, just resolve
-        [(or (App: _ _) (Name/struct:)) (t->sc (resolve-once type))]
-        [(Univ:) (if (from-typed? typed-side) any-wrap/sc any/sc)]
-        [(Bottom:) (or/sc)]
-        [(Listof: elem-ty) (listof/sc (t->sc elem-ty))]
-        [(Base: sym cnt _ _)
-         (flat/sc #`(flat-named-contract '#,sym (flat-contract-predicate #,cnt)) sym)]
-        [(Distinction: _ _ t) ; from define-new-subtype
-         (t->sc t)]
-        [(Refinement: par p?)
-         (and/sc (t->sc par) (flat/sc p?))]
-        [(? Union? t)
-         (match (normalize-type t)
-           [(Union: (app hset->list elems))
-            (define-values (numeric non-numeric) (partition (λ (t) (eq? mask:number (mask t))) elems))
-            (define numeric-sc (numeric-type->static-contract (apply Un numeric)))
-            (if numeric-sc
-                (apply or/sc numeric-sc (map t->sc non-numeric))
-                (apply or/sc (map t->sc elems)))]
-           [t (t->sc t)])]
-        [(Intersection: ts)
-         (define-values (chaperones/impersonators others)
-           (for/fold ([cs/is null] [others null])
-                     ([elem (in-hset ts)])
-             (define c (t->sc elem))
-             (if (equal? flat-sym (get-max-contract-kind c))
-                 (values cs/is (cons c others))
-                 (values (cons c cs/is) others))))
-         (cond
-           [(> (length chaperones/impersonators) 1)
-            (fail #:reason (~a "Intersection type contract contains"
-                               " more than 1 non-flat contract: "
-                               type))]
-           [else
-            (apply and/sc (append others chaperones/impersonators))])]
-        [(and t (Function: arrs))
-         #:when (any->bool? arrs)
-         ;; Avoid putting (-> any T) contracts on struct predicates (where Boolean <: T)
-         ;; Optimization: if the value is typed, we can assume it's not wrapped
-         ;;  in a type-unsafe chaperone/impersonator and use the unsafe contract
-         (let* ([unsafe-spp/sc (flat/sc #'struct-predicate-procedure?)]
-                [safe-spp/sc (flat/sc #'struct-predicate-procedure?/c)]
-                [optimized/sc (if (from-typed? typed-side)
-                                  unsafe-spp/sc
-                                  safe-spp/sc)])
-           (or/sc optimized/sc (t->sc/fun t)))]
-        [(and t (Function: _)) (t->sc/fun t)]
-        [(Set: t) (set/sc (t->sc t))]
-        [(Sequence: ts) (apply sequence/sc (map t->sc ts))]
-        [(Vector: t) (vectorof/sc (t->sc/both t))]
-        [(HeterogeneousVector: ts) (apply vector/sc (map t->sc/both ts))]
-        [(Box: t) (box/sc (t->sc/both t))]
-        [(Pair: t1 t2)
-         (cons/sc (t->sc t1) (t->sc t2))]
-        [(Async-Channel: t) (async-channel/sc (t->sc t))]
-        [(Promise: t)
-         (promise/sc (t->sc t))]
-        [(Opaque: p?)
-         (flat/sc #`(flat-named-contract (quote #,(syntax-e p?)) #,p?))]
-        [(Continuation-Mark-Keyof: t)
-         (continuation-mark-key/sc (t->sc t))]
-        ;; TODO: this is not quite right for case->
-        [(Prompt-Tagof: s (Function: (list (arr: (list ts ...) _ _ _ _))))
-         (prompt-tag/sc (map t->sc ts) (t->sc s))]
-        ;; TODO
-        [(F: v)
-         (triple-lookup
-           (hash-ref recursive-values v
-             (λ () (error 'type->static-contract
-                          "Recursive value lookup failed. ~a ~a" recursive-values v)))
-           typed-side)]
-        [(VectorTop:) (only-untyped vector?/sc)]
-        [(BoxTop:) (only-untyped box?/sc)]
-        [(ChannelTop:) (only-untyped channel?/sc)]
-        [(Async-ChannelTop:) (only-untyped async-channel?/sc)]
-        [(HashtableTop:) (only-untyped hash?/sc)]
-        [(MPairTop:) (only-untyped mpair?/sc)]
-        [(ThreadCellTop:) (only-untyped thread-cell?/sc)]
-        [(Prompt-TagTop:) (only-untyped prompt-tag?/sc)]
-        [(Continuation-Mark-KeyTop:) (only-untyped continuation-mark-key?/sc)]
-        [(ClassTop:) (only-untyped class?/sc)]
-        [(UnitTop:) (only-untyped unit?/sc)]
-        [(StructTypeTop:) (struct-type/sc null)]
-        ;; TODO Figure out how this should work
-        ;[(StructTop: s) (struct-top/sc s)]
+      (cached-match
+       sc-cache type typed-side
+       ;; Applications of implicit recursive type aliases
+       ;;
+       ;; We special case this rather than just resorting to standard
+       ;; App resolution (see case below) because the resolution process
+       ;; will make type->static-contract infinite loop.
+       [(App: (Name: name _ #f) _)
+        ;; Key with (cons name 'app) instead of just name because the
+        ;; application of the Name is not necessarily the same as the
+        ;; Name type alone
+        (cond [(hash-ref recursive-values (cons name 'app) #f)]
+              [else
+               (define name* (generate-temporary name))
+               (recursive-sc (list name*)
+                             (list
+                              (t->sc (resolve-once type)
+                                     #:recursive-values
+                                     (hash-set recursive-values
+                                               (cons name 'app)
+                                               (recursive-sc-use name*))))
+                             (recursive-sc-use name*))])]
+       ;; Implicit recursive aliases
+       [(Name: name-id args #f)
+        (cond [ ;; recursive references are looked up in a special table
+               ;; that's handled differently by sc instantiation
+               (lookup-name-sc type typed-side)]
+              [else
+               (define rv recursive-values)
+               (define resolved-name (resolve-once type))
+               (register-name-sc type
+                                 (λ () (loop resolved-name 'untyped rv))
+                                 (λ () (loop resolved-name 'typed rv))
+                                 (λ () (loop resolved-name 'both rv)))
+               (lookup-name-sc type typed-side)])]
+       ;; Ordinary type applications or struct type names, just resolve
+       [(or (App: _ _) (Name/struct:)) (t->sc (resolve-once type))]
+       [(Univ:) (if (from-typed? typed-side) any-wrap/sc any/sc)]
+       [(Bottom:) (or/sc)]
+       [(Listof: elem-ty) (listof/sc (t->sc elem-ty))]
+       ;; This comes before Base-ctc to use the Value-style logic
+       ;; for the singleton base types (e.g. -Null, 1, etc)
+       [(Val-able: v)
+        (if (and (c:flat-contract? v)
+                 ;; numbers used as contracts compare with =, but TR
+                 ;; requires an equal? check
+                 (not (number? v))
+                 ;; regexps don't match themselves when used as contracts
+                 (not (regexp? v)))
+            (flat/sc #`(quote #,v))
+            (flat/sc #`(flat-named-contract '#,v (lambda (x) (equal? x '#,v))) v))]
+       [(Base-name/contract: sym ctc)
+        (flat/sc #`(flat-named-contract '#,sym (flat-contract-predicate #,ctc)) sym)]
+       [(Distinction: _ _ t) ; from define-new-subtype
+        (t->sc t)]
+       [(Refinement: par p?)
+        (and/sc (t->sc par) (flat/sc p?))]
+       [(BaseUnion: bbits nbits)
+        (define numeric (make-BaseUnion #b0 nbits))
+        (define other-scs (map t->sc (bbits->base-types bbits)))
+        (define numeric-sc (numeric-type->static-contract numeric))
+        (if numeric-sc
+            (apply or/sc numeric-sc other-scs)
+            (apply or/sc (append other-scs (map t->sc (nbits->base-types nbits)))))]
+       [(? Union? t)
+        (match (normalize-type t)
+          [(Union: (? Bottom?) elems) (apply or/sc (map t->sc elems))]
+          [(Union: base elems) (apply or/sc (t->sc base) (map t->sc elems))]
+          [t (t->sc t)])]
+       [(Intersection: ts)
+        (define-values (chaperones/impersonators others)
+          (for/fold ([cs/is null] [others null])
+                    ([elem (in-list ts)])
+            (define c (t->sc elem))
+            (if (equal? flat-sym (get-max-contract-kind c))
+                (values cs/is (cons c others))
+                (values (cons c cs/is) others))))
+        (cond
+          [(> (length chaperones/impersonators) 1)
+           (fail #:reason (~a "Intersection type contract contains"
+                              " more than 1 non-flat contract: "
+                              type))]
+          [else
+           (apply and/sc (append others chaperones/impersonators))])]
+       [(and t (Function: arrs))
+        #:when (any->bool? arrs)
+        ;; Avoid putting (-> any T) contracts on struct predicates (where Boolean <: T)
+        ;; Optimization: if the value is typed, we can assume it's not wrapped
+        ;;  in a type-unsafe chaperone/impersonator and use the unsafe contract
+        (let* ([unsafe-spp/sc (flat/sc #'struct-predicate-procedure?)]
+               [safe-spp/sc (flat/sc #'struct-predicate-procedure?/c)]
+               [optimized/sc (if (from-typed? typed-side)
+                                 unsafe-spp/sc
+                                 safe-spp/sc)])
+          (or/sc optimized/sc (t->sc/fun t)))]
+       [(and t (Function: _)) (t->sc/fun t)]
+       [(Set: t) (set/sc (t->sc t))]
+       [(Sequence: ts) (apply sequence/sc (map t->sc ts))]
+       [(Vector: t) (vectorof/sc (t->sc/both t))]
+       [(HeterogeneousVector: ts) (apply vector/sc (map t->sc/both ts))]
+       [(Box: t) (box/sc (t->sc/both t))]
+       [(Pair: t1 t2)
+        (cons/sc (t->sc t1) (t->sc t2))]
+       [(Async-Channel: t) (async-channel/sc (t->sc t))]
+       [(Promise: t)
+        (promise/sc (t->sc t))]
+       [(Opaque: p?)
+        (flat/sc #`(flat-named-contract (quote #,(syntax-e p?)) #,p?))]
+       [(Continuation-Mark-Keyof: t)
+        (continuation-mark-key/sc (t->sc t))]
+       ;; TODO: this is not quite right for case->
+       [(Prompt-Tagof: s (Function: (list (arr: (list ts ...) _ _ _ _))))
+        (prompt-tag/sc (map t->sc ts) (t->sc s))]
+       ;; TODO
+       [(F: v)
+        (triple-lookup
+         (hash-ref recursive-values v
+                   (λ () (error 'type->static-contract
+                                "Recursive value lookup failed. ~a ~a" recursive-values v)))
+         typed-side)]
+       [(VectorTop:) (only-untyped vector?/sc)]
+       [(BoxTop:) (only-untyped box?/sc)]
+       [(ChannelTop:) (only-untyped channel?/sc)]
+       [(Async-ChannelTop:) (only-untyped async-channel?/sc)]
+       [(HashtableTop:) (only-untyped hash?/sc)]
+       [(MPairTop:) (only-untyped mpair?/sc)]
+       [(ThreadCellTop:) (only-untyped thread-cell?/sc)]
+       [(Prompt-TagTop:) (only-untyped prompt-tag?/sc)]
+       [(Continuation-Mark-KeyTop:) (only-untyped continuation-mark-key?/sc)]
+       [(ClassTop:) (only-untyped class?/sc)]
+       [(UnitTop:) (only-untyped unit?/sc)]
+       [(StructTypeTop:) (struct-type/sc null)]
+       ;; TODO Figure out how this should work
+       ;[(StructTop: s) (struct-top/sc s)]
 
 
-        [(? Poly?)
-         (t->sc/poly type fail typed-side recursive-values t->sc)]
-        [(? PolyDots?)
-         (t->sc/polydots type fail typed-side recursive-values t->sc)]
-        [(? PolyRow?)
-         (t->sc/polyrow type fail typed-side recursive-values t->sc)]
+       [(? Poly?)
+        (t->sc/poly type fail typed-side recursive-values t->sc)]
+       [(? PolyDots?)
+        (t->sc/polydots type fail typed-side recursive-values t->sc)]
+       [(? PolyRow?)
+        (t->sc/polyrow type fail typed-side recursive-values t->sc)]
 
-        [(Mu: n b)
-         (match-define (and n*s (list untyped-n* typed-n* both-n*)) (generate-temporaries (list n n n)))
-         (define rv
-           (hash-set recursive-values n
-                     (triple (recursive-sc-use untyped-n*)
-                             (recursive-sc-use typed-n*)
-                             (recursive-sc-use both-n*))))
-         (case typed-side
-           [(both) (recursive-sc
-                     (list both-n*)
-                     (list (loop b 'both rv))
-                     (recursive-sc-use both-n*))]
-           [(typed untyped)
-            (define (rec b side rv)
-              (loop b side rv))
-            ;; TODO not fail in cases that don't get used
-            (define untyped (rec b 'untyped rv))
-            (define typed (rec b 'typed rv))
-            (define both (rec b 'both rv))
-  
-            (recursive-sc
-                     n*s
-                     (list untyped typed both)
-                     (recursive-sc-use (if (from-typed? typed-side) typed-n* untyped-n*)))])]
-        ;; Don't directly use the class static contract generated for Name,
-        ;; because that will get an #:opaque class contract. This will do the
-        ;; wrong thing for object types since it errors too eagerly.
-        [(Instance: (? Name? t))
-         #:when (Class? (resolve-once t))
-         (cond [(lookup-name-sc type typed-side)]
-               [else
-                (define rv recursive-values)
-                (define resolved (make-Instance (resolve-once t)))
-                (register-name-sc type
-                                  (λ () (loop resolved 'untyped rv))
-                                  (λ () (loop resolved 'typed rv))
-                                  (λ () (loop resolved 'both rv)))
-                (lookup-name-sc type typed-side)])]
-        [(Instance: (Class: _ _ fields methods _ _))
-         (match-define (list (list field-names field-types) ...) fields)
-         (match-define (list (list public-names public-types) ...) methods)
-         (object/sc (from-typed? typed-side)
-                    (append (map (λ (n sc) (member-spec 'method n sc))
-                                 public-names (map t->sc/meth public-types))
-                            (map (λ (n sc) (member-spec 'field n sc))
-                                 field-names (map t->sc/both field-types))))]
-        [(Class: row-var inits fields publics augments _)
-         (match-define (list (list init-names init-types _) ...) inits)
-         (match-define (list (list field-names field-types) ...) fields)
-         (match-define (list (list public-names public-types) ...) publics)
-         (match-define (list (list augment-names augment-types) ...) augments)
-         (define-values (pubment-names pubment-types)
-           (for/lists (_1 _2) ([name (in-list public-names)]
-                               [type (in-list public-types)]
-                               #:when (memq name augment-names))
-             (values name type)))
-         (define-values (override-names override-types)
-           (for/lists (_1 _2) ([name (in-list public-names)]
-                               [type (in-list public-types)]
-                               #:unless (memq name pubment-names))
-             (values name type)))
-         ;; we need to generate absent clauses for non-opaque class contracts
-         ;; that occur inside of a mixin type
-         (define absents
-           (cond [;; row constraints are only mapped when it's a row polymorphic
-                  ;; function in *positive* position (with no sealing)
-                  (and (F? row-var) (lookup-row-constraints (F-n row-var)))
-                  =>
-                  (λ (constraints)
-                    ;; the constraints with no corresponding type/contract need
-                    ;; to be absent
-                    (append (remove* field-names (cadr constraints))
-                            (remove* public-names (caddr constraints))))]
-                 [else null]))
-         ;; add a seal/unseal if there was a row variable and the
-         ;; row polymorphic function type was in negative position
-         (define seal/sc
-           (and (F? row-var)
-                (not (lookup-row-constraints (F-n row-var)))
-                (triple-lookup
-                 (hash-ref recursive-values (F-n row-var)
-                           (λ () (error 'type->static-contract
-                                        "Recursive value lookup failed. ~a ~a"
-                                        recursive-values (F-n row-var))))
-                 typed-side)))
-         (define sc-for-class
-           (class/sc ;; only enforce opaqueness if there's no row variable
-                     ;; and we are importing from untyped
-                     (and (from-untyped? typed-side) (not row-var))
-                     (append
-                       (map (λ (n sc) (member-spec 'override n sc))
-                            override-names (map t->sc/meth override-types))
-                       (map (λ (n sc) (member-spec 'pubment n sc))
-                            pubment-names (map t->sc/meth pubment-types))
-                       (map (λ (n sc) (member-spec 'inner n sc))
-                            augment-names (map t->sc/meth augment-types))
-                       (map (λ (n sc) (member-spec 'init n sc))
-                            init-names (map t->sc/neg init-types))
-                       (map (λ (n sc) (member-spec 'field n sc))
-                            field-names (map t->sc/both field-types)))
-                     absents))
-         (if seal/sc
-             (and/sc seal/sc sc-for-class)
-             sc-for-class)]
-        [(Unit: imports exports init-depends results)
-         (define (traverse sigs)
-           (for/list ([sig (in-list sigs)])
-             (define mapping 
-               (map
-                (match-lambda 
-                  [(cons id type) (cons id (t->sc type))])
-                (Signature-mapping sig)))
-             (signature-spec (Signature-name sig) (map car mapping) (map cdr mapping))))
-         
-         (define imports-specs (traverse imports))
-         (define exports-specs (traverse exports))
-         (define init-depends-ids (map Signature-name init-depends))
-         (match results
-           [(? AnyValues?)
-            (fail #:reason (~a "cannot generate contract for unit type"
-                               " with unknown return values"))]
-           [(Values: (list (Result: rngs _ _) ...))
-            (unit/sc imports-specs exports-specs init-depends-ids (map t->sc rngs))])]
-        [(Struct: nm par (list (fld: flds acc-ids mut?) ...) proc poly? pred?)
-         (cond
-           [(dict-ref recursive-values nm #f)]
-           [proc (fail #:reason "procedural structs are not supported")]
-           [poly?
-            (define nm* (generate-temporary #'n*))
-            (define fields
-              (for/list ([fty flds] [mut? mut?])
-                (t->sc fty #:recursive-values (hash-set
-                                                recursive-values
-                                                nm (recursive-sc-use nm*)))))
-            (recursive-sc (list nm*) (list (struct/sc nm (ormap values mut?) fields))
-                                (recursive-sc-use nm*))]
-           [else (flat/sc #`(flat-named-contract '#,(syntax-e pred?) (lambda (x) (#,pred? x))))])]
-        [(StructType: s)
-         (if (from-untyped? typed-side)
-             (fail #:reason (~a "cannot import structure types from"
-                                "untyped code"))
-             (struct-type/sc null))]
-        [(Syntax: (Base: 'Symbol _ _ _)) identifier?/sc]
-        [(Syntax: t)
-         (syntax/sc (t->sc t))]
-        [(Value: v)
-         (if (and (c:flat-contract? v)
-                  ;; numbers used as contracts compare with =, but TR
-                  ;; requires an equal? check
-                  (not (number? v))
-                  ;; regexps don't match themselves when used as contracts
-                  (not (regexp? v)))
-             (flat/sc #`(quote #,v))
-             (flat/sc #`(flat-named-contract '#,v (lambda (x) (equal? x '#,v))) v))]
-        [(Param: in out) 
-         (parameter/sc (t->sc in) (t->sc out))]
-        [(Hashtable: k v)
-         (hash/sc (t->sc k) (t->sc v))]
-        [(Channel: t)
-         (channel/sc (t->sc t))]
-        [(Evt: t)
-         (evt/sc (t->sc t))]
-        [else
-         (fail #:reason "contract generation not supported for this type")]))))
+       [(Mu: n b)
+        (match-define (and n*s (list untyped-n* typed-n* both-n*)) (generate-temporaries (list n n n)))
+        (define rv
+          (hash-set recursive-values n
+                    (triple (recursive-sc-use untyped-n*)
+                            (recursive-sc-use typed-n*)
+                            (recursive-sc-use both-n*))))
+        (case typed-side
+          [(both) (recursive-sc
+                   (list both-n*)
+                   (list (loop b 'both rv))
+                   (recursive-sc-use both-n*))]
+          [(typed untyped)
+           (define (rec b side rv)
+             (loop b side rv))
+           ;; TODO not fail in cases that don't get used
+           (define untyped (rec b 'untyped rv))
+           (define typed (rec b 'typed rv))
+           (define both (rec b 'both rv))
+           
+           (recursive-sc
+            n*s
+            (list untyped typed both)
+            (recursive-sc-use (if (from-typed? typed-side) typed-n* untyped-n*)))])]
+       ;; Don't directly use the class static contract generated for Name,
+       ;; because that will get an #:opaque class contract. This will do the
+       ;; wrong thing for object types since it errors too eagerly.
+       [(Instance: (? Name? t))
+        #:when (Class? (resolve-once t))
+        (cond [(lookup-name-sc type typed-side)]
+              [else
+               (define rv recursive-values)
+               (define resolved (make-Instance (resolve-once t)))
+               (register-name-sc type
+                                 (λ () (loop resolved 'untyped rv))
+                                 (λ () (loop resolved 'typed rv))
+                                 (λ () (loop resolved 'both rv)))
+               (lookup-name-sc type typed-side)])]
+       [(Instance: (Class: _ _ fields methods _ _))
+        (match-define (list (list field-names field-types) ...) fields)
+        (match-define (list (list public-names public-types) ...) methods)
+        (object/sc (from-typed? typed-side)
+                   (append (map (λ (n sc) (member-spec 'method n sc))
+                                public-names (map t->sc/meth public-types))
+                           (map (λ (n sc) (member-spec 'field n sc))
+                                field-names (map t->sc/both field-types))))]
+       [(Class: row-var inits fields publics augments _)
+        (match-define (list (list init-names init-types _) ...) inits)
+        (match-define (list (list field-names field-types) ...) fields)
+        (match-define (list (list public-names public-types) ...) publics)
+        (match-define (list (list augment-names augment-types) ...) augments)
+        (define-values (pubment-names pubment-types)
+          (for/lists (_1 _2) ([name (in-list public-names)]
+                              [type (in-list public-types)]
+                              #:when (memq name augment-names))
+            (values name type)))
+        (define-values (override-names override-types)
+          (for/lists (_1 _2) ([name (in-list public-names)]
+                              [type (in-list public-types)]
+                              #:unless (memq name pubment-names))
+            (values name type)))
+        ;; we need to generate absent clauses for non-opaque class contracts
+        ;; that occur inside of a mixin type
+        (define absents
+          (cond [ ;; row constraints are only mapped when it's a row polymorphic
+                 ;; function in *positive* position (with no sealing)
+                 (and (F? row-var) (lookup-row-constraints (F-n row-var)))
+                 =>
+                 (λ (constraints)
+                   ;; the constraints with no corresponding type/contract need
+                   ;; to be absent
+                   (append (remove* field-names (cadr constraints))
+                           (remove* public-names (caddr constraints))))]
+                [else null]))
+        ;; add a seal/unseal if there was a row variable and the
+        ;; row polymorphic function type was in negative position
+        (define seal/sc
+          (and (F? row-var)
+               (not (lookup-row-constraints (F-n row-var)))
+               (triple-lookup
+                (hash-ref recursive-values (F-n row-var)
+                          (λ () (error 'type->static-contract
+                                       "Recursive value lookup failed. ~a ~a"
+                                       recursive-values (F-n row-var))))
+                typed-side)))
+        (define sc-for-class
+          (class/sc ;; only enforce opaqueness if there's no row variable
+           ;; and we are importing from untyped
+           (and (from-untyped? typed-side) (not row-var))
+           (append
+            (map (λ (n sc) (member-spec 'override n sc))
+                 override-names (map t->sc/meth override-types))
+            (map (λ (n sc) (member-spec 'pubment n sc))
+                 pubment-names (map t->sc/meth pubment-types))
+            (map (λ (n sc) (member-spec 'inner n sc))
+                 augment-names (map t->sc/meth augment-types))
+            (map (λ (n sc) (member-spec 'init n sc))
+                 init-names (map t->sc/neg init-types))
+            (map (λ (n sc) (member-spec 'field n sc))
+                 field-names (map t->sc/both field-types)))
+           absents))
+        (if seal/sc
+            (and/sc seal/sc sc-for-class)
+            sc-for-class)]
+       [(Unit: imports exports init-depends results)
+        (define (traverse sigs)
+          (for/list ([sig (in-list sigs)])
+            (define mapping 
+              (map
+               (match-lambda 
+                 [(cons id type) (cons id (t->sc type))])
+               (Signature-mapping sig)))
+            (signature-spec (Signature-name sig) (map car mapping) (map cdr mapping))))
+        
+        (define imports-specs (traverse imports))
+        (define exports-specs (traverse exports))
+        (define init-depends-ids (map Signature-name init-depends))
+        (match results
+          [(? AnyValues?)
+           (fail #:reason (~a "cannot generate contract for unit type"
+                              " with unknown return values"))]
+          [(Values: (list (Result: rngs _ _) ...))
+           (unit/sc imports-specs exports-specs init-depends-ids (map t->sc rngs))])]
+       [(Struct: nm par (list (fld: flds acc-ids mut?) ...) proc poly? pred?)
+        (cond
+          [(dict-ref recursive-values nm #f)]
+          [proc (fail #:reason "procedural structs are not supported")]
+          [poly?
+           (define nm* (generate-temporary #'n*))
+           (define fields
+             (for/list ([fty flds] [mut? mut?])
+               (t->sc fty #:recursive-values (hash-set
+                                              recursive-values
+                                              nm (recursive-sc-use nm*)))))
+           (recursive-sc (list nm*) (list (struct/sc nm (ormap values mut?) fields))
+                         (recursive-sc-use nm*))]
+          [else (flat/sc #`(flat-named-contract '#,(syntax-e pred?) (lambda (x) (#,pred? x))))])]
+       [(StructType: s)
+        (if (from-untyped? typed-side)
+            (fail #:reason (~a "cannot import structure types from"
+                               "untyped code"))
+            (struct-type/sc null))]
+       [(Syntax: (? Base:Symbol?)) identifier?/sc]
+       [(Syntax: t)
+        (syntax/sc (t->sc t))]
+       [(Param: in out) 
+        (parameter/sc (t->sc in) (t->sc out))]
+       [(Hashtable: k v)
+        (hash/sc (t->sc k) (t->sc v))]
+       [(Channel: t)
+        (channel/sc (t->sc t))]
+       [(Evt: t)
+        (evt/sc (t->sc t))]
+       [else
+        (fail #:reason "contract generation not supported for this type")]))))
 
 (define (t->sc/function f fail typed-side recursive-values loop method?)
   (define (t->sc t #:recursive-values (recursive-values recursive-values))
@@ -783,8 +789,8 @@
           (let loop ([ty b])
             (match (resolve ty)
               [(Function: _) #t]
-              [(Union: elems) (for/and ([elem (in-hset elems)]) (loop elem))]
-              [(Intersection: elems) (for/or ([elem (in-hset elems)]) (loop elem))]
+              [(Union: _ elems) (andmap loop elems)]
+              [(Intersection: elems) (ormap loop elems)]
               [(Poly: _ body) (loop body)]
               [(PolyDots: _ body) (loop body)]
               [_ #f])))
@@ -822,8 +828,8 @@
           (let loop ([ty b])
             (match (resolve ty)
               [(Function: _) #t]
-              [(Union: elems) (for/and ([elem (in-hset elems)]) (loop elem))]
-              [(Intersection: elems) (for/or ([elem (in-hset elems)]) (loop elem))]
+              [(Union: _ elems) (andmap loop elems)]
+              [(Intersection: elems) (ormap loop elems)]
               [(Poly: _ body) (loop body)]
               [(PolyDots: _ body) (loop body)]
               [_ #f])))
diff --git a/typed-racket-lib/typed-racket/rep/base-type-rep.rkt b/typed-racket-lib/typed-racket/rep/base-type-rep.rkt
new file mode 100644
index 00000000..360c68b1
--- /dev/null
+++ b/typed-racket-lib/typed-racket/rep/base-type-rep.rkt
@@ -0,0 +1,109 @@
+#lang racket/base
+
+(require "rep-utils.rkt"
+         "core-rep.rkt"
+         "type-mask.rkt"
+         racket/match
+         (for-syntax racket/base
+                     racket/syntax
+                     syntax/parse))
+
+(provide define-base-types
+         Base?
+         Base-name
+         Base-predicate
+         Base-bits:
+         Base-predicate:
+         Base-name/contract:)
+
+;;-----------------
+;; Base Type
+;;-----------------
+
+;; name - a printable type name (unique for each Base)
+;; numeric? - is this Base type for values where 'number?' is #t
+;; bits - the binary representation of this Base type, used in BaseUnions
+;; to efficiently represent unions of Bases. NOTE: this should include only
+;; one bit set to 1.
+;; contract - used when generating contracts from types
+;; predicate - used to check (at compile-time) whether a value belongs
+;; to that base type. This is used to check for subtyping between value
+;; types and base types.
+(def-type Base ([name symbol?]
+                [numeric? boolean?]
+                [bits exact-nonnegative-integer?]
+                [contract syntax?]
+                [predicate procedure?])
+  #:base
+  #:no-provide
+  [#:mask (λ (t) (if (Base-numeric? t)
+                     mask:number
+                     mask:base))]
+  #:non-transparent
+  [#:extras
+   ;; equality only need consider the 'name' field
+   #:methods gen:equal+hash
+   [(define (equal-proc a b _)
+      (eq? (Base-name a) (Base-name b)))
+    (define (hash-proc a _)
+      (equal-hash-code (Base-name a)))
+    (define (hash2-proc a _)
+      (equal-secondary-hash-code (Base-name a)))]])
+
+(define-match-expander Base-bits:
+  (λ (stx) (syntax-case stx ()
+             [(_ numeric? bits)
+              (syntax/loc stx (Base: _ numeric? bits _ _))])))
+
+(define-match-expander Base-predicate:
+  (λ (stx) (syntax-case stx ()
+             [(_ pred)
+              (syntax/loc stx (Base: _ _ _ _ pred))])))
+
+(define-match-expander Base-name/contract:
+  (λ (stx) (syntax-case stx ()
+             [(_ name ctc)
+              (syntax/loc stx (Base: name _ _ ctc _))])))
+
+;; macro for easily defining sets of types whose representation
+;; relies on predefined fixnum bitfields
+(define-syntax (define-base-types stx)
+  (define-syntax-class atoms-spec
+    (pattern [abbrev:id
+              name:id
+              contract:expr
+              predicate:expr]
+             #:with type-pred (format-id #'name "Base:~a?" (syntax-e #'name))
+             #:with provide #'(provide abbrev type-pred)))
+  (syntax-parse stx
+    [(_ #:numeric? num?:boolean
+        #:max-count max-count-stx:exact-nonnegative-integer
+        #:count count:id
+        #:atom-vector atom-vector:id
+        #:atom-hash atom-hash:id
+        #:atoms
+        atoms:atoms-spec ...)
+     (define max-count (syntax->datum #'max-count-stx))
+     (define atom-list (syntax->datum #'(atoms.name ...)))
+     (define atom-count (length atom-list))
+     (unless (<= atom-count max-count)
+       (raise-syntax-error
+        'define-type-bitfield
+        (format "too many atomic base types (~a is the max)"
+                max-count)
+        stx))
+     (with-syntax ([(n ... ) (for/list ([i (in-range atom-count)]) i)]
+                   [(2^n ...)
+                    (build-list atom-count (λ (n) (arithmetic-shift 1 n)))])
+       #`(begin
+           (define count #,atom-count)
+           ;; define the actual type references (e.g. -Null)
+           (define/decl atoms.abbrev
+             (make-Base (quote atoms.name) num? 2^n atoms.contract atoms.predicate))
+           ...
+           (define atoms.type-pred (λ (t) (equal? t atoms.abbrev))) ...
+           atoms.provide ...
+           (define atom-vector
+             (vector-immutable atoms.abbrev ...))
+           (define atom-hash
+             (make-immutable-hasheqv (list (cons 2^n atoms.abbrev) ...)))))]))
diff --git a/typed-racket-lib/typed-racket/rep/base-types.rkt b/typed-racket-lib/typed-racket/rep/base-types.rkt
new file mode 100644
index 00000000..9ad32671
--- /dev/null
+++ b/typed-racket-lib/typed-racket/rep/base-types.rkt
@@ -0,0 +1,220 @@
+#lang racket/base
+
+;; This file contains the definitions for Base types that are not numeric
+;; (i.e. where number? returns #f for values of the type)
+
+(require "../utils/utils.rkt"
+         (rep rep-utils base-type-rep type-mask core-rep)
+         racket/undefined
+         (types numeric-predicates)
+         racket/extflonum
+         ;; for base type contracts and predicates
+         ;; use '#%place to avoid the other dependencies of `racket/place`
+         (for-template
+           racket/base
+           racket/contract/base
+           racket/undefined
+           racket/extflonum
+           (only-in racket/pretty pretty-print-style-table?)
+           (only-in racket/udp udp?)
+           (only-in racket/tcp tcp-listener?)
+           (only-in racket/flonum flvector?)
+           (only-in racket/extflonum extflvector?)
+           (only-in racket/fixnum fxvector?)
+           (only-in racket/future fsemaphore?)
+           (only-in '#%place place? place-channel?))
+         (only-in racket/pretty pretty-print-style-table?)
+         (only-in racket/udp udp?)
+         (only-in racket/tcp tcp-listener?)
+         (only-in racket/flonum flvector?)
+         (only-in racket/extflonum extflvector?)
+         (only-in racket/fixnum fxvector?)
+         (only-in racket/future fsemaphore?)
+         (only-in '#%place place? place-channel?))
+
+(provide bbits->base-types
+         bbits->atom?
+         bbits-subset?
+         bbits-overlap?
+         bbits-union
+         bbits-intersect
+         bbits-subtract)
+
+;; these logical combinators are for single argument 
+;; functions and perform better than the generic
+;; variants from racket/function
+(define-syntax-rule (¬ f) (λ (x) (not (f x))))
+(define-syntax-rule (compose/and f ...) (λ (x) (and (f x) ...)))
+
+;; returns the single non-numeric Base type represented
+;; represented by bits, or #f if it is #b0 or more than
+;; one bit is set
+(define (bbits->atom? bits)
+  (hash-ref base-atom-hash bits #f))
+
+;; takes the bitwise representation of a union of non-numeric
+;; Base types and returns a list of the present Base types
+(define (bbits->base-types bbits)
+  (cond
+    [(eqv? 0 bbits) '()]
+    [else
+     (for*/fold ([acc '()])
+                ([low (in-range 0 base-count 8)]
+                 [high (in-value (min (+ low 8) base-count))]
+                 #:when (not (zero? (bitwise-bit-field bbits low high))))
+       (for/fold ([acc acc])
+                 ([idx (in-range low high)]
+                  #:when (bitwise-bit-set? bbits idx))
+         (cons (vector-ref base-atom-vector idx) acc)))]))
+
+;; bitwise set operations
+;;
+;; Note that for for non-numeric Base bits we assume they
+;; can be up to 62 bits (see declarations below), so we use
+;; 'bitwise' operations since on 32-bit machines they are
+;; not guaranteed to be fixnums.
+
+(define (bbits-subset? bbits1 bbits2)
+  (eqv? 0 (bbits-subtract bbits1 bbits2)))
+
+(define (bbits-overlap? bbits1 bbits2)
+  (not (eqv? 0 (bitwise-and bbits1 bbits2))))
+
+(define (bbits-union bbits1 bbits2)
+  (bitwise-ior bbits1 bbits2))
+
+(define (bbits-intersect bbits1 bbits2)
+  (bitwise-and bbits1 bbits2))
+
+(define (bbits-subtract bbits1 bbits2)
+  (bitwise-and bbits1 (bitwise-not bbits2)))
+
+(define-base-types
+  #:numeric? #f
+  ;; 62 bits is the max for a 2's complement 64-bit fixnum
+  #:max-count 62
+  #:count base-count
+  #:atom-vector base-atom-vector
+  #:atom-hash base-atom-hash
+  #:atoms
+  [-False False #'not not]
+  [-True True #'(λ (x) (eq? #t x)) (λ (x) (eq? #t x))]
+  [-Null Null #'null? null?]
+  [-Void Void #'void? void?]
+  [-Char Char #'char? char?]
+  [-Symbol Symbol #'symbol? symbol?]
+  [-String String #'string? string?]
+  [-Output-Port Output-Port #'output-port? output-port?]
+  [-Input-Port Input-Port #'input-port? input-port?]
+  [-Bytes Bytes #'bytes? bytes?]
+  [-Base-Regexp
+   Base-Regexp
+   #'(and/c regexp? (not/c pregexp?))
+   (compose/and regexp? (¬ pregexp?))]
+  [-PRegexp PRegexp #'pregexp? pregexp?]
+  [-Byte-Base-Regexp Byte-Base-Regexp
+                     #'(and/c byte-regexp? (not/c byte-pregexp?))
+                     (compose/and byte-regexp? (¬ byte-pregexp?))]
+  [-Byte-PRegexp Byte-PRegexp #'byte-pregexp? byte-pregexp?]
+  [-Keyword Keyword #'keyword? keyword?]
+  [-Thread Thread #'thread? thread?]
+  [-Path Path #'path? path?]
+  [-Resolved-Module-Path
+   Resolved-Module-Path
+   #'resolved-module-path?
+   resolved-module-path?]
+  [-Module-Path-Index
+   Module-Path-Index
+   #'module-path-index?
+   module-path-index?]
+  [-OtherSystemPath
+   OtherSystemPath
+   #'(and/c path-for-some-system? (not/c path?))
+   (compose/and path-for-some-system? (¬ path?))]
+  [-Cont-Mark-Set
+   Continuation-Mark-Set
+   #'continuation-mark-set?
+   continuation-mark-set?]
+  [-TCP-Listener TCP-Listener #'tcp-listener? tcp-listener?]
+  [-UDP-Socket UDP-Socket #'udp? udp?]
+  [-FlVector FlVector #'flvector? flvector?]
+  [-FxVector FxVector #'fxvector? fxvector?]
+  [-Namespace Namespace #'namespace? namespace?]
+  [-Compiled-Module-Expression
+   Compiled-Module-Expression
+   #'compiled-module-expression?
+   compiled-module-expression?]
+  [-Compiled-Non-Module-Expression
+   Compiled-Non-Module-Expression
+   #'(and/c compiled-expression?
+            (not/c  compiled-module-expression?))
+   (compose/and compiled-expression?
+                (¬ compiled-module-expression?))]
+  [-Pretty-Print-Style-Table
+   Pretty-Print-Style-Table
+   #'pretty-print-style-table?
+   pretty-print-style-table?]
+  [-Read-Table Read-Table #'readtable? readtable?]
+  [-Special-Comment Special-Comment #'special-comment? special-comment?]
+  [-Custodian Custodian #'custodian? custodian?]
+  [-Parameterization Parameterization #'parameterization? parameterization?]
+  [-Inspector Inspector #'inspector? inspector?]
+  [-Namespace-Anchor Namespace-Anchor #'namespace-anchor? namespace-anchor?]
+  [-Variable-Reference Variable-Reference #'variable-reference? variable-reference?]
+  [-Internal-Definition-Context
+   Internal-Definition-Context
+   #'internal-definition-context?
+   internal-definition-context?]
+  [-Subprocess Subprocess #'subprocess? subprocess?]
+  [-Security-Guard Security-Guard #'security-guard? security-guard?]
+  [-Thread-Group Thread-Group #'thread-group? thread-group?]
+  [-Struct-Type-Property Struct-Type-Property #'struct-type-property? struct-type-property?]
+  [-Impersonator-Property Impersonator-Property #'impersonator-property? impersonator-property?]
+  [-Semaphore Semaphore #'semaphore? semaphore?]
+  [-FSemaphore FSemaphore #'fsemaphore? fsemaphore?]
+  [-Bytes-Converter Bytes-Converter #'bytes-converter? bytes-converter?]
+  [-Pseudo-Random-Generator
+   Pseudo-Random-Generator
+   #'pseudo-random-generator?
+   pseudo-random-generator?]
+  [-Logger Logger #'logger? logger?]
+  [-Log-Receiver Log-Receiver #'log-receiver? log-receiver?]
+  [-Place Place #'place? place?]
+  [-Base-Place-Channel
+   Base-Place-Channel #'(and/c place-channel? (not/c place?))
+   (compose/and place-channel? (¬ place?))]
+  [-Will-Executor Will-Executor #'will-executor? will-executor?]
+  [-Environment-Variables
+   Environment-Variables
+   #'environment-variables?
+   environment-variables?]
+  [-Undefined
+   Undefined
+   #'(λ (x) (eq? x undefined))
+   (λ (x) (eq? x undefined))]
+  [-ExtFlVector ExtFlVector #'extflvector? extflvector?]
+  ;; 80-bit floating-point numbers
+  ;; +nan.t is included in all 80-bit floating-point types
+  ;; NOTE: these are here and not in the numeric tower because
+  ;; they return #f for number?
+  [-ExtFlonumNan
+   ExtFlonum-Nan
+   #'(and/c extflonum? (lambda (x) (eqv? x +nan.t)))
+   (λ (x) (and (extflonum? x) (eqv? x +nan.t)))]
+  [-ExtFlonumPosZero
+   ExtFlonum-Positive-Zero
+   #'(λ (x) (eqv? x 0.0t0))
+   (λ (x) (eqv? x 0.0t0))]
+  [-ExtFlonumNegZero
+   ExtFlonum-Negative-Zero
+   #'(λ (x) (eqv? x -0.0t0))
+   (λ (x) (eqv? x -0.0t0))]
+  [-NegExtFlonumNoNan
+   Negative-ExtFlonum-No-NaN
+   #'(and/c extflonum? (λ (x) (extfl<= x 0.0t0)))
+   (λ (x) (and (extflonum? x) (extfl<= x 0.0t0)))]
+  [-PosExtFlonumNoNan
+   Positive-ExtFlonum-No-NaN
+   #'(and/c extflonum? (λ (x) (extfl>= x 0.0t0)))
+   (λ (x) (and (extflonum? x) (extfl>= x 0.0t0)))]
+  [-Dead-Code Dead-Code #'(make-none/c 'dead-code/c) (λ (v) #f)])
diff --git a/typed-racket-lib/typed-racket/rep/base-union.rkt b/typed-racket-lib/typed-racket/rep/base-union.rkt
new file mode 100644
index 00000000..77ffd2f6
--- /dev/null
+++ b/typed-racket-lib/typed-racket/rep/base-union.rkt
@@ -0,0 +1,63 @@
+#lang racket/base
+
+(require "rep-utils.rkt"
+         "type-mask.rkt"
+         "core-rep.rkt"
+         "base-types.rkt"
+         "numeric-base-types.rkt"
+         racket/match
+         (for-syntax racket/base))
+
+(provide BaseUnion-bases:
+         BaseUnion-bases)
+
+;; BaseUnion
+;;
+;; BaseUnions contain a compact representation for unions
+;; of Base types. Base types are divided into two categories:
+;; those that are numeric (i.e. number? returns #t) and those
+;; that are not. See 'base-types.rkt' and 'numeric-base-types.rkt'
+;; for the various defined Base types.
+;; 
+;; bbits - the combined bits (via inclusive bit or) for
+;; all Base members where Base-numeric? is #f
+;; nbits - the combined bits (via inclusive bit or) for
+;; all Base members where Base-numeric? is #t
+(def-type BaseUnion ([bbits exact-nonnegative-integer?]
+                     [nbits exact-nonnegative-integer?])
+  #:base
+  [#:mask (match-lambda [(BaseUnion: bbits nbits)
+                         (cond
+                           [(eqv? #b0 bbits) mask:number]
+                           [(eqv? #b0 nbits) mask:base]
+                           [else mask:base+number])])]
+  [#:custom-constructor
+   ;; make sure we do not build BaseUnions equivalent to
+   ;; Bottom or a *single* Base type
+   (cond
+     [(eqv? bbits 0)
+      (cond
+        [(eqv? nbits 0) -Bottom]
+        [(nbits->atom? nbits)]
+        [else (make-BaseUnion bbits nbits)])]
+     [(eqv? nbits 0)
+      (cond
+        [(bbits->atom? bbits)]
+        [else (make-BaseUnion bbits nbits)])]
+     [else (make-BaseUnion bbits nbits)])])
+
+(define-match-expander BaseUnion-bases:
+  (λ (stx) (syntax-case stx ()
+             [(_ bases)
+              (syntax/loc stx
+                (and (? BaseUnion?)
+                     (app BaseUnion-bases bases)))])))
+
+(define (BaseUnion-bases t)
+  (match t
+    [(BaseUnion: bbits nbits)
+     (cond
+       [(eqv? bbits 0) (nbits->base-types nbits)]
+       [(eqv? nbits 0) (bbits->base-types bbits)]
+       [else (append (bbits->base-types bbits)
+                     (nbits->base-types nbits))])]))
diff --git a/typed-racket-lib/typed-racket/rep/core-rep.rkt b/typed-racket-lib/typed-racket/rep/core-rep.rkt
index c05a6e87..14f9d044 100644
--- a/typed-racket-lib/typed-racket/rep/core-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/core-rep.rkt
@@ -111,6 +111,7 @@
   [#:mask mask:bottom]
   [#:singleton -Bottom])
 
+
 ;;************************************************************
 ;; Prop
 ;;************************************************************
diff --git a/typed-racket-lib/typed-racket/rep/numeric-base-types.rkt b/typed-racket-lib/typed-racket/rep/numeric-base-types.rkt
new file mode 100644
index 00000000..dce4a03a
--- /dev/null
+++ b/typed-racket-lib/typed-racket/rep/numeric-base-types.rkt
@@ -0,0 +1,247 @@
+#lang racket/base
+
+;; This file contains the definitions for Base types that are numeric
+;; (i.e. where number? returns #t for values of the type)
+
+
+(require "../utils/utils.rkt"
+         (rep rep-utils base-type-rep type-mask core-rep)
+         (types numeric-predicates)
+         racket/unsafe/ops
+         ;; For base type contracts
+         (for-template racket/base racket/contract/base (types numeric-predicates)))
+
+(provide portable-fixnum?
+         portable-index?
+         nbits->atom?
+         nbits->base-types
+         nbits-subset?
+         nbits-overlap?
+         nbits-intersect
+         nbits-union
+         nbits-subtract)
+
+;; Is the number a fixnum on *all* the platforms Racket supports?  This
+;; works because Racket compiles only on 32+ bit systems.  This check is
+;; done at compile time to typecheck literals -- so use it instead of
+;; `fixnum?' to avoid creating platform-dependent .zo files.
+(define (portable-fixnum? n)
+  (and (exact-integer? n)
+       (< n (expt 2 30))
+       (>= n (- (expt 2 30)))))
+;; same, for indexes
+(define (portable-index? n)
+  (and (exact-integer? n)
+       (< n (expt 2 28))
+       (>= n 0)))
+
+
+;; returns the single numeric Base type represented
+;; represented by bits, or #f if it is #b0 or more than
+;; one bit is set
+(define (nbits->atom? bits)
+  (hash-ref numeric-atom-hash bits #f))
+
+
+;; bitwise set operations
+;;
+;; Note that for numeric Base bits we assume they can be up
+;; to 30 bits (see declarations below), so we use 'unsafe-fx'
+;; operations since even on 32-bit machines they are all fixnums.
+
+
+(define (nbits-subset? nbits1 nbits2)
+  (unsafe-fx= 0 (nbits-subtract nbits1 nbits2)))
+
+(define (nbits-overlap? nbits1 nbits2)
+  (not (unsafe-fx= 0 (unsafe-fxand nbits1 nbits2))))
+
+(define (nbits-union nbits1 nbits2)
+  (unsafe-fxior nbits1 nbits2))
+
+(define (nbits-intersect nbits1 nbits2)
+  (unsafe-fxand nbits1 nbits2))
+
+(define (nbits-subtract nbits1 nbits2)
+  (unsafe-fxand nbits1 (unsafe-fxnot nbits2)))
+
+;; takes the bitwise representation of a union of numeric Base types
+;; and returns a list of the present Base types
+(define (nbits->base-types nbits)
+  (cond
+    [(eqv? 0 nbits) '()]
+    [else
+     (for*/fold ([acc '()])
+                ([low (in-range 0 numeric-count 8)]
+                 [high (in-value (min (+ low 8) numeric-count))]
+                 #:when (not (zero? (bitwise-bit-field nbits low high))))
+       (for/fold ([acc acc])
+                 ([idx (in-range low high)]
+                  #:when (bitwise-bit-set? nbits idx))
+         (cons (vector-ref numeric-atom-vector idx) acc)))]))
+
+
+(define-base-types
+  #:numeric? #t
+  ;; 30 bits is the max for a 2's complement 32-bit fixnum
+  ;; (since the numeric tower requires < 30 bits, we can
+  ;;  make that the max and use unsafe-fx ops for bit computations)
+  #:max-count 30
+  #:count numeric-count
+  #:atom-vector numeric-atom-vector
+  #:atom-hash numeric-atom-hash
+  #:atoms
+  [-Zero Zero #'(λ (n) (eq? n 0)) (λ (n) (eq? n 0))]
+  [-One One #'(λ (n) (eq? n 1)) (λ (n) (eq? n 1))]
+  [-Byte>1
+   Byte-Larger-Than-One
+   #'(λ (n) (and (byte? n) (> n 1)))
+   (λ (n) (and (byte? n) (> n 1)))]
+  [-PosIndexNotByte
+   Positive-Index-Not-Byte
+   #'(and/c index? positive? (not/c byte?))
+   (λ (x) (and (portable-index? x)
+               (positive? x)
+               (not (byte? x))))]
+  [-PosFixnumNotIndex
+   Positive-Fixnum-Not-Index
+   #'(and/c fixnum? positive? (not/c index?))
+   (λ (x) (and (portable-fixnum? x)
+               (positive? x)
+               (not (portable-index? x))))]
+  [-NegFixnum
+   Negative-Fixnum
+   #'(and/c fixnum? negative?)
+   (λ (x) (and (portable-fixnum? x)
+               (negative? x)))]
+  [-PosIntNotFixnum
+   Positive-Integer-Not-Fixnum
+   #'(and/c exact-integer? positive? (not/c fixnum?))
+   (λ (x) (and (exact-integer? x)
+               (positive? x)
+               (not (portable-fixnum? x))))]
+  [-NegIntNotFixnum
+   Negative-Integer-Not-Fixnum
+   #'(and/c exact-integer? negative? (not/c fixnum?))
+   (λ (x) (and (exact-integer? x)
+               (negative? x)
+               (not (portable-fixnum? x))))]
+  [-PosRatNotInt
+   Positive-Rational-Not-Integer
+   #'(and/c exact-rational? positive? (not/c integer?))
+   (λ (x) (and (exact-rational? x)
+               (positive? x)
+               (not (exact-integer? x))))]
+  [-NegRatNotInt
+   Negative-Rational-Not-Integer
+   #'(and/c exact-rational? negative? (not/c integer?))
+   (λ (x) (and (exact-rational? x)
+               (negative? x)
+               (not (exact-integer? x))))]
+  [-FlonumNan
+   Float-Nan
+   #'(and/c flonum? (lambda (x) (eqv? x +nan.0)))
+   (λ (x) (and (flonum? x) (eqv? x +nan.0)))]
+  [-FlonumPosZero
+   Float-Positive-Zero
+   #'(λ (x) (eqv? x 0.0))
+   (λ (x) (eqv? x 0.0))]
+  [-FlonumNegZero
+   Float-Negative-Zero
+   #'(λ (x) (eqv? x -0.0))
+   (λ (x) (eqv? x -0.0))]
+  [-PosFlonumNoNan
+   Positive-Float-No-NaN
+   #'(and/c flonum? positive?)
+   (λ (x) (and (flonum? x) (positive? x)))]
+  [-NegFlonumNoNan
+   Negative-Float-No-NaN
+   #'(and/c flonum? negative?)
+   (λ (x) (and (flonum? x) (negative? x)))]
+  [-SingleFlonumNan
+   Single-Flonum-Nan
+   #'(and/c single-flonum? (lambda (x) (eqv? x +nan.f)))
+   (λ (x) (and (single-flonum? x) (eqv? x +nan.f)))]
+  [-SingleFlonumPosZero ; disjoint from Flonum 0s
+   Single-Flonum-Positive-Zero
+   ;; eqv? equates 0.0f0 with itself, but not eq?
+   #'(λ (x) (eqv? x 0.0f0))
+   (λ (x) (eqv? x 0.0f0))]
+  [-SingleFlonumNegZero
+   Single-Flonum-Negative-Zero
+   #'(λ (x) (eqv? x -0.0f0))
+   (λ (x) (eqv? x -0.0f0))]
+  [-PosSingleFlonumNoNan
+   Positive-Single-Flonum-No-Nan
+   #'(and/c single-flonum? positive?)
+   (λ (x) (and (single-flonum? x) (positive? x)))]
+  [-NegSingleFlonumNoNan
+   Negative-Single-Flonum-No-Nan
+   #'(and/c single-flonum? negative?)
+   (λ (x) (and (single-flonum? x) (negative? x)))]
+  [-ExactImaginary
+   Exact-Imaginary
+   #'(and/c number?
+            (not/c real?)
+            (λ (x)
+              (and
+               (eqv? 0 (real-part x))
+               (exact? (imag-part x)))))
+   (λ (x) (and (number? x)
+               (not (real? x))
+               (eqv? 0 (real-part x))
+               (exact? (imag-part x))))]
+  [-ExactComplex
+   Exact-Complex
+   #'(and/c number?
+            (not/c real?)
+            (lambda (x)
+              (and
+               (not (eqv? 0 (real-part x)))
+               (exact? (real-part x))
+               (exact? (imag-part x)))))
+   (λ (x) (and (number? x)
+               (not (real? x))
+               (not (eqv? 0 (real-part x)))
+               (exact? (real-part x))
+               (exact? (imag-part x))))]
+  [-FloatImaginary
+   Float-Imaginary
+   #'(and/c number?
+            (λ (x)
+              (and (flonum? (imag-part x))
+                   (eqv? 0 (real-part x)))))
+   (λ (x)
+     (and (number? x)
+          (flonum? (imag-part x))
+          (eqv? 0 (real-part x))))]
+  [-SingleFlonumImaginary
+   Single-Flonum-Imaginary
+   #'(and/c number?
+            (λ (x)
+              (and (single-flonum? (imag-part x))
+                   (eqv? 0 (real-part x)))))
+   (λ (x)
+     (and (number? x)
+          (single-flonum? (imag-part x))
+          (eqv? 0 (real-part x))))]
+  [-FloatComplex
+   Float-Complex
+   #'(and/c number?
+            (lambda (x)
+              (and (flonum? (imag-part x))
+                   (flonum? (real-part x)))))
+   (λ (x)
+     (and (number? x)
+          (flonum? (imag-part x))
+          (flonum? (real-part x))))]
+  [-SingleFlonumComplex
+   Single-Flonum-Complex
+   #'(and/c number?
+            (λ (x)
+              (and (single-flonum? (imag-part x))
+                   (single-flonum? (real-part x)))))
+   (λ (x)
+     (and (number? x)
+          (single-flonum? (imag-part x))
+          (single-flonum? (real-part x))))])
diff --git a/typed-racket-lib/typed-racket/rep/rep-utils.rkt b/typed-racket-lib/typed-racket/rep/rep-utils.rkt
index 40bc5346..14562610 100644
--- a/typed-racket-lib/typed-racket/rep/rep-utils.rkt
+++ b/typed-racket-lib/typed-racket/rep/rep-utils.rkt
@@ -452,91 +452,3 @@
               mexpdr-def
               provides ...
               (provide uid-id)))]))]))
-
-
-;; macro for easily defining sets of types represented by fixnum bitfields
-(define-syntax (define-type-bitfield stx)
-  (define-syntax-class atoms-spec
-    (pattern [abbrev:id
-              name:id
-              contract:expr
-              predicate:expr]
-             #:with bits (format-id #'name "bits:~a" (syntax-e #'name))
-             #:with provide #'(provide bits)))
-  (define-syntax-class union-spec
-    (pattern [abbrev:id
-              name:id
-              contract:expr
-              predicate:expr
-              (elements:id ...)
-              (~optional (~and #:no-provide no-provide?))]
-             #:with bits (format-id #'name "bits:~a" (syntax-e #'name))
-             #:with provide #'(provide bits)))
-  (syntax-parse stx
-    [(_ #:atom-count atomic-type-count:id
-        #:atomic-type-vector atomic-type-vector:id
-        #:atomic-name-vector atomic-name-vector:id
-        #:name-hash name-hash:id
-        #:atomic-contract-vector atomic-contract-vector:id
-        #:contract-hash contract-hash:id
-        #:atomic-predicate-vector atomic-predicate-vector:id
-        #:predicate-hash predicate-hash:id
-        #:constructor-template (mk-bits:id) mk-expr:expr
-        #:atoms
-        atoms:atoms-spec ...
-        #:unions
-        unions:union-spec ...)
-     (define max-base-atomic-count 31) ;; this way we can do unsafe fx ops on any machine
-     (define atom-list (syntax->datum #'(atoms.name ...)))
-     (define atom-count (length atom-list))
-     (unless (<= atom-count max-base-atomic-count)
-       (raise-syntax-error
-        'define-type-bitfield
-        (format "too many atomic base types (~a is the max)"
-                max-base-atomic-count)
-        stx))
-     (with-syntax ([(n ... ) (range atom-count)]
-                   [(2^n ...)
-                    (build-list atom-count (λ (n) (arithmetic-shift 1 n)))])
-       #`(begin
-           ;; how many atomic types?
-           (define atomic-type-count #,atom-count)
-           ;; define the atomic types' bit identifiers (e.g. bits:Null)
-           (begin (define atoms.bits 2^n) ...)
-           ;; define the union types' bit identifiers
-           (begin (define unions.bits
-                    (bitwise-ior unions.elements ...))
-                  ...)
-           ;; define the actual type references (e.g. -Null)
-           (begin (define/decl atoms.abbrev
-                    (let ([mk-bits atoms.bits]) mk-expr)) ...)
-           (begin (define/decl unions.abbrev
-                    (let ([mk-bits unions.bits]) mk-expr)) ...)
-           ;; define the various vectors and hashes
-           (define atomic-type-vector
-             (vector-immutable atoms.abbrev ...))
-           (define atomic-name-vector
-             (vector-immutable (quote atoms.name) ...))
-           (define name-hash
-             (make-immutable-hasheqv
-              (list (cons atoms.bits (quote atoms.name)) ...
-                    (cons unions.bits (quote unions.name)) ...)))
-           (define atomic-contract-vector
-             (vector-immutable atoms.contract ...))
-           (define contract-hash
-             (make-immutable-hasheqv
-              (list
-               (cons atoms.bits atoms.contract)
-              ...
-              (cons unions.bits unions.contract)
-              ...)))
-           (define atomic-predicate-vector
-             (vector-immutable atoms.predicate ...))
-           (define predicate-hash
-             (make-immutable-hasheqv
-              (list
-               (cons atoms.bits atoms.predicate) ...
-               (cons unions.bits unions.predicate) ...)))
-           ;; provide the bit variables (e.g. bits:Null)
-           atoms.provide ...
-           unions.provide ...))]))
diff --git a/typed-racket-lib/typed-racket/rep/type-mask.rkt b/typed-racket-lib/typed-racket/rep/type-mask.rkt
index 8112ef93..57696d19 100644
--- a/typed-racket-lib/typed-racket/rep/type-mask.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-mask.rkt
@@ -30,7 +30,8 @@
          disjoint-masks?
          sub-mask?
          mask:bottom
-         mask:unknown)
+         mask:unknown
+         mask:base+number)
 
 (define-syntax OR (make-rename-transformer #'unsafe-fxior))
 (define-syntax AND (make-rename-transformer #'unsafe-fxand))
@@ -121,16 +122,7 @@
 ;; but which we are not specifically tracking
 
 (declare-type-flags
- ;; a few common base types have their own masks
- mask:null
- mask:true
- mask:false
- mask:char
- mask:symbol
- mask:void
- mask:string
- ;; the other base types use this catch-all
- mask:base-other
+ mask:base
  mask:number
  mask:pair
  mask:mpair
@@ -154,3 +146,5 @@
  mask:class
  mask:instance
  mask:unit)
+
+(define mask:base+number (mask-union mask:base mask:number))
diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt
index eae71e50..922eb5f3 100644
--- a/typed-racket-lib/typed-racket/rep/type-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt
@@ -6,22 +6,28 @@
 (require "../utils/utils.rkt")
 
 ;; TODO use contract-req
-(require (utils tc-utils hset)
+(require (utils tc-utils)
          "rep-utils.rkt"
          "core-rep.rkt"
          "values-rep.rkt"
          "type-mask.rkt"
-         "object-rep.rkt"
          "free-variance.rkt"
+         "base-type-rep.rkt"
+         "base-types.rkt"
+         "numeric-base-types.rkt"
+         "base-union.rkt"
          racket/match racket/list
          syntax/id-table
          racket/contract
+         racket/set
          racket/lazy-require
          (for-syntax racket/base
                      racket/syntax
                      syntax/parse))
 
-(provide (except-out (all-from-out "core-rep.rkt")
+(provide (except-out (all-from-out "core-rep.rkt"
+                                   "base-type-rep.rkt"
+                                   "base-union.rkt")
                      Type Prop Object PathElem SomeValues)
          Type?
          Mu-name:
@@ -40,12 +46,17 @@
          unfold
          Union?
          Union-elems
-         Union-map
+         Union-fmap
          Un
          resolvable?
+         Union-all:
+         Union-all-flat:
+         Union/set:
+         Intersection?
          (rename-out [instantiate instantiate-raw-type]
-                     [make-Union* make-Union]
                      [Union:* Union:]
+                     [Intersection:* Intersection:]
+                     [make-Intersection* make-Intersection]
                      [Class:* Class:]
                      [Class* make-Class]
                      [Row* make-Row]
@@ -130,33 +141,6 @@
    (f rator)
    (for-each f rands)])
 
-(define base-table (make-hasheq))
-
-;; name is a Symbol (not a Name)
-;; contract is used when generating contracts from types
-;; predicate is used to check (at compile-time) whether a value belongs
-;; to that base type. This is used to check for subtyping between value
-;; types and base types.
-;; numeric determines if the type is a numeric type
-(def-type Base ([name symbol?]
-                [contract syntax?]
-                [predicate procedure?]
-                [numeric? boolean?])
-  #:base 
-  [#:mask (match-lambda
-            [(Base: name _ _ numeric?)
-             (if numeric?
-                 mask:number
-                 (case name
-                   [(Char) mask:char]
-                   [(String) mask:string]
-                   [(Void) mask:void]
-                   [(Symbol) mask:symbol]
-                   [else mask:base-other]))])]
-  #:non-transparent
-  [#:custom-constructor
-   (hash-ref! base-table name (λ () (make-Base name contract predicate numeric?)))])
-
 
 ;;************************************************************
 ;; Structural Types
@@ -425,7 +409,9 @@
   [#:custom-constructor
    (cond
      [(Bottom? body) -Bottom]
-     [(or (Value? body) (Base? body)) body]
+     [(or (Base? body)
+          (BaseUnion? body))
+      body]
      [else (make-Mu body)])])
 
 ;; n is how many variables are bound here
@@ -605,104 +591,219 @@
   #:base
   [#:mask (λ (t) (match (Value-val t)
                    [(? number?) mask:number]
-                   [#t mask:true]
-                   [#f mask:false]
-                   [(? symbol?) mask:symbol]
-                   [(? string?) mask:string]
-                   [(? char?) mask:char]
-                   [(? null?) mask:null]
-                   [(? void?) mask:void]
-                   [_ mask:unknown]))])
+                   [(? symbol?) mask:base]
+                   [(? string?) mask:base]
+                   [(? char?) mask:base]
+                   [_ mask:unknown]))]
+  [#:custom-constructor
+   (match val
+     [#f -False]
+     [#t -True]
+     ['() -Null]
+     [(? void?) -Void]
+     [0 -Zero]
+     [1 -One]
+     [_ (make-Value val)])])
 
-;; elems : Listof[Type]
+;; mask - cached type mask
+;; base - any Base types, or Bottom if none are present
+;; ts - the list of types in the union (contains no duplicates,
+;; gives us deterministic iteration order)
+;; elems - the set equivalent of 'ts', useful for equality
+;; and constant time membership tests
+;; NOTE: The types contained in a union have had complicated
+;; invariants in the past. Currently, we are using a few simple
+;; guidelines:
+;; 1. Unions do not contain duplicate types
+;; 2. Unions do not contain Univ or Bottom
+;; 3. Unions do not contain 'Base' or 'BaseUnion'
+;;    types outside of the 'base' field.
+;; That's it -- we may contain some redundant types,
+;; but in general its quicker to not worry about those
+;; until we're printing to the user or generating contracts,
+;; at which point the 'normalize-type' function from 'types/union.rkt'
+;; is used to remove overlapping types from unions.
 (def-type Union ([mask type-mask?]
-                 [elems (and/c (hsetof Type?)
-                               (λ (h) (zero? (hset-count h))))])
+                 [base (or/c Bottom? Base? BaseUnion?)]
+                 [ts (cons/c Type? (cons/c Type? (listof Type?)))]
+                 [elems (and/c (set/c Type?)
+                               (λ (h) (> (set-count h) 1)))])
   #:no-provide
-  [#:frees (f) (combine-frees (hset-map elems f))]
-  [#:fmap (f) (Union-map elems f)]
-  [#:for-each (f) (hset-for-each elems f)]
-  [#:mask (λ (t) (Union-mask t))])
+  #:non-transparent
+  [#:frees (f) (combine-frees (map f ts))]
+  [#:fmap (f) (Union-fmap f base ts)]
+  [#:for-each (f) (for-each f ts)]
+  [#:mask (λ (t) (Union-mask t))]
+  [#:custom-constructor
+   ;; make sure we do not build Unions equivalent to
+   ;; Bottom, a single BaseUnion, or a single type
+   (cond
+     [(set-member? elems Univ) Univ]
+     [else
+      (set-remove! elems -Bottom)
+      (match (set-count elems)
+        [0 base]
+        [1 #:when (Bottom? base) (set-first elems)]
+        [_ (intern-double-ref!
+            union-intern-table
+            elems
+            base
+            ;; now, if we need to build a new union, remove duplicates from 'ts'
+            #:construct (make-Union mask base (remove-duplicates ts) elems))])])])
 
+(define union-intern-table (make-weak-hash))
+
+;; Custom match expanders for Union that expose various
+;; components or combinations of components
 (define-match-expander Union:*
-  (syntax-rules () [(_ elems-pat) (Union: _ elems-pat)]))
+  (syntax-rules () [(_ b ts) (Union: _ b ts _)]))
 
-(define build-union
-  (let ([union-intern-table (make-weak-hash)])
-    (λ (m ts)
-      (cond
-        [(hset-member? ts Univ) Univ]
-        [else
-         (let ([ts (hset-remove ts -Bottom)])
-           (case (hset-count ts)
-             [(0) -Bottom]
-             [(1) (hset-first ts)]
-             [else (ephemeron-value
-                    (hash-ref! union-intern-table ts
-                               (λ () (let ([t (make-Union m ts)])
-                                       (make-ephemeron ts t)))))]))]))))
+(define-match-expander Union/set:
+  (syntax-rules () [(_ b ts elems) (Union: _ b ts elems)]))
 
-;; Union-map
+(define-match-expander Union-all:
+  (syntax-rules () [(_ elems) (app Union-all-list? (? list? elems))]))
+
+(define-match-expander Union-all-flat:
+  (syntax-rules () [(_ elems) (app Union-all-flat-list? (? list? elems))]))
+
+;; returns all of the elements of a Union (sans Bottom),
+;; and any BaseUnion is left in tact
+;; if a non-Union is passed, returns #f
+(define (Union-all-list? t)
+  (match t
+    [(Union: _ (? Bottom? b) ts _) ts]
+    [(Union: _ b ts _) (cons b ts)]
+    [_ #f]))
+
+;; returns all of the elements of a Union (sans Bottom),
+;; and any BaseUnion is flattened into the atomic Base elements
+;; if a non-Union is passed, returns #f
+(define (Union-all-flat-list? t)
+  (match t
+    [(Union: _ b ts _)
+     (match b
+       [(? Bottom?) ts]
+       [(BaseUnion-bases: bs) (append bs ts)]
+       [_ (cons b ts)])]
+    [_ #f]))
+
+;; Union-fmap
 ;;
-;; maps function 'f' over hashet 'args', producing a Union
-;; Note: this is the core constructor for all Unions!
-;; Unions are interned according to their element set,
-;; but in a way which does not leak memory (i.e. Unions which
-;; are no longer referenced outside of the interning machinery
-;; will be garbage collected)
-(define/cond-contract (Union-map args f)
-  (-> (hsetof Type?) procedure? Type?)
-  (define-values (m ts)
-    (for*/fold ([m mask:bottom] [ts (hset)])
-               ([arg (in-hset args)]
-                [arg (in-value (f arg))])
+;; maps function 'f' over 'base-arg' and 'args', producing a Union
+;; of all of the arguments.
+;;
+;; This is often used in functions that walk over and rebuild types
+;; in the following form:
+;; (match t
+;;  [(Union: b ts) (Union-fmap f b ts)]
+;;  ...)
+;;
+;; Note: this is also the core constructor for all Unions!
+(define/cond-contract (Union-fmap f base-arg args)
+  (-> procedure? (or/c Bottom? Base? BaseUnion?) (listof Type?) Type?)
+  ;; these fields are destructively updated during this process
+  (define m mask:bottom)
+  (define bbits #b0)
+  (define nbits #b0)
+  (define ts '())
+  (define elems (mutable-set))
+  ;; process a Base element
+  (define (process-base! numeric? bits)
+    (cond
+      [numeric? (set! nbits (nbits-union nbits bits))]
+      [else (set! bbits (bbits-union bbits bits))]))
+  ;; process a BaseUnion element
+  (define (process-base-union! bbits* nbits*)
+    (set! nbits (nbits-union nbits nbits*))
+    (set! bbits (bbits-union bbits bbits*)))
+  ;; process a type from the 'base' field of a Union
+  (define (process-any-base! b)
+    (match b
+      [(Base-bits: numeric? bits) (process-base! numeric? bits)]
+      [(BaseUnion: bbits* nbits*) (process-base-union! bbits* nbits*)]
+      ;; else Bottom
+      [_ (void)]))
+  ;; process a list of types
+  (define (process! args)
+    (for* ([arg (in-list args)]
+           [arg (in-value (f arg))])
       (match arg
-        [(Union: m* ts*)
-         (values (mask-union m m*)
-                 (hset-union ts ts*))]
-        [_ (values
-            (mask-union m (mask arg))
-            (hset-add ts arg))])))
-  (build-union m ts))
+        [(Base-bits: numeric? bits) (process-base! numeric? bits)]
+        [(BaseUnion: bbits* nbits*) (process-base-union! bbits* nbits*)]
+        [(Union: m* b* ts* _)
+         (set! m (mask-union m m*))
+         (process-any-base! b*)
+         (set! ts (append ts* ts))
+         (for ([t* (in-list ts*)])
+           (set-add! elems t*))]
+        [_ (set! m (mask-union m (mask arg)))
+           (set! ts (cons arg ts))
+           (set-add! elems arg)])))
+  ;; process the input arguments
+  (process-any-base! (f base-arg))
+  (process! args)
+  ;; construct a BaseUnion (or Base or Bottom) based on the
+  ;; Base data gathered during processing
+  (define bs (make-BaseUnion bbits nbits))
+  ;; call the Union smart constructor
+  (make-Union (mask-union m (mask bs))
+              bs
+              ts
+              elems))
 
 (define (Un . args)
-  (Union-map (list->hset args) values))
-
-(define (make-Union* args)
-  (Union-map args values))
+  (Union-fmap (λ (x) x) -Bottom args))
 
 ;; Intersection
-(def-type Intersection ([elems (and/c (hsetof Type?)
-                                      (λ (h) (zero? (hset-count h))))])
-  [#:frees (f) (combine-frees (hset-map elems f))]
-  [#:fmap (f) (apply -unsafe-intersect (hset-map elems f))]
-  [#:for-each (f) (hset-for-each elems f)]
+;; ts - the list of types (gives deterministic behavior)
+;; elems - the set equivalent of 'ts', useful for equality tests
+(def-type Intersection ([ts (cons/c Type? (cons/c Type? (listof Type?)))]
+                        [elems (set/c Type?)])
+  #:non-transparent
+  #:no-provide
+  [#:frees (f) (combine-frees (map f ts))]
+  [#:fmap (f) (apply -unsafe-intersect (map f ts))]
+  [#:for-each (f) (for-each f ts)]
   [#:mask (λ (t) (for/fold ([m mask:unknown])
-                           ([elem (in-hset (Intersection-elems t))])
-                   (mask-intersect m (mask elem))))])
+                           ([elem (in-list (Intersection-ts t))])
+                   (mask-intersect m (mask elem))))]
+  [#:custom-constructor
+   (intern-single-ref! intersection-table
+                       elems
+                       #:construct (make-Intersection ts elems))])
+
+(define intersection-table (make-weak-hash))
+
+(define-match-expander Intersection:*
+  (syntax-rules () [(_ ts) (Intersection: ts _)]))
+
+(define (make-Intersection* ts)
+  (apply -unsafe-intersect ts))
 
 ;;  constructor for intersections
 ;; in general, intersections should be built
 ;; using the 'intersect' operator, which worries
 ;; about actual subtyping, etc...
 (define (-unsafe-intersect . ts)
-  (let loop ([elems (hset)]
+  (let loop ([elems (set)]
              [ts ts])
     (match ts
       [(list)
-       (cond
-         [(hset-empty? elems) Univ]
-         ;; size = 1 ?
-         [(= 1 (hset-count elems)) (hset-first elems)]
-         ;; size > 1, build an intersection
-         [else (make-Intersection elems)])]
+       (let ([ts (set->list elems)])
+         (cond
+           [(null? ts) Univ]
+           ;; size = 1 ?
+           [(null? (cdr ts)) (car ts)]
+           ;; size > 1, build an intersection
+           [else (make-Intersection ts elems)]))]
       [(cons t ts)
        (match t
          [(Univ:) (loop elems ts)]
-         [(Intersection: ts*) (loop elems (append (hset->list ts*) ts))]
-         [_ #:when (for/or ([elem (in-hset elems)]) (not (overlap? elem t)))
+         [(Intersection: ts* _) (loop elems (append ts* ts))]
+         [_ #:when (for/or ([elem (in-immutable-set elems)]) (not (overlap? elem t)))
             -Bottom]
-         [_ (loop (hset-add elems t) ts)])])))
+         [_ (loop (set-add elems t) ts)])])))
 
 
 (def-type Refinement ([parent Type?] [pred identifier?])
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-eq.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-eq.rkt
index 68e05d99..44243327 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-eq.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-eq.rkt
@@ -5,7 +5,7 @@
          "utils.rkt"
          syntax/parse syntax/stx racket/match
          (typecheck signatures tc-funapp)
-         (types abbrev prop-ops utils)
+         (types abbrev prop-ops utils match-expanders)
          (rep type-rep object-rep)
 
          (for-label racket/base racket/bool))
@@ -53,23 +53,23 @@
         (alt eqv? eqv?-able)
         (alt equal? equal?-able)))
   (match* ((single-value v1) (single-value v2))
-    [((tc-result1: (Value: (? ok? val1)) _ o1)
-      (tc-result1: (Value: (? ok? val2)) _ o2))
+    [((tc-result1: (Val-able: (? ok? val1)) _ o1)
+      (tc-result1: (Val-able: (? ok? val2)) _ o2))
      (ret -Boolean (-PS (-and (-is-type o1 (-val val2))
                               (-is-type o2 (-val val1)))
                         (-and (-not-type o1 (-val val2))
                               (-not-type o2 (-val val1)))))]
-    [((tc-result1: t _ o) (tc-result1: (Value: (? ok? val))))
+    [((tc-result1: t _ o) (tc-result1: (Val-able: (? ok? val))))
      (ret -Boolean (-PS (-is-type o (-val val)) (-not-type o (-val val))))]
-    [((tc-result1: (Value: (? ok? val))) (tc-result1: t _ o))
+    [((tc-result1: (Val-able: (? ok? val))) (tc-result1: t _ o))
      (ret -Boolean (-PS (-is-type o (-val val)) (-not-type o (-val val))))]
     [((tc-result1: t _ o)
       (or (and (? (lambda _ (id=? #'member comparator)))
-               (tc-result1: (List: (list (and ts (Value: _)) ...))))
+               (tc-result1: (List: (list (and ts (Val-able: _)) ...))))
           (and (? (lambda _ (id=? #'memv comparator)))
-               (tc-result1: (List: (list (and ts (Value: (? eqv?-able))) ...))))
+               (tc-result1: (List: (list (and ts (Val-able: (? eqv?-able))) ...))))
           (and (? (lambda _ (id=? #'memq comparator)))
-               (tc-result1: (List: (list (and ts (Value: (? eq?-able))) ...))))))
+               (tc-result1: (List: (list (and ts (Val-able: (? eq?-able))) ...))))))
      (let ([ty (apply Un ts)])
        (ret (Un (-val #f) t)
             (-PS (-is-type o ty)
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt
index 35c54013..f4ab20be 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt
@@ -1,11 +1,11 @@
 #lang racket/unit
 
 (require "../../utils/utils.rkt"
-         (utils hset)
          syntax/parse syntax/stx racket/match racket/sequence
          "signatures.rkt"
          "utils.rkt"
-         (types utils abbrev numeric-tower resolve type-table generalize)
+         (types utils abbrev numeric-tower resolve type-table
+                generalize match-expanders)
          (typecheck signatures check-below)
          (rep type-rep type-mask rep-utils)
          (for-label racket/unsafe/ops racket/base))
@@ -30,7 +30,7 @@
       (syntax-e #'i))]
    [_
     (match (tc-expr expr)
-     [(tc-result1: (Value: (? number? i))) i]
+     [(tc-result1: (Val-able: (? number? i))) i]
      [tc-results
        (check-below tc-results (ret -Integer))
        #f])]))
@@ -127,8 +127,8 @@
       ;; of the union that are vectors.  If there's only one of those,
       ;; we re-run this whole algorithm with that.  Otherwise, we treat
       ;; it like any other expected type.
-      [(tc-result1: (app resolve (Union: ts))) (=> continue)
-       (define u-ts (for/list ([t (in-hset ts)]
+      [(tc-result1: (app resolve (Union: _ ts))) (=> continue)
+       (define u-ts (for/list ([t (in-list ts)]
                                #:when (eq? mask:vector (mask t)))
                       t))
        (match u-ts
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-keywords.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-keywords.rkt
index 2183ec8a..ef25b4bb 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-keywords.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-keywords.rkt
@@ -133,7 +133,7 @@
   (match t
     [(Pair: (Value: (? keyword? k)) b)
      (cons k (type->list b))]
-    [(Value: '()) null]
+    [(? Base:Null?) null]
     [_ (int-err "bad value in type->list: ~a" t)]))
 
 
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt b/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
index b5955c1e..0e74152e 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
@@ -1,7 +1,6 @@
 #lang racket/base
 
 (require (rename-in "../utils/utils.rkt" [infer r:infer])
-         (utils hset)
          racket/match racket/list
          (prefix-in c: (contract-req))
          (env tvar-env)
@@ -170,9 +169,9 @@
       [(? resolvable?)
        (tc/funapp f-stx args-stx (resolve-once f-type) args-res expected)]
       ;; a union of functions can be applied if we can apply all of the elements
-      [(Union: ts) #:when (for/and ([t (in-hset ts)]) (Function? t))
+      [(Union: (? Bottom?) ts) #:when (andmap Function? ts)
        (merge-tc-results
-        (for/list ([fty (in-hset ts)])
+        (for/list ([fty (in-list ts)])
           (tc/funapp f-stx args-stx fty args-res expected)))]
       ;; bottom or error type is a perfectly good fcn type
       [(or (Bottom:) (Error:)) (ret f-type)]
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-send.rkt b/typed-racket-lib/typed-racket/typecheck/tc-send.rkt
index f10842e3..12333de8 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-send.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-send.rkt
@@ -9,7 +9,7 @@
          (typecheck signatures tc-funapp tc-metafunctions)
          (types base-abbrev resolve utils type-table)
          (rep type-rep)
-         (utils tc-utils hset)
+         (utils tc-utils)
          (for-template racket/base))
 
 (import tc-expr^)
@@ -41,8 +41,8 @@
          [_ (int-err "non-symbol methods not supported by Typed Racket: ~a"
                      rcvr-type)])]
       ;; union of objects, check pointwise and union the results
-      [(Union: objs) #:when (for/and ([t (in-hset objs)]) (Instance? t))
-       (merge-tc-results (hset-map objs do-check))]
+      [(Union: (? Bottom?) objs) #:when (andmap Instance? objs)
+       (merge-tc-results (map do-check objs))]
       [_ (tc-error/expr/fields
           "send: type mismatch"
           "expected" "an object"
diff --git a/typed-racket-lib/typed-racket/types/abbrev.rkt b/typed-racket-lib/typed-racket/types/abbrev.rkt
index 9c3d0ec7..83af25ae 100644
--- a/typed-racket-lib/typed-racket/types/abbrev.rkt
+++ b/typed-racket-lib/typed-racket/types/abbrev.rkt
@@ -12,8 +12,7 @@
          racket/function
 
          (prefix-in c: (contract-req))
-         (rename-in (rep rep-utils type-rep prop-rep object-rep values-rep)
-                    [make-Base make-Base*])
+         (rep rep-utils type-rep prop-rep object-rep values-rep)
          (types numeric-tower prefab)
          ;; Using this form so all-from-out works
          "base-abbrev.rkt" "match-expanders.rkt"
@@ -49,13 +48,9 @@
          (only-in racket/future fsemaphore?)
          (only-in '#%place place? place-channel?))
 
-(provide (except-out (all-defined-out) make-Base)
+(provide (all-defined-out)
          (except-out (all-from-out "base-abbrev.rkt" "match-expanders.rkt") make-arr))
 
-;; All the types defined here are not numeric
-(define (make-Base name contract predicate)
-  (make-Base* name contract predicate #f))
-
 ;; Convenient constructors
 (define -App make-App)
 (define -mpair make-MPair)
@@ -86,10 +81,6 @@
 
 (define (-ne-lst t) (-pair t (-lst t)))
 
-;; For casted-exprs in unreachable code, to fill in the cast table.
-;; TODO: This contract normally gets optimized away. Is there away to stop that?
-(define -Dead-Code (make-Base 'Dead-Code #'(make-none/c 'dead-code/c) (λ (v) #f)))
-
 ;; Convenient constructor for Values
 ;; (wraps arg types with Result)
 (define/cond-contract (-values args)
@@ -107,29 +98,9 @@
 
 ;; Basic types
 (define -Listof (-poly (list-elem) (make-Listof list-elem)))
-(define/decl -Undefined
-  (make-Base 'Undefined
-             #'(lambda (x) (eq? x undefined))
-             (lambda (x) (eq? x undefined))))
-(define/decl -Bytes (make-Base 'Bytes #'bytes? bytes?))
-(define/decl -Base-Regexp (make-Base 'Base-Regexp
-                           #'(and/c regexp? (not/c pregexp?))
-                           (conjoin regexp? (negate pregexp?))))
-(define/decl -PRegexp (make-Base 'PRegexp
-				 #'pregexp?
-				 pregexp?))
 (define/decl -Regexp (Un -PRegexp -Base-Regexp))
-(define/decl -Byte-Base-Regexp
-  (make-Base 'Byte-Base-Regexp
-	     #'(and/c byte-regexp? (not/c byte-pregexp?))
-	     (conjoin byte-regexp? (negate byte-pregexp?))))
-(define/decl -Byte-PRegexp
-  (make-Base 'Byte-PRegexp #'byte-pregexp? byte-pregexp?))
 (define/decl -Byte-Regexp (Un -Byte-Base-Regexp -Byte-PRegexp))
 (define/decl -Pattern (Un -Bytes -Regexp -Byte-Regexp -String))
-(define/decl -Keyword (make-Base 'Keyword #'keyword? keyword?))
-(define/decl -Thread (make-Base 'Thread #'thread? thread?))
-(define/decl -Path (make-Base 'Path #'path? path?))
 (define/decl -Module-Path
   (-mu X
        (Un -Symbol -String -Path
@@ -148,27 +119,7 @@
                                                  -Nat)))))))
            (-lst* (-val 'submod) X
                   #:tail (-lst (Un -Symbol (-val "..")))))))
-(define/decl -Resolved-Module-Path (make-Base 'Resolved-Module-Path #'resolved-module-path? resolved-module-path?))
-(define/decl -Module-Path-Index (make-Base 'Module-Path-Index #'module-path-index? module-path-index?))
-(define/decl -Compiled-Module-Expression (make-Base 'Compiled-Module-Expression #'compiled-module-expression? compiled-module-expression?))
-(define/decl -Compiled-Non-Module-Expression
-  (make-Base 'Compiled-Non-Module-Expression
-             #'(and/c    compiled-expression? (not/c  compiled-module-expression?))
-	     (conjoin  compiled-expression? (negate compiled-module-expression?))))
 (define/decl -Compiled-Expression (Un -Compiled-Module-Expression -Compiled-Non-Module-Expression))
-(define/decl -Cont-Mark-Set (make-Base 'Continuation-Mark-Set #'continuation-mark-set? continuation-mark-set?))
-(define/decl -OtherSystemPath
-  (make-Base 'OtherSystemPath
-	     #'(and/c path-for-some-system? (not/c path?))
-	     (conjoin path-for-some-system? (negate path?))))
-(define/decl -Namespace (make-Base 'Namespace #'namespace? namespace?))
-(define/decl -Output-Port (make-Base 'Output-Port #'output-port? output-port?))
-(define/decl -Input-Port (make-Base 'Input-Port #'input-port? input-port?))
-(define/decl -TCP-Listener (make-Base 'TCP-Listener #'tcp-listener? tcp-listener?))
-(define/decl -UDP-Socket (make-Base 'UDP-Socket #'udp? udp?))
-(define/decl -FlVector (make-Base 'FlVector #'flvector? flvector?))
-(define/decl -ExtFlVector (make-Base 'ExtFlVector #'extflvector? extflvector?))
-(define/decl -FxVector (make-Base 'FxVector #'fxvector? fxvector?))
 ;; in the type (-Syntax t), t is the type of the result of syntax-e, not syntax->datum
 (define -Syntax make-Syntax)
 (define/decl In-Syntax
@@ -203,47 +154,16 @@
 (define/decl -SomeSystemPathlike*
   (Un -String -SomeSystemPath(-val 'up) (-val 'same)))
 (define/decl -PathConventionType (Un (-val 'unix) (-val 'windows)))
-(define/decl -Pretty-Print-Style-Table
-  (make-Base 'Pretty-Print-Style-Table #'pretty-print-style-table? pretty-print-style-table?))
-(define/decl -Read-Table
-  (make-Base 'Read-Table #'readtable? readtable?))
-(define/decl -Special-Comment
-  (make-Base 'Special-Comment #'special-comment? special-comment?))
-(define/decl -Custodian (make-Base 'Custodian #'custodian? custodian?))
-(define/decl -Parameterization (make-Base 'Parameterization #'parameterization? parameterization?))
-(define/decl -Inspector (make-Base 'Inspector #'inspector? inspector?))
-(define/decl -Namespace-Anchor (make-Base 'Namespace-Anchor #'namespace-anchor? namespace-anchor?))
-(define/decl -Variable-Reference (make-Base 'Variable-Reference #'variable-reference? variable-reference?))
-(define/decl -Internal-Definition-Context
-  (make-Base 'Internal-Definition-Context
-	     #'internal-definition-context?
-	     internal-definition-context?))
-(define/decl -Subprocess
-  (make-Base 'Subprocess #'subprocess? subprocess?))
-(define/decl -Security-Guard
-  (make-Base 'Security-Guard #'security-guard? security-guard?))
-(define/decl -Thread-Group
-  (make-Base 'Thread-Group #'thread-group? thread-group?))
-(define/decl -Struct-Type-Property
-  (make-Base 'Struct-Type-Property #'struct-type-property? struct-type-property?))
-(define/decl -Impersonator-Property
-  (make-Base 'Impersonator-Property #'impersonator-property? impersonator-property?))
-(define/decl -Semaphore (make-Base 'Semaphore #'semaphore? semaphore?))
-(define/decl -FSemaphore (make-Base 'FSemaphore #'fsemaphore? fsemaphore?))
-(define/decl -Bytes-Converter (make-Base 'Bytes-Converter #'bytes-converter? bytes-converter?))
-(define/decl -Pseudo-Random-Generator
-  (make-Base 'Pseudo-Random-Generator #'pseudo-random-generator? pseudo-random-generator?))
-(define/decl -Logger (make-Base 'Logger #'logger? logger?))
-(define/decl -Log-Receiver (make-Base 'LogReceiver #'log-receiver? log-receiver?))
 (define/decl -Log-Level (one-of/c 'fatal 'error 'warning 'info 'debug))
-(define/decl -Place (make-Base 'Place #'place? place?))
-(define/decl -Base-Place-Channel
-  (make-Base 'Base-Place-Channel #'(and/c place-channel? (not/c place?))  (conjoin place-channel? (negate place?))))
 (define/decl -Place-Channel (Un -Place -Base-Place-Channel))
-(define/decl -Will-Executor
-  (make-Base 'Will-Executor #'will-executor? will-executor?))
-(define/decl -Environment-Variables
-  (make-Base 'Environment-Variables #'environment-variables? environment-variables?))
+
+;; note, these are number? #f
+(define/decl -ExtFlonumZero (Un -ExtFlonumPosZero -ExtFlonumNegZero -ExtFlonumNan))
+(define/decl -PosExtFlonum (Un -PosExtFlonumNoNan -ExtFlonumNan))
+(define/decl -NonNegExtFlonum (Un -PosExtFlonum -ExtFlonumZero))
+(define/decl -NegExtFlonum (Un -NegExtFlonumNoNan -ExtFlonumNan))
+(define/decl -NonPosExtFlonum (Un -NegExtFlonum -ExtFlonumZero))
+(define/decl -ExtFlonum (Un -NegExtFlonumNoNan -ExtFlonumNegZero -ExtFlonumPosZero -PosExtFlonumNoNan -ExtFlonumNan))
 
 ;; Type alias names
 (define (-struct-name name)
diff --git a/typed-racket-lib/typed-racket/types/base-abbrev.rkt b/typed-racket-lib/typed-racket/types/base-abbrev.rkt
index b6538aff..a9a1bfd3 100644
--- a/typed-racket-lib/typed-racket/types/base-abbrev.rkt
+++ b/typed-racket-lib/typed-racket/types/base-abbrev.rkt
@@ -7,6 +7,8 @@
 
 (require "../utils/utils.rkt"
          "../rep/type-rep.rkt"
+         "../rep/base-types.rkt"
+         "../rep/numeric-base-types.rkt"
          (rep prop-rep object-rep values-rep rep-utils)
          (env mvar-env)
          racket/match racket/list (prefix-in c: (contract-req))
@@ -18,7 +20,9 @@
          -is-type
          -not-type
          -id-path
-         (all-from-out "../rep/type-rep.rkt")
+         (all-from-out "../rep/type-rep.rkt"
+                       "../rep/base-types.rkt"
+                       "../rep/numeric-base-types.rkt")
          (rename-out [make-Listof -lst]
                      [make-MListof -mlst]))
 
@@ -32,25 +36,16 @@
                -Bottom
                (mk t ...)))))]))
 
-(define/decl -False (make-Value #f))
-(define/decl -True (make-Value #t))
+
 (define/decl -Boolean (Un -False -True))
 
 (define -val make-Value)
 (define/decl -Null (-val null))
 
 ;; Char type and List type (needed because of how sequences are checked in subtype)
-(define/decl -Char (make-Base 'Char #'char? char? #f))
 (define (make-Listof elem) (-mu list-rec (Un -Null (make-Pair elem list-rec))))
 (define (make-MListof elem) (-mu list-rec (Un -Null (make-MPair elem list-rec))))
 
-;; Needed for evt checking in subtype.rkt
-(define/decl -Symbol (make-Base 'Symbol #'symbol? symbol? #f))
-(define/decl -String (make-Base 'String #'string? string? #f))
-
-;; Void is needed for Params
-(define/decl -Void (make-Base 'Void #'void? void? #f))
-
 ;; -Tuple Type is needed by substitute for ListDots
 (define -pair make-Pair)
 (define (-lst* #:tail [tail -Null] . args)
diff --git a/typed-racket-lib/typed-racket/types/generalize.rkt b/typed-racket-lib/typed-racket/types/generalize.rkt
index 96ad346c..34ed1b6b 100644
--- a/typed-racket-lib/typed-racket/types/generalize.rkt
+++ b/typed-racket-lib/typed-racket/types/generalize.rkt
@@ -14,8 +14,8 @@
   (let/ec exit
     (let loop ([t* t])
       (match t*
-        [(Value: '()) (-lst Univ)]
-        [(Value: 0) -Int]
+        [(== -Null) (-lst Univ)]
+        [(== -Zero) -Int]
         [(List: ts) (-lst (apply Un ts))]
         [(? (lambda (t) (subtype t -Bottom))) Univ]
         [(? (lambda (t) (subtype t -Int))) -Int]
@@ -30,8 +30,8 @@
         [(? (lambda (t) (subtype t -Number))) -Number]
         [(? (lambda (t) (subtype t -ExtFlonum))) -ExtFlonum]
         [(Listof: _) t*]
-        [(Pair: t1 (Value: '())) (-lst t1)]
-        [(MPair: t1 (Value: '())) (-mlst t1)]
+        [(Pair: t1 (== -Null)) (-lst t1)]
+        [(MPair: t1 (== -Null)) (-mlst t1)]
         [(or (Pair: t1 t2) (MPair: t1 t2))
          (let ([t-new (loop t2)])
            (define -lst-type
@@ -39,10 +39,10 @@
                 [(Pair: _ _) -lst]
                 [(MPair: _ _) -mlst])
               t1))
-           (if (type-compare? -lst-type t-new)
+           (if (type-equiv? -lst-type t-new)
                -lst-type
                (exit t)))]
         [(ListDots: t bound) (-lst (substitute Univ bound t))]
         [(? (lambda (t) (subtype t -Symbol))) -Symbol]
-        [(Value: #t) -Boolean]
+        [(== -True) -Boolean]
         [_ t*]))))
diff --git a/typed-racket-lib/typed-racket/types/match-expanders.rkt b/typed-racket-lib/typed-racket/types/match-expanders.rkt
index 8ec49c3a..a2d94ae1 100644
--- a/typed-racket-lib/typed-racket/types/match-expanders.rkt
+++ b/typed-racket-lib/typed-racket/types/match-expanders.rkt
@@ -1,18 +1,40 @@
 #lang racket/base
 
 (require "../utils/utils.rkt"
-         (utils hset)
          (rep type-rep values-rep rep-utils)
          racket/match
          syntax/parse/define
+         racket/set
          (types resolve base-abbrev)
          (for-syntax racket/base syntax/parse))
 
 (provide Listof: List: MListof: AnyPoly: AnyPoly-names: Function/arrs:
          SimpleListof: SimpleMListof:
-         PredicateProp:)
+         PredicateProp:
+         Val-able:)
 
 
+;; some types used to be represented by a Value rep,
+;; but are now represented by a Base rep. This function
+;; helps us recover the singleton values for those types.
+(define (Base->val? b)
+  (match b
+    [(== -Null) (box-immutable '())]
+    [(== -Void) (box-immutable (void))]
+    [(== -True) (box-immutable #t)]
+    [(== -False) (box-immutable #f)]
+    [(== -Zero) (box-immutable 0)]
+    [(== -One) (box-immutable 1)]
+    [_ #f]))
+
+(define-match-expander Val-able:
+  (lambda (stx)
+    (syntax-parse stx
+      [(_ pat)
+       (syntax/loc stx
+         (or (Value: pat)
+             (app Base->val? (box pat))))])))
+
 (define-match-expander Listof:
   (lambda (stx)
     (syntax-parse stx
@@ -31,26 +53,18 @@
 (define-simple-macro (make-Listof-pred listof-pred?:id pair-matcher:id)
   (define (listof-pred? t [simple? #f])
     (match t
-      [(Mu-unsafe: (Union: elems))
-       #:when (and (= 2 (hset-count elems))
-                   (hset-member? elems -Null))
-       (match (hset-first (hset-remove elems -Null))
-         [(pair-matcher elem-t (B: 0))
-          (define elem-t* (instantiate-raw-type t elem-t))
-          (cond
-            [simple? (and (equal? elem-t elem-t*) elem-t)]
-            [else elem-t*])]
-         [_ #f])]
-      [(Union: elems)
-       #:when (and (= 2 (hset-count elems))
-                   (hset-member? elems -Null))
-       (match (hset-first (hset-remove elems -Null))
-         [(pair-matcher hd-t tl-t)
-          (cond
-            [(listof-pred? tl-t)
-             => (λ (lst-t) (and (equal? hd-t lst-t) hd-t))]
-            [else #f])]
-         [_ #f])]
+      [(Mu-unsafe:
+        (Union: (== -Null)
+                (list (pair-matcher elem-t (B: 0)))))
+       (define elem-t* (instantiate-raw-type t elem-t))
+       (cond
+         [simple? (and (equal? elem-t elem-t*) elem-t)]
+         [else elem-t*])]
+      [(Union: (== -Null) (list (pair-matcher hd-t tl-t)))
+       (cond
+         [(listof-pred? tl-t)
+          => (λ (lst-t) (and (equal? hd-t lst-t) hd-t))]
+         [else #f])]
       [_ #f])))
 
 (make-Listof-pred Listof? Pair:)
@@ -62,7 +76,7 @@
   (lambda (stx)
     (syntax-parse stx
       [(_ elem-pats)
-       #'(? Type? (app untuple (? values elem-pats) (Value: '())))]
+       #'(? Type? (app untuple (? values elem-pats) (== -Null)))]
       [(_ elem-pats #:tail tail-pat)
        #'(? Type? (app untuple (? values elem-pats) tail-pat))])))
 
@@ -84,11 +98,11 @@
 ;; The last type may contain pairs if it is a list type.
 (define (untuple t)
   (let loop ([t t]
-             [seen (hset)])
-    (if (not (hset-member? seen t))
+             [seen (set)])
+    (if (not (set-member? seen t))
         (match (resolve t)
           [(Pair: a b)
-           (define-values (elems tail) (loop b (hset-add seen t)))
+           (define-values (elems tail) (loop b (set-add seen t)))
            (values (cons a elems) tail)]
           [_ (values null t)])
         (values null t))))
diff --git a/typed-racket-lib/typed-racket/types/numeric-tower.rkt b/typed-racket-lib/typed-racket/types/numeric-tower.rkt
index 67ac7a95..d2922e63 100644
--- a/typed-racket-lib/typed-racket/types/numeric-tower.rkt
+++ b/typed-racket-lib/typed-racket/types/numeric-tower.rkt
@@ -1,13 +1,11 @@
 #lang racket/base
 
 (require "../utils/utils.rkt"
-         (rep rep-utils)
-         (types numeric-predicates base-abbrev)
-         (rename-in (rep type-rep) [make-Base make-Base*])
-         racket/function
-         racket/extflonum
+         (rep rep-utils type-mask numeric-base-types)
+         (types numeric-predicates)
+         (only-in (rep type-rep) Un make-Value)
          ;; For base type contracts
-         (for-template racket/base racket/contract/base racket/extflonum (types numeric-predicates)))
+         (for-template racket/base racket/contract/base (types numeric-predicates)))
 
 (provide portable-fixnum? portable-index?
          -Zero -One -PosByte -Byte -PosIndex -Index
@@ -21,161 +19,53 @@
          -PosInfinity -NegInfinity
          -ExactImaginary -FloatImaginary -SingleFlonumImaginary -InexactImaginary -Imaginary
          -ExactNumber -ExactComplex -FloatComplex -SingleFlonumComplex -InexactComplex -Number
-         (rename-out (-Int -Integer))
-         -ExtFlonumPosZero -ExtFlonumNegZero -ExtFlonumZero -ExtFlonumNan
-         -PosExtFlonum -NonNegExtFlonum -NegExtFlonum -NonPosExtFlonum -ExtFlonum)
+         (rename-out (-Int -Integer)))
 
-;; all the types defined here are numeric (except 80-bit flonums)
-(define (make-Base name contract predicate)
-  (make-Base* name contract predicate #t))
+;;
+;; unions of numeric bits defined below
+;;
 
 
-;; Numeric hierarchy
-;; All built as unions of non-overlapping base types.
-;; This should make encoding mathematical properties in the base env easier.
-;; The base types that don't have an interesting mathematical meaning
-;; (e.g. -Byte>1, -PosFixnumNotIndex, etc.) should not be used anywhere, as
-;; they should not be exposed to the user and could easily be misused in
-;; the base type environment. They are not provided.
-;; A lot of these contracts will be overriden in type->contract, so their
-;; hairiness should not be of much consequence.
-
-;; Is the number a fixnum on *all* the platforms Racket supports?  This
-;; works because Racket compiles only on 32+ bit systems.  This check is
-;; done at compile time to typecheck literals -- so use it instead of
-;; `fixnum?' to avoid creating platform-dependent .zo files.
-(define (portable-fixnum? n)
-  (and (exact-integer? n)
-       (< n (expt 2 30))
-       (>= n (- (expt 2 30)))))
-;; same, for indexes
-(define (portable-index? n)
-  (and (exact-integer? n)
-       (< n (expt 2 28))
-       (>= n 0)))
-
-;; Singletons
-(define/decl -Zero (make-Value 0)) ; exact
-(define/decl -One  (make-Value 1))
-
 ;; Infinities (These are part of Flonum/Single-Flonum, but useful abbreviatios.)
-(define/decl -PosInfinity (Un (-val +inf.0) (-val +inf.f)))
-(define/decl -NegInfinity (Un (-val -inf.0) (-val -inf.f)))
+(define/decl -PosInfinity (Un (make-Value +inf.0) (make-Value +inf.f)))
+(define/decl -NegInfinity (Un (make-Value -inf.0) (make-Value -inf.f)))
+
 
 ;; Integers
-(define/decl -Byte>1 (make-Base 'Byte-Larger-Than-One ; unsigned
-				#'(and/c byte? (lambda (x) (> x 1)))
-				(conjoin byte? (lambda (x) (> x 1)))))
 (define/decl -PosByte (Un -One -Byte>1))
 (define/decl -Byte    (Un -Zero -PosByte))
-(define/decl -PosIndexNotByte
-  (make-Base 'Positive-Index-Not-Byte
-             ;; index? will be checked at runtime, can be platform-specific
-             ;; portable-index? will be checked at compile-time, must be portable
-             #'(and/c index? positive? (not/c byte?))
-             (lambda (x) (and (portable-index? x)
-                              (positive? x)
-                              (not (byte? x))))))
+
 (define/decl -PosIndex    (Un -One -Byte>1 -PosIndexNotByte))
 (define/decl -Index       (Un -Zero -PosIndex))
-(define/decl -PosFixnumNotIndex
-  (make-Base 'Positive-Fixnum-Not-Index
-             #'(and/c fixnum? positive? (not/c index?))
-             (lambda (x) (and (portable-fixnum? x)
-                              (positive? x)
-                              (not (portable-index? x))))))
+
 (define/decl -PosFixnum    (Un -PosFixnumNotIndex -PosIndex))
 (define/decl -NonNegFixnum (Un -PosFixnum -Zero))
-(define/decl -NegFixnum
-  (make-Base 'Negative-Fixnum
-             #'(and/c fixnum? negative?)
-             (lambda (x) (and (portable-fixnum? x)
-                              (negative? x)))))
+
 (define/decl -NonPosFixnum (Un -NegFixnum -Zero))
 (define/decl -Fixnum       (Un -NegFixnum -Zero -PosFixnum))
-;; This type, and others like it, should *not* be exported, or used for
-;; anything but building unions. Especially, no literals should be given
-;; these types.
-(define/decl -PosIntNotFixnum
-  (make-Base 'Positive-Integer-Not-Fixnum
-             #'(and/c exact-integer? positive? (not/c fixnum?))
-             (lambda (x) (and (exact-integer? x)
-                              (positive? x)
-                              (not (portable-fixnum? x))))))
+
 (define/decl -PosInt    (Un -PosIntNotFixnum -PosFixnum))
 (define/decl -NonNegInt (Un -PosInt -Zero))
-(define/decl -Nat       -NonNegInt)
-(define/decl -NegIntNotFixnum
-  (make-Base 'Negative-Integer-Not-Fixnum
-             #'(and/c exact-integer? negative? (not/c fixnum?))
-             (lambda (x) (and (exact-integer? x)
-                              (negative? x)
-                              (not (portable-fixnum? x))))))
+(define/decl -Nat -NonNegInt)
+
 (define/decl -NegInt    (Un -NegIntNotFixnum -NegFixnum))
 (define/decl -NonPosInt (Un -NegInt -Zero))
 (define/decl -Int       (Un -NegInt -Zero -PosInt))
 
-;; Rationals
-(define/decl -PosRatNotInt
-  (make-Base 'Positive-Rational-Not-Integer
-             #'(and/c exact-rational? positive? (not/c integer?))
-             (lambda (x) (and (exact-rational? x)
-                              (positive? x)
-                              (not (exact-integer? x))))))
 (define/decl -PosRat    (Un -PosRatNotInt -PosInt))
 (define/decl -NonNegRat (Un -PosRat -Zero))
-(define/decl -NegRatNotInt
-  (make-Base 'Negative-Rational-Not-Integer
-             #'(and/c exact-rational? negative? (not/c integer?))
-             (lambda (x) (and (exact-rational? x)
-                              (negative? x)
-                              (not (exact-integer? x))))))
+
 (define/decl -NegRat    (Un -NegRatNotInt -NegInt))
 (define/decl -NonPosRat (Un -NegRat -Zero))
 (define/decl -Rat       (Un -NegRat -Zero -PosRat))
 
-;; Floating-point numbers
-;; NaN is included in all floating-point types
-(define/decl -FlonumNan
-  (make-Base 'Float-Nan
-	     #'(and/c flonum? (lambda (x) (eqv? x +nan.0)))
-	     (lambda (x) (and (flonum? x) (eqv? x +nan.0)))))
-(define/decl -FlonumPosZero
-  (make-Base 'Float-Positive-Zero
-	     #'(lambda (x) (eqv? x 0.0))
-	     (lambda (x) (eqv? x 0.0))))
-(define/decl -FlonumNegZero
-  (make-Base 'Float-Negative-Zero
-	     #'(lambda (x) (eqv? x -0.0))
-	     (lambda (x) (eqv? x -0.0))))
 (define/decl -FlonumZero (Un -FlonumPosZero -FlonumNegZero -FlonumNan))
-(define/decl -PosFlonumNoNan
-  (make-Base 'Positive-Float-No-NaN
-             #'(and/c flonum? positive?)
-             (lambda (x) (and (flonum? x) (positive? x)))))
 (define/decl -PosFlonum (Un -PosFlonumNoNan -FlonumNan))
 (define/decl -NonNegFlonum (Un -PosFlonum -FlonumZero))
-(define/decl -NegFlonumNoNan
-  (make-Base 'Negative-Float-No-NaN
-             #'(and/c flonum? negative?)
-             (lambda (x) (and (flonum? x) (negative? x)))))
 (define/decl -NegFlonum (Un -NegFlonumNoNan -FlonumNan))
 (define/decl -NonPosFlonum (Un -NegFlonum -FlonumZero))
-(define/decl -Flonum (Un -NegFlonumNoNan -FlonumNegZero -FlonumPosZero -PosFlonumNoNan -FlonumNan)) ; 64-bit floats
-;; inexact reals can be flonums (64-bit floats) or 32-bit floats
-(define/decl -SingleFlonumNan
-  (make-Base 'Single-Flonum-Nan
-	     #'(and/c single-flonum? (lambda (x) (eqv? x +nan.f)))
-	     (lambda (x) (and (single-flonum? x) (eqv? x +nan.f)))))
-(define/decl -SingleFlonumPosZero ; disjoint from Flonum 0s
-  (make-Base 'Single-Flonum-Positive-Zero
-             ;; eqv? equates 0.0f0 with itself, but not eq?
-             #'(lambda (x) (eqv? x 0.0f0))
-             (lambda (x) (eqv? x 0.0f0))))
-(define/decl -SingleFlonumNegZero
-  (make-Base 'Single-Flonum-Negative-Zero
-             #'(lambda (x) (eqv? x -0.0f0))
-             (lambda (x) (eqv? x -0.0f0))))
+(define/decl -Flonum (Un -NegFlonumNoNan -FlonumNegZero -FlonumPosZero -PosFlonumNoNan -FlonumNan))
+
 (define/decl -SingleFlonumZero (Un -SingleFlonumPosZero -SingleFlonumNegZero -SingleFlonumNan))
 (define/decl -InexactRealNan     (Un -FlonumNan -SingleFlonumNan))
 (define/decl -InexactRealPosZero (Un -SingleFlonumPosZero -FlonumPosZero))
@@ -183,18 +73,13 @@
 (define/decl -InexactRealZero    (Un -InexactRealPosZero
                                  -InexactRealNegZero
                                  -InexactRealNan))
-(define/decl -PosSingleFlonumNoNan
-  (make-Base 'Positive-Single-Flonum-No-Nan
-             #'(and/c single-flonum? positive?)
-             (lambda (x) (and (single-flonum? x) (positive? x)))))
+
+
 (define/decl -PosSingleFlonum    (Un -PosSingleFlonumNoNan -SingleFlonumNan))
 (define/decl -PosInexactReal     (Un -PosSingleFlonum -PosFlonum))
 (define/decl -NonNegSingleFlonum (Un -PosSingleFlonum -SingleFlonumZero))
 (define/decl -NonNegInexactReal  (Un -PosInexactReal -InexactRealZero))
-(define/decl -NegSingleFlonumNoNan
-  (make-Base 'Negative-Single-Flonum-No-Nan
-             #'(and/c single-flonum? negative?)
-             (lambda (x) (and (single-flonum? x) (negative? x)))))
+
 (define/decl -NegSingleFlonum    (Un -NegSingleFlonumNoNan -SingleFlonumNan))
 (define/decl -NegInexactReal     (Un -NegSingleFlonum -NegFlonum))
 (define/decl -NonPosSingleFlonum (Un -NegSingleFlonum -SingleFlonumZero))
@@ -211,127 +96,9 @@
 (define/decl -NonPosReal    (Un -NonPosRat -NonPosInexactReal))
 (define/decl -Real          (Un -Rat -InexactReal))
 
-;; Complexes
-;; We could go into _much_ more precision here.
-;; We could have types that reflect the size/exactness of both components
-;; (e.g. PosFixnumNonNegIntComplex), to give more interesting types to
-;; real-part, imag-part and others.
-;; We could have Complex be a 2-argument type constructor (although it
-;; could construct uninhabitable types like (Complex Integer Float), which
-;; can't exist in Racket (parts must be both exact, both inexact, or one is
-;; exact-zero)).  That's future work.
-
-;; Thus, the only possible kinds of complex numbers are:
-;; Zero/Rat, Zero/Flonum, Zero/SingleFlonum.
-;; Rat/Rat, Flonum/Flonum, SingleFlonum/SingleFlonum.
-(define/decl -ExactImaginary
-  (make-Base 'Exact-Imaginary
-             #'(and/c number?
-                      (not/c real?)
-                      (lambda (x)
-                        (and
-                          (eqv? 0 (real-part x))
-                          (exact? (imag-part x)))))
-             (lambda (x) (and (number? x)
-                              (not (real? x))
-                              (eqv? 0 (real-part x))
-                              (exact? (imag-part x))))))
-(define/decl -ExactComplex
-  (make-Base 'Exact-Complex
-             #'(and/c number?
-                      (not/c real?)
-                      (lambda (x)
-                        (and
-                          (not (eqv? 0 (real-part x)))
-                          (exact? (real-part x))
-                          (exact? (imag-part x)))))
-             (lambda (x) (and (number? x)
-                              (not (real? x))
-                              (not (eqv? 0 (real-part x)))
-                              (exact? (real-part x))
-                              (exact? (imag-part x))))))
-(define/decl -FloatImaginary
-  (make-Base 'Float-Imaginary
-	     #'(and/c number?
-		      (lambda (x)
-			(and (flonum? (imag-part x))
-			     (eqv? 0 (real-part x)))))
-	     (lambda (x)
-	       (and (number? x)
-		    (flonum? (imag-part x))
-		    (eqv? 0 (real-part x))))))
-(define/decl -SingleFlonumImaginary 
-  (make-Base 'Single-Flonum-Imaginary
-	     #'(and/c number?
-		      (lambda (x)
-			(and (single-flonum? (imag-part x))
-			     (eqv? 0 (real-part x)))))
-	     (lambda (x)
-	       (and (number? x)
-		    (single-flonum? (imag-part x))
-		    (eqv? 0 (real-part x))))))
-(define/decl -FloatComplex
-  (make-Base 'Float-Complex
-	     #'(and/c number?
-		      (lambda (x)
-			(and (flonum? (imag-part x))
-			     (flonum? (real-part x)))))
-	     (lambda (x)
-	       (and (number? x)
-		    (flonum? (imag-part x))
-		    (flonum? (real-part x))))))
-(define/decl -SingleFlonumComplex
-  (make-Base 'Single-Flonum-Complex
-	     #'(and/c number?
-		      (lambda (x)
-			(and (single-flonum? (imag-part x))
-			     (single-flonum? (real-part x)))))
-	     (lambda (x)
-	       (and (number? x)
-		    (single-flonum? (imag-part x))
-		    (single-flonum? (real-part x))))))
 (define/decl -ExactNumber (Un -ExactImaginary -ExactComplex -Rat))
 (define/decl -InexactImaginary (Un -FloatImaginary -SingleFlonumImaginary))
 (define/decl -Imaginary (Un -ExactImaginary -InexactImaginary))
 (define/decl -InexactComplex (Un -FloatComplex -SingleFlonumComplex))
 (define/decl -Complex (Un -Real -Imaginary -ExactComplex -InexactComplex))
 (define/decl -Number -Complex)
-
-;; 80-bit floating-point numbers
-;; +nan.t is included in all 80-bit floating-point types
-(define/decl -ExtFlonumNan
-  (make-Base* 'ExtFlonum-Nan
-              #'(and/c extflonum? (lambda (x) (eqv? x +nan.t)))
-              (lambda (x) (and (extflonum? x) (eqv? x +nan.t)))
-              #f))
-
-(define/decl -ExtFlonumPosZero
-  (make-Base* 'ExtFlonum-Positive-Zero
-              #'(lambda (x) (eqv? x 0.0t0))
-              (lambda (x) (eqv? x 0.0t0))
-              #f))
-
-(define/decl -ExtFlonumNegZero
-  (make-Base* 'ExtFlonum-Negative-Zero
-              #'(lambda (x) (eqv? x -0.0t0))
-              (lambda (x) (eqv? x -0.0t0))
-              #f))
-
-(define/decl -NegExtFlonumNoNan
-  (make-Base* 'Negative-ExtFlonum-No-NaN
-              #'(and/c extflonum? (λ (x) (extfl<= x 0.0t0)))
-              (lambda (x) (and (extflonum? x) (extfl<= x 0.0t0)))
-              #f))
-
-(define/decl -PosExtFlonumNoNan
-  (make-Base* 'Positive-ExtFlonum-No-NaN
-              #'(and/c extflonum? (λ (x) (extfl>= x 0.0t0)))
-              (lambda (x) (and (extflonum? x) (extfl>= x 0.0t0)))
-              #f))
-
-(define/decl -ExtFlonumZero (Un -ExtFlonumPosZero -ExtFlonumNegZero -ExtFlonumNan))
-(define/decl -PosExtFlonum (Un -PosExtFlonumNoNan -ExtFlonumNan))
-(define/decl -NonNegExtFlonum (Un -PosExtFlonum -ExtFlonumZero))
-(define/decl -NegExtFlonum (Un -NegExtFlonumNoNan -ExtFlonumNan))
-(define/decl -NonPosExtFlonum (Un -NegExtFlonum -ExtFlonumZero))
-(define/decl -ExtFlonum (Un -NegExtFlonumNoNan -ExtFlonumNegZero -ExtFlonumPosZero -PosExtFlonumNoNan -ExtFlonumNan))
diff --git a/typed-racket-lib/typed-racket/types/overlap.rkt b/typed-racket-lib/typed-racket/types/overlap.rkt
index ad596b39..2a08911f 100644
--- a/typed-racket-lib/typed-racket/types/overlap.rkt
+++ b/typed-racket-lib/typed-racket/types/overlap.rkt
@@ -1,10 +1,10 @@
 #lang racket/base
 
 (require "../utils/utils.rkt"
-         (utils hset)
          (rep type-rep rep-utils type-mask)
          (prefix-in c: (contract-req))
          (types abbrev subtype resolve utils)
+         racket/set
          racket/match)
 
 
@@ -61,37 +61,46 @@
          (overlap? t (resolve-once s))]
         [((? Mu? t1) t2) #:no-order (overlap? (unfold t1) t2)]
         [((Refinement: t1 _) t2) #:no-order (overlap? t1 t2)]
-        [((Union: ts1) t2)
-         (match t2
-           [(Union: ts2)
-            (or (hset-overlap? ts1 ts2)
-                (for*/or ([t1 (in-hset ts1)]
-                          [t2 (in-hset ts2)])
-                  (overlap? t1 t2)))]
-           [_ (or (hset-member? ts1 t2)
-                  (for/or ([t1 (in-hset ts1)])
-                    (overlap? t1 t2)))])]
-        [(t1 (Union: ts2))
-         (or (hset-member? ts2 t1)
-             (for/or ([t2 (in-hset ts2)]) (overlap? t1 t2)))]
+        [((BaseUnion: bbits1 nbits1)
+          (BaseUnion: bbits2 nbits2))
+         (or (bbits-overlap? bbits1 bbits2)
+             (nbits-overlap? nbits1 nbits2))]
+        [((BaseUnion: bbits nbits) (Base-bits: num? bits))
+         #:no-order
+         (if num?
+             (nbits-overlap? nbits bits)
+             (bbits-overlap? bbits bits))]
+        [((BaseUnion-bases: bases1) t2)
+         #:no-order
+         (for/or ([b1 (in-list bases1)]) (overlap? b1 t2))]
+        [((Union: (BaseUnion: bbits1 nbits1) _)
+          (Union: (BaseUnion: bbits2 nbits2) _))
+         #:when (or (bbits-overlap? bbits1 bbits2)
+                    (nbits-overlap? nbits1 nbits2))
+         #t]
+        [((Union/set: base1 ts1 elems1) t2)
+         #:no-order
+         (or (set-member? elems1 t2)
+             (overlap? base1 t2)
+             (for/or ([t1 (in-list ts1)]) (overlap? t1 t2)))]
         [((Intersection: ts) s)
          #:no-order
-         (for/and ([t (in-hset ts)]) (overlap? t s))]
+         (for/and ([t (in-list ts)]) (overlap? t s))]
         [((or (Poly-unsafe: _ t1)
               (PolyDots-unsafe: _ t1))
           t2)
          #:no-order
          (overlap? t1 t2)] ;; conservative
-        [((Base: s1 _ _ _) (Base: s2 _ _ _)) (or (subtype t1 t2) (subtype t2 t1))]
+        [((? Base?) (? Base?)) (or (subtype t1 t2) (subtype t2 t1))]
         [((? Base? t) (? Value? s)) #:no-order (subtype s t)] ;; conservative
         [((Syntax: t) (Syntax: t*)) (overlap? t t*)]
         [((Syntax: _) _) #:no-order #f]
-        [((Base: _ _ _ _) _) #:no-order #f]
+        [((? Base?) _) #:no-order #f]
         [((Value: (? pair?)) (Pair: _ _)) #:no-order #t]
         [((Pair: a b) (Pair: a* b*)) (and (overlap? a a*)
                                           (overlap? b b*))]
         ;; lots of things are sequences, but not values where sequence? produces #f
-        [((Sequence: _) (Value: v)) #:no-order (sequence? v)]
+        [((Sequence: _) (Val-able: v)) #:no-order (sequence? v)]
         ;; hash tables are two-valued sequences
         [((Sequence: (or (list _) (list _ _ _ ...)))
           (or (? Hashtable?) (? HashtableTop?)))
@@ -105,16 +114,16 @@
         ;; be conservative about other kinds of sequences
         [((Sequence: _) _) #:no-order #t]
         ;; Values where evt? produces #f cannot be Evt
-        [((Evt: _) (Value: v)) #:no-order (evt? v)]
+        [((Evt: _) (Val-able: v)) #:no-order (evt? v)]
         [((Pair: _ _) _) #:no-order #f]
-        [((Value: (? simple-datum? v1))
-          (Value: (? simple-datum? v2)))
+        [((Val-able: (? simple-datum? v1))
+          (Val-able: (? simple-datum? v2)))
          (equal? v1 v2)]
-        [((Value: (? simple-datum?))
+        [((Val-able: (? simple-datum?))
           (or (? Struct?) (? StructTop?) (? Function?)))
          #:no-order
          #f]
-        [((Value: (not (? hash?)))
+        [((Val-able: (not (? hash?)))
           (or (? Hashtable?) (? HashtableTop?)))
          #:no-order
          #f]
@@ -128,6 +137,10 @@
           (StructTop: (Struct: n* #f _ _ _ _)))
          #:when (free-identifier=? n n*)
          #t]
+        [((StructTop: (Struct: n* #f _ _ _ _))
+          (Struct: n #f _ _ _ _))
+         #:when (free-identifier=? n n*)
+         #t]
         ;; n and n* must be different, so there's no overlap
         [((Struct: n #f flds _ _ _)
           (Struct: n* #f flds* _ _ _))
@@ -135,6 +148,9 @@
         [((Struct: n #f flds _ _ _)
           (StructTop: (Struct: n* #f flds* _ _ _)))
          #f]
+        [((StructTop: (Struct: n* #f flds* _ _ _))
+          (Struct: n #f flds _ _ _))
+         #f]
         [((and t1 (Struct: _ _ _ _ _ _))
           (and t2 (Struct: _ _ _ _ _ _)))
          (or (subtype t1 t2) (subtype t2 t1)
diff --git a/typed-racket-lib/typed-racket/types/path-type.rkt b/typed-racket-lib/typed-racket/types/path-type.rkt
index a492b26a..b2c748d0 100644
--- a/typed-racket-lib/typed-racket/types/path-type.rkt
+++ b/typed-racket-lib/typed-racket/types/path-type.rkt
@@ -4,7 +4,7 @@
          racket/match racket/set
          (contract-req)
          (rep object-rep type-rep values-rep)
-         (utils tc-utils hset)
+         (utils tc-utils)
          (typecheck renamer)
          (types subtype resolve)
          (except-in (types utils abbrev kw-types) -> ->* one-of/c))
@@ -32,6 +32,8 @@
       ;; empty path
       [(t (list)) t]
 
+      ;; -- non-empty path beyond here --
+      
       ;; pair ops
       [((Pair: t s) (cons (CarPE:) rst))
        (path-type rst t (hash))]
@@ -53,12 +55,13 @@
          (path-type rst ft (hash)))]
 
       [((Intersection: ts) _)
-       (apply -unsafe-intersect (for*/list ([t (in-hset ts)]
+       (apply -unsafe-intersect (for*/list ([t (in-list ts)]
                                             [t (in-value (path-type path t resolved))]
                                             #:when t)
                                   t))]
-      [((Union: ts) _)
-       (Union-map ts (λ (t) (or (path-type path t resolved) -Bottom)))]
+      [((Union: _ ts) _)
+       ;; drop base types, since they are incompatible w/ a path element
+       (Union-fmap (λ (t) (or (path-type path t resolved) -Bottom)) -Bottom ts)]
 
       ;; paths into polymorphic types
       ;; TODO can this expose unbound type indices... probably. It should be
diff --git a/typed-racket-lib/typed-racket/types/printer.rkt b/typed-racket-lib/typed-racket/types/printer.rkt
index 8d32a08e..d31e664c 100644
--- a/typed-racket-lib/typed-racket/types/printer.rkt
+++ b/typed-racket-lib/typed-racket/types/printer.rkt
@@ -13,13 +13,12 @@
                   "types/match-expanders.rkt"
                   "types/kw-types.rkt"
                   "types/utils.rkt" "types/abbrev.rkt"
-                  "types/union.rkt"
+                  "types/union.rkt" "types/numeric-tower.rkt"
                   "types/resolve.rkt"
                   "types/prefab.rkt"
                   "utils/utils.rkt"
                   "utils/primitive-comparison.rkt"
-                  "utils/tc-utils.rkt"
-                  "utils/hset.rkt")
+                  "utils/tc-utils.rkt")
          (for-syntax racket/base syntax/parse))
 
 ;; printer-type: (one-of/c 'custom 'debug)
@@ -166,23 +165,22 @@
 ;; be nicer to print them using higher-level descriptions instead.
 ;; We do set coverage, with the elements of the union being what we want to
 ;; cover, and all the names types we know about being the sets.
-(define (cover-union t ignored-names)
-  (match-define (Union: (app hset->list elems)) t)
+(define (cover-union t elems ignored-names)
   (define valid-names
     ;; We keep only unions, and only those that are subtypes of t.
     ;; It's no use attempting to cover t with things that go outside of t.
     (filter (lambda (p)
               (match p
-                [(cons name (? Union? t*))
+                [(cons name (and t* (or (? Union?) (? BaseUnion?))))
                  (and (not (member name ignored-names))
                       (subtype t* t))]
                 [_ #f]))
             (force (current-type-names))))
   ;; names and the sets themselves (not the union types)
-  ;; note that racket/set supports lists with equal?, which in
-  ;; the case of Types will be type-equal?
+  ;; note that racket/set supports lists with equal?
   (define candidates
-    (map (match-lambda [(cons name (Union: (app hset->list elts))) (cons name elts)])
+    (map (match-lambda [(cons name (Union-all-flat: elts)) (cons name elts)]
+                       [(cons name (BaseUnion-bases: elts)) (cons name elts)])
          valid-names))
   ;; some types in the union may not be coverable by the candidates
   ;; (e.g. type variables, etc.)
@@ -439,12 +437,12 @@
   (define (tuple? t)
     (match t
       [(Pair: a (? tuple?)) #t]
-      [(Value: '()) #t]
+      [(== -Null) #t]
       [_ #f]))
   (define (tuple-elems t)
     (match t
       [(Pair: a e) (cons a (tuple-elems e))]
-      [(Value: '()) null]))
+      [(== -Null) null]))
   (match type
     [(Univ:) 'Any]
     [(Bottom:) 'Nothing]
@@ -466,10 +464,13 @@
                           (append names ignored-names)))]
            [else
             ;; to allow :type to cue the user on unexpanded aliases
-            (when (Union? type) ; only unions can be expanded
+            (when (or (Union? type) (BaseUnion? type)) ; only unions can be expanded
               (set-box! (current-print-unexpanded)
                         (cons (car names) (unbox (current-print-unexpanded)))))
             (car names)])]
+    ;; format as a string to preserve reader abbreviations and primitive
+    ;; values like characters (when `display`ed)
+    [(Val-able: v) (format "~v" v)]
     [(? Base?) (Base-name type)]
     [(StructType: (Struct: nm _ _ _ _ _)) `(StructType ,(syntax-e nm))]
     ;; this case occurs if the contained type is a type variable
@@ -499,9 +500,6 @@
      `(Listof ,(t->s elem-ty))]
     [(SimpleMListof: elem-ty)
      `(MListof ,(t->s elem-ty))]
-    ;; format as a string to preserve reader abbreviations and primitive
-    ;; values like characters (when `display`ed)
-    [(Value: v) (format "~v" v)]
     [(? tuple? t)
      `(List ,@(map type->sexp (tuple-elems t)))]
     [(Opaque: pred) `(Opaque ,(syntax->datum pred))]
@@ -529,11 +527,14 @@
     [(Evt: r) `(Evtof ,(t->s r))]
     [(? Union? (app normalize-type type))
      (match type
-       [(? Union?)
-        (define-values (covered remaining) (cover-union type ignored-names))
+       [(Union-all-flat: ts)
+        (define-values (covered remaining) (cover-union type ts ignored-names))
         (cons 'U (sort (append covered (map t->s remaining)) primitive<=?))]
        [_ (t->s type)])]
-    [(Intersection: (app hset->list elems))
+    [(BaseUnion-bases: bs)
+     (define-values (covered remaining) (cover-union type bs ignored-names))
+     (cons 'U (sort (append covered (map t->s remaining)) primitive<=?))]
+    [(Intersection: elems)
      (cons '∩ (sort (map t->s elems) primitive<=?))]
     [(Pair: l r) `(Pairof ,(t->s l) ,(t->s r))]
     [(ListDots: dty dbound) `(List ,(t->s dty) ... ,dbound)]
@@ -555,17 +556,25 @@
     [(PolyRow-names: names _ body)
      `(All (,(car names) #:row) ,(t->s body))]
     ;; x1 --> ()
-    [(Mu: x (Syntax: (Union: (list
-                              (Base: 'Number _ _ _)
-                              (Base: 'Boolean _ _ _)
-                              (Base: 'Symbol _ _ _)
-                              (Base: 'String _ _ _)
-                              (Mu: var (Union: (list (Value: '())
-                                                     (Pair: (F: x) (F: var)))))
-                              (Mu: y (Union: (list (F: x)
-                                                   (Pair: (F: x) (F: y)))))
-                              (Vector: (F: x))
-                              (Box: (F: x))))))
+    [(Mu-unsafe:
+      (Syntax: (Union: (== (Un -Number -Boolean -Symbol -String))
+                       ts)))
+     #:when (and (= 4 (length ts))
+                 (member (-vec (make-B 0)) ts)
+                 (member (-box (make-B 0)) ts)
+                 (let ([ts (remove (-box (make-B 0))
+                                   (remove (-vec (make-B 0)) ts))])
+                   (match ts
+                     [(list-no-order (Mu-unsafe:
+                                      (Union: (== -Null)
+                                              (list (Pair: (B: 1) (B: 0)))))
+                                     (Mu-unsafe:
+                                      (Union: (== -Bottom)
+                                              (list-no-order
+                                               (B: 1)
+                                               (Pair: (B: 1) (B: 0))))))
+                      #t]
+                     [_ #f])))
      'Syntax]
     [(Mu-name: name body)
      `(Rec ,name ,(t->s body))]
diff --git a/typed-racket-lib/typed-racket/types/subtract.rkt b/typed-racket-lib/typed-racket/types/subtract.rkt
index 2a4710b3..72bc6413 100644
--- a/typed-racket-lib/typed-racket/types/subtract.rkt
+++ b/typed-racket-lib/typed-racket/types/subtract.rkt
@@ -1,7 +1,6 @@
 #lang racket/base
 
 (require "../utils/utils.rkt"
-         (utils hset)
          (rep type-rep rep-utils type-mask)
          (types abbrev subtype resolve utils)
          racket/match)
@@ -14,18 +13,30 @@
 ;; conservatively calculates set subtraction
 ;; between the types (i.e. t - s)
 (define (subtract t s)
+  (define s-mask (mask s))
   (define result
     (let sub ([t t])
       (match t
-        [_ #:when (disjoint-masks? (mask t) (mask s)) t]
+        [_ #:when (disjoint-masks? (mask t) s-mask) t]
         [_ #:when (subtype t s) -Bottom]
         [(or (App: _ _) (? Name?))
          ;; must be different, since they're not subtypes
          ;; and n must refer to a distinct struct type
          t]
-        [(Union: elems) (Union-map elems sub)]
+        [(BaseUnion: bbits nbits)
+         (match s
+           [(Base-bits: num? bits)
+            (if num?
+                (make-BaseUnion bbits (nbits-subtract nbits bits))
+                (make-BaseUnion (bbits-subtract bbits bits) nbits))]
+           [(BaseUnion: bbits* nbits*)
+            (make-BaseUnion (bbits-subtract bbits bbits*)
+                            (nbits-subtract nbits nbits*))]
+           [_ (apply Un (for/list ([b (in-list (BaseUnion-bases t))])
+                          (sub b)))])]
+        [(Union: base elems) (Union-fmap sub base elems)]
         [(Intersection: ts)
-         (apply -unsafe-intersect (hset-map ts sub))]
+         (apply -unsafe-intersect (map sub ts))]
         [(? Mu?) (sub (unfold t))]
         [(Poly: vs b) (make-Poly vs (sub b))]
         [_ t])))
diff --git a/typed-racket-lib/typed-racket/types/subtype.rkt b/typed-racket-lib/typed-racket/types/subtype.rkt
index adcbfe5a..bb8f6451 100644
--- a/typed-racket-lib/typed-racket/types/subtype.rkt
+++ b/typed-racket-lib/typed-racket/types/subtype.rkt
@@ -1,31 +1,34 @@
 #lang racket/base
 (require (except-in "../utils/utils.rkt" infer)
          racket/match racket/function racket/lazy-require
-         racket/list
+         racket/list racket/set
          (contract-req)
          (rep type-rep prop-rep object-rep
               core-rep type-mask values-rep rep-utils
               free-variance rep-switch)
-         (utils tc-utils hset)
+         (utils tc-utils)
          (types utils resolve match-expanders current-seen
                 numeric-tower substitute prefab signatures)
          (for-syntax racket/base syntax/parse racket/sequence)
-         (rename-in "base-abbrev.rkt"
-                    [-> t->]
-                    [->* t->*]))
+         (except-in (rename-in "abbrev.rkt"
+                               [-> t->]
+                               [->* t->*])
+                    one-of/c))
 
 (lazy-require
-  ("../infer/infer.rkt" (infer))
-  ("../typecheck/tc-subst.rkt" (restrict-values)))
+ ("../infer/infer.rkt" (infer))
+ ("../typecheck/tc-subst.rkt" (restrict-values)))
 
+(provide NameStruct:)
 
 (provide/cond-contract
  [subtype (-> Type? Type? boolean?)]
  [subresult (-> Result? Result? boolean?)]
  [subval (-> SomeValues? SomeValues? boolean?)]
- [type-compare? (-> (or/c Type? SomeValues?) (or/c Type? SomeValues?) boolean?)]
+ [type-equiv? (-> Type? Type? boolean?)]
  [subtypes (-> (listof Type?) (listof Type?) boolean?)]
- [subtypes/varargs (-> (listof Type?) (listof Type?) (or/c Type? #f) boolean?)])
+ [subtypes/varargs (-> (listof Type?) (listof Type?) (or/c Type? #f) boolean?)]
+ [unrelated-structs (-> Struct? Struct? boolean?)])
 
 
 ;;************************************************************
@@ -45,9 +48,8 @@
   (and (subval* (seen) v1 v2) #t))
 
 ;; are t1 and t2 equivalent types (w.r.t. subtyping)
-(define (type-compare? t1 t2)
-  (or (equal? t1 t2) (and (subtype t1 t2)
-                          (subtype t2 t1))))
+(define (type-equiv? t1 t2)
+  (and (type≡? (seen) t1 t2) #t))
 
 ;; are all the s's subtypes of all the t's?
 ;; [type] [type] -> boolean
@@ -145,15 +147,15 @@
      A
      (match* (kws1 kws2)
        [((cons (Keyword: k1 t1 r1) rest1) (cons (Keyword: k2 t2 r2) rest2))
-	(cond [(eq? k2 k1)
-	       (and ;; if t is optional, s must be as well
-		(or r2 (not r1))
-		(loop (subtype* A t2 t1) rest1 rest2))]
-	      ;; optional extra keywords in s are ok
-	      ;; we just ignore them
-	      [(and (not r1) (keyword<? k1 k2)) (loop A rest1 kws2)]
-	      ;; extra keywords in t are a problem
-	      [else #f])]
+        (cond [(eq? k2 k1)
+               (and ;; if t is optional, s must be as well
+                (or r2 (not r1))
+                (loop (subtype* A t2 t1) rest1 rest2))]
+              ;; optional extra keywords in s are ok
+              ;; we just ignore them
+              [(and (not r1) (keyword<? k1 k2)) (loop A rest1 kws2)]
+              ;; extra keywords in t are a problem
+              [else #f])]
        ;; no more keywords to satisfy, the rest in t must be optional
        [(_ '()) (and (andmap (match-lambda [(Keyword: _ _ r1) (not r1)])
                              kws1) A)]
@@ -352,7 +354,7 @@
 
 (define/cond-contract (subresult* A res1 res2)
   (-> (listof (cons/c Type? Type?)) Result? Result?
-        any/c)
+      any/c)
   (match* (res1 res2)
     [((Result: t1 (PropSet: p1+ p1-) o1)
       (Result: t2 (PropSet: p2+ p2-) o2))
@@ -366,14 +368,14 @@
 ;; Type Subtyping
 ;;************************************************************
 
-(define/cond-contract (type-equiv? A t1 t2)
+(define/cond-contract (type≡? A t1 t2)
   (-> list? Type? Type? any/c)
   (subtype-seq A
-	       (subtype* t1 t2)
-	       (subtype* t2 t1)))
+               (subtype* t1 t2)
+               (subtype* t2 t1)))
 
-(define union-super-cache (make-weak-hasheq))
-(define union-sub-cache (make-weak-hasheq))
+(define union-super-cache (make-weak-hash))
+(define union-sub-cache (make-weak-hash))
 
 ;; cache-set!
 ;; caches 'result' as the answer for 't1 <: t2'
@@ -415,7 +417,7 @@
      (match t2
        [(Intersection: t2s)
         (for/fold ([A A])
-                  ([t2 (in-hset t2s)]
+                  ([t2 (in-list t2s)]
                    #:break (not A))
           (subtype* A t1 t2))]
        [(? resolvable?)
@@ -425,45 +427,77 @@
               ;; check needed for if a name that hasn't been resolved yet
               (and (Type? t2) (subtype* A t1 t2)))))]
        [_
-        (or
-         ;; then we try a switch on t1
-         (subtype-switch
-          t1 t2 A
-          ;; if we're still not certain after the switch,
-          ;; check the cases that need to come at the end
-          (λ (A t1 t2)
-            (match* (t1 t2)
-              [(t1 (Union: elems2))
-               (cond
-                 [(hset-member? elems2 t1) A]
-                 [(cache-ref union-super-cache t2 t1)
-                  => (λ (b) (and (unbox b) A))]
-                 [else
-                  (define result
-                    (for/or ([elem (in-hset elems2)])
-                      (and (subtype* A t1 elem) A)))
-                  (when (null? A)
-                    (cache-set! union-super-cache t2 t1 (and result #t)))
-                  result])]
-              [((Intersection: t1s) _)
-               (for/or ([t1 (in-hset t1s)])
-                 (subtype* A t1 t2))]
-              [(_ (Instance: (? resolvable? t2*)))
-               (let ([A (remember t1 t2 A)])
-                 (with-updated-seen A
-                   (let ([t2* (resolve-once t2*)])
-                     (and (Type? t2*)
-                          (subtype* A t1 (make-Instance t2*))))))]
-              [(_ (Poly: vs2 b2))
-               #:when (null? (fv b2))
-               (subtype* A t1 b2)]
-              [(_ (PolyDots: vs2 b2))
-               #:when (and (null? (fv b2))
-                           (null? (fi b2)))
-               (subtype* A t1 b2)]
-              [(_ _) #f]))))])]))
+        ;; then we try a switch on t1
+        (subtype-switch
+         t1 t2 A
+         ;; if we're still not certain after the switch,
+         ;; check the cases that need to come at the end
+         (λ (A t1 t2)
+           (match* (t1 t2)
+             [(t1 (Union/set: base2 ts2 elems2))
+              (cond
+                [(set-member? elems2 t1) A]
+                [(cache-ref union-super-cache t2 t1)
+                 => (λ (b) (and (unbox b) A))]
+                [else
+                 (define result
+                   (or (subtype* A t1 base2)
+                       (for/or ([elem (in-list ts2)])
+                         (subtype* A t1 elem))))
+                 (when (null? A)
+                   (cache-set! union-super-cache t2 t1 (and result #t)))
+                 result])]
+             [((Intersection: t1s) _)
+              (for/or ([t1 (in-list t1s)])
+                (subtype* A t1 t2))]
+             [(_ (Instance: (? resolvable? t2*)))
+              (let ([A (remember t1 t2 A)])
+                (with-updated-seen A
+                  (let ([t2* (resolve-once t2*)])
+                    (and (Type? t2*)
+                         (subtype* A t1 (make-Instance t2*))))))]
+             [(_ (Poly: vs2 b2))
+              #:when (null? (fv b2))
+              (subtype* A t1 b2)]
+             [(_ (PolyDots: vs2 b2))
+              #:when (and (null? (fv b2))
+                          (null? (fi b2)))
+              (subtype* A t1 b2)]
+             [(_ _) #f])))])]))
 
 
+;; these data structures are allocated once and
+;; used below in 'subtype-switch'
+(define seq->elem-table
+  (hash -FlVector    -Flonum
+        -ExtFlVector -ExtFlonum
+        -FxVector    -Fixnum
+        -String      -Char
+        -Bytes       -Byte
+        -Input-Port  -Nat))
+
+(define event-types
+  (list -Semaphore
+        -Output-Port
+        -Input-Port
+        -TCP-Listener
+        -Thread
+        -Subprocess
+        -Will-Executor))
+
+(define event-univ-types (list -Place -Base-Place-Channel))
+(define num-seq-types (list -Byte -Index -NonNegFixnum -Nat))
+(define log-vect-type (make-HeterogeneousVector
+                       (list -Symbol -String Univ
+                             (Un -False -Symbol))))
+(define null-or-mpair-top (Un -Null -MPairTop))
+
+(define value-numeric-seq-possibilities
+  (list
+   (cons byte? -Byte)
+   (cons portable-index? -Index)
+   (cons portable-fixnum? -NonNegFixnum)
+   (cons values -Nat)))
 
 (define-switch (subtype-switch t1 t2 A continue)
   ;; NOTE: keep these in alphabetical order
@@ -477,24 +511,25 @@
   [(case: Async-Channel (Async-Channel: elem1))
    (match t2
      [(? Async-ChannelTop?) A]
-     [(Async-Channel: elem2) (type-equiv? A elem1 elem2)]
+     [(Async-Channel: elem2) (type≡? A elem1 elem2)]
      [(Evt: evt-t) (subtype* A elem1 evt-t)]
      [_ (continue A t1 t2)])]
-  [(case: Base (Base: kind _ pred numeric?))
+  [(case: Base (Base-bits: num? bits))
    (match t2
+     [(BaseUnion: bbits nbits)
+      (and (if num?
+               (nbits-overlap? nbits bits)
+               (bbits-overlap? bbits bits))
+           A)]
      [(Sequence: (list seq-t))
       (cond
-        [(assq kind `((FlVector . ,-Flonum)
-                      (ExtFlVector . ,-ExtFlonum)
-                      (FxVector . ,-Fixnum)
-                      (String . ,-Char)
-                      (Bytes . ,-Byte)
-                      (Input-Port . ,-Nat)))
-         => (λ (p) (subtype* A (cdr p) seq-t))]
-        [numeric?
+        [(Base:Null? t1) A]
+        [(hash-ref seq->elem-table t1 #f)
+         => (λ (elem-ty) (subtype* A elem-ty seq-t))]
+        [num?
          (define type
            ;; FIXME: thread the store through here
-           (for/or ([num-t (in-list (list -Byte -Index -NonNegFixnum -Nat))])
+           (for/or ([num-t (in-list num-seq-types)])
              (or (and (subtype* A t1 num-t) num-t))))
          (if type
              (subtype* A type seq-t)
@@ -502,33 +537,48 @@
         [else #f])]
      [(Evt: evt-t)
       (cond
-        [(memq kind '(Semaphore
-                      Output-Port
-                      Input-Port
-                      TCP-Listener
-                      Thread
-                      Subprocess
-                      Will-Executor))
+        [(member t1 event-types)
          (subtype* A t1 evt-t)]
         ;; FIXME: change Univ to Place-Message-Allowed if/when that type is defined
-        [(and (Univ? evt-t) (memq kind '(Place Base-Place-Channel)))
+        [(and (Univ? evt-t) (member t1 event-univ-types))
          A]
-        [(eq? kind 'LogReceiver) (subtype* A
-                                           (make-HeterogeneousVector
-                                            (list -Symbol -String Univ
-                                                  (Un (-val #f) -Symbol)))
-                                           evt-t)]
+        [(Base:Log-Receiver? t1)
+         (subtype* A log-vect-type evt-t)]
         [else #f])]
      [_ (continue A t1 t2)])]
+  [(case: BaseUnion (BaseUnion: bbits1 nbits1))
+   (match t2
+     [(? Base?) #f]
+     [(BaseUnion: bbits2 nbits2)
+      (and (bbits-subset? bbits1 bbits2)
+           (nbits-subset? nbits1 nbits2)
+           A)]
+     [(Union: (BaseUnion: bbits2 nbits2) _)
+      #:when (and (bbits-subset? bbits1 bbits2)
+                  (nbits-subset? nbits1 nbits2))
+      A]
+     [_
+      (cond
+        [(cache-ref union-sub-cache t1 t2)
+         => (λ (b) (and (unbox b) A))]
+        [else
+         (define result
+           (for/fold ([A A])
+                     ([b (in-list (BaseUnion-bases t1))]
+                      #:break (not A))
+             (subtype* A b t2)))
+         (when (null? A)
+           (cache-set! union-sub-cache t1 t2 (and result #t)))
+         result])])]
   [(case: Box (Box: elem1))
    (match t2
      [(? BoxTop?) A]
-     [(Box: elem2) (type-equiv? A elem1 elem2)]
+     [(Box: elem2) (type≡? A elem1 elem2)]
      [_ (continue A t1 t2)])]
   [(case: Channel (Channel: elem1))
    (match t2
      [(? ChannelTop?) A]
-     [(Channel: elem2) (type-equiv? A elem1 elem2)]
+     [(Channel: elem2) (type≡? A elem1 elem2)]
      [(Evt: evt-t) (subtype* A elem1 evt-t)]
      [_ (continue A t1 t2)])]
   [(case: Class (Class: row inits fields methods augments init-rest))
@@ -575,7 +625,7 @@
    (match t2
      [(? Continuation-Mark-KeyTop?) A]
      [(Continuation-Mark-Keyof: val2)
-      (type-equiv? A val1 val2)]
+      (type≡? A val1 val2)]
      [_ (continue A t1 t2)])]
   [(case: CustodianBox (CustodianBox: elem1))
    (match t2
@@ -634,8 +684,8 @@
    (match t2
      [(? HashtableTop?) A]
      [(Hashtable: key2 val2) (subtype-seq A
-                                          (type-equiv? key1 key2)
-                                          (type-equiv? val1 val2))]
+                                          (type≡? key1 key2)
+                                          (type≡? val1 val2))]
      [(Sequence: (list key2 val2))
       (subtype-seq A
                    (subtype* key1 key2)
@@ -651,12 +701,12 @@
                        ([elem1 (in-list elems1)]
                         [elem2 (in-list elems2)]
                         #:break (not A))
-               (type-equiv? A elem1 elem2))]
+               (type≡? A elem1 elem2))]
             [else #f])]
      [(Vector: elem2)
       (for/fold ([A A])
                 ([elem1 (in-list elems1)] #:break (not A))
-        (type-equiv? A elem1 elem2))]
+        (type≡? A elem1 elem2))]
      [(Sequence: (list seq-t))
       (for/fold ([A A])
                 ([elem1 (in-list elems1)]
@@ -681,7 +731,8 @@
                   (assq key map))
                 (let/ec escape
                   (for/fold ([A A])
-                            ([key+type (in-list map)])
+                            ([key+type (in-list map)]
+                             #:break (not A))
                     (match-define (list key type) key+type)
                     (define result (assq (car key+type) map*))
                     (or (and (not result) A)
@@ -694,7 +745,7 @@
         [(_ _) (continue A t1 t2)])])]
   [(case: Intersection (Intersection: t1s))
    (cond
-     [(for/or ([t1 (in-hset t1s)])
+     [(for/or ([t1 (in-list t1s)])
         (subtype* A t1 t2))]
      [else (continue A t1 t2)])]
   [(case: ListDots (ListDots: dty1 dbound1))
@@ -716,14 +767,14 @@
      [(? MPairTop?) A]
      [(MPair: t21 t22)
       (subtype-seq A
-                   (type-equiv? t11 t21)
-                   (type-equiv? t12 t22))]
+                   (type≡? t11 t21)
+                   (type≡? t12 t22))]
      ;; To check that mutable pair is a sequence we check that the cdr
      ;; is both an mutable list and a sequence 
      [(Sequence: (list seq-t))
       (subtype-seq A
                    (subtype* t11 seq-t)
-                   (subtype* t12 (Un -Null -MPairTop))
+                   (subtype* t12 null-or-mpair-top)
                    (subtype* t12 (make-Sequence (list seq-t))))]
      [_ (continue A t1 t2)])]
   [(case: Mu _)
@@ -826,8 +877,8 @@
      [(? Prompt-TagTop?) A]
      [(Prompt-Tagof: body2 handler2)
       (subtype-seq A
-                   (type-equiv? body1 body2)
-                   (type-equiv? handler1 handler2))]
+                   (type≡? body1 body2)
+                   (type≡? handler1 handler2))]
      [_ (continue A t1 t2)])]
   [(case: Refinement (Refinement: t1-parent id1))
    (match t2
@@ -866,7 +917,7 @@
      [(StructTop: (Struct: nm2 _ _ _ _ _))
       #:when (free-identifier=? nm1 nm2)
       A]
-     [(Value: (? (negate struct?) _)) #f]
+     [(Val-able: (? (negate struct?) _)) #f]
      ;; subtyping on structs follows the declared hierarchy
      [_ (cond
           [(and (Type? parent1)
@@ -886,26 +937,29 @@
   [(case: ThreadCell (ThreadCell: elem1))
    (match t2
      [(? ThreadCellTop?) A]
-     [(ThreadCell: elem2) (type-equiv? A elem1 elem2)]
+     [(ThreadCell: elem2) (type≡? A elem1 elem2)]
      [_ (continue A t1 t2)])]
-  [(case: Union (Union: elems1))
+  [(case: Union (Union/set: base1 ts1 elems1))
    (cond
      [(cache-ref union-sub-cache t1 t2)
       => (λ (b) (and (unbox b) A))]
      [else
       (define result
-        (match t2
-          [(Union: elems2)
-           (for/fold ([A A])
-                     ([elem1 (in-hset elems1)]
-                      #:break (not A))
-             (if (hset-member? elems2 elem1)
-                 A
-                 (subtype* A elem1 t2)))]
-          [_ (for/fold ([A A])
-                       ([elem1 (in-hset elems1)]
-                        #:break (not A))
-               (subtype* A elem1 t2))]))
+        (let ([A (subtype* A base1 t2)])
+          (and A
+               (match t2
+                 [(Union/set: base2 ts2 elems2)
+                  (for/fold ([A A])
+                            ([elem1 (in-list ts1)]
+                             #:break (not A))
+                    (cond
+                      [(set-member? elems2 elem1) A]
+                      [(subtype* A elem1 base2)]
+                      [else (subtype* A elem1 t2)]))]
+                 [_ (for/fold ([A A])
+                              ([elem1 (in-list ts1)]
+                               #:break (not A))
+                      (subtype* A elem1 t2))]))))
       (when (null? A)
         (cache-set! union-sub-cache t1 t2 (and result #t)))
       result])]
@@ -924,22 +978,19 @@
      [_ (continue A t1 t2)])]
   [(case: Value (Value: val1))
    (match t2
-     [(Base: _ _ pred _) (and (pred val1) A)]
+     [(Base-predicate: pred) (and (pred val1) A)]
+     [(BaseUnion-bases: bs)
+      (for*/or ([b (in-list bs)]
+                [pred (in-value (Base-predicate b))])
+        (and (pred val1) A))]
      [(Sequence: (list seq-t))
       (cond
-        [(null? val1) A]
         [(exact-nonnegative-integer? val1)
-         (define possibilities
-           (list
-            (list byte? -Byte)
-            (list portable-index? -Index)
-            (list portable-fixnum? -NonNegFixnum)
-            (list values -Nat)))
          (define type
-           (for/or ([pred-type (in-list possibilities)])
-             (match pred-type
-               [(list pred? type)
-                (and (pred? val1) type)])))
+           (for*/or ([pred/type (in-list value-numeric-seq-possibilities)]
+                     [pred? (in-value (car pred/type))]
+                     #:when (pred? val1))
+             (cdr pred/type)))
          (subtype* A type seq-t)]
         [else #f])]
      [(or (? Struct? s1) (NameStruct: s1))
@@ -949,12 +1000,12 @@
   [(case: Vector (Vector: elem1))
    (match t2
      [(? VectorTop?) A]
-     [(Vector: elem2) (type-equiv? A elem1 elem2)]
+     [(Vector: elem2) (type≡? A elem1 elem2)]
      [(Sequence: (list seq-t)) (subtype* A elem1 seq-t)]
      [_ (continue A t1 t2)])]
   [(case: Weak-Box (Weak-Box: elem1))
    (match t2
      [(? Weak-BoxTop?) A]
-     [(Weak-Box: elem2) (type-equiv? A elem1 elem2)]
+     [(Weak-Box: elem2) (type≡? A elem1 elem2)]
      [_ (continue A t1 t2)])]
   [else: (continue A t1 t2)])
diff --git a/typed-racket-lib/typed-racket/types/union.rkt b/typed-racket-lib/typed-racket/types/union.rkt
index d446b631..4822a111 100644
--- a/typed-racket-lib/typed-racket/types/union.rkt
+++ b/typed-racket-lib/typed-racket/types/union.rkt
@@ -1,7 +1,6 @@
 #lang racket/base
 
 (require "../utils/utils.rkt"
-         (utils hset)
          (rep type-rep rep-utils)
          (prefix-in c: (contract-req))
          (types subtype base-abbrev resolve current-seen)
@@ -27,20 +26,11 @@
 ;; The output is a non overlapping hset of non Union types.
 (define (merge t ts)
   (let ([t (normalize-type t)])
-    (define t* (make-Union ts))
+    (define t* (apply Un ts))
     (cond
-      [(subtype t* t) (hset t)]
+      [(subtype t* t) (list t)]
       [(subtype t t*) ts]
-      [else (hset-add (hset-filter ts (λ (b-elem) (not (subtype b-elem t))))
-                      t)])))
-
-;; list[Type] -> hset[Type]
-(define (flatten ts)
-  (for/fold ([s (hset)])
-            ([t (in-hset ts)])
-    (match t
-      [(Union: ts) (hset-union s ts)]
-      [_ (hset-add s t)])))
+      [else (cons t (filter-not (λ (ts-elem) (subtype ts-elem t)) ts))])))
 
 ;; Recursively reduce unions so that they do not contain
 ;; reduntant information w.r.t. subtyping. We used to maintain
@@ -49,7 +39,6 @@
 ;; don't want to do redundant runtime checks, etc.
 (define (normalize-type t)
   (match t
-    [(Union: ts) (make-Union (for/fold ([ts (hset)])
-                                       ([t (in-hset (flatten ts))])
-                               (merge t ts)))]
+    [(? BaseUnion?) t]
+    [(Union-all-flat: ts) (apply Un (foldl merge '() ts))]
     [_ (Rep-fmap t normalize-type)]))
diff --git a/typed-racket-lib/typed-racket/types/update.rkt b/typed-racket-lib/typed-racket/types/update.rkt
index 2f6bde85..cec66eb8 100644
--- a/typed-racket-lib/typed-racket/types/update.rkt
+++ b/typed-racket-lib/typed-racket/types/update.rkt
@@ -5,7 +5,7 @@
          (contract-req)
          (infer-in infer)
          (rep core-rep type-rep prop-rep object-rep values-rep rep-utils)
-         (utils tc-utils hset)
+         (utils tc-utils)
          (types resolve subtype subtract)
          (rename-in (types abbrev)
                     [-> -->]
@@ -78,12 +78,15 @@
           (make-Function
            (list (make-arr* doms (update rng rst))))]
          
-         [((Union: ts) _)
-          (Union-map ts (λ (t) (update t path)))]
+         [((Union: _ ts) _)
+          ;; Note: if there is a path element, then all Base types are
+          ;; incompatible with the type and we can therefore drop the
+          ;; bases from the union
+          (Union-fmap (λ (t) (update t path)) -Bottom ts)]
 
          [((Intersection: ts) _)
           (for/fold ([t Univ])
-                    ([elem (in-hset ts)])
+                    ([elem (in-list ts)])
             (intersect t (update elem path)))]
          
          [(_ _)
diff --git a/typed-racket-lib/typed-racket/utils/hset.rkt b/typed-racket-lib/typed-racket/utils/hset.rkt
deleted file mode 100644
index 129486a9..00000000
--- a/typed-racket-lib/typed-racket/utils/hset.rkt
+++ /dev/null
@@ -1,169 +0,0 @@
-#lang racket/base
-(require "utils.rkt"
-         (contract-req)
-         racket/match
-         (for-syntax racket/base racket/match))
-
-;; Lightweight variant of sets
-
-(provide hset hseteq hseteqv
-         hset?
-         hset-empty?
-         hset-member?
-         hset-count
-         hset-add
-         hset-remove
-         hset-first
-         hsubset?
-         hset-overlap?
-         hset=?
-         hset-subtract
-         hset-union
-         hset-intersect
-         hset-partition
-         hset-map
-         hset-filter
-         hset-for-each
-         hset->list
-         list->hset
-         list->hseteq
-         for/hset
-         for/hseteq
-         for/hseteqv
-         for*/hset
-         for*/hseteq
-         in-hset)
-
-(provide-for-cond-contract hsetof)
-
-(define-for-cond-contract (hsetof c) (hash/c c #t #:immutable #t #:flat? #t))
-
-(define build-hset
-  (case-lambda
-    [() #hash()]
-    [l (for/fold ([s #hash()]) ([e (in-list l)])
-         (hash-set s e #t))]))
-
-
-(define hset
-  (case-lambda
-    [() #hash()]
-    [l (for/fold ([s #hash()]) ([e (in-list l)])
-         (hash-set s e #t))]))
-
-(define hseteq
-  (case-lambda
-    [() #hasheq()]
-    [l (for/fold ([s #hasheq()]) ([e (in-list l)])
-         (hash-set s e #t))]))
-
-(define (hseteqv)
-  (case-lambda
-    [() #hasheqv()]
-    [l (for/fold ([s #hasheqv()]) ([e (in-list l)])
-         (hash-set s e #t))]))
-
-(define (hset? s) (hash? s))
-
-(define (hset-empty? s) (zero? (hash-count s)))
-(define (hset-member? s e) (hash-ref s e #f))
-(define (hset-count s) (hash-count s))
-
-(define (hset-add s e) (hash-set s e #t))
-(define (hset-remove s e) (hash-remove s e))
-(define (hset-first s) (hash-iterate-key s (hash-iterate-first s)))
-
-(define-syntax in-hset (make-rename-transformer #'in-immutable-hash-keys))
-
-(define (hsubset? s1 s2)
-  (hash-keys-subset? s1 s2))
-
-(define (hset-overlap? s1 s2)
-  (if ((hset-count s1) . < . (hset-count s2))
-      (hset-overlap? s2 s1)
-      (for/or ([k (in-hset s2)])
-        (hset-member? s1 k))))
-
-(define (hset=? s1 s2)
-  (or (eq? s1 s2)
-      (and (= (hash-count s1) (hash-count s2))
-           (hash-keys-subset? s1 s2))))
-
-(define (hset-subtract s1 s2)
-  (for/fold ([s1 s1]) ([k (in-hset s2)])
-    (hash-remove s1 k)))
-
-(define (hset-union s1 s2)
-  (if ((hset-count s1) . < . (hset-count s2))
-      (hset-union s2 s1)
-      (for/fold ([s1 s1]) ([k (in-hset s2)])
-        (hash-set s1 k #t))))
-
-(define (hset-intersect s1 s2)
-  (if ((hset-count s1) . < . (hset-count s2))
-      (hset-union s2 s1)
-      (for/fold ([s s2]) ([k (in-hset s2)])
-        (if (hash-ref s1 k #f)
-            s
-            (hash-remove s k)))))
-
-(define (hset-partition s pred empty-y-set empty-n-set)
-  (for/fold ([y empty-y-set] [n empty-n-set]) ([v (in-hset s)])
-    (if (pred v)
-        (values (hset-add y v) n)
-        (values y (hset-add n v)))))
-
-(define (hset->list s) (hash-keys s))
-
-(define (list->hset l)
-  (for/hset ([k (in-list l)])
-    k))
-
-(define (list->hseteq l)
-  (for/hseteq ([k (in-list l)])
-    k))
-
-(define (hset-map h f)
-  (for/fold ([result '()])
-            ([x (in-hset h)])
-    (cons (f x) result)))
-
-(define (hset-filter h f)
-  (for/fold ([result h])
-            ([x (in-hset h)])
-    (if (f x)
-        result
-        (hset-remove result x))))
-
-(define (hset-for-each h f)
-  (for ([x (in-hset h)]) (f x)))
-
-(define-syntax-rule (for/hset bindings body ...)
-  (for/hash bindings (values
-                      (let ()
-                        body ...)
-                      #t)))
-
-(define-syntax-rule (for/hseteq bindings body ...)
-  (for/hasheq bindings (values
-                        (let ()
-                          body ...)
-                        #t)))
-
-(define-syntax-rule (for/hseteqv bindings body ...)
-  (for/hasheqv bindings (values
-                         (let ()
-                           body ...)
-                         #t)))
-
-(define-syntax-rule (for*/hset bindings body ...)
-  (for*/hash bindings (values
-                       (let ()
-                         body ...)
-                       #t)))
-
-(define-syntax-rule (for*/hseteq bindings body ...)
-  (for*/hasheq bindings (values
-                         (let ()
-                           body ...)
-                         #t)))
diff --git a/typed-racket-test/unit-tests/infer-tests.rkt b/typed-racket-test/unit-tests/infer-tests.rkt
index b4a7096f..8885f04c 100644
--- a/typed-racket-test/unit-tests/infer-tests.rkt
+++ b/typed-racket-test/unit-tests/infer-tests.rkt
@@ -268,7 +268,7 @@
 
    [infer-t
     (-lst (-mu A (Un (-v b) (-lst A))))
-    (-mu C (Un (-v b2) (-lst C)))
+    (-mu C (Un (-lst C) (-v b2)))
     #:vars '(b2)
     #:result [(-vec (-v b2)) (-vec (-lst (-mu A (Un (-v b) (-lst A)))))]]
 
diff --git a/typed-racket-test/unit-tests/remove-intersect-tests.rkt b/typed-racket-test/unit-tests/remove-intersect-tests.rkt
index 478636ec..15b8833a 100644
--- a/typed-racket-test/unit-tests/remove-intersect-tests.rkt
+++ b/typed-racket-test/unit-tests/remove-intersect-tests.rkt
@@ -25,7 +25,7 @@
     [(_ [t1 t2 res] ...)
      #'(test-suite "Tests for intersect"
                    (test-check (format "~a ~a" 't1 't2)
-                               type-compare?
+                               type-equiv?
                                (intersect t1 t2) res) ...)]))
 
 
@@ -65,12 +65,18 @@
     [(_ [t1 t2 res] ...)
      (syntax/loc stx
        (test-suite "Tests for subtract"
-                   (test-check (format "~a ~a" 't1 't2) type-compare? (subtract t1 t2) res) ...))]))
+                   (test-check (format "~a ~a" 't1 't2) type-equiv? (subtract t1 t2) res) ...))]))
 
 (define subtract-tests
   (remo-tests
    [(Un -Number -Symbol) -Number -Symbol]
    [-Number -Number (Un)]
+   [(Un -Zero -Symbol (make-Listof Univ))
+    -Zero
+    (Un -Symbol (make-Listof Univ))]
+   [(-mu x (Un -Zero -Symbol (make-Listof x)))
+    -Zero
+    (Un -Symbol (make-Listof (-mu x (Un -Zero -Symbol (make-Listof x)))))]
    [(-mu x (Un -Number -Symbol (make-Listof x)))
     -Number
     (Un -Symbol (make-Listof (-mu x (Un -Number -Symbol (make-Listof x)))))]
diff --git a/typed-racket-test/unit-tests/subtype-tests.rkt b/typed-racket-test/unit-tests/subtype-tests.rkt
index 8cafe610..fce4d2bf 100644
--- a/typed-racket-test/unit-tests/subtype-tests.rkt
+++ b/typed-racket-test/unit-tests/subtype-tests.rkt
@@ -207,7 +207,7 @@
     [FAIL (-channel -String) (-evt -Int)]
     [-Log-Receiver (-evt (make-HeterogeneousVector
                           (list -Symbol -String Univ
-                                (Un (-val #f) -Symbol))))]
+                                (Un -False -Symbol))))]
     [FAIL -Log-Receiver (-evt -Int)])
    (subtyping-tests
     "Sequence special cases"
@@ -228,6 +228,7 @@
     [(-pair -String (-lst -String)) (-seq -String)]
     [FAIL (-pair -String (-lst -Symbol)) (-seq -String)]
     [FAIL (-pair -String (-vec -String)) (-seq -String)]
+    [-Null (-seq -String)]
     [(-mpair -String -Null) (-seq -String)]
     [(-mlst -String) (-seq -String)]
     [(-mpair -String (-mlst -String)) (-seq -String)]
@@ -246,6 +247,8 @@
    [(Un (-pair Univ (-lst Univ)) -Null) (-lst Univ)]
    [(-lst* -Number -Number (-val 'foo)) (-lst Univ)]
    [(Un (-val #f) (Un (-val 6) (-val 7))) (-mu x (Un -Number (Un -Boolean -Symbol)))]
+   [(-mu x (Un -Zero (make-Listof x)))
+    (-mu x (Un -Number (make-Listof x)))]
    [(Un -Number (-val #f) (-mu x (Un -Number -Symbol (make-Listof x))))
     (-mu x (Un -Number -Symbol -Boolean (make-Listof x)))]
    ;; sexps vs list*s of nums
@@ -309,6 +312,8 @@
    [(Un -Number -Symbol) (Un -Symbol -Number)]
    [(Un (-val 6) (-val 7)) -Number]
    [(Un (-val #f) (Un (-val 6) (-val 7))) (Un -Number (Un -Boolean -Symbol))]
+   [(Un -Number (-pair -Number -Number)) (Un -Number -Symbol (-pair Univ Univ))]
+   [(Un -Number -Symbol (-pair -Number -Number)) (Un -Number -Symbol (-pair Univ Univ))]
    ;; intersections
    [(-unsafe-intersect -Number) -Number]
    [(-unsafe-intersect -Number -Symbol) -Number]
@@ -373,11 +378,11 @@
    [(-poly (a) (a . -> . a)) top-func]
    [FAIL (-> Univ) (null Univ . ->* . Univ)]
 
-   [(-poly (b) ((Un (make-Base 'foo #'dummy values #f)
+   [(-poly (b) ((Un (make-Opaque #'dummy)
                     (-struct #'bar #f
                              (list (make-fld -Number #'values #f) (make-fld b #'values #f))))
                 . -> . (-lst b)))
-    ((Un (make-Base 'foo #'dummy values #f) (-struct #'bar #f (list (make-fld -Number #'values #f) (make-fld (-pair -Number (-v a)) #'values #f))))
+    ((Un (make-Opaque #'dummy) (-struct #'bar #f (list (make-fld -Number #'values #f) (make-fld (-pair -Number (-v a)) #'values #f))))
      . -> . (-lst (-pair -Number (-v a))))]
    [(-poly (b) ((-struct #'bar #f (list (make-fld -Number #'values #f) (make-fld b #'values #f))) . -> . (-lst b)))
     ((-struct #'bar #f (list (make-fld -Number #'values #f) (make-fld (-pair -Number (-v a)) #'values #f)))
diff --git a/typed-racket-test/unit-tests/type-equal-tests.rkt b/typed-racket-test/unit-tests/type-equal-tests.rkt
index fa4620b2..dc6ba3db 100644
--- a/typed-racket-test/unit-tests/type-equal-tests.rkt
+++ b/typed-racket-test/unit-tests/type-equal-tests.rkt
@@ -8,7 +8,7 @@
 (provide tests)
 (gen-test-main)
 
-(define (-base x) (make-Base x #'dummy values #f))
+(define (-opaque x) (make-Opaque x))
 
 
 (define-syntax (te-tests stx)
@@ -38,9 +38,15 @@
    ;; found bug
    [FAIL (Un (-mu heap-node
                   (-struct #'heap-node #f
-                           (map fld* (list (-base 'comparator) -Number (-v a) (Un heap-node (-base 'heap-empty))))))
-             (-base 'heap-empty))
+                           (map fld* (list (-opaque #'comparator)
+                                           -Number
+                                           (-v a)
+                                           (Un heap-node (-opaque #'heap-empty))))))
+             (-opaque #'heap-empty))
          (Un (-mu heap-node
                   (-struct #'heap-node #f
-                           (map fld* (list (-base 'comparator) -Number (-pair -Number -Number) (Un heap-node (-base 'heap-empty))))))
-             (-base 'heap-empty))]))
+                           (map fld* (list (-opaque #'comparator)
+                                           -Number
+                                           (-pair -Number -Number)
+                                           (Un heap-node (-opaque #'heap-empty))))))
+             (-opaque #'heap-empty))]))