Dear list,

I apologize in advance as I believe this has been discussed already in some very close forms, such as in the thread "Narrowing a signature with a constrained type" or a few other threads too.  The other examples I've found in the archives I thought were maybe slightly more involving (containing either some type variable, type paramters, an object type, or type variable constraints, etc.).  So in the hope that what I am trying to do might be simpler, here goes:

$ cat > /tmp/a.ml
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

$ ocamlopt /tmp/a.ml
File "/tmp/a.ml", line 8, characters 10-28:
Error: In this `with' constraint, the new definition of t
       does not match its original definition in the constrained signature:
       Type declarations do not match:
         type t = t
       is not included in
         type t = int
       File "/tmp/a.ml", line 2, characters 7-14: Expected declaration
       File "/tmp/a.ml", line 8, characters 17-28: Actual declaration
EXIT STATUS 2

$ ocamlopt -version
4.00.1

In a previous answer from Jacques Garrigue I read that 

> to ensure the coherence of the with constraints, we require that
> the new signature be a subtype of the original one (as a module, not as an object).
> This is where your code gets rejected.

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.

I've used the following workaround [1], however I was just wondering what was the reason behind the rejection.

Thanks,
Mathieu.

[1]
module type S = sig
  type t
  val of_int : int -> t
end

module type A = sig
  type t = int
  include S with type t := t
end

module type B = sig
  type t
  include S with type t := t
end