Proper type instantiation discipline

[yannham]

Closes #584 #360 #1027

This PR is the last missing piece toward a reasonable bidirectional typechecking algorithm that properly handles higher-rank polymorphic types.

Until now, instantiation of polymorphic types has been sometimes ad-hoc and bizarrely limited. Simple programs such as:

let r : { id : forall a. a -> a } = { id = fun r => r } in
r.id "x"

or

let eval : forall a. (forall b. b -> b) -> a -> a = fun f x => f x in
(eval (fun x => x) 1) : Number

wouldn't typecheck (cf related issues at the top). Variable levels introduced in #1372 were an important preliminary step before we could attack this issue.

This PR is building on #1372 to use a proper instantiation discipline, derived from Complete and Easy Bidirectional Typechecking for Higher-Rank
Polymorphism (ideally from the specification of the type system in this repository, but it's unfortunately not complete enough yet to be used as a reliable source of truth).

This commit gets rid of the ad-hoc cases of instantiation for Op1 applications, the variable rule and others: those are now all subsumed by the subsumption rule, because they are special cases of a switch from inference mode to checking mode. Now, check and subsumption are the only place where the checked type might be instantiated with rigid type variable (I suspect we might even get rid of the instantiation of the checked type in subsumption, because it's always done by check before anyway, but this has to be verified first), and subsumption is the only rule to instantiate an inferred type with fresh unification variables.

The result is that the previously mentioned cases, plus other examples of higher-rank polymoprhic functions are now typechecking just fine.

Funnily, one test in typecheck/fail was actually well-typed, but didn't typecheck because of the described previous limitations. It's just been transformed to a passing test.

TODO

• actually enforce that the instantiation is predicative (mark unification variables coming from the instantiation of a polytype and avoid unifying them with non instantiated polytypes). Currently we do naive impredicative instantiation, but it's just because I didn't want to load this PR too much: it's going to be predicative before the next release. Not that the current version isn't unsound, but doing naive impredicative instantiation makes typechecking sensitive to arguments order for such impredicative cases.

[vkleen]

This looks reasonable, with the caveat that I'm not an expert in the current Nickel typechecker 😅

[vkleen]

Is this a change in behaviour or was this just implicit in the previous typechecking code?

[yannham]

This is a change in behavior, but I think the previous behavior was accidental, and neither officially supported nor documented. The previous behavior was indeed to let the type of fields without values be unconstrained.