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