Why aren't the closed subsets of polymorphic variant types checked over a superset?

The variant is [`A | `B]

not compatible with the supernet type, for example[`A | `B | `C]

I understand that they cannot be unified if subset or <

not added >

, but I am wondering if there is an example where accepting this type of input could result in incorrect programs.

In a very simplified use:

let return_a : bool -> [ `A ] = fun _ -> `A

let foo : bool -> [ `A | `B ] = return_a

      

        
        
        
      

    

It seems perfectly safe to accept an implementation, since the declared type foo

is a strict superset of the implementation type (which is the type return_a

). However (as expected) it will not introduce validation:

Error: This expression has type bool -> [ `A ]
but an expression was expected of type bool -> [ `A | `B ]
The first variant type does not allow tag(s) `B

      

        
        
        
      

    

It actually looks like a more restrictive type than

let return_a : bool -> [ `A ] = fun _ -> `A

let foo : bool -> [< `A | `B ] = return_a

      

        
        
        
      

    

What type checking does.

Is this limitation on the use of polymorphic variants just a limitation of how type inference works, or is there a practical reason for marking the first chunk as unassigned?