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

OCaml 4.03.0+beta1 rejects previously accepted cast #7199

Closed
vicuna opened this Issue Mar 29, 2016 · 4 comments

Comments

Projects
None yet
2 participants
@vicuna
Copy link
Collaborator

commented Mar 29, 2016

Original bug ID: 7199
Reporter: talex
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2017-09-24T15:32:10Z)
Resolution: fixed
Priority: normal
Severity: major
Fixed in version: 4.03.0+dev / +beta1
Category: typing
Related to: #7135
Monitored by: @yallop

Bug description

This 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 information

This is a simplified version of the error reported in ocaml/opam-repository#6138

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Mar 29, 2016

Comment author: @lpw25

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

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Mar 29, 2016

Comment author: @stedolan

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])

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Mar 30, 2016

Comment author: @garrigue

Fixed in 4.03 by commit 50ecb4.
This was a side-effect of the fix of #7135.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Mar 30, 2016

Comment author: @lpw25

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 ]).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.