Version française
Home     About     Download     Resources     Contact us    
Browse thread
Weird behavior with mutually recursive type definitions
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Francois Pottier <Francois.Pottier@i...>
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/