Ensure that ascriptions in function types don't cause errors
Ensure that ascriptions in function types don't cause errors

The errors were of the form "Impossible! let-bound lambda … = … has a type
that's not a function".

For example, this now works::

   let rec n_args_fn_type (n: int{n > 0}) (dom codom: Type) =
     if n = 1 then dom -> codom
     else dom -> n_args_fn_type (n - 1) dom codom

   let f : normalize (n_args_fn_type 3 int unit) = (fun (x y z: int) -> ())

A-Manning/FStar,FStarLang/FStar,A-Manning/FStar,A-Manning/FStar,FStarLang/FStar,FStarLang/FStar