Dear Leo, Thank you for the explanation and the illustrating example.


On Mon, Mar 9, 2015 at 4:50 AM, Leo White <leo@lpw25.net> wrote:

>  > 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
>