Original bug ID: 7592
Reporter: lavi
Assigned to: @garrigue
Status: confirmed (set by @garrigue on 2017-08-02T04:17:38Z)
Resolution: open
Priority: normal
Severity: feature
Version: 4.05.0
Category: typing
Child of: #5998

Bug description

This is not a bug as OCaml stay in the safe side, but behavior of GADT in presence of polymorphic variant is sometimes disturbing.

For example, the following is accepted:

type _ c1 = C1 : [> `A | `B ] c1
type _ c2 = C2 : [> `A | `C ] c2 
let f : type a. a c1 -> a c2 -> a  = fun C1 C2 -> `A
let x = f C1 C2
let g : type a. a c1 -> a c2 -> a  = fun C1 C2 -> `B
let y = g C1 C2

with the right type:

val y : [> `A | `B | `C ] = `B

However this does not work with `C:

let h : type a. a c1 -> a c2 -> a  = fun C1 C2 -> `C;;
Error: This expression has type [> `C ]
       but an expression was expected of type a
       The second variant type does not allow tag(s) `C