Actually typecheck actuals even when there's a type annotation.

collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt

@@ -808,7 +808,10 @@
                 (vector-ref #("a" "b") (- x 1)))
               -String]
         [tc-err (string-append "bar" (if (zero? (ann 0.0 Float)) #f "foo"))]
-        )
+        [tc-err (do: : Void
+                     ([j : Natural (+ i 'a) (+ j i)])
+                     ((>= j 10))
+                     #f)])
   (test-suite
    "check-type tests"
    (test-exn "Fails correctly" exn:fail:syntax? (lambda () (parameterize ([orig-module-stx #'here])

collects/typed-scheme/typecheck/tc-app.rkt

@@ -238,9 +238,10 @@
     [_     
      (let ([ts (for/list ([ac (syntax->list actuals)]
                           [f (syntax->list args)])
-                 (or 
-                  (type-annotation f #:infer #t)
-                  (generalize (tc-expr/t ac))))])
+                 (let ([infer-t (type-annotation f #:infer #t)])
+                   (if infer-t
+                       (check-below (tc-expr/t ac) infer-t)
+                       (generalize (tc-expr/t ac)))))])
        (tc/rec-lambda/check form args body lp ts expected)
        expected)]))