diff --git a/collects/typed-scheme/typecheck/signatures.ss b/collects/typed-scheme/typecheck/signatures.ss
index ec810d10..76c69b1b 100644
--- a/collects/typed-scheme/typecheck/signatures.ss
+++ b/collects/typed-scheme/typecheck/signatures.ss
@@ -11,39 +11,39 @@
 
 (define-signature tc-expr^
   ([cnt tc-expr (syntax? . -> . tc-result?)]
-   [cnt tc-expr/check (syntax? Type? . -> . tc-result?)]
-   [cnt tc-expr/check/t (syntax? Type? . -> . Type?)]
-   [cnt check-below (->d ([s (or/c Type? tc-result?)] [t Type?]) () [_ (if (Type? s) Type? tc-result?)])]
-   [cnt tc-literal (any/c . -> . Type?)]
+   [cnt tc-expr/check (syntax? Type/c . -> . tc-result?)]
+   [cnt tc-expr/check/t (syntax? Type/c . -> . Type/c)]
+   [cnt check-below (->d ([s (or/c Type/c tc-result?)] [t Type/c]) () [_ (if (Type/c s) Type/c tc-result?)])]
+   [cnt tc-literal (any/c . -> . Type/c)]
    [cnt tc-exprs ((listof syntax?) . -> . tc-result?)]
-   [cnt tc-exprs/check ((listof syntax?) Type? . -> . tc-result?)]
-   [cnt tc-expr/t (syntax? . -> . Type?)]))
+   [cnt tc-exprs/check ((listof syntax?) Type/c . -> . tc-result?)]
+   [cnt tc-expr/t (syntax? . -> . Type/c)]))
 
 (define-signature check-subforms^
   ([cnt check-subforms/ignore (syntax? . -> . any)]
    [cnt check-subforms/with-handlers (syntax? . -> . any)]
-   [cnt check-subforms/with-handlers/check (syntax? Type? . -> . any)]))
+   [cnt check-subforms/with-handlers/check (syntax? Type/c . -> . any)]))
 
 (define-signature tc-if^
   ([cnt tc/if-twoarm (syntax? syntax? syntax? . -> . tc-result?)]   
-   [cnt tc/if-twoarm/check (syntax? syntax? syntax? Type? . -> . tc-result?)]))
+   [cnt tc/if-twoarm/check (syntax? syntax? syntax? Type/c . -> . tc-result?)]))
 
 (define-signature tc-lambda^
   ([cnt tc/lambda (syntax? syntax? syntax? . -> . tc-result?)]
-   [cnt tc/lambda/check (syntax? syntax? syntax? Type? . -> . tc-result?)]
-   [cnt tc/rec-lambda/check (syntax? syntax? syntax? syntax? (listof Type?) Type? . -> . Type?)]))
+   [cnt tc/lambda/check (syntax? syntax? syntax? Type/c . -> . tc-result?)]
+   [cnt tc/rec-lambda/check (syntax? syntax? syntax? syntax? (listof Type/c) Type/c . -> . Type/c)]))
 
 (define-signature tc-app^
   ([cnt tc/app (syntax? . -> . tc-result?)] 
-   [cnt tc/app/check (syntax? Type? . -> . tc-result?)]
-   [cnt tc/funapp (syntax? syntax? tc-result? (listof tc-result?) (or/c #f Type?) . -> . tc-result?)]))
+   [cnt tc/app/check (syntax? Type/c . -> . tc-result?)]
+   [cnt tc/funapp (syntax? syntax? tc-result? (listof tc-result?) (or/c #f Type/c) . -> . tc-result?)]))
 
 (define-signature tc-let^
   ([cnt tc/let-values (syntax? syntax? syntax? syntax? . -> . tc-result?)]
    [cnt tc/letrec-values (syntax? syntax? syntax? syntax? . -> . tc-result?)]
-   [cnt tc/let-values/check (syntax? syntax? syntax? syntax? Type? . -> . tc-result?)]
-   [cnt tc/letrec-values/check (syntax? syntax? syntax? syntax? Type? . -> . tc-result?)]))
+   [cnt tc/let-values/check (syntax? syntax? syntax? syntax? Type/c . -> . tc-result?)]
+   [cnt tc/letrec-values/check (syntax? syntax? syntax? syntax? Type/c . -> . tc-result?)]))
 
 (define-signature tc-dots^
-  ([cnt tc/dots (syntax? . -> . (values Type? symbol?))]))
+  ([cnt tc/dots (syntax? . -> . (values Type/c symbol?))]))
 
diff --git a/collects/typed-scheme/typecheck/tc-envops.ss b/collects/typed-scheme/typecheck/tc-envops.ss
index 2b4f8496..a7fa2786 100644
--- a/collects/typed-scheme/typecheck/tc-envops.ss
+++ b/collects/typed-scheme/typecheck/tc-envops.ss
@@ -12,6 +12,8 @@
          stxclass/util
          (for-syntax scheme/base))
 
+(provide env+)
+
 (define (replace-nth l i f)
   (cond [(null? l) (error 'replace-nth "list not long enough" l i f)]
         [(zero? i) (cons (f (car l)) (cdr l))]
diff --git a/collects/typed-scheme/typecheck/tc-metafunctions.ss b/collects/typed-scheme/typecheck/tc-metafunctions.ss
index 96258fd0..090e6004 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)                   
+(require (rename-in (types subtype convenience remove-intersect union)                   
                     [-> -->]
                     [->* -->*]
                     [one-of/c -one-of/c])
@@ -10,6 +10,8 @@
          stxclass/util
          (for-syntax scheme/base))
 
+(provide combine-filter apply-filter abstract-filter)
+
 ;; this implements the sequence invariant described on the first page relating to Bot
 (define (lcombine l1 l2)
   (cond [(memq (make-LBot) l1)
diff --git a/collects/typed-scheme/typecheck/tc-new-if.ss b/collects/typed-scheme/typecheck/tc-new-if.ss
new file mode 100644
index 00000000..95b70021
--- /dev/null
+++ b/collects/typed-scheme/typecheck/tc-new-if.ss
@@ -0,0 +1,39 @@
+#lang scheme/unit
+
+
+(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)
+                    [remove *remove])
+         (env lexical-env)
+         (r:infer infer)
+	 (utils tc-utils mutated-vars)
+         (typecheck tc-envops tc-metafunctions)
+         syntax/kerncase
+         mzlib/trace
+         mzlib/plt-match)
+
+;; if typechecking   
+(import tc-expr^)
+(export tc-if^)
+
+(define (tc/if-twoarm tst thn els [expected #f])
+  (define (tc e) (if expected (tc-expr/check e expected) (tc-expr e)))
+  (match (tc-expr tst)
+    [(list (tc-result: _ (and f1 (FilterSet: fs+ fs-)) _))
+     (match-let ([(tc-results: ts fs2 _) (with-lexical-env (env+ (lexical-env) fs+) (tc thn))]
+                 [(tc-results: us fs3 _) (with-lexical-env (env+ (lexical-env) fs-) (tc els))])
+       ;; if we have the same number of values in both cases
+       (cond [(= (length ts) (length us))
+              (for/list ([t ts] [u us] [f2 fs2] [f3 fs3])
+                (ret (Un t u) (combine-filter f1 f2 f2)))]
+             [else
+              (tc-error/expr #:ret (ret Err)
+                             "Expected the same number of values from both branches of if expression, but got ~a and ~a"
+                             (length ts) (length us))]))]
+    [(tc-results: t _ _)
+     (tc-error/expr #:ret (ret (or expected Err))
+                    "Test expression expects one value, given ~a" t)]))
+
+(define tc/if-twoarm/check tc/if-twoarm)
\ No newline at end of file
diff --git a/collects/typed-scheme/types/utils.ss b/collects/typed-scheme/types/utils.ss
index d92760d7..202c7414 100644
--- a/collects/typed-scheme/types/utils.ss
+++ b/collects/typed-scheme/types/utils.ss
@@ -167,6 +167,17 @@
 
 ;; this structure represents the result of typechecking an expression
 (d-s/c tc-result ([t Type/c] [f FilterSet?] [o Object?]) #:transparent)
+(define-struct tc-result (t f o) #:transparent #:omit-define-values)
+
+(define-match-expander tc-result:
+  (syntax-parser
+   [(_ tp fp op) #'(struct tc-result (tp fp op))]))
+
+(define-match-expander tc-results:
+  (syntax-parser
+   [(_ tp fp op) #'(list (struct tc-result (tp fp op)) (... ...))]))
+
+(provide tc-result: tc-results:)
 
 ;; convenience function for returning the result of typechecking an expression
 (define ret
@@ -175,7 +186,10 @@
                     (list (make-tc-result t (make-FilterSet null null) (make-Empty)))
                     (for/list ([i t])
                         (make-tc-result i (make-FilterSet null null) (make-Empty))))]
-               [(t f) (error 'ret "two arguments not supported")]
+               [(t f) (if (Type? t)
+                          (list (make-tc-result t f (make-Empty)))
+                          (for/list ([i t] [f f])
+                            (make-tc-result i f (make-Empty))))]
                [(t f o)
                 (if (and (list? t) (list? f) (list? o))
                     (map make-tc-result t f o)
@@ -187,11 +201,9 @@
        ([f (if (list? t)
                (listof FilterSet?)
                FilterSet?)]
-        [o (if (or (list? f) (FilterSet? f))
-               (if (list? t)
-                   (listof Object?)
-                   Object?)
-               (lambda (e) (eq? e f)))])                
+        [o (if (list? t)
+               (listof Object?)
+               Object?)])                
        [_ (listof tc-result?)])])
 
 (define (subst v t e) (substitute t v e))