Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007824OCamltypingpublic2018-07-17 21:542018-07-19 19:03
Reportertalex 
Assigned Totrefis 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version4.07.0 
Target VersionFixed in Version4.07.1+dev 
Summary0007824: Previously-working code gets a subtype error with 4.07
DescriptionI'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 InformationThis 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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0019252)
yallop (developer)
2018-07-18 00:00

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
   https://github.com/ocaml/ocaml/pull/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.
(0019253)
trefis (manager)
2018-07-18 11:55

It seems that on trunk the code from talex compiles fine but the one from yallop is still broken.

I'll look into it.
(0019254)
trefis (manager)
2018-07-18 12:26

Apparently it's https://github.com/ocaml/ocaml/pull/1735 [^] that "fixed" the simple case (leaving the GADT one broken).
(0019255)
lpw25 (developer)
2018-07-18 13:36

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>
(0019256)
trefis (manager)
2018-07-18 13:58

Proposed fix: https://github.com/ocaml/ocaml/pull/1914 [^]
(0019262)
trefis (manager)
2018-07-19 19:03

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

- Issue History
Date Modified Username Field Change
2018-07-17 21:54 talex New Issue
2018-07-18 00:00 yallop Note Added: 0019252
2018-07-18 11:55 trefis Note Added: 0019253
2018-07-18 12:26 trefis Note Added: 0019254
2018-07-18 13:36 lpw25 Note Added: 0019255
2018-07-18 13:58 trefis Note Added: 0019256
2018-07-19 19:03 trefis Note Added: 0019262
2018-07-19 19:03 trefis Status new => resolved
2018-07-19 19:03 trefis Fixed in Version => 4.07.1+dev
2018-07-19 19:03 trefis Resolution open => fixed
2018-07-19 19:03 trefis Assigned To => trefis


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker