From mboxrd@z Thu Jan  1 00:00:00 1970
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id PAA26896 for caml-redistribution; Mon, 30 Aug 1999 15:36:39 +0200 (MET DST)
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id NAA19047 for <caml-list@pauillac.inria.fr>; Fri, 27 Aug 1999 13:40:47 +0200 (MET DST)
Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35])
	by concorde.inria.fr (8.8.7/8.8.7) with ESMTP id NAA26580;
	Fri, 27 Aug 1999 13:32:09 +0200 (MET DST)
Received: (from vouillon@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id NAA15070; Fri, 27 Aug 1999 13:32:07 +0200 (MET DST)
Message-ID: <19990827133207.53446@pauillac.inria.fr>
Date: Fri, 27 Aug 1999 13:32:07 +0200
From: Jerome Vouillon <Jerome.Vouillon@inria.fr>
To: Francois Pottier <Francois.Pottier@inria.fr>,
        Jacques GARRIGUE <garrigue@kurims.kyoto-u.ac.jp>
Cc: caml-list@inria.fr
Subject: Re: Weird behavior with mutually recursive type definitions
References: <19990804155239.50895@pauillac.inria.fr> <19990813104206X.garrigue@kurims.kyoto-u.ac.jp> <19990816083158.52649@pauillac.inria.fr>
Mime-Version: 1.0
Content-Type: text/plain; charset=iso-8859-1
Content-Transfer-Encoding: 8bit
X-Mailer: Mutt 0.89.1
In-Reply-To: <19990816083158.52649@pauillac.inria.fr>; from Francois Pottier on Mon, Aug 16, 1999 at 08:31:58AM +0200
Sender: weis

On Mon, Aug 16, 1999 at 08:31:58AM +0200, Francois Pottier wrote:

> By the way, I find O'Caml's error messages on this topic rather
> strange. If I try:
> 
>   type 'a t = ('a -> 'a) u
>   and 'a u = ('a -> 'a) t
> 
> then I obtain
> 
>   This type ('a -> 'a) -> 'a -> 'a should be an instance of type 'a
> 
> which corresponds to the problem discussed so far. This seems to
> indicate that t and u are understood as mutually recursive type
> abbreviations. However, if I try:
> 
>   type t = u and u = t
> 
> then O'Caml answers
> 
>   A type variable is unbound in this type declaration
> 
> which surprises me. I would rather expect to be warned about
> cyclic type abbreviations.

In fact, in the latter case, the abbreviations are underspecified :
the expansion of t and u could be any type. When typing this
declaration, the compiler first assumes that the type t expand to some
type variable 'a and then tries to use the equalities t = u and u = t
to refine the expansion. In this case, the expansion remains unchanged
and therefore, the compiler complains that the type t expands to an
unbound type variable 'a.

-- Jérôme