Re: Weird behavior with mutually recursive type definitions

[Francois Pottier <Francois.Pottier@inria.fr>]

> Why is it so? Constraints are required for the object system, and if
> there are constraints you must expand abbreviations inside definitions
> to check them.  If recursion occurs before the abbreviation is
> generalized, this means that all occurences of an abbreviation in the
> same type definition will be unified, and have the same constraints.

I fail to see why type abbreviations should be monomorphic while
their declaration is being checked. Is this intended to make the
type system safe, or to guarantee the typechecker's termination?

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.

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/