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

  1. module F12 (M : S1) = (M : S2)
  2. 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:

  1. module type S1 = sig module N : sig type t end type u = N.t end
  2.  
  3. module type S2 = sig
  4. type u
  5. module N : sig
  6. type t = u
  7. end
  8. end
  9.  
  10. module F12 (M : S1) = (M : S2)
  11. module F21 (M : S2) = (M : S1)

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

  1. module F1 (A : S1) = struct
  2. module F (B : sig type t end) = (B : module type of A.N)
  3. end
  4. module F2 (A : S2) = struct
  5. module F (B : sig type t end) = (B : module type of A.N)
  6. 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.