From: Francois Pottier <Francois.Pottier@inria.fr>

> Now, here's the problem. Let's change just one word, and make the type
> declarations mutually recursive, even though they needn't be:
> 
>   type 'a t = 'a dummy
>    and specialized = int t
> 
> O'Caml still accepts the code, but this time, it constrains 'a to be equal to
> int, as if the type constructor t could not be used polymorphically within its
> own declaration:
> 
>   type 'a t = 'a dummy constraint 'a = int
>                        ^^^^^^^^^^^^^^^^^^^
>   type specialized = int t
> 
> Why is this? Can someone explain, or is it a typechecker bug?

As Hendrik Tews already answered, this is not a bug.
Like value definitions, recursive type abbreviation definitions are
not polymorphic (while they are defined). So if in your defintion you
use the abbreviation at a different type, a constraint is added.

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 personnaly think that, like for polymorphic recursion, the semantics
could be changed so that the user has to write explicitely the
constraints. In type definitions, this makes sense. If a constraint
appears to be needed somewhere and was not declared, there would be an
error.  Technically this would probably mean doing two passes on type
definitions: one to introduce definitions (polymorphically) and one to
check the constraints. In such a way, one could avoid this strange
side-effect of the object system on the rest of the language.

Comments, Jerome ?

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