From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <j.d.yallop@sms.ed.ac.uk>
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 AE954BB83
	for <caml-list@yquem.inria.fr>; Thu,  4 May 2006 17:52:06 +0200 (CEST)
Received: from grassmarket.ucs.ed.ac.uk (grassmarket.ucs.ed.ac.uk [129.215.166.64])
	by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k44Fq6Hu003038
	for <caml-list@yquem.inria.fr>; Thu, 4 May 2006 17:52:06 +0200
Received: from [129.215.11.81] (dhcp-11-81.inf.ed.ac.uk [129.215.11.81])
	by grassmarket.ucs.ed.ac.uk (8.13.6/8.12.10) with ESMTP id k44Fq2qx026131
	for <caml-list@yquem.inria.fr>; Thu, 4 May 2006 16:52:02 +0100 (BST)
Message-ID: <445A22BA.4070807@sms.ed.ac.uk>
Date: Thu, 04 May 2006 16:50:18 +0100
From: Jeremy Yallop <j.d.yallop@sms.ed.ac.uk>
User-Agent: Thunderbird 1.5.0.2 (X11/20060501)
MIME-Version: 1.0
To: caml-list@yquem.inria.fr
Subject: Oddness with recursive polymorphic variants
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
X-Edinburgh-Scanned: at grassmarket.ucs.ed.ac.uk
    with MIMEDefang 2.33, Sophie, Sophos Anti-Virus
X-Scanned-By: MIMEDefang 2.33 (www . roaringpenguin . com / mimedefang)
X-Miltered: at concorde with ID 445A2326.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)!
X-Spam: no; 0.00; recursive:01 variants:01 compiler:01 variants:01 bug:01 polymorphic:01 polymorphic:01 minor:01 expression:01 variant:02 variant:02 types:02 sms:96 seems:03 let:03 
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

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)?

Indeed, minor variants of the function are accepted.  Both of the 
following are ok:

   let s2 : f -> g = function
     | `A -> `A
     | `B (#f as b) -> b

   let s3 : f -> g = function
     | `A -> `A
     | `B ((`A|`B _) as b) -> b

Am I missing something, or is this a bug?

Thanks,

Jeremy.