From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <caml-list-owner@inria.fr>
Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83])
	by c5ff346549e7 (Postfix) with ESMTPS id 3ECE11E6
	for <caml-list@inbox.ocaml.org>; Fri, 13 Nov 2020 13:07:39 +0000 (UTC)
X-IronPort-AV: E=Sophos;i="5.77,475,1596492000"; 
   d="scan'208";a="477381571"
Received: from prod-listesu18.inria.fr (HELO sympa.inria.fr) ([128.93.162.160])
  by mail2-relais-roc.national.inria.fr with ESMTP; 13 Nov 2020 14:07:38 +0100
Received: by sympa.inria.fr (Postfix, from userid 20132)
	id 187C0E1F4A; Fri, 13 Nov 2020 14:07:38 +0100 (CET)
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 8FBEDE1F43
	for <caml-list@sympa.inria.fr>; Fri, 13 Nov 2020 14:07:36 +0100 (CET)
X-IronPort-AV: E=Sophos;i="5.77,475,1596492000"; 
   d="scan'208";a="477381551"
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 14:07:36 +0100
To: caml-list@inria.fr
References: <23c53e70-4045-6812-9767-1bb60f70465e@inria.fr>
From: =?UTF-8?Q?Fran=c3=a7ois_Pottier?= <francois.pottier@inria.fr>
Message-ID: <ad95e76b-8dfc-5ba0-0f26-7e020a4d5994@inria.fr>
Date: Fri, 13 Nov 2020 14:07:36 +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
In-Reply-To: <23c53e70-4045-6812-9767-1bb60f70465e@inria.fr>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: fr
Content-Transfer-Encoding: 8bit
Subject: Re: [Caml-list] Another question on subsumption of polymorphic
 variants
Reply-To: =?UTF-8?Q?Fran=c3=a7ois_Pottier?= <francois.pottier@inria.fr>
X-Loop: caml-list@inria.fr
X-Sequence: 18286
Errors-To: caml-list-owner@inria.fr
Precedence: list
Precedence: bulk
Sender: caml-list-request@inria.fr
X-no-archive: yes
List-Id: <caml-list.inria.fr>
List-Help: <mailto:sympa_inria@inria.fr?subject=help>
List-Subscribe: <mailto:sympa_inria@inria.fr?subject=subscribe%20caml-list>
List-Unsubscribe: <mailto:sympa_inria@inria.fr?subject=unsubscribe%20caml-list>
List-Post: <mailto:caml-list@inria.fr>
List-Owner: <mailto:caml-list-request@inria.fr>
List-Archive: <http://sympa.inria.fr/sympa/arc/caml-list>
Archived-At: <http://sympa.inria.fr/sympa/arcsearch_id/caml-list/2020-11/ad95e76b-8dfc-5ba0-0f26-7e020a4d5994%40inria.fr>

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/