Re: Weird behavior with mutually recursive type definitions

[Jerome Vouillon <Jerome.Vouillon@inria.fr>]

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