> 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