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

["François Pottier" <francois.pottier@inria.fr>]

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/