Skip to content
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

Closed
vicuna opened this issue Jul 17, 2018 · 6 comments
Closed

Previously-working code gets a subtype error with 4.07 #7824

vicuna opened this issue Jul 17, 2018 · 6 comments
Assignees

Comments

@vicuna
Copy link

vicuna commented Jul 17, 2018

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 -> unit
end = 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) C

Additional 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.

@vicuna
Copy link
Author

vicuna commented Jul 17, 2018

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
type +'a t

 val from_a : [`A] t -> unit
 val from_ab : [< `A | `B] t -> unit

end = struct
type 'a t = 'a

 let from_a x = assert false
 let from_ab x = assert false

end

type _ t = T : 'a -> 'a t

let f x =
Element.from_a x;
Element.from_ab x;
match T () with
| T _ -> (x :> [A | C] Element.t)

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
File "/tmp/test.ml", line 19, characters 14-40:
Error: Type [ A ] Element.t is not a subtype of [ A | C ] Element.t The first variant type does not allow tag(s) C

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
#1648

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
that aren't required if there are none.
However, because of disambiguation, we can't know for sure whether the
patterns contain some GADT constructors. So we conservatively assume that
any constructor might be a GADT constructor. *)

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.

@vicuna
Copy link
Author

vicuna commented Jul 18, 2018

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.

@vicuna
Copy link
Author

vicuna commented Jul 18, 2018

Comment author: @trefis

Apparently it's #1735 that "fixed" the simple case (leaving the GADT one broken).

@vicuna
Copy link
Author

vicuna commented Jul 18, 2018

Comment author: @lpw25

I had a look at this with trefis. This seems to be a bug in Ctype.subtype where it doesn't ignore absent variant constructors. You can get it to trigger without any GADTs:

# module Element : sig
     type +'a t

     val to_a : unit -> [`A] t
     val to_ab : unit -> [< `A | `B] t
  end = struct
     type +'a t

     let to_a x = assert false
     let to_ab x = assert false
   end;;
 module Element :
  sig
    type +'a t
    val to_a : unit -> [ `A ] t
    val to_ab : unit -> [< `A | `B ] t
  end

# let f () =
    let open Element in
    let x = if true then to_ab () else to_a () in
    (x :> [ `A | `C ] Element.t);;
Characters 89-117:
      (x :> [ `A | `C ] Element.t);;
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Type [ `A ] Element.t is not a subtype of [ `A | `C ] Element.t
       The first variant type does not allow tag(s) `C

which also causes a break in principality:

# let f () =
    let open Element in
    let x = if true then to_a () else to_ab () in
    (x :> [ `A | `C ] Element.t);;
val f : unit -> [ `A | `C ] Element.t = <fun>

@vicuna
Copy link
Author

vicuna commented Jul 18, 2018

Comment author: @trefis

Proposed fix: #1914

@vicuna
Copy link
Author

vicuna commented Jul 19, 2018

Comment author: @trefis

The fix was merged in trunk and cherry-picked on the 4.07 branch.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants