From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <francois.pottier@inria.fr>
Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83])
	by sympa.inria.fr (Postfix) with ESMTPS id 8D72AE1F43
	for <caml-list@sympa.inria.fr>; Fri, 13 Nov 2020 13:55:50 +0100 (CET)
X-IronPort-AV: E=Sophos;i="5.77,475,1596492000"; 
   d="scan'208";a="477378692"
Received: from 91-175-127-215.subs.proxad.net (HELO MacBook-Pro-5.local) ([91.175.127.215])
  by mail2-relais-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 13 Nov 2020 13:55:50 +0100
To: OCaML Mailing List <caml-list@inria.fr>
From: =?UTF-8?Q?Fran=c3=a7ois_Pottier?= <francois.pottier@inria.fr>
Message-ID: <23c53e70-4045-6812-9767-1bb60f70465e@inria.fr>
Date: Fri, 13 Nov 2020 13:55:50 +0100
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:68.0)
 Gecko/20100101 Thunderbird/68.12.1
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: fr
Content-Transfer-Encoding: 8bit
Subject: [Caml-list] Another question on subsumption of polymorphic variants


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/