diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 29ffe7e0..98793c5a 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 6c22040b..76a69213 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 0cbae61e..0d3d23ac 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 1311e9ca..434b5f5a 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 e9f70374..33d09553 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 3de0e278..9c1d66af 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 530ad009..ec810d10 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-metafunctions.ss b/collects/typed-scheme/typecheck/tc-metafunctions.ss
new file mode 100644
index 00000000..5382d22c
--- /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 f0553c1e..937568aa 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 c5054fce..d6bb00ec 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 7fdfdf21..5db79868 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)