From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <garrigue@math.nagoya-u.ac.jp>
X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr
X-Spam-Level: 
X-Spam-Status: No, score=0.4 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE 
	autolearn=disabled version=3.1.3
Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82])
	by yquem.inria.fr (Postfix) with ESMTP id 896EBBBC4
	for <caml-list@yquem.inria.fr>; Thu, 16 Apr 2009 14:23:19 +0200 (CEST)
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: ApoEAEzA5kmCNhAB/2dsb2JhbADQb4N9Bg
X-IronPort-AV: E=Sophos;i="4.38,431,1233529200"; 
   d="scan'208";a="27787838"
Received: from kurims.kurims.kyoto-u.ac.jp ([130.54.16.1])
  by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 16 Apr 2009 14:23:18 +0200
Received: from localhost (orion [130.54.16.5])
	by kurims.kurims.kyoto-u.ac.jp (8.13.8/8.13.8) with ESMTP id n3GCNCdC009525;
	Thu, 16 Apr 2009 21:23:12 +0900 (JST)
Date: Thu, 16 Apr 2009 21:23:14 +0900 (JST)
Message-Id: <20090416.212314.107686494.garrigue@math.nagoya-u.ac.jp>
To: philippe.veber@googlemail.com
Cc: caml-list@yquem.inria.fr
Subject: Re: [Caml-list] Typing of polymorphic variants
From: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
In-Reply-To: <721f7f5a0904150548o7351d50fm44aaf29b249b67f6@mail.gmail.com>
References: <721f7f5a0904150548o7351d50fm44aaf29b249b67f6@mail.gmail.com>
X-Mailer: Mew version 5.2 on Emacs 22.1 / Mule 5.0 (SAKAKI)
Mime-Version: 1.0
Content-Type: Text/Plain; charset=us-ascii
Content-Transfer-Encoding: 7bit
X-Spam: no; 0.00; variants:01 datatypes:01 recursion:01 datatype:01 abbreviation:01 abbreviation:01 datatype:01 recursive:01 polymorphic:01 typing:01 caml-list:01 int:01 int:01 behaviour:01 caml:02 

From: Philippe Veber <philippe.veber@googlemail.com>
> I don't understand the following behaviour:
> 
>         Objective Caml version 3.11.0
> 
> # type t = [`A | `B of int u] and 'a u = 'a * t;;
> Error: In the definition of t, type int u should be 'a u
> # type t = A | B of int u and 'a u = 'a * t;;
> type t = A | B of int u
> and 'a u = 'a * t
> 
> Anyone's got a simple explanation for this ?

This is due to the difference between type abbreviations and
datatypes. In your first example, you are defining two types
abbreviations, and you are not allowed to instantiate a type you are
defining in mutual recursion. In the second example, you are defining a
datatype and a type abbreviation, and it is ok to instantiate the type
abbreviation inside the datatype definition.

The technical reason for this difference is the restriction to regular
types in type abbreviations. It only applies when the definitions are
mutually recursive, and do not go through any datatype definition.

Jacques Garrigue