Comment author: @sliquister

I think the problem is Includemod calls Includecore.value_descriptions, which calls Ctype.more_general, which drops the Unify exception and returns a boolean instead.

Comment author: @trefis

Follow-up: since #792 was merged (in 4.06) I believe the example can be reduced to:

module type S = sig
  type ('a, 'b) t
  type 'a key
  val fold :
    ('a, 'b) t -> init:'c -> f:(key:'a key -> data:'b -> 'c -> 'c) -> 'c
end

module M : S with type 'a key = 'a = struct
  type ('a, 'b) t
  type 'a key = 'a
  let fold = assert false
end

type ('a, 'b) t = ('a, 'b) M.t

module Make(Key : sig type t end) = struct
  type nonrec 'a t = (Key.t, 'a) t

  (* roughly equivalent type error at the value level:
    type a type b type c
    let x : (a, b) hashtbl -> init:c -> f:(key:a M.key -> data:b -> c -> c) -> c = assert false
    let y : (a, b) t1 -> init:c -> f:(key:Key.t -> data:b -> c -> c) -> c = assert false
    let _ = if true then x else y
  *)
  include (M : S
           with type ('a, 'b) t := 'a t
           with type 'a key := Key.t)
end

Which gives the following error messages (when running without -short-paths):

File "./a.ml", line 25, characters 11-12:
Error: Signature mismatch:
       ...
       Values do not match:
         val fold :
           ('a, 'b) t ->
           init:'c -> f:(key:'a key -> data:'b -> 'c -> 'c) -> 'c
       is not included in
         val fold :
           'a t -> init:'c -> f:(key:Key.t -> data:'b -> 'c -> 'c) -> 'c
       File "./a.ml", line 4, characters 2-85: Expected declaration
       File "./a.ml", line 4, characters 2-85: Actual declaration

When trying it with #1737 the last two lines become:

       File "./a.ml", line 25, characters 15-93: Expected declaration
       File "./a.ml", line 4, characters 2-85: Actual declaration

While this is very slightly better, it's indeed still fairly confusing.
I agree with sliquister previous message: reusing the trace we get from [moregen] instead of discarding it would probably help matters a lot.

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.

I think the bug is still valid: we should expose the unification trace in case of signature item mismatch. IIRC, the additional information exposed by #9331 should make that easier to achieve.

@Drup could you submit a testsuite PR that contains the current behavior, in a known-misbehavior category or with otherwise a clear indication that this is something we want to improve?

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.

See #10407 for a possible solution to this issue.

There is a label "error-messages", I suggest to assign it to this issue, it will finding all these error message improvements easier:
error-messages

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 current error message has been extended to include the error trace:

         val fold :
           ('a, 'b) t/1 ->
           init:'c -> f:(key:'a key -> data:'b -> 'c -> 'c) -> 'c
       is not included in
         val fold :
           'a t/2 -> init:'c -> f:(key:Key.t -> data:'b -> 'c -> 'c) -> 'c
       The type
         (Key.t, 'a) t/1 ->
         init:'b -> f:(key:Key.t key -> data:'a -> 'b -> 'b) -> 'b
       is not compatible with the type
         'a t/2 -> init:'b -> f:(key:Key.t -> data:'c -> 'b -> 'b) -> 'b
       Type 'a is not compatible with type 'c 

which does point to incompatibility for the type of data. Let's thus close this issue.