Comment author: @garrigue

This is just a fresh instance of the "unprintable signature bug", with the variant that here, there is a way to print it correctly.
Unfortunately, this is not so easy in general.
For instance, consider:

module type S = sig type t module M : sig type u = U of v * t and t and v = u end with type t = t end

In order to print this type correctly, one would have to reorder the definitions, to remove t from its recursive group, and have it come first. This is doable, but not completely trivial. And there is the question of whether we want to do that always, or only when needed (requires some detection code), i.e. avoid to change the apparence of the signature when this is not needed.

So my feeling is that it is doable (move each instantiated definition just before its recursion group, and add a nonrec keyword), but requires a bit of code to do it, and more code if we want to be conservative.

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.

Local substitutions should make this easier. For example, @garrigue's example now has a straightforward solution:

module type S = sig
  type t
  module M : sig
    type t' := t
    type u = U of v * t
     and t = t'
     and v = u
  end
end

as does my original example:

module type S = sig
   type t
   module M : sig
     type t' := t
     type t = t'
   end
end

#6634 seems to be the place where the discussion is happening; so I'm closing this.