caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
* [Caml-list] Another question on subsumption of polymorphic variants
@ 2020-11-13 12:55 François Pottier
  2020-11-13 13:07 ` François Pottier
  0 siblings, 1 reply; 2+ messages in thread
From: François Pottier @ 2020-11-13 12:55 UTC (permalink / raw)
  To: OCaML Mailing List


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/

^ permalink raw reply	[flat|nested] 2+ messages in thread

end of thread, other threads:[~2020-11-13 13:07 UTC | newest]

Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2020-11-13 12:55 [Caml-list] Another question on subsumption of polymorphic variants François Pottier
2020-11-13 13:07 ` François Pottier

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).