Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007199OCamltypingpublic2016-03-29 21:182017-09-24 17:32
Reportertalex 
Assigned Togarrigue 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version4.03.0+dev / +beta1 
Summary0007199: OCaml 4.03.0+beta1 rejects previously accepted cast
DescriptionThis code is accepted by 4.02.3, but rejected by 4.03.0+beta1:

module type S = sig
  type +'a t

  val foo : [`A] t -> unit
  val bar : [< `A | `B] t -> unit
end

module Make(T : S) = struct
  let f x =
    T.foo x;
    T.bar x;
    (x :> [`A | `C] T.t)
end
Steps To Reproduce$ ocaml -version
The OCaml toplevel, version 4.02.3
$ ocaml test.ml
$

but

$ ocaml -version
The OCaml toplevel, version 4.03.0+beta1
$ ocaml test.ml
File "./test.ml", line 12, characters 4-24:
Error: Type [ `A ] T.t is not a subtype of [ `A | `C ] T.t
       The first variant type does not allow tag(s) `C
Additional InformationThis is a simplified version of the error reported in https://github.com/ocaml/opam-repository/pull/6138 [^]
TagsNo tags attached.
Attached Files

- Relationships
related to 0007135closedgarrigue Surprising "This ground coercion is not principal" warning 

-  Notes
(0015641)
lpw25 (developer)
2016-03-29 23:14

From a quick glance, I don't think that coercion is principal. If you turn on '-principal' it will probably give you a warning. If so then this may not be a bug but merely a change in the inference algorithm. To be robust against such changes you should periodically compile things with '-principal'.
(0015642)
stedolan (developer)
2016-03-30 00:02

This seems like a bug. It's accepted by 4.02.1 (normal and -principal, no warnings), accepted by 4.03.0+beta1 -principal (again with no warnings), but rejected by 4.03.0+beta1 without -principal.

Should there be programs accepted by -principal with no warnings but rejected otherwise?

In any case, the error message is wrong: [ `A ] T.t is indeed a subtype of [ `A | `C ] T.t

Incidentally, the test case can be simplified, and seems to have nothing to do with abstract types, covariance or modules:

let f (foo : [`A] -> unit) (bar : [< `A | `B] -> unit) x =
  foo x; bar x; (x :> [`A | `C])
(0015644)
garrigue (manager)
2016-03-30 03:51

Fixed in 4.03 by commit 50ecb4.
This was a side-effect of the fix of PR#7135.
(0015645)
lpw25 (developer)
2016-03-30 09:00
edited on: 2016-03-30 09:00

> Should there be programs accepted by -principal with no warnings but rejected otherwise?

No, that's always a bug. In fact it's quite a good way of detecting this kind of bug.

Looking again I can see that the coercion is principal. I had forgotten that in such cases OCaml treats ( x :> [`Foo ]) as ( x : [< `Foo ] :> [`Foo ]).


- Issue History
Date Modified Username Field Change
2016-03-29 21:18 talex New Issue
2016-03-29 23:14 lpw25 Note Added: 0015641
2016-03-30 00:02 stedolan Note Added: 0015642
2016-03-30 03:17 garrigue Relationship added related to 0007135
2016-03-30 03:51 garrigue Note Added: 0015644
2016-03-30 03:51 garrigue Status new => resolved
2016-03-30 03:51 garrigue Fixed in Version => 4.03.0+dev / +beta1
2016-03-30 03:51 garrigue Resolution open => fixed
2016-03-30 03:51 garrigue Assigned To => garrigue
2016-03-30 09:00 lpw25 Note Added: 0015645
2016-03-30 09:00 lpw25 Note Edited: 0015645 View Revisions
2017-02-23 16:45 doligez Category OCaml typing => typing
2017-09-24 17:32 xleroy Status resolved => closed


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker