Improve type instantiation

[yannham]

Is your feature request related to a problem? Please describe. Currently, polymorphic types are instantiated as in a standard Hindley-Milner system, that is as soon as a variable is used. While this is customary in the Hindley-Milner type system, it's limiting in a type system with full polymorphism (à la System F) like Nickel, as it results in polymorphic types being instantiated without necessity, and thus overspecialized:

nickel> let f : (forall b. b -> b) -> Num = fun f => f 0 in
let id : forall a. a -> a = fun x => x in
f id : Num

error: Incompatible types
  ┌─ repl-input-8:3:3
  │
3 │ f id : Num
  │   ^^ this expression
  │
  = The type of the expression was expected to be `forall b. b -> b`
  = The type of the expression was inferred to be `_a -> _a`
  = These types are not compatible

In this example, the type of id is unnecessarily instantiated to a monomorphic type _a -> _a, causing the application to fail, while this example is expected to typecheck.

Describe the solution you'd like Polymorphic types should be instantiated as late as possible, at function application, or even when trying to do types unification.

Describe alternatives you've considered

• Keep the current status-quo. This means accepting that some simple terms that typecheck in System F won't typecheck in Nickel, for no deep reason.
• Introduce a syntax for explicit type application, as in Haskell. However the cost is high for limited benefits:
  1. Yet a new syntactic construct users must know about, for something that will be fairly rare (polymorphic types of rank > 1)
  2. Users have to think about type instantiation, which requires non trivial notions in type systems, that Nickel users may not know nor care about. It seems better to try to do the natural thing silently without having the user to think about it too much.

[yannham]

Revisiting this issue later, actually I think the issue and the fix, while related to instantiation, don't need to change when the instantiation is done. Rather, it seems that the current algorithm doesn't perform correctly the (shallow) skolemization of a polymorphic type when checking against one.

In practical terms, when typechecking an expression exp against forall a1 a2 ... an. t where t is not a forall, the typechecker doesn't always instantiate a1 a2 ... an with constants. It does it only when the check is induced by an annotation like let exp : forall a b. a -> b -> b = ..., but not when the check is induced by checking the argument of a call, as in the example above, without apparent reason.

[aspiwack]

When you typecheck expressions like these, you need to take care of your variables' levels. That is, in this case, you are typechecking id with forall b. b -> b, it means that you introduce a rigid variable b and typecheck id at type b -> b. Then id has type _a -> _a because of the variable rule. But _a can unify with b because b existed when _a was created. (it's “for all b, there exists _a, such that…”, rather than “there exists _a, such that for all b, …).

This is yet another thing where bidirectional type-checking helps see things more clearly.

[yannham]

But _a _can unify with b

Just to be sure, did you mean can, or cannot ?

[aspiwack]

I did mean “can”.

[yannham]

Right. And if we remove the polymorphic annotation from id, then we are in the dual case (id is given the type _a -> _a at its definition), and we should forbid unification of _a to b, should we?

[aspiwack]

I don't think that I understand what you mean here. Sorry.

[yannham]

I just want to confirm that I rightly understand what your remark is about. I'm considering a variation of the original example with the annotation on id removed:

let f : (forall b. b -> b) -> Num = fun f => f 0 in
let id = fun x => x in
f id : Num

In this case, because of variable levels, we should reject this program, as now the _a is introduced at the definition of id, and is anterior to the skolem variable b, and thus _a cannot unify with b this time. Is it exact?

[aspiwack]

It is most definitely correct. (unless we are doing some sort of let-generalisation, but we decided not to go that way)

---

There are two typical ways to handle this sort of situations in unifiers that I'm aware of:

• Each unification variable _a keeps track of all the rigid variables that exist when _a is created. Then, the solution for _a mustn't use rigid variables from outside the list. This solution is used by Coq. It's useful to type the substitution of a variable in isolation, as you can keep the type of your unification variables as well. It's great for interactive unification
• Each unification and rigid variable keeps track of an integer (the level), the level is incremented whenever a (set of) rigid variable is introduced, and unification variable can only be substituted with variables of lower (or equal) levels. This is the solution used by GHC. It's faster and consumes less memory, so probably preferable in automated unifiers. Unless there is a reason that would make it insufficient, I suppose, but I can't think of one out of the top of my head.

[yannham]

Closed by #1473.