From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id EB164BB83 for ; Thu, 4 May 2006 21:01:48 +0200 (CEST) Received: from swip.net (mailfe10.tele2.fr [212.247.155.44]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k44J1mEF025118 for ; Thu, 4 May 2006 21:01:48 +0200 X-T2-Posting-ID: VOFteLZ+LTHhOWGZw3zDiXYGNWCfSPl1g+TbJcmKNB0= X-Cloudmark-Score: 0.000000 [] Received: from [83.177.250.40] (HELO lycoperdon.mycelium) by mailfe10.swip.net (CommuniGate Pro SMTP 5.0.8) with SMTP id 20860212 for caml-list@yquem.inria.fr; Thu, 04 May 2006 21:01:45 +0200 Date: Thu, 4 May 2006 21:03:19 +0200 From: Nils Gesbert To: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Oddness with recursive polymorphic variants Message-Id: <20060504210319.5e05f7a6.nils.gesbert@ens.fr> In-Reply-To: <445A22BA.4070807@sms.ed.ac.uk> References: <445A22BA.4070807@sms.ed.ac.uk> X-Mailer: Sylpheed version 2.2.3 (GTK+ 2.4.1; i686-pc-linux-gnu) Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-Miltered: at concorde with ID 445A4F9C.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; nils:01 nils:01 recursive:01 variants:01 compiler:01 subtype:01 polymorphic:01 polymorphic:01 caml-list:01 expression:01 coercion:01 variant:02 variant:02 ens:02 types:02 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.1 required=5.0 tests=FORGED_RCVD_HELO autolearn=disabled version=3.0.3 Jeremy Yallop a écrit : » I have two polymorphic variant types, as follows: » » type f = [`A | `B of f] » type g = [f | `C] » » Next, I have a function from f to g: » » let s1 : f -> g = function » | `A -> `A » | `B b -> b » » Sadly, the compiler rejects this: » » Characters 57-58: » | `B b -> b;; » ^ » This expression has type f but is here used with type g » The first variant type does not allow tag(s) `C » » The error message seems odd. Why should it matter that g has more tags » than f, since every value of f is a value of g (by definition)? f is indeed a subtype of g, but to forget the precise type of b (that is, forget the information that it cannot contain the tag `C), you have to use explicit coercion, i. e. : let s1 : f -> g = function | `A -> `A | `B b -> (b :> g)