From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 97C21BBB7 for ; Thu, 14 Aug 2008 17:27:49 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: At8BAGjro0hCbwQZlGdsb2JhbACRfwEBAQEJAwoHEQSkCIFV X-IronPort-AV: E=Sophos;i="4.32,210,1217800800"; d="scan'208";a="28223266" Received: from concorde.inria.fr ([192.93.2.39]) by mail4-smtp-sop.national.inria.fr with ESMTP; 14 Aug 2008 17:27:49 +0200 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id m7EFRkM1019256 for ; Thu, 14 Aug 2008 17:27:49 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: At8BAGjro0hCbwQZlGdsb2JhbACRfwEBAQEJAwoHEQSkCIFV X-IronPort-AV: E=Sophos;i="4.32,210,1217800800"; d="scan'208";a="28223259" Received: from out1.smtp.messagingengine.com ([66.111.4.25]) by mail4-smtp-sop.national.inria.fr with ESMTP; 14 Aug 2008 17:27:28 +0200 Received: from compute2.internal (compute2.internal [10.202.2.42]) by out1.messagingengine.com (Postfix) with ESMTP id D0FC515771D; Thu, 14 Aug 2008 11:27:23 -0400 (EDT) Received: from heartbeat1.messagingengine.com ([10.202.2.160]) by compute2.internal (MEProxy); Thu, 14 Aug 2008 11:27:23 -0400 X-Sasl-enc: U+Ygj4pGGMAZal0H5WDzOzIxP8l1b/c+kyGhVtF4HPB9 1218727643 Received: from [192.168.1.10] (ALyon-157-1-41-125.w83-201.abo.wanadoo.fr [83.201.72.125]) by mail.messagingengine.com (Postfix) with ESMTPSA id D6708138BA; Thu, 14 Aug 2008 11:27:22 -0400 (EDT) Date: Thu, 14 Aug 2008 17:22:01 +0200 (CEST) From: Martin Jambon X-X-Sender: martin@martin.ec.wink.com To: Jacques Carette Cc: caml-list@inria.fr Subject: Re: [Caml-list] Why is this coercion necessary? In-Reply-To: <48A395FA.2050704@mcmaster.ca> Message-ID: References: <48A395FA.2050704@mcmaster.ca> MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed X-Miltered: at concorde with ID 48A44EF2.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; ens-lyon:01 'n':01 intersection:01 intersection:01 type-checker:01 coercions:01 polluting:01 'recursive:01 bug:01 coercions:01 wrote:01 caml-list:01 coercion:01 coercion:01 jambon:01 On Wed, 13 Aug 2008, Jacques Carette wrote: > Here is a much simplified version from a (much) larger problem I have > recently encountered: > > type 'a a = [`A of 'a b] > and 'a b = [`B of 'a a] > and 'a c = [`C ] > > type 'a d = [ 'a a | 'a b | 'a c] > type e = e d > > # this code gives an error (details below) > let f1 (x:e) : e = match x with > | `A n -> n > | `B n -> n > | `C -> `C > > # this works > let f2 (x:e) : e = match x with > | `A n -> (n :> e) > | `B n -> (n :> e) > | `C -> `C > > f1 gives an error on the "| `B n -> n" line, pointing to the second 'n' with > This expression has type e a but is used with type e b > These two variant types have no intersection > > Indeed, they have no intersection, but they have a union! That is what it > seems the coercion in f2 'forces' the type-checker to realize, and all works > fine. But of course, such coercions end up polluting my code all over the > place (since the actual example is made of 9 types with 20 tags in total, and > the 'recursive knot' requires 2 parameters to close properly). > > So, is this a bug? Is there a way to avoid these coercions? The following works, but I doubt it would make your code shorter: type 'a a = [`A of 'a b] and 'a b = [`B of 'a a] and 'a c = [`C ] type 'a d = [ 'a a | 'a b | 'a c] type e = e d type f = [`A of e | `B of e | `C ] let f3 (x:e) : e = match (x :> f) with | `A n -> n | `B n -> n | `C -> `C Martin -- http://mjambon.com/