New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Previously-working code gets a subtype error with 4.07 #7824
Comments
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
end 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: @trefis It seems that on trunk the code from talex compiles fine but the one from yallop is still broken. I'll look into it. |
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:
|
Comment author: @trefis The fix was merged in trunk and cherry-picked on the 4.07 branch. |
Original bug ID: 7824
Reporter: talex
Assigned to: @trefis
Status: resolved (set by @trefis on 2018-07-19T17:03:46Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.07.0
Fixed in version: 4.07.1+dev/rc1
Category: typing
Monitored by: @nojb
Bug description
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
module Element : sig
type +'a t
val from_a : [
A] t -> unit val from_ab : [<
A | `B] t -> unitend = struct
type 'a t = 'a
let from_a x = assert false
let from_ab x = assert false
end
let f x =
Element.from_a x;
Element.from_ab x;
match [] with
| :: -> (x :> [
A |
C] Element.t)opam@2688edb5639b:~/opam-repository$ ocaml test.ml
File "./test.ml", line 17, characters 12-38:
Error: Type [
A ] Element.t is not a subtype of [
A |C ] Element.t The first variant type does not allow tag(s)
CAdditional information
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.
The text was updated successfully, but these errors were encountered: