Re: Weird behavior with mutually recursive type definitions

[Jacques GARRIGUE <garrigue@kurims.kyoto-u.ac.jp>]

From: 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?

My explanation probably lacked clarity.

Since abbreviations may contain constraints, one must expand them when
defining types depending on them (to check that the constraints are
satisfied).

If the abbreviation has been defined earlier, no problem, you just
extract its constraints.

But if it is yet to be defined (which is the case with mutually
recursive definitions), you must keep everything monomorphic so that
constraints can be enforced later.

What we want is just to enforce constraints from the abbreviation to
other type definitions, but as a result this means also introducing
constraints the other way round (classical problem with unification).

My comment was that such a restrictive algorithm is needed if we want
to collect all constraints in one pass, but if we require that all
abbreviation definitions contain explicitely all their constraints,
the above problem can be avoided with a two-pass algorithm.

> By the way, I find O'Caml's error messages on this topic rather
> strange.

Error messages with unification are hard.
You can see here another funny behaviour with recursive definitions:

	# type t = u and u = unit;;
	type t = unit
	type u = t


	Jacques
---------------------------------------------------------------------------
Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>