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

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

Comment author: @garrigue

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

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