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

[Xavier Leroy <Xavier.Leroy@inria.fr>]

> 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