Give hints about existential types appearing in error messages

[lpw25]

This PR changes the names of existential types from things like $Foo_'a to just $a and instead adds an explicit hint describing where $a came from. For instance, this message from the testsuite:

 Line 2, characters 6-7:
 2 |   | A x
           ^
Error: This pattern matches values of type "$A_'a"
       The type constructor "$A_'a" would escape its scope

becomes:

 Line 2, characters 6-7:
 2 |   | A x
           ^
Error: This pattern matches values of type "$a"
       The type constructor "$a" would escape its scope
       Hint: "$a" is an existential type bound by the constructor "A".

It does this by broadening the abstract_reason type to a type_origin type that describes where a type has come from, and uses that to annotate existential types in the environment with the constructor they have come from.

The printing is done in the same way as the existing hints about conflicting names. Personally, I think these don't have the best indentation -- it would be better if the hint was unindented -- but I can't see an obvious way to achieve that and it's as much a problem with the conflict hints as with the new ones.

[nojb]

Naïve question: do we need to introduce another kind of type variable, $a? Why not use 'a?

[gasche]

(Only very superficial review comments for now.)

[lpw25]

Naïve question: do we need to introduce another kind of type variable, $a? Why not use 'a?

The $a aren't a new kind of variable, they are just abstract types with generated names. Printing them as unification variables would be confusing because it would cause the compiler to say things like "'a cannot be unified with int" to the user.

Also worth pointing out that this PR isn't adding these generated abstract types with $ in the name, it is just adjusting their names.

[gasche]

I like the feature, and the code is pleasantly not-too-invasive. If we had a type-checker expert at hand they should review the design, but if they are busy I would feel confident approving after a review for code quality -- I have done a pass already and don't expect that there is much more for me to discuss.

[Octachron]

I tend to agree that this change overall reduces noise:

On the one hand, we lose some information locality because the name $a no longer carries the constructor name.
On the other hand, with meaningful constructor argument names or locally named existentials, the constructor names don't add much more information , but they add a lot of redundancy.
Keeping the origin of the existentials in a shared hint sounds like a good compromise.
The fact that the hint explains what the strange $a means is also an improvement.

I am wondering if later we could show the constructor definition in the hint to gives an even more useful context.
But that would require hints to be a distinct part of the error report rather than ad-hoc part of the error message, which could be a way to solve the indentation issue (but that should be a matter for another PR).

A small remark, the manual description of the existential nomenclature should be updated. In particular, we are left with only three categories now that we always name anonymous constructor argument types.

[lpw25]

Comments addressed and Changes entry added

[gasche]

I find the revised implementation (and documentation) satisfactory. Approved.

I would think of "squashing" the commits together as they are not split in independent changes currently.

[garrigue]

A tiny amount of information is lost here: originally the names combined the constructor name, and the name of the existential variable inside the definition. Here the hint only gives the constructor name.
Of course this only matters if the same constructor introduces several existentials.
It should be possible to add the name of the variable to type_origin, and include it in the hint. Or would it be confusing ?

[lpw25]

We could add it to give an error like:

Hint: "$a" is an existential type "'a" bound by the constructor "A".

normally it would be pretty redundant, but I guess in some cases it would be more like:

Hint: "$a3" is an existential type "'a" bound by the constructor "A".

where the two names aren't quite identical, and so perhaps useful.

[gasche]

How easy would it be to always reuse the variable name as prefix, with the counter as suffix?

[Octachron]

That's already what happens: we use the variable name in the constructor definition if it exists when we choose the existential variable name at instantiation, and the type printer only adds a numerical suffix in case of collisions:

type any = Any: 'any * 'more -> any
type other = Other: 'any * 'more -> other
type variant = Variant: 'any * 'more -> variant
let f (Any(x,y)) (Other(a,_)) (Variant(r,_)) = (x,y) = (r,a)

Error: This expression has type $any2 but an expression was expected of type
$any
Hint: $any is an existential type bound by the constructor Any.
Hint: $any2 is an existential type bound by the constructor Variant.

[gasche]

Ah, so I don't think that any change is necessary?

[garrigue]

I see, since all the variables were named $a I thought that the name was forgotten.
I still think that the connection would be clearer if the existential was named $'a rather than $a.