diff --git a/tapl/stlc+occurrence.rkt b/tapl/stlc+occurrence.rkt
index 32cb7f8..763c525 100644
--- a/tapl/stlc+occurrence.rkt
+++ b/tapl/stlc+occurrence.rkt
@@ -1,17 +1,24 @@
 #lang s-exp "typecheck.rkt"
 (extends "stlc+sub.rkt" #:except #%datum)
-;; TODO import if- form?
 
 ;; Calculus for occurrence typing.
 ;; - Types can be simple, or sets of simple types
-;;   (aka "ambiguous types".
-;;    The type is one of a few ambiguous possibilities at compile-time)
-;; - The U constructor makes ambiguous types
-;; - `(if-τ? [x : τ] e1 e2)` form will insert a run-time check to discriminate amb. types
-;; - For non-top types, τ is a subtype of (∪ τ1 ... τ τ2 ...)
+;;   (aka "ambiguous types";
+;;    the run-time value will have one of a few ambiguous possible types.)
+;; - The ∪ constructor makes ambiguous types
+;; - `(test [τ ? x] e1 e2)` form will insert a run-time check to discriminate ∪
+;; -- If the value at identifier x has type τ, then we continue to e1 with [x : τ]
+;; -- Otherwise, we move to e2 with [x : (- (typeof x) τ)].
+;;    i.e., [x : τ] is not possible
+;; - Subtyping rules:
+;; -- ALL : t ... <: t' => (U t ...) <: t'
+;; -- AMB : t <: (U ... t ...)
+;; -- EXT : (U t' ...) <: (U t t' ...)
+;; -- ONE : a<:b => (U a t' ...) <: (U b t' ...)
 
 ;; =============================================================================
 
+(define-base-type Bot) ;; For empty unions
 (define-base-type Boolean)
 (define-base-type Str)
 
@@ -28,8 +35,6 @@
 ;; Occurrence type operations
 ;; These assume that τ is a type in 'normal form'
 (begin-for-syntax
-  ;; True if τ is a union type, otherwise #f
-
   (define (∪->list τ)
     ;; Ignore type constructor & the kind
     ;;  (because there are no bound identifiers)
@@ -40,33 +45,34 @@
       (error '∪->list (format "Given non-ambiguous type '~a'" τ))]))
 
   (define (list->∪ τ*)
-    (τ-eval #`(∪ #,@τ*)))
+    (if (null? τ*)
+        #'Bot
+        (τ-eval #`(∪ #,@τ*))))
     
-  (define (type->filter τ)
-    ;; Going to have the same problem here, matching on types
-    ;; (Γ is stored insisde τ)
-    ;; (define Π (get-context τ 'filter))
-    ;; (Π τ))
-    ;; TODO filter properly
-    #'boolean?)
-
   (define (∖ τ1 τ2)
     (cond
      [(∪? τ1)
-      (printf "SETMINUS got an ∪ ~a\n" τ1)
       (define (not-τ2? τ)
         (not (typecheck? τ τ2)))
       (list->∪ (filter not-τ2? (∪->list τ1)))]
-     [else ; do nothing
+     [else ; do nothing not non-union types
       τ1]))
 )
 
 ;; -----------------------------------------------------------------------------
 ;; --- Normal Form
+;; Evaluate each type in the union,
+;; remove duplicates
+;; determinize the ordering of members
+;; flatten nested unions
+
 (begin-for-syntax
   (define τ-eval (current-type-eval))
+
   (define (τ->symbol τ)
+    ;; TODO recurse for function types
     (cadr (syntax->datum τ)))
+
   (define (∪-eval τ-stx)
     (syntax-parse (τ-eval τ-stx)
      [(~∪ τ-stx* ...)
@@ -82,7 +88,7 @@
         (sort
          (remove-duplicates (apply append τ**) (current-type=?))
          symbol<?
-         #:key τ->symbol)) ;; TODO handle functions & other constructors
+         #:key τ->symbol))
       ;; Check for empty & singleton lists
       (define τ
         (cond
@@ -101,13 +107,7 @@
 
 ;; -----------------------------------------------------------------------------
 ;; --- Subtyping
-;; Problem: matching on normal forms is tricky
-;; (use stlc+reco+sub as an example)
 
-;; - subtype U with simple, U with contained
-;; - AMB : t <: (U ... t ...)
-;; - SUB : a<:b => (U a t' ...) <: (U b t' ...)
-;; - EXT : (U t' ...) <: (U t t' ...)
 (begin-for-syntax
  ;; True if one ordered list (of types) is a subset of another
  (define (subset? x* y* #:leq [cmp (current-typecheck-relation)])
@@ -121,39 +121,44 @@
        (loop x* (cdr y*))])))
 
  (define sub? (current-sub?))
+
  (define (∪-sub? τ1-stx τ2-stx)
    (define τ1 ((current-type-eval) τ1-stx))
    (define τ2 ((current-type-eval) τ2-stx))
-   (match `(,(∪? τ1) ,(∪? τ2))
-     ['(#f #t)
-      ;; AMB : a<:b => a <: (U ... b ...)
-      (for/or ([τ (in-list (∪->list τ2))])
-        (sub? τ1 τ))]
-     ['(#t #t)
-      (define τ1* (∪->list τ1))
-      (define τ2* (∪->list τ2))
-      (match `(,(length τ1*) ,(length τ2*))
-        [`(,L1 ,L2) #:when (< L1 L2)
-         ;; - EXT : (U t' ...) <: (U t t' ...)
-         (subset? τ1* τ2* #:leq sub?)]
-        [`(,L1 ,L2) #:when (= L1 L2)
-         ;; - SUB : a<:b => (U a t' ...) <: (U b t' ...)
-         ;; `∪->list` guarantees same order on type members
-         ;; `sub?` is reflexive
-         (andmap sub? τ1* τ2*)]
-        [_ #f])]
-     [_
-      ;; Could be (U ...) <: T
-      (sub? τ1 τ2)]))
+   (or (Bot? τ1) (Top? τ2)
+       (match `(,(∪? τ1) ,(∪? τ2))
+         ['(#f #t)
+          ;; AMB : a<:b => a <: (U ... b ...)
+          (for/or ([τ (in-list (∪->list τ2))])
+            (sub? τ1 τ))]
+         ['(#t #t)
+          (define τ1* (∪->list τ1))
+          (define τ2* (∪->list τ2))
+          (match `(,(length τ1*) ,(length τ2*))
+            [`(,L1 ,L2) #:when (< L1 L2)
+             ;; - EXT : (U t' ...) <: (U t t' ...)
+             (subset? τ1* τ2* #:leq sub?)]
+            [`(,L1 ,L2) #:when (= L1 L2)
+             ;; - SUB : a<:b => (U a t' ...) <: (U b t' ...)
+             ;; `∪->list` guarantees same order on type members
+             ;; `sub?` is reflexive
+             (andmap sub? τ1* τ2*)]
+            [_ #f])]
+         ['(#t #f)
+          ;; - ALL : t... <: t' => (U t ...) <: t'
+          (andmap (lambda (τ) (sub? τ τ2)) (∪->list τ1))]
+         ['(#f #f)
+          (sub? τ1 τ2)])))
      
  (current-sub? ∪-sub?)
  (current-typecheck-relation (current-sub?))
 )
 
-;; - TEST subtyping, with 'values' and with 'functions'
-
 ;; -----------------------------------------------------------------------------
 ;; --- Filters
+;; These are stored imperatively, in a function.
+;; Makes it easy to add a new filter & avoids duplicating this map
+
 (begin-for-syntax
  (define (simple-Π τ)
    (syntax-parse (τ-eval τ)
@@ -163,21 +168,20 @@
      #'integer?]
     [~Str
      #'string?]
-    ['Number
+    [~Num
      #'number?]
-    ['Natural
+    [~Nat
      #'(lambda (n) (and (integer? n) (not (negative? n))))]
     [_
      (error 'Π "Cannot make filter for type ~a\n" (syntax->datum τ))]))
  (define current-Π (make-parameter simple-Π)))
 
-;; - "simple", (Int ? e)
-;; - "correct", where the function is effectful and independent of cond
-
+;; (test (τ ? x) e1 e2)
+;; TODO:
 ;; - check if τ0 is a union type
 ;; - check if τ-filter is a subtype of τ0
 ;; - drop absurd branches?
-;; - allow x not identifier
+;; - allow x not identifier (1. does nothing 2. latent filters)
 (define-typed-syntax test #:datum-literals (?)
   [(_ [τ-filter:type ? x-stx:id] e1 e2)
    ;; Get the filter type, evaluate to a runtime predicate
@@ -186,17 +190,14 @@
      (format "Could not express type '~a' as a filter." #'τ-filter-stx)
    ;; TypeCheck e0:normally, e1:positive, e2:negative
    #:with (x τ0) (infer+erase #'x-stx)
-   ;; #:when (printf "Check'd e0, type is ~a\n" (syntax->datum #'τ0))
-   #:with [_ e1+ τ1] (infer/tyctx+erase #'([x-stx : τ-filter]) #'e1)
-   ;; #:when (printf "Check'd e1\n")
-   #:with [_ e2+ τ2] (infer/tyctx+erase #`([x-stx : #,(∖ #'τ0 #'τ-filter)]) #'e2)
-   ;; #:when (printf "Checked e2\n")
+   #:with [x1 e1+ τ1] (infer/ctx+erase #'([x-stx : τ-filter]) #'e1)
+   #:with [x2 e2+ τ2] (infer/ctx+erase #`([x-stx : #,(∖ #'τ0 #'τ-filter)]) #'e2)
    ;; Expand to a conditional, using the runtime predicate
-   (⊢ (if (f x) e1+ e2+)
+   (⊢ (if (f x-stx)
+          ((lambda x1 e1+) x-stx)
+          ((lambda x2 e2+) x-stx))
       : (∪ τ1 τ2))])
 
-;; - add filters (install filters, at start of file)
-;; - TEST basic filters
 ;; - TEST function filters (delayed filters?)
 ;; - disallow (U (-> ...) (-> ...))
 ;; - TEST latent filters -- listof BLAH
diff --git a/tapl/tests/stlc+occurrence-tests.rkt b/tapl/tests/stlc+occurrence-tests.rkt
index a4f7d77..fa9f1c4 100644
--- a/tapl/tests/stlc+occurrence-tests.rkt
+++ b/tapl/tests/stlc+occurrence-tests.rkt
@@ -59,6 +59,8 @@
 ;; ---- basics
 (check-type 1 : (∪ Int))
 (check-type 1 : (∪ (∪ Int)))
+(check-type (λ ([x : Int]) x)
+            : (→ Bot Top))
 
 (check-not-type 1 : (∪ Boolean))
 
@@ -93,6 +95,19 @@
 (check-not-type (λ ([x : (∪ Int Str)]) x)
             : (→ Top (∪ Num Str)))
 
+;; --- ALL
+(check-type (λ ([x : (∪ Boolean Int Str)]) x)
+            : (→ (∪ Boolean Int Str) Top))
+(check-type (λ ([x : (∪ Nat Int Num)]) x)
+            : (→ (∪ Nat Int Num) Num))
+(check-type (λ ([x : (∪ Nat Int Num)]) x)
+            : (→ Nat Num))
+
+;; --- misc
+;; Because Int<:(U Int ...)
+(check-type (λ ([x : (∪ Int Nat)]) #t)
+                  : (→ Int Boolean))
+
 ;; -----------------------------------------------------------------------------
 ;; --- Basic Filters (applying functions)
 
@@ -117,30 +132,30 @@
   : Boolean ⇒ #f)
 
 ;; --- successor
-;; (check-type
-;;  (λ ([x : (∪ Int Boolean)])
-;;     (test (Int ? x)
-;;           (+ 1 x)
-;;           (if x 1 0)))
-;;  : Int)
-;; (check-type-and-result
-;;  ((λ ([x : (∪ Int Boolean)])
-;;     (test (Int ? x)
-;;           (+ 1 x)
-;;           (if x 1 0))) #f)
-;;  : Int ⇒ 0)
-;; (check-type-and-result
-;;  ((λ ([x : (∪ Int Boolean)])
-;;     (test (Int ? x)
-;;           (+ 1 x)
-;;           (if x 1 0))) #t)
-;;  : Int ⇒ 1)
-;; (check-type-and-result
-;;  ((λ ([x : (∪ Int Boolean)])
-;;     (test (Int ? x)
-;;           (+ 1 x)
-;;           (if x 1 0))) 9000)
-;;  : Int ⇒ 9001)
+(check-type
+ (λ ([x : (∪ Int Boolean)])
+    (test (Int ? x)
+          (+ 1 x)
+          0))
+ : (→ (∪ Int Boolean) (∪ Num Nat)))
+(check-type-and-result
+ ((λ ([x : (∪ Int Boolean)])
+    (test (Int ? x)
+          (+ 1 x)
+          0)) #f)
+ : Num ⇒ 0)
+(check-type-and-result
+ ((λ ([x : (∪ Int Boolean)])
+    (test (Int ? x)
+          (+ 1 x)
+          1)) #t)
+ : Num ⇒ 1)
+(check-type-and-result
+ ((λ ([x : (∪ Int Boolean)])
+    (test (Int ? x)
+          (+ 1 x)
+          0)) 9000)
+ : Num ⇒ 9001)
 
 ;; ;; --- Do-nothing filter
 (check-type
@@ -149,40 +164,48 @@
  : (→ Int Boolean))
 (check-type
  (λ ([x : Int])
-    (test (Boolean ? x) 1 0))
- : (→ Int Int))
+    (test (Boolean ? x) 0 x))
+ : (→ Int (∪ Nat Int)))
 
 ;; --- Filter a subtype
-;; (check-type
-;;  (λ ([x : (∪ Nat Boolean)])
-;;     (test (Int ? x)
-;;           x
-;;           x))
-;;  : (→ (∪ Nat Bool) (∪ Int (∪ Nat Bool))))
+(check-type
+ (λ ([x : (∪ Nat Boolean)])
+    (test (Int ? x)
+          x
+          x))
+ : (→ (∪ Nat Boolean) (∪ Int (∪ Nat Boolean))))
 
-;; (check-type
-;;  (λ ([x : (∪ Int Bool)])
-;;     (test (Nat ? x)
-;;           (+ 2 x)
-;;           x))
-;;  : (→ (∪ Bool Int) (∪ Int Bool)))
+(check-type
+ (λ ([x : (∪ Int Boolean)])
+    (test (Nat ? x)
+          x
+          x))
+ : (→ (∪ Boolean Int) (∪ Int Nat Boolean)))
 
-;; (check-type-and-result
-;;  ((λ ([x : (∪ Int Bool)])
-;;      (test (Num ? x)
-;;            #f
-;;            x)) #t)
-;;  : (→ (∪ Int Bool) Bool)
-;;  ⇒ #t)
+;; --- Filter a supertype
+(check-type
+ (λ ([x : (∪ Int Boolean)])
+    (test (Num ? x)
+          1
+          x))
+ : (→ (∪ Boolean Int) (∪ Nat Boolean)))
 
-;; ;; Should filter all the impossible types 
-;; (check-type-and-result
-;;  ((λ ([x : (∪ Nat Int Num Bool)])
-;;      (test (Num ? x)
-;;            #f
-;;            x)) #t)
-;;  : (→ (∪ Nat Int Num Bool) Bool)
-;;  ⇒ #t)
+(check-type-and-result
+ ((λ ([x : (∪ Int Boolean)])
+     (test (Num ? x)
+           #f
+           x)) #t)
+ : Boolean
+ ⇒ #t)
+
+;; Should filter all the impossible types 
+(check-type-and-result
+ ((λ ([x : (∪ Nat Int Num Boolean)])
+     (test (Num ? x)
+           #f
+           x)) #t)
+ : Boolean
+ ⇒ #t)
 
 ;; ----------------------------------------------------------------------------- 
 ;; --- misc subtyping + filters (regression tests)
@@ -217,16 +240,45 @@
  #:with-msg "not a valid type")
 
 ;; -----------------------------------------------------------------------------
-;; --- TODO Subtypes should not be collapsed
-;; (Not sure how to test this, because type=? is subtyping and these ARE subtypes)
-;; (check-not-type (λ ([x : (∪ Int Nat)]) #t)
-;;                   : (→ Nat Boolean))
-;; (check-not-type (λ ([x : (∪ Int Nat)]) #t)
-;;                 : (→ Int Boolean))
+;; --- Subtypes should not be collapsed
+
+(check-not-type (λ ([x : (∪ Int Nat)]) #t)
+                : (→ Num Boolean))
+(check-type ((λ ([x : (∪ Int Nat Boolean)])
+                (test (Int ? x)
+                      2
+                      (test (Nat ? x)
+                            1
+                            0)))
+             #t)
+            : Nat ⇒ 0)
+(check-type ((λ ([x : (∪ Int Nat)])
+                (test (Nat ? x)
+                      1
+                      (test (Int ? x)
+                            2
+                            0)))
+             1)
+            : Nat ⇒ 1)
+(check-type ((λ ([x : (∪ Int Nat)])
+                (test (Int ? x)
+                      2
+                      (test (Nat ? x)
+                            1
+                            0)))
+             -10)
+            : Nat ⇒ 2)
                
-;; ;; -----------------------------------------------------------------------------
-;; ;; --- Filter values (should do nothing)
+;; -----------------------------------------------------------------------------
+;; --- TODO Filter values (should do nothing)
 
 ;; (check-type
 ;;  (test (Int ? 1) #t #f)
 ;;  : Boolean)
+
+;; -----------------------------------------------------------------------------
+;; --- TODO Filter functions
+
+;; -----------------------------------------------------------------------------
+;; --- TODO Latent filters (on data structures)
+