> module type A = sig type t = int val of_int : int -> t end
>
> module type B = sig type t include A with type t := t end
>
> [...]
>
> In the example, I am not sure what exactly are the signatures involved
> in the comparison, since the included signature does not contain the
> definition of the type t ( removed by the use of := ), and without the
> type [t] the signature are virtually identical.

The two signatures being compared are the signatures before the
definition of t is removed, so essentially:

sig type t = int val of_int : int -> t end

is being compared with:

sig type t = t' val of_int : int -> t end

where t' refers to the type defined by the `type t` definition in the B
signature.

This prevents inconsistent signatures being created. For example,

type t = T of int

module type C = sig type s = int type r = t = T of s end

module type D = C with type s := float

would result in:

module type D = sig type r = t = T of float end

which is inconsistent, since the definition does not match the equation.

Regards,

Leo