When defining a functor that takes an abstract module type as input, applications of that functor do not get strengthened after the abstract module type has been resolved to a concrete one. This leads to loss of type sharing (making an applicative functor actually generative).

Here is a minimal example. We start by defining a functor F that takes an abstract module type as input and re-exports it. We build an argument Arg with a concrete module type. Finally, we call the functor twice on the same arguments and get two incompatible types.

module F (Y:sig module type A module X:A end) = Y.X

module Arg = struct
  module type A = sig type t end
  module X : A = struct type t = int end
end

(* Loss of type sharing : *)
module X1 = F(Arg)
module X2 = F(Arg)
let f (x: X1.t) = (x: X2.t) (* error *)

Here, we would expect f to typecheck (because the functor F is applicative).

Interestingly, doing the same thing with a "two_step" approach does not have the same issue. The following code correctly type-checks:

module G(Y:sig module type A end)(X:Y.A) = X

module Arg1 = struct module type A = sig type t end end
module Arg2 = struct type t end

module G_concrete = G(Arg1)
module X1 = G_concrete(Arg2) (* module X1 : sig type t = G_concrete(Arg2).t end *)
module X2 = G_concrete(Arg2) (* module X2 : sig type t = X1.t end *)
let f (x: X1.t) = (x : X2.t) (* ok *)