Recursive module inside functor

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

1 Like