There are many cases where you would like these two modules to be compatible. A simpler use case:
module Hashtbl = struct ... (* definition in the stdlib *) end module ExtHashtbl = struct ... (* my own layer on top of it *) end
I want ExtHashtbl.t compatible with Hashtbl.t , so I can execute ExtHashtbl functions in the middle of the code using Hashtbl.t or work with values that were created by someone who knows only about the Hashtbl library, not about mine own things.
In the theory of ML modules, there is an operation called “strengthening” that enriches the definition of a module with the maximum possible equations by subjecting them to a signature. The idea is that if you want to have more abstraction (less equations), you can always use a type signature to limit it, so there should be more general equations for a more rigorous one.
The situation is slightly different in the case of functors. Note that instead of defining A and B as simple modules, you made them functors on an empty signature:
module A (U : sig end) = struct include M end module B (U : sig end) = struct include M end
There are two different concepts of functors in ML module systems: those that are called "generative" (each call to the functor generates "fresh" types that are incompatible with other calls), and those that are called "applicative" "(all calls to the functor with equal arguments have compatible types.) The OCaml system behaves applicatively if you create an instance with a module argument that is called (in a more general way), and in a generative way if you create an instance with a module argument that is not specified.
You can learn much more than you ever wanted to know about OCaml modular systems in the Xavier Leroy 2000 Modular Modular System (PDF) document (from the Caml Multiple Works webpage). You will also find below code examples for all situations described above.
Recent work on modular ML systems, in particular by Andrei Rosberg, Derek Dreyer, and Claudio Russo, tends to bring a different perspective on the classic distinction between “applicative” and “generative” functors. They argue that they must correspond to “pure” and “unclean” functors: functors whose use performs side effects must always be generative, while functors that bring only pure terms should be applicable by default (with some construction seals for forced incompatibility, thereby providing abstraction).
module type S = sig type t val x : t end;; module M : S = struct type t = int let x = 1 end;; (* definitions below are compatible, the test type-checks *) module A1 = M;; module B1 = M;; let _ = (A1.x = B1.x);; (* definitions below are each independently sealed with an abstract signature, so incompatible; the test doesn't type-check *) module A2 : S = M;; module B2 : S = M;; let _ = (A2.x = B2.x);; (*This expression has type B2.t but an expression was expected of type A2.t*) (* note: if you don't seal Make with the S module type, all functor applications will be transparently equal to M, and all examples below then have compatible types. *) module Make (U : sig end) : S = M;; (* same functor applied to same argument: compatible (applicative behavior) *) module U = struct end;; module A3 = Make(U);; module B3 = Make(U);; let _ = (A3.x = B3.x);; (* same functor applied to different argument: incompatible (applicative behavior) *) module V = struct end;; module A4 = Make(U);; module B4 = Make(V);; let _ = (A4.x = B4.x);; (* This expression has type B4.t = Make(V).t but an expression was expected of type A4.t = Make(U).t *) (* same functor applied to non-path (~unnamed) arguments: incompatible (generative behavior) *) module A5 = Make(struct end);; module B5 = Make(struct end);; let _ = (A5.x = B5.x);; (* This expression has type B5.t but an expression was expected of type A5.t *)