diff --git a/collects/typed-scheme/test.ss b/collects/typed-scheme/test.ss
index a5354a7f..90be8df4 100644
--- a/collects/typed-scheme/test.ss
+++ b/collects/typed-scheme/test.ss
@@ -9,3 +9,14 @@
 (plambda: (a) ([y : a]) y)
 (plambda: (a) ([y : a]) y)
 (plambda: () ([y : Boolean]) (if y #t #f))
+
+#{(if #t #t #t) :: Boolean}
+
+(let () 3)
+(let ([x 1] [y 2]) x)
+#{(let ([x 1] [y 2]) x) :: Number}
+(let: ([x : Number 1] [y : Integer 2]) x)
+#{(let: ([x : Integer 1] [y : Integer 2]) x) :: Integer}
+
+#{(let*: ([x : Number 1] [x : Integer 2]) x) :: Integer}
+
diff --git a/collects/typed-scheme/typecheck/signatures.ss b/collects/typed-scheme/typecheck/signatures.ss
index c68b5e95..577dbd2b 100644
--- a/collects/typed-scheme/typecheck/signatures.ss
+++ b/collects/typed-scheme/typecheck/signatures.ss
@@ -12,11 +12,11 @@
 (define-signature tc-expr^
   ([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 tc-expr/check/t (syntax? tc-results? . -> . Type/c)]
    [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-exprs/check ((listof syntax?) tc-results? . -> . tc-results?)]
    [cnt tc-expr/t (syntax? . -> . Type/c)]))
 
 (define-signature check-subforms^
@@ -26,11 +26,11 @@
 
 (define-signature tc-if^
   ([cnt tc/if-twoarm (syntax? syntax? syntax? . -> . tc-results?)]   
-   [cnt tc/if-twoarm/check (syntax? syntax? syntax? Type/c . -> . tc-results?)]))
+   [cnt tc/if-twoarm/check (syntax? syntax? syntax? tc-results? . -> . tc-results?)]))
 
 (define-signature tc-lambda^
   ([cnt tc/lambda (syntax? syntax? syntax? . -> . tc-results?)]
-   [cnt tc/lambda/check (syntax? syntax? syntax? Type/c . -> . tc-results?)]
+   [cnt tc/lambda/check (syntax? syntax? syntax? tc-results? . -> . tc-results?)]
    [cnt tc/rec-lambda/check (syntax? syntax? syntax? syntax? (listof Type/c) Type/c . -> . Type/c)]))
 
 (define-signature tc-app^
diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss
index 9dbc9eab..aaee854b 100644
--- a/collects/typed-scheme/typecheck/tc-expr-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-expr-unit.ss
@@ -126,7 +126,7 @@
 
 (define (tc-expr/check/t e t)
   (match (tc-expr/check e t)
-    [(tc-result: t) t]))
+    [(tc-result1: t) t]))
 
 ;; check-below : (/\ (Results Type -> Result)
 ;;                   (Results Results -> Result)
@@ -146,6 +146,10 @@
        (tc-error/expr "Expected ~a, but got ~a" t2 t1))
      expected]))
 
+(define (tc-expr/check/type form expected)
+  #;(syntax? Type/c . -> . tc-results?)
+  (tc-expr/check form (ret expected)))
+
 ;; tc-expr/check : syntax tc-results -> tc-results
 (define (tc-expr/check form expected)
   (parameterize ([current-orig-stx form])
@@ -194,8 +198,8 @@
            (check-below (tc-id #'x) expected)]
         ;; w-c-m
         [(with-continuation-mark e1 e2 e3)
-         (begin (tc-expr/check #'e1 Univ)
-                (tc-expr/check #'e2 Univ)
+         (begin (tc-expr/check/type #'e1 Univ)
+                (tc-expr/check/type #'e2 Univ)
                 (tc-expr/check #'e3 expected))]  
         ;; application        
         [(#%plain-app . _) (tc/app/check form expected)]
@@ -264,8 +268,8 @@
       [(quote-syntax datum) (ret (-Syntax (tc-literal #'datum)))]
       ;; w-c-m
       [(with-continuation-mark e1 e2 e3)
-       (begin (tc-expr/check #'e1 Univ)
-              (tc-expr/check #'e2 Univ)
+       (begin (tc-expr/check/type #'e1 Univ)
+              (tc-expr/check/type #'e2 Univ)
               (tc-expr #'e3))]
       ;; lambda
       [(#%plain-lambda formals . body)
@@ -326,7 +330,7 @@
       (int-err "bad form input to tc-expr: ~a" form))
     ;; typecheck form
     (let ([ty (cond [(type-ascription form) => (lambda (ann)
-                                                 (tc-expr/check form ann))]
+                                                 (tc-expr/check/type form ann))]
                     [else (internal-tc-expr form)])])
       (match ty
         [(tc-results: ts fs os)
@@ -353,11 +357,11 @@
 (define (tc-exprs exprs)
   (cond [(null? exprs) (ret -Void)]
         [(null? (cdr exprs)) (tc-expr (car exprs))]
-        [else (tc-expr/check (car exprs) Univ)
+        [else (tc-expr/check/type (car exprs) Univ)
               (tc-exprs (cdr exprs))]))
 
 (define (tc-exprs/check exprs expected)
   (cond [(null? exprs) (check-below (ret -Void) expected)]
         [(null? (cdr exprs)) (tc-expr/check (car exprs) expected)]
-        [else (tc-expr/check (car exprs) Univ)
+        [else (tc-expr/check/type (car exprs) Univ)
               (tc-exprs/check (cdr exprs) expected)]))
diff --git a/collects/typed-scheme/typecheck/tc-let-unit.ss b/collects/typed-scheme/typecheck/tc-let-unit.ss
index c8a3a1ce..81ae2668 100644
--- a/collects/typed-scheme/typecheck/tc-let-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-let-unit.ss
@@ -126,7 +126,8 @@
          ;; the types of the exprs
          #;[inferred-types (map (tc-expr-t/maybe-expected expected) exprs)]
          ;; the annotated types of the name (possibly using the inferred types)
-         [types (for/list ([name names] [e exprs]) (get-type/infer name e (tc-expr-t/maybe-expected expected) tc-expr/check/t))]
+         [types (for/list ([name names] [e exprs]) (get-type/infer name e (tc-expr-t/maybe-expected expected) 
+                                                                   (lambda (e t) (tc-expr/check/t e (ret t)))))]
          ;; the clauses for error reporting
          [clauses (syntax-case form () [(lv cl . b) (syntax->list #'cl)])])
     (do-check void names types form types body clauses expected)))