Re: Weird behavior with mutually recursive type definitions

From: Jerome Vouillon (Jerome.Vouillon@inria.fr)
Date: Fri Aug 27 1999 - 13:32:07 MET DST


Date: Fri, 27 Aug 1999 13:32:07 +0200
From: Jerome Vouillon <Jerome.Vouillon@inria.fr>
To: Francois Pottier <Francois.Pottier@inria.fr>,
Subject: Re: Weird behavior with mutually recursive type definitions
In-Reply-To: <19990816083158.52649@pauillac.inria.fr>; from Francois Pottier on Mon, Aug 16, 1999 at 08:31:58AM +0200

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



This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:24 MET