I usually think of two module types S1 and S2 as being equivalent if the following two functors type check:

module F12 (M : S1) = (M : S2)
module F21 (M : S2) = (M : S1)

And by equivalent, I mean indisinguishable – one should be able to use S1 anywhere one uses S2, and vice versa, with exactly the same type checker and semantic behavior.

However, I found an an example today with two module types that are equivalent, both in my internal mental model of equivalence and in my formal definition that F12 and F21 type check, but that one can distinguish using module type of. Here are the module types:

module type S1 = sig module N : sig type t end type u = N.t end

    module type S2 = sig
      type u
      module N : sig
        type t = u
      end
    end

    module F12 (M : S1) = (M : S2)
    module F21 (M : S2) = (M : S1)

And here is a context that distinguishes them: F1 type checks, but F2 does not:

module F1 (A : S1) = struct
  module F (B : sig type t end) = (B : module type of A.N)
end
module F2 (A : S2) = struct
  module F (B : sig type t end) = (B : module type of A.N)
end

What’s going on is that in F1, module type of A.N decides to abstract t, because it doesn’t have a definition. But in F2, module type of A.N does not abstract t, because it is defined to be u.

Since I thought of S1 and S2 as equivalent, I would have preferred that module type of not abstract t in both cases, and thus that both F1 and F2 be rejected. But I don’t see anything unsound about what OCaml is doing.