Use checking mode for let bindings with annotations.

If there's an annotation on a let binding, we should enter checking mode
to propagate more information. Also, generate constraints for the return
type of parametrized functions when in checking mode.
Fleshing out methods for t-app