I think this problem is related to the issue 0003674.

Using recursive modules, 
I can define structural types forming non-regular trees.
These types can cause non-termination of the core language type checker
when they are used.

Type checking of G and F is succeed:

module rec G : functor (X:sig type s end) -> 
  sig type s = X.s * X.s type t = [`A of X.s |  `B of G(G(X)).t] end
    = functor (X: sig type s end) -> 
  struct type s = X.s * X.s 
    type t =  [`A of X.s | `B of G(G(X)).t ]
  end

module rec F : functor (X:sig type s end) -> 
  sig type s = X.s * X.s type t = [`A of X.s |  `B of F(F(X)).t] end
    = functor (X: sig type s end) -> 
  struct type s = X.s * X.s 
    type t =  [`A of X.s | `B of F(F(X)).t ]
  end

I can instantiate G and F, thus can define non-regular structural types:

module M = struct type s = int end

module X = G(M)

module Y = F(M)

Type checking of the function f below does not terminate:

let f (x : X.t) : Y.t = x 

When I instantiate G directly without using M,
then I trigger the non-termination earlier:

module Z = G(struct type s = int end)

I suppose that the type checker does attempt to check regularity of the types
for the module Z but not for X.
I do not understand why it behaves differently between X and Z.

Best regards.