Typechecker doesn't catch mismatch between type abstractions and foralls

[jstolarek]

During work on #693 I modified the compiler such that compiling fun (x) {1} produced:

let it : forall a,b::Row. a -b-> Int = /\a,b::Row. {
    let fun g1 (x : a) : forall c,d::Row. c -d-> Int = /\ a,b::Row. 1
    in ~g1
  }
in ~it

(this can be easily obtained by modifications in desugarFuns.desugarFunLit) Notice that the body of it has two big lambdas, effectively giving it a type forall a,b::Row,c,d::Row. a -b-> Int, but the signature for it is forall a,b::Row. a -b-> Int. The typechecker (enabled via recheck_frontend_transformations=true) does not catch this as an error.

[jstolarek]

Design question: do we actually require that each big lambda gives rise to a forall variable? If that would be the case then the implication is we also permit unused forall variables.

[jamescheney]

I think this is because after the first typechecking pass, functions are frozen (fun_frozen is set) and because of this, the following line https://github.com/links-lang/links/blob/0e3a7e51bc6237e34b98acc661bbfd11064200bd/core/typeSugar.ml#L4292

results in the quantifiers of the annotated type (obtained from the initial type inference or annotation) being blindly trusted (the later checks are guaranteed to succeed because we are checking that the type annotation matches itself, not the generalized, inferred type). In particular, if the type contains quantifiers obtained as a result of typechecking expressions containing TAbstr then I see no place where we check that the quantifiers obtained by typechecking the "body" of the function matches the annotation.

Simply disabling the alternative behavior when fun_frozen is set may fix the issue, at the cost that we may wind up re-inferring the type (but we currently seem to be doing most of the work of that anyway). However, that seems to be the only place where the fun_frozen flag is ever actually used (as opposed to set or passed-through.) It is also set by the parser when a ~fun is encountered, so perhaps the behavior controlled by the flag is the right thing to do during type inference but not during subsequent typechecking.

A better solution, I think already suggested elsewhere, may be to have a separate typechecker that handles all revalidation and does not attempt to do any inference/unification. This would hopefully also enable simplifying the type inference code somewhat since we would not have to worry about revalidation situations (though a lot of the same issues come up when typechecking code that has explicit type annotations.)