Hello,

I am puzzled by O'Caml 2.02's bizarre behavior regarding mutually recursive
type declarations. 

Let's start by defining a dummy, unary type constructor.

  type 'a dummy = Dummy

(The right-hand side of this definition isn't relevant here; the problem
also shows up when 'a dummy is an abstract type constructor, provided by
a functor argument.)

Then, consider the following type definitions:

  type 'a t = 'a dummy
  type specialized = int t

The first type declaration simply renames ``dummy'' into ``t'', and the second
one creates a specialized instance of it. O'Caml correctly analyzes these
declarations.

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?

Thanks,

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