[Caml-list] Another question on subsumption of polymorphic variants

[Caml-list] Another question on subsumption of polymorphic variants

[François Pottier]

Dear all,

Here is another question, which will show how little I understand
about the subsumption (subtyping) rules for polymorphic variants.

The following code is rejected:

module F (X : sig
   val x : [< `A > `A ]
end) : sig
   val x : [> `A ]
end
= X

Yet I would intuitively expect it to be accepted, because
the type [< `A > `A ] seems to be a subtype of the type [> `A ].
The former type is inhabited only by the value `A, while the
latter type is inhabited by this value and others. In fact,
this semantically equivalent piece of code is accepted:

module F (X : sig
   val x : [< `A > `A ]
end) : sig
   val x : [> `A ]
end
= struct
   let x = match X.x with `A -> `A
end

Is there any way of convincing the type-checker that
[< `A > `A ] can be coerced to [> `A ]?

More generally, this suggests that when a polymorphic variant
type appears in a positive position, it should be permitted
to drop the upper bound that appears inside it.

-- 
François Pottier
francois.pottier@inria.fr
http://cambium.inria.fr/~fpottier/

Re: [Caml-list] Another question on subsumption of polymorphic variants

[François Pottier]

Le 13/11/2020 à 13:55, François Pottier a écrit :
> Yet I would intuitively expect it to be accepted, because
> the type [< `A > `A ] seems to be a subtype of the type [> `A ].

Replying to my own question, I note that the type-checker seems to
recognize that this subsumption relation holds when I use an
explicit coercion:

# let f x = (x : [`A] :> [> `A ]);;
val f : [ `A ] -> [> `A ] = <fun>

but it does not recognize it when comparing one module signature
against another module signature.

-- 
François Pottier
francois.pottier@inria.fr
http://cambium.inria.fr/~fpottier/