From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <furr@cs.umd.edu>
X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr
X-Spam-Level: 
X-Spam-Status: No, score=0.6 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE 
	autolearn=disabled version=3.1.3
X-Original-To: caml-list@yquem.inria.fr
Delivered-To: caml-list@yquem.inria.fr
Received: from discorde.inria.fr (discorde.inria.fr [192.93.2.38])
	by yquem.inria.fr (Postfix) with ESMTP id 05296BC69
	for <caml-list@yquem.inria.fr>; Tue, 12 Jun 2007 01:10:34 +0200 (CEST)
Received: from flyer.cs.umd.edu (flyer.cs.umd.edu [128.8.128.178])
	by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l5BNAUiY005521
	(version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO)
	for <caml-list@inria.fr>; Tue, 12 Jun 2007 01:10:33 +0200
Received: from loompa.cs.umd.edu (loompa.cs.umd.edu [128.8.128.63])
	by flyer.cs.umd.edu (8.12.11.20060308/8.12.5) with ESMTP id l5BNAP6N013839
	for <caml-list@inria.fr>; Mon, 11 Jun 2007 19:10:25 -0400
Received: from localhost (localhost [127.0.0.1])
	by loompa.cs.umd.edu (8.12.10/8.12.5) with ESMTP id l5BNAPbr012039
	for <caml-list@inria.fr>; Mon, 11 Jun 2007 19:10:25 -0400 (EDT)
Date: Mon, 11 Jun 2007 19:10:25 -0400 (EDT)
From: Michael Furr <furr@cs.umd.edu>
To: <caml-list@inria.fr>
Subject: Recursive module signatures + functors
Message-ID: <Pine.SOL.4.33.0706111848240.11389-100000@loompa.cs.umd.edu>
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
X-Miltered: at discorde with ID 466DD666.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 functor:01 val:01 struct:01 sig:01 val:01 struct:01 checker:01 mismatch:01 sig:01 bug: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.
Assume I have the following functor:

  module Mix(M : type t val f : t -> t) = struct
    let f_twice x = M.f (M.f x)
  end

If I then write:

  module type S = sig
    type t
    val f : t -> t
    val f_twice : t -> t
  end
  module rec M : S = struct
    type t = int
    let f t = t + 1
    include Mix(M)
  end

then the type checker complains
  Signature mismatch:
  Modules do not match:
    sig type t = int val f : int -> int val f_twice : M.t -> M.t end
  is not included in
    S
  Values do not match:
    val f_twice : M.t -> M.t
  is not included in
    val f_twice : t -> t

I don't quite understand why the type system doesn't know that t and M.t
are the same.  However, if I inline the signature and directly reference
M.t there, it works:

  module rec M : sig
    type t
    val f : t -> t
    val f_twice : M.t -> M.t  (* Note M. prefix *)
  end = struct
    type t = int
    let f t = t + 1
    include Mix(M)
  end

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


Cheers,
-Mike

P.S. This is with 3.10.0.