Recursive module inside functor

Learning
1

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?

2 Likes
2

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)
3

Yes, that works! Thanks.

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

4

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)

1 Like
5

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

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

1 Like
7

Thanks to blement’s analysis, I found another workaround. Changing the functor to generative by adding (), like


module B ( F : Fam) () =

and


module N = B(E)()

fixes the error (at the cost of applicativity).