From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <Xavier.Leroy@inria.fr>
X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr
X-Spam-Level: 
X-Spam-Status: No, score=0.0 required=5.0 tests=AWL autolearn=disabled 
	version=3.1.3
X-Original-To: caml-list@yquem.inria.fr
Delivered-To: caml-list@yquem.inria.fr
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39])
	by yquem.inria.fr (Postfix) with ESMTP id DDEE3BC69
	for <caml-list@yquem.inria.fr>; Tue, 12 Jun 2007 11:47:53 +0200 (CEST)
Received: from [128.93.11.95] (estephe.inria.fr [128.93.11.95])
	by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l5C9lkDI004322;
	Tue, 12 Jun 2007 11:47:47 +0200
Message-ID: <466E6BC2.1080001@inria.fr>
Date: Tue, 12 Jun 2007 11:47:46 +0200
From: Xavier Leroy <Xavier.Leroy@inria.fr>
User-Agent: Thunderbird 1.5.0.7 (X11/20060915)
MIME-Version: 1.0
To: Michael Furr <furr@cs.umd.edu>
Cc: Caml List <caml-list@yquem.inria.fr>
Subject: Re: [Caml-list] Recursive module signatures + functors
References: <Pine.SOL.4.33.0706111848240.11389-100000@loompa.cs.umd.edu>
In-Reply-To: <Pine.SOL.4.33.0706111848240.11389-100000@loompa.cs.umd.edu>
X-Enigmail-Version: 0.94.0.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
X-Miltered: at concorde with ID 466E6BC3.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)!
X-Spam: no; 0.00; recursive:01 functors:01 recursive:01 mixins:01 checker:01 ocaml:01 type-checker:01 generative:01 sig:01 val:01 struct:01 type-checker:01 abbreviation:01 sig:01 val:01 

> I've been playing around with using recursive modules to implement mixins
> and don't understand why the type checker fails to accept code below.
> [...]
> I don't quite understand why the type system doesn't know that t and M.t
> are the same.

As Andreas said, this is an instance of the infamous "double vision"
problem.  The OCaml module type-checker can deal with this, but the
current implementation is incomplete and works only for generative
type definitions, not for type abbreviations.

Continuing Andreas' example:

module rec M : sig type t val f : t -> t end =
struct
   type t = N of int
   let f (x : M.t) = x
end

This is accepted because the type-checker can add a type equality
"t = M.t" while type-checking the body of the structure.  However,
with a type abbreviation

module rec M : sig type t val f : t -> t end =
struct
   type t = int
   let f (x : M.t) = x
end

there is already a type equality over t, namely "t = int", and the
current implementation of the type-checker is not able to record and
maintain several type equalities (here, t = int = M.t) over one type
constructor.

Likewise, your example goes through if you put "type t = Constr of ..."
instead of "type t = int".

> Is this a bug in the type checker or is there a reason that it does not
> unify 't' and 'M.t'?

Well, there is a technical reason, but I agree this limitation is a bug.

- Xavier Leroy