caml-list - the Caml user's mailing list
 help / 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

* Re: [Caml-list] Another question on subsumption of polymorphic variants
  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
  0 siblings, 0 replies; 2+ messages in thread
From: François Pottier @ 2020-11-13 13:07 UTC (permalink / raw)
  To: caml-list

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/

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

end of thread, back to index

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

caml-list - the Caml user's mailing list

Archives are clonable: git clone --mirror https://inbox.ocaml.org/caml-list

AGPL code for this site: git clone https://public-inbox.org/ public-inbox