From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <weis@pauillac.inria.fr>
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 0223FBB86
	for <caml-list@yquem.inria.fr>; Fri,  5 May 2006 00:37:18 +0200 (CEST)
Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35])
	by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k44MbIIL012522
	for <caml-list@yquem.inria.fr>; Fri, 5 May 2006 00:37:18 +0200
Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id AAA19132 for <caml-list@pauillac.inria.fr>; Fri, 5 May 2006 00:37:17 +0200 (MET DST)
Received: from mcr-smtp-001.bulldogdsl.com (smtp.bulldogdsl.com [212.158.248.7])
	by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id k44MbGcv030948;
	Fri, 5 May 2006 00:37:17 +0200
Received: by mcr-smtp-001.bulldogdsl.com (Postfix, from userid 1005)
	id B4F6C7129B7; Thu,  4 May 2006 20:11:40 +0100 (BST)
Received: from [192.168.123.123] (host-84-9-232-199.bulldogdsl.com [84.9.232.199])
	by mcr-smtp-001.bulldogdsl.com (Postfix) with ESMTP id 2E2797135DD;
	Thu,  4 May 2006 19:58:13 +0100 (BST)
Message-ID: <445A4ED7.9080900@sms.ed.ac.uk>
Date: Thu, 04 May 2006 19:58:31 +0100
From: Jeremy Yallop <j.d.yallop@sms.ed.ac.uk>
User-Agent: Mozilla Thunderbird 1.0.7 (X11/20051013)
X-Accept-Language: en-us, en
MIME-Version: 1.0
To: caml-list@inria.fr
Cc: brogoff <brogoff@speakeasy.net>,
	Luc Maranget <luc.maranget@inria.fr>
Subject: Re: [Caml-list] Oddness with recursive polymorphic variants
References: <445A23BF.4030001@sms.ed.ac.uk> <20060504171010.GB23421@yquem.inria.fr> <Pine.LNX.4.58.0605041128440.9940@shell3.speakeasy.net>
In-Reply-To: <Pine.LNX.4.58.0605041128440.9940@shell3.speakeasy.net>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
X-Miltered: at concorde with ID 445A821E.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)!
X-Miltered: at nez-perce with ID 445A821C.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)!
X-Spam: no; 0.00; recursive:01 variants:01 maranget:01 polymorphism:01 behaves:01 wrote:01 wrote:01 luc:01 polymorphic:01 caml-list:01 expression:01 'g':01 constraint:01 variant:02 match: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.0 required=5.0 tests=none autolearn=disabled 
	version=3.0.3

brogoff wrote:
> On Thu, 4 May 2006, Luc Maranget wrote:
> 
>>I cannot really explain why it matters, but I can supply a minimal (?) example
>>
>>type f = [`A ]
>>type g = [f | `C]
>>
>>let k (x:f) = (x:g);;
>>               ^
>>This expression has type f but is here used with type g
>>The first variant type does not allow tag(s) `C
> 
> 
> Not enough polymorphism, the error message seems clear
> 
> type 'a h = 'a constraint 'a = [> `A];;
> let k (x : 'a h) = (x : g)

Thanks for the reply.  That doesn't seem to be what I want, though.  The 
input to k should have type 'f'.  The output should have type 'g'.  Your 
'k' can be called with values that don't match type 'f':

    # k `C;;
    - : g = `C

The following does what I want:

    let k (#f as x:f) = (x:g)

I'd like to understand why it behaves differently from the following:

    let k (x:f) = (x:g)

Jeremy.