Comment author: @garrigue

I'm not sure what the issue is.
In

sig type t end with type t = [`T of t]

the last t refers to int, so clearly they do not match.
So I suppose the problem is in the error message ?
For unification errors, we detect name conflicts and print internal ids in that case. This could be helpful here too.
Note that the error message you get with -short-paths is slightly better:

Error: Signature mismatch:
       Modules do not match:
         sig type t = [ `T of t ] end
       is not included in
         sig type t = [ `T of int ] end
       Type declarations do not match:
         type t = [ `T of t ]
       is not included in
         type t = [ `T of t ]

Note that in the signature, t is expanded as int, but not in the type itself.
I think this is due to the fact the definition is not added to the reference environment in the last case; this could be improved.

Comment author: @yallop

Sorry, yes: the problem is in the error message.

Comment author: @garrigue

pr6634.diff is a first attempt at fixing the problem, using the new "type nonrec" keyword.
The current version only works if the original definition is the first one in its recursive group, and gives the following error message:

Error: Signature mismatch:
       Modules do not match:
         sig type t = [ `T of t ] end
       is not included in
         sig type nonrec t = [ `T of t ] end
       Type declarations do not match:
         type t = [ `T of t ]
       is not included in
         type nonrec t = [ `T of t ]

A full(?) solution would put all the changed definitions at the top of the signatures, merging them in a single type nonrec.
Of course, one could be concerned about the noise involved in doing so.

Note, the error is currently (>= 4.08) like this:

Error: Signature mismatch:
       Modules do not match:
         sig type t = [ `T of t ] end
       is not included in
         sig type t = [ `T of t ] end
       Type declarations do not match:
         type t = [ `T of t/2 ]
       is not included in
         type t = [ `T of t/1 ]

This is not ideal, but is a slight improvement.

(I'm assuming that @yallop indeed had the "one part is implicitly nonrec and not the other" issue in mind when opening this issue, so indeed this part of the issue is not resolved: we would like to have a type-declaration printer that knows when to insert nonrec for correctness).

Another fix might be to introduce local type substitutions as needed:

Type declarations do not match:
  type t = [ `T of t ]
is not included in
  type alias := t
  type t = [ `T of alias ]

@Octachron That's actually one of the argument that @yallop gave in his presentation on generalized includes (aka private declarations, aka :=, ...).

I don't think anyone as come up with a complete algorithm for inserting the right aliases ... @yallop ?

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

The error message has improved again:

module M : sig type t end with type t = [`T of t] = struct type t = [`T of t] end;;
Error: Signature mismatch:
       Modules do not match:
         sig type t = [ `T of t ] end
       is not included in
         sig type t = [ `T of t ] end
       Type declarations do not match:
         type t = [ `T of t/2 ]
       is not included in
         type t = [ `T of t/1 ]
       Hint: The type t has been defined multiple times in this toplevel
         session. Some toplevel values still refer to old versions of this
         type. Did you try to redefine them?

This said, this is a case where one would want to see that t/1 is actually int. I would say this is essentially a problem with the way we report module subtyping errors.

But the problem remains that sig type t = [ `T of t ] end is an incorrect signature to print for the signature put by the user. We have to insert a nonrec here otherwise this will remain incorrect and thus confusing.

We can't use nonrec in general because it can't handle cases that have a mixture of recursive and non-recursive references with the same name, like this:

type t

module type S =
sig
  type s
  type t = [`T of t * s]
end with type s := t

Instead we should use signature-local bindings (#2122), like this:

type t

module type S =
sig
  type s := t
  type t = [`T of t * s]
end

If I understand correctly, the idea is that it is unclear how to add these signature-local bindings in general, but that it is a perfect fit for with signature equations (or substitutions). But do we have information in the typedtree to know that the particular signature shape comes from a with?

I would say that this part of the error message is wrong because some occurrences of t are not disambiguated.

       Type declarations do not match:
         type t = [ `T of t/2 ]
       is not included in
         type t = [ `T of t/1 ]

It would be better printed as:

       Type declarations do not match:
         type t/2 = [ `T of t/2 ]
       is not included in
         type t/2 = [ `T of t/1 ]

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

For the input we are discussing

type t = int
module M
  : sig type t end with type t = [`T of t]
  = struct type t = [`T of t] end

The ocamlc error message is as follows:

Error: Signature mismatch:
       Modules do not match:
         sig type t = [ `T of t ] end
       is not included in
         sig type t = [ `T of t ] end
       Type declarations do not match:
         type t = [ `T of t/2 ]
       is not included in
         type t = [ `T of t/1 ]
       The type [ `T of t/1 ] is not equal to the type [ `T of t/2 ]
       Type t/1 = [ `T of t/1 ] is not equal to type t/2 = int 
       Types for tag `T are incompatible

and the toplevel adds, in addition,

       Hint: The type t has been defined multiple times in this toplevel
         session. Some toplevel values still refer to old versions of this
         type. Did you try to redefine them?

It looks like we are getting better thanks to the ongoing error-message work, without doing anything specific for this issue. Not bad.

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

Continuing the tradition of improving the error message in this specific case indirectly, the #11515 PR ensures that the reader will be able to pick up which definition is recursive:

Error: Signature mismatch:
       Modules do not match:
         sig type t = [ `T of t ] end
       is not included in
         sig type t = [ `T of t/2 ] end
       Type declarations do not match:
         type t = [ `T of t ]
       is not included in
         type t = [ `T of t/3 ]
       The type [ `T of t ] is not equal to the type [ `T of t/2 ]
       Type t = [ `T of t ] is not equal to type t/2 = int
       Types for tag `T are incompatible