Use the new structured errors (ocaml#10170) for better error messages

We now produce more detailed error messages during various kinds of
module inclusion, taking advantage of the new structured error trace
generation from ocaml#10170.  Previously, these errors were "shallow",
ending as soon as there was an incompatibility; this patch makes them
"deep", reporting the *reasons* for those problems.  For example,
consider the following module:

    module M : sig
      val x : bool * int
    end = struct
      let x = false , "not an int"
    end

This now produces the following error:

    Error: Signature mismatch:
           Modules do not match:
             sig val x : bool * string end
           is not included in
             sig val x : bool * int end
           Values do not match:
             val x : bool * string
           is not included in
             val x : bool * int
           The type bool * string is not compatible with the type bool * int
           Type string is not compatible with type int

The last two lines are new in this patch.  Previously, the error
message stopped two lines earlier, omitting the key detail that the
reason there is an error is specifically that `string` is not equal to
`int`.

.depend

@@ -689,6 +689,7 @@ typing/includecore.cmo : \
     typing/printtyp.cmi \
     typing/primitive.cmi \
     typing/path.cmi \
+    utils/misc.cmi \
     typing/ident.cmi \
     typing/errortrace.cmi \
     typing/env.cmi \
@@ -704,6 +705,7 @@ typing/includecore.cmx : \
     typing/printtyp.cmx \
     typing/primitive.cmx \
     typing/path.cmx \
+    utils/misc.cmx \
     typing/ident.cmx \
     typing/errortrace.cmx \
     typing/env.cmx \

Changes

@@ -19,6 +19,10 @@ Working version
 - #10328: Give more precise error when disambiguation could not possibly work.
   (Leo White, review by Gabriel Scherer and Florian Angeletti)
 
+- #10407: Produce more detailed error messages that contain full error traces
+  when module inclusion fails.
+  (Antal Spector-Zabusky, NOT YET REVIEWED)
+
 ### Internal/compiler-libs changes:
 
 - #10433: Remove the distinction between 32-bit aligned and 64-bit aligned

testsuite/tests/printing-types/disambiguation.ml

@@ -9,14 +9,16 @@ Error: Type declarations do not match:
          type !'a x = private [> `x ] constraint 'a = 'a x
        is not included in
          type 'a x
-       Their constraints differ.
+       Their parameters differ
+       The type 'b x as 'b is not equal to the type 'a
 |}, Principal{|
 Line 1:
 Error: Type declarations do not match:
          type !'a x = private 'a constraint 'a = [> `x ]
        is not included in
          type 'a x
-       Their constraints differ.
+       Their parameters differ
+       The type [> `x ] is not equal to the type 'a
 |}];;
 
 

testsuite/tests/typing-extensions/extensions.ml

@@ -322,9 +322,9 @@ Error: Signature mismatch:
          type ('a, 'b) bar += A of int
        Constructors do not match:
          A of float
-       is not compatible with:
+       is not the same as:
          A of int
-       The types are not equal.
+       The type float is not equal to the type int
 |}]
 
 module M : sig
@@ -348,9 +348,9 @@ Error: Signature mismatch:
          type ('a, 'b) bar += A of 'a
        Constructors do not match:
          A of 'b
-       is not compatible with:
+       is not the same as:
          A of 'a
-       The types are not equal.
+       The type 'b is not equal to the type 'a
 |}]
 
 module M : sig
@@ -374,9 +374,9 @@ Error: Signature mismatch:
          type ('a, 'b) bar = A of 'a
        Constructors do not match:
          A of 'a
-       is not compatible with:
+       is not the same as:
          A of 'a
-       The types are not equal.
+       The type 'a is not equal to the type 'b
 |}];;
 
 
@@ -401,9 +401,9 @@ Error: Signature mismatch:
          type ('a, 'b) bar += A : 'c -> ('c, 'd) bar
        Constructors do not match:
          A : 'd -> ('c, 'd) bar
-       is not compatible with:
+       is not the same as:
          A : 'c -> ('c, 'd) bar
-       The types are not equal.
+       The type 'd is not equal to the type 'c
 |}]
 
 (* Extensions can be rebound *)

testsuite/tests/typing-extensions/open_types.ml

@@ -117,7 +117,8 @@ Line 1, characters 0-37:
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: This variant or record definition does not match that of type
          ('a, 'a) foo
-       Their constraints differ.
+       Their parameters differ
+       The type 'a is not equal to the type 'b
 |}]
 
 (* Check that signatures can hide exstensibility *)

testsuite/tests/typing-gadts/ambiguity.ml

@@ -233,6 +233,9 @@ Error: Signature mismatch:
          val r : '_weak1 list ref
        is not included in
          val r : T.u list ref
+       The type 'weak1 list ref is not compatible with the type T.u list ref
+       This instance of T.u is ambiguous:
+       it would escape the scope of its equation
 |}]
 
 module M = struct
@@ -264,4 +267,7 @@ Error: Signature mismatch:
          val r : '_weak2 list ref
        is not included in
          val r : T.t list ref
+       The type 'weak2 list ref is not compatible with the type T.t list ref
+       This instance of T.t is ambiguous:
+       it would escape the scope of its equation
 |}]

testsuite/tests/typing-gadts/pr7160.ml

@@ -20,7 +20,8 @@ Lines 4-5, characters 0-77:
 Error: This variant or record definition does not match that of type 'a t
        Constructors do not match:
          Same : 'l t -> 'l t
-       is not compatible with:
+       is not the same as:
          Same : 'l1 t -> 'l2 t
-       The types are not equal.
+       The type 'l t is not equal to the type 'l1 t
+       Type 'l is not equal to type 'l1
 |}];;

testsuite/tests/typing-gadts/pr7378.ml

@@ -21,9 +21,10 @@ Lines 2-3, characters 2-37:
 Error: This variant or record definition does not match that of type X.t
        Constructors do not match:
          A : 'a * 'b * ('a -> unit) -> X.t
-       is not compatible with:
+       is not the same as:
          A : 'a * 'b * ('b -> unit) -> X.t
-       The types are not equal.
+       The type 'a -> unit is not equal to the type 'b -> unit
+       Type 'a is not equal to type 'b
 |}]
 
 (* would segfault

testsuite/tests/typing-misc/deep.ml

@@ -21,6 +21,8 @@ Error: Signature mismatch:
          val x : bool * string
        is not included in
          val x : bool * int
+       The type bool * string is not compatible with the type bool * int
+       Type string is not compatible with type int
 |}]
 
 module T : sig
@@ -42,6 +44,9 @@ Error: Signature mismatch:
          val f : int -> int
        is not included in
          val f : int -> (float * string option) list
+       The type int -> int is not compatible with the type
+         int -> (float * string option) list
+       Type int is not compatible with type (float * string option) list
 |}]
 
 (* Alpha-equivalence *)
@@ -64,6 +69,9 @@ Error: Signature mismatch:
          val f : 'c list * 'd option -> int
        is not included in
          val f : 'a list * 'b list -> int
+       The type 'a list * 'b option -> int is not compatible with the type
+         'a list * 'c list -> int
+       Type 'b option is not compatible with type 'c list
 |}]
 
 module T : sig
@@ -85,4 +93,6 @@ Error: Signature mismatch:
          type t = bool * float
        is not included in
          type t = int * float
+       The type bool * float is not equal to the type int * float
+       Type bool is not equal to type int
 |}]

testsuite/tests/typing-misc/enrich_typedecl.ml

@@ -31,6 +31,7 @@ Error: Signature mismatch:
          type t = A.t = A | B
        is not included in
          type t = int * string
+       The type A.t is not equal to the type int * string
 |}]
 
 module rec B : sig
@@ -62,6 +63,7 @@ Error: Signature mismatch:
          type 'a t = 'a B.t = A of 'a | B
        is not included in
          type 'a t = 'a
+       The type 'a B.t is not equal to the type 'a
 |}];;
 
 module rec C : sig
@@ -126,6 +128,7 @@ Error: Signature mismatch:
          type 'a t = 'a D.t = A of 'a | B
        is not included in
          type 'a t = int
+       The type 'a D.t is not equal to the type int
 |}];;
 
 module rec E : sig
@@ -157,6 +160,7 @@ Error: Signature mismatch:
          type 'a t = 'a E.t = A of 'a | B
        is not included in
          type 'a t = 'a constraint 'a = [> `Foo ]
+       The type 'a is not equal to the type [> `Foo ]
 |}];;
 
 module rec E2 : sig
@@ -188,6 +192,7 @@ Error: Signature mismatch:
          type 'a t = 'a E2.t = A of 'a | B
        is not included in
          type 'a t = [ `Foo ]
+       The type 'a E2.t is not equal to the type [ `Foo ]
 |}];;
 
 module rec E3 : sig
@@ -219,6 +224,7 @@ Error: Signature mismatch:
          type 'a t = 'a E3.t = A of 'a | B
        is not included in
          type 'a t = 'a constraint 'a = [< `Foo ]
+       The type 'a is not equal to the type [< `Foo ]
 |}];;
 
 
@@ -254,7 +260,7 @@ Error: Signature mismatch:
          type ('a, 'b) t = Foo of 'a
        Constructors do not match:
          Foo of 'b
-       is not compatible with:
+       is not the same as:
          Foo of 'a
-       The types are not equal.
+       The type 'b is not equal to the type 'a
 |}];;

testsuite/tests/typing-misc/pr6416.ml

@@ -26,6 +26,8 @@ Error: Signature mismatch:
          val f : t/1 -> unit
        is not included in
          val f : t/2 -> unit
+       The type t/1 -> unit is not compatible with the type t/2 -> unit
+       Type t/1 is not compatible with type t/2
        Line 6, characters 4-14:
          Definition of type t/1
        Line 2, characters 2-12:
@@ -52,9 +54,9 @@ Error: Signature mismatch:
          type u = A of t/2
        Constructors do not match:
          A of t/1
-       is not compatible with:
+       is not the same as:
          A of t/2
-       The types are not equal.
+       The type t/1 is not equal to the type t/2
        Line 4, characters 9-19:
          Definition of type t/1
        Line 2, characters 2-11:
@@ -121,9 +123,9 @@ Error: Signature mismatch:
          type t = A of T/2.t
        Constructors do not match:
          A of T/1.t
-       is not compatible with:
+       is not the same as:
          A of T/2.t
-       The types are not equal.
+       The type T/1.t is not equal to the type T/2.t
        Line 5, characters 6-34:
          Definition of module T/1
        Line 2, characters 2-30:
@@ -150,6 +152,9 @@ Error: Signature mismatch:
          val f : (module s/1) -> t/2 -> t/1
        is not included in
          val f : (module s/2) -> t/2 -> t/2
+       The type (module s/1) -> t/2 -> t/1 is not compatible with the type
+         (module s/2) -> t/2 -> t/2
+       Type (module s/1) is not compatible with type (module s/2)
        Line 5, characters 23-33:
          Definition of type t/1
        Line 3, characters 2-12:
@@ -180,6 +185,9 @@ Error: Signature mismatch:
          val f : a/2 -> 'a -> a/1
        is not included in
          val f : a/2 -> (module a) -> a/2
+       The type a/2 -> (module a) -> a/1 is not compatible with the type
+         a/2 -> (module a) -> a/2
+       Type a/1 is not compatible with type a/2
        Line 5, characters 12-22:
          Definition of type a/1
        Line 3, characters 2-12:
@@ -333,6 +341,7 @@ Error: Signature mismatch:
          type a = M/1.t
        is not included in
          type a = M/2.t
+       The type M/1.t is not equal to the type M/2.t
        Line 2, characters 14-42:
          Definition of module M/1
        File "_none_", line 1:
@@ -366,6 +375,9 @@ Error: Signature mismatch:
          val f : t/2 -> t/3 -> t/4 -> t/1
        is not included in
          val f : t/1 -> t/1 -> t/1 -> t/1
+       The type t/2 -> t/3 -> t/4 -> t/1 is not compatible with the type
+         t/1 -> t/1 -> t/1 -> t/1
+       Type t/2 is not compatible with type t/1
        Line 4, characters 0-10:
          Definition of type t/1
        Line 1, characters 0-10:

testsuite/tests/typing-misc/pr6634.ml

@@ -23,8 +23,10 @@ Error: Signature mismatch:
          type t = [ `T of t/2 ]
        is not included in
          type t = [ `T of t/1 ]
-       Line 1, characters 0-12:
-         Definition of type t/1
+       The type [ `T of t/1 ] is not equal to the type [ `T of t/2 ]
+       Types for tag `T are incompatible
        Line 4, characters 2-20:
+         Definition of type t/1
+       Line 1, characters 0-12:
          Definition of type t/2
 |}]

testsuite/tests/typing-misc/pr7668_bad.ml

@@ -89,4 +89,9 @@ Error: Signature mismatch:
            [> `B of [> `BA | `BB of int list ] | `C of unit ]
        is not included in
          val a : t -> t
+       The type
+         [ `A of int | `B of [ `BA | `BB of unit list ] | `C of unit ] ->
+         [> `B of [> `BA | `BB of int list ] | `C of unit ]
+       is not compatible with the type t -> t
+       Types for tag `BB are incompatible
 |}]

testsuite/tests/typing-misc/records.ml

@@ -197,7 +197,8 @@ Line 1, characters 0-40:
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: This variant or record definition does not match that of type
          (int, [> `A ]) def
-       Their constraints differ.
+       Their parameters differ
+       The type int is not equal to the type 'a
 |}]
 
 type ('a,'b) kind = ('a, 'b) def = A constraint 'b = [> `A];;
@@ -220,7 +221,7 @@ Line 2, characters 0-37:
 Error: This variant or record definition does not match that of type d
        Fields do not match:
          y : int;
-       is not compatible with:
+       is not the same as:
          mutable y : int;
        This is mutable and the original is not.
 |}]
@@ -242,9 +243,9 @@ Line 1, characters 0-31:
 Error: This variant or record definition does not match that of type d
        Fields do not match:
          x : int;
-       is not compatible with:
+       is not the same as:
          x : float;
-       The types are not equal.
+       The type int is not equal to the type float
 |}]
 
 type mono = {foo:int}