Confusing error message with GADTs and polymorphic recursion

[DemiMarie]

The following OCaml program results in a very confusing error:

type ('a, 'b) bogus =
  | Fixed : ('a, 'b) bogus -> (int -> 'a, 'b) bogus
  | String : ('a, 'b) bogus -> (string -> 'a, 'b) bogus
  | Done : ('a, 'a) bogus

let rec apply = fun checker callback -> 
  match checker with
  | Fixed rest -> apply rest (callback 0)
  | String rest -> apply rest (callback "")
  | Done -> callback

OCaml 5.2 reports:

This expression has type 'a but an expression was expected of type int -> 'a
The type variable 'b occurs inside int -> 'b

which suggests enabling -rectypes, but that doesn’t help.

The correct solution is to add a type annotation:

type ('a, 'b) bogus =
  | Fixed : ('a, 'b) bogus -> (int -> 'a, 'b) bogus
  | String : ('a, 'b) bogus -> (string -> 'a, 'b) bogus
  | Done : ('a, 'a) bogus

let rec apply : type a b. (a, b) bogus -> a -> b = fun checker callback -> 
  match checker with
  | Fixed rest -> apply rest (callback 0)
  | String rest -> apply rest (callback "")
  | Done -> callback

but the error does not provide any indication of this.

I understand that type inference for polymorphic recursion is undecideable, but a suggestion to use the explict polymorphism syntax would have been very helpful.

[gasche]

It's not easy to tell which errors come from a lack of annotation and which are completely unrelated. The best I can think of is to locate whether the error is at an application site for a recursive name and we are in the definition scope for this name. But this would be fairly fragile as many related errors are caught at a different location than an application site.

In fact if I try your repro case with OCaml 5.2.0, I get a different error from the one you suggest:

File "test.ml", line 9, characters 4-15:
9 |   | String rest -> apply rest (callback "")
        ^^^^^^^^^^^
Error: This pattern matches values of type (string -> 'a, 'b) bogus
       but a pattern was expected which matches values of type
         (int -> 'c, 'd) bogus
       Type string is not compatible with type int

(An error similar to the one you suggest is produced by Merlin, but not by the type-checker itself.)

The heuristic I tried to think of above does not work for that other error. In fact for that error it may be relatively easier to think of an appropriate hint: if the error is when unifying the types of patterns, and they are incompatible instances of the same GADT type, we should probably suggest having a type annotations with locally abstract types.

[DemiMarie]

It's not easy to tell which errors come from a lack of annotation and which are completely unrelated. The best I can think of is to locate whether the error is at an application site for a recursive name and we are in the definition scope for this name. But this would be fairly fragile as many related errors are caught at a different location than an application site.

In fact if I try your repro case with OCaml 5.2.0, I get a different error from the one you suggest:

File "test.ml", line 9, characters 4-15:
9 |   | String rest -> apply rest (callback "")
        ^^^^^^^^^^^
Error: This pattern matches values of type (string -> 'a, 'b) bogus
       but a pattern was expected which matches values of type
         (int -> 'c, 'd) bogus
       Type string is not compatible with type int

(An error similar to the one you suggest is produced by Merlin, but not by the type-checker itself.)

That explains the mismatch: I was using Merlin and assumed that Merlin just used the type-checker directly, so I didn’t think to use ocamlc. Is this a Merlin bug?

The heuristic I tried to think of above does not work for that other error. In fact for that error it may be relatively easier to think of an appropriate hint: if the error is when unifying the types of patterns, and they are incompatible instances of the same GADT type, we should probably suggest having a type annotations with locally abstract types.

:+1:

[gasche]

That explains the mismatch: I was using Merlin and assumed that Merlin just used the type-checker directly, so I didn’t think to use ocamlc. Is this a Merlin bug?

It's hard to tell. Merlin makes small changes to the type-checker logic to better deal with partial/incomplete files, and sometimes this changes the type-checking behavior a bit. It can be locally worse (sometimes better), but the gains we get from handle partial buffers gracefully are often worth it. I am not familiar enough with the Merlin type-checker to tell if this one can be fixed easily or is a fundamental consequence of Merlin's type error recovery.

[gasche]

I don't have the bandwith to work on this, and no one has volunteered to work on it. (Maybe @Octachron should have a second look just in case.) I propose to close as "won't fix" for now, but we can reopen if there is motivation.