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`

.

[Edit] 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 *)
```

[1] (Page 4 of https://caml.inria.fr/pub/papers/xleroy-recursive_modules-03.pdf)

[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.