diff --git a/collects/typed-scheme/env/type-environments.ss b/collects/typed-scheme/env/type-environments.ss
index 6640e8e363..00ceb443ff 100644
--- a/collects/typed-scheme/env/type-environments.ss
+++ b/collects/typed-scheme/env/type-environments.ss
@@ -4,7 +4,7 @@
          (prefix-in r: "../utils/utils.ss")
          scheme/match (r:rep filter-rep rep-utils type-rep) unstable/struct
          (except-in (r:utils tc-utils) make-env)
-         (r:typecheck tc-metafunctions))
+         #;(r:typecheck tc-metafunctions))
 
 (provide current-tvars
          extend
diff --git a/collects/typed-scheme/typecheck/tc-app.ss b/collects/typed-scheme/typecheck/tc-app.ss
index e2ed72376b..32081060ee 100644
--- a/collects/typed-scheme/typecheck/tc-app.ss
+++ b/collects/typed-scheme/typecheck/tc-app.ss
@@ -748,15 +748,19 @@
          (parameterize ([current-orig-stx a]) (check-below arg-t dom-t))))
      ;(printf "got to here 2 ~a ~a ~a ~n" dom names o-a)
      (let* ([dom-count (length dom)]
-            [arg-count (+ dom-count (if rest 1 0) (length kws))]
-            [o-a (for/list ([nm (in-range arg-count)]
-                            [oa (in-sequence-forever (in-list o-a) (make-Empty))])
-                   (if (>= nm dom-count) (make-Empty) oa))])
-       (define-values (t-r f-r o-r)
-         (for/lists (t-r f-r o-r) 
-           ([r (in-list results)])
-           (open-Result r o-a)))
-       (ret t-r f-r o-r))]
+            [arg-count (+ dom-count (if rest 1 0) (length kws))])
+       (let-values
+           ([(o-a t-a) (for/lists (os ts)
+                         ([nm (in-range arg-count)]
+                          [oa (in-sequence-forever (in-list o-a) (make-Empty))]
+                          [ta (in-sequence-forever (in-list t-a) (Un))])
+                         (values (if (>= nm dom-count) (make-Empty) oa)
+                                 ta))])
+         (define-values (t-r f-r o-r)
+           (for/lists (t-r f-r o-r) 
+             ([r (in-list results)])
+             (open-Result r o-a t-a)))
+         (ret t-r f-r o-r)))]
     [((arr: _ _ _ drest '()) _)
      (int-err "funapp with drest args NYI")]
     [((arr: _ _ _ _ kws) _)
diff --git a/collects/typed-scheme/typecheck/tc-if.ss b/collects/typed-scheme/typecheck/tc-if.ss
index 0b0ee46a98..962631f44a 100644
--- a/collects/typed-scheme/typecheck/tc-if.ss
+++ b/collects/typed-scheme/typecheck/tc-if.ss
@@ -4,7 +4,7 @@
 (require (rename-in "../utils/utils.ss" [infer r:infer]))
 (require "signatures.ss"
          (rep type-rep filter-rep object-rep)
-         (rename-in (types convenience subtype union utils comparison remove-intersect abbrev)
+         (rename-in (types convenience subtype union utils comparison remove-intersect abbrev filter-ops)
                     [remove *remove])
          (env lexical-env type-environments)
          (r:infer infer)
@@ -53,6 +53,7 @@
          ;(printf "old els-props: ~a\n" (env-props (lexical-env)))
          ;(printf "fs-: ~a~n" fs-)
          ;(printf "els-props: ~a~n" (env-props env-els))
+         ;(printf "thn-props: ~a~n" (env-props env-thn))
          ;(printf "new-els-props: ~a~n" new-els-props)
          ;; if we have the same number of values in both cases
          (cond [(= (length ts) (length us))
diff --git a/collects/typed-scheme/typecheck/tc-metafunctions.ss b/collects/typed-scheme/typecheck/tc-metafunctions.ss
index e2a589168e..9be99d9b2e 100644
--- a/collects/typed-scheme/typecheck/tc-metafunctions.ss
+++ b/collects/typed-scheme/typecheck/tc-metafunctions.ss
@@ -1,7 +1,7 @@
 #lang scheme/base
 
 (require "../utils/utils.ss")
-(require (rename-in (types subtype convenience remove-intersect union utils)                   
+(require (rename-in (types subtype convenience remove-intersect union utils filter-ops)                   
                     [-> -->]
                     [->* -->*]
                     [one-of/c -one-of/c])
@@ -146,7 +146,9 @@
                (if (OrFilter? new-or)
                    (loop (cons new-or derived-props) derived-atoms (cdr worklist))
                    (loop derived-props derived-atoms (cons new-or (cdr worklist)))))]
+            [(TypeFilter: (== (Un) type-equal?) _ _) (set-box! flag #f) (values derived-props derived-atoms)]
             [(TypeFilter: _ _ _) (loop derived-props (cons p derived-atoms) (cdr worklist))]
+            [(NotTypeFilter: (== Univ type-equal?) _ _) (set-box! flag #f) (values derived-props derived-atoms)]
             [(NotTypeFilter: _ _ _) (loop derived-props (cons p derived-atoms) (cdr worklist))]
             [(Top:) (loop derived-props derived-atoms (cdr worklist))]
             [(Bot:) (set-box! flag #f) (values derived-props derived-atoms)]
diff --git a/collects/typed-scheme/typecheck/tc-subst.ss b/collects/typed-scheme/typecheck/tc-subst.ss
index c52427f5e2..a1ddb45b26 100644
--- a/collects/typed-scheme/typecheck/tc-subst.ss
+++ b/collects/typed-scheme/typecheck/tc-subst.ss
@@ -1,7 +1,7 @@
 #lang scheme/base
 
 (require "../utils/utils.ss")
-(require (rename-in (types subtype convenience remove-intersect union utils)                   
+(require (rename-in (types subtype convenience remove-intersect union utils filter-ops)                   
                     [-> -->]
                     [->* -->*]
                     [one-of/c -one-of/c])
@@ -16,28 +16,23 @@
   (begin (d/c (name . args) c . body)
          (p/c [name c])))
 
-(define (name-ref=? a b)
-  (or (eq? a b)
-      (and (identifier? a)
-           (identifier? b)
-           (free-identifier=? a b))))
-
-(d/c/p (open-Result r objs)
-       (-> Result? (listof Object?) (values Type/c FilterSet? Object?))
+(d/c/p (open-Result r objs ts)
+       (-> Result? (listof Object?) (listof Type/c) (values Type/c FilterSet? Object?))
        (match r
          [(Result: t fs old-obj)
           (for/fold ([t t] [fs fs] [old-obj old-obj])
-            ([(o k) (in-indexed (in-list objs))])
+            ([(o k) (in-indexed (in-list objs))]
+             [arg-ty (in-list ts)])
             (values (subst-type t k o #t)
-                    (subst-filter-set fs k o #t)
+                    (subst-filter-set fs k o #t arg-ty)
                     (subst-object old-obj k o #t)))]))
 
-(d/c/p (subst-filter-set fs k o polarity)
-       (-> FilterSet? name-ref/c Object? boolean? FilterSet?)
+(d/c/p (subst-filter-set fs k o polarity t)
+       (-> FilterSet? name-ref/c Object? boolean? Type/c FilterSet?)
   (match fs
     [(FilterSet: f+ f-)
-     (combine (subst-filter f+ k o polarity) 
-	      (subst-filter f- k o polarity))]))
+     (combine (subst-filter (-and (make-TypeFilter t null k) f+) k o polarity)
+	      (subst-filter (-and (make-TypeFilter t null k) f-) k o polarity))]))
 
 (d/c/p (subst-type t k o polarity)
      (-> Type/c name-ref/c Object? boolean? Type/c)
diff --git a/collects/typed-scheme/types/convenience.ss b/collects/typed-scheme/types/convenience.ss
index 78589b203f..8619e1133c 100644
--- a/collects/typed-scheme/types/convenience.ss
+++ b/collects/typed-scheme/types/convenience.ss
@@ -71,115 +71,3 @@
 
 (define Ident (-Syntax -Symbol))
 
-(define (atomic-filter? e)
-  (or (TypeFilter? e) (NotTypeFilter? e)))
-
-(define (opposite? f1 f2)
-  (match* (f1 f2)
-          [((TypeFilter: t1 p1 i1)
-            (NotTypeFilter: t2 p1 i2))
-           (and (free-identifier=? i1 i2)
-                (subtype t1 t2))]
-          [((NotTypeFilter: t2 p1 i2)
-            (TypeFilter: t1 p1 i1))
-           (and (free-identifier=? i1 i2)
-                (subtype t1 t2))]
-          [(_ _) #f]))
-
-;; is f1 implied by f2?
-(define (implied-atomic? f1 f2)
-  (if (filter-equal? f1 f2)
-      #t
-      (match* (f1 f2)
-              [((TypeFilter: t1 p1 i1)
-                (TypeFilter: t2 p1 i2))
-               (and (free-identifier=? i1 i2)
-                    (subtype t1 t2))]
-              [((NotTypeFilter: t2 p1 i2)
-                (NotTypeFilter: t1 p1 i1))
-               (and (free-identifier=? i1 i2)
-                    (subtype t1 t2))]
-              [(_ _) #f])))
-
-;; props : propositions to compress
-;; or? : is this or OrFilter (alternative is AndFilter)
-(define (compact props or?)
-  (define tf-map (make-hash))
-  (define ntf-map (make-hash))
-  (let loop ([props props] [others null])
-    (if (null? props)
-        (append others
-                (for/list ([v (in-dict-values tf-map)]) v)
-                (for/list ([v (in-dict-values ntf-map)]) v))
-        (match (car props)
-          [(and p (TypeFilter: t1 f1 x) (? (lambda _ or?)))
-           (hash-update! tf-map
-                         (list f1 (hash-id x))
-                         (match-lambda [(TypeFilter: t2 _ _) (make-TypeFilter (Un t1 t2) f1 x)]
-                                       [p (int-err "got something that isn't a typefilter ~a" p)])
-                         p)
-           (loop (cdr props) others)]
-          [(and p (NotTypeFilter: t1 f1 x) (? (lambda _ (not or?))))
-           (hash-update! ntf-map
-                         (list f1 (hash-id x))
-                         (match-lambda [(NotTypeFilter: t2 _ _) (make-NotTypeFilter (Un t1 t2) f1 x)]
-                                       [p (int-err "got something that isn't a nottypefilter ~a" p)])
-                         p)
-           (loop (cdr props) others)]
-          [p (loop (cdr props) (cons p others))]))))
-
-(define (-or . args)
-  (define mk
-    (case-lambda [() -bot]
-                 [(f) f]
-                 [fs (make-OrFilter fs)]))
-  (define (distribute args)
-    (define-values (ands others) (partition AndFilter? args))
-    (if (null? ands)
-        (apply mk others)
-        (match-let ([(AndFilter: elems) (car ands)])
-          (apply -and (for/list ([a (in-list elems)])
-                        (apply -or a (append (cdr ands) others)))))))  
-  (let loop ([fs args] [result null])
-    (if (null? fs)
-        (match result
-          [(list) -bot]
-          [(list f) f]
-          [_ (distribute (compact result #t))])
-        (match (car fs)
-          [(and t (Top:)) t]
-          [(OrFilter: fs*) (loop (append fs* (cdr fs)) result)]
-          [(Bot:) (loop (cdr fs) result)]
-          [t 
-           (cond [(for/or ([f (in-list (append (cdr fs) result))])
-                    (opposite? f t))
-                  -top]
-                 [(for/or ([f (in-list result)]) (or (filter-equal? f t) (implied-atomic? f t)))
-                  (loop (cdr fs) result)]
-                 [else
-                  (loop (cdr fs) (cons t result))])]))))
-
-(define (-and . args) 
-  (let loop ([fs (remove-duplicates args filter-equal?)] [result null])
-    (if (null? fs)
-        (match result
-          [(list) -top]
-          [(list f) f]
-          ;; don't think this is useful here
-          [(list f1 f2) (if (opposite? f1 f2)
-                            -bot
-                            (if (filter-equal? f1 f2)
-                                f1
-                                (make-AndFilter (compact (list f1 f2) #f))))]
-          [_ (make-AndFilter (compact result #f))])
-        (match (car fs)
-          [(and t (Bot:)) t]
-          [(AndFilter: fs*) (loop (cdr fs) (append fs* result))]
-          [(Top:) (loop (cdr fs) result)]
-          [t (cond [(for/or ([f (in-list (append (cdr fs) result))])
-                      (opposite? f t))
-                    -bot]
-                   [(for/or ([f (in-list result)]) (or (filter-equal? f t) (implied-atomic? t f)))
-                    (loop (cdr fs) result)]
-                   [else
-                    (loop (cdr fs) (cons t result))])]))))
diff --git a/collects/typed-scheme/types/filter-ops.ss b/collects/typed-scheme/types/filter-ops.ss
new file mode 100644
index 0000000000..72aa081241
--- /dev/null
+++ b/collects/typed-scheme/types/filter-ops.ss
@@ -0,0 +1,156 @@
+#lang scheme/base
+
+(require "../utils/utils.ss"
+         (rep type-rep filter-rep object-rep rep-utils)
+         (utils tc-utils) (only-in (infer infer) restrict)
+         "abbrev.ss" (only-in scheme/contract current-blame-format [-> -->] listof)
+	 (types comparison printer union subtype utils remove-intersect)
+         scheme/list scheme/match scheme/promise
+         (for-syntax syntax/parse scheme/base)
+         unstable/debug syntax/id-table scheme/dict
+         scheme/trace
+         (for-template scheme/base))
+
+(provide (all-defined-out))
+
+(define (atomic-filter? e)
+  (or (TypeFilter? e) (NotTypeFilter? e)))
+
+(define (opposite? f1 f2)
+  (match* (f1 f2)
+          [((TypeFilter: t1 p1 i1)
+            (NotTypeFilter: t2 p1 i2))
+           (and (name-ref=? i1 i2)
+                (subtype t1 t2))]
+          [((NotTypeFilter: t2 p1 i2)
+            (TypeFilter: t1 p1 i1))
+           (and (name-ref=? i1 i2)
+                (subtype t1 t2))]
+          [(_ _) #f]))
+
+
+(define (name-ref=? a b)
+  (or (eq? a b)
+      (and (identifier? a)
+           (identifier? b)
+           (free-identifier=? a b))))
+
+;; is f1 implied by f2?
+(define (implied-atomic? f1 f2)
+  (if (filter-equal? f1 f2)
+      #t
+      (match* (f1 f2)
+              [((TypeFilter: t1 p1 i1)
+                (TypeFilter: t2 p1 i2))
+               (and (name-ref=? i1 i2)
+                    (subtype t1 t2))]
+              [((NotTypeFilter: t2 p1 i2)
+                (NotTypeFilter: t1 p1 i1))
+               (and (name-ref=? i1 i2)
+                    (subtype t1 t2))]
+              [(_ _) #f])))
+
+(define (hash-name-ref i)
+  (if (identifier? i) (hash-id i) i))
+
+;; compact : (Listof prop) bool -> (Listof prop)
+;; props : propositions to compress
+;; or? : is this an OrFilter (alternative is AndFilter)
+(d/c (compact props or?)
+     ((listof Filter/c) boolean? . --> . (listof Filter/c))
+  (define tf-map (make-hash))
+  (define ntf-map (make-hash))
+  (let loop ([props props] [others null])
+    (if (null? props)
+        (append others
+                (for/list ([v (in-dict-values tf-map)]) v)
+                (for/list ([v (in-dict-values ntf-map)]) v))
+        (match (car props)
+          [(and p (TypeFilter: t1 f1 x) (? (lambda _ or?)))
+           (hash-update! tf-map
+                         (list f1 (hash-name-ref x))
+                         (match-lambda [(TypeFilter: t2 _ _) (make-TypeFilter (Un t1 t2) f1 x)]
+                                       [p (int-err "got something that isn't a typefilter ~a" p)])
+                         p)
+           (loop (cdr props) others)]
+          [(and p (TypeFilter: t1 f1 x) (? (lambda _ (not or?))))
+           (match (hash-ref tf-map (list f1 (hash-name-ref x)) #f)
+             [(TypeFilter: (? (lambda (t2) (not (overlap t1 t2)))) _ _)
+              ;; we're in an And, and we got two types for the same path that do not overlap
+              (list -bot)]
+             [(TypeFilter: t2 _ _)
+              (hash-set! tf-map (list f1 (hash-name-ref x))
+                         (make-TypeFilter (restrict t1 t2) f1 x))
+              (loop (cdr props) others)]
+             [#f
+              (hash-set! tf-map (list f1 (hash-name-ref x))
+                         (make-TypeFilter t1 f1 x))
+              (loop (cdr props) others)])]
+          [(and p (NotTypeFilter: t1 f1 x) (? (lambda _ (not or?))))
+           (hash-update! ntf-map
+                         (list f1 (hash-name-ref x))
+                         (match-lambda [(NotTypeFilter: t2 _ _) (make-NotTypeFilter (Un t1 t2) f1 x)]
+                                       [p (int-err "got something that isn't a nottypefilter ~a" p)])
+                         p)
+           (loop (cdr props) others)]
+          [p (loop (cdr props) (cons p others))]))))
+
+(define (-or . args)
+  (define mk
+    (case-lambda [() -bot]
+                 [(f) f]
+                 [fs (make-OrFilter fs)]))
+  (define (distribute args)
+    (define-values (ands others) (partition AndFilter? args))
+    (if (null? ands)
+        (apply mk others)
+        (match-let ([(AndFilter: elems) (car ands)])
+          (apply -and (for/list ([a (in-list elems)])
+                        (apply -or a (append (cdr ands) others)))))))  
+  (let loop ([fs args] [result null])
+    (if (null? fs)
+        (match result
+          [(list) -bot]
+          [(list f) f]
+          [_ (distribute (compact result #t))])
+        (match (car fs)
+          [(and t (Top:)) t]
+          [(OrFilter: fs*) (loop (append fs* (cdr fs)) result)]
+          [(Bot:) (loop (cdr fs) result)]
+          [t 
+           (cond [(for/or ([f (in-list (append (cdr fs) result))])
+                    (opposite? f t))
+                  -top]
+                 [(for/or ([f (in-list result)]) (or (filter-equal? f t) (implied-atomic? f t)))
+                  (loop (cdr fs) result)]
+                 [else
+                  (loop (cdr fs) (cons t result))])]))))
+
+(define (-and . args)
+  (define mk
+    (case-lambda [() -top]
+                 [(f) f]
+                 [fs (make-AndFilter fs)]))
+  (let loop ([fs (remove-duplicates args filter-equal?)] [result null])
+    (if (null? fs)
+        (match result
+          [(list) -top]
+          [(list f) f]
+          ;; don't think this is useful here
+          [(list f1 f2) (if (opposite? f1 f2)
+                            -bot
+                            (if (filter-equal? f1 f2)
+                                f1
+                                (apply mk (compact (list f1 f2) #f))))]
+          [_ (apply mk (compact result #f))])
+        (match (car fs)
+          [(and t (Bot:)) t]
+          [(AndFilter: fs*) (loop (cdr fs) (append fs* result))]
+          [(Top:) (loop (cdr fs) result)]
+          [t (cond [(for/or ([f (in-list (append (cdr fs) result))])
+                      (opposite? f t))
+                    -bot]
+                   [(for/or ([f (in-list result)]) (or (filter-equal? f t) (implied-atomic? t f)))
+                    (loop (cdr fs) result)]
+                   [else
+                    (loop (cdr fs) (cons t result))])]))))