Weird behavior with mutually recursive type definitions

From: Francois Pottier (Francois.Pottier@inria.fr)
Date: Wed Aug 04 1999 - 15:52:39 MET DST


Date: Wed, 4 Aug 1999 15:52:39 +0200
From: Francois Pottier <Francois.Pottier@inria.fr>
To: caml-list@inria.fr
Subject: Weird behavior with mutually recursive type definitions

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/



This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:24 MET