Specialized error message for syntactic function arity type clash

[ncik-roberts]

This continues a discussion with @Octachron from #12236. The topic is what error message to generate in a case of typing backward-incompatibility. Here's an example of such a case:

type (_, _) eq = Eq : ('a, 'a) eq
let f : type a. (a, int -> int) eq -> a =
  fun Eq x -> x 

As of #12236, the error message is a generic-looking unification error:

Error: This expression has type "(a, int -> int) eq -> 'a -> 'b"
       but an expression was expected of type "(a, int -> int) eq -> a"
       Type "'a -> 'b" is not compatible with type "a"

We thought we should do better to explain the problem, especially given that the change to typing is backward-incompatible. I'm making this PR to summarize the ideas so far, suggest a wording, and solicit further refinements/ideas.

---

(A) First try from original PR that we decided against:

3 |   fun Eq x -> x
      ^^^^^^^^^^^^^
Error: The type of a function with 2 arguments must have at least 2 arrows.
       This expression has type "(a, int -> int) eq -> 'a -> 'b"
       but an expression was expected of type "(a, int -> int) eq -> a"
       Type "'a -> 'b" is not compatible with type "a"

Some remarks that @Octachron made:

• The criteria is not actually syntactic on types, despite the error message's claim to the contrary, since having a type (int -> int -> int as 'a) ->'a is fine.
• The type (a, int -> int) eq -> 'a -> 'b is potentially confusing to include in the output. It doesn't match any type written by the user, so they may struggle to connect it to the main point of the error message.

(B) @Octachron 's suggestion that focuses on syntactic arity:

3 |   fun Eq x -> x
      ^^^^^^^^^^^^^
Error: The syntactic arity of the function doesn't match the type constraint:
       syntactic function arity and function type arity must agree without relying
       on local type equations.
       This function has two syntactic arguments, but its type is constrained to 
       "(a,int->int) eq -> a".

(C) Current draft:

3 |   fun Eq x -> x
      ^^^^^^^^^^^^^
Error: The syntactic arity of the function doesn't match the type constraint:
       Syntactic function arity must agree with (i.e., must be less than or
       equal to) function type arity without using local type equations.
       This function has 2 syntactic arguments, but its type is constrained
         to "(a, int -> int) eq -> a".
       Hint: consider splitting up the function's syntactic arity by
       inserting "-> fun" after the argument that introduces the local
       type equation.

This latest version:

• clarifies what it means for syntactic function arity to "agree" with the function type arity. (It's not just that they are equal, as the function type can have more arrows than the function has syntactic arguments without any issue.)
• attempts to suggest a fix.

This fix is meant to guide the user to this program, which type-checks:

type (_, _) eq = Eq : ('a, 'a) eq
let f : type a. (a, int -> int) eq -> a =
  fun Eq -> fun x -> x 

Here are a few areas of discussion that immediately come to mind:

• In the hint, we could generate a list of candidate parameters with GADT patterns, as these are the only ones that could have introduced local type equations.
• It doesn’t seem great to say “insert -> fun” as the grammatical object is a snippet of text, not a sensible AST. But maybe it is still a good way to guide the user to a type-checking program.

[gasche]

Your proposal:

Error: The syntactic arity of the function doesn't match the type constraint:
       Syntactic function arity must agree with (i.e., must be less than or
       equal to) function type arity without using local type equations.
       This function has 2 syntactic arguments, but its type is constrained
         to "(a, int -> int) eq -> a".
       Hint: consider splitting up the function's syntactic arity by
       inserting "-> fun" after the argument that introduces the local
       type equation.

I find the "must agree with" sentence too general/formal. I prefer the same message without it:

Error: The syntactic arity of the function doesn't match the type constraint:
       This function has 2 syntactic arguments, but its type is constrained
         to "(a, int -> int) eq -> a".
       Hint: consider splitting up the function's syntactic arity by
       inserting "-> fun" after the argument that introduces the local
       type equation.

[Octachron]

If we want to have a hint which is grammatically valid, I propose to add ellipses:

Hint: consider splitting up the function definition into "fun ... gadt_pat -> fun ... "
where "gadt_pat" is the GADT constructor pattern that introduces the local type equation on "a". 

which from my point view has the advantage of making obvious what we mean by "splitting up the function".

I think it would helpful for users on their first reading of the error message to mention the local type abstract blocking the arity in the external view. If I am not mistaken, we can extract this local abstract type by looking up at the last Diff of the error trace.

Listing the GADT constructor pattern could be helpful but I believe that we are hitting diminishing return at this point.

[ncik-roberts]

I like both of those suggestions, and I find the reworded hint helpful. In full, with minor tweaks to wording, that would be:

3 |   fun Eq x -> x
      ^^^^^^^^^^^^^
Error: The syntactic arity of the function doesn't match the type constraint:
       This function has 2 syntactic arguments, but its type is constrained
         to "(a, int -> int) eq -> a".
       Hint: consider splitting the function definition into "fun ... gadt_pat -> fun ..."
       where "gadt_pat" is the pattern with the GADT constructor that introduces the
       local type equation on "a".

I will look into extracting the locally abstract type's name, as I agree that it helps clarify the message.

[ncik-roberts]

(Is a Changes entry needed? My feeling was no, but I will defer to others.)

[gasche]

You could add the PR number to the #12236 changes entry.

[ncik-roberts]

Good idea, thanks. And done.

[gasche]

I think that the testsuite output is not up-to-date with the error message.

[ncik-roberts]

Yes, sorry about that. I pushed a fix just as you left this comment.