Type check with expected type when checking recursive loops.

Closes PR12678.

original commit: 3c02bb1abbe0d8965c2cd70649ebb1357499a3ee

collects/tests/typed-racket/succeed/pr12678.rkt

@@ -0,0 +1,9 @@
+#lang typed/racket
+
+(define: memo : (HashTable Natural String)  (make-immutable-hash empty))
+(define strs '("Hello" "Goodbye"))
+
+(for/fold: : (HashTable Natural String)
+    ([memo : (HashTable Natural String)  (make-immutable-hash empty)])
+    ([i : Natural  (in-naturals)] [str : String  (in-list strs)])
+  (hash-set memo i str))

collects/typed-racket/typecheck/tc-app/tc-app-lambda.rkt

@@ -6,7 +6,7 @@
          syntax/parse racket/match racket/list
          syntax/parse/experimental/reflect
          unstable/sequence
-         (typecheck signatures tc-funapp check-below find-annotation )
+         (typecheck signatures tc-funapp find-annotation)
          (types abbrev utils generalize type-table)
          (private type-annotation)
          (rep type-rep)
@@ -98,7 +98,7 @@
                  (let* ([infer-t (or (type-annotation f #:infer #t)
                                      (find-annotation #'(begin . body*) f))])
                    (if infer-t
-                       (check-below (tc-expr/t ac) infer-t)
+                       (tc-expr/check/t ac (ret infer-t))
                        (generalize (tc-expr/t ac)))))])
        (add-typeof-expr lam (tc/rec-lambda/check form args body lp ts expected))
        expected)]))