diff --git a/collects/tests/typed-racket/unit-tests/typecheck-tests.rkt b/collects/tests/typed-racket/unit-tests/typecheck-tests.rkt
index 899add9dae..5d7497d4a5 100644
--- a/collects/tests/typed-racket/unit-tests/typecheck-tests.rkt
+++ b/collects/tests/typed-racket/unit-tests/typecheck-tests.rkt
@@ -1612,6 +1612,10 @@
         [tc-err (vector-set! (ann (vector 'a 'b) (Vector Symbol Symbol)) -4 'c)]
         [tc-e (vector-set! (ann (vector 'a 'b) (Vector Symbol Symbol)) (+ -1 2) 'c)
               -Void]
+        [tc-err
+          (ann 
+            ((letrec ((x (lambda (acc #{ v : Symbol}) (if v (list v) acc)))) x) null (list 'bad 'prog))
+            (Listof Symbol))]
         )
   (test-suite
    "check-type tests"
diff --git a/collects/typed-racket/typecheck/tc-app/tc-app-lambda.rkt b/collects/typed-racket/typecheck/tc-app/tc-app-lambda.rkt
index 13180d8648..1efad62de5 100644
--- a/collects/typed-racket/typecheck/tc-app/tc-app-lambda.rkt
+++ b/collects/typed-racket/typecheck/tc-app/tc-app-lambda.rkt
@@ -63,8 +63,10 @@
      (let* ([ts1 (generalize (tc-expr/t #'actual))]
             [ann-ts (for/list ([a (in-syntax #'(acc ...))]
                                [ac (in-syntax #'(actuals ...))])
-                      (or (find-annotation #'inner-body a)
-                          (generalize (tc-expr/t ac))))]
+                      (let ([type (find-annotation #'inner-body a)])
+                        (if type
+                            (tc-expr/check/t ac (ret type))
+                            (generalize (tc-expr/t ac)))))]
             [ts (cons ts1 ann-ts)])
        ;; check that the actual arguments are ok here
        (for/list ([a (syntax->list #'(actuals ...))]
@@ -80,9 +82,10 @@
      #:when (free-identifier=? #'val #'e3)
      (let ([ts (for/list ([ac (syntax->list #'(actuals ...))]
                           [f (syntax->list #'(acc ...))])
-                 (or
-                  (type-annotation f #:infer #t)
-                  (generalize (tc-expr/t ac))))]
+                 (let ([type (type-annotation f #:infer #t)])
+                   (if type
+                       (tc-expr/check/t ac (ret type))
+                       (generalize (tc-expr/t ac)))))]
            [acc-ty (or
                     (type-annotation #'val #:infer #t)
                     (match expected