Menhir's type inference is unsound in the presence of open polymorphic variants
This problem was reported by Joe, who created a minimal reproducible test case.
This is interesting indeed. It boils down to the fact that there are two ways
in OCaml of checking whether an expression e
has type t
. One can either
write
let x : t = e
and check whether this is accepted, or write
module M : sig val x : t end = struct let x = e end
It may seem naively as though the two ways are equivalent, but it turns out
that in the presence of certain types such as the polymorphic variant type
[>`Hello]
, they are not. For example, the following definition is accepted:
let f : unit -> [> `Hello ] =
fun () -> `Haha
but this one is rejected:
module P : sig
val f : unit -> [> `Hello ]
end = struct
let f : unit -> [> `Hello ] =
fun () -> `Haha
end
The problem is that Menhir uses the first way of checking whether e
has type
t
, which is simpler but unsound.
I was not aware of this problem!
It looks as though the correct fix would be to change Menhir to use the second
way of checking whether e
has type t
, but I am afraid that this might
require changing the protocol through which Menhir interacts with the OCaml
type-checker; we might have to call the type-checker once to infer a type and
once to check that this inferred type is correct.
A cruder fix would be to disallow the (declared or inferred) type of a symbol
to mention an open polymorphic variant type of the form [> `Hello]
or [< `Hello]
. It seems necessary to apply this rule to every symbol,
not just start symbols.