Ok, that makes sense. I was mislead by this example: Managing functor dependencies - #11 by n4323 which seemed to show that inside the functor, the full argument module is available without constraint.
So my current understanding is: in
module F (X:S) = struct
module M = X
end
the module type of F(X).M is S but no type equalities link M to X. If I want them I have to use an with constraint, or use X inside F unchanged.
My remaining problem actually refers to functor application inside another functor. I’ll try a shortened version:
module F1 (X:S) = struct ... end
module F2 (X:S) = struct module F1_ = F1 (X) ... end
module X_ = struct ... end
module F1_ = F1 (X_)
module F2_ = F2 (X_)
Now I want F2_.F1_ to be compatible with F1_. Somehow the compiler thinks otherwise. What can I do?
(The functors live in different compilation units, so they have signatures explicitly written in .mli files.)
module type s = sig type t val x: t end
module F(X:s) = struct module Y = X end
module F2(X:s) = struct module Z = F(X) end
module X: s = struct
type t = int
let x = 0
end
module FX = F(X)
module F2X = F2(X)
let eq = FX.Y.x = F2X.Z.Y.x
works as expected. The problem is thus in the signature that you have written, they are most probably hiding some type equality. This is the reason why I am generally advising to start by looking at the inferred signature for functors before writing down the explicit interface.
As an illustration, the signature for the above example to allow eq to type would be something like:
module type s = sig type t val x: t end
module F(X:s): sig module Y: s end = struct module Y = X end
module F2(X:s): sig
module Z: sig
module Y: s with type t = F(X).Y.t
end
end = struct
module Z = F(X)
end
But even in this case, the equality between F(X) and F2(X).Z is lost at the module frontier.
Thanks, that’s helpful. Maybe I can get further by looking at inferred functor signatures in the original code.
Dealing with signature constraints feels like a hairy business. For instance, I tried X.x = FX.Y.x in your first, unconstrained example which passes. In the second example it does not. I can see why: applying s makes a fresh type for Y.t. Actually, the inferred signature for FX in the unconstrained example is sig module Y: sig type t = X.t val x: t end end, so the type equality with the input X.t is indeed inferred. To rescue that in a signature I would have to constrain like this: module F(X:s) : sig module Y: s with type t = X.t end
My feeling is that repeating such equalities for each type in (nested sub)modules would not scale well to bigger functors?
[Edit:] Actually, the signature sig module Y: s end with module Y = X for F(X:s) also works. Maybe with module annotations are more scalable.
Ok, I finally got it to compile! Thanks so much to all for your help and considerable patience!
I started by looking at the inferred module interfaces, and then introducing a module signature with a with type trouble = ... constraint for exactly the type trouble that was making problems further down. The mismatching types had exactly the same explicit representation, just derived by different functor applications, which seemed really odd and persuaded me that the problem must be elsewhere.
After poking around, and by luck, I discovered a re-export of the form:
module F (X:S) : sig
module X : S
= struct
module X = X
end
deeper down in the module dependency chain.
I removed the unnecessary re-export for purely esthetic reasons. I then had to replace all uses of the re-export by just the input module. This made my project compile again! Yay!
I now believe that because X: sig type t ... end has an abstract type t, different instantiations of F became incompatible, as t was generated fresh each time. So indeed early answers by @Drup and @octachron contained the answer, it was just difficult to locate the actual place where the error happened.