diff --git a/collects/typed-scheme/typecheck/signatures.ss b/collects/typed-scheme/typecheck/signatures.ss
index 76c69b1b25..c68b5e95e1 100644
--- a/collects/typed-scheme/typecheck/signatures.ss
+++ b/collects/typed-scheme/typecheck/signatures.ss
@@ -10,13 +10,13 @@
    [cnt tc-toplevel-form (syntax? . -> . any)]))
 
 (define-signature tc-expr^
-  ([cnt tc-expr (syntax? . -> . tc-result?)]
-   [cnt tc-expr/check (syntax? Type/c . -> . tc-result?)]
+  ([cnt tc-expr (syntax? . -> . tc-results?)]
+   [cnt tc-expr/check (syntax? tc-results? . -> . tc-results?)]
    [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/c . -> . tc-result?)]
+   [cnt check-below (->d ([s (or/c Type/c tc-results?)] [t (or/c Type/c tc-results?)]) () [_ (if (Type? s) Type/c tc-results?)])]
+   ;[cnt tc-literal (any/c . -> . Type/c)]
+   [cnt tc-exprs ((listof syntax?) . -> . tc-results?)]
+   [cnt tc-exprs/check ((listof syntax?) Type/c . -> . tc-results?)]
    [cnt tc-expr/t (syntax? . -> . Type/c)]))
 
 (define-signature check-subforms^
@@ -25,24 +25,24 @@
    [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/c . -> . tc-result?)]))
+  ([cnt tc/if-twoarm (syntax? syntax? syntax? . -> . tc-results?)]   
+   [cnt tc/if-twoarm/check (syntax? syntax? syntax? Type/c . -> . tc-results?)]))
 
 (define-signature tc-lambda^
-  ([cnt tc/lambda (syntax? syntax? syntax? . -> . tc-result?)]
-   [cnt tc/lambda/check (syntax? syntax? syntax? Type/c . -> . tc-result?)]
+  ([cnt tc/lambda (syntax? syntax? syntax? . -> . tc-results?)]
+   [cnt tc/lambda/check (syntax? syntax? syntax? Type/c . -> . tc-results?)]
    [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/c . -> . tc-result?)]
-   [cnt tc/funapp (syntax? syntax? tc-result? (listof tc-result?) (or/c #f Type/c) . -> . tc-result?)]))
+  ([cnt tc/app (syntax? . -> . tc-results?)] 
+   [cnt tc/app/check (syntax? tc-results? . -> . tc-results?)]
+   [cnt tc/funapp (syntax? syntax? tc-result? (listof tc-results?) (or/c #f Type/c) . -> . tc-results?)]))
 
 (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/c . -> . tc-result?)]
-   [cnt tc/letrec-values/check (syntax? syntax? syntax? syntax? Type/c . -> . tc-result?)]))
+  ([cnt tc/let-values (syntax? syntax? syntax? syntax? . -> . tc-results?)]
+   [cnt tc/letrec-values (syntax? syntax? syntax? syntax? . -> . tc-results?)]
+   [cnt tc/let-values/check (syntax? syntax? syntax? syntax? tc-results? . -> . tc-results?)]
+   [cnt tc/letrec-values/check (syntax? syntax? syntax? syntax? tc-results? . -> . tc-results?)]))
 
 (define-signature tc-dots^
   ([cnt tc/dots (syntax? . -> . (values Type/c symbol?))]))
diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss
index d83daf0dd4..ae1ebf768d 100644
--- a/collects/typed-scheme/typecheck/tc-expr-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-expr-unit.ss
@@ -3,7 +3,7 @@
 
 (require (rename-in "../utils/utils.ss" [private private-in]))
 (require syntax/kerncase
-         scheme/match
+         scheme/match (prefix-in - scheme/contract)
          "signatures.ss"
          (types utils convenience union subtype)
          (private-in parse-type type-annotation)
@@ -23,7 +23,8 @@
 
 ;; return the type of a literal value
 ;; scheme-value -> type
-(define (tc-literal v-stx [expected #f])
+(d/c (tc-literal v-stx [expected #f])
+  (-->* (syntax?) ((-or/c #f Type/c)) Type/c)
   (define-syntax-class exp
     (pattern i
              #:when expected
@@ -45,7 +46,7 @@
     [(i ...) 
      (-Tuple (map tc-literal (syntax->list #'(i ...))))]
     [i #:declare i (3d vector?)
-     (make-Vector (apply Un (map tc-literal (vector->list #'i.datum))))]
+       (make-Vector (apply Un (map tc-literal (vector->list #'i.datum))))]
     [_ Univ]))
 
 
@@ -120,15 +121,20 @@
   (match (tc-expr/check e t)
     [(tc-result: t) t]))
 
-;; check-below : (/\ (Result Type -> Result)
+;; check-below : (/\ (Results Type -> Result)
+;;                   (Results Results -> Result)
 ;;                   (Type Type -> Type))
 (define (check-below tr1 expected)
-  (match (list tr1 expected)      
-    [(list (tc-result: t1 te1 ee1) t2)
+  (match* (tr1 expected)
+    [((tc-results: t1) (tc-results: t2))
+     (unless (andmap subtype t1 t2)
+       (tc-error/expr "Expected ~a, but got ~a" t2 t1))
+     (ret expected)]
+    [((tc-result1: t1) (? Type? t2))
      (unless (subtype t1 t2)
        (tc-error/expr "Expected ~a, but got ~a" t2 t1))
      (ret expected)]
-    [(list t1 t2)
+    [((? Type? t1) (? Type? t2))
      (unless (subtype t1 t2)
        (tc-error/expr"Expected ~a, but got ~a" t2 t1))
      expected]))
@@ -159,7 +165,9 @@
         ;; data
         [(quote #f) (ret (-val #f) false-filter)]
         [(quote #t) (ret (-val #t) true-filter)]
-        [(quote val)  (ret (tc-literal #'val expected))]
+        [(quote val)  (match expected
+                        [(tc-result1: t)
+                         (ret (tc-literal #'val t))])]
         ;; syntax
         [(quote-syntax datum) (ret (-Syntax (tc-literal #'datum)))]
         ;; mutation!
@@ -314,9 +322,9 @@
                                                  (tc-expr/check form ann))]
                     [else (internal-tc-expr form)])])
       (match ty
-        [(tc-result: t eff1 eff2)
-         (let ([ty* (do-inst form t)])
-           (ret ty* eff1 eff2))]))))
+        [(tc-results: ts fs os)
+         (let ([ts* (do-inst form ts)])
+           (ret ts fs os))]))))
 
 (define (tc/send rcvr method args [expected #f])
   (match (tc-expr rcvr)
diff --git a/collects/typed-scheme/typecheck/tc-lambda-unit.ss b/collects/typed-scheme/typecheck/tc-lambda-unit.ss
index d443fd77bc..c6dbd98474 100644
--- a/collects/typed-scheme/typecheck/tc-lambda-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-lambda-unit.ss
@@ -19,10 +19,10 @@
 (import tc-expr^)
 (export tc-lambda^)
 
-(d-s/c lam-result ([args (listof (list identifier? Type/c))] 
-                   [kws (listof (list keyword? identifier? Type/c boolean?))]
+(d-s/c lam-result ([args (listof (list/c identifier? Type/c))] 
+                   [kws (listof (list/c keyword? identifier? Type/c boolean?))]
                    [rest (or/c #f Type/c)]
-                   [drest (or/c #f (cons symbol? Type/c))]
+                   [drest (or/c #f (cons/c symbol? Type/c))]
                    [body tc-results?])
        #:transparent)
 
diff --git a/collects/typed-scheme/typecheck/tc-new-app-unit.ss b/collects/typed-scheme/typecheck/tc-new-app-unit.ss
new file mode 100644
index 0000000000..a29568b275
--- /dev/null
+++ b/collects/typed-scheme/typecheck/tc-new-app-unit.ss
@@ -0,0 +1,18 @@
+#lang scheme/unit
+
+(require "signatures.ss" "../utils/utils.ss")
+(require (utils tc-utils))
+
+(import tc-expr^ tc-lambda^ tc-dots^)
+(export tc-app^)
+
+(define (tc/app . args)
+  (int-err "tc/app NYI"))
+
+(define (tc/app/check . args)
+  (int-err "tc/app/check NYI"))
+
+(define (tc/funapp . args)
+  (int-err "tc/funapp NYI"))
+
+
diff --git a/collects/typed-scheme/typecheck/tc-toplevel.ss b/collects/typed-scheme/typecheck/tc-toplevel.ss
index 937568aab1..fce1a1a30e 100644
--- a/collects/typed-scheme/typecheck/tc-toplevel.ss
+++ b/collects/typed-scheme/typecheck/tc-toplevel.ss
@@ -161,7 +161,7 @@
       [(define-values (var ...) expr)
        (let* ([vars (syntax->list #'(var ...))]
               [ts (map lookup-type vars)])
-         (tc-expr/check #'expr (-values ts)))
+         (tc-expr/check #'expr (ret ts)))
        (void)]
       
       ;; to handle the top-level, we have to recur into begins
diff --git a/collects/typed-scheme/typecheck/typechecker.ss b/collects/typed-scheme/typecheck/typechecker.ss
index ed935ff901..2f41a66a9e 100644
--- a/collects/typed-scheme/typecheck/typechecker.ss
+++ b/collects/typed-scheme/typecheck/typechecker.ss
@@ -5,11 +5,11 @@
          mzlib/trace
          (only-in scheme/unit provide-signature-elements)
          "signatures.ss" "tc-toplevel.ss"         
-         "tc-if-unit.ss" "tc-lambda-unit.ss" "tc-app-unit.ss"
+         "tc-new-if.ss" "tc-lambda-unit.ss" "tc-new-app-unit.ss"
          "tc-let-unit.ss" "tc-dots-unit.ss"
          "tc-expr-unit.ss" "check-subforms-unit.ss")
 
 (provide-signature-elements typechecker^ tc-expr^)
 
 (define-values/link-units/infer
-  tc-toplevel@ tc-if@ tc-lambda@ tc-dots@ tc-app@ tc-let@ tc-expr@ check-subforms@)
+  tc-toplevel@ tc-new-if@ tc-lambda@ tc-dots@ tc-new-app@ tc-let@ tc-expr@ check-subforms@)
diff --git a/collects/typed-scheme/types/utils.ss b/collects/typed-scheme/types/utils.ss
index 0c4af4ee67..facbcf88ad 100644
--- a/collects/typed-scheme/types/utils.ss
+++ b/collects/typed-scheme/types/utils.ss
@@ -180,7 +180,12 @@
    [(_ tp fp op dty dbound) #'(struct tc-results ((list (struct tc-result (tp fp op)) (... ...)) (cons dty dbound)))]
    [(_ tp) #'(struct tc-results ((list (struct tc-result (tp _ _)) (... ...)) #f))]))
 
-(provide tc-result: tc-results: tc-result? tc-results?)
+(define-match-expander tc-result1:
+  (syntax-parser
+   [(_ tp fp op) #'(struct tc-results ((list (struct tc-result (tp fp op))) #f))]
+   [(_ tp) #'(struct tc-results ((list (struct tc-result (tp _ _))) #f))]))
+
+(provide tc-result: tc-results: tc-result1: tc-result? tc-results?)
 
 ;; convenience function for returning the result of typechecking an expression
 (define ret
@@ -214,7 +219,7 @@
         [o (if (list? t)
                (listof Object?)
                Object?)])                
-       [_ (listof tc-result?)])])
+       [_ tc-results?])])
 
 (define (subst v t e) (substitute t v e))