diff --git a/.depend b/.depend
index f713e75a2cfb..d7a7c18f3cc3 100644
--- a/.depend
+++ b/.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 \
diff --git a/Changes b/Changes
index 1bfec98d7774..ddf6ffbc6cc0 100644
--- a/Changes
+++ b/Changes
@@ -297,6 +297,10 @@ Working version
 - #10232: Warning for unused record fields.
   (Leo White, review by 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:
 
 - #9243, simplify parser rules for array indexing operations
diff --git a/testsuite/tests/printing-types/disambiguation.ml b/testsuite/tests/printing-types/disambiguation.ml
index e27bba9f88d2..12e244ec5524 100644
--- a/testsuite/tests/printing-types/disambiguation.ml
+++ b/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
 |}];;
 
 
diff --git a/testsuite/tests/typing-extensions/extensions.ml b/testsuite/tests/typing-extensions/extensions.ml
index 259712b21b57..beea8d031c54 100644
--- a/testsuite/tests/typing-extensions/extensions.ml
+++ b/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 *)
diff --git a/testsuite/tests/typing-extensions/open_types.ml b/testsuite/tests/typing-extensions/open_types.ml
index 210254418b84..3b44fe23f32c 100644
--- a/testsuite/tests/typing-extensions/open_types.ml
+++ b/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 *)
diff --git a/testsuite/tests/typing-gadts/ambiguity.ml b/testsuite/tests/typing-gadts/ambiguity.ml
index d43f33841a4a..7f023f845a3f 100644
--- a/testsuite/tests/typing-gadts/ambiguity.ml
+++ b/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
 |}]
diff --git a/testsuite/tests/typing-gadts/pr7160.ml b/testsuite/tests/typing-gadts/pr7160.ml
index a615a462821c..5a613052b805 100644
--- a/testsuite/tests/typing-gadts/pr7160.ml
+++ b/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
 |}];;
diff --git a/testsuite/tests/typing-gadts/pr7378.ml b/testsuite/tests/typing-gadts/pr7378.ml
index 9252b43ddbc0..fe771d8d0ad9 100644
--- a/testsuite/tests/typing-gadts/pr7378.ml
+++ b/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
diff --git a/testsuite/tests/typing-misc/deep.ml b/testsuite/tests/typing-misc/deep.ml
index 883e44b68364..01ade06106a9 100644
--- a/testsuite/tests/typing-misc/deep.ml
+++ b/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
 |}]
diff --git a/testsuite/tests/typing-misc/enrich_typedecl.ml b/testsuite/tests/typing-misc/enrich_typedecl.ml
index 295cab1ef287..c6087a9dc716 100644
--- a/testsuite/tests/typing-misc/enrich_typedecl.ml
+++ b/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
 |}];;
diff --git a/testsuite/tests/typing-misc/pr6416.ml b/testsuite/tests/typing-misc/pr6416.ml
index 7464356b6dbf..69ee3422c0b9 100644
--- a/testsuite/tests/typing-misc/pr6416.ml
+++ b/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:
diff --git a/testsuite/tests/typing-misc/pr6634.ml b/testsuite/tests/typing-misc/pr6634.ml
index 3e1daa8218e7..6e0b08d4bdb9 100644
--- a/testsuite/tests/typing-misc/pr6634.ml
+++ b/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
 |}]
diff --git a/testsuite/tests/typing-misc/pr7668_bad.ml b/testsuite/tests/typing-misc/pr7668_bad.ml
index 95b64fb50425..06ad53d1277e 100644
--- a/testsuite/tests/typing-misc/pr7668_bad.ml
+++ b/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
 |}]
diff --git a/testsuite/tests/typing-misc/records.ml b/testsuite/tests/typing-misc/records.ml
index 51623ef2cf5d..9c2c83f96ee7 100644
--- a/testsuite/tests/typing-misc/records.ml
+++ b/testsuite/tests/typing-misc/records.ml
@@ -198,7 +198,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];;
@@ -221,7 +222,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.
 |}]
@@ -243,9 +244,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 unboxed = d = {x:float} [@@unboxed]
diff --git a/testsuite/tests/typing-misc/variant.ml b/testsuite/tests/typing-misc/variant.ml
index d8356cd819e0..8bb51375427a 100644
--- a/testsuite/tests/typing-misc/variant.ml
+++ b/testsuite/tests/typing-misc/variant.ml
@@ -25,6 +25,7 @@ Error: Signature mismatch:
          type t = X.t = A | B
        is not included in
          type t = int * bool
+       The type X.t is not equal to the type int * bool
 |}];;
 
 
@@ -65,7 +66,8 @@ Line 1, characters 0-41:
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 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:int} constraint 'b = [> `A];;
@@ -98,9 +100,9 @@ Line 1, characters 0-32:
 Error: This variant or record definition does not match that of type d
        Constructors do not match:
          X of int
-       is not compatible with:
+       is not the same as:
          X of float
-       The types are not equal.
+       The type int is not equal to the type float
 |}]
 
 type unboxed = d = X of float [@@unboxed]
@@ -143,7 +145,7 @@ Error: Signature mismatch:
          type t = Foo of int
        Constructors do not match:
          Foo : int -> t
-       is not compatible with:
+       is not the same as:
          Foo of int
        The first has explicit return type and the second doesn't.
 |}]
diff --git a/testsuite/tests/typing-modules-bugs/pr7414_2_bad.compilers.reference b/testsuite/tests/typing-modules-bugs/pr7414_2_bad.compilers.reference
index 141621af49c7..c2a565288d63 100644
--- a/testsuite/tests/typing-modules-bugs/pr7414_2_bad.compilers.reference
+++ b/testsuite/tests/typing-modules-bugs/pr7414_2_bad.compilers.reference
@@ -12,5 +12,8 @@ Error: Modules do not match:
        val r : '_weak1 list ref ref
      is not included in
        val r : Choice.t list ref ref
+     The type 'weak1 list ref ref is not compatible with the type
+       Choice.t list ref ref
+     The type constructor Choice.t would escape its scope
      File "pr7414_2_bad.ml", line 29, characters 2-31: Expected declaration
      File "pr7414_2_bad.ml", line 40, characters 8-9: Actual declaration
diff --git a/testsuite/tests/typing-modules-bugs/pr7414_bad.compilers.reference b/testsuite/tests/typing-modules-bugs/pr7414_bad.compilers.reference
index 35ccca760d4f..4677c3702ad9 100644
--- a/testsuite/tests/typing-modules-bugs/pr7414_bad.compilers.reference
+++ b/testsuite/tests/typing-modules-bugs/pr7414_bad.compilers.reference
@@ -12,5 +12,8 @@ Error: Modules do not match:
        val r : '_weak1 list ref ref
      is not included in
        val r : Choice.t list ref ref
+     The type 'weak1 list ref ref is not compatible with the type
+       Choice.t list ref ref
+     The type constructor Choice.t would escape its scope
      File "pr7414_bad.ml", line 38, characters 2-31: Expected declaration
      File "pr7414_bad.ml", line 33, characters 6-7: Actual declaration
diff --git a/testsuite/tests/typing-modules/Test.ml b/testsuite/tests/typing-modules/Test.ml
index 6287a6e6f605..f87fa521d158 100644
--- a/testsuite/tests/typing-modules/Test.ml
+++ b/testsuite/tests/typing-modules/Test.ml
@@ -97,9 +97,9 @@ Line 3, characters 23-33:
 Error: This variant or record definition does not match that of type u
        Constructors do not match:
          X of bool
-       is not compatible with:
+       is not the same as:
          X of int
-       The types are not equal.
+       The type bool is not equal to the type int
 |}];;
 
 (* PR#5815 *)
@@ -147,7 +147,7 @@ Error: Signature mismatch:
          type t += E
        Constructors do not match:
          E of int
-       is not compatible with:
+       is not the same as:
          E
        They have different arities.
 |}];;
@@ -168,9 +168,9 @@ Error: Signature mismatch:
          type t += E of char
        Constructors do not match:
          E of int
-       is not compatible with:
+       is not the same as:
          E of char
-       The types are not equal.
+       The type int is not equal to the type char
 |}];;
 
 module M : sig type t += C of int end = struct type t += E of int end;;
@@ -207,7 +207,7 @@ Error: Signature mismatch:
          type t += E of { x : int; }
        Constructors do not match:
          E of int
-       is not compatible with:
+       is not the same as:
          E of { x : int; }
        The second uses inline records and the first doesn't.
 |}];;
diff --git a/testsuite/tests/typing-modules/applicative_functor_type.ml b/testsuite/tests/typing-modules/applicative_functor_type.ml
index a9e79b33d1e3..01c6127490bd 100644
--- a/testsuite/tests/typing-modules/applicative_functor_type.ml
+++ b/testsuite/tests/typing-modules/applicative_functor_type.ml
@@ -48,6 +48,7 @@ Error: Modules do not match:
        val equal : 'a -> 'a -> bool
      is not included in
        val equal : unit
+     The type 'a -> 'a -> bool is not compatible with the type unit
 |} ]
 
 
diff --git a/testsuite/tests/typing-modules/extension_constructors_errors_test.ml b/testsuite/tests/typing-modules/extension_constructors_errors_test.ml
index 0985084ac358..9cf39a750c13 100644
--- a/testsuite/tests/typing-modules/extension_constructors_errors_test.ml
+++ b/testsuite/tests/typing-modules/extension_constructors_errors_test.ml
@@ -21,7 +21,7 @@ Error: Signature mismatch:
          type t += F
        Constructors do not match:
          F of int
-       is not compatible with:
+       is not the same as:
          F
        They have different arities.
 |}];;
diff --git a/testsuite/tests/typing-modules/functors.ml b/testsuite/tests/typing-modules/functors.ml
index 9319829018a3..1459c66a08b5 100644
--- a/testsuite/tests/typing-modules/functors.ml
+++ b/testsuite/tests/typing-modules/functors.ml
@@ -1617,11 +1617,9 @@ Error: The functor application is ill-typed.
             type t = Y of X.t
           Constructors do not match:
             Y of int
-          is not compatible with:
+          is not the same as:
             Y of X.t
-          The types are not equal.
-          Line 5, characters 0-32:
-            Definition of module X/1
+          The type int is not equal to the type X.t
        4. Modules do not match:
             Z : sig type t = Z.t = Z of int end
           is not included in
@@ -1632,9 +1630,9 @@ Error: The functor application is ill-typed.
             type t = Z of X.t
           Constructors do not match:
             Z of int
-          is not compatible with:
+          is not the same as:
             Z of X.t
-          The types are not equal.
+          The type int is not equal to the type X.t
 |}]
 
 (** Final state in the presence of extensions
diff --git a/testsuite/tests/typing-modules/inclusion_errors.ml b/testsuite/tests/typing-modules/inclusion_errors.ml
index d8296ae1b9cc..138a49e33e25 100644
--- a/testsuite/tests/typing-modules/inclusion_errors.ml
+++ b/testsuite/tests/typing-modules/inclusion_errors.ml
@@ -23,6 +23,8 @@ Error: Signature mismatch:
          type ('a, 'b) t = 'a * 'a
        is not included in
          type ('a, 'b) t = 'a * 'b
+       The type 'a * 'a is not equal to the type 'a * 'b
+       Type 'a is not equal to type 'b
 |}];;
 
 module M : sig
@@ -44,6 +46,8 @@ Error: Signature mismatch:
          type ('a, 'b) t = 'a * 'b
        is not included in
          type ('a, 'b) t = 'a * 'a
+       The type 'a * 'b is not equal to the type 'a * 'a
+       Type 'b is not equal to type 'a
 |}];;
 
 type 'a x
@@ -67,6 +71,9 @@ Error: Signature mismatch:
          type ('b, 'c, 'a) t = ('b * 'c * 'a * 'c * 'a) x
        is not included in
          type ('a, 'b, 'c) t = ('a * 'b * 'c * 'b * 'a) x
+       The type ('b * 'c * 'a * 'c * 'a) x is not equal to the type
+         ('b * 'c * 'a * 'c * 'b) x
+       Type 'a is not equal to type 'b
 |}]
 
 module M : sig
@@ -88,6 +95,11 @@ Error: Signature mismatch:
          type t = < m : 'a. 'a * ('a * 'b) > as 'b
        is not included in
          type t = < m : 'b. 'b * ('b * < m : 'c. 'c * 'a > as 'a) >
+       The type < m : 'a. 'a * ('a * 'd) > as 'd is not equal to the type
+         < m : 'b. 'b * ('b * < m : 'c. 'c * 'e > as 'e) >
+       The method m has type 'a. 'a * ('a * < m : 'a. 'b >) as 'b,
+       but the expected method type was 'c. 'c * ('b * < m : 'c. 'a >) as 'a
+       The universal variable 'b would escape its scope
 |}];;
 
 type s = private < m : int; .. >;;
@@ -114,6 +126,8 @@ Error: Signature mismatch:
          type t = < m : int >
        is not included in
          type t = s
+       The type < m : int > is not equal to the type s
+       The second object type has an abstract row, it cannot be closed
 |}];;
 
 module M : sig
@@ -135,6 +149,8 @@ Error: Signature mismatch:
          type t = s
        is not included in
          type t = < m : int >
+       The type s is not equal to the type < m : int >
+       The first object type has an abstract row, it cannot be closed
 |}];;
 
 module M : sig
@@ -161,9 +177,9 @@ Error: Signature mismatch:
          type t = Foo of int * float
        Constructors do not match:
          Foo of (int * int) * float
-       is not compatible with:
+       is not the same as:
          Foo of int * float
-       The types are not equal.
+       The type int * int is not equal to the type int
 |}];;
 
 module M : sig
@@ -185,6 +201,7 @@ Error: Signature mismatch:
          type t = int * float * int
        is not included in
          type t = int * float
+       The type int * float * int is not equal to the type int * float
 |}];;
 
 module M : sig
@@ -206,6 +223,9 @@ Error: Signature mismatch:
          type t = < f : float; n : int >
        is not included in
          type t = < m : float; n : int >
+       The type < f : float; n : int > is not equal to the type
+         < m : float; n : int >
+       The second object type has no method f
 |}];;
 
 module M : sig
@@ -227,6 +247,8 @@ Error: Signature mismatch:
          type t = < n : int >
        is not included in
          type t = < m : float; n : int >
+       The type < n : int > is not equal to the type < m : float; n : int >
+       The first object type has no method m
 |}];;
 
 module M4 : sig
@@ -248,6 +270,9 @@ Error: Signature mismatch:
          type t = < m : int; n : int >
        is not included in
          type t = < m : float * int; n : int >
+       The type < m : int; n : int > is not equal to the type
+         < m : float * int; n : int >
+       Types for method m are incompatible
 |}];;
 
 module M4 : sig
@@ -274,9 +299,11 @@ Error: Signature mismatch:
          type t = Foo of [ `Bar of string | `Foo of string ]
        Constructors do not match:
          Foo of [ `Bar of string ]
-       is not compatible with:
+       is not the same as:
          Foo of [ `Bar of string | `Foo of string ]
-       The types are not equal.
+       The type [ `Bar of string ] is not equal to the type
+         [ `Bar of string | `Foo of string ]
+       The first variant type does not allow tag(s) `Foo
 |}];;
 
 module M : sig
@@ -298,6 +325,8 @@ Error: Signature mismatch:
          type t = private [ `C ]
        is not included in
          type t = private [ `C of int ]
+       The type [ `C ] is not equal to the type [ `C of int ]
+       Types for tag `C are incompatible
 |}];;
 
 module M : sig
@@ -319,6 +348,8 @@ Error: Signature mismatch:
          type t = private [ `C of int ]
        is not included in
          type t = private [ `C ]
+       The type [ `C of int ] is not equal to the type [ `C ]
+       Types for tag `C are incompatible
 |}];;
 
 module M : sig
@@ -349,6 +380,8 @@ Error: Signature mismatch:
          type t = private [ `A of int ]
        is not included in
          type t = private [> `A of int ]
+       The type [ `A of int ] is not equal to the type [> `A of int ]
+       The second variant type is open and the first is not
 |}];;
 
 module M : sig
@@ -370,6 +403,8 @@ Error: Signature mismatch:
          type t = private [> `A of int ]
        is not included in
          type t = private [ `A of int ]
+       The type [> `A of int ] is not equal to the type [ `A of int ]
+       The first variant type is open and the second is not
 |}];;
 
 module M : sig
@@ -391,6 +426,9 @@ Error: Signature mismatch:
          type 'a t = 'a constraint 'a = [> `A of int ]
        is not included in
          type 'a t = 'a constraint 'a = [> `A of int | `B of int ]
+       The type [> `A of int ] is not equal to the type
+         [> `A of int | `B of int ]
+       The first variant type does not allow tag(s) `B
 |}];;
 
 module M : sig
@@ -412,6 +450,9 @@ Error: Signature mismatch:
          type 'a t = 'a constraint 'a = [> `A of int | `C of float ]
        is not included in
          type 'a t = 'a constraint 'a = [> `A of int ]
+       The type [> `A of int | `C of float ] is not equal to the type
+         [> `A of int ]
+       The second variant type does not allow tag(s) `C
 |}];;
 
 module M : sig
@@ -442,6 +483,7 @@ Error: Signature mismatch:
          type t = private [< `C of int & float ]
        is not included in
          type t = private [< `C ]
+       Types for tag `C are incompatible
 |}];;
 
 (********************************** Moregen ***********************************)
@@ -484,6 +526,9 @@ Error: Modules do not match:
        val r : '_weak1 list ref ref
      is not included in
        val r : Choice.t list ref ref
+     The type 'weak1 list ref ref is not compatible with the type
+       Choice.t list ref ref
+     The type constructor Choice.t would escape its scope
 |}];;
 
 module O = struct
@@ -510,6 +555,9 @@ Error: Signature mismatch:
          val f : (module s/1) -> unit
        is not included in
          val f : (module s/2) -> unit
+       The type (module s/1) -> unit is not compatible with the type
+         (module s/2) -> unit
+       Type (module s/1) is not compatible with type (module s/2)
        Line 6, characters 4-17:
          Definition of module type s/1
        Line 2, characters 2-15:
@@ -535,6 +583,12 @@ Error: Signature mismatch:
          val f : (< m : 'a. 'a * 'b > as 'b) -> unit
        is not included in
          val f : < m : 'b. 'b * < m : 'c. 'c * 'a > as 'a > -> unit
+       The type (< m : 'a. 'a * 'd > as 'd) -> unit
+       is not compatible with the type
+         < m : 'b. 'b * < m : 'c. 'c * 'e > as 'e > -> unit
+       The method m has type 'a. 'a * < m : 'a. 'b > as 'b,
+       but the expected method type was 'c. 'c * ('b * < m : 'c. 'a >) as 'a
+       The universal variable 'b would escape its scope
 |}];;
 
 type s = private < m : int; .. >;;
@@ -559,6 +613,9 @@ Error: Signature mismatch:
          val f : < m : int > -> < m : int >
        is not included in
          val f : s -> s
+       The type < m : int > -> < m : int > is not compatible with the type
+         s -> s
+       The second object type has an abstract row, it cannot be closed
 |}];;
 
 module M : sig
@@ -580,6 +637,8 @@ Error: Signature mismatch:
          val f : 'b -> int
        is not included in
          val f : 'a -> float
+       The type 'a -> int is not compatible with the type 'a -> float
+       Type int is not compatible with type float
 |}]
 
 module M : sig
@@ -601,6 +660,8 @@ Error: Signature mismatch:
          val x : '_weak2 list ref
        is not included in
          val x : 'a list ref
+       The type 'weak2 list ref is not compatible with the type 'a list ref
+       Type 'weak2 is not compatible with type 'a
 |}];;
 
 module M = struct let r = ref [] end;;
@@ -621,6 +682,8 @@ Error: Signature mismatch:
          val r : '_weak3 list ref
        is not included in
          val r : t list ref
+       The type 'weak3 list ref is not compatible with the type t list ref
+       The type constructor t would escape its scope
 |}];;
 
 type (_, _) eq = Refl : ('a, 'a) eq;;
@@ -662,6 +725,9 @@ Error: Signature mismatch:
          val r : '_weak4 list ref
        is not included in
          val r : T.s list ref
+       The type 'weak4 list ref is not compatible with the type T.s list ref
+       This instance of T.s is ambiguous:
+       it would escape the scope of its equation
 |}];;
 
 module M: sig
@@ -683,6 +749,8 @@ Error: Signature mismatch:
          val f : 'a -> 'a
        is not included in
          val f : int -> float
+       The type int -> int is not compatible with the type int -> float
+       Type int is not compatible with type float
 |}];;
 
 module M: sig
@@ -704,6 +772,9 @@ Error: Signature mismatch:
          val f : int * int -> int * int
        is not included in
          val f : int * float * int -> int -> int
+       The type int * int -> int * int is not compatible with the type
+         int * float * int -> int -> int
+       Type int * int is not compatible with type int * float * int
 |}];;
 
 module M: sig
@@ -725,6 +796,10 @@ Error: Signature mismatch:
          val f : < f : float; m : int > -> < f : float; m : int >
        is not included in
          val f : < m : int; n : float > -> < m : int; n : float >
+       The type < f : float; m : int > -> < f : float; m : int >
+       is not compatible with the type
+         < m : int; n : float > -> < m : int; n : float >
+       The second object type has no method f
 |}];;
 
 module M : sig
@@ -746,6 +821,9 @@ Error: Signature mismatch:
          val f : [ `Bar | `Foo ] -> unit
        is not included in
          val f : [ `Foo ] -> unit
+       The type [ `Bar | `Foo ] -> unit is not compatible with the type
+         [ `Foo ] -> unit
+       The second variant type does not allow tag(s) `Bar
 |}];;
 
 module M : sig
@@ -767,6 +845,9 @@ Error: Signature mismatch:
          val f : [< `Foo ] -> unit
        is not included in
          val f : [> `Foo ] -> unit
+       The type [< `Foo ] -> unit is not compatible with the type
+         [> `Foo ] -> unit
+       The second variant type is open and the first is not
 |}];;
 
 module M : sig
@@ -788,6 +869,9 @@ Error: Signature mismatch:
          val f : [< `Foo ] -> unit
        is not included in
          val f : [< `Bar | `Foo ] -> unit
+       The type [< `Foo ] -> unit is not compatible with the type
+         [< `Bar | `Foo ] -> unit
+       The first variant type does not allow tag(s) `Bar
 |}];;
 
 module M : sig
@@ -809,6 +893,9 @@ Error: Signature mismatch:
          val f : < m : 'a. [< `Foo ] as 'a > -> unit
        is not included in
          val f : < m : [< `Foo ] > -> unit
+       The type < m : 'a. [< `Foo ] as 'a > -> unit
+       is not compatible with the type < m : [< `Foo ] > -> unit
+       Types for method m are incompatible
 |}];;
 
 module M : sig
@@ -830,6 +917,9 @@ Error: Signature mismatch:
          val f : < m : [ `Foo ] > -> unit
        is not included in
          val f : < m : 'a. [< `Foo ] as 'a > -> unit
+       The type < m : [ `Foo ] > -> unit is not compatible with the type
+         < m : 'a. [< `Foo ] as 'a > -> unit
+       Types for method m are incompatible
 |}];;
 
 module M : sig
@@ -851,6 +941,9 @@ Error: Signature mismatch:
          val f : [< `C of int & float ] -> unit
        is not included in
          val f : [< `C ] -> unit
+       The type [< `C of & int & float ] -> unit
+       is not compatible with the type [< `C ] -> unit
+       Types for tag `C are incompatible
 |}];;
 
 module M : sig
@@ -872,6 +965,9 @@ Error: Signature mismatch:
          val f : [ `Foo of int ] -> unit
        is not included in
          val f : [ `Foo ] -> unit
+       The type [ `Foo of int ] -> unit is not compatible with the type
+         [ `Foo ] -> unit
+       Types for tag `Foo are incompatible
 |}];;
 
 module M : sig
@@ -893,6 +989,9 @@ Error: Signature mismatch:
          val f : [ `Foo ] -> unit
        is not included in
          val f : [ `Foo of int ] -> unit
+       The type [ `Foo ] -> unit is not compatible with the type
+         [ `Foo of int ] -> unit
+       Types for tag `Foo are incompatible
 |}];;
 
 module M : sig
@@ -923,6 +1022,10 @@ Error: Signature mismatch:
          val f : [> `Bar | `Foo ] -> unit
        is not included in
          val f : [< `Bar | `Baz | `Foo ] -> unit
+       The type [> `Bar | `Foo ] -> unit is not compatible with the type
+         [< `Bar | `Baz | `Foo ] -> unit
+       The tag `Foo is guaranteed to be present in the first variant type,
+       but not in the second
 |}];;
 
 (******************************* Type manifests *******************************)
@@ -946,6 +1049,7 @@ Error: Signature mismatch:
          type t = [ `C ]
        is not included in
          type t = private [< `A | `B ]
+       The constructor C is only present in the second declaration.
 |}];;
 
 module M : sig
@@ -967,6 +1071,7 @@ Error: Signature mismatch:
          type t = private [> `A ]
        is not included in
          type t = private [< `A | `B ]
+       The second is private and closed, but the first is not closed
 |}];;
 
 module M : sig
@@ -988,6 +1093,7 @@ Error: Signature mismatch:
          type t = [ `B ]
        is not included in
          type t = private [< `A | `B > `A ]
+       The constructor A is only present in the first declaration.
 |}];;
 
 module M : sig
@@ -1009,6 +1115,7 @@ Error: Signature mismatch:
          type t = [ `A ]
        is not included in
          type t = private [> `A of int ]
+       Types for tag `A are incompatible
 |}];;
 
 module M : sig
@@ -1030,6 +1137,7 @@ Error: Signature mismatch:
          type t = private [< `A of & int ]
        is not included in
          type t = private [< `A of int ]
+       Types for tag `A are incompatible
 |}];;
 
 
@@ -1052,6 +1160,7 @@ Error: Signature mismatch:
          type t = private [< `A ]
        is not included in
          type t = private [< `A of int ]
+       Types for tag `A are incompatible
 |}];;
 
 
@@ -1074,6 +1183,7 @@ Error: Signature mismatch:
          type t = private [< `A ]
        is not included in
          type t = private [< `A of int & float ]
+       Types for tag `A are incompatible
 |}];;
 
 module M : sig
@@ -1095,6 +1205,7 @@ Error: Signature mismatch:
          type t = [ `A of float ]
        is not included in
          type t = private [> `A of int ]
+       The type float is not equal to the type int
 |}];;
 
 module M : sig
@@ -1116,6 +1227,9 @@ Error: Signature mismatch:
          type t = private [ `A | `B ]
        is not included in
          type t = private [< `A | `B ]
+       The type [ `A | `B ] is not equal to the type [< `A | `B ]
+       The tag `B is guaranteed to be present in the first variant type,
+       but not in the second
 |}];;
 
 module M : sig
@@ -1159,6 +1273,8 @@ Error: Signature mismatch:
          type t = private [< `A | `B ]
        is not included in
          type t = private [< `A | `B > `B ]
+       The tag `B is present in the the second declaration,
+       but might not be in the the first
 |}];;
 
 module M : sig
@@ -1180,6 +1296,7 @@ Error: Signature mismatch:
          type t = < b : int >
        is not included in
          type t = private < a : int; .. >
+       The implementation is missing the method a
 |}];;
 
 module M : sig
@@ -1201,6 +1318,8 @@ Error: Signature mismatch:
          type t = < a : int >
        is not included in
          type t = private < a : float; .. >
+       The type int is not equal to the type float
+       Type int is not equal to type float
 |}];;
 
 type w = private float
@@ -1228,6 +1347,8 @@ Error: Signature mismatch:
          type t = private u
        is not included in
          type t = private int * (int * int)
+       The type int * q is not equal to the type int * (int * int)
+       Type q is not equal to type int * int
 |}];;
 
 type w = float
@@ -1255,6 +1376,8 @@ Error: Signature mismatch:
          type t = private u
        is not included in
          type t = private int * (int * int)
+       The type int * q is not equal to the type int * (int * int)
+       Type w is not equal to type int
 |}];;
 
 type s = private int
@@ -1279,6 +1402,7 @@ Error: Signature mismatch:
          type t = private s
        is not included in
          type t = private float
+       The type int is not equal to the type float
 |}];;
 
 module M : sig
diff --git a/testsuite/tests/typing-modules/module_type_substitution.ml b/testsuite/tests/typing-modules/module_type_substitution.ml
index d4a68a3267ec..2bcd706d222d 100644
--- a/testsuite/tests/typing-modules/module_type_substitution.ml
+++ b/testsuite/tests/typing-modules/module_type_substitution.ml
@@ -149,9 +149,9 @@ Error: In this `with' constraint, the new definition of t
          type t = X of int | Y of float
        Constructors do not match:
          X of x
-       is not compatible with:
+       is not the same as:
          X of int
-       The types are not equal.
+       The type x is not equal to the type int
 |}]
 
 (** First class module types require an identity *)
diff --git a/testsuite/tests/typing-modules/nondep_private_abbrev.ml b/testsuite/tests/typing-modules/nondep_private_abbrev.ml
index 9b31538f4e82..a0daa1fb95ee 100644
--- a/testsuite/tests/typing-modules/nondep_private_abbrev.ml
+++ b/testsuite/tests/typing-modules/nondep_private_abbrev.ml
@@ -125,6 +125,9 @@ Error: Signature mismatch:
          type s = t
        is not included in
          type s = private [ `Bar of int | `Foo of 'a -> int ] as 'a
+       The type [ `Bar of int | `Foo of t -> int ] is not equal to the type
+         [ `Bar of int | `Foo of 'a -> int ] as 'a
+       Types for tag `Foo are incompatible
 |}]
 
 (* nondep_type_decl + nondep_type_rec *)
diff --git a/testsuite/tests/typing-modules/pr10399.ml b/testsuite/tests/typing-modules/pr10399.ml
index 0e376da8401f..cce02f41a213 100644
--- a/testsuite/tests/typing-modules/pr10399.ml
+++ b/testsuite/tests/typing-modules/pr10399.ml
@@ -41,4 +41,6 @@ Error: Signature mismatch:
            val o : t
          end
        Values do not match: val o : c is not included in val o : t
+       The type c is not compatible with the type t
+       The second object type has no method y
 |}]
diff --git a/testsuite/tests/typing-modules/pr6394.ml b/testsuite/tests/typing-modules/pr6394.ml
index 97bbeebf1ecd..d785fb50651a 100644
--- a/testsuite/tests/typing-modules/pr6394.ml
+++ b/testsuite/tests/typing-modules/pr6394.ml
@@ -24,4 +24,5 @@ Error: Signature mismatch:
          type t = X.t = A | B
        is not included in
          type t = int * bool
+       The type X.t is not equal to the type int * bool
 |}];;
diff --git a/testsuite/tests/typing-modules/pr7818.ml b/testsuite/tests/typing-modules/pr7818.ml
index 84f7d8f702f1..834b8ccae084 100644
--- a/testsuite/tests/typing-modules/pr7818.ml
+++ b/testsuite/tests/typing-modules/pr7818.ml
@@ -323,7 +323,9 @@ Line 15, characters 0-69:
 Error: This variant or record definition does not match that of type M.t
        Constructors do not match:
          E of (MkT(M.T).t, MkT(M.T).t) eq
-       is not compatible with:
+       is not the same as:
          E of (MkT(Desc).t, MkT(Desc).t) eq
-       The types are not equal.
+       The type (MkT(M.T).t, MkT(M.T).t) eq is not equal to the type
+         (MkT(Desc).t, MkT(Desc).t) eq
+       Type MkT(M.T).t is not equal to type MkT(Desc).t
 |}]
diff --git a/testsuite/tests/typing-modules/pr7851.ml b/testsuite/tests/typing-modules/pr7851.ml
index bcd3281bedca..96719d2dc1fe 100644
--- a/testsuite/tests/typing-modules/pr7851.ml
+++ b/testsuite/tests/typing-modules/pr7851.ml
@@ -29,9 +29,9 @@ Line 1, characters 0-58:
 Error: This variant or record definition does not match that of type M1.t
        Constructors do not match:
          E of M1.x
-       is not compatible with:
+       is not the same as:
          E of M1.y
-       The types are not equal.
+       The type M1.x is not equal to the type M1.y
 |}]
 
 let bool_of_int x =
@@ -81,7 +81,8 @@ Line 1, characters 0-58:
 Error: This variant or record definition does not match that of type M1.t
        Constructors do not match:
          E of (M1.x, M1.x) eq
-       is not compatible with:
+       is not the same as:
          E of (M1.x, M1.y) eq
-       The types are not equal.
+       The type (M1.x, M1.x) eq is not equal to the type (M1.x, M1.y) eq
+       Type M1.x is not equal to type M1.y
 |}]
diff --git a/testsuite/tests/typing-modules/records_errors_test.ml b/testsuite/tests/typing-modules/records_errors_test.ml
index f85c1e7db9b1..f0b015b5cb16 100644
--- a/testsuite/tests/typing-modules/records_errors_test.ml
+++ b/testsuite/tests/typing-modules/records_errors_test.ml
@@ -42,9 +42,11 @@ Error: Signature mismatch:
          }
        Fields do not match:
          f0 : unit * unit * unit * float * unit * unit * unit;
-       is not compatible with:
+       is not the same as:
          f0 : unit * unit * unit * int * unit * unit * unit;
-       The types are not equal.
+       The type unit * unit * unit * float * unit * unit * unit
+       is not equal to the type unit * unit * unit * int * unit * unit * unit
+       Type float is not equal to type int
 |}];;
 
 
@@ -88,7 +90,7 @@ Error: Signature mismatch:
          }
        Fields do not match:
          f0 : unit * unit * unit * float * unit * unit * unit;
-       is not compatible with:
+       is not the same as:
          mutable f0 : unit * unit * unit * int * unit * unit * unit;
        The second is mutable and the first is not.
 |}];;
diff --git a/testsuite/tests/typing-modules/variants_errors_test.ml b/testsuite/tests/typing-modules/variants_errors_test.ml
index a923ebcfa77c..d531d36b0ae0 100644
--- a/testsuite/tests/typing-modules/variants_errors_test.ml
+++ b/testsuite/tests/typing-modules/variants_errors_test.ml
@@ -26,9 +26,9 @@ Error: Signature mismatch:
          type t = Foo of int * int
        Constructors do not match:
          Foo of float * int
-       is not compatible with:
+       is not the same as:
          Foo of int * int
-       The types are not equal.
+       The type float is not equal to the type int
 |}];;
 
 module M2 : sig
@@ -55,7 +55,7 @@ Error: Signature mismatch:
          type t = Foo of int * int
        Constructors do not match:
          Foo of float
-       is not compatible with:
+       is not the same as:
          Foo of int * int
        They have different arities.
 |}];;
@@ -84,13 +84,13 @@ Error: Signature mismatch:
          type t = Foo of { x : int; y : int; }
        Constructors do not match:
          Foo of { x : float; y : int; }
-       is not compatible with:
+       is not the same as:
          Foo of { x : int; y : int; }
        Fields do not match:
          x : float;
-       is not compatible with:
+       is not the same as:
          x : int;
-       The types are not equal.
+       The type float is not equal to the type int
 |}];;
 
 module M4 : sig
@@ -117,7 +117,7 @@ Error: Signature mismatch:
          type t = Foo of { x : int; y : int; }
        Constructors do not match:
          Foo of float
-       is not compatible with:
+       is not the same as:
          Foo of { x : int; y : int; }
        The second uses inline records and the first doesn't.
 |}];;
@@ -146,7 +146,7 @@ Error: Signature mismatch:
          type 'a t = Foo : int -> int t
        Constructors do not match:
          Foo of 'a
-       is not compatible with:
+       is not the same as:
          Foo : int -> int t
        The second has explicit return type and the first doesn't.
 |}];;
@@ -172,9 +172,9 @@ Error: Signature mismatch:
          type ('a, 'b) t = 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
@@ -198,7 +198,7 @@ Error: Signature mismatch:
          type ('a, 'b) t = 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
 |}];;
diff --git a/testsuite/tests/typing-objects-bugs/pr3968_bad.compilers.reference b/testsuite/tests/typing-objects-bugs/pr3968_bad.compilers.reference
index 9bf6524d6b84..7bb5181984fa 100644
--- a/testsuite/tests/typing-objects-bugs/pr3968_bad.compilers.reference
+++ b/testsuite/tests/typing-objects-bugs/pr3968_bad.compilers.reference
@@ -14,10 +14,12 @@ Error: The class type
            val l :
              [ `Abs of
                  string *
-                 ([ `Abs of string * expr | `App of 'a * exp ] as 'b)
-             | `App of expr * expr ] as 'a
+                 ([> `App of
+                       [ `Abs of string * 'a | `App of expr * expr ] * exp ]
+                  as 'a)
+             | `App of expr * expr ]
            val r : exp
-           method eval : (string, exp) Hashtbl.t -> 'b
+           method eval : (string, exp) Hashtbl.t -> 'a
          end
        is not matched by the class type exp
        The class type
@@ -25,22 +27,22 @@ Error: The class type
            val l :
              [ `Abs of
                  string *
-                 ([ `Abs of string * expr | `App of 'a * exp ] as 'b)
-             | `App of expr * expr ] as 'a
+                 ([> `App of
+                       [ `Abs of string * 'a | `App of expr * expr ] * exp ]
+                  as 'a)
+             | `App of expr * expr ]
            val r : exp
-           method eval : (string, exp) Hashtbl.t -> 'b
+           method eval : (string, exp) Hashtbl.t -> 'a
          end
        is not matched by the class type
          object method eval : (string, exp) Hashtbl.t -> expr end
        The method eval has type
          (string, exp) Hashtbl.t ->
-         ([ `Abs of string * expr
-          | `App of [ `Abs of string * 'a | `App of expr * expr ] * exp ]
+         ([> `App of [ `Abs of string * 'a | `App of expr * expr ] * exp ]
           as 'a)
        but is expected to have type (string, exp) Hashtbl.t -> expr
        Type
-         [ `Abs of string * expr
-         | `App of [ `Abs of string * 'a | `App of expr * expr ] * exp ]
+         [> `App of [ `Abs of string * 'a | `App of expr * expr ] * exp ]
          as 'a
        is not compatible with type
          expr = [ `Abs of string * expr | `App of expr * expr ] 
diff --git a/testsuite/tests/typing-objects/Tests.ml b/testsuite/tests/typing-objects/Tests.ml
index 7bd13f19c7b0..1ecd3fdd9d6e 100644
--- a/testsuite/tests/typing-objects/Tests.ml
+++ b/testsuite/tests/typing-objects/Tests.ml
@@ -702,6 +702,8 @@ Error: Signature mismatch:
          val f : (#c as 'a) -> 'a
        is not included in
          val f : #c -> #c
+       The type (#c as 'a) -> 'a is not compatible with the type 'a -> #c
+       Type 'a is not compatible with type 'b
 |}];;
 
 module M = struct type t = int class t () = object end end;;
diff --git a/testsuite/tests/typing-poly/poly.ml b/testsuite/tests/typing-poly/poly.ml
index 92fb99d33d6e..93f862594429 100644
--- a/testsuite/tests/typing-poly/poly.ml
+++ b/testsuite/tests/typing-poly/poly.ml
@@ -1177,6 +1177,12 @@ Error: Signature mismatch:
          val f : (< m : 'a. 'a * ('a * 'b) > as 'b) -> unit
        is not included in
          val f : < m : 'b. 'b * ('b * < m : 'c. 'c * 'a > as 'a) > -> unit
+       The type (< m : 'a. 'a * ('a * 'd) > as 'd) -> unit
+       is not compatible with the type
+         < m : 'b. 'b * ('b * < m : 'c. 'c * 'e > as 'e) > -> unit
+       The method m has type 'a. 'a * ('a * < m : 'a. 'b >) as 'b,
+       but the expected method type was 'c. 'c * ('b * < m : 'c. 'a >) as 'a
+       The universal variable 'b would escape its scope
 |}];;
 
 module M : sig type 'a t type u = <m: 'a. 'a t> end
@@ -1569,6 +1575,11 @@ Error: Values do not match:
        is not included in
          val f :
            < m : 'a. [< `Bar | `Foo of 'b & int ] as 'c > -> < m : 'b. 'c >
+       The type
+         < m : 'a. [< `Bar | `Foo of 'b & int ] as 'c > -> < m : 'b. 'c >
+       is not compatible with the type
+         < m : 'a. [< `Bar | `Foo of 'b & int ] as 'd > -> < m : 'b. 'd >
+       Types for tag `Foo are incompatible
 |}]
 
 (* PR#6171 *)
diff --git a/testsuite/tests/typing-polyvariants-bugs/pr7817_bad.ml b/testsuite/tests/typing-polyvariants-bugs/pr7817_bad.ml
index 85d82c928da4..5649e29864d2 100644
--- a/testsuite/tests/typing-polyvariants-bugs/pr7817_bad.ml
+++ b/testsuite/tests/typing-polyvariants-bugs/pr7817_bad.ml
@@ -26,4 +26,9 @@ Error: Signature mismatch:
          val write : _[< `A of '_weak2 | `B of '_weak3 ] -> unit
        is not included in
          val write : [< `A of string | `B of int ] -> unit
+       The type ([< `A of 'weak2 | `B of 'weak3 ] as 'a) -> unit
+       is not compatible with the type
+         ([< `A of string | `B of int ] as 'b) -> unit
+       Type [< `A of 'weak2 | `B of 'weak3 ] as 'a
+       is not compatible with type [< `A of string | `B of int ] as 'b
 |}]
diff --git a/testsuite/tests/typing-private/private.compilers.principal.reference b/testsuite/tests/typing-private/private.compilers.principal.reference
index 2be849e10280..357975b65ac5 100644
--- a/testsuite/tests/typing-private/private.compilers.principal.reference
+++ b/testsuite/tests/typing-private/private.compilers.principal.reference
@@ -30,6 +30,7 @@ Error: Signature mismatch:
          type t = M2.t
        is not included in
          type t = private M3.t
+       The type M2.t is not equal to the type M3.t
 Line 1, characters 44-45:
 1 | module M4 : sig type t = private M3.t end = M;; (* fails *)
                                                 ^
@@ -42,6 +43,7 @@ Error: Signature mismatch:
          type t = < m : int >
        is not included in
          type t = private M3.t
+       The type < m : int > is not equal to the type M3.t
 Line 1, characters 44-46:
 1 | module M4 : sig type t = private M3.t end = M1;; (* might be ok *)
                                                 ^^
@@ -54,6 +56,7 @@ Error: Signature mismatch:
          type t = M1.t
        is not included in
          type t = private M3.t
+       The type M1.t is not equal to the type M3.t
 module M5 : sig type t = private M1.t end
 Line 1, characters 53-55:
 1 | module M6 : sig type t = private < n:int; .. > end = M1;; (* fails *)
@@ -67,6 +70,7 @@ Error: Signature mismatch:
          type t = M1.t
        is not included in
          type t = private < n : int; .. >
+       The implementation is missing the method n
 Line 3, characters 2-51:
 3 |   struct type t = int let f (x : int) = (x : t) end;; (* must fail *)
       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
@@ -79,6 +83,7 @@ Error: Signature mismatch:
          type t = int
        is not included in
          type t = private Foobar.t
+       The type int is not equal to the type Foobar.t
 module M : sig type t = private T of int val mk : int -> t end
 module M1 : sig type t = M.t val mk : int -> t end
 module M2 : sig type t = M.t val mk : int -> t end
@@ -117,7 +122,8 @@ Error: Type declarations do not match:
          type !'a t = private 'a constraint 'a = < x : int; .. >
        is not included in
          type 'a t
-       Their constraints differ.
+       Their parameters differ
+       The type < x : int; .. > is not equal to the type 'a
 type 'a t = private 'a constraint 'a = < x : int; .. >
 type t = [ `Closed ]
 type nonrec t = private [> t ]
diff --git a/testsuite/tests/typing-private/private.compilers.reference b/testsuite/tests/typing-private/private.compilers.reference
index 06968cd0e088..3e7546a6caed 100644
--- a/testsuite/tests/typing-private/private.compilers.reference
+++ b/testsuite/tests/typing-private/private.compilers.reference
@@ -30,6 +30,7 @@ Error: Signature mismatch:
          type t = M2.t
        is not included in
          type t = private M3.t
+       The type M2.t is not equal to the type M3.t
 Line 1, characters 44-45:
 1 | module M4 : sig type t = private M3.t end = M;; (* fails *)
                                                 ^
@@ -42,6 +43,7 @@ Error: Signature mismatch:
          type t = < m : int >
        is not included in
          type t = private M3.t
+       The type < m : int > is not equal to the type M3.t
 Line 1, characters 44-46:
 1 | module M4 : sig type t = private M3.t end = M1;; (* might be ok *)
                                                 ^^
@@ -54,6 +56,7 @@ Error: Signature mismatch:
          type t = M1.t
        is not included in
          type t = private M3.t
+       The type M1.t is not equal to the type M3.t
 module M5 : sig type t = private M1.t end
 Line 1, characters 53-55:
 1 | module M6 : sig type t = private < n:int; .. > end = M1;; (* fails *)
@@ -67,6 +70,7 @@ Error: Signature mismatch:
          type t = M1.t
        is not included in
          type t = private < n : int; .. >
+       The implementation is missing the method n
 Line 3, characters 2-51:
 3 |   struct type t = int let f (x : int) = (x : t) end;; (* must fail *)
       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
@@ -79,6 +83,7 @@ Error: Signature mismatch:
          type t = int
        is not included in
          type t = private Foobar.t
+       The type int is not equal to the type Foobar.t
 module M : sig type t = private T of int val mk : int -> t end
 module M1 : sig type t = M.t val mk : int -> t end
 module M2 : sig type t = M.t val mk : int -> t end
@@ -117,7 +122,8 @@ Error: Type declarations do not match:
          type !'a t = private < x : int; .. > constraint 'a = 'a t
        is not included in
          type 'a t
-       Their constraints differ.
+       Their parameters differ
+       The type 'b t as 'b is not equal to the type 'a
 type 'a t = private 'a constraint 'a = < x : int; .. >
 type t = [ `Closed ]
 type nonrec t = private [> t ]
diff --git a/testsuite/tests/typing-short-paths/short-paths.compilers.reference b/testsuite/tests/typing-short-paths/short-paths.compilers.reference
index 7265fe11bcbd..2238467f5f86 100644
--- a/testsuite/tests/typing-short-paths/short-paths.compilers.reference
+++ b/testsuite/tests/typing-short-paths/short-paths.compilers.reference
@@ -96,6 +96,7 @@ Error: Signature mismatch:
          type t = int
        is not included in
          type t = string
+       The type t is not equal to the type string
 module A : sig module B : sig type t = T end end
 module M2 : sig type u = A.B.t type foo = int type v = u end
 
diff --git a/testsuite/tests/typing-sigsubst/test_locations.compilers.reference b/testsuite/tests/typing-sigsubst/test_locations.compilers.reference
index 8417a68993a1..92566fa4d157 100644
--- a/testsuite/tests/typing-sigsubst/test_locations.compilers.reference
+++ b/testsuite/tests/typing-sigsubst/test_locations.compilers.reference
@@ -7,6 +7,7 @@ Error: Signature mismatch:
          type elt = String.t
        is not included in
          type elt = unit
+       The type String.t is not equal to the type unit
        File "test_loc_type_eq.ml", line 1, characters 31-46:
          Expected declaration
        File "test_functor.ml", line 8, characters 45-61: Actual declaration
@@ -26,6 +27,7 @@ Error: Signature mismatch:
          type elt = String.t
        is not included in
          type elt = unit
+       The type String.t is not equal to the type unit
        File "test_loc_modtype_type_eq.ml", line 1, characters 36-51:
          Expected declaration
        File "test_functor.ml", line 8, characters 45-61: Actual declaration
@@ -45,6 +47,8 @@ Error: Signature mismatch:
          val create : elt -> t
        is not included in
          val create : unit -> t
+       The type elt -> t is not compatible with the type unit -> t
+       Type elt is not compatible with type unit 
        File "test_loc_type_subst.ml", line 1, characters 11-47:
          Expected declaration
        File "test_functor.ml", line 5, characters 2-23: Actual declaration
@@ -64,6 +68,8 @@ Error: Signature mismatch:
          val create : elt -> t
        is not included in
          val create : unit -> t
+       The type elt -> t is not compatible with the type unit -> t
+       Type elt is not compatible with type unit 
        File "test_loc_modtype_type_subst.ml", line 1, characters 16-52:
          Expected declaration
        File "test_functor.ml", line 5, characters 2-23: Actual declaration
diff --git a/testsuite/tests/typing-unboxed/test.ml b/testsuite/tests/typing-unboxed/test.ml
index e57ed3b4e8c4..d0f658d43f1c 100644
--- a/testsuite/tests/typing-unboxed/test.ml
+++ b/testsuite/tests/typing-unboxed/test.ml
@@ -119,6 +119,7 @@ Error: Signature mismatch:
          external f : int -> (int [@untagged]) = "f" "f_nat"
        is not included in
          external f : int -> int = "f" "f_nat"
+       The two primitives' results have different representations
 |}]
 
 module Bad2 : sig
@@ -141,6 +142,7 @@ Error: Signature mismatch:
          external f : (int [@untagged]) -> int = "f" "f_nat"
        is not included in
          external f : int -> int = "f" "f_nat"
+       The two primitives' 1st arguments have different representations
 |}]
 
 module Bad3 : sig
@@ -163,6 +165,7 @@ Error: Signature mismatch:
          external f : (int [@untagged]) -> int = "f" "f_nat"
        is not included in
          external f : int -> int = "a" "a_nat"
+       The names of the primitives are not the same
 |}]
 
 module Bad4 : sig
@@ -185,6 +188,7 @@ Error: Signature mismatch:
          external f : float -> (float [@unboxed]) = "f" "f_nat"
        is not included in
          external f : float -> float = "f" "f_nat"
+       The two primitives' results have different representations
 |}]
 
 module Bad5 : sig
@@ -207,6 +211,7 @@ Error: Signature mismatch:
          external f : (float [@unboxed]) -> float = "f" "f_nat"
        is not included in
          external f : float -> float = "f" "f_nat"
+       The two primitives' 1st arguments have different representations
 |}]
 
 module Bad6 : sig
@@ -229,6 +234,7 @@ Error: Signature mismatch:
          external f : (float [@unboxed]) -> float = "f" "f_nat"
        is not included in
          external f : float -> float = "a" "a_nat"
+       The names of the primitives are not the same
 |}]
 
 module Bad7 : sig
@@ -251,6 +257,7 @@ Error: Signature mismatch:
          external f : int -> int = "f" "f_nat" [@@noalloc]
        is not included in
          external f : int -> int = "f" "f_nat"
+       The first primitive is [@@noalloc] but the second is not
 |}]
 
 (* Bad: attributes in the interface but not in the implementation *)
@@ -275,6 +282,7 @@ Error: Signature mismatch:
          external f : int -> int = "f" "f_nat"
        is not included in
          external f : int -> (int [@untagged]) = "f" "f_nat"
+       The two primitives' results have different representations
 |}]
 
 module Bad9 : sig
@@ -297,6 +305,7 @@ Error: Signature mismatch:
          external f : int -> int = "f" "f_nat"
        is not included in
          external f : (int [@untagged]) -> int = "f" "f_nat"
+       The two primitives' 1st arguments have different representations
 |}]
 
 module Bad10 : sig
@@ -319,6 +328,7 @@ Error: Signature mismatch:
          external f : int -> int = "a" "a_nat"
        is not included in
          external f : (int [@untagged]) -> int = "f" "f_nat"
+       The names of the primitives are not the same
 |}]
 
 module Bad11 : sig
@@ -341,6 +351,7 @@ Error: Signature mismatch:
          external f : float -> float = "f" "f_nat"
        is not included in
          external f : float -> (float [@unboxed]) = "f" "f_nat"
+       The two primitives' results have different representations
 |}]
 
 module Bad12 : sig
@@ -363,6 +374,7 @@ Error: Signature mismatch:
          external f : float -> float = "f" "f_nat"
        is not included in
          external f : (float [@unboxed]) -> float = "f" "f_nat"
+       The two primitives' 1st arguments have different representations
 |}]
 
 module Bad13 : sig
@@ -385,6 +397,7 @@ Error: Signature mismatch:
          external f : float -> float = "a" "a_nat"
        is not included in
          external f : (float [@unboxed]) -> float = "f" "f_nat"
+       The names of the primitives are not the same
 |}]
 
 module Bad14 : sig
@@ -407,6 +420,7 @@ Error: Signature mismatch:
          external f : int -> int = "f" "f_nat"
        is not included in
          external f : int -> int = "f" "f_nat" [@@noalloc]
+       The second primitive is [@@noalloc] but the first is not
 |}]
 
 (* Bad: claiming something is a primitive when it isn't *)
@@ -431,6 +445,7 @@ Error: Signature mismatch:
          val f : int -> int
        is not included in
          external f : int -> int = "f" "f_nat"
+       The definition is not a primitive
 |}]
 
 (* Good: not claiming something is a primitive when it is *)
@@ -470,6 +485,7 @@ Error: Signature mismatch:
          external f : int -> int = "gg" "f_nat"
        is not included in
          external f : int -> int = "f" "f_nat"
+       The names of the primitives are not the same
 |}]
 
 module Bad18 : sig
@@ -492,6 +508,7 @@ Error: Signature mismatch:
          external f : int -> int = "f" "gg_nat"
        is not included in
          external f : int -> int = "f" "f_nat"
+       The native names of the primitives are not the same
 |}]
 
 module Bad19 : sig
@@ -514,6 +531,7 @@ Error: Signature mismatch:
          external f : int -> int = "gg" "gg_nat"
        is not included in
          external f : int -> int = "f" "f_nat"
+       The names of the primitives are not the same
 |}]
 
 (* Bad: mismatched arities *)
@@ -544,6 +562,8 @@ Error: Signature mismatch:
          external f : int -> int -> int = "f" "f_nat"
        is not included in
          external f : int -> int -> int = "f" "f_nat"
+       The syntactic arities of these primitives were not the same
+       (They must have the same number of ->s present in the source)
 |}]
 
 module Bad21 : sig
@@ -571,6 +591,8 @@ Error: Signature mismatch:
          external f : int -> int_int = "f" "f_nat"
        is not included in
          external f : int -> int -> int = "f" "f_nat"
+       The syntactic arities of these primitives were not the same
+       (They must have the same number of ->s present in the source)
 |}]
 
 (* This will fail with a *type* error, instead of an arity mismatch *)
@@ -594,6 +616,8 @@ Error: Signature mismatch:
          external f : int -> int -> int = "f" "f_nat"
        is not included in
          external f : int -> int = "f" "f_nat"
+       The type int -> int -> int is not compatible with the type int -> int
+       Type int -> int is not compatible with type int
 |}]
 
 (* Bad: unboxed or untagged with the wrong type *)
diff --git a/testsuite/tests/typing-warnings/pr6587.ml b/testsuite/tests/typing-warnings/pr6587.ml
index baa45b692c21..36b9044718ad 100644
--- a/testsuite/tests/typing-warnings/pr6587.ml
+++ b/testsuite/tests/typing-warnings/pr6587.ml
@@ -36,4 +36,7 @@ Error: Signature mismatch:
          val f : fpclass -> Stdlib.fpclass
        is not included in
          val f : fpclass -> fpclass
+       The type fpclass -> Stdlib.fpclass is not compatible with the type
+         fpclass -> fpclass
+       Type Stdlib.fpclass is not compatible with type fpclass
 |}]
diff --git a/toplevel/topdirs.ml b/toplevel/topdirs.ml
index 21930567acfe..b8417639677b 100644
--- a/toplevel/topdirs.ml
+++ b/toplevel/topdirs.ml
@@ -169,6 +169,8 @@ let _ = add_directive "mod_use" (Directive_string (dir_mod_use std_out))
 
 (* Install, remove a printer *)
 
+exception Bad_printing_function
+
 let filter_arrow ty =
   let ty = Ctype.expand_head !toplevel_env ty in
   match ty.desc with
@@ -177,10 +179,10 @@ let filter_arrow ty =
 
 let rec extract_last_arrow desc =
   match filter_arrow desc with
-  | None -> raise (Ctype.Unify [])
+  | None -> raise Bad_printing_function
   | Some (_, r as res) ->
       try extract_last_arrow r
-      with Ctype.Unify _ -> res
+      with Bad_printing_function -> res
 
 let extract_target_type ty = fst (extract_last_arrow ty)
 let extract_target_parameters ty =
@@ -209,9 +211,14 @@ let printer_type ppf typename =
 let match_simple_printer_type desc printer_type =
   Ctype.begin_def();
   let ty_arg = Ctype.newvar() in
-  Ctype.unify !toplevel_env
-    (Ctype.newconstr printer_type [ty_arg])
-    (Ctype.instance desc.val_type);
+  begin try
+    (* Only the call to [Ctype.unify] can actually fail *)
+    Ctype.unify !toplevel_env
+      (Ctype.newconstr printer_type [ty_arg])
+      (Ctype.instance desc.val_type);
+  with Ctype.Unify _ ->
+    raise Bad_printing_function
+  end;
   Ctype.end_def();
   Ctype.generalize ty_arg;
   (ty_arg, None)
@@ -227,13 +234,18 @@ let match_generic_printer_type desc path args printer_type =
       (fun ty_arg ty -> Ctype.newty (Tarrow (Asttypes.Nolabel, ty_arg, ty,
                                              Cunknown)))
       ty_args (Ctype.newconstr printer_type [ty_target]) in
-  Ctype.unify !toplevel_env
-    ty_expected
-    (Ctype.instance desc.val_type);
+  begin try
+    (* Only the call to [Ctype.unify] can actually fail *)
+    Ctype.unify !toplevel_env
+      ty_expected
+      (Ctype.instance desc.val_type);
+  with Ctype.Unify _ ->
+    raise Bad_printing_function
+  end;
   Ctype.end_def();
   Ctype.generalize ty_expected;
   if not (Ctype.all_distinct_vars !toplevel_env args) then
-    raise (Ctype.Unify []);
+    raise Bad_printing_function;
   (ty_expected, Some (path, ty_args))
 
 let match_printer_type ppf desc =
@@ -241,10 +253,10 @@ let match_printer_type ppf desc =
   let printer_type_old = printer_type ppf "printer_type_old" in
   try
     (match_simple_printer_type desc printer_type_new, false)
-  with Ctype.Unify _ ->
+  with Bad_printing_function ->
     try
       (match_simple_printer_type desc printer_type_old, true)
-    with Ctype.Unify _ as exn ->
+    with Bad_printing_function as exn ->
       match extract_target_parameters desc.val_type with
       | None -> raise exn
       | Some (path, args) ->
@@ -256,8 +268,8 @@ let find_printer_type ppf lid =
   | (path, desc) -> begin
     match match_printer_type ppf desc with
     | (ty_arg, is_old_style) -> (ty_arg, path, is_old_style)
-    | exception Ctype.Unify _ ->
-      fprintf ppf "%a has a wrong type for a printing function.@."
+    | exception Bad_printing_function ->
+      fprintf ppf "%a has the wrong type for a printing function.@."
       Printtyp.longident lid;
       raise Exit
   end
diff --git a/typing/ctype.ml b/typing/ctype.ml
index eb4630dfdbde..e46367ee4231 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -57,10 +57,14 @@ open Local_store
 
 (**** Errors ****)
 
-exception Unify of unification Errortrace.t
-exception Equality of comparison Errortrace.t
-exception Moregen of comparison Errortrace.t
-exception Subtype of Errortrace.Subtype.t * unification Errortrace.t
+exception Unify_trace    of unification Errortrace.t
+exception Equality_trace of comparison  Errortrace.t
+exception Moregen_trace  of comparison  Errortrace.t
+
+exception Unify    of unification_error
+exception Equality of equality_error
+exception Moregen  of moregen_error
+exception Subtype  of Errortrace.Subtype.t * unification_error
 
 exception Escape of desc Errortrace.escape
 
@@ -76,9 +80,9 @@ let raise_trace_for
       (tr_exn : variant trace_exn)
       (tr     : variant Errortrace.t) : 'a =
   match tr_exn with
-  | Unify    -> raise (Unify    tr)
-  | Equality -> raise (Equality tr)
-  | Moregen  -> raise (Moregen  tr)
+  | Unify    -> raise (Unify_trace    tr)
+  | Equality -> raise (Equality_trace tr)
+  | Moregen  -> raise (Moregen_trace  tr)
 
 (* Uses of this function are a bit suspicious, as we usually want to maintain
    trace information; sometimes it makes sense, however, since we're maintaining
@@ -121,7 +125,7 @@ exception Cannot_subst
 
 exception Cannot_unify_universal_variables
 
-exception Matches_failure of Env.t * unification Errortrace.t
+exception Matches_failure of Env.t * unification_error
 
 exception Incompatible
 
@@ -1467,7 +1471,8 @@ let instance_label fixed lbl =
 
 (**** Instantiation with parameter substitution ****)
 
-let unify' = (* Forward declaration *)
+(* NB: since this is [unify_var], it raises [Unify], not [Unify_trace] *)
+let unify_var' = (* Forward declaration *)
   ref (fun _env _ty1 _ty2 -> assert false)
 
 
@@ -1490,8 +1495,8 @@ let subst env level priv abbrev ty params args body =
   let (params', body') = instance_parameterized_type params body in
   abbreviations := ref Mnil;
   try
-    !unify' env body0 body';
-    List.iter2 (!unify' env) params' args;
+    !unify_var' env body0 body';
+    List.iter2 (!unify_var' env) params' args;
     current_level := old_level;
     body'
   with Unify _ ->
@@ -1724,7 +1729,7 @@ let full_expand ~may_forget_scope env ty =
   let ty =
     if may_forget_scope then
       let ty = repr ty in
-      try expand_head_unif env ty with Unify _ ->
+      try expand_head_unif env ty with Unify_trace _ ->
         (* #10277: forget scopes when printing trace *)
         begin_def ();
         init_def ty.level;
@@ -2275,9 +2280,9 @@ let rec mcomp type_pairs env t1 t2 =
         | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _)) ->
             mcomp_type_decl type_pairs env p1 p2 tl1 tl2
         | (Tconstr (_, [], _), _) when has_injective_univars env t2' ->
-            raise (Unify [])
+            raise_unexplained_for Unify
         | (_, Tconstr (_, [], _)) when has_injective_univars env t1' ->
-            raise (Unify [])
+            raise_unexplained_for Unify
         | (Tconstr (p, _, _), _) | (_, Tconstr (p, _, _)) ->
             begin try
               let decl = Env.find_type p env in
@@ -2590,7 +2595,7 @@ let unify1_var env t1 t2 =
       end;
       link_type t1 t2;
       true
-  | exception Unify _ when !umode = Pattern ->
+  | exception Unify_trace _ when !umode = Pattern ->
       false
 
 (* Can only be called when generate_equations is true *)
@@ -2604,7 +2609,7 @@ let unify3_var env t1' t2 t2' =
   occur_for Unify !env t1' t2;
   match occur_univar_for Unify !env t2 with
   | () -> link_type t1' t2
-  | exception Unify _ when !umode = Pattern ->
+  | exception Unify_trace _ when !umode = Pattern ->
       reify env t1';
       reify env t2';
       if can_generate_equations () then begin
@@ -2686,9 +2691,9 @@ let rec unify (env:Env.t ref) t1 t2 =
         unify2 env t1 t2
     end;
     reset_trace_gadt_instances reset_tracing;
-  with Unify trace ->
+  with Unify_trace trace ->
     reset_trace_gadt_instances reset_tracing;
-    raise( Unify (Errortrace.diff t1 t2 :: trace) )
+    raise_trace_for Unify (Errortrace.diff t1 t2 :: trace)
 
 and unify2 env t1 t2 =
   (* Second step: expansion of abbreviations *)
@@ -2718,7 +2723,7 @@ and unify2 env t1 t2 =
   if unify_eq t1 t1' || not (unify_eq t2 t2') then
     unify3 env t1 t1' t2 t2'
   else
-    try unify3 env t2 t2' t1 t1' with Unify trace ->
+    try unify3 env t2 t2' t1 t1' with Unify_trace trace ->
       raise_trace_for Unify (swap_trace trace)
 
 and unify3 env t1 t1' t2 t2' =
@@ -2784,7 +2789,7 @@ and unify3 env t1 t1' t2 t2' =
                   ~allow_recursive:!allow_recursive_equation
                   begin fun () ->
                     let snap = snapshot () in
-                    try unify env t1 t2 with Unify _ ->
+                    try unify env t1 t2 with Unify_trace _ ->
                       backtrack snap;
                       reify env t1;
                       reify env t2
@@ -2835,7 +2840,7 @@ and unify3 env t1 t1' t2 t2' =
           else begin
             let snap = snapshot () in
             try unify_row env row1 row2
-            with Unify _ ->
+            with Unify_trace _ ->
               backtrack snap;
               reify env t1';
               reify env t2';
@@ -2874,9 +2879,9 @@ and unify3 env t1 t1' t2 t2' =
             (* if !generate_equations then List.iter2 (mcomp !env) tl1 tl2 *)
           end
       | (Tnil,  Tconstr _ ) ->
-          raise (Unify Errortrace.[Obj(Abstract_row Second)])
+          raise_for Unify (Obj (Abstract_row Second))
       | (Tconstr _,  Tnil ) ->
-          raise (Unify Errortrace.[Obj(Abstract_row First)])
+          raise_for Unify (Obj (Abstract_row First))
       | (_, _) -> raise_unexplained_for Unify
       end;
       (* XXX Commentaires + changer "create_recursion"
@@ -2890,7 +2895,7 @@ and unify3 env t1 t1' t2 t2' =
               link_type (repr t2) (repr t2')
         | _ ->
             () (* t2 has already been expanded by update_level *)
-    with Unify trace ->
+    with Unify_trace trace ->
       Private_type_expr.set_desc t1' d1;
       raise_trace_for Unify trace
   end
@@ -2939,8 +2944,9 @@ and unify_fields env ty1 ty2 =          (* Optimization *)
             update_scope_for Unify va.scope t1
           end;
           unify env t1 t2
-        with Unify trace ->
-          raise( Unify (Errortrace.incompatible_fields n t1 t2 :: trace) )
+        with Unify_trace trace ->
+          raise_trace_for Unify
+            (Errortrace.incompatible_fields n t1 t2 :: trace)
       )
       pairs
   with exn ->
@@ -3047,7 +3053,7 @@ and unify_row env row1 row2 =
     List.iter
       (fun (l,f1,f2) ->
         try unify_row_field env fixed1 fixed2 rm1 rm2 l f1 f2
-        with Unify trace ->
+        with Unify_trace trace ->
           raise_trace_for Unify (Variant (Incompatible_types_for l) :: trace)
       )
       pairs;
@@ -3160,9 +3166,9 @@ let unify env ty1 ty2 =
   try
     unify env ty1 ty2
   with
-    Unify trace ->
+    Unify_trace trace ->
       undo_compress snap;
-      raise (Unify (expand_trace !env trace))
+      raise (Unify {trace = expand_trace !env trace})
 
 let unify_gadt ~equations_level:lev ~allow_recursive (env:Env.t ref) ty1 ty2 =
   try
@@ -3196,17 +3202,17 @@ let unify_var env t1 t2 =
         update_scope_for Unify t1.scope t2;
         link_type t1 t2;
         reset_trace_gadt_instances reset_tracing;
-      with Unify trace ->
+      with Unify_trace trace ->
         reset_trace_gadt_instances reset_tracing;
         let expanded_trace =
           expand_trace env @@ Errortrace.diff t1 t2 :: trace
         in
-        raise_trace_for Unify expanded_trace
+        raise (Unify {trace = expanded_trace})
       end
   | _ ->
       unify (ref env) t1 t2
 
-let _ = unify' := unify_var
+let _ = unify_var' := unify_var
 
 let unify_pairs env ty1 ty2 pairs =
   univar_pairs := pairs;
@@ -3233,19 +3239,20 @@ let expand_head_trace env t =
 *)
 
 let filter_arrow env t l =
-  let t = expand_head_trace env t in
-  match t.desc with
-    Tvar _ ->
-      let lv = t.level in
-      let t1 = newvar2 lv and t2 = newvar2 lv in
-      let t' = newty2 lv (Tarrow (l, t1, t2, Cok)) in
-      link_type t t';
-      (t1, t2)
-  | Tarrow(l', t1, t2, _)
-    when l = l' || !Clflags.classic && l = Nolabel && not (is_optional l') ->
-      (t1, t2)
-  | _ ->
-      raise_unexplained_for Unify
+  match expand_head_trace env t with
+  | exception Unify_trace _ -> assert false
+  | t -> match t.desc with
+    | Tvar _ ->
+        let lv = t.level in
+        let t1 = newvar2 lv and t2 = newvar2 lv in
+        let t' = newty2 lv (Tarrow (l, t1, t2, Cok)) in
+        link_type t t';
+        (t1, t2)
+    | Tarrow(l', t1, t2, _)
+      when l = l' || !Clflags.classic && l = Nolabel && not (is_optional l') ->
+        (t1, t2)
+    | _ ->
+        raise (Unify {trace=[]})
 
 (* Used by [filter_method]. *)
 let rec filter_method_field env name priv ty =
@@ -3276,19 +3283,22 @@ let rec filter_method_field env name priv ty =
 
 (* Unify [ty] and [< name : 'a; .. >]. Return ['a]. *)
 let filter_method env name priv ty =
-  let ty = expand_head_trace env ty in
-  match ty.desc with
-    Tvar _ ->
-      let ty1 = newvar () in
-      let ty' = newobj ty1 in
-      update_level_for Unify env ty.level ty';
-      update_scope_for Unify ty.scope ty';
-      link_type ty ty';
-      filter_method_field env name priv ty1
-  | Tobject(f, _) ->
-      filter_method_field env name priv f
-  | _ ->
-      raise_unexplained_for Unify
+  try
+    let ty = expand_head_trace env ty in
+    match ty.desc with
+      Tvar _ ->
+        let ty1 = newvar () in
+        let ty' = newobj ty1 in
+        update_level_for Unify env ty.level ty';
+        update_scope_for Unify ty.scope ty';
+        link_type ty ty';
+        filter_method_field env name priv ty1
+    | Tobject(f, _) ->
+        filter_method_field env name priv f
+    | _ ->
+        raise_unexplained_for Unify
+  with Unify_trace trace ->
+    raise (Unify {trace})
 
 let check_filter_method env name priv ty =
   ignore(filter_method env name priv ty)
@@ -3395,7 +3405,8 @@ let rec moregen inst_nongen type_pairs env t1 t2 =
           | (_, _) ->
               raise_unexplained_for Moregen
         end
-  with Moregen trace -> raise ( Moregen ( Errortrace.diff t1 t2 :: trace ) );
+  with Moregen_trace trace ->
+    raise_trace_for Moregen (Errortrace.diff t1 t2 :: trace)
 
 
 and moregen_list inst_nongen type_pairs env tl1 tl2 =
@@ -3419,8 +3430,9 @@ and moregen_fields inst_nongen type_pairs env ty1 ty2 =
     (fun (n, k1, t1, k2, t2) ->
        (* The below call should never throw [Public_method_to_private_method] *)
        moregen_kind k1 k2;
-       try moregen inst_nongen type_pairs env t1 t2 with Moregen trace ->
-         raise( Moregen ( Errortrace.incompatible_fields n t1 t2 :: trace ) )
+       try moregen inst_nongen type_pairs env t1 t2 with Moregen_trace trace ->
+         raise_trace_for Moregen
+           (Errortrace.incompatible_fields n t1 t2 :: trace)
     )
     pairs
 
@@ -3455,6 +3467,7 @@ and moregen_row inst_nongen type_pairs env row1 row2 =
     | _, _ :: _ -> raise_for Moregen (Variant (No_tags (First, r2)))
     | _, [] -> ()
   end;
+  let md1 = rm1.desc (* This lets us undo a following [link_type] *) in
   begin match rm1.desc, rm2.desc with
     Tunivar _, Tunivar _ ->
       unify_univar_for Moregen rm1 rm2 !univar_pairs
@@ -3467,47 +3480,82 @@ and moregen_row inst_nongen type_pairs env row1 row2 =
       in
       moregen_occur env rm1.level ext;
       update_scope_for Moregen rm1.scope ext;
+      (* This [link_type] has to be undone if the rest of the function fails *)
       link_type rm1 ext
   | Tconstr _, Tconstr _ ->
       moregen inst_nongen type_pairs env rm1 rm2
   | _ -> raise_unexplained_for Moregen
   end;
-  List.iter
-    (fun (l,f1,f2) ->
-       try
+  try
+    List.iter
+      (fun (l,f1,f2) ->
          let f1 = row_field_repr f1 and f2 = row_field_repr f2 in
          if f1 == f2 then () else
          match f1, f2 with
-         | Rpresent(Some t1), Rpresent(Some t2) ->
-             moregen inst_nongen type_pairs env t1 t2
+         (* Both matching [Rpresent]s *)
+         | Rpresent(Some t1), Rpresent(Some t2) -> begin
+             try
+               moregen inst_nongen type_pairs env t1 t2
+             with Moregen_trace trace ->
+               raise_trace_for Moregen
+                 (Variant (Incompatible_types_for l) :: trace)
+           end
          | Rpresent None, Rpresent None -> ()
-         | Reither(false, tl1, _, e1), Rpresent(Some t2) when may_inst ->
-             set_row_field e1 f2;
-             List.iter (fun t1 -> moregen inst_nongen type_pairs env t1 t2) tl1
-         | Reither(c1, tl1, _, e1), Reither(c2, tl2, m2, e2) ->
-             if e1 != e2 then begin
-               if c1 && not c2 then raise_unexplained_for Moregen;
-               set_row_field e1 (Reither (c2, [], m2, e2));
-               if List.length tl1 = List.length tl2 then
-                 List.iter2 (moregen inst_nongen type_pairs env) tl1 tl2
-               else match tl2 with
-                 | t2 :: _ ->
+         (* Both [Reither] *)
+         | Reither(c1, tl1, _, e1), Reither(c2, tl2, m2, e2) -> begin
+             try
+               if e1 != e2 then begin
+                 if c1 && not c2 then raise_unexplained_for Moregen;
+                 set_row_field e1 (Reither (c2, [], m2, e2));
+                 if List.length tl1 = List.length tl2 then
+                   List.iter2 (moregen inst_nongen type_pairs env) tl1 tl2
+                 else match tl2 with
+                   | t2 :: _ ->
                      List.iter
                        (fun t1 -> moregen inst_nongen type_pairs env t1 t2)
                        tl1
-                 | [] -> if tl1 <> [] then raise_unexplained_for Moregen
-             end
+                   | [] -> if tl1 <> [] then raise_unexplained_for Moregen
+               end
+             with Moregen_trace trace ->
+               raise_trace_for Moregen
+                 (Variant (Incompatible_types_for l) :: trace)
+           end
+         (* Generalizing [Reither] *)
+         | Reither(false, tl1, _, e1), Rpresent(Some t2) when may_inst -> begin
+             try
+               set_row_field e1 f2;
+               List.iter
+                 (fun t1 -> moregen inst_nongen type_pairs env t1 t2)
+                 tl1
+             with Moregen_trace trace ->
+               raise_trace_for Moregen
+                 (Variant (Incompatible_types_for l) :: trace)
+           end
          | Reither(true, [], _, e1), Rpresent None when may_inst ->
              set_row_field e1 f2
          | Reither(_, _, _, e1), Rabsent when may_inst -> set_row_field e1 f2
+         (* Both [Rabsent]s *)
          | Rabsent, Rabsent -> ()
-         | Rpresent (Some _), Rpresent None -> raise_unexplained_for Moregen
-         | Rpresent None, Rpresent (Some _) -> raise_unexplained_for Moregen
-         | Rpresent _, Reither _ -> raise_unexplained_for Moregen
-         | _ -> raise_unexplained_for Moregen
-       with Moregen err ->
-         raise (Moregen (Variant (Incompatible_types_for l) :: err)))
-    pairs
+         (* Mismatched constructor arguments *)
+         | Rpresent (Some _), Rpresent None
+         | Rpresent None, Rpresent (Some _) ->
+             raise_for Moregen (Variant (Incompatible_types_for l))
+         (* Mismatched presence *)
+         | Reither _, Rpresent _ ->
+             raise_for Moregen
+               (Variant (Presence_not_guaranteed_for (First, l)))
+         | Rpresent _, Reither _ ->
+             raise_for Moregen
+               (Variant (Presence_not_guaranteed_for (Second, l)))
+         (* Missing tags *)
+         | Rabsent, ((Rpresent _ | Reither _) as r) ->
+             raise_for Moregen (Variant (No_tags (First, [l, r])))
+         | ((Rpresent _ | Reither _) as r), Rabsent ->
+             raise_for Moregen (Variant (No_tags (Second, [l, r]))))
+      pairs
+  with exn ->
+    (* Undo [link_type] if we failed *)
+    set_type_desc rm1 md1; raise exn
 
 (* Must empty univar_pairs first *)
 let moregen inst_nongen type_pairs env patt subj =
@@ -3537,7 +3585,11 @@ let moregeneral env inst_nongen pat_sch subj_sch =
   let patt = instance pat_sch in
 
   Misc.try_finally
-    (fun () -> moregen inst_nongen (TypePairs.create 13) env patt subj)
+    (fun () ->
+       try
+         moregen inst_nongen (TypePairs.create 13) env patt subj
+       with Moregen_trace trace ->
+         raise (Moregen {trace}))
     ~always:(fun () -> current_level := old_level)
 
 let is_moregeneral env inst_nongen pat_sch subj_sch =
@@ -3594,12 +3646,12 @@ let matches env ty ty' =
   | () ->
       if not (all_distinct_vars env vars) then begin
         backtrack snap;
-        raise (Matches_failure (env, [Errortrace.diff ty ty']))
+        raise (Matches_failure (env, {trace = [Errortrace.diff ty ty']}))
       end;
       backtrack snap
-  | exception Unify trace ->
+  | exception Unify err ->
       backtrack snap;
-      raise (Matches_failure (env, trace))
+      raise (Matches_failure (env, err))
 
 let does_match env ty ty' =
   match matches env ty ty' with
@@ -3699,7 +3751,8 @@ let rec eqtype rename type_pairs subst env t1 t2 =
           | (_, _) ->
               raise_unexplained_for Equality
         end
-  with Equality trace ->  raise ( Equality (Errortrace.diff t1 t2 :: trace) )
+  with Equality_trace trace ->
+    raise_trace_for Equality (Errortrace.diff t1 t2 :: trace)
 
 and eqtype_list rename type_pairs subst env tl1 tl2 =
   if List.length tl1 <> List.length tl2 then
@@ -3730,8 +3783,9 @@ and eqtype_fields rename type_pairs subst env ty1 ty2 =
            eqtype_kind k1 k2;
            try
              eqtype rename type_pairs subst env t1 t2;
-           with Equality trace ->
-             raise (Equality (Errortrace.incompatible_fields n t1 t2 :: trace)))
+           with Equality_trace trace ->
+             raise_trace_for Equality
+               (Errortrace.incompatible_fields n t1 t2 :: trace))
         pairs
 
 and eqtype_kind k1 k2 =
@@ -3740,7 +3794,7 @@ and eqtype_kind k1 k2 =
   match k1, k2 with
   | (Fvar _, Fvar _)
   | (Fpresent, Fpresent) -> ()
-  | _                    -> raise_unexplained_for Equality
+  | _                    -> assert false
 
 and eqtype_row rename type_pairs subst env row1 row2 =
   (* Try expansion, needed when called from Includecore.type_manifest *)
@@ -3773,13 +3827,23 @@ and eqtype_row rename type_pairs subst env row1 row2 =
     eqtype rename type_pairs subst env row1.row_more row2.row_more;
   List.iter
     (fun (l,f1,f2) ->
-       try
-         match row_field_repr f1, row_field_repr f2 with
-         | Rpresent(Some t1), Rpresent(Some t2) ->
+       let f1 = row_field_repr f1 and f2 = row_field_repr f2 in
+       if f1 == f2 then () else
+       match f1, f2 with
+       (* Both matching [Rpresent]s *)
+       | Rpresent(Some t1), Rpresent(Some t2) -> begin
+           try
              eqtype rename type_pairs subst env t1 t2
-         | Reither(c1, [], _, _), Reither(c2, [], _, _) when c1 = c2 -> ()
-         | Reither(c1, t1::tl1, _, _), Reither(c2, t2::tl2, _, _)
-           when c1 = c2 ->
+           with Equality_trace trace ->
+             raise_trace_for Equality
+               (Variant (Incompatible_types_for l) :: trace)
+         end
+       | Rpresent None, Rpresent None -> ()
+       (* Both matching [Reither]s *)
+       | Reither(c1, [], _, _), Reither(c2, [], _, _) when c1 = c2 -> ()
+       | Reither(c1, t1::tl1, _, _), Reither(c2, t2::tl2, _, _)
+         when c1 = c2 -> begin
+           try
              eqtype rename type_pairs subst env t1 t2;
              if List.length tl1 = List.length tl2 then
                (* if same length allow different types (meaning?) *)
@@ -3790,15 +3854,29 @@ and eqtype_row rename type_pairs subst env row1 row2 =
                List.iter
                  (fun t1 -> eqtype rename type_pairs subst env t1 t2) tl1
              end
-         | Rpresent None, Rpresent None -> ()
-         | Rabsent, Rabsent -> ()
-         | Rpresent (Some _), Rpresent None -> raise_unexplained_for Equality
-         | Rpresent None, Rpresent (Some _) -> raise_unexplained_for Equality
-         | Rpresent _, Reither _ -> raise_unexplained_for Equality
-         | Reither _, Rpresent _ -> raise_unexplained_for Equality
-         | _ -> raise_unexplained_for Equality
-       with Equality err ->
-         raise (Equality (Variant (Incompatible_types_for l):: err)))
+           with Equality_trace trace ->
+             raise_trace_for Equality
+               (Variant (Incompatible_types_for l) :: trace)
+         end
+       (* Both [Rabsent]s *)
+       | Rabsent, Rabsent -> ()
+       (* Mismatched constructor arguments *)
+       | Rpresent (Some _), Rpresent None
+       | Rpresent None, Rpresent (Some _)
+       | Reither _, Reither _ ->
+           raise_for Equality (Variant (Incompatible_types_for l))
+       (* Mismatched presence *)
+       | Reither _, Rpresent _ ->
+           raise_for Equality
+             (Variant (Presence_not_guaranteed_for (First, l)))
+       | Rpresent _, Reither _ ->
+           raise_for Equality
+             (Variant (Presence_not_guaranteed_for (Second, l)))
+       (* Missing tags *)
+       | Rabsent, ((Rpresent _ | Reither _) as r) ->
+           raise_for Equality (Variant (No_tags (First, [l, r])))
+       | ((Rpresent _ | Reither _) as r), Rabsent ->
+           raise_for Equality (Variant (No_tags (Second, [l, r]))))
     pairs
 
 (* Must empty univar_pairs first *)
@@ -3814,7 +3892,11 @@ let eqtype rename type_pairs subst env t1 t2 =
 
 (* Two modes: with or without renaming of variables *)
 let equal env rename tyl1 tyl2 =
-  eqtype_list rename (TypePairs.create 11) (ref []) env tyl1 tyl2
+  let subst = ref [] in
+  try eqtype_list rename (TypePairs.create 11) subst env tyl1 tyl2
+  with Equality_trace trace ->
+    normalize_subst subst;
+    raise (Equality {subst = !subst; trace})
 
 let is_equal env rename tyl1 tyl2 =
   match equal env rename tyl1 tyl2 with
@@ -3833,20 +3915,14 @@ let rec equal_private env params1 ty1 params2 ty2 =
                           (*  Class type matching  *)
                           (*************************)
 
-type class_match_failure_trace_type =
-  | CM_Equality
-  | CM_Moregen
-
 type class_match_failure =
     CM_Virtual_class
   | CM_Parameter_arity_mismatch of int * int
-  | CM_Type_parameter_mismatch of Env.t * comparison Errortrace.t (* Equality *)
+  | CM_Type_parameter_mismatch of Env.t * equality_error
   | CM_Class_type_mismatch of Env.t * class_type * class_type
-  | CM_Parameter_mismatch of Env.t * comparison Errortrace.t (* Moregen *)
-  | CM_Val_type_mismatch of
-      class_match_failure_trace_type * string * Env.t * comparison Errortrace.t
-  | CM_Meth_type_mismatch of
-      class_match_failure_trace_type * string * Env.t * comparison Errortrace.t
+  | CM_Parameter_mismatch of Env.t * moregen_error
+  | CM_Val_type_mismatch of string * Env.t * comparison_error
+  | CM_Meth_type_mismatch of string * Env.t * comparison_error
   | CM_Non_mutable_value of string
   | CM_Non_concrete_value of string
   | CM_Missing_value of string
@@ -3867,8 +3943,10 @@ let rec moregen_clty trace type_pairs env cty1 cty2 =
     | _, Cty_constr (_, _, cty2) ->
         moregen_clty true type_pairs env cty1 cty2
     | Cty_arrow (l1, ty1, cty1'), Cty_arrow (l2, ty2, cty2') when l1 = l2 ->
-        begin try moregen true type_pairs env ty1 ty2 with Moregen trace ->
-          raise (Failure [CM_Parameter_mismatch (env, expand_trace env trace)])
+        begin
+          try moregen true type_pairs env ty1 ty2 with Moregen_trace trace ->
+            raise (Failure [
+              CM_Parameter_mismatch (env, {trace = expand_trace env trace})])
         end;
         moregen_clty false type_pairs env cty1' cty2'
     | Cty_signature sign1, Cty_signature sign2 ->
@@ -3879,18 +3957,18 @@ let rec moregen_clty trace type_pairs env cty1 cty2 =
         let (pairs, _miss1, _miss2) = associate_fields fields1 fields2 in
         List.iter
           (fun (lab, _k1, t1, _k2, t2) ->
-            try moregen true type_pairs env t1 t2 with Moregen trace ->
+            try moregen true type_pairs env t1 t2 with Moregen_trace trace ->
               raise (Failure [
                 CM_Meth_type_mismatch
-                  (CM_Moregen, lab, env, expand_trace env trace)]))
+                  (lab, env, Moregen_error {trace = expand_trace env trace})]))
           pairs;
       Vars.iter
         (fun lab (_mut, _v, ty) ->
            let (_mut', _v', ty') = Vars.find lab sign1.csig_vars in
-           try moregen true type_pairs env ty' ty with Moregen trace ->
+           try moregen true type_pairs env ty' ty with Moregen_trace trace ->
              raise (Failure [
                CM_Val_type_mismatch
-                 (CM_Moregen, lab, env, expand_trace env trace)]))
+                 (lab, env, Moregen_error {trace = expand_trace env trace})]))
         sign2.csig_vars
   | _ ->
       raise (Failure [])
@@ -4005,17 +4083,28 @@ let equal_clsig trace type_pairs subst env sign1 sign2 =
     List.iter
       (fun (lab, _k1, t1, _k2, t2) ->
          begin try eqtype true type_pairs subst env t1 t2 with
-           Equality trace ->
-           raise (Failure [CM_Meth_type_mismatch
-                             (CM_Equality, lab, env, expand_trace env trace)])
+           Equality_trace trace ->
+             normalize_subst subst;
+             raise (Failure
+                      [CM_Meth_type_mismatch
+                         (lab,
+                          env,
+                          Equality_error {subst = !subst;
+                                          trace = expand_trace env trace})])
          end)
       pairs;
     Vars.iter
       (fun lab (_, _, ty) ->
          let (_, _, ty') = Vars.find lab sign1.csig_vars in
-         try eqtype true type_pairs subst env ty' ty with Equality trace ->
-           raise (Failure [CM_Val_type_mismatch
-                             (CM_Equality, lab, env, expand_trace env trace)]))
+         try eqtype true type_pairs subst env ty' ty
+         with Equality_trace trace ->
+           normalize_subst subst;
+           raise (Failure
+                    [CM_Val_type_mismatch
+                       (lab,
+                        env,
+                        Equality_error {subst = !subst;
+                                        trace = expand_trace env trace})]))
       sign2.csig_vars
   with
     Failure error when trace ->
@@ -4104,9 +4193,12 @@ let match_class_declarations env patt_params patt_type subj_params subj_type =
         if lp  <> ls then
           raise (Failure [CM_Parameter_arity_mismatch (lp, ls)]);
         List.iter2 (fun p s ->
-          try eqtype true type_pairs subst env p s with Equality trace ->
-            raise (Failure [CM_Type_parameter_mismatch
-                               (env, expand_trace env trace)]))
+          try eqtype true type_pairs subst env p s with Equality_trace trace ->
+            normalize_subst subst;
+            raise (Failure
+                     [CM_Type_parameter_mismatch
+                        (env,
+                         {subst = !subst; trace = expand_trace env trace})]))
           patt_params subj_params;
      (* old code: equal_clty false type_pairs subst env patt_type subj_type; *)
         equal_clsig false type_pairs subst env sign1 sign2;
@@ -4360,7 +4452,7 @@ let enlarge_type env ty =
 let subtypes = TypePairs.create 17
 
 let subtype_error env trace =
-  raise (Subtype (expand_subtype_trace env (List.rev trace), []))
+  raise (Subtype (expand_subtype_trace env (List.rev trace), {trace=[]}))
 
 let rec subtype_rec env trace t1 t2 cstrs =
   let t1 = repr t1 in
@@ -4549,9 +4641,9 @@ let subtype env ty1 ty2 =
   function () ->
     List.iter
       (function (trace0, t1, t2, pairs) ->
-         try unify_pairs (ref env) t1 t2 pairs with Unify trace ->
+         try unify_pairs (ref env) t1 t2 pairs with Unify {trace} ->
            raise (Subtype (expand_subtype_trace env (List.rev trace0),
-                           List.tl trace)))
+                           {trace = List.tl trace})))
       (List.rev cstrs)
 
                               (*******************)
@@ -4660,13 +4752,11 @@ let rec normalize_type_rec visited ty =
               let tyl' =
                 List.fold_left
                   (fun tyl ty ->
-                    if List.exists
-                          (fun ty' ->
-                             match equal Env.empty false [ty] [ty'] with
-                             | () -> true
-                             | exception Equality _ -> false)
+                     if List.exists
+                          (fun ty' -> is_equal Env.empty false [ty] [ty'])
                           tyl
-                     then tyl else ty::tyl)
+                     then tyl
+                     else ty::tyl)
                   [ty] tyl
               in
               if f != f0 || List.length tyl' < List.length tyl then
diff --git a/typing/ctype.mli b/typing/ctype.mli
index 7185cdb7e01e..1b92dda9e7e2 100644
--- a/typing/ctype.mli
+++ b/typing/ctype.mli
@@ -20,16 +20,17 @@ open Types
 
 module TypePairs : Hashtbl.S with type key = type_expr * type_expr
 
-exception Unify of Errortrace.unification Errortrace.t
-exception Equality of Errortrace.comparison Errortrace.t
-exception Moregen of Errortrace.comparison Errortrace.t
-exception Subtype of Errortrace.Subtype.t * Errortrace.unification Errortrace.t
+exception Unify    of Errortrace.unification_error
+exception Equality of Errortrace.equality_error
+exception Moregen  of Errortrace.moregen_error
+exception Subtype  of Errortrace.Subtype.t * Errortrace.unification_error
+
 exception Escape of Errortrace.desc Errortrace.escape
 
 exception Tags of label * label
 exception Cannot_expand
 exception Cannot_apply
-exception Matches_failure of Env.t * Errortrace.unification Errortrace.t
+exception Matches_failure of Env.t * Errortrace.unification_error
   (* Raised from [matches], hence the odd name *)
 exception Incompatible
   (* Raised from [mcomp] *)
@@ -234,22 +235,14 @@ val does_match: Env.t -> type_expr -> type_expr -> bool
 val reify_univars : Env.t -> Types.type_expr -> Types.type_expr
         (* Replaces all the variables of a type by a univar. *)
 
-type class_match_failure_trace_type =
-  | CM_Equality
-  | CM_Moregen
-
 type class_match_failure =
     CM_Virtual_class
   | CM_Parameter_arity_mismatch of int * int
-  | CM_Type_parameter_mismatch of Env.t * Errortrace.comparison Errortrace.t
+  | CM_Type_parameter_mismatch of Env.t * Errortrace.equality_error
   | CM_Class_type_mismatch of Env.t * class_type * class_type
-  | CM_Parameter_mismatch of Env.t * Errortrace.comparison Errortrace.t
-  | CM_Val_type_mismatch of
-      class_match_failure_trace_type *
-      string * Env.t * Errortrace.comparison Errortrace.t
-  | CM_Meth_type_mismatch of
-      class_match_failure_trace_type *
-      string * Env.t * Errortrace.comparison Errortrace.t
+  | CM_Parameter_mismatch of Env.t * Errortrace.moregen_error
+  | CM_Val_type_mismatch of string * Env.t * Errortrace.comparison_error
+  | CM_Meth_type_mismatch of string * Env.t * Errortrace.comparison_error
   | CM_Non_mutable_value of string
   | CM_Non_concrete_value of string
   | CM_Missing_value of string
@@ -259,6 +252,7 @@ type class_match_failure =
   | CM_Public_method of string
   | CM_Private_method of string
   | CM_Virtual_method of string
+
 val match_class_types:
     ?trace:bool -> Env.t -> class_type -> class_type -> class_match_failure list
         (* Check if the first class type is more general than the second. *)
diff --git a/typing/errortrace.ml b/typing/errortrace.ml
index eca74088de8e..66176d22801b 100644
--- a/typing/errortrace.ml
+++ b/typing/errortrace.ml
@@ -85,6 +85,7 @@ type 'variety variant =
   | Fixed_row :
       position * fixed_row_case * fixed_explanation -> unification variant
   (* Equality & Moregen *)
+  | Presence_not_guaranteed_for : position * string -> comparison variant
   | Openness : position (* Always [Second] for Moregen *) -> comparison variant
 
 type 'variety obj =
@@ -141,6 +142,21 @@ let swap_elt (type variety) : ('a, variety) elt -> ('a, variety) elt = function
 
 let swap_trace e = List.map swap_elt e
 
+type unification_error = { trace : unification t } [@@unboxed]
+
+type equality_error =
+  { trace : comparison t;
+    subst : (type_expr * type_expr) list }
+
+type moregen_error = { trace : comparison t } [@@unboxed]
+
+type comparison_error =
+  | Equality_error of equality_error
+  | Moregen_error  of moregen_error
+
+let swap_unification_error ({trace} : unification_error) =
+  ({trace = swap_trace trace} : unification_error)
+
 module Subtype = struct
   type 'a elt =
     | Diff of 'a diff
diff --git a/typing/errortrace.mli b/typing/errortrace.mli
index be6000ed1069..85abfe8395e2 100644
--- a/typing/errortrace.mli
+++ b/typing/errortrace.mli
@@ -66,6 +66,7 @@ type 'variety variant =
   | Fixed_row :
       position * fixed_row_case * fixed_explanation -> unification variant
   (* Equality & Moregen *)
+  | Presence_not_guaranteed_for : position * string -> comparison variant
   | Openness : position (* Always [Second] for Moregen *) -> comparison variant
 
 type 'variety obj =
@@ -102,6 +103,30 @@ val incompatible_fields : string -> type_expr -> type_expr -> (desc, _) elt
 
 val swap_trace : 'variety t -> 'variety t
 
+(* The traces (['variety t]) are the core error types.  However, we bundle them
+   up into three "top-level" error types, which are used elsewhere:
+   [unification_error], [equality_error], and [moregen_error].  In the case of
+   [equality_error], this has to bundle in extra information; in general, it
+   distinguishes the three types of errors and allows us to distinguish traces
+   that are being built (or processed) from those that are complete and have
+   become the final error. *)
+
+type unification_error = { trace : unification t } [@@unboxed]
+
+type equality_error =
+  { trace : comparison t;
+    subst : (type_expr * type_expr) list }
+
+type moregen_error = { trace : comparison t } [@@unboxed]
+
+(* Wraps up the two different kinds of [comparison] errors in one type *)
+type comparison_error =
+  | Equality_error of equality_error
+  | Moregen_error  of moregen_error
+
+(* Lift [swap_trace] to [unification_error] *)
+val swap_unification_error : unification_error -> unification_error
+
 module Subtype : sig
   type 'a elt =
     | Diff of 'a diff
diff --git a/typing/includeclass.ml b/typing/includeclass.ml
index 2f0c057ff9e6..acc423d2afb6 100644
--- a/typing/includeclass.ml
+++ b/typing/includeclass.ml
@@ -49,10 +49,6 @@ let rec hide_params = function
   | cty -> cty
 *)
 
-let report_error_for = function
-  | CM_Equality -> Printtyp.report_equality_error
-  | CM_Moregen  -> Printtyp.report_moregen_error
-
 let include_err ppf =
   function
   | CM_Virtual_class ->
@@ -60,8 +56,8 @@ let include_err ppf =
   | CM_Parameter_arity_mismatch _ ->
       fprintf ppf
         "The classes do not have the same number of type parameters"
-  | CM_Type_parameter_mismatch (env, trace) ->
-      Printtyp.report_equality_error ppf env trace
+  | CM_Type_parameter_mismatch (env, err) ->
+      Printtyp.report_equality_error ppf env err
         (function ppf ->
           fprintf ppf "A type parameter has type")
         (function ppf ->
@@ -73,20 +69,20 @@ let include_err ppf =
           Printtyp.class_type cty1
           "is not matched by the class type"
           Printtyp.class_type cty2)
-  | CM_Parameter_mismatch (env, trace) ->
-      Printtyp.report_moregen_error ppf env trace
+  | CM_Parameter_mismatch (env, err) ->
+      Printtyp.report_moregen_error ppf env err
         (function ppf ->
           fprintf ppf "A parameter has type")
         (function ppf ->
           fprintf ppf "but is expected to have type")
-  | CM_Val_type_mismatch (trace_type, lab, env, trace) ->
-      report_error_for trace_type ppf env trace
+  | CM_Val_type_mismatch (lab, env, err) ->
+      Printtyp.report_comparison_error ppf env err
         (function ppf ->
           fprintf ppf "The instance variable %s@ has type" lab)
         (function ppf ->
           fprintf ppf "but is expected to have type")
-  | CM_Meth_type_mismatch (trace_type, lab, env, trace) ->
-      report_error_for trace_type  ppf env trace
+  | CM_Meth_type_mismatch (lab, env, err) ->
+      Printtyp.report_comparison_error ppf env err
         (function ppf ->
           fprintf ppf "The method %s@ has type" lab)
         (function ppf ->
diff --git a/typing/includecore.ml b/typing/includecore.ml
index 20aa7493bf47..5086e51278a2 100644
--- a/typing/includecore.ml
+++ b/typing/includecore.ml
@@ -66,7 +66,7 @@ let primitive_descriptions pd1 pd2 =
 type value_mismatch =
   | Primitive_mismatch of primitive_mismatch
   | Not_a_primitive
-  | Type of Env.t * Errortrace.comparison Errortrace.t
+  | Type of Errortrace.moregen_error
 
 exception Dont_match of value_mismatch
 
@@ -80,7 +80,7 @@ let value_descriptions ~loc env name
     vd1.val_attributes vd2.val_attributes
     name;
   match Ctype.moregeneral env true vd1.val_type vd2.val_type with
-  | exception Ctype.Moregen trace -> raise (Dont_match (Type (env, trace)))
+  | exception Ctype.Moregen err -> raise (Dont_match (Type err))
   | () -> begin
       match (vd1.val_kind, vd2.val_kind) with
       | (Val_prim p1, Val_prim p2) -> begin
@@ -105,7 +105,8 @@ let private_flags decl1 decl2 =
   | Private, Public ->
       decl2.type_kind = Type_abstract &&
       (decl2.type_manifest = None || decl1.type_kind <> Type_abstract)
-  | _, _ -> true
+  | _, _ ->
+      true
 
 (* Inclusion between manifest types (particularly for private row types) *)
 
@@ -131,7 +132,7 @@ let choose_other ord first second =
   | Second -> choose First first second
 
 type label_mismatch =
-  | Type of Env.t * Errortrace.comparison Errortrace.t
+  | Type of Errortrace.equality_error
   | Mutability of position
 
 type record_mismatch =
@@ -143,7 +144,7 @@ type record_mismatch =
   | Unboxed_float_representation of position
 
 type constructor_mismatch =
-  | Type of Env.t * Errortrace.comparison Errortrace.t
+  | Type of Errortrace.equality_error
   | Arity
   | Inline_record of record_mismatch
   | Kind of position
@@ -164,22 +165,22 @@ type extension_constructor_mismatch =
                             * constructor_mismatch
 
 type private_variant_mismatch =
-  | Openness
+  | Only_outer_closed (* It's only dangerous in one direction *)
   | Missing of position * string
   | Presence of string
   | Incompatible_types_for of string
-  | Types of Env.t * Errortrace.comparison Errortrace.t
+  | Types of Errortrace.equality_error
 
 type private_object_mismatch =
   | Missing of string
-  | Types of Env.t * Errortrace.comparison Errortrace.t
+  | Types of Errortrace.equality_error
 
 type type_mismatch =
   | Arity
   | Privacy
   | Kind
-  | Constraint of Env.t * Errortrace.comparison Errortrace.t
-  | Manifest of Env.t * Errortrace.comparison Errortrace.t
+  | Constraint of Errortrace.equality_error
+  | Manifest of Errortrace.equality_error
   | Private_variant of type_expr * type_expr * private_variant_mismatch
   | Private_object of type_expr * type_expr * private_object_mismatch
   | Variance
@@ -188,25 +189,63 @@ type type_mismatch =
   | Unboxed_representation of position
   | Immediate of Type_immediacy.Violation.t
 
-let report_label_mismatch first second ppf err =
+let report_primitive_mismatch first second ppf err =
   let pr fmt = Format.fprintf ppf fmt in
+  match (err : primitive_mismatch) with
+  | Name ->
+      pr "The names of the primitives are not the same"
+  | Arity ->
+      pr "The syntactic arities of these primitives were not the same@ \
+          (They must have the same number of ->s present in the source)"
+  | No_alloc ord ->
+      pr "%s primitive is [@@@@noalloc] but %s is not"
+        (String.capitalize_ascii (choose ord first second))
+        (choose_other ord first second)
+  | Native_name ->
+      pr "The native names of the primitives are not the same"
+  | Result_repr ->
+      pr "The two primitives' results have different representations"
+  | Argument_repr n ->
+      pr "The two primitives' %d%s arguments have different representations"
+        n (Misc.ordinal_suffix n)
+
+let report_value_mismatch first second env ppf err =
+  let pr fmt = Format.fprintf ppf fmt in
+  pr "@ ";
+  match (err : value_mismatch) with
+  | Primitive_mismatch pm ->
+      report_primitive_mismatch first second ppf pm
+  | Not_a_primitive ->
+      pr "The definition is not a primitive"
+  | Type trace ->
+      Printtyp.report_moregen_error ppf env trace
+        (fun ppf -> Format.fprintf ppf "The type")
+        (fun ppf -> Format.fprintf ppf "is not compatible with the type")
+
+let report_type_inequality env ppf err =
+  Printtyp.report_equality_error ppf env err
+    (fun ppf -> Format.fprintf ppf "The type")
+    (fun ppf -> Format.fprintf ppf "is not equal to the type")
+
+let report_label_mismatch first second env ppf err =
   match (err : label_mismatch) with
-  | Type _ -> pr "The types are not equal."
+  | Type err ->
+      report_type_inequality env ppf err
   | Mutability ord ->
-      pr "%s is mutable and %s is not."
-        (String.capitalize_ascii  (choose ord first second))
+      Format.fprintf ppf "%s is mutable and %s is not."
+        (String.capitalize_ascii (choose ord first second))
         (choose_other ord first second)
 
-let report_record_mismatch first second decl ppf err =
+let report_record_mismatch first second decl env ppf err =
   let pr fmt = Format.fprintf ppf fmt in
   match err with
   | Label_mismatch (l1, l2, err) ->
       pr
-        "@[<hv>Fields do not match:@;<1 2>%a@ is not compatible with:\
+        "@[<hv>Fields do not match:@;<1 2>%a@ is not the same as:\
          @;<1 2>%a@ %a@]"
         Printtyp.label l1
         Printtyp.label l2
-        (report_label_mismatch first second) err
+        (report_label_mismatch first second env) err
   | Label_names (n, name1, name2) ->
       pr "@[<hv>Fields number %i have different names, %s and %s.@]"
         n (Ident.name name1) (Ident.name name2)
@@ -218,12 +257,12 @@ let report_record_mismatch first second decl ppf err =
         (choose ord first second) decl
         "uses unboxed float representation"
 
-let report_constructor_mismatch first second decl ppf err =
+let report_constructor_mismatch first second decl env ppf err =
   let pr fmt  = Format.fprintf ppf fmt in
   match (err : constructor_mismatch) with
-  | Type _ -> pr "The types are not equal."
+  | Type err -> report_type_inequality env ppf err
   | Arity -> pr "They have different arities."
-  | Inline_record err -> report_record_mismatch first second decl ppf err
+  | Inline_record err -> report_record_mismatch first second decl env ppf err
   | Kind ord ->
       pr "%s uses inline records and %s doesn't."
         (String.capitalize_ascii (choose ord first second))
@@ -233,16 +272,16 @@ let report_constructor_mismatch first second decl ppf err =
         (String.capitalize_ascii (choose ord first second))
         (choose_other ord first second)
 
-let report_variant_mismatch first second decl ppf err =
+let report_variant_mismatch first second decl env ppf err =
   let pr fmt = Format.fprintf ppf fmt in
   match (err : variant_mismatch) with
   | Constructor_mismatch (c1, c2, err) ->
       pr
-        "@[<hv>Constructors do not match:@;<1 2>%a@ is not compatible with:\
+        "@[<hv>Constructors do not match:@;<1 2>%a@ is not the same as:\
          @;<1 2>%a@ %a@]"
         Printtyp.constructor c1
         Printtyp.constructor c2
-        (report_constructor_mismatch first second decl) err
+        (report_constructor_mismatch first second decl env) err
   | Constructor_names (n, name1, name2) ->
       pr "Constructors number %i have different names, %s and %s."
         n (Ident.name name1) (Ident.name name2)
@@ -250,30 +289,68 @@ let report_variant_mismatch first second decl ppf err =
       pr "The constructor %s is only present in %s %s."
         (Ident.name s) (choose ord first second) decl
 
-let report_extension_constructor_mismatch first second decl ppf err =
+let report_extension_constructor_mismatch first second decl env ppf err =
   let pr fmt = Format.fprintf ppf fmt in
   match (err : extension_constructor_mismatch) with
   | Constructor_privacy -> pr "A private type would be revealed."
   | Constructor_mismatch (id, ext1, ext2, err) ->
-      pr "@[<hv>Constructors do not match:@;<1 2>%a@ is not compatible with:\
+      pr "@[<hv>Constructors do not match:@;<1 2>%a@ is not the same as:\
           @;<1 2>%a@ %a@]"
         (Printtyp.extension_only_constructor id) ext1
         (Printtyp.extension_only_constructor id) ext2
-        (report_constructor_mismatch first second decl) err
+        (report_constructor_mismatch first second decl env) err
 
-let report_type_mismatch0 first second decl ppf err =
+let report_private_variant_mismatch first second decl env ppf err =
   let pr fmt = Format.fprintf ppf fmt in
+  match (err : private_variant_mismatch) with
+  | Only_outer_closed ->
+      (* It's only dangerous in one direction, so we don't have a position *)
+      pr "%s is private and closed, but %s is not closed"
+        (String.capitalize_ascii second) first
+  | Missing (ord, name) ->
+      pr "The constructor %s is only present in %s %s."
+        name (choose ord first second) decl
+  | Presence s ->
+      pr "The tag `%s is present in the %s %s,@ but might not be in the %s"
+        s second decl first
+  | Incompatible_types_for s -> pr "Types for tag `%s are incompatible" s
+  | Types err ->
+      report_type_inequality env ppf err
+
+let report_private_object_mismatch env ppf err =
+  let pr fmt = Format.fprintf ppf fmt in
+  match (err : private_object_mismatch) with
+  | Missing s -> pr "The implementation is missing the method %s" s
+  | Types err -> report_type_inequality env ppf err
+
+let report_type_mismatch first second decl env ppf err =
+  let pr fmt = Format.fprintf ppf fmt in
+  pr "@ ";
   match err with
-  | Arity -> pr "They have different arities."
-  | Privacy -> pr "A private type would be revealed."
-  | Kind -> pr "Their kinds differ."
-  | Constraint _ -> pr "Their constraints differ."
-  | Manifest _ -> ()
-  | Private_variant _ -> ()
-  | Private_object _ -> ()
-  | Variance -> pr "Their variances do not agree."
-  | Record_mismatch err -> report_record_mismatch first second decl ppf err
-  | Variant_mismatch err -> report_variant_mismatch first second decl ppf err
+  | Arity ->
+      pr "They have different arities."
+  | Privacy ->
+      pr "A private type would be revealed."
+  | Kind ->
+      pr "Their kinds differ."
+  | Constraint err ->
+      (* This error can come from implicit parameter disagreement or from
+         explicit `constraint`s.  Both affect the parameters, hence this choice
+         of explanatory text *)
+      pr "Their parameters differ@,";
+      report_type_inequality env ppf err
+  | Manifest err ->
+      report_type_inequality env ppf err
+  | Private_variant (_ty1, _ty2, mismatch) ->
+      report_private_variant_mismatch first second decl env ppf mismatch
+  | Private_object (_ty1, _ty2, mismatch) ->
+      report_private_object_mismatch env ppf mismatch
+  | Variance ->
+      pr "Their variances do not agree."
+  | Record_mismatch err ->
+      report_record_mismatch first second decl env ppf err
+  | Variant_mismatch err ->
+      report_variant_mismatch first second decl env ppf err
   | Unboxed_representation ord ->
       pr "Their internal representations differ:@ %s %s %s."
          (choose ord first second) decl
@@ -287,13 +364,6 @@ let report_type_mismatch0 first second decl ppf err =
           pr "%s is not a type that is always immediate on 64 bit platforms."
             first
 
-let report_type_mismatch first second decl ppf err =
-  match err with
-  | Manifest _ -> ()
-  | Private_variant _ -> ()
-  | Private_object _ -> ()
-  | _ -> Format.fprintf ppf "@ %a" (report_type_mismatch0 first second decl) err
-
 let rec compare_constructor_arguments ~loc env params1 params2 arg1 arg2 =
   match arg1, arg2 with
   | Types.Cstr_tuple arg1, Types.Cstr_tuple arg2 ->
@@ -302,7 +372,7 @@ let rec compare_constructor_arguments ~loc env params1 params2 arg1 arg2 =
       else begin
         (* Ctype.equal must be called on all arguments at once, cf. PR#7378 *)
         match Ctype.equal env true (params1 @ arg1) (params2 @ arg2) with
-        | exception Ctype.Equality trace -> Some (Type (env, trace))
+        | exception Ctype.Equality err -> Some (Type err)
         | () -> None
       end
   | Types.Cstr_record l1, Types.Cstr_record l2 ->
@@ -316,7 +386,7 @@ and compare_constructors ~loc env params1 params2 res1 res2 args1 args2 =
   match res1, res2 with
   | Some r1, Some r2 -> begin
       match Ctype.equal env true [r1] [r2] with
-      | exception Ctype.Equality trace -> Some (Type (env, trace))
+      | exception Ctype.Equality err -> Some (Type err)
       | () -> compare_constructor_arguments ~loc env [r1] [r2] args1 args2
     end
   | Some _, None -> Some (Explicit_return_type First)
@@ -357,8 +427,7 @@ and compare_labels env params1 params2
     let tl1 = params1 @ [ld1.ld_type] in
     let tl2 = params2 @ [ld2.ld_type] in
     match Ctype.equal env true tl1 tl2 with
-    | exception Ctype.Equality trace ->
-        Some (Type (env, trace) : label_mismatch)
+    | exception Ctype.Equality err -> Some (Type err : label_mismatch)
     | () -> None
   end
 
@@ -402,7 +471,7 @@ let private_variant env row1 params1 row2 params2 =
       Ctype.merge_row_fields row1.row_fields row2.row_fields
     in
     let err =
-      if row2.row_closed && not row1.row_closed then Some Openness
+      if row2.row_closed && not row1.row_closed then Some Only_outer_closed
       else begin
         match row2.row_closed, Ctype.filter_row_fields false r1 with
         | true, (s, _) :: _ ->
@@ -429,8 +498,8 @@ let private_variant env row1 params1 row2 params2 =
       match pairs with
       | [] -> begin
           match Ctype.equal env true tl1 tl2 with
-          | exception Ctype.Equality trace ->
-              Some (Types (env, trace) : private_variant_mismatch)
+          | exception Ctype.Equality err ->
+              Some (Types err : private_variant_mismatch)
           | () -> None
         end
       | (s, f1, f2) :: pairs -> begin
@@ -482,11 +551,11 @@ let private_object env fields1 params1 fields2 params2 =
   in
   begin
     match Ctype.equal env true (params1 @ tl1) (params2 @ tl2) with
-    | exception Ctype.Equality trace -> Some (Types (env, trace))
+    | exception Ctype.Equality err -> Some (Types err)
     | () -> None
   end
 
-let type_manifest env ty1 params1 ty2 params2 priv2 =
+let type_manifest env ty1 params1 ty2 params2 priv2 kind2 =
   let ty1' = Ctype.expand_head env ty1 and ty2' = Ctype.expand_head env ty2 in
   match ty1'.desc, ty2'.desc with
   | Tvariant row1, Tvariant row2
@@ -507,14 +576,28 @@ let type_manifest env ty1 params1 ty2 params2 priv2 =
       | Some err -> Some (Private_object(ty1, ty2, err))
     end
   | _ -> begin
-    match
-      match priv2 with
-      | Private -> Ctype.equal_private env params1 ty1 params2 ty2
-      | Public -> Ctype.equal env true (params1 @ [ty1]) (params2 @ [ty2])
-    with
-    | exception Ctype.Equality trace -> Some (Manifest (env, trace))
-    | () -> None
-  end
+      let is_private_abbrev_2 =
+        match priv2, kind2 with
+        | Private, Type_abstract -> begin
+            (* Same checks as the [when] guards from above, inverted *)
+            match ty2'.desc with
+            | Tvariant row ->
+                not (is_absrow env (Btype.row_more row))
+            | Tobject (fi, _) ->
+                not (is_absrow env (snd (Ctype.flatten_fields fi)))
+            | _ -> true
+          end
+        | _, _ -> false
+      in
+      match
+        if is_private_abbrev_2 then
+          Ctype.equal_private env params1 ty1 params2 ty2
+        else
+          Ctype.equal env true (params1 @ [ty1]) (params2 @ [ty2])
+      with
+      | exception Ctype.Equality err -> Some (Manifest err)
+      | () -> None
+    end
 
 let type_declarations ?(equality = false) ~loc env ~mark name
       decl1 path decl2 =
@@ -530,21 +613,21 @@ let type_declarations ?(equality = false) ~loc env ~mark name
       (_, None) ->
         begin
           match Ctype.equal env true decl1.type_params decl2.type_params with
-          | exception Ctype.Equality trace -> Some (Constraint(env, trace))
+          | exception Ctype.Equality err -> Some (Constraint err)
           | () -> None
         end
     | (Some ty1, Some ty2) ->
          type_manifest env ty1 decl1.type_params ty2 decl2.type_params
-           decl2.type_private
+           decl2.type_private decl2.type_kind
     | (None, Some ty2) ->
         let ty1 =
           Btype.newgenty (Tconstr(path, decl2.type_params, ref Mnil))
         in
         match Ctype.equal env true decl1.type_params decl2.type_params with
-        | exception Ctype.Equality trace -> Some (Constraint(env, trace))
+        | exception Ctype.Equality err -> Some (Constraint err)
         | () ->
           match Ctype.equal env false [ty1] [ty2] with
-          | exception Ctype.Equality trace -> Some (Manifest(env, trace))
+          | exception Ctype.Equality err -> Some (Manifest err)
           | () -> None
   in
   if err <> None then err else
@@ -648,8 +731,8 @@ let extension_constructors ~loc env ~mark id ext1 ext2 =
   let tl1 = ty1 :: ext1.ext_type_params in
   let tl2 = ty2 :: ext2.ext_type_params in
   match Ctype.equal env true tl1 tl2 with
-  | exception Ctype.Equality trace ->
-      Some (Constructor_mismatch (id, ext1, ext2, Type(env, trace)))
+  | exception Ctype.Equality err ->
+      Some (Constructor_mismatch (id, ext1, ext2, Type err))
   | () ->
     let r =
       compare_constructors ~loc env
diff --git a/typing/includecore.mli b/typing/includecore.mli
index 95bcbb23cb99..37a77ad907af 100644
--- a/typing/includecore.mli
+++ b/typing/includecore.mli
@@ -31,12 +31,12 @@ type primitive_mismatch =
 type value_mismatch =
   | Primitive_mismatch of primitive_mismatch
   | Not_a_primitive
-  | Type of Env.t * Errortrace.comparison Errortrace.t
+  | Type of Errortrace.moregen_error
 
 exception Dont_match of value_mismatch
 
 type label_mismatch =
-  | Type of Env.t * Errortrace.comparison Errortrace.t
+  | Type of Errortrace.equality_error
   | Mutability of position
 
 type record_mismatch =
@@ -46,7 +46,7 @@ type record_mismatch =
   | Unboxed_float_representation of position
 
 type constructor_mismatch =
-  | Type of Env.t * Errortrace.comparison Errortrace.t
+  | Type of Errortrace.equality_error
   | Arity
   | Inline_record of record_mismatch
   | Kind of position
@@ -67,22 +67,22 @@ type extension_constructor_mismatch =
                             * constructor_mismatch
 
 type private_variant_mismatch =
-  | Openness
+  | Only_outer_closed
   | Missing of position * string
   | Presence of string
   | Incompatible_types_for of string
-  | Types of Env.t * Errortrace.comparison Errortrace.t
+  | Types of Errortrace.equality_error
 
 type private_object_mismatch =
   | Missing of string
-  | Types of Env.t * Errortrace.comparison Errortrace.t
+  | Types of Errortrace.equality_error
 
 type type_mismatch =
   | Arity
   | Privacy
   | Kind
-  | Constraint of Env.t * Errortrace.comparison Errortrace.t
-  | Manifest of Env.t * Errortrace.comparison Errortrace.t
+  | Constraint of Errortrace.equality_error
+  | Manifest of Errortrace.equality_error
   | Private_variant of type_expr * type_expr * private_variant_mismatch
   | Private_object of type_expr * type_expr * private_object_mismatch
   | Variance
@@ -110,7 +110,17 @@ val class_types:
         Env.t -> class_type -> class_type -> bool
 *)
 
-val report_type_mismatch:
-    string -> string -> string -> Format.formatter -> type_mismatch -> unit
-val report_extension_constructor_mismatch: string -> string -> string ->
+val report_value_mismatch :
+  string -> string ->
+  Env.t ->
+  Format.formatter -> value_mismatch -> unit
+
+val report_type_mismatch :
+  string -> string -> string ->
+  Env.t ->
+  Format.formatter -> type_mismatch -> unit
+
+val report_extension_constructor_mismatch :
+  string -> string -> string ->
+  Env.t ->
   Format.formatter -> extension_constructor_mismatch -> unit
diff --git a/typing/includemod.ml b/typing/includemod.ml
index 1b542d5f5d6d..1b198356e38e 100644
--- a/typing/includemod.ml
+++ b/typing/includemod.ml
@@ -60,7 +60,7 @@ module Error = struct
   let sdiff x y = {got=x; expected=y; symptom=()}
 
   type core_sigitem_symptom =
-    | Value_descriptions of value_description core_diff
+    | Value_descriptions of (value_description, Includecore.value_mismatch) diff
     | Type_declarations of (type_declaration, Includecore.type_mismatch) diff
     | Extension_constructors of
         (extension_constructor, Includecore.extension_constructor_mismatch) diff
@@ -159,8 +159,8 @@ let value_descriptions ~loc env ~mark subst id vd1 vd2 =
   let vd2 = Subst.value_description subst vd2 in
   try
     Ok (Includecore.value_descriptions ~loc env (Ident.name id) vd1 vd2)
-  with Includecore.Dont_match _err ->
-    Error Error.(Core (Value_descriptions (sdiff vd1 vd2)))
+  with Includecore.Dont_match err ->
+    Error Error.(Core (Value_descriptions (diff vd1 vd2 err)))
 
 (* Inclusion between type declarations *)
 
diff --git a/typing/includemod.mli b/typing/includemod.mli
index f4bd3a6f118c..ff350faf5d75 100644
--- a/typing/includemod.mli
+++ b/typing/includemod.mli
@@ -45,7 +45,8 @@ module Error: sig
     | Unit
 
   type core_sigitem_symptom =
-    | Value_descriptions of Types.value_description core_diff
+    | Value_descriptions of
+        (Types.value_description, Includecore.value_mismatch) diff
     | Type_declarations of
         (Types.type_declaration, Includecore.type_mismatch) diff
     | Extension_constructors of
diff --git a/typing/includemod_errorprinter.ml b/typing/includemod_errorprinter.ml
index 013275b57b05..0a802010bd8b 100644
--- a/typing/includemod_errorprinter.ml
+++ b/typing/includemod_errorprinter.ml
@@ -607,15 +607,18 @@ let subcase_list l ppf = match l with
         (List.rev l)
 
 (* Printers for leaves *)
-let core id x =
+let core env id x =
   match x with
   | Err.Value_descriptions diff ->
-      let t1 = Printtyp.tree_of_value_description id diff.got in
-      let t2 = Printtyp.tree_of_value_description id diff.expected in
-      Format.dprintf
-        "@[<hv 2>Values do not match:@ %a@;<1 -2>is not included in@ %a@]%a%t"
-        !Oprint.out_sig_item t1
-        !Oprint.out_sig_item t2
+      Format.dprintf "@[<v>@[<hv>%s:@;<1 2>%a@ %s@;<1 2>%a@]%a%a%t@]"
+        "Values do not match"
+        !Oprint.out_sig_item
+        (Printtyp.tree_of_value_description id diff.got)
+        "is not included in"
+        !Oprint.out_sig_item
+        (Printtyp.tree_of_value_description id diff.expected)
+        (Includecore.report_value_mismatch
+           "the first" "the second" env) diff.symptom
         show_locs (diff.got.val_loc, diff.expected.val_loc)
         Printtyp.Conflicts.print_explanations
   | Err.Type_declarations diff ->
@@ -627,7 +630,7 @@ let core id x =
         !Oprint.out_sig_item
         (Printtyp.tree_of_type_declaration id diff.expected Trec_first)
         (Includecore.report_type_mismatch
-           "the first" "the second" "declaration") diff.symptom
+           "the first" "the second" "declaration" env) diff.symptom
         show_locs (diff.got.type_loc, diff.expected.type_loc)
         Printtyp.Conflicts.print_explanations
   | Err.Extension_constructors diff ->
@@ -639,7 +642,7 @@ let core id x =
         !Oprint.out_sig_item
         (Printtyp.tree_of_extension_constructor id diff.expected Text_first)
         (Includecore.report_extension_constructor_mismatch
-           "the first" "the second" "declaration") diff.symptom
+           "the first" "the second" "declaration" env) diff.symptom
         show_locs (diff.got.ext_loc, diff.expected.ext_loc)
         Printtyp.Conflicts.print_explanations
   | Err.Class_type_declarations diff ->
@@ -777,7 +780,7 @@ and signature ~expansion_token ~env:_ ~before ~ctx sgs =
     )
 and sigitem ~expansion_token ~env ~before ~ctx (name,s) = match s with
   | Core c ->
-      dwith_context ctx (core name c):: before
+      dwith_context ctx (core env name c) :: before
   | Module_type diff ->
       module_type ~expansion_token ~eqmode:false ~env ~before
         ~ctx:(Context.Module name :: ctx) diff
@@ -864,7 +867,7 @@ let all env = function
       let first = Location.msg "%a" interface_mismatch diff in
       signature ~expansion_token:true ~env ~before:[first] ~ctx:[] diff.symptom
   | In_Type_declaration (id,reason) ->
-      [Location.msg "%t" (core id reason)]
+      [Location.msg "%t" (core env id reason)]
   | In_Module_type diff ->
       module_type ~expansion_token:true ~eqmode:false ~before:[] ~env ~ctx:[]
         diff
diff --git a/typing/printtyp.ml b/typing/printtyp.ml
index 8c189832d8e1..47f8075a7fc4 100644
--- a/typing/printtyp.ml
+++ b/typing/printtyp.ml
@@ -782,77 +782,143 @@ let best_type_path p =
 
 (* Print a type expression *)
 
-let names = ref ([] : (type_expr * string) list)
-let name_counter = ref 0
-let named_vars = ref ([] : string list)
+module Names : sig
+  val reset_names : unit -> unit
 
-let weak_counter = ref 1
-let weak_var_map = ref TypeMap.empty
-let named_weak_vars = ref String.Set.empty
+  val add_named_var : type_expr -> unit
+  val add_subst : (type_expr * type_expr) list -> unit
 
-let reset_names () = names := []; name_counter := 0; named_vars := []
-let add_named_var ty =
-  match ty.desc with
-    Tvar (Some name) | Tunivar (Some name) ->
-      if List.mem name !named_vars then () else
-      named_vars := name :: !named_vars
-  | _ -> ()
+  val has_name : type_expr -> bool
 
-let name_is_already_used name =
-  List.mem name !named_vars
-  || List.exists (fun (_, name') -> name = name') !names
-  || String.Set.mem name !named_weak_vars
-
-let rec new_name () =
-  let name =
-    if !name_counter < 26
-    then String.make 1 (Char.chr(97 + !name_counter))
-    else String.make 1 (Char.chr(97 + !name_counter mod 26)) ^
-           Int.to_string(!name_counter / 26) in
-  incr name_counter;
-  if name_is_already_used name then new_name () else name
-
-let rec new_weak_name ty () =
-  let name = "weak" ^ Int.to_string !weak_counter in
-  incr weak_counter;
-  if name_is_already_used name then new_weak_name ty ()
-  else begin
-      named_weak_vars := String.Set.add name !named_weak_vars;
-      weak_var_map := TypeMap.add ty name !weak_var_map;
-      name
-    end
+  val new_name : unit -> string
+  val new_weak_name : type_expr -> unit -> string
+
+  val name_of_type : (unit -> string) -> type_expr -> string
+  val check_name_of_type : type_expr -> unit
+
+  val remove_names : type_expr list -> unit
+
+  val with_local_names : (unit -> 'a) -> 'a
+
+  (* For [print_items], which is itself for the toplevel *)
+  val refresh_weak :
+    (type_expr ->
+     string ->
+     string TypeMap.t * String.Set.t ->
+     string TypeMap.t * String.Set.t) ->
+    unit
+end = struct
+  (* We map from types to names, but not directly; we also store a substitution,
+     which maps from types to types.  The lookup process is
+     "type -> apply substitution -> find name".  The substitution is presumed to
+     be acyclic. *)
+  let names = ref ([] : (type_expr * string) list)
+  let name_subst = ref ([] : (type_expr * type_expr) list)
+  let name_counter = ref 0
+  let named_vars = ref ([] : string list)
+
+  let weak_counter = ref 1
+  let weak_var_map = ref TypeMap.empty
+  let named_weak_vars = ref String.Set.empty
+
+  let reset_names () =
+    names := []; name_subst := []; name_counter := 0; named_vars := []
+
+  let add_named_var ty =
+    match ty.desc with
+      Tvar (Some name) | Tunivar (Some name) ->
+        if List.mem name !named_vars then () else
+        named_vars := name :: !named_vars
+    | _ -> ()
+
+  let rec substitute ty =
+    match List.assq ty !name_subst with
+    | ty' -> substitute ty'
+    | exception Not_found -> ty
 
-let name_of_type name_generator t =
-  (* We've already been through repr at this stage, so t is our representative
-     of the union-find class. *)
-  try List.assq t !names with Not_found ->
-    try TypeMap.find t !weak_var_map with Not_found ->
+  let add_subst subst =
+    name_subst := subst @ !name_subst
+
+  let has_name ty =
+    List.mem_assq (substitute ty) !names
+
+  let name_is_already_used name =
+    List.mem name !named_vars
+    || List.exists (fun (_, name') -> name = name') !names
+    || String.Set.mem name !named_weak_vars
+
+  let rec new_name () =
     let name =
-      match t.desc with
-        Tvar (Some name) | Tunivar (Some name) ->
-          (* Some part of the type we've already printed has assigned another
-           * unification variable to that name. We want to keep the name, so try
-           * adding a number until we find a name that's not taken. *)
-          let current_name = ref name in
-          let i = ref 0 in
-          while List.exists (fun (_, name') -> !current_name = name') !names do
-            current_name := name ^ (Int.to_string !i);
-            i := !i + 1;
-          done;
-          !current_name
-      | _ ->
-          (* No name available, create a new one *)
-          name_generator ()
-    in
-    (* Exception for type declarations *)
-    if name <> "_" then names := (t, name) :: !names;
-    name
+      if !name_counter < 26
+      then String.make 1 (Char.chr(97 + !name_counter))
+      else String.make 1 (Char.chr(97 + !name_counter mod 26)) ^
+             Int.to_string(!name_counter / 26) in
+    incr name_counter;
+    if name_is_already_used name then new_name () else name
+
+  let rec new_weak_name ty () =
+    let name = "weak" ^ Int.to_string !weak_counter in
+    incr weak_counter;
+    if name_is_already_used name then new_weak_name ty ()
+    else begin
+        named_weak_vars := String.Set.add name !named_weak_vars;
+        weak_var_map := TypeMap.add ty name !weak_var_map;
+        name
+      end
 
-let check_name_of_type t = ignore(name_of_type new_name t)
+  let name_of_type name_generator t =
+    (* We've already been through repr at this stage, so t is our representative
+       of the union-find class. *)
+    let t = substitute t in
+    try List.assq t !names with Not_found ->
+      try TypeMap.find t !weak_var_map with Not_found ->
+      let name =
+        match t.desc with
+          Tvar (Some name) | Tunivar (Some name) ->
+            (* Some part of the type we've already printed has assigned another
+             * unification variable to that name. We want to keep the name, so
+             * try adding a number until we find a name that's not taken. *)
+            let current_name = ref name in
+            let i = ref 0 in
+            while List.exists
+                    (fun (_, name') -> !current_name = name')
+                    !names
+            do
+              current_name := name ^ (Int.to_string !i);
+              i := !i + 1;
+            done;
+            !current_name
+        | _ ->
+            (* No name available, create a new one *)
+            name_generator ()
+      in
+      (* Exception for type declarations *)
+      if name <> "_" then names := (t, name) :: !names;
+      name
 
-let remove_names tyl =
-  let tyl = List.map repr tyl in
-  names := List.filter (fun (ty,_) -> not (List.memq ty tyl)) !names
+  let check_name_of_type t = ignore(name_of_type new_name t)
+
+  let remove_names tyl =
+    let tyl = List.map (fun ty -> substitute (repr ty)) tyl in
+    names := List.filter (fun (ty,_) -> not (List.memq ty tyl)) !names
+
+  let with_local_names f =
+    let old_names = !names in
+    let old_subst = !name_subst in
+    names      := [];
+    name_subst := [];
+    try_finally
+      ~always:(fun () ->
+        names      := old_names;
+        name_subst := old_subst)
+      f
+
+  let refresh_weak refresh =
+    let m, s =
+      TypeMap.fold refresh !weak_var_map (TypeMap.empty ,String.Set.empty)  in
+    named_weak_vars := s;
+    weak_var_map := m
+end
 
 let visited_objects = ref ([] : type_expr list)
 let aliased = ref ([] : type_expr list)
@@ -866,7 +932,7 @@ let add_alias ty =
   let px = proxy ty in
   if not (is_aliased px) then begin
     aliased := px :: !aliased;
-    add_named_var px
+    Names.add_named_var px
   end
 
 let aliasable ty =
@@ -892,7 +958,7 @@ let rec mark_loops_rec visited ty =
   if List.memq px visited && aliasable ty then add_alias px else
     let visited = px :: visited in
     match ty.desc with
-    | Tvar _ -> add_named_var ty
+    | Tvar _ -> Names.add_named_var ty
     | Tarrow(_, ty1, ty2, _) ->
         mark_loops_rec visited ty1; mark_loops_rec visited ty2
     | Ttuple tyl -> List.iter (mark_loops_rec visited) tyl
@@ -940,7 +1006,7 @@ let rec mark_loops_rec visited ty =
     | Tpoly (ty, tyl) ->
         List.iter (fun t -> add_alias t) tyl;
         mark_loops_rec visited ty
-    | Tunivar _ -> add_named_var ty
+    | Tunivar _ -> Names.add_named_var ty
 
 let mark_loops ty =
   normalize_type ty;
@@ -950,7 +1016,7 @@ let reset_loop_marks () =
   visited_objects := []; aliased := []; delayed := []
 
 let reset_except_context () =
-  reset_names (); reset_loop_marks ()
+  Names.reset_names (); reset_loop_marks ()
 
 let reset () =
   reset_naming_context (); Conflicts.reset ();
@@ -968,9 +1034,12 @@ let print_labels = ref true
 let rec tree_of_typexp sch ty =
   let ty = repr ty in
   let px = proxy ty in
-  if List.mem_assq px !names && not (List.memq px !delayed) then
+  if Names.has_name px && not (List.memq px !delayed) then
    let mark = is_non_gen sch ty in
-   let name = name_of_type (if mark then new_weak_name ty else new_name) px in
+   let name = Names.name_of_type
+                (if mark then Names.new_weak_name ty else Names.new_name)
+                px
+   in
    Otyp_var (mark, name) else
 
   let pr_typ () =
@@ -979,8 +1048,10 @@ let rec tree_of_typexp sch ty =
         (*let lev =
           if is_non_gen sch ty then "/" ^ Int.to_string ty.level else "" in*)
         let non_gen = is_non_gen sch ty in
-        let name_gen = if non_gen then new_weak_name ty else new_name in
-        Otyp_var (non_gen, name_of_type name_gen ty)
+        let name_gen =
+          if non_gen then Names.new_weak_name ty else Names.new_name
+        in
+        Otyp_var (non_gen, Names.name_of_type name_gen ty)
     | Tarrow(l, ty1, ty2, _) ->
         let lab =
           if !print_labels || is_optional l then string_of_label l else ""
@@ -1059,14 +1130,14 @@ let rec tree_of_typexp sch ty =
           (* Make the names delayed, so that the real type is
              printed once when used as proxy *)
           List.iter add_delayed tyl;
-          let tl = List.map (name_of_type new_name) tyl in
+          let tl = List.map (Names.name_of_type Names.new_name) tyl in
           let tr = Otyp_poly (tl, tree_of_typexp sch ty) in
           (* Forget names when we leave scope *)
-          remove_names tyl;
+          Names.remove_names tyl;
           delayed := old_delayed; tr
         end
     | Tunivar _ ->
-        Otyp_var (false, name_of_type new_name ty)
+        Otyp_var (false, Names.name_of_type Names.new_name ty)
     | Tpackage (p, fl) ->
         let fl =
           List.map
@@ -1078,8 +1149,8 @@ let rec tree_of_typexp sch ty =
   in
   if List.memq px !delayed then delayed := List.filter ((!=) px) !delayed;
   if is_aliased px && aliasable ty then begin
-    check_name_of_type px;
-    Otyp_alias (pr_typ (), name_of_type new_name px) end
+    Names.check_name_of_type px;
+    Otyp_alias (pr_typ (), Names.name_of_type Names.new_name px) end
   else pr_typ ()
 
 and tree_of_row_field sch (l, f) =
@@ -1164,7 +1235,7 @@ let type_path ppf p =
 
 (* Maxence *)
 let type_scheme_max ?(b_reset_names=true) ppf ty =
-  if b_reset_names then reset_names () ;
+  if b_reset_names then Names.reset_names () ;
   typexp true ppf ty
 (* End Maxence *)
 
@@ -1219,7 +1290,7 @@ let rec tree_of_type_decl id decl =
 
   List.iter add_alias params;
   List.iter mark_loops params;
-  List.iter check_name_of_type (List.map proxy params);
+  List.iter Names.check_name_of_type (List.map proxy params);
   let ty_manifest =
     match decl.type_manifest with
     | None -> None
@@ -1335,12 +1406,10 @@ and tree_of_constructor cd =
   match cd.cd_res with
   | None -> (name, arg (), None)
   | Some res ->
-      let nm = !names in
-      names := [];
-      let ret = tree_of_typexp false res in
-      let args = arg () in
-      names := nm;
-      (name, args, Some ret)
+      Names.with_local_names (fun () ->
+        let ret = tree_of_typexp false res in
+        let args = arg () in
+        (name, args, Some ret))
 
 and tree_of_label l =
   (Ident.name l.ld_id, l.ld_mutable = Mutable, tree_of_typexp false l.ld_type)
@@ -1369,12 +1438,10 @@ let extension_constructor_args_and_ret_type_subtree ext_args ext_ret_type =
   match ext_ret_type with
   | None -> (tree_of_constructor_arguments ext_args, None)
   | Some res ->
-    let nm = !names in
-    names := [];
-    let ret = tree_of_typexp false res in
-    let args = tree_of_constructor_arguments ext_args in
-    names := nm;
-    (args, Some ret)
+      Names.with_local_names (fun () ->
+        let ret = tree_of_typexp false res in
+        let args = tree_of_constructor_arguments ext_args in
+        (args, Some ret))
 
 let tree_of_extension_constructor id ext es =
   reset_except_context ();
@@ -1382,7 +1449,7 @@ let tree_of_extension_constructor id ext es =
   let ty_params = filter_params ext.ext_type_params in
   List.iter add_alias ty_params;
   List.iter mark_loops ty_params;
-  List.iter check_name_of_type (List.map proxy ty_params);
+  List.iter Names.check_name_of_type (List.map proxy ty_params);
   mark_loops_constructor_arguments ext.ext_args;
   Option.iter mark_loops ext.ext_ret_type;
   let type_param =
@@ -1465,7 +1532,7 @@ let tree_of_metho sch concrete csil (lab, kind, ty) =
     let virt = not (Concr.mem lab concrete) in
     let (ty, tyl) = method_type (lab, kind, ty) in
     let tty = tree_of_typexp sch ty in
-    remove_names tyl;
+    Names.remove_names tyl;
     Ocsg_method (lab, priv, virt, tty) :: csil
   end
   else csil
@@ -1508,7 +1575,7 @@ let rec tree_of_class_type sch params =
       let sty = repr sign.csig_self in
       let self_ty =
         if is_aliased sty then
-          Some (Otyp_var (false, name_of_type new_name (proxy sty)))
+          Some (Otyp_var (false, Names.name_of_type Names.new_name (proxy sty)))
         else None
       in
       let (fields, _) =
@@ -1577,8 +1644,8 @@ let tree_of_class_declaration id cl rs =
   let sty = Ctype.self_type cl.cty_type in
   List.iter mark_loops params;
 
-  List.iter check_name_of_type (List.map proxy params);
-  if is_aliased sty then check_name_of_type (proxy sty);
+  List.iter Names.check_name_of_type (List.map proxy params);
+  if is_aliased sty then Names.check_name_of_type (proxy sty);
 
   let vir_flag = cl.cty_new = None in
   Osig_class
@@ -1599,8 +1666,8 @@ let tree_of_cltype_declaration id cl rs =
   let sty = Ctype.self_type cl.clty_type in
   List.iter mark_loops params;
 
-  List.iter check_name_of_type (List.map proxy params);
-  if is_aliased sty then check_name_of_type (proxy sty);
+  List.iter Names.check_name_of_type (List.map proxy params);
+  if is_aliased sty then Names.check_name_of_type (proxy sty);
 
   let sign = Ctype.signature_of_class_type cl.clty_type in
 
@@ -1822,17 +1889,13 @@ let modtype_declaration id ppf decl =
 
 (* Refresh weak variable map in the toplevel *)
 let refresh_weak () =
-  let refresh t name (m,s) =
+  Names.refresh_weak (fun t name (m,s) ->
     if is_non_gen true (repr t) then
       begin
         TypeMap.add t name m,
         String.Set.add name s
       end
-    else m, s in
-  let m, s =
-    TypeMap.fold refresh !weak_var_map (TypeMap.empty ,String.Set.empty)  in
-  named_weak_vars := s;
-  weak_var_map := m
+    else m, s)
 
 let print_items showval env x =
   refresh_weak();
@@ -2096,10 +2159,18 @@ let explain_variant (type variety) : variety Errortrace.variant -> _ = function
       (* this case never happens *)
       None
   (* Equality & Moregen *)
+  | Errortrace.Presence_not_guaranteed_for (pos, s) -> Some(
+      dprintf
+        "@,@[The tag `%s is guaranteed to be present in the %a variant type,\
+         @ but not in the %a@]"
+        s
+        Errortrace.print_pos (Errortrace.swap_position pos)
+        Errortrace.print_pos pos
+    )
   | Errortrace.Openness pos ->
-    Some(dprintf "@,The %a variant type is open and the %a is not"
-           Errortrace.print_pos pos
-           Errortrace.print_pos (Errortrace.swap_position pos))
+      Some(dprintf "@,The %a variant type is open and the %a is not"
+             Errortrace.print_pos pos
+             Errortrace.print_pos (Errortrace.swap_position pos))
 
 let explain_escape pre = function
   | Errortrace.Univ u -> Some(
@@ -2216,8 +2287,11 @@ let warn_on_missing_defs env ppf = function
       warn_on_missing_def env ppf te1;
       warn_on_missing_def env ppf te2
 
-let error trace_format env tr txt1 ppf txt2 ty_expect_explanation =
+(* [subst] comes out of equality, and is [[]] otherwise *)
+let error trace_format subst env tr txt1 ppf txt2 ty_expect_explanation =
   reset ();
+  (* We want to substitute in the opposite order from [Eqtype] *)
+  Names.add_subst (List.map (fun (ty1,ty2) -> ty2,ty1) subst);
   let tr = prepare_trace (fun t t' -> t, hide_variant_name t') tr in
   let mis = mismatch txt1 env tr in
   match tr with
@@ -2247,18 +2321,23 @@ let error trace_format env tr txt1 ppf txt2 ty_expect_explanation =
       raise exn
 
 let report_error trace_format ppf env tr
+      ?(subst = [])
       ?(type_expected_explanation = fun _ -> ())
       txt1 txt2 =
-  wrap_printing_env env (fun () -> error trace_format env tr txt1 ppf txt2
+  wrap_printing_env env (fun () -> error trace_format subst env tr txt1 ppf txt2
                                      type_expected_explanation)
     ~error:true
 
-let report_unification_error =
-  report_error Unification
-let report_equality_error =
-  report_error Equality ?type_expected_explanation:None
-let report_moregen_error =
-  report_error Moregen ?type_expected_explanation:None
+let report_unification_error ppf env ({trace} : Errortrace.unification_error) =
+  report_error Unification ppf env ?subst:None trace
+let report_equality_error ppf env ({subst; trace} : Errortrace.equality_error) =
+  report_error Equality ppf env ~subst ?type_expected_explanation:None trace
+let report_moregen_error ppf env ({trace} : Errortrace.moregen_error) =
+  report_error Moregen ppf env ?subst:None ?type_expected_explanation:None trace
+
+let report_comparison_error ppf env = function
+  | Errortrace.Equality_error error -> report_equality_error ppf env error
+  | Errortrace.Moregen_error  error -> report_moregen_error  ppf env error
 
 module Subtype = struct
   (* There's a frustrating amount of code duplication between this module and
@@ -2315,7 +2394,8 @@ module Subtype = struct
     | Errortrace.Subtype.Diff diff ->
         Some (Errortrace.map_diff trees_of_type_expansion diff)
 
-  let report_error ppf env tr1 txt1 tr2 =
+  let report_error
+        ppf env tr1 txt1 ({trace=tr2} : Errortrace.unification_error) =
     wrap_printing_env ~error:true env (fun () ->
       reset ();
       let tr1 =
diff --git a/typing/printtyp.mli b/typing/printtyp.mli
index 01c76c89c7a4..d7e24c77f20e 100644
--- a/typing/printtyp.mli
+++ b/typing/printtyp.mli
@@ -113,7 +113,6 @@ val tree_of_type_scheme: type_expr -> out_type
 val type_sch : formatter -> type_expr -> unit
 val type_scheme: formatter -> type_expr -> unit
 (* Maxence *)
-val reset_names: unit -> unit
 val type_scheme_max: ?b_reset_names: bool ->
         formatter -> type_expr -> unit
 (* End Maxence *)
@@ -179,20 +178,26 @@ val report_ambiguous_type_error:
 
 val report_unification_error :
   formatter -> Env.t ->
-  Errortrace.unification Errortrace.t ->
+  Errortrace.unification_error ->
   ?type_expected_explanation:(formatter -> unit) ->
   (formatter -> unit) -> (formatter -> unit) ->
   unit
 
 val report_equality_error :
   formatter -> Env.t ->
-  Errortrace.comparison Errortrace.t ->
+  Errortrace.equality_error ->
   (formatter -> unit) -> (formatter -> unit) ->
   unit
 
 val report_moregen_error :
   formatter -> Env.t ->
-  Errortrace.comparison Errortrace.t ->
+  Errortrace.moregen_error ->
+  (formatter -> unit) -> (formatter -> unit) ->
+  unit
+
+val report_comparison_error :
+  formatter -> Env.t ->
+  Errortrace.comparison_error ->
   (formatter -> unit) -> (formatter -> unit) ->
   unit
 
@@ -202,7 +207,7 @@ module Subtype : sig
     Env.t ->
     Errortrace.Subtype.t ->
     string ->
-    Errortrace.unification Errortrace.t ->
+    Errortrace.unification_error ->
     unit
 end
 
diff --git a/typing/typeclass.ml b/typing/typeclass.ml
index 8d76f5343be8..4e4baa8bc9a1 100644
--- a/typing/typeclass.ml
+++ b/typing/typeclass.ml
@@ -66,8 +66,8 @@ type 'a full_class = {
 type class_env = { val_env : Env.t; met_env : Env.t; par_env : Env.t }
 
 type error =
-  | Unconsistent_constraint of Errortrace.unification Errortrace.t
-  | Field_type_mismatch of string * string * Errortrace.unification Errortrace.t
+  | Unconsistent_constraint of Errortrace.unification_error
+  | Field_type_mismatch of string * string * Errortrace.unification_error
   | Structure_expected of class_type
   | Cannot_apply of class_type
   | Apply_wrong_label of arg_label
@@ -76,10 +76,10 @@ type error =
   | Unbound_class_2 of Longident.t
   | Unbound_class_type_2 of Longident.t
   | Abbrev_type_clash of type_expr * type_expr * type_expr
-  | Constructor_type_mismatch of string * Errortrace.unification Errortrace.t
+  | Constructor_type_mismatch of string * Errortrace.unification_error
   | Virtual_class of bool * bool * string list * string list
   | Parameter_arity_mismatch of Longident.t * int * int
-  | Parameter_mismatch of Errortrace.unification Errortrace.t
+  | Parameter_mismatch of Errortrace.unification_error
   | Bad_parameters of Ident.t * type_expr * type_expr
   | Class_match_failure of Ctype.class_match_failure list
   | Unbound_val of string
@@ -87,8 +87,8 @@ type error =
   | Non_generalizable_class of Ident.t * Types.class_declaration
   | Cannot_coerce_self of type_expr
   | Non_collapsable_conjunction of
-      Ident.t * Types.class_declaration * Errortrace.unification Errortrace.t
-  | Final_self_clash of Errortrace.unification Errortrace.t
+      Ident.t * Types.class_declaration * Errortrace.unification_error
+  | Final_self_clash of Errortrace.unification_error
   | Mutability_mismatch of string * mutable_flag
   | No_overriding of string * string
   | Duplicate of string * string
@@ -274,18 +274,18 @@ let enter_met_env ?check loc lab kind unbound_kind ty class_env =
 let enter_val cl_num vars inh lab mut virt ty class_env loc =
   let val_env = class_env.val_env in
   let (id, virt) =
-    try
-      let (id, mut', virt', ty') = Vars.find lab !vars in
-      if mut' <> mut then
-        raise (Error(loc, val_env, Mutability_mismatch(lab, mut)));
-      Ctype.unify val_env (Ctype.instance ty) (Ctype.instance ty');
-      (if not inh then Some id else None),
-      (if virt' = Concrete then virt' else virt)
-    with
-      Ctype.Unify tr ->
-        raise (Error(loc, val_env,
-                     Field_type_mismatch("instance variable", lab, tr)))
-    | Not_found -> None, virt
+    match Vars.find lab !vars with
+    | exception Not_found -> None, virt
+    | (id, mut', virt', ty') ->
+        if mut' <> mut then
+          raise (Error(loc, val_env, Mutability_mismatch(lab, mut)));
+        match Ctype.unify val_env (Ctype.instance ty) (Ctype.instance ty') with
+        | () ->
+            (if not inh then Some id else None),
+            (if virt' = Concrete then virt' else virt)
+        | exception Ctype.Unify err ->
+            raise (Error(loc, val_env,
+                         Field_type_mismatch("instance variable", lab, err)))
   in
   let (id, _) as result =
     match id with Some id -> (id, class_env)
@@ -308,10 +308,12 @@ let inheritance self_type env ovf concr_meths warn_vals loc parent =
       (* Methods *)
       begin try
         Ctype.unify env self_type cl_sig.csig_self
-      with Ctype.Unify trace ->
+      with Ctype.Unify {trace} ->
         match trace with
         | Diff _ :: Incompatible_fields {name = n; _ } :: rem ->
-            raise(Error(loc, env, Field_type_mismatch ("method", n, rem)))
+            raise (Error(loc,
+                         env,
+                         Field_type_mismatch ("method", n, {trace = rem})))
         | _ -> assert false
       end;
 
@@ -355,8 +357,8 @@ let virtual_method val_env meths self_type lab priv sty loc =
   let cty = transl_simple_type val_env false sty in
   let ty = cty.ctyp_type in
   begin
-    try Ctype.unify val_env ty ty' with Ctype.Unify trace ->
-        raise(Error(loc, val_env, Field_type_mismatch ("method", lab, trace)));
+    try Ctype.unify val_env ty ty' with Ctype.Unify err ->
+        raise(Error(loc, val_env, Field_type_mismatch ("method", lab, err)));
   end;
   cty
 
@@ -367,8 +369,8 @@ let declare_method val_env meths self_type lab priv sty loc =
      Ctype.filter_self_method val_env lab priv meths self_type
   in
   let unif ty =
-    try Ctype.unify val_env ty ty' with Ctype.Unify trace ->
-      raise(Error(loc, val_env, Field_type_mismatch ("method", lab, trace)))
+    try Ctype.unify val_env ty ty' with Ctype.Unify err ->
+      raise(Error(loc, val_env, Field_type_mismatch ("method", lab, err)))
   in
   let sty = Ast_helper.Typ.force_poly sty in
   match sty.ptyp_desc, priv with
@@ -398,8 +400,8 @@ let type_constraint val_env sty sty' loc =
   let cty' = transl_simple_type val_env false sty' in
   let ty' = cty'.ctyp_type in
   begin
-    try Ctype.unify val_env ty ty' with Ctype.Unify trace ->
-        raise(Error(loc, val_env, Unconsistent_constraint trace));
+    try Ctype.unify val_env ty ty' with Ctype.Unify err ->
+        raise(Error(loc, val_env, Unconsistent_constraint err));
   end;
   (cty, cty')
 
@@ -547,8 +549,8 @@ and class_type_aux env scty =
           let cty' = transl_simple_type env false sty in
           let ty' = cty'.ctyp_type in
           begin
-           try Ctype.unify env ty' ty with Ctype.Unify trace ->
-                  raise(Error(sty.ptyp_loc, env, Parameter_mismatch trace))
+           try Ctype.unify env ty' ty with Ctype.Unify err ->
+                  raise(Error(sty.ptyp_loc, env, Parameter_mismatch err))
             end;
             cty'
         )       styl params
@@ -741,9 +743,9 @@ and class_field_aux self_loc cl_num self_type meths vars
           | _ -> assert false
           end
       | _ -> assert false
-      with Ctype.Unify trace ->
+      with Ctype.Unify err ->
         raise(Error(loc, val_env,
-                    Field_type_mismatch ("method", lab.txt, trace)))
+                    Field_type_mismatch ("method", lab.txt, err)))
       end;
       let meth_expr = make_method self_loc cl_num expr in
       (* backup variables for Pexp_override *)
@@ -905,7 +907,7 @@ and class_structure cl_num final val_env met_env loc
       Ctype.unify val_env private_self
         (Ctype.newty (Tobject(self_methods, ref None)));
       Ctype.unify val_env public_self self_type
-    with Ctype.Unify trace -> raise(Error(loc, val_env, Final_self_clash trace))
+    with Ctype.Unify err -> raise(Error(loc, val_env, Final_self_clash err))
     end;
   end;
 
@@ -964,8 +966,8 @@ and class_expr_aux cl_num val_env met_env scl =
       List.iter2
         (fun cty' ty ->
           let ty' = cty'.ctyp_type in
-           try Ctype.unify val_env ty' ty with Ctype.Unify trace ->
-             raise(Error(cty'.ctyp_loc, val_env, Parameter_mismatch trace)))
+           try Ctype.unify val_env ty' ty with Ctype.Unify err ->
+             raise(Error(cty'.ctyp_loc, val_env, Parameter_mismatch err)))
         tyl params;
       let cl =
         rc {cl_desc = Tcl_ident (path, lid, tyl);
@@ -1481,9 +1483,9 @@ let class_infos define_class kind
     Ctype.unify env
       (constructor_type constr obj_type)
       (Ctype.instance constr_type)
-  with Ctype.Unify trace ->
+  with Ctype.Unify err ->
     raise(Error(cl.pci_loc, env,
-                Constructor_type_mismatch (cl.pci_name.txt, trace)))
+                Constructor_type_mismatch (cl.pci_name.txt, err)))
   end;
 
   (* Class and class type temporary definitions *)
@@ -1614,8 +1616,8 @@ let final_decl env define_class
      arity, pub_meths, coe, expr) =
 
   begin try Ctype.collapse_conj_params env clty.cty_params
-  with Ctype.Unify trace ->
-    raise(Error(cl.pci_loc, env, Non_collapsable_conjunction (id, clty, trace)))
+  with Ctype.Unify err ->
+    raise(Error(cl.pci_loc, env, Non_collapsable_conjunction (id, clty, err)))
   end;
 
   (* make the dummy method disappear *)
@@ -1729,8 +1731,8 @@ let check_coercions env { id; id_loc; clty; ty_id; cltydef; obj_id; obj_abbr;
         | _ -> assert false
       in
       begin try Ctype.subtype env cl_ty obj_ty ()
-      with Ctype.Subtype (tr1, tr2) ->
-        raise(Typecore.Error(loc, env, Typecore.Not_subtype(tr1, tr2)))
+      with Ctype.Subtype (err1, err2) ->
+        raise(Typecore.Error(loc, env, Typecore.Not_subtype(err1, err2)))
       end;
       if not (Ctype.opened_object cl_ty) then
         raise(Error(loc, env, Cannot_coerce_self obj_ty))
@@ -1887,14 +1889,14 @@ open Format
 let report_error env ppf = function
   | Repeated_parameter ->
       fprintf ppf "A type parameter occurs several times"
-  | Unconsistent_constraint trace ->
+  | Unconsistent_constraint err ->
       fprintf ppf "@[<v>The class constraints are not consistent.@ ";
-      Printtyp.report_unification_error ppf env trace
+      Printtyp.report_unification_error ppf env err
         (fun ppf -> fprintf ppf "Type")
         (fun ppf -> fprintf ppf "is not compatible with type");
       fprintf ppf "@]"
-  | Field_type_mismatch (k, m, trace) ->
-      Printtyp.report_unification_error ppf env trace
+  | Field_type_mismatch (k, m, err) ->
+      Printtyp.report_unification_error ppf env err
         (function ppf ->
            fprintf ppf "The %s %s@ has type" k m)
         (function ppf ->
@@ -1931,8 +1933,8 @@ let report_error env ppf = function
         !Oprint.out_type (Printtyp.tree_of_typexp false abbrev)
         !Oprint.out_type (Printtyp.tree_of_typexp false actual)
         !Oprint.out_type (Printtyp.tree_of_typexp false expected)
-  | Constructor_type_mismatch (c, trace) ->
-      Printtyp.report_unification_error ppf env trace
+  | Constructor_type_mismatch (c, err) ->
+      Printtyp.report_unification_error ppf env err
         (function ppf ->
            fprintf ppf "The expression \"new %s\" has type" c)
         (function ppf ->
@@ -1959,8 +1961,8 @@ let report_error env ppf = function
         "@[The class constructor %a@ expects %i type argument(s),@ \
            but is here applied to %i type argument(s)@]"
         Printtyp.longident lid expected provided
-  | Parameter_mismatch trace ->
-      Printtyp.report_unification_error ppf env trace
+  | Parameter_mismatch err ->
+      Printtyp.report_unification_error ppf env err
         (function ppf ->
            fprintf ppf "The type parameter")
         (function ppf ->
@@ -2010,17 +2012,17 @@ let report_error env ppf = function
            the type of the current class:@ %a.@.\
            Some occurrences are contravariant@]"
         Printtyp.type_scheme ty
-  | Non_collapsable_conjunction (id, clty, trace) ->
+  | Non_collapsable_conjunction (id, clty, err) ->
       fprintf ppf
         "@[The type of this class,@ %a,@ \
            contains non-collapsible conjunctive types in constraints.@ %t@]"
         (Printtyp.class_declaration id) clty
-        (fun ppf -> Printtyp.report_unification_error ppf env trace
+        (fun ppf -> Printtyp.report_unification_error ppf env err
             (fun ppf -> fprintf ppf "Type")
             (fun ppf -> fprintf ppf "is not compatible with type")
         )
-  | Final_self_clash trace ->
-      Printtyp.report_unification_error ppf env trace
+  | Final_self_clash err ->
+      Printtyp.report_unification_error ppf env err
         (function ppf ->
            fprintf ppf "This object is expected to have type")
         (function ppf ->
diff --git a/typing/typeclass.mli b/typing/typeclass.mli
index ac8eb06ec508..6013b72ad6ec 100644
--- a/typing/typeclass.mli
+++ b/typing/typeclass.mli
@@ -90,8 +90,8 @@ val type_classes :
 *)
 
 type error =
-  | Unconsistent_constraint of Errortrace.unification Errortrace.t
-  | Field_type_mismatch of string * string * Errortrace.unification Errortrace.t
+  | Unconsistent_constraint of Errortrace.unification_error
+  | Field_type_mismatch of string * string * Errortrace.unification_error
   | Structure_expected of class_type
   | Cannot_apply of class_type
   | Apply_wrong_label of arg_label
@@ -100,10 +100,10 @@ type error =
   | Unbound_class_2 of Longident.t
   | Unbound_class_type_2 of Longident.t
   | Abbrev_type_clash of type_expr * type_expr * type_expr
-  | Constructor_type_mismatch of string * Errortrace.unification Errortrace.t
+  | Constructor_type_mismatch of string * Errortrace.unification_error
   | Virtual_class of bool * bool * string list * string list
   | Parameter_arity_mismatch of Longident.t * int * int
-  | Parameter_mismatch of Errortrace.unification Errortrace.t
+  | Parameter_mismatch of Errortrace.unification_error
   | Bad_parameters of Ident.t * type_expr * type_expr
   | Class_match_failure of Ctype.class_match_failure list
   | Unbound_val of string
@@ -111,8 +111,8 @@ type error =
   | Non_generalizable_class of Ident.t * Types.class_declaration
   | Cannot_coerce_self of type_expr
   | Non_collapsable_conjunction of
-      Ident.t * Types.class_declaration * Errortrace.unification Errortrace.t
-  | Final_self_clash of Errortrace.unification Errortrace.t
+      Ident.t * Types.class_declaration * Errortrace.unification_error
+  | Final_self_clash of Errortrace.unification_error
   | Mutability_mismatch of string * mutable_flag
   | No_overriding of string * string
   | Duplicate of string * string
diff --git a/typing/typecore.ml b/typing/typecore.ml
index 498ea5f3a33e..63ead1c62aa9 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -76,14 +76,14 @@ type existential_restriction =
 
 type error =
   | Constructor_arity_mismatch of Longident.t * int * int
-  | Label_mismatch of Longident.t * Errortrace.unification Errortrace.t
+  | Label_mismatch of Longident.t * Errortrace.unification_error
   | Pattern_type_clash :
-      Errortrace.unification Errortrace.t * _ pattern_desc option -> error
-  | Or_pattern_type_clash of Ident.t * Errortrace.unification Errortrace.t
+      Errortrace.unification_error * _ pattern_desc option -> error
+  | Or_pattern_type_clash of Ident.t * Errortrace.unification_error
   | Multiply_bound_variable of string
   | Orpat_vars of Ident.t * Ident.t list
   | Expr_type_clash of
-      Errortrace.unification Errortrace.t * type_forcing_context option
+      Errortrace.unification_error * type_forcing_context option
       * expression_desc option
   | Apply_non_function of type_expr
   | Apply_wrong_label of arg_label * type_expr * bool
@@ -102,17 +102,17 @@ type error =
   | Private_constructor of constructor_description * type_expr
   | Unbound_instance_variable of string * string list
   | Instance_variable_not_mutable of string
-  | Not_subtype of Errortrace.Subtype.t * Errortrace.unification Errortrace.t
+  | Not_subtype of Errortrace.Subtype.t * Errortrace.unification_error
   | Outside_class
   | Value_multiply_overridden of string
   | Coercion_failure of
-      type_expr * type_expr * Errortrace.unification Errortrace.t * bool
+      type_expr * type_expr * Errortrace.unification_error * bool
   | Too_many_arguments of bool * type_expr * type_forcing_context option
   | Abstract_wrong_label of arg_label * type_expr * type_forcing_context option
   | Scoping_let_module of string * type_expr
   | Not_a_variant_type of Longident.t
   | Incoherent_label_order
-  | Less_general of string * Errortrace.unification Errortrace.t
+  | Less_general of string * Errortrace.unification_error
   | Modules_not_allowed
   | Cannot_infer_signature
   | Not_a_packed_module of type_expr
@@ -132,9 +132,9 @@ type error =
   | Illegal_letrec_pat
   | Illegal_letrec_expr
   | Illegal_class_expr
-  | Letop_type_clash of string * Errortrace.unification Errortrace.t
-  | Andop_type_clash of string * Errortrace.unification Errortrace.t
-  | Bindings_type_clash of Errortrace.unification Errortrace.t
+  | Letop_type_clash of string * Errortrace.unification_error
+  | Andop_type_clash of string * Errortrace.unification_error
+  | Bindings_type_clash of Errortrace.unification_error
   | Unbound_existential of Ident.t list * type_expr
   | Missing_type_constraint
 
@@ -142,15 +142,15 @@ exception Error of Location.t * Env.t * error
 exception Error_forward of Location.error
 
 let trace_of_error = function
-    Label_mismatch (_,tr)
-  | Pattern_type_clash (tr,_)
-  | Or_pattern_type_clash (_,tr)
-  | Expr_type_clash (tr,_,_)
-  | Coercion_failure (_,_,tr,_)
-  | Less_general (_,tr)
-  | Letop_type_clash (_,tr)
-  | Andop_type_clash (_,tr)
-  | Bindings_type_clash tr -> Some tr
+    Label_mismatch (_,{trace})
+  | Pattern_type_clash ({trace},_)
+  | Or_pattern_type_clash (_,{trace})
+  | Expr_type_clash ({trace},_,_)
+  | Coercion_failure (_,_,{trace},_)
+  | Less_general (_,{trace})
+  | Letop_type_clash (_,{trace})
+  | Andop_type_clash (_,{trace})
+  | Bindings_type_clash {trace} -> Some trace
   | _ -> None
 
 (* Forward declaration, to be filled in by Typemod.type_module *)
@@ -312,8 +312,8 @@ let unify_exp_types loc env ty expected_ty =
   try
     unify env ty expected_ty
   with
-    Unify trace ->
-      raise(Error(loc, env, Expr_type_clash(trace, None, None)))
+    Unify err ->
+      raise(Error(loc, env, Expr_type_clash(err, None, None)))
   | Tags(l1,l2) ->
       raise(Typetexp.Error(loc, env, Typetexp.Variant_tags (l1, l2)))
 
@@ -337,8 +337,8 @@ let unify_pat_types_return_equated_pairs ?(refine = None) loc env ty ty' =
         unify !env ty ty';
         nothing_equated
   with
-  | Unify trace ->
-      raise(Error(loc, !env, Pattern_type_clash(trace, None)))
+  | Unify err ->
+      raise(Error(loc, !env, Pattern_type_clash(err, None)))
   | Tags(l1,l2) ->
       raise(Typetexp.Error(loc, !env, Typetexp.Variant_tags (l1, l2)))
 
@@ -347,8 +347,8 @@ let unify_pat_types ?refine loc env ty ty' =
 
 let unify_pat ?refine env pat expected_ty =
   try unify_pat_types ?refine pat.pat_loc env pat.pat_type expected_ty
-  with Error (loc, env, Pattern_type_clash(trace, None)) ->
-    raise(Error(loc, env, Pattern_type_clash(trace, Some pat.pat_desc)))
+  with Error (loc, env, Pattern_type_clash(err, None)) ->
+    raise(Error(loc, env, Pattern_type_clash(err, Some pat.pat_desc)))
 
 (* unification of a type with a Tconstr with freshly created arguments *)
 let unify_head_only ~refine loc env ty constr =
@@ -479,8 +479,8 @@ let enter_orpat_variables loc env  p1_vs p2_vs =
               unify_var env (newvar ()) t1;
               unify env t1 t2
             with
-            | Unify trace ->
-                raise(Error(loc, env, Or_pattern_type_clash(x1, trace)))
+            | Unify err ->
+                raise(Error(loc, env, Or_pattern_type_clash(x1, err)))
             end;
           (x2,x1)::unify_vars rem1 rem2
           end
@@ -716,9 +716,9 @@ let solve_Ppat_record_field ~refine loc env label label_lid record_ty =
   let (_, ty_arg, ty_res) = instance_label false label in
   begin try
     unify_pat_types ~refine loc env ty_res (instance record_ty)
-  with Error(_loc, _env, Pattern_type_clash(trace, _)) ->
+  with Error(_loc, _env, Pattern_type_clash(err, _)) ->
     raise(Error(label_lid.loc, !env,
-                Label_mismatch(label_lid.txt, trace)))
+                Label_mismatch(label_lid.txt, err)))
   end;
   end_def ();
   generalize_structure ty_res;
@@ -1303,8 +1303,8 @@ let rec has_literal_pattern p = match p.ppat_desc with
 
 let check_scope_escape loc env level ty =
   try Ctype.check_scope_escape env level ty
-  with Escape trace ->
-    raise(Error(loc, env, Pattern_type_clash([Escape trace], None)))
+  with Escape esc ->
+    raise(Error(loc, env, Pattern_type_clash({trace=[Escape esc]}, None)))
 
 type pattern_checking_mode =
   | Normal
@@ -2435,8 +2435,8 @@ let rec type_approx env sexp =
   | Pexp_constraint (e, sty) ->
       let ty = type_approx env e in
       let ty1 = approx_type env sty in
-      begin try unify env ty ty1 with Unify trace ->
-        raise(Error(sexp.pexp_loc, env, Expr_type_clash (trace, None, None)))
+      begin try unify env ty ty1 with Unify err ->
+        raise(Error(sexp.pexp_loc, env, Expr_type_clash (err, None, None)))
       end;
       ty1
   | Pexp_coerce (e, sty1, sty2) ->
@@ -2447,8 +2447,8 @@ let rec type_approx env sexp =
       let ty = type_approx env e
       and ty1 = approx_ty_opt sty1
       and ty2 = approx_type env sty2 in
-      begin try unify env ty ty1 with Unify trace ->
-        raise(Error(sexp.pexp_loc, env, Expr_type_clash (trace, None, None)))
+      begin try unify env ty ty1 with Unify err ->
+        raise(Error(sexp.pexp_loc, env, Expr_type_clash (err, None, None)))
       end;
       ty2
   | _ -> newvar ()
@@ -2490,8 +2490,10 @@ let check_univars env kind exp ty_expected vars =
   let ty, complete = polyfy env exp_ty vars in
   if not complete then
     let ty_expected = instance ty_expected in
-    raise (Error (exp.exp_loc, env,
-                  Less_general(kind, [Errortrace.diff ty ty_expected])))
+    raise (Error (exp.exp_loc,
+                  env,
+                  Less_general(kind,
+                               {trace = [Errortrace.diff ty ty_expected]})))
 
 let generalize_and_check_univars env kind exp ty_expected vars =
   generalize exp.exp_type;
@@ -2712,8 +2714,8 @@ let unify_exp env exp expected_ty =
   let loc = proper_exp_loc exp in
   try
     unify_exp_types loc env exp.exp_type expected_ty
-  with Error(loc, env, Expr_type_clash(trace, tfc, None)) ->
-    raise (Error(loc, env, Expr_type_clash(trace, tfc, Some exp.exp_desc)))
+  with Error(loc, env, Expr_type_clash(err, tfc, None)) ->
+    raise (Error(loc, env, Expr_type_clash(err, tfc, Some exp.exp_desc)))
 
 (* If [is_inferred e] is true, [e] will be typechecked without using
    the "expected type" provided by the context. *)
@@ -2733,9 +2735,9 @@ let with_explanation explanation f =
   | None -> f ()
   | Some explanation ->
       try f ()
-      with Error (loc', env', Expr_type_clash(trace', None, exp'))
+      with Error (loc', env', Expr_type_clash(err', None, exp'))
         when not loc'.Location.loc_ghost ->
-        let err = Expr_type_clash(trace', Some explanation, exp') in
+        let err = Expr_type_clash(err', Some explanation, exp') in
         raise (Error (loc', env', err))
 
 let rec type_exp ?recarg env sexp =
@@ -3352,10 +3354,10 @@ and type_expect_
             | _ ->
                 let ty, b = enlarge_type env ty' in
                 force ();
-                begin try Ctype.unify env arg.exp_type ty with Unify trace ->
+                begin try Ctype.unify env arg.exp_type ty with Unify err ->
                   let expanded = full_expand ~may_forget_scope:true env ty' in
                   raise(Error(sarg.pexp_loc, env,
-                              Coercion_failure(ty', expanded, trace, b)))
+                              Coercion_failure(ty', expanded, err, b)))
                 end
             end;
             (arg, ty', None, cty')
@@ -3817,8 +3819,8 @@ and type_expect_
       in
       begin try
         unify env op_type ty_op
-      with Unify trace ->
-        raise(Error(let_loc, env, Letop_type_clash(slet.pbop_op.txt, trace)))
+      with Unify err ->
+        raise(Error(let_loc, env, Letop_type_clash(slet.pbop_op.txt, err)))
       end;
       if !Clflags.principal then begin
         end_def ();
@@ -4263,8 +4265,8 @@ and type_label_exp create env loc ty_expected
   end;
   begin try
     unify env (instance ty_res) (instance ty_expected)
-  with Unify trace ->
-    raise (Error(lid.loc, env, Label_mismatch(lid.txt, trace)))
+  with Unify err ->
+    raise (Error(lid.loc, env, Label_mismatch(lid.txt, err)))
   end;
   (* Instantiate so that we can generalize internal nodes *)
   let ty_arg = instance ty_arg in
@@ -5280,8 +5282,8 @@ and type_andops env sarg sands expected_ty =
         let ty_op = newty (Tarrow(Nolabel, ty_rest, ty_rest_fun, Cok)) in
         begin try
           unify env op_type ty_op
-        with Unify trace ->
-          raise(Error(sop.loc, env, Andop_type_clash(sop.txt, trace)))
+        with Unify err ->
+          raise(Error(sop.loc, env, Andop_type_clash(sop.txt, err)))
         end;
         if !Clflags.principal then begin
           end_def ();
@@ -5293,8 +5295,8 @@ and type_andops env sarg sands expected_ty =
         let exp = type_expect env sexp (mk_expected ty_arg) in
         begin try
           unify env (instance ty_result) (instance expected_ty)
-        with Unify trace ->
-          raise(Error(loc, env, Bindings_type_clash(trace)))
+        with Unify err ->
+          raise(Error(loc, env, Bindings_type_clash(err)))
         end;
         let andop =
           { bop_op_name = sop;
@@ -5436,10 +5438,10 @@ let report_type_expected_explanation_opt expl ppf =
   | None -> ()
   | Some expl -> report_type_expected_explanation expl ppf
 
-let report_unification_error ~loc ?sub env trace
+let report_unification_error ~loc ?sub env err
     ?type_expected_explanation txt1 txt2 =
   Location.error_of_printer ~loc ?sub (fun ppf () ->
-    Printtyp.report_unification_error ppf env trace
+    Printtyp.report_unification_error ppf env err
       ?type_expected_explanation txt1 txt2
   ) ()
 
@@ -5449,24 +5451,24 @@ let report_error ~loc env = function
        "@[The constructor %a@ expects %i argument(s),@ \
         but is applied here to %i argument(s)@]"
        longident lid expected provided
-  | Label_mismatch(lid, trace) ->
-      report_unification_error ~loc env trace
+  | Label_mismatch(lid, err) ->
+      report_unification_error ~loc env err
         (function ppf ->
            fprintf ppf "The record field %a@ belongs to the type"
                    longident lid)
         (function ppf ->
            fprintf ppf "but is mixed here with fields of type")
-  | Pattern_type_clash (trace, pat) ->
-      let diff = type_clash_of_trace trace in
+  | Pattern_type_clash (err, pat) ->
+      let diff = type_clash_of_trace err.trace in
       let sub = report_pattern_type_clash_hints pat diff in
-      report_unification_error ~loc ~sub env trace
+      report_unification_error ~loc ~sub env err
         (function ppf ->
           fprintf ppf "This pattern matches values of type")
         (function ppf ->
           fprintf ppf "but a pattern was expected which matches values of \
                        type");
-  | Or_pattern_type_clash (id, trace) ->
-      report_unification_error ~loc env trace
+  | Or_pattern_type_clash (id, err) ->
+      report_unification_error ~loc env err
         (function ppf ->
           fprintf ppf "The variable %s on the left-hand side of this \
                        or-pattern has type" (Ident.name id))
@@ -5483,10 +5485,10 @@ let report_error ~loc env = function
           (Ident.name id);
         spellcheck_idents ppf id valid_idents
       ) ()
-  | Expr_type_clash (trace, explanation, exp) ->
-      let diff = type_clash_of_trace trace in
+  | Expr_type_clash (err, explanation, exp) ->
+      let diff = type_clash_of_trace err.trace in
       let sub = report_expr_type_clash_hints exp diff in
-      report_unification_error ~loc ~sub env trace
+      report_unification_error ~loc ~sub env err
         ~type_expected_explanation:
           (report_type_expected_explanation_opt explanation)
         (function ppf ->
@@ -5607,9 +5609,9 @@ let report_error ~loc env = function
       Location.errorf ~loc
         "The instance variable %s is overridden several times"
         v
-  | Coercion_failure (ty, ty', trace, b) ->
+  | Coercion_failure (ty, ty', err, b) ->
       Location.error_of_printer ~loc (fun ppf () ->
-        Printtyp.report_unification_error ppf env trace
+        Printtyp.report_unification_error ppf env err
           (function ppf ->
              let ty, ty' = Printtyp.prepare_expansion (ty, ty') in
              fprintf ppf "This expression cannot be coerced to type@;<1 2>%a;@ \
@@ -5669,8 +5671,8 @@ let report_error ~loc env = function
         "This function is applied to arguments@ \
         in an order different from other calls.@ \
         This is only allowed when the real type is known."
-  | Less_general (kind, trace) ->
-      report_unification_error ~loc env trace
+  | Less_general (kind, err) ->
+      report_unification_error ~loc env err
         (fun ppf -> fprintf ppf "This %s has type" kind)
         (fun ppf -> fprintf ppf "which is less general than")
   | Modules_not_allowed ->
@@ -5761,20 +5763,20 @@ let report_error ~loc env = function
   | Illegal_class_expr ->
       Location.errorf ~loc
         "This kind of recursive class expression is not allowed"
-  | Letop_type_clash(name, trace) ->
-      report_unification_error ~loc env trace
+  | Letop_type_clash(name, err) ->
+      report_unification_error ~loc env err
         (function ppf ->
           fprintf ppf "The operator %s has type" name)
         (function ppf ->
           fprintf ppf "but it was expected to have type")
-  | Andop_type_clash(name, trace) ->
-      report_unification_error ~loc env trace
+  | Andop_type_clash(name, err) ->
+      report_unification_error ~loc env err
         (function ppf ->
           fprintf ppf "The operator %s has type" name)
         (function ppf ->
           fprintf ppf "but it was expected to have type")
-  | Bindings_type_clash(trace) ->
-      report_unification_error ~loc env trace
+  | Bindings_type_clash(err) ->
+      report_unification_error ~loc env err
         (function ppf ->
           fprintf ppf "These bindings have type")
         (function ppf ->
diff --git a/typing/typecore.mli b/typing/typecore.mli
index 4994075e778b..00e01f328104 100644
--- a/typing/typecore.mli
+++ b/typing/typecore.mli
@@ -127,15 +127,15 @@ val self_coercion : (Path.t * Location.t list ref) list ref
 
 type error =
   | Constructor_arity_mismatch of Longident.t * int * int
-  | Label_mismatch of Longident.t * Errortrace.unification Errortrace.t
+  | Label_mismatch of Longident.t * Errortrace.unification_error
   | Pattern_type_clash :
-      Errortrace.unification Errortrace.t * _ Typedtree.pattern_desc option
+      Errortrace.unification_error * _ Typedtree.pattern_desc option
       -> error
-  | Or_pattern_type_clash of Ident.t * Errortrace.unification Errortrace.t
+  | Or_pattern_type_clash of Ident.t * Errortrace.unification_error
   | Multiply_bound_variable of string
   | Orpat_vars of Ident.t * Ident.t list
   | Expr_type_clash of
-      Errortrace.unification Errortrace.t * type_forcing_context option
+      Errortrace.unification_error * type_forcing_context option
       * Typedtree.expression_desc option
   | Apply_non_function of type_expr
   | Apply_wrong_label of arg_label * type_expr * bool
@@ -154,17 +154,17 @@ type error =
   | Private_constructor of constructor_description * type_expr
   | Unbound_instance_variable of string * string list
   | Instance_variable_not_mutable of string
-  | Not_subtype of Errortrace.Subtype.t * Errortrace.unification Errortrace.t
+  | Not_subtype of Errortrace.Subtype.t * Errortrace.unification_error
   | Outside_class
   | Value_multiply_overridden of string
   | Coercion_failure of
-      type_expr * type_expr * Errortrace.unification Errortrace.t * bool
+      type_expr * type_expr * Errortrace.unification_error * bool
   | Too_many_arguments of bool * type_expr * type_forcing_context option
   | Abstract_wrong_label of arg_label * type_expr * type_forcing_context option
   | Scoping_let_module of string * type_expr
   | Not_a_variant_type of Longident.t
   | Incoherent_label_order
-  | Less_general of string * Errortrace.unification Errortrace.t
+  | Less_general of string * Errortrace.unification_error
   | Modules_not_allowed
   | Cannot_infer_signature
   | Not_a_packed_module of type_expr
@@ -184,9 +184,9 @@ type error =
   | Illegal_letrec_pat
   | Illegal_letrec_expr
   | Illegal_class_expr
-  | Letop_type_clash of string * Errortrace.unification Errortrace.t
-  | Andop_type_clash of string * Errortrace.unification Errortrace.t
-  | Bindings_type_clash of Errortrace.unification Errortrace.t
+  | Letop_type_clash of string * Errortrace.unification_error
+  | Andop_type_clash of string * Errortrace.unification_error
+  | Bindings_type_clash of Errortrace.unification_error
   | Unbound_existential of Ident.t list * type_expr
   | Missing_type_constraint
 
diff --git a/typing/typedecl.ml b/typing/typedecl.ml
index 22960c69d3e8..24db6b1858f0 100644
--- a/typing/typedecl.ml
+++ b/typing/typedecl.ml
@@ -33,10 +33,10 @@ type error =
   | Duplicate_label of string
   | Recursive_abbrev of string
   | Cycle_in_def of string * type_expr
-  | Definition_mismatch of type_expr * Includecore.type_mismatch option
-  | Constraint_failed of Env.t * Errortrace.unification Errortrace.t
-  | Inconsistent_constraint of Env.t * Errortrace.unification Errortrace.t
-  | Type_clash of Env.t * Errortrace.unification Errortrace.t
+  | Definition_mismatch of type_expr * Env.t * Includecore.type_mismatch option
+  | Constraint_failed of Env.t * Errortrace.unification_error
+  | Inconsistent_constraint of Env.t * Errortrace.unification_error
+  | Type_clash of Env.t * Errortrace.unification_error
   | Non_regular of {
       definition: Path.t;
       used_as: type_expr;
@@ -48,9 +48,9 @@ type error =
   | Unbound_type_var of type_expr * type_declaration
   | Cannot_extend_private_type of Path.t
   | Not_extensible_type of Path.t
-  | Extension_mismatch of Path.t * Includecore.type_mismatch
+  | Extension_mismatch of Path.t * Env.t * Includecore.type_mismatch
   | Rebind_wrong_type of
-      Longident.t * Env.t * Errortrace.unification Errortrace.t
+      Longident.t * Env.t * Errortrace.unification_error
   | Rebind_mismatch of Longident.t * Path.t * Path.t
   | Rebind_private of Longident.t
   | Variance of Typedecl_variance.error
@@ -135,8 +135,8 @@ let update_type temp_env env id loc =
   | Some ty ->
       let params = List.map (fun _ -> Ctype.newvar ()) decl.type_params in
       try Ctype.unify env (Ctype.newconstr path params) ty
-      with Ctype.Unify trace ->
-        raise (Error(loc, Type_clash (env, trace)))
+      with Ctype.Unify err ->
+        raise (Error(loc, Type_clash (env, err)))
 
 let get_unboxed_type_representation env ty =
   match Typedecl_unboxed.get_unboxed_type_representation env ty with
@@ -278,11 +278,13 @@ let make_constructor env type_path type_params sargs sret_type =
       begin match (Ctype.repr ret_type).desc with
         | Tconstr (p', _, _) when Path.same type_path p' -> ()
         | _ ->
-          raise (Error (sret_type.ptyp_loc,
-                        Constraint_failed
-                          (env, [Errortrace.diff
-                                   ret_type
-                                   (Ctype.newconstr type_path type_params)])))
+          raise (Error
+                   (sret_type.ptyp_loc,
+                    Constraint_failed
+                      (env, {trace =
+                               [Errortrace.diff
+                                  ret_type
+                                  (Ctype.newconstr type_path type_params)]})))
       end;
       widen z;
       targs, Some tret_type, args, Some ret_type
@@ -432,8 +434,8 @@ let transl_declaration env sdecl (id, uid) =
       (fun (cty, cty', loc) ->
         let ty = cty.ctyp_type in
         let ty' = cty'.ctyp_type in
-        try Ctype.unify env ty ty' with Ctype.Unify tr ->
-          raise(Error(loc, Inconsistent_constraint (env, tr))))
+        try Ctype.unify env ty ty' with Ctype.Unify err ->
+          raise(Error(loc, Inconsistent_constraint (env, err))))
       cstrs;
     Ctype.end_def ();
   (* Add abstract row *)
@@ -486,8 +488,8 @@ let rec check_constraints_rec env loc visited ty =
       let ty' = Ctype.newconstr path (Ctype.instance_list decl.type_params) in
       begin
         try Ctype.matches env ty ty'
-        with Ctype.Matches_failure (env, trace) ->
-          raise (Error(loc, Constraint_failed (env, trace)))
+        with Ctype.Matches_failure (env, err) ->
+          raise (Error(loc, Constraint_failed (env, err)))
       end;
       List.iter (check_constraints_rec env loc visited) args
   | Tpoly (ty, tl) ->
@@ -585,8 +587,8 @@ let check_coherence env loc dpath decl =
               then Some Includecore.Arity
               else begin
                 match Ctype.equal env false args decl.type_params with
-                | exception Ctype.Equality trace ->
-                    Some (Includecore.Constraint (env, trace))
+                | exception Ctype.Equality err ->
+                    Some (Includecore.Constraint err)
                 | () ->
                     Includecore.type_declarations ~loc ~equality:true env
                       ~mark:true
@@ -598,11 +600,11 @@ let check_coherence env loc dpath decl =
               end
             in
             if err <> None then
-              raise(Error(loc, Definition_mismatch (ty, err)))
+              raise(Error(loc, Definition_mismatch (ty, env, err)))
           with Not_found ->
             raise(Error(loc, Unavailable_type_constructor path))
           end
-      | _ -> raise(Error(loc, Definition_mismatch (ty, None)))
+      | _ -> raise(Error(loc, Definition_mismatch (ty, env, None)))
       end
   | _ -> ()
 
@@ -721,8 +723,8 @@ let check_recursion ~orig_env env loc path decl to_check =
                 Ctype.instance_parameterized_type params0 body0 in
               begin
                 try List.iter2 (Ctype.unify orig_env) params args'
-                with Ctype.Unify trace ->
-                  raise (Error(loc, Constraint_failed (orig_env, trace)));
+                with Ctype.Unify err ->
+                  raise (Error(loc, Constraint_failed (orig_env, err)));
               end;
               check_regular path' args
                 (path' :: prev_exp) ((ty,body) :: prev_expansions)
@@ -990,9 +992,9 @@ let transl_extension_constructor ~scope env type_path type_params
         begin
           try
             Ctype.unify env cstr_res res
-          with Ctype.Unify trace ->
+          with Ctype.Unify err ->
             raise (Error(lid.loc,
-                     Rebind_wrong_type(lid.txt, env, trace)))
+                     Rebind_wrong_type(lid.txt, env, err)))
         end;
         (* Remove "_" names from parameters used in the constructor *)
         if not cdescr.cstr_generalized then begin
@@ -1138,7 +1140,7 @@ let transl_type_extension extend env loc styext =
   in
   begin match err with
   | None -> ()
-  | Some err -> raise (Error(loc, Extension_mismatch (type_path, err)))
+  | Some err -> raise (Error(loc, Extension_mismatch (type_path, env, err)))
   end;
   let ttype_params = make_params env styext.ptyext_params in
   let type_params = List.map (fun (cty, _) -> cty.ctyp_type) ttype_params in
@@ -1454,16 +1456,16 @@ let transl_with_constraint id ?fixed_row_path ~sig_env ~sig_decl ~outer_env
   if arity_ok then
     List.iter2 (fun (cty, _) tparam ->
       try Ctype.unify_var env cty.ctyp_type tparam
-      with Ctype.Unify tr ->
-        raise(Error(cty.ctyp_loc, Inconsistent_constraint (env, tr)))
+      with Ctype.Unify err ->
+        raise(Error(cty.ctyp_loc, Inconsistent_constraint (env, err)))
     ) tparams sig_decl.type_params;
   List.iter (fun (cty, cty', loc) ->
     (* Note: constraints must also be enforced in [sig_env] because
        they may contain parameter variables from [tparams]
        that have now be unified in [sig_env]. *)
     try Ctype.unify env cty.ctyp_type cty'.ctyp_type
-    with Ctype.Unify tr ->
-      raise(Error(loc, Inconsistent_constraint (env, tr)))
+    with Ctype.Unify err ->
+      raise(Error(loc, Inconsistent_constraint (env, err)))
   ) constraints;
   let priv =
     if sdecl.ptype_private = Private then Private else
@@ -1664,19 +1666,20 @@ let report_error ppf = function
   | Cycle_in_def (s, ty) ->
       fprintf ppf "@[<v>The definition of %s contains a cycle:@ %a@]"
         s Printtyp.type_expr ty
-  | Definition_mismatch (ty, None) ->
+  | Definition_mismatch (ty, _env, None) ->
       fprintf ppf "@[<v>@[<hov>%s@ %s@;<1 2>%a@]@]"
         "This variant or record definition" "does not match that of type"
         Printtyp.type_expr ty
-  | Definition_mismatch (ty, Some err) ->
+  | Definition_mismatch (ty, env, Some err) ->
       fprintf ppf "@[<v>@[<hov>%s@ %s@;<1 2>%a@]%a@]"
         "This variant or record definition" "does not match that of type"
         Printtyp.type_expr ty
-        (Includecore.report_type_mismatch "the original" "this" "definition")
+        (Includecore.report_type_mismatch
+           "the original" "this" "definition" env)
         err
-  | Constraint_failed (env, trace) ->
+  | Constraint_failed (env, err) ->
       fprintf ppf "@[<v>Constraints are not satisfied in this type.@ ";
-      Printtyp.report_unification_error ppf env trace
+      Printtyp.report_unification_error ppf env err
         (fun ppf -> fprintf ppf "Type")
         (fun ppf -> fprintf ppf "should be an instance of");
       fprintf ppf "@]"
@@ -1715,14 +1718,14 @@ let report_error ppf = function
             !Oprint.out_type (Printtyp.tree_of_typexp false used_as)
             pp_expansions expansions
       end
-  | Inconsistent_constraint (env, trace) ->
+  | Inconsistent_constraint (env, err) ->
       fprintf ppf "@[<v>The type constraints are not consistent.@ ";
-      Printtyp.report_unification_error ppf env trace
+      Printtyp.report_unification_error ppf env err
         (fun ppf -> fprintf ppf "Type")
         (fun ppf -> fprintf ppf "is not compatible with type");
       fprintf ppf "@]"
-  | Type_clash (env, trace) ->
-      Printtyp.report_unification_error ppf env trace
+  | Type_clash (env, err) ->
+      Printtyp.report_unification_error ppf env err
         (function ppf ->
            fprintf ppf "This type constructor expands to type")
         (function ppf ->
@@ -1768,15 +1771,15 @@ let report_error ppf = function
         "Type definition"
         Printtyp.path path
         "is not extensible"
-  | Extension_mismatch (path, err) ->
+  | Extension_mismatch (path, env, err) ->
       fprintf ppf "@[<v>@[<hov>%s@ %s@;<1 2>%s@]%a@]"
         "This extension" "does not match the definition of type"
         (Path.name path)
         (Includecore.report_type_mismatch
-           "the type" "this extension" "definition")
+           "the type" "this extension" "definition" env)
         err
-  | Rebind_wrong_type (lid, env, trace) ->
-      Printtyp.report_unification_error ppf env trace
+  | Rebind_wrong_type (lid, env, err) ->
+      Printtyp.report_unification_error ppf env err
         (function ppf ->
            fprintf ppf "The constructor %a@ has type"
              Printtyp.longident lid)
@@ -1803,14 +1806,6 @@ let report_error ppf = function
         | false, true  -> inj ^ "contravariant"
         | false, false -> if inj = "" then "unrestricted" else inj
       in
-      let suffix n =
-        let teen = (n mod 100)/10 = 1 in
-        match n mod 10 with
-        | 1 when not teen -> "st"
-        | 2 when not teen -> "nd"
-        | 3 when not teen -> "rd"
-        | _ -> "th"
-      in
       (match n with
        | Variance_not_reflected ->
            fprintf ppf "@[%s@ %s@ It"
@@ -1828,7 +1823,7 @@ let report_error ppf = function
            fprintf ppf "@[%s@ %s@ The %d%s type parameter"
              "In this definition, expected parameter"
              "variances are not satisfied."
-             n (suffix n));
+             n (Misc.ordinal_suffix n));
       (match n with
        | No_variable -> ()
        | _ ->
diff --git a/typing/typedecl.mli b/typing/typedecl.mli
index 2ec3fef33779..901e63fc6b37 100644
--- a/typing/typedecl.mli
+++ b/typing/typedecl.mli
@@ -70,10 +70,10 @@ type error =
   | Duplicate_label of string
   | Recursive_abbrev of string
   | Cycle_in_def of string * type_expr
-  | Definition_mismatch of type_expr * Includecore.type_mismatch option
-  | Constraint_failed of Env.t * Errortrace.unification Errortrace.t
-  | Inconsistent_constraint of Env.t * Errortrace.unification Errortrace.t
-  | Type_clash of Env.t * Errortrace.unification Errortrace.t
+  | Definition_mismatch of type_expr * Env.t * Includecore.type_mismatch option
+  | Constraint_failed of Env.t * Errortrace.unification_error
+  | Inconsistent_constraint of Env.t * Errortrace.unification_error
+  | Type_clash of Env.t * Errortrace.unification_error
   | Non_regular of {
       definition: Path.t;
       used_as: type_expr;
@@ -85,9 +85,9 @@ type error =
   | Unbound_type_var of type_expr * type_declaration
   | Cannot_extend_private_type of Path.t
   | Not_extensible_type of Path.t
-  | Extension_mismatch of Path.t * Includecore.type_mismatch
+  | Extension_mismatch of Path.t * Env.t * Includecore.type_mismatch
   | Rebind_wrong_type of
-      Longident.t * Env.t * Errortrace.unification Errortrace.t
+      Longident.t * Env.t * Errortrace.unification_error
   | Rebind_mismatch of Longident.t * Path.t * Path.t
   | Rebind_private of Longident.t
   | Variance of Typedecl_variance.error
diff --git a/typing/typetexp.ml b/typing/typetexp.ml
index b1a908a41124..7c413294e855 100644
--- a/typing/typetexp.ml
+++ b/typing/typetexp.ml
@@ -33,8 +33,8 @@ type error =
   | Bound_type_variable of string
   | Recursive_type
   | Unbound_row_variable of Longident.t
-  | Type_mismatch of Errortrace.unification Errortrace.t
-  | Alias_type_mismatch of Errortrace.unification Errortrace.t
+  | Type_mismatch of Errortrace.unification_error
+  | Alias_type_mismatch of Errortrace.unification_error
   | Present_has_conjunction of string
   | Present_has_no_type of string
   | Constructor_mismatch of type_expr * type_expr
@@ -234,9 +234,9 @@ and transl_type_aux env policy styp =
       in
       List.iter2
         (fun (sty, cty) ty' ->
-           try unify_param env ty' cty.ctyp_type with Unify trace ->
-             let trace = Errortrace.swap_trace trace in
-             raise (Error(sty.ptyp_loc, env, Type_mismatch trace))
+           try unify_param env ty' cty.ctyp_type with Unify err ->
+             let err = Errortrace.swap_unification_error err in
+             raise (Error(sty.ptyp_loc, env, Type_mismatch err))
         )
         (List.combine stl args) params;
       let constr =
@@ -284,17 +284,13 @@ and transl_type_aux env policy styp =
       let params = instance_list decl.type_params in
       List.iter2
         (fun (sty, cty) ty' ->
-           try unify_var env ty' cty.ctyp_type with Unify trace ->
-             let trace = Errortrace.swap_trace trace in
-             raise (Error(sty.ptyp_loc, env, Type_mismatch trace))
+           try unify_var env ty' cty.ctyp_type with Unify err ->
+             let err = Errortrace.swap_unification_error err in
+             raise (Error(sty.ptyp_loc, env, Type_mismatch err))
         )
         (List.combine stl args) params;
         let ty_args = List.map (fun ctyp -> ctyp.ctyp_type) args in
-      let ty =
-        try Ctype.expand_head env (newconstr path ty_args)
-        with Unify trace ->
-          raise (Error(styp.ptyp_loc, env, Type_mismatch trace))
-      in
+      let ty = Ctype.expand_head env (newconstr path ty_args) in
       let ty = match ty.desc with
         Tvariant row ->
           let row = Btype.row_repr row in
@@ -336,9 +332,9 @@ and transl_type_aux env policy styp =
               instance (fst(TyVarMap.find alias !used_variables))
           in
           let ty = transl_type env policy st in
-          begin try unify_var env t ty.ctyp_type with Unify trace ->
-            let trace = Errortrace.swap_trace trace in
-            raise(Error(styp.ptyp_loc, env, Alias_type_mismatch trace))
+          begin try unify_var env t ty.ctyp_type with Unify err ->
+            let err = Errortrace.swap_unification_error err in
+            raise(Error(styp.ptyp_loc, env, Alias_type_mismatch err))
           end;
           ty
         with Not_found ->
@@ -347,9 +343,9 @@ and transl_type_aux env policy styp =
           used_variables :=
             TyVarMap.add alias (t, styp.ptyp_loc) !used_variables;
           let ty = transl_type env policy st in
-          begin try unify_var env t ty.ctyp_type with Unify trace ->
-            let trace = Errortrace.swap_trace trace in
-            raise(Error(styp.ptyp_loc, env, Alias_type_mismatch trace))
+          begin try unify_var env t ty.ctyp_type with Unify err ->
+             let err = Errortrace.swap_unification_error err in
+            raise(Error(styp.ptyp_loc, env, Alias_type_mismatch err))
           end;
           if !Clflags.principal then begin
             end_def ();
@@ -632,8 +628,8 @@ let globalize_used_variables env fixed =
   fun () ->
     List.iter
       (function (loc, t1, t2) ->
-        try unify env t1 t2 with Unify trace ->
-          raise (Error(loc, env, Type_mismatch trace)))
+        try unify env t1 t2 with Unify err ->
+          raise (Error(loc, env, Type_mismatch err)))
       !r
 
 let transl_simple_type env fixed styp =
diff --git a/typing/typetexp.mli b/typing/typetexp.mli
index 609305ba060b..a5ebc79c8b60 100644
--- a/typing/typetexp.mli
+++ b/typing/typetexp.mli
@@ -50,8 +50,8 @@ type error =
   | Bound_type_variable of string
   | Recursive_type
   | Unbound_row_variable of Longident.t
-  | Type_mismatch of Errortrace.unification Errortrace.t
-  | Alias_type_mismatch of Errortrace.unification Errortrace.t
+  | Type_mismatch of Errortrace.unification_error
+  | Alias_type_mismatch of Errortrace.unification_error
   | Present_has_conjunction of string
   | Present_has_no_type of string
   | Constructor_mismatch of type_expr * type_expr
diff --git a/utils/misc.ml b/utils/misc.ml
index c5bfadfdc08f..942061720d85 100644
--- a/utils/misc.ml
+++ b/utils/misc.ml
@@ -597,6 +597,14 @@ let cut_at s c =
   let pos = String.index s c in
   String.sub s 0 pos, String.sub s (pos+1) (String.length s - pos - 1)
 
+let ordinal_suffix n =
+  let teen = (n mod 100)/10 = 1 in
+  match n mod 10 with
+  | 1 when not teen -> "st"
+  | 2 when not teen -> "nd"
+  | 3 when not teen -> "rd"
+  | _ -> "th"
+
 (* Color handling *)
 module Color = struct
   (* use ANSI color codes, see https://en.wikipedia.org/wiki/ANSI_escape_code *)
diff --git a/utils/misc.mli b/utils/misc.mli
index 741ebf73f112..6aea772091a9 100644
--- a/utils/misc.mli
+++ b/utils/misc.mli
@@ -351,6 +351,12 @@ val cut_at : string -> char -> string * string
    @since 4.01
 *)
 
+val ordinal_suffix : int -> string
+(** [ordinal_suffix n] is the appropriate suffix to append to the numeral [n] as
+    an ordinal number: [1] -> ["st"], [2] -> ["nd"], [3] -> ["rd"],
+    [4] -> ["th"], and so on.  Handles larger numbers (e.g., [42] -> ["nd"]) and
+    the numbers 11--13 (which all get ["th"]) correctly. *)
+
 (* Color handling *)
 module Color : sig
   type color =