Join GitHub today
GitHub is home to over 31 million developers working together to host and review code, manage projects, and build software together.Sign up
Previously-working code gets a subtype error with 4.07 #7824
Original bug ID: 7824
I'm trying to find out why 0install doesn't compile on OCaml 4.07. I now have a fairly small test case which works on 4.06 and seems very suspicious.
Steps to reproduce
$ docker run --rm -it ocaml/opam2:4.07
opam@2688edb5639b:~/opam-repository$ cat > test.ml
val from_a : [
let from_a x = assert false
let f x =
opam@2688edb5639b:~/opam-repository$ ocaml test.ml
This happens on my dev machine with 4.07, as well as with the Docker image.
Making seemingly-unrelated changes (e.g. changing the :: pattern to _) allows it to be type checked successfully. Asking merlin for the type of [x] and then adding that, as [let f (x:[ `A ] Element.t) = ...], also allows it to pass.
Comment author: @yallop
This looks like an old bug that is newly triggered by the fact that improved support for constructor disambiguation takes a different path through the type checker.
Here's a very similar program that is also rejected by earlier versions of OCaml, unless -principal is specified:
module Element : sig
end = struct
type _ t = T : 'a -> 'a t
let f x =
Note the difference with the code in the original report: the pattern match at the end involves a GADT-style definition.
OCaml 4.02.3 rejects the above program as follows:
$ ocaml /tmp/test.ml
However, with -principal, the program is accepted by OCaml 4.02.3:
$ ocaml -principal /tmp/test.ml
I think (but haven't confirmed for sure) that since the following pull request:
Allow type-based selection of GADTs constructors
the GADT code is triggered even for ordinary constructors. The pull request notes:
(* There are various things that we need to do in presence of GADT constructors
So it looks like there's a longstanding bug in the GADT path (since code accepted with -principal should usually also be accepted without -principal), and in 4.07.0 the GADT path is now taken more frequently, causing new failures in existing code.
Comment author: @lpw25
I had a look at this with trefis. This seems to be a bug in
which also causes a break in principality: