Recursive module inside functor

I am trying to define a recursive module inside a functor. The definition of the functor is accepted, but when I try to instantiate it, I get a signature mismatch. Here’s a small example:

``````module type Fam = sig
type 'b t
end

module type Fam2 = sig
type ('a, 'b) t
end

module A (F : Fam2) = struct
type 'b t = |
end

module B ( F : Fam) = struct
module rec C : sig
type 'b foo = Entry of 'b C.D.t
module M : sig
type ('a, 'b) t = ('a * 'b) foo
end
module D : module type of A(M)
end = struct
type 'b foo = Entry of 'b C.D.t
module M = struct
type ('a, 'b) t = ('a * 'b) foo
end
module D = A(M)
end
end

module E = struct
type 'b t = { x : int }
end

module N = B(E)
``````

Here the final line gives the error

``````Error: In the signature of this functor application:
This variant or record definition does not match that of type
'b B(E).C.foo
Constructors do not match:
Entry of 'b B(E).C.D.t
is not the same as:
Entry of 'b C.D.t
The type 'b A(B(E).C.M).t is not equal to the type 'b C.D.t
``````

Am I doing something wrong? Is there a way to make this work?

1 Like

With a more recent version of the compiler, the error message is

``````  The type 'b B(E).C.D.t = 'b A(B(E).C.M).t is not equal to the type
'b C.D.t = 'b A(C.M).t
``````

Thus there is an issue with propagating in a timely fashion that `B(E).C.M` is `C.M`.
One easy solution in this specific example is to unnest the recursive module:

``````module rec C: functor(F:Fam) -> sig
type 'b foo = Entry of 'b C(F).D.t
module M : sig
type ('a, 'b) t = ('a * 'b) foo
end
module D : sig type 'b t = 'b A(M).t = | end
end = functor(F:Fam) -> struct
type 'b foo = Entry of 'b C(F).D.t
module M = struct
type ('a, 'b) t = ('a * 'b) foo
end
module D = A(M)
end

module E = struct
type 'b t = { x : int }
end

module N = C(E)
``````

Yes, that works! Thanks.

Is this issue a bug that should be reported, or at least recorded?

I think it might be related to the fact that the inferred signature of a recursive module is strengthened before being compared against the signature given by the user [1]. When doing that outside an applicative functor, this works well. But inside an applicative functor, the full path (with the application) should be used : `B(E).C` instead of `C`.

 It is actually the opposite : the smaller path should be used ?

A smaller (minimal ?) example would be :

``````module F (_: sig end) = struct type t end

module B (_: sig end) = struct
module rec X : sig type t = Entry of F(X).t end =
struct type t = Entry of F(X).t end
end

module CopyB = B (* works *)
module EtaExpB = (functor (Y : sig end) -> B(Y)) (* fails *)
``````

[Edited] Actually it’s more a problem of aliasing and applicativity : the issues does not appear when creating B, but when trying to strengthen its signature (to create `B'`). The signature of `B` is strengthened by the full path `B(Y).` and the type declaration inside X goes from :

``````type t = Entry of F(X).t
``````

to a manifest :

``````type t = B(Y).X.t = Entry of F(B(Y).X).t
``````

which fails at typechecking, because `F(B(Y).X).t` is not considered the same type as `F(X).t`. The types are not equal as `B(Y).X` and `X` are not aliases, because (1) Ocaml disallows aliases using a functor parameter and (2) OCaml disallows aliases on paths with functor applications.

Here, strengthening produces an incorrect signature, which makes the functor unusable in practice. I think can be considered a bug.

For reference, I’ve opened a bug report : Sub-module identities inside an applicative functor are actually generative, leading to invalid signatures · Issue #13173 · ocaml/ocaml · GitHub