Lazy evaluation prevents typechecking

[vincent-163]

The expression (a:(.* *) (:(.* a) a)) can be normalized and typed without errors. The type is inferred as (a.(.* *) (.(.* a) (.* *))). However, when inferring the type of that type, the script gives an error (correctly).

I think the issue is that the type of the body of Forall must be type "*", so in :(.* a), a is not a valid body for forall. However, this is not checked due to HOAS semantics, and it proceeds to infer the wrong type without noticing the error.

Since most of the value of CoC lies in robust typechecking, it might be a good idea to either use an implementation that checks types rigorously or make it explicit that not all invalid expressions fail typechecking.