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/