diff --git a/typed-racket-lib/typed-racket/infer/intersect.rkt b/typed-racket-lib/typed-racket/infer/intersect.rkt
index 4c755651..9334ebb2 100644
--- a/typed-racket-lib/typed-racket/infer/intersect.rkt
+++ b/typed-racket-lib/typed-racket/infer/intersect.rkt
@@ -2,7 +2,7 @@
 
 (require "../utils/utils.rkt")
 (require (rep type-rep)
-         (types abbrev base-abbrev union subtype remove-intersect resolve)
+         (types abbrev base-abbrev union subtype resolve)
          "signatures.rkt"
          racket/match
          racket/set)
@@ -21,54 +21,51 @@
   ;; (i.e. pairs of t1 t2) to prevent infinite unfolding.
   ;; subtyping performs a similar check for the same
   ;; reason
-  (define (intersect* t1 t2 resolved)
-    (match* (t1 t2)
+  (let intersect
+    ([t1 t1] [t2 t2] [resolved (set)])
+    (match*/no-order
+     (t1 t2)
       ;; already a subtype
-      [(_ _) #:when (subtype t1 t2) t1]
-      [(_ _) #:when (subtype t2 t1) t2]
+      [(t1 t2) #:no-order #:when (subtype t1 t2) t1]
       
       ;; polymorphic intersect
-      [(_ (Poly: vars t))
+      [(t1 (Poly: vars t))
+       #:no-order
        #:when (infer vars null (list t1) (list t) #f)
        t1]
       
       ;; structural recursion on types
       [((Pair: a1 d1) (Pair: a2 d2)) 
        (build-type -pair 
-                   (intersect* a1 a2 resolved) 
-                   (intersect* d1 d2 resolved))]
+                   (intersect a1 a2 resolved) 
+                   (intersect 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*))
-       (build-type -Syntax (intersect* t1* t2* resolved))]
+       (build-type -Syntax (intersect t1* t2* resolved))]
       [((Promise: t1*) (Promise: t2*))
-       (build-type -Promise (intersect* t1* t2* resolved))]
+       (build-type -Promise (intersect t1* t2* resolved))]
       
       ;; unions
-      [((Union: t1s) _) (apply Un (map (λ (t1*) (intersect* t1* t2 resolved)) t1s))]
-      [(_ (Union: t2s)) (apply Un (map (λ (t2*) (intersect* t1 t2* resolved)) t2s))]
+      [((Union: t1s) t2)
+       #:no-order
+       (apply Un (map (λ (t1) (intersect t1 t2 resolved)) t1s))]
 
       ;; intersections
-      [((Intersection: t1s) _)
+      [((Intersection: t1s) t2)
+       #:no-order
        (apply -unsafe-intersect (for/list ([t1 (in-immutable-set t1s)])
-                                  (intersect* t1 t2 resolved)))]
-      [(_ (Intersection: t2s))
-       (apply -unsafe-intersect (for/list ([t2 (in-immutable-set t2s)])
-                                  (intersect* t1 t2 resolved)))]
+                                  (intersect t1 t2 resolved)))]
       
       ;; resolve resolvable types if we haven't already done so
-      [((? needs-resolving?) _)
-       #:when (and (not (set-member? resolved (cons t1 t2)))
-                   (not (set-member? resolved (cons t2 t1))))
-       (intersect* (resolve t1) t2 (set-add resolved (cons t1 t2)))]
-      [(_ (? needs-resolving?))
-       #:when (and (not (set-member? resolved (cons t1 t2)))
-                   (not (set-member? resolved (cons t2 t1))))
-       (intersect* t1 (resolve t2) (set-add resolved (cons t1 t2)))]
+      [((? needs-resolving? t1) t2)
+       #:no-order
+       #:when (not (or (set-member? resolved (cons t1 t2))
+                       (set-member? resolved (cons t2 t1))))
+       (intersect (resolve t1) t2 (set-add resolved (cons t1 t2)))]
      
       ;; t2 and t1 have a complex relationship, so we build an intersection
       ;; (note: intersection checks for overlap)
-      [(_ _) (-unsafe-intersect t1 t2)]))
-  (intersect* t1 t2 (set)))
+      [(t1 t2) (-unsafe-intersect t1 t2)])))
diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt
index 880b063d..19c8cb92 100644
--- a/typed-racket-lib/typed-racket/rep/type-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt
@@ -55,7 +55,7 @@
 ;; Ugly hack - should use units
 (lazy-require
  ("../types/union.rkt" (Un))
- ("../types/remove-intersect.rkt" (overlap))
+ ("../types/overlap.rkt" (overlap?))
  ("../types/resolve.rkt" (resolve-app)))
 
 (define name-table (make-weak-hasheq))
@@ -495,7 +495,7 @@
          [(Univ:) (loop elems ts)]
          [(Intersection: ts*) (loop (set-union elems ts*) ts)]
          [t (cond
-              [(for/or ([elem (in-immutable-set elems)]) (not (overlap elem t)))
+              [(for/or ([elem (in-immutable-set elems)]) (not (overlap? elem t)))
                (*Union (list))]
               [else (loop (set-add elems t) ts)])])])))
 
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt b/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
index 8f145a4e..c2cda2b1 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
@@ -1,13 +1,12 @@
 #lang racket/base
 
-(require (rename-in "../utils/utils.rkt" [infer infer-in]))
-(require racket/match racket/list
+(require "../utils/utils.rkt"
+         racket/match racket/list
          (for-syntax racket/base syntax/parse)
          (contract-req)
-         (infer-in infer)
          (rep type-rep prop-rep object-rep rep-utils)
          (utils tc-utils)
-         (types tc-result resolve subtype remove-intersect union prop-ops)
+         (types tc-result resolve subtype remove update union prop-ops)
          (env type-env-structs lexical-env)
          (rename-in (types abbrev)
                     [-> -->]
@@ -17,70 +16,6 @@
 
 (provide with-lexical-env/extend-props)
 
-
-(define/cond-contract (update t new-t pos? lo)
-  (Type/c Type/c boolean? (listof PathElem?) . -> . Type/c)
-  ;; build-type: build a type while propogating bottom
-  (define (build-type constructor . args)
-    (if (memf Bottom? args) -Bottom (apply constructor args)))
-  (match* ((resolve t) lo)
-    ;; pair ops
-    [((Pair: t s) (list rst ... (CarPE:)))
-     (build-type -pair (update t new-t pos? rst) s)]
-    [((Pair: t s) (list rst ... (CdrPE:)))
-     (build-type -pair t (update s new-t pos? rst))]
-
-    ;; syntax ops
-    [((Syntax: t) (list rst ... (SyntaxPE:)))
-     (build-type -Syntax (update t new-t pos? rst))]
-
-    ;; promise op
-    [((Promise: t) (list rst ... (ForcePE:)))
-     (build-type -Promise (update t new-t pos? rst))]
-
-    ;; struct ops
-    [((Struct: nm par flds proc poly pred)
-      (list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx)))
-     ;; note: this updates fields regardless of whether or not they are
-     ;; a polymorphic field. Because subtyping is nominal and accessor 
-     ;; functions do not reflect this, this behavior is unobservable
-     ;; except when an a variable aliases the field in a let binding
-     (let*-values ([(lhs rhs) (split-at flds idx)]
-                   [(ty* acc-id) (match rhs
-                                   [(cons (fld: ty acc-id #f) _)
-                                    (values (update ty new-t pos? rst) acc-id)]
-                                   [_ (int-err "update on mutable struct field")])]) 
-       (cond 
-        [(Bottom? ty*) ty*]
-        [else (let ([flds* (append lhs (cons (make-fld ty* acc-id #f) (cdr rhs)))])
-                (make-Struct nm par flds* proc poly pred))]))]
-
-    ;; class field ops
-    ;;
-    ;; A refinement of a private field in a class is really a refinement of the
-    ;; return type of the accessor function for that field (rather than a variable).
-    ;; We cannot just refine the type of the argument to the accessor, since that
-    ;; is an object type that doesn't mention private fields. Thus we use the
-    ;; FieldPE path element as a marker to refine the result of the accessor
-    ;; function.
-    [((Function: (list (arr: doms (Values: (list (Result: rng _ _))) _ _ _)))
-      (list rst ... (FieldPE:)))
-     (make-Function
-      (list (make-arr* doms (update rng new-t pos? rst))))]
-
-    ;; otherwise
-    [(t '())
-     (if pos?
-         (intersect t new-t)
-         (remove t new-t))]
-    [((Union: ts) lo)
-     (apply Un (map (λ (t) (update t new-t pos? lo)) ts))]
-    [(t* lo)
-     ;; This likely comes up with (-lst t) and we need to improve the system to make sure this case
-     ;; dosen't happen
-     ;;(int-err "update along ill-typed path: ~a ~a ~a" t t* lo)
-     t]))
-
 ;; Returns #f if anything becomes (U)
 (define (env+ env ps)
   (let/ec exit*
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
index 0ba725f5..00de9951 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
@@ -6,7 +6,7 @@
          "signatures.rkt"
          "check-below.rkt" "../types/kw-types.rkt"
          (types utils abbrev union subtype type-table path-type
-                prop-ops remove-intersect resolve generalize)
+                prop-ops overlap resolve generalize)
          (private-in syntax-properties)
          (rep type-rep prop-rep object-rep)
          (only-in (infer infer) intersect)
@@ -54,7 +54,7 @@
   (define ty (path-type alias-path (lookup-type/lexical alias-id)))
   
   (ret ty
-       (if (overlap ty (-val #f))
+       (if (overlap? ty (-val #f))
            (-PS (-not-type obj (-val #f)) (-is-type obj (-val #f)))
            -true-propset)
        obj))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
index 9699e98c..0472dd86 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
@@ -1,7 +1,7 @@
 #lang racket/unit
 
 (require "../utils/utils.rkt"
-         (except-in (types utils abbrev prop-ops remove-intersect type-table)
+         (except-in (types utils abbrev prop-ops overlap type-table)
                     -> ->* one-of/c)
          (only-in (types abbrev) (-> t:->) [->* t:->*])
          (private type-annotation parse-type syntax-properties)
@@ -65,7 +65,7 @@
                                      [f- (in-list fs-)]
                                      [o (in-list os)])
                             (cond
-                              [(not (overlap t (-val #f)))
+                              [(not (overlap? t (-val #f)))
                                (list f+)]
                               [(is-var-mutated? n)
                                (list)]
diff --git a/typed-racket-lib/typed-racket/types/overlap.rkt b/typed-racket-lib/typed-racket/types/overlap.rkt
new file mode 100644
index 00000000..26f2d9f3
--- /dev/null
+++ b/typed-racket-lib/typed-racket/types/overlap.rkt
@@ -0,0 +1,106 @@
+#lang racket/base
+
+(require "../utils/utils.rkt"
+         (rep type-rep rep-utils)
+         (types abbrev subtype resolve utils)
+         racket/match racket/set)
+
+
+(provide overlap?)
+
+(define (simple-datum? v)
+  (or (null? v)
+      (symbol? v)
+      (number? v)
+      (boolean? v)
+      (pair? v)
+      (string? v)
+      (keyword? v)
+      (char? v)
+      (void? v)
+      (eof-object? v)))
+
+;; overlap?
+;; Type Type -> Boolean
+;; a conservative check to see if two types
+;; have a non-empty intersection
+(define/cond-contract (overlap? t1 t2)
+  (-> Type/c Type/c boolean?)
+  (define k1 (Type-key t1))
+  (define k2 (Type-key t2))
+  (cond
+    [(type-equal? t1 t2) #t]
+    [(and (symbol? k1) (symbol? k2) (not (eq? k1 k2))) #f]
+    [(and (symbol? k1) (pair? k2) (not (memq k1 k2))) #f]
+    [(and (symbol? k2) (pair? k1) (not (memq k2 k1))) #f]
+    [(and (pair? k1) (pair? k2)
+          (for/and ([i (in-list k1)]) (not (memq i k2))))
+     #f]
+    [else
+     (match*/no-order
+      (t1 t2)
+      [((Univ:) _) #:no-order #t]
+      [((or (B: _) (F: _)) _) #:no-order #t]
+      [((Opaque: _) _) #:no-order #t]
+      [((Name/simple: n) (Name/simple: n*))
+       (or (free-identifier=? n n*)
+           (overlap? (resolve-once t1) (resolve-once t2)))]
+      [(t (? Name? s))
+       #:no-order
+       (overlap? t (resolve-once s))]
+      [((? Mu? t) s) #:no-order (overlap? (unfold t) s)]
+      [((Refinement: t _) s) #:no-order (overlap? t s)]
+      [((Union: ts) s)
+       #:no-order
+       (ormap (λ (t) (overlap? t s)) ts)]
+      [((Intersection: ts) s)
+       #:no-order
+       (for/and ([t (in-immutable-set ts)])
+         (overlap? t s))]
+      [((? Poly?) _) #:no-order #t] ;; conservative
+      [((Base: s1 _ _ _) (Base: s2 _ _ _)) (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]
+      [((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: _) _) #:no-order #t]
+      ;; Values where evt? produces #f cannot be Evt
+      [((Evt: _) (Value: v)) #:no-order (evt? v)]
+      [((Pair: _ _) _) #:no-order #f]
+      [((Value: (? simple-datum? v1))
+        (Value: (? simple-datum? v2)))
+       (equal? v1 v2)]
+      [((Value: (? simple-datum?))
+        (or (? Struct?) (? StructTop?) (? Function?)))
+       #:no-order
+       #f]
+      [((Value: (not (? hash?)))
+        (or (? Hashtable?) (? HashtableTop?)))
+       #:no-order
+       #f]
+      [((Struct: n _ flds _ _ _)
+        (Struct: n* _ flds* _ _ _)) 
+       #:when (free-identifier=? n n*)
+       (for/and ([f (in-list flds)] [f* (in-list flds*)])
+         (match* (f f*)
+           [((fld: t _ _) (fld: t* _ _)) (overlap? t t*)]))]
+      [((Struct: n #f _ _ _ _)
+        (StructTop: (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* _ _ _))
+       #f]
+      [((Struct: n #f flds _ _ _)
+        (StructTop: (Struct: n* #f flds* _ _ _)))
+       #f]
+      [((and t1 (Struct: _ _ _ _ #f _))
+        (and t2 (Struct: _ _ _ _ #f _)))
+       (or (subtype t1 t2) (subtype t2 t1))]
+      [(_ _) #t])]))
diff --git a/typed-racket-lib/typed-racket/types/prop-ops.rkt b/typed-racket-lib/typed-racket/types/prop-ops.rkt
index aa3ee306..1b5e5fbd 100644
--- a/typed-racket-lib/typed-racket/types/prop-ops.rkt
+++ b/typed-racket-lib/typed-racket/types/prop-ops.rkt
@@ -5,7 +5,7 @@
          (prefix-in c: (contract-req))
          (rep type-rep prop-rep object-rep rep-utils)
          (only-in (infer infer) intersect)
-         (types union subtype remove-intersect abbrev tc-result))
+         (types union subtype overlap abbrev tc-result))
 
 (provide/cond-contract
   [-and (c:->* () #:rest (c:listof Prop?) Prop?)]
@@ -80,7 +80,7 @@
      (subtype t2 t1)]
     ;; t1 ∩ t2 = ∅ ?
     [((TypeProp: o t1) (NotTypeProp: o t2))
-     (not (overlap t1 t2))]
+     (not (overlap? t1 t2))]
     ;; otherwise we give up
     [(_ _) #f]))
 
diff --git a/typed-racket-lib/typed-racket/types/remove-intersect.rkt b/typed-racket-lib/typed-racket/types/remove-intersect.rkt
deleted file mode 100644
index f97fd534..00000000
--- a/typed-racket-lib/typed-racket/types/remove-intersect.rkt
+++ /dev/null
@@ -1,120 +0,0 @@
-#lang racket/base
-
-(require "../utils/utils.rkt"
-         (rep type-rep rep-utils)
-         (types union subtype resolve utils)
-         racket/match racket/set)
-
-(provide (rename-out [*remove remove]) overlap)
-
-(define (simple-datum? v)
-  (or (null? v)
-      (symbol? v)
-      (number? v)
-      (boolean? v)
-      (pair? v)
-      (string? v)
-      (keyword? v)
-      (char? v)
-      (void? v)
-      (eof-object? v)))
-
-
-(define (overlap t1 t2)
-  (let ([ks (Type-key t1)] [kt (Type-key t2)])
-    (cond
-      [(type-equal? t1 t2) #t]
-      [(and (symbol? ks) (symbol? kt) (not (eq? ks kt))) #f]
-      [(and (symbol? ks) (pair? kt) (not (memq ks kt))) #f]
-      [(and (symbol? kt) (pair? ks) (not (memq kt ks))) #f]
-      [(and (pair? ks) (pair? kt)
-            (for/and ([i (in-list ks)]) (not (memq i kt))))
-       #f]
-      [else
-       (match (list t1 t2)
-         [(list-no-order (Univ:) _) #t]
-         [(list-no-order (or (B: _) (F: _)) _) #t]
-         [(list-no-order (Opaque: _) _) #t]
-         [(list (Name/simple: n) (Name/simple: n*))
-          (or (free-identifier=? n n*)
-              (overlap (resolve-once t1) (resolve-once t2)))]
-         [(list-no-order t (? Name? s))
-           (overlap t (resolve-once s))]
-         [(list-no-order (? Mu? t) s) (overlap (unfold t) s)]
-         [(list-no-order (Refinement: t _) s) (overlap t s)]
-         [(list-no-order (Union: ts) s)
-          (ormap (lambda (t*) (overlap t* s)) ts)]
-         [(list-no-order (Intersection: ts) s)
-          (for/and ([t (in-immutable-set ts)])
-            (overlap t s))]
-         [(list-no-order (? Poly?) _) #t] ;; conservative
-         [(list (Base: s1 _ _ _) (Base: s2 _ _ _)) (or (subtype t1 t2) (subtype t2 t1))]
-         [(list-no-order (? Base? t) (? Value? s)) (subtype s t)] ;; conservative
-         [(list (Syntax: t) (Syntax: t*)) (overlap t t*)]
-         [(list-no-order (Syntax: _) _) #f]
-         [(list-no-order (Base: _ _ _ _) _) #f]
-         [(list-no-order (Value: (? pair?)) (Pair: _ _)) #t]
-         [(list (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
-         [(list-no-order (Sequence: _) (Value: v)) (sequence? v)]
-         [(list-no-order (Sequence: _) _) #t]
-         ;; Values where evt? produces #f cannot be Evt
-         [(list-no-order (Evt: _) (Value: v)) (evt? v)]
-         [(list-no-order (Pair: _ _) _) #f]
-         [(list (Value: (? simple-datum? v1))
-                (Value: (? simple-datum? v2)))
-          (equal? v1 v2)]
-         [(list-no-order (Value: (? simple-datum?))
-                         (or (? Struct?) (? StructTop?) (? Function?)))
-          #f]
-         [(list-no-order (Value: (not (? hash?)))
-                         (or (? Hashtable?) (? HashtableTop?)))
-          #f]
-         [(list (Struct: n _ flds _ _ _)
-                (Struct: n* _ flds* _ _ _)) 
-          #:when (free-identifier=? n n*)
-          (for/and ([f (in-list flds)] [f* (in-list flds*)])
-            (match* (f f*)
-              [((fld: t _ _) (fld: t* _ _)) (overlap t t*)]))]
-         [(list (Struct: n #f _ _ _ _)
-                (StructTop: (Struct: n* #f _ _ _ _))) 
-          #:when (free-identifier=? n n*)
-          #t]
-         ;; n and n* must be different, so there's no overlap
-         [(list (Struct: n #f flds _ _ _)
-                (Struct: n* #f flds* _ _ _))
-          #f]
-         [(list (Struct: n #f flds _ _ _)
-                (StructTop: (Struct: n* #f flds* _ _ _)))
-          #f]
-         [(list (and t1 (Struct: _ _ _ _ #f _))
-                (and t2 (Struct: _ _ _ _ #f _)))
-          (or (subtype t1 t2) (subtype t2 t1))]
-         [else #t])])))
-
-
-;(trace overlap)
-
-;; also not yet correct
-;; produces old without the contents of rem
-(define (*remove old rem)
-  (define initial
-    (if (subtype old rem)
-        (Un) ;; the empty type
-        (match (list old rem)
-          [(list (or (App: _ _ _) (? Name?)) t)
-           ;; must be different, since they're not subtypes
-           ;; and n must refer to a distinct struct type
-           old]
-          [(list (Union: l) rem)
-           (apply Un (map (lambda (e) (*remove e rem)) l))]
-          [(list (Intersection: ts) rem)
-           (apply -unsafe-intersect
-                  (for/list ([t (in-immutable-set ts)]) (*remove t rem)))]
-          [(list (? Mu? old) t) (*remove (unfold old) t)]
-          [(list (Poly: vs b) t) (make-Poly vs (*remove b rem))]
-          [_ old])))
-  (if (subtype old initial) old initial))
-
-;(trace *remove)
diff --git a/typed-racket-lib/typed-racket/types/remove.rkt b/typed-racket-lib/typed-racket/types/remove.rkt
new file mode 100644
index 00000000..ff7cd61f
--- /dev/null
+++ b/typed-racket-lib/typed-racket/types/remove.rkt
@@ -0,0 +1,32 @@
+#lang racket/base
+
+(require "../utils/utils.rkt"
+         (rep type-rep rep-utils)
+         (types abbrev union subtype resolve utils)
+         racket/match racket/set)
+
+(provide remove)
+
+
+;; remove
+;; Type Type -> Type
+;; conservatively calculates set subtraction
+;; between the types (i.e. t - s)
+(define (remove t s)
+  (define result
+    (let rem ([t t])
+      (match 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) (apply Un (map rem elems))]
+        [(Intersection: ts)
+         (apply -unsafe-intersect (set-map ts rem))]
+        [(? Mu?) (rem (unfold t))]
+        [(Poly: vs b) (make-Poly vs (rem b))]
+        [_ t])))
+  (cond
+    [(subtype t result) t]
+    [else result]))
diff --git a/typed-racket-lib/typed-racket/types/subtype.rkt b/typed-racket-lib/typed-racket/types/subtype.rkt
index e5f46015..aafc26b0 100644
--- a/typed-racket-lib/typed-racket/types/subtype.rkt
+++ b/typed-racket-lib/typed-racket/types/subtype.rkt
@@ -480,14 +480,12 @@
                    (loop (cdr l1) (cdr l2))]
                   [else
                    (loop l1 (cdr l2))]))]
-         [((Union: es) t)
+         [((Union: elems) t)
           (and 
-           (for/and ([elem (in-list es)])
-             (subtype* A0 elem t))
+           (andmap (λ (elem) (subtype* A0 elem t)) elems)
            A0)]
-         [(s (Union: es))
-          (and (for/or ([elem (in-list es)])
-                 (subtype* A0 s elem))
+         [(s (Union: elems))
+          (and (ormap (λ (elem) (subtype* A0 s elem)) elems)
                A0)]
          ;; subtyping on immutable structs is covariant
          [((Struct: nm _ flds proc _ _) (Struct: nm* _ flds* proc* _ _)) 
diff --git a/typed-racket-lib/typed-racket/types/update.rkt b/typed-racket-lib/typed-racket/types/update.rkt
new file mode 100644
index 00000000..aea5a456
--- /dev/null
+++ b/typed-racket-lib/typed-racket/types/update.rkt
@@ -0,0 +1,91 @@
+#lang racket/base
+
+(require (rename-in "../utils/utils.rkt" [infer infer-in]))
+(require racket/match racket/list
+         (contract-req)
+         (infer-in infer)
+         (rep type-rep prop-rep object-rep rep-utils)
+         (utils tc-utils)
+         (types abbrev resolve subtype remove union))
+
+
+(provide update)
+
+;; update
+;; t          : type being updated
+;; new-t      : new type
+;; pos?       : whether the update is positive or negative
+;; path-elems : which fields we're traversing to update,
+;;   in *syntactic order* (e.g. (car (cdr x)) -> '(car cdr))  
+(define/cond-contract (update t new-t pos? path-elems)
+  (Type/c Type/c boolean? (listof PathElem?) . -> . Type/c)
+  ;; build-type: build a type while propogating bottom
+  (define (build constructor . args)
+    (if (memf Bottom? args) -Bottom (apply constructor args)))
+  ;; update's inner recursive loop
+  ;; puts path in *accessed* order
+  ;; (i.e. (car (cdr x)) --> (list cdr car))
+  (let update
+    ([t t] [path (reverse path-elems)])
+    (match path
+      ;; path is empty (base case)
+      [(list) (cond
+                [pos? (intersect (resolve t) new-t)]
+                [else (remove (resolve t) new-t)])]
+      ;; path is non-empty
+      ;; (i.e. there is some field access we'll try and traverse)
+      [(cons path-elem rst)
+       (match* ((resolve t) path-elem)
+         ;; pair ops
+         [((Pair: t s) (CarPE:))
+          (build -pair (update t rst) s)]
+         [((Pair: t s) (CdrPE:))
+          (build -pair t (update s rst))]
+         ;; syntax ops
+         [((Syntax: t) (SyntaxPE:))
+          (build -Syntax (update t rst))]
+         ;; promise op
+         [((Promise: t) (ForcePE:))
+          (build -Promise (update t rst))]
+         
+         ;; struct ops
+         [((Struct: nm par flds proc poly pred)
+           (StructPE: (? (λ (s) (subtype t s))) idx))
+          ;; Note: this updates fields even if they are not polymorphic.
+          ;; Because subtyping is nominal and accessor functions do not
+          ;; reflect this, this behavior is unobservable except when a
+          ;; variable aliases the field in a let binding
+          (define-values (lhs rhs) (split-at flds idx))
+          (define-values (ty* acc-id)
+            (match rhs
+              [(cons (fld: ty acc-id #f) _)
+               (values (update ty rst) acc-id)]
+              [_ (int-err "update on mutable struct field")]))
+          (cond 
+            [(Bottom? ty*) ty*]
+            [else
+             (define flds*
+               (append lhs (cons (make-fld ty* acc-id #f) (cdr rhs))))
+             (make-Struct nm par flds* proc poly pred)])]
+         
+         ;; class field ops
+         ;;
+         ;; A refinement of a private field in a class is really a refinement of the
+         ;; return type of the accessor function for that field (rather than a variable).
+         ;; We cannot just refine the type of the argument to the accessor, since that
+         ;; is an object type that doesn't mention private fields. Thus we use the
+         ;; FieldPE path element as a marker to refine the result of the accessor
+         ;; function.
+         [((Function: (list (arr: doms (Values: (list (Result: rng _ _))) _ _ _)))
+           (FieldPE:))
+          (make-Function
+           (list (make-arr* doms (update rng rst))))]
+         
+         [((Union: ts) _)
+          (apply Un (map (λ (t) (update t path)) ts))]
+         
+         [(_ _)
+          ;; This likely comes up with (-lst t) and we need to improve the system to make sure this case
+          ;; dosen't happen
+          ;;(int-err "update along ill-typed path: ~a ~a ~a" t t* lo)
+          t])])))
\ No newline at end of file
diff --git a/typed-racket-lib/typed-racket/utils/utils.rkt b/typed-racket-lib/typed-racket/utils/utils.rkt
index a41a61fa..f73c9abb 100644
--- a/typed-racket-lib/typed-racket/utils/utils.rkt
+++ b/typed-racket-lib/typed-racket/utils/utils.rkt
@@ -7,6 +7,7 @@ at least theoretically.
 
 (require (for-syntax racket/base syntax/parse/pre racket/string)
          racket/require-syntax racket/provide-syntax
+         racket/match
          racket/struct-info "timing.rkt")
 
 (provide
@@ -20,7 +21,8 @@ at least theoretically.
  list-extend
  filter-multiple
  syntax-length
- in-sequence-forever)
+ in-sequence-forever
+ match*/no-order)
 
 (define optimize? (make-parameter #t))
 (define-for-syntax enable-contracts? (and (getenv "PLT_TR_CONTRACTS") #t))
@@ -232,3 +234,22 @@ at least theoretically.
                (λ (_) #t)
                (λ _ #t)
                (λ _ #t))))))
+
+(define-syntax (match*/no-order stx)
+  (define (parse-clauses clauses)
+    (syntax-parse clauses
+      [() #'()]
+      [([(lpat rpat) #:no-order . body]
+        . rst)
+       #`([(lpat rpat) . body]
+          [(rpat lpat) . body]
+          . #,(parse-clauses #'rst))]
+      [((~and cl [(lpat rpat) . body])
+        . rst)
+       #`(#,(syntax/loc #'cl [(lpat rpat) . body])
+          . #,(parse-clauses #'rst))]))
+  (syntax-parse stx
+    [(_ (val1:expr val2:expr)
+        . clauses)
+     #`(match* (val1 val2)
+         . #,(parse-clauses #'clauses))]))
diff --git a/typed-racket-test/unit-tests/remove-intersect-tests.rkt b/typed-racket-test/unit-tests/remove-intersect-tests.rkt
index 3e0a4ed5..b06e350a 100644
--- a/typed-racket-test/unit-tests/remove-intersect-tests.rkt
+++ b/typed-racket-test/unit-tests/remove-intersect-tests.rkt
@@ -3,7 +3,7 @@
          (for-syntax racket/base)
          (r:infer infer)
          (rep type-rep)
-         (types abbrev numeric-tower subtype union remove-intersect)
+         (types abbrev numeric-tower subtype union remove overlap)
          rackunit)
 (provide tests)
 (gen-test-main)
@@ -12,7 +12,9 @@
   (syntax-case stx ()
     [(_ [t1 t2 res] ...)
      #'(test-suite "Tests for overlap"
-                   (test-check (format "~a ~a" 't1 't2) (lambda (a b) (eq? (not (not a)) b)) (overlap t1 t2) res) ...)]))
+                   (test-check (format "~a ~a" 't1 't2)
+                               (lambda (a b) (eq? (not (not a)) b))
+                               (overlap? t1 t2) res) ...)]))
 
 (define overlap-tests
   (over-tests
@@ -22,7 +24,9 @@
   (syntax-case stx ()
     [(_ [t1 t2 res] ...)
      #'(test-suite "Tests for intersect"
-                   (test-check (format "~a ~a" 't1 't2) type-compare? (intersect t1 t2) res) ...)]))
+                   (test-check (format "~a ~a" 't1 't2)
+                               type-compare?
+                               (intersect t1 t2) res) ...)]))
 
 
 (define intersect-tests
@@ -61,14 +65,20 @@
   (remo-tests
    [(Un -Number -Symbol) -Number -Symbol]
    [-Number -Number (Un)]
-   [(-mu x (Un -Number -Symbol (make-Listof x))) -Number (Un -Symbol (make-Listof (-mu x (Un -Number -Symbol (make-Listof x)))))]
-   [(-mu x (Un -Number -Symbol -Boolean (make-Listof x))) -Number (Un -Symbol -Boolean (make-Listof (-mu x (Un -Number -Symbol -Boolean (make-Listof x)))))]
+   [(-mu x (Un -Number -Symbol (make-Listof x)))
+    -Number
+    (Un -Symbol (make-Listof (-mu x (Un -Number -Symbol (make-Listof x)))))]
+   [(-mu x (Un -Number -Symbol -Boolean (make-Listof x)))
+    -Number
+    (Un -Symbol -Boolean (make-Listof (-mu x (Un -Number -Symbol -Boolean (make-Listof x)))))]
    [(Un (-val #f) (-mu x (Un -Number -Symbol (make-Listof (-v x)))))
     (Un -Boolean -Number)
     (Un -Symbol (make-Listof (-mu x (Un -Number -Symbol (make-Listof x)))))]
    [(Un (-val 'foo) (-val 6)) (Un -Number -Symbol) (Un)]
    [(-> (Un -Symbol -Number) -Number) (-> -Number -Number) (Un)]
-   [(Un (-poly (a) (make-Listof a)) (-> -Number -Number)) (-> -Number -Number) (-poly (a) (make-Listof a))]
+   [(Un (-poly (a) (make-Listof a)) (-> -Number -Number))
+    (-> -Number -Number)
+    (-poly (a) (make-Listof a))]
    [(Un -Symbol -Number) (-poly (a) -Number) -Symbol]
    [(-pair -Number (-v a)) (-pair Univ Univ) (Un)]
    ))