Recursive module signatures + functors

Recursive module signatures + functors

[Michael Furr]

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.

Re: [Caml-list] Recursive module signatures + functors

[rossberg]

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

It is not a bug, but a limitation of the current semantics of recursive
modules. It is unrelated to functors - here is a simpler version of your
example that fails in the same way:

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

It's basically the same issue as described here:

http://caml.inria.fr/pub/ml-archives/caml-list/2007/05/d9414d45a9a6f30f2609e08c43f011a0.en.html

- Andreas

Re: [Caml-list] Recursive module signatures + functors

[Xavier Leroy]

> 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