diff --git a/collects/typed-scheme/env/lexical-env.ss b/collects/typed-scheme/env/lexical-env.ss
index 52b2659d..36c3eecd 100644
--- a/collects/typed-scheme/env/lexical-env.ss
+++ b/collects/typed-scheme/env/lexical-env.ss
@@ -7,6 +7,7 @@
          (only-in scheme/contract ->* ->)
          (utils tc-utils)
          (only-in (rep type-rep) Type/c)
+         (typecheck tc-metafunctions)
 	 (except-in (types utils convenience) -> ->*))
 
 (provide lexical-env with-lexical-env with-lexical-env/extend with-update-type/lexical)
diff --git a/collects/typed-scheme/env/type-environments.ss b/collects/typed-scheme/env/type-environments.ss
index 12c570c2..2ae35bc6 100644
--- a/collects/typed-scheme/env/type-environments.ss
+++ b/collects/typed-scheme/env/type-environments.ss
@@ -2,8 +2,9 @@
 
 (require scheme/contract
          (prefix-in r: "../utils/utils.ss")
-         scheme/match
-         (except-in (r:utils tc-utils) make-env))
+         scheme/match (r:rep filter-rep rep-utils) unstable/struct
+         (except-in (r:utils tc-utils) make-env)
+         (r:typecheck tc-metafunctions))
 
 (provide current-tvars
          extend
@@ -17,10 +18,13 @@
          env-filter
          env-vals
          env-keys+vals
+         env-props
+         replace-props
          with-dotted-env/extend)
 
 ;; eq? has the type of equal?, and l is an alist (with conses!)
-(r:d-s/c env ([eq? (any/c any/c . -> . boolean?)] [l (listof pair?)]) #:transparent)
+;; props is a list of known propositions
+(r:d-s/c env ([eq? (any/c any/c . -> . boolean?)] [l (listof pair?)] [props (listof Filter/c)]) #:transparent)
 
 (define (env-vals e)
   (map cdr (env-l e)))
@@ -30,39 +34,44 @@
 
 (define (env-filter f e)
   (match e
-    [(struct env (eq? l))
-    (make-env eq? (filter f l))]))
+    [(struct env (eq? l props))
+    (make-env eq? (filter f l) props)]))
+
+(define (make-empty-env p?) (make env p? null null))
 
 ;; the initial type variable environment - empty
 ;; this is used in the parsing of types
-(define initial-tvar-env (make-env eq? '()))
+(define initial-tvar-env (make-empty-env eq?))
 
 ;; a parameter for the current type variables
 (define current-tvars (make-parameter initial-tvar-env))  
 
-(define (make-empty-env p?) (make-env p? '()))
-
 ;; the environment for types of ... variables
 (define dotted-env (make-parameter (make-empty-env free-identifier=?)))
 
-(define/contract (env-map f env)
+(define/contract (env-map f e)
   ((pair? . -> . pair?) env? . -> . env?)
-  (make-env (env-eq? env) (map f (env-l env))))
+  (make env (env-eq? e) (map f (env-l e)) (env-props e)))
 
 ;; extend that works on single arguments
 (define (extend e k v) 
   (match e
-    [(struct env (f l)) (make-env f (cons (cons k v) l))]
+    [(struct env (f l p)) (make env f (cons (cons k v) l) p)]
     [_ (int-err "extend: expected environment, got ~a" e)]))
 
 (define (extend-env ks vs e)
   (match e
-    [(struct env (f l)) (make-env f (append (map cons ks vs) l))]
+    [(struct env (f l p)) (make env f (append (map cons ks vs) l) p)]
     [_ (int-err "extend-env: expected environment, got ~a" e)]))
 
+(define (replace-props e props)
+  (match e
+    [(struct env (f l p))
+     (make env f l props)]))
+
 (define (lookup e key fail)
   (match e
-    [(struct env (f? l))
+    [(struct env (f? l p))
      (let loop ([l l])
        (cond [(null? l) (fail key)]
              [(f? (caar l) key) (cdar l)]
diff --git a/collects/typed-scheme/rep/filter-rep.ss b/collects/typed-scheme/rep/filter-rep.ss
index 8f353d7b..3c66be2a 100644
--- a/collects/typed-scheme/rep/filter-rep.ss
+++ b/collects/typed-scheme/rep/filter-rep.ss
@@ -32,7 +32,9 @@
   [#:fold-rhs (*NotTypeFilter (type-rec-id t) (map pathelem-rec-id p) v)])
 
 ;; implication
-(df ImpFilter ([a (listof Filter/c)] [c (listof Filter/c)]))
+(df ImpFilter ([a (listof Filter/c)] [c (listof Filter/c)])
+    [#:frees (combine-frees (map free-vars* (append a c)))
+	     (combine-frees (map free-idxs* (append a c)))])
 
 (df FilterSet (thn els)
      [#:frees (combine-frees (map free-vars* (append thn els)))
@@ -68,7 +70,10 @@
   [#:fold-rhs (*LNotTypeFilter (type-rec-id t) (map pathelem-rec-id p) idx)])
 
 ;; implication
-(df LImpFilter ([a (listof LatentFilter/c)] [c (listof LatentFilter/c)]))
+(df LImpFilter ([a (listof LatentFilter/c)] [c (listof LatentFilter/c)])
+    #;[#:frees (combine-frees (map free-vars* (append a c)))
+	     (combine-frees (map free-idxs* (append a c)))])
+
 
 (dlf LFilterSet (thn els)
      [#:frees (combine-frees (map free-vars* (append thn els)))
@@ -96,3 +101,6 @@
   (flat-named-contract
    'LatentFilterSet
    (λ (e) (or (LFilterSet? e)))))
+
+(define filter-equal? eq?)
+(provide filter-equal?)
\ No newline at end of file
diff --git a/collects/typed-scheme/rep/free-variance.ss b/collects/typed-scheme/rep/free-variance.ss
index 7e4014e3..6b87ae63 100644
--- a/collects/typed-scheme/rep/free-variance.ss
+++ b/collects/typed-scheme/rep/free-variance.ss
@@ -1,9 +1,8 @@
 #lang scheme/base
-(require "../utils/utils.ss")
-
-(require (for-syntax scheme/base)
-         (utils tc-utils)
-         mzlib/etc)
+(require "../utils/utils.ss"
+	 (for-syntax scheme/base)
+         (utils tc-utils) scheme/list
+         mzlib/etc scheme/contract)
 
 ;; this file contains support for calculating the free variables/indexes of types
 ;; actual computation is done in rep-utils.ss  and type-rep.ss
@@ -22,19 +21,28 @@
 
 (provide Covariant Contravariant Invariant Constant Dotted)
 
+(define (variance? e)
+  (memq e (list Covariant Contravariant Invariant Constant Dotted)))
+
 ;; hashtables for keeping track of free variables and indexes
-(define index-table (make-weak-hasheq))
+(define index-table (make-weak-hash))
 ;; maps Type to List[Cons[Number,Variance]]
-(define var-table (make-weak-hasheq))
+(define var-table (make-weak-hash))
 ;; maps Type to List[Cons[Symbol,Variance]]
 
-(define (free-idxs* t) (hash-ref index-table t (lambda _ (int-err "type ~a not in index-table" (syntax-e t)))))
-(define (free-vars* t) (hash-ref var-table t (lambda _ (int-err "type ~a not in var-table" (syntax-e t)))))
+(define ((input/c tbl) val) (hash-ref tbl val #f))
 
+(define (free-idxs* t)
+  (hash-ref index-table t (lambda _ (int-err "type ~a not in index-table" t))))
+(define (free-vars* t)
+  (hash-ref var-table t (lambda _ (int-err "type ~a not in var-table" t))))
 
 (define empty-hash-table (make-immutable-hasheq null))
 
-(provide free-vars* free-idxs* empty-hash-table make-invariant)
+(p/c [free-vars* (-> (input/c var-table) (hash/c symbol? variance?))]
+     [free-idxs* (-> (input/c index-table) (hash/c exact-nonnegative-integer? variance?))])
+
+(provide empty-hash-table make-invariant)
 
 ;; frees = HT[Idx,Variance] where Idx is either Symbol or Number
 ;; (listof frees) -> frees
diff --git a/collects/typed-scheme/rep/rep-utils.ss b/collects/typed-scheme/rep/rep-utils.ss
index ca994b19..a0de7c5a 100644
--- a/collects/typed-scheme/rep/rep-utils.ss
+++ b/collects/typed-scheme/rep/rep-utils.ss
@@ -143,9 +143,10 @@
                    (syntax/loc s (struct nm pat))])))
             (begin-for-syntax
               (hash-set! ht-stx 'kw-stx (list #'ex #'flds.fs bfs-fold-rhs #'#,stx)))
-            intern
-            provides
-            frees))])))
+            (w/c nm ()
+		 intern
+		 frees)
+	    provides))])))
 
 (define-for-syntax (mk-fold ht type-rec-id rec-ids kws)
   (lambda (stx)
diff --git a/collects/typed-scheme/typecheck/tc-envops.ss b/collects/typed-scheme/typecheck/tc-envops.ss
index c6d8a223..9acea43b 100644
--- a/collects/typed-scheme/typecheck/tc-envops.ss
+++ b/collects/typed-scheme/typecheck/tc-envops.ss
@@ -9,9 +9,10 @@
          (rep type-rep)
          (utils tc-utils)
          (types resolve)
-         (only-in (env type-environments lexical-env) env? update-type/lexical env-map)
+         (only-in (env type-environments lexical-env) env? update-type/lexical env-map env-props replace-props)
          scheme/contract scheme/match
          mzlib/trace
+         (typecheck tc-metafunctions)
          (for-syntax scheme/base))
 
 (provide env+)
@@ -57,9 +58,11 @@
 ;; sets the flag box to #f if anything becomes (U)
 (d/c (env+ env fs flag)
   (env? (listof Filter/c) (box/c #t). -> . env?)
-  (for/fold ([Γ env]) ([f fs])
+  (define-values (imps atoms) (combine-props fs (env-props env)))
+  (for/fold ([Γ (replace-props env imps)]) ([f atoms])
     (match f
       [(Bot:) (set-box! flag #f) (env-map (lambda (x) (cons (car x) (Un))) Γ)]
+      [(ImpFilter: _ _) Γ]
       [(or (TypeFilter: _ _ x) (NotTypeFilter: _ _ x))
        (update-type/lexical (lambda (x t) (let ([new-t (update t f)])
                                             (when (type-equal? new-t (Un))
diff --git a/collects/typed-scheme/typecheck/tc-if.ss b/collects/typed-scheme/typecheck/tc-if.ss
index 94f6aabe..b286b474 100644
--- a/collects/typed-scheme/typecheck/tc-if.ss
+++ b/collects/typed-scheme/typecheck/tc-if.ss
@@ -41,9 +41,11 @@
       [else (ret (Un))]))
   (match (single-value tst)
     [(tc-result1: _ (and f1 (FilterSet: fs+ fs-)) _)
-     (let-values ([(flag+ flag-) (values (box #t) (box #t))])
-       (match-let ([(tc-results: ts fs2 os2) (with-lexical-env (env+ (lexical-env) fs+ flag+) (tc thn (unbox flag+)))]
-                   [(tc-results: us fs3 os3) (with-lexical-env (env+ (lexical-env) fs- flag-) (tc els (unbox flag-)))])
+     (let*-values ([(flag+ flag-) (values (box #t) (box #t))]
+                   [(derived-imps+ derived-atoms+)
+                    (combine-props fs+ (env-props (lexical-env)))])
+       (match-let* ([(tc-results: ts fs2 os2) (with-lexical-env (env+ (lexical-env) fs+ flag+) (tc thn (unbox flag+)))]
+                    [(tc-results: us fs3 os3) (with-lexical-env (env+ (lexical-env) fs- flag-) (tc els (unbox flag-)))])
          ;; if we have the same number of values in both cases
          (cond [(= (length ts) (length us))
                 (let ([r
diff --git a/collects/typed-scheme/typecheck/tc-metafunctions.ss b/collects/typed-scheme/typecheck/tc-metafunctions.ss
index 716faecc..3d98e766 100644
--- a/collects/typed-scheme/typecheck/tc-metafunctions.ss
+++ b/collects/typed-scheme/typecheck/tc-metafunctions.ss
@@ -5,11 +5,11 @@
                     [-> -->]
                     [->* -->*]
                     [one-of/c -one-of/c])
-         (rep type-rep)
+         (rep type-rep filter-rep) scheme/list
          scheme/contract scheme/match unstable/match
          (for-syntax scheme/base))
 
-(provide combine-filter apply-filter abstract-filter abstract-filters
+(provide combine-filter apply-filter abstract-filter abstract-filters combine-props
          split-lfilters merge-filter-sets values->tc-results tc-results->values)
 
 ;; this implements the sequence invariant described on the first page relating to Bot
@@ -147,7 +147,7 @@
     ;; and
     [((FilterSet: f1+ f1-) (FilterSet: f2+ f2-) (F-FS:)) 
      (mk (combine (append f1+ f2+)
-		  null		  
+		  #;null		  
 		  (append (for/list ([f f1-])
 			    (make-ImpFilter f2+ (list f)))
 			  (for/list ([f f2-])
@@ -203,3 +203,18 @@
 (define (tc-results->values tc)
   (match tc
     [(tc-results: ts) (-values ts)]))
+
+(define (combine-props new-props old-props)
+  (define-values (new-imps new-atoms) (partition ImpFilter? new-props))
+  (define-values (derived-imps derived-atoms)
+    (for/fold 
+        ([derived-imps null]
+         [derived-atoms null])
+      ([o old-props])
+      (match o
+        [(ImpFilter: as cs)
+         (let ([as* (remove* new-atoms as filter-equal?)])
+           (if (null? as*)
+               (values derived-imps (append cs new-atoms))
+               (values (cons (make-ImpFilter as* cs) derived-imps) derived-atoms)))])))
+  (values (append new-imps derived-imps) (append new-atoms derived-atoms)))
diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss
index 4ebd614f..04559f03 100644
--- a/collects/typed-scheme/types/abbrev.ss
+++ b/collects/typed-scheme/types/abbrev.ss
@@ -121,7 +121,7 @@
 
 (define -Zero (-val 0))
 (define -Real (*Un -Flonum -ExactRational))
-(define -ExactNonnegativeInteger (*Un -Zero -ExactPositiveInteger))
+(define -ExactNonnegativeInteger (*Un -ExactPositiveInteger -Zero))
 (define -Nat -ExactNonnegativeInteger)
 
 (define -Byte -Number)
diff --git a/collects/typed-scheme/types/convenience.ss b/collects/typed-scheme/types/convenience.ss
index f281022b..15d818f6 100644
--- a/collects/typed-scheme/types/convenience.ss
+++ b/collects/typed-scheme/types/convenience.ss
@@ -46,7 +46,7 @@
 
 (define In-Syntax
   (-mu e
-       (*Un -Number -Boolean -Symbol -String -Keyword -Char
+       (*Un -Boolean -Symbol -String -Keyword -Char -Number
             (make-Vector (-Syntax e))
             (make-Box (-Syntax e))
             (-mu list
diff --git a/collects/typed-scheme/utils/utils.ss b/collects/typed-scheme/utils/utils.ss
index 8300d461..3fb7d363 100644
--- a/collects/typed-scheme/utils/utils.ss
+++ b/collects/typed-scheme/utils/utils.ss
@@ -145,7 +145,7 @@ at least theoretically.
 ;; - 1 printers have to be defined at the same time as the structs
 ;; - 2 we want to support things printing corectly even when the custom printer is off
 
-(define-for-syntax printing? #t)
+(define-for-syntax printing? #f)
 
 (define-syntax-rule (defprinter t ...)
   (begin
@@ -179,7 +179,7 @@ at least theoretically.
 
 
 ;; turn contracts on and off - off by default for performance.
-(define-for-syntax enable-contracts? #f)
+(define-for-syntax enable-contracts? #t)
 (provide (for-syntax enable-contracts?) p/c w/c cnt d-s/c d/c)
 
 ;; these are versions of the contract forms conditionalized by `enable-contracts?'