improve "Their kinds differ" error message

[ygrek]

$ ocaml -stdin <<EOF
type x=T
type a=x=T
type y=x
type b=y=T
EOF
File "(stdin)", line 4, characters 0-10:
4 | type b=y=T
    ^^^^^^^^^^
Error: This variant or record definition does not match that of type y
       Their kinds differ.

I guess there is a reason why compiler wouldn't follow the type abbreviation but error message is confusing for the beginners, i think it can be improved by explaining a little more (what is that "kind") - e.g. "Their kinds differ - this type b is a re-exported variant (equation and representation) while type y is an abbreviation (equation without representation)."

[smuenzel]

I think this is better in trunk?

File "/tmp/a.ml", line 4, characters 0-10:
4 | type b=y=T
    ^^^^^^^^^^
Error: This variant or record definition does not match that of type y
       The original is abstract, but this is a variant.

[Octachron]

Since 5.1 rather than trunk.

[gasche]

But I do agree with @ygrek that it is strange that this program is rejected. Is there a good reason or should we just do more work in typedecl? ( Maybe @garrigue would know? )

[garrigue]

I do not know about whether there is a "good" reason. I suppose this coincides with the theory @xavierleroy implemented.
Morally, the idea is that a concrete type definition does two things: it defines a type, and it defines accessors.
An abbreviation only defines a type.
And you can only export accessors which are already in the definition.
This said, type-based disambiguation has considerably blurred the line, and it would be relatively easy to look up the original definition (including accessors) from the abbreviation.
Note also that there are other restrictions about exporting: the type parameters (and their constraints) should be identical for instance. Relaxing that one would be more complicated (and possibly dangerous).

[Octachron]

This issue was discussed at a core developer meeting and the point of view was that we should focus on improving the error message, possibly by doing the path compression on the typechecker side and proposing it as a hint, something like:

4 | type b=y=T
   ^^^^^^^^^^
Error: The type y is an abbreviation for a and not a direct definition. 
Hint: Did you mean "type b = a = T"?

[gasche]

The issue was discussed again at the type-system meeting, where it looks like a different consensus is emerging that it would be fine to support this example instead of finding a clear way to explain why we reject it. I like this new consensus better!

[github-actions]

This issue has been open one year with no activity and without being identified as a bug. Consequently, it is being marked with the "stale" label to see if anyone has comments that provide new information on the issue. Is the issue still reproducible? Did it appear in other contexts? How critical is it? Did you miss this feature in a new setting? etc. Note that the issue will not be closed in the absence of new activity: the "stale" label is only used for triaging reason.

[smuenzel]

I think allowing this alias is pretty simple. But it seems to uncover other cases where we treat aliases differently than the type definition (for example when extending extensible variants)