diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 29ffe7e09f..98793c5a99 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -9,7 +9,8 @@
  (only-in '#%kernel [apply kernel:apply])
  scheme/promise
  (only-in string-constants/private/only-once maybe-print-message)
- (only-in scheme/match/runtime match:error))
+ (only-in scheme/match/runtime match:error)
+ (for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym])))
 
 [raise (Univ . -> . (Un))]
 
diff --git a/collects/typed-scheme/private/base-special-env.ss b/collects/typed-scheme/private/base-special-env.ss
index 6c22040b31..76a692136c 100644
--- a/collects/typed-scheme/private/base-special-env.ss
+++ b/collects/typed-scheme/private/base-special-env.ss
@@ -25,8 +25,8 @@
 
 (define-for-syntax (initialize-others) 
   (d-s date 
-       ([second : N] [minute : N] [hour : N] [day : N] [month : N] 
-        [year : N] [weekday : N] [year-day : N] [dst? : B] [time-zone-offset : N])
+       ([second : -Number] [minute : -Number] [hour : -Number] [day : -Number] [month : -Number] 
+        [year : -Number] [weekday : -Number] [year-day : -Number] [dst? : -Boolean] [time-zone-offset : -Number])
        ())
   (d-s exn ([message : -String] [continuation-marks : Univ]) ())
   (d-s (exn:fail exn) () (-String -Cont-Mark-Set))
@@ -65,7 +65,7 @@
   ;; make-promise
   (-poly (a) (-> (-> a) (-Promise a)))
   ;; language
-  Sym
+  -Symbol
   ;; qq-append
   (-poly (a b) 
          (cl->*
diff --git a/collects/typed-scheme/private/base-types.ss b/collects/typed-scheme/private/base-types.ss
index 0cbae61e0b..0d3d23acde 100644
--- a/collects/typed-scheme/private/base-types.ss
+++ b/collects/typed-scheme/private/base-types.ss
@@ -1,10 +1,10 @@
 #lang s-exp "type-env-lang.ss"
 
-[Number N]
+[Number -Number]
 [Integer -Integer]
 [Void -Void]
-[Boolean B]
-[Symbol Sym]
+[Boolean -Boolean]
+[Symbol -Symbol]
 [String -String]
 [Any Univ]
 [Port -Port]
diff --git a/collects/typed-scheme/private/env-lang.ss b/collects/typed-scheme/private/env-lang.ss
index 1311e9cae4..434b5f5a1b 100644
--- a/collects/typed-scheme/private/env-lang.ss
+++ b/collects/typed-scheme/private/env-lang.ss
@@ -31,6 +31,7 @@
 (provide #%module-begin
          require
          (all-from-out scheme/base)
+         types rep private utils
          (for-syntax          
           (types-out convenience union)
           (all-from-out scheme/base)))
diff --git a/collects/typed-scheme/rep/filter-rep.ss b/collects/typed-scheme/rep/filter-rep.ss
index e9f70374ba..33d095532e 100644
--- a/collects/typed-scheme/rep/filter-rep.ss
+++ b/collects/typed-scheme/rep/filter-rep.ss
@@ -3,6 +3,20 @@
 (require scheme/match scheme/contract)
 (require "rep-utils.ss" "free-variance.ss")
 
+(define Filter/c
+  (flat-named-contract
+   'Filter
+   (λ (e)
+     (and (Filter? e) (not (FilterSet? e))))))
+
+(define LatentFilter/c
+  (flat-named-contract
+   'LatentFilter
+   (λ (e)
+     (and (LatentFilter? e) (not (LFilterSet? e))))))
+
+(provide Filter/c LatentFilter/c index/c)
+
 (df Bot () [#:fold-rhs #:base])
 
 (df TypeFilter ([t Type?] [p (listof PathElem?)] [v identifier?])
@@ -17,11 +31,22 @@
 	   (combine-frees (map free-idxs* (cons t p)))]
   [#:fold-rhs (*NotTypeFilter (type-rec-id t) (map pathelem-rec-id p) v)])
 
-(df FilterSet ([thn (listof (and/c Filter? (not/c FilterSet?)))]
-	       [els (listof (and/c Filter? (not/c FilterSet?)))])
+(df FilterSet (thn els)
      [#:frees (combine-frees (map free-vars* (append thn els)))
 	      (combine-frees (map free-idxs* (append thn els)))]
-     [#:fold-rhs (*FilterSet (map filter-rec-id thn) (map filter-rec-id els))])
+     [#:fold-rhs (*FilterSet (map filter-rec-id thn) (map filter-rec-id els))]
+     [#:contract (->d ([t (cond [(ormap Bot? t)
+                                 (list/c Bot?)]
+                                [(ormap Bot? e)
+                                 (list/c)]
+                                [else (listof Filter/c)])]
+                       [e (cond [(ormap Bot? e)
+                                 (list/c Bot?)]
+                                [(ormap Bot? t)
+                                 (list/c)]
+                                [else (listof Filter/c)])])
+                      ()
+                      [result FilterSet?])])
 
 (define index/c (or/c natural-number/c keyword?))
 
@@ -35,8 +60,19 @@
   [#:frees (lambda (frees*) (combine-frees (map (compose make-invariant frees*) (cons t p))))]
   [#:fold-rhs (*LNotTypeFilter (type-rec-id t) (map pathelem-rec-id p) idx)])
 
-(dlf LFilterSet ([thn (listof (and/c LatentFilter? (not/c LFilterSet?)))]
-		 [els (listof (and/c LatentFilter? (not/c LFilterSet?)))])
+(dlf LFilterSet (thn els)
      [#:frees (combine-frees (map free-vars* (append thn els)))
 	      (combine-frees (map free-idxs* (append thn els)))]
-     [#:fold-rhs (*LFilterSet (map latentfilter-rec-id thn) (map latentfilter-rec-id els))])
+     [#:fold-rhs (*LFilterSet (map latentfilter-rec-id thn) (map latentfilter-rec-id els))]
+     [#:contract (->d ([t (cond [(ormap LBot? t)
+                                 (list/c LBot?)]
+                                [(ormap LBot? e)
+                                 (list/c)]
+                                [else (listof LatentFilter/c)])]
+                       [e (cond [(ormap LBot? e)
+                                 (list/c LBot?)]
+                                [(ormap LBot? t)
+                                 (list/c)]
+                                [else (listof LatentFilter/c)])])
+                      ()
+                      [result LFilterSet?])])
diff --git a/collects/typed-scheme/rep/rep-utils.ss b/collects/typed-scheme/rep/rep-utils.ss
index 3de0e278e8..9c1d66af7a 100644
--- a/collects/typed-scheme/rep/rep-utils.ss
+++ b/collects/typed-scheme/rep/rep-utils.ss
@@ -95,7 +95,7 @@
          [provides (if #'no-provide?
                        #'(begin)                                 
                        #`(begin 
-                           (provide ex pred acc ...)
+                           (provide #;nm ex pred acc ...)
                            (p/c (rename *maker maker *maker-cnt))))]
          [intern 
           (let ([mk (lambda (int) 
diff --git a/collects/typed-scheme/typecheck/signatures.ss b/collects/typed-scheme/typecheck/signatures.ss
index 530ad0094c..ec810d1067 100644
--- a/collects/typed-scheme/typecheck/signatures.ss
+++ b/collects/typed-scheme/typecheck/signatures.ss
@@ -2,7 +2,7 @@
 (require scheme/unit scheme/contract "../utils/utils.ss")
 (require (rep type-rep)
          (utils unit-utils)
-         (private type-utils))
+         (types utils))
 (provide (all-defined-out))
 
 (define-signature typechecker^
diff --git a/collects/typed-scheme/typecheck/tc-if-unit.ss b/collects/typed-scheme/typecheck/tc-if-unit.ss
index cc87ca8b13..24bb6cd2df 100644
--- a/collects/typed-scheme/typecheck/tc-if-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-if-unit.ss
@@ -2,13 +2,12 @@
 
 (require (rename-in "../utils/utils.ss" [infer r:infer]))
 (require "signatures.ss"
-         (rep type-rep effect-rep)
-         (private type-effect-convenience subtype union type-utils type-comparison mutated-vars)
+         (rep type-rep filter-rep object-rep)
+         (rename-in (types convenience subtype union utils comparison remove-intersect)
+                    [remove *remove])
          (env lexical-env)
-         (only-in (private remove-intersect)
-                  [remove *remove])
          (r:infer infer)
-	 (utils tc-utils)
+	 (utils tc-utils mutated-vars)
          syntax/kerncase
          mzlib/trace
          mzlib/plt-match)
@@ -24,17 +23,14 @@
 ;;      neccessary for handling true/false effects
 ;; Boolean Expr listof[Effect] option[type] -> TC-Result
 (define (tc-expr/eff t/f expr effs expected)
-  #;(printf "tc-expr/eff : ~a~n" (syntax-object->datum expr))
   ;; this flag represents whether the refinement proves that this expression cannot be executed
   (let ([flag (box #f)])
     ;; this does the operation on the old type
     ;; type-op : (Type Type -> Type) Type -> _ Type -> Type
     (define ((type-op f t) _ old)
       (let ([new-t (f old t)])
-        ;(printf "new-t ~a~n" new-t)
         ;; if this operation produces an uninhabitable type, then this expression can't be executed
         (when (type-equal? new-t (Un))
-          ;(printf "setting flag!~n")
           (set-box! flag #t))
         ;; have to return something here, so that we can continue typechecking
         new-t))
@@ -87,16 +83,10 @@
 
 ;; the main function
 (define (tc/if-twoarm tst thn els)
-  #;(printf "tc-if/twoarm~n")
   ;; check in the context of the effects, and return
   (match-let* ([(tc-result: tst-ty tst-thn-eff tst-els-eff) (tc-expr tst)]
                [(tc-result: thn-ty thn-thn-eff thn-els-eff) (tc-expr/eff #t thn tst-thn-eff #f)]
-               #;[_ (printf "v is ~a~n" v)]
-               #;[c (current-milliseconds)]
                [(tc-result: els-ty els-thn-eff els-els-eff) (tc-expr/eff #f els tst-els-eff #f)])
-    #;(printf "tst thn-eff: ~a~ntst els-eff: ~a~n" tst-thn-eff tst-els-eff)
-    #;(printf "thn ty:~a thn-eff: ~a thn els-eff: ~a~n" thn-ty thn-thn-eff thn-els-eff)
-    #;(printf "els ty:~a thn-eff: ~a els els-eff: ~a~n" els-ty els-thn-eff els-els-eff)
     (match* (els-ty thn-thn-eff thn-els-eff els-thn-eff els-els-eff)
       ;; this is the case for `or'
       ;; the then branch has to be #t
@@ -106,7 +96,6 @@
       ;; FIXME - mzscheme's or macro doesn't match this!
       [(_ (list (True-Effect:)) (list (True-Effect:)) (list (Restrict-Effect: t v)) (list (Remove-Effect: t v*)))
        (=> unmatch)
-       #;(printf "or branch~n")
        (match (list tst-thn-eff tst-els-eff)
          ;; check that the test was also a simple predicate
          [(list (list (Restrict-Effect: s u)) (list (Remove-Effect: s u*)))
@@ -126,7 +115,6 @@
          [_ (unmatch)])]
       ;; this is the case for `and'
       [(_ _ _ (list (False-Effect:)) (list (False-Effect:)))
-       #;(printf "and branch~n")
        (ret (Un (-val #f) thn-ty) 
             ;; we change variable effects to type effects in the test, 
             ;; because only the boolean result of the test is used
@@ -136,41 +124,17 @@
             (list))]
       ;; if the else branch can never happen, just use the effect of the then branch
       [((Union: (list)) _ _ _ _)
-       #;(printf "and branch~n")
-       (ret thn-ty 
-            ;; we change variable effects to type effects in the test, 
-            ;; because only the boolean result of the test is used
-            ;; whereas, the actual value of the then branch is returned, not just the boolean result
-            (append #;(map var->type-eff tst-thn-eff) thn-thn-eff)
-            ;; no else effects for and, because any branch could have been false
-            (append #;(map var->type-eff tst-els-eff) thn-els-eff))]
+       (ret thn-ty thn-thn-eff thn-els-eff)]
       ;; otherwise this expression has no effects
       [(_ _ _ _ _) 
-       #;(printf "if base case:~a ~n" (syntax-object->datum tst))
-       #;(printf "els-ty ~a ~a~n" 
-                 els-ty c)
-       #;(printf "----------------------~nels-ty ~a ~nUn~a~n ~a~n" 
-                 els-ty (Un thn-ty els-ty) c)
        (ret (Un thn-ty els-ty))])))
 
 ;; checking version
 (define (tc/if-twoarm/check tst thn els expected)
-  #;(printf "tc-if/twoarm/check~n")
   ;; check in the context of the effects, and return
   (match-let* ([(tc-result: tst-ty tst-thn-eff tst-els-eff) (tc-expr tst)]
-               #;[_ (printf "got to here 0~n")]
                [(tc-result: thn-ty thn-thn-eff thn-els-eff) (tc-expr/eff #t thn tst-thn-eff expected)]
-               #;[_ (printf "v is ~a~n" v)]
-               #;[c (current-milliseconds)]
-               #;[_ (printf "got to here 1~n")]
-               [(tc-result: els-ty els-thn-eff els-els-eff) (tc-expr/eff #f els tst-els-eff expected)]
-               #;[_ (printf "got to here 2~n")])
-    #;(printf "check: v now is ~a~n" (ret els-ty els-thn-eff els-els-eff))
-    #;(printf "els-ty ~a ~a~n" 
-              els-ty c)
-    #;(printf "tst/check thn-eff: ~a~ntst els-eff: ~a~n" tst-thn-eff tst-els-eff)
-    #;(printf "thn/check thn-eff: ~a~nthn els-eff: ~a~n" thn-thn-eff thn-els-eff)
-    #;(printf "els/check thn-eff: ~a~nels els-eff: ~a~n" els-thn-eff els-els-eff)
+               [(tc-result: els-ty els-thn-eff els-els-eff) (tc-expr/eff #f els tst-els-eff expected)])
     (match* (els-ty thn-thn-eff thn-els-eff els-thn-eff els-els-eff) 
       ;; this is the case for `or'
       ;; the then branch has to be #t
@@ -180,7 +144,6 @@
       ;; FIXME - mzscheme's or macro doesn't match this!
       [(_ (list (True-Effect:)) (list (True-Effect:)) (list (Restrict-Effect: t v)) (list (Remove-Effect: t v*)))
        (=> unmatch)
-       ;(printf "or branch~n")
        (match (list tst-thn-eff tst-els-eff)
          ;; check that the test was also a simple predicate
          [(list (list (Restrict-Effect: s u)) (list (Remove-Effect: s u*)))
@@ -202,7 +165,6 @@
          [_ (unmatch)])]
       ;; this is the case for `and'
       [(_ _ _ (list (False-Effect:)) (list (False-Effect:)))
-       #;(printf "and branch~n")
        (let ([t (Un thn-ty (-val #f))])
          (check-below t expected)              
          (ret t 
@@ -226,6 +188,3 @@
        (let ([t (Un thn-ty els-ty)])
          (check-below t expected)
          (ret t))])))
-
-
-;)
diff --git a/collects/typed-scheme/typecheck/tc-metafunctions.ss b/collects/typed-scheme/typecheck/tc-metafunctions.ss
new file mode 100644
index 0000000000..5382d22c96
--- /dev/null
+++ b/collects/typed-scheme/typecheck/tc-metafunctions.ss
@@ -0,0 +1,62 @@
+#lang scheme/base
+
+(require "../utils/utils.ss")
+(require (rename-in (types subtype convenience remove-intersect)                   
+                    [-> -->]
+                    [->* -->*]
+                    [one-of/c -one-of/c])
+         (rep type-rep)
+         scheme/contract scheme/match
+         stxclass/util
+         (for-syntax scheme/base))
+
+;; this implements the sequence invariant described on the first page relating to Bot
+(define (lcombine l1 l2)
+  (cond [(memq (make-LBot) l1)
+         (make-LFilterSet (list (make-LBot)) null)]
+        [(memq (make-LBot) l2)
+         (make-LFilterSet null (list (make-LBot)))]
+        [else (make-LFilterSet l1 l2)]))
+
+(define (combine l1 l2)
+  (cond [(memq (make-Bot) l1)
+         (make-FilterSet (list (make-Bot)) null)]
+        [(memq (make-Bot) l2)
+         (make-FilterSet null (list (make-Bot)))]
+        [else (make-FilterSet l1 l2)]))
+
+(define/contract (abstract-filter x idx fs)
+  (-> identifier? index/c FilterSet? LFilterSet?)
+  (match fs
+    [(FilterSet: f+ f-)
+     (lcombine
+      (apply append (for/list ([f f+]) (abo x idx f)))
+      (apply append (for/list ([f f-]) (abo x idx f))))]))
+
+(define/contract (abo x idx f)
+  (-> identifier? index/c Filter/c (or/c '() (list/c LatentFilter/c)))
+  (define-match-expander =x
+    (lambda (stx) #'(? (lambda (id) (free-identifier=? id x)))))
+  (match f
+    [(Bot:) (list (make-LBot))]
+    [(TypeFilter: t p (=x)) (list (make-LTypeFilter t p))]
+    [(NotTypeFilter: t p (=x)) (list (make-LNotTypeFilter t p))]
+    [_ null]))
+
+(define/contract (apply-filter lfs t o)
+  (-> LFilterSet? Type/c Object?)
+  (match lfs
+    [(LFilterSet: lf+ lf-)
+     (combine
+      (apply append (for/list ([lf lf+]) (apo lf t o)))
+      (apply append (for/list ([lf lf-]) (apo lf t o))))]))
+
+(define/contract (apo lf s o)
+  (-> LatentFilter/c Type/c Object? (or/c '() (list/c Filter/c)))
+  (match* (lf s o)
+    [((LBot:) _ _) (list (make-Bot))]
+    [((LNotTypeFilter: (? (lambda (t) (subtype s t))) (list) _) _ _) (list (make-Bot))]
+    [((LTypeFilter: (? (lambda (t) (not (overlap s t)))) (list) _) _ _) (list (make-Bot))]
+    [(_ _ (Empty:)) null]
+    [((LTypeFilter: t pi* _) _ (Path: pi x)) (make-TypeFilter t (append pi* pi) x)]
+    [((LNotTypeFilter: t pi* _) _ (Path: pi x)) (make-NotTypeFilter t (append pi* pi) x)]))
\ No newline at end of file
diff --git a/collects/typed-scheme/typecheck/tc-toplevel.ss b/collects/typed-scheme/typecheck/tc-toplevel.ss
index f0553c1e21..937568aab1 100644
--- a/collects/typed-scheme/typecheck/tc-toplevel.ss
+++ b/collects/typed-scheme/typecheck/tc-toplevel.ss
@@ -8,9 +8,10 @@
          "signatures.ss"
          "tc-structs.ss"
          (rep type-rep)
-         (private type-utils type-effect-convenience parse-type type-annotation mutated-vars type-contract)
+         (types utils convenience)
+         (private parse-type type-annotation type-contract)
 	 (env type-env init-envs type-name-env type-alias-env)
-	 (utils tc-utils)
+	 (utils tc-utils mutated-vars)
 	 "provide-handling.ss"
          "def-binding.ss"
          (for-template
diff --git a/collects/typed-scheme/typed-scheme.ss b/collects/typed-scheme/typed-scheme.ss
index c5054fce78..d6bb00ec51 100644
--- a/collects/typed-scheme/typed-scheme.ss
+++ b/collects/typed-scheme/typed-scheme.ss
@@ -2,10 +2,11 @@
 
 (require (rename-in "utils/utils.ss" [infer r:infer]))
 
-(require (private #;base-env base-types)
+(require (private base-types)
          (for-syntax 
           scheme/base
-	  (private type-utils type-contract type-effect-convenience)
+          (private type-contract)
+          (types utils convenience)
 	  (typecheck typechecker provide-handling)
 	  (env type-environments type-name-env type-alias-env)
 	  (r:infer infer)
diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss
index 7fdfdf216c..5db79868df 100644
--- a/collects/typed-scheme/types/abbrev.ss
+++ b/collects/typed-scheme/types/abbrev.ss
@@ -66,10 +66,10 @@
 (define -Listof (-poly (list-elem) (make-Listof list-elem)))
 
 
-(define N (make-Base 'Number #'number?))
+(define -Number (make-Base 'Number #'number?))
 (define -Integer (make-Base 'Integer #'exact-integer?))
-(define B (make-Base 'Boolean #'boolean?))
-(define Sym (make-Base 'Symbol #'symbol?))
+(define -Boolean (make-Base 'Boolean #'boolean?))
+(define -Symbol (make-Base 'Symbol #'symbol?))
 (define -Void (make-Base 'Void #'void?))
 (define -Bytes (make-Base 'Bytes #'bytes?))
 (define -Regexp (make-Base 'Regexp #'(and/c regexp? (not/c pregexp?) (not/c byte-regexp?))))
@@ -99,24 +99,24 @@
 (define Any-Syntax
   (-mu x
        (-Syntax (*Un 
-                 N
-                 B
-                 Sym
+                 -Number
+                 -Boolean
+                 -Symbol
                  -String
 		 -Keyword                 
                  (-mu y (*Un (-val '()) (-pair x (*Un x y))))
                  (make-Vector x)
                  (make-Box x)))))
 
-(define Ident (-Syntax Sym))
+(define Ident (-Syntax -Symbol))
 
-(define -Sexp (-mu x (*Un (-val null) N B Sym -String (-pair x x))))
+(define -Sexp (-mu x (*Un (-val null) -Number -Boolean -Symbol -String (-pair x x))))
 (define -Port (*Un -Output-Port -Input-Port))
 
 (define -Pathlike (*Un -String -Path))
 (define -Pathlike* (*Un -String -Path (-val 'up) (-val 'same)))
 (define -Pattern (*Un -Bytes -Regexp -PRegexp -Byte-Regexp -Byte-PRegexp -String))
-(define -Byte N)
+(define -Byte -Number)
 
 (define -no-lfilter (make-LFilterSet null null))
 (define -no-filter (make-FilterSet null null))
@@ -249,7 +249,7 @@
   (case-lambda 
     [(in out t)
      (->* in out : (-LFS (list (-filter t)) (list (-not-filter t))))]
-    [(t) (make-pred-ty (list Univ) B t)]))
+    [(t) (make-pred-ty (list Univ) -Boolean t)]))
 
 
 (define (opt-fn args opt-args result)