Incorrect error message on external arity mismatch with local substitution

[craigfe]

I ran into the following example today:

module Identity : sig
  type 'a t = 'a
  type ('a, 'b) arrow := 'a -> 'b
  external map : ('a -> 'b) -> ('a t, 'b t) arrow = "%identity"
end = struct
  type 'a t = 'a
  external map : ('a -> 'b) -> 'a t -> 'b t = "%identity"
end

This is rightly rejected because the two externals have differing arities. (It also happens that the implementation expects the wrong arity of %identity, but this won't be determined until after type checking.)

However, the reason that OCaml gives for rejecting it is not correct:

Lines 5-8, characters 6-3:
Error: Signature mismatch:
       ...
       Values do not match:
         external map : ('a -> 'b) -> 'a -> 'b = "%identity"
       is not included in
         external map : ('a -> 'b) -> 'a -> 'b = "%identity"

The compiler is making a distinction between two different classes of arrows that isn't conveyed to the user. It seems better for the compiler to state that the arities of the two types differ, and perhaps even refer to the corresponding section of the manual since this notion of arity can be surprising for users (e.g. here).

[lpw25]

I think this is fixed by #10407

[antalsz]

Yes – the new error will be

Error: Signature mismatch:
       ...
       Values do not match:
         external map : ('a -> 'b) -> 'a t -> 'b t = "%identity"
       is not included in
         external map : ('a -> 'b) -> 'a t -> 'b t = "%identity"
       The syntactic arities of these primitives were not the same
       (They must have the same number of arrows present in the source)

There is now extra explanatory text that points to the syntactic restriction that's present. However, because of the destructive substitution, the reported types are still unclear.

[github-actions]

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.