Respond to review for the new structured error messages (ocaml#10407)

In addition to the smaller fixes, there were two major changes:

1. `Errortrace` has its type completely refactored, removing `desc`
   and exposing both `'variant trace` and `'variant error`.  The
   former is for traces that are being built up, and contains
   `type_expr`s; the lattern is for complete traces, and contains
   `expanded_type`s (a record containing two `type_expr`s).  This
   dramatically affected a number of call sites, but is much cleaner.

2. We now detect weakly polymorphic types much better during
   printing.  This involved fixing a bug in moregeneral, which was not
   restoring enough information in the error case; it also involved
   exposing the flag that differentiated between printing a type (no
   weakly polymorphic type detection) and a scheme (yes weakly
   polymorphic type detection) in more places, and giving it its own
   custom variant type, `Printtyp.type_or_scheme`.

Among the minor changes, the updates to `Includecore` to more
carefully detect privacy violation errors and differentiate between
the various kinds thereof (recorded in the `privacy_mismatch` type) is
the most visible in the code.

.depend

@@ -679,6 +679,7 @@ typing/includeclass.cmx : \
     typing/includeclass.cmi
 typing/includeclass.cmi : \
     typing/types.cmi \
+    typing/printtyp.cmi \
     parsing/location.cmi \
     typing/env.cmi \
     typing/ctype.cmi

Changes

@@ -299,7 +299,7 @@ Working version
 
 - #10407: Produce more detailed error messages that contain full error
   #traces when module inclusion fails.
-  (Antal Spector-Zabusky, NOT YET REVIEWED)
+  (Antal Spector-Zabusky, review by Florian Angeletti)
 
 ### Internal/compiler-libs changes:
 

testsuite/tests/typing-extensions/open_types.ml

@@ -237,7 +237,7 @@ Error: Signature mismatch:
          type foo = M.foo = private ..
        is not included in
          type foo = ..
-       A private type would be revealed.
+       A private extensible variant would be revealed
 |}]
 
 

testsuite/tests/typing-gadts/ambiguity.ml

@@ -233,8 +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:
+       The type '_weak1 list ref is not compatible with the type T.u list ref
+       Type '_weak1 is not compatible with type T.u = T.t
+       This instance of T.t is ambiguous:
        it would escape the scope of its equation
 |}]
 
@@ -267,7 +268,8 @@ 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:
+       The type '_weak2 list ref is not compatible with the type T.t list ref
+       Type '_weak2 is not compatible with type T.t = T.u
+       This instance of T.u is ambiguous:
        it would escape the scope of its equation
 |}]

testsuite/tests/typing-misc/pr6416.ml

@@ -341,7 +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
+       The type M/1.t = M/2.M.t is not equal to the type M/2.t
        Line 2, characters 14-42:
          Definition of module M/1
        File "_none_", line 1:

testsuite/tests/typing-misc/pr6634.ml

@@ -24,6 +24,7 @@ Error: Signature mismatch:
        is not included in
          type t = [ `T of t/1 ]
        The type [ `T of t/1 ] is not equal to the type [ `T of t/2 ]
+       Type t/1 = [ `T of t/1 ] is not equal to type t/2 = int
        Types for tag `T are incompatible
        Line 4, characters 2-20:
          Definition of type t/1

testsuite/tests/typing-misc/pr7668_bad.ml

@@ -91,7 +91,10 @@ Error: Signature mismatch:
          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 ]
+         ([> `B of [> `BA | `BB of int list ] | `C of unit ] as 'a)
        is not compatible with the type t -> t
+       Type [> `B of [> `BA | `BB of int list ] | `C of unit ] as 'a
+       is not compatible with type
+         t = [ `A of int | `B of [ `BA | `BB of unit list ] | `C of unit ]
        Types for tag `BB are incompatible
 |}]

testsuite/tests/typing-modules-bugs/pr7414_2_bad.compilers.reference

@@ -12,7 +12,7 @@ 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
+     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

testsuite/tests/typing-modules-bugs/pr7414_bad.compilers.reference

@@ -12,7 +12,7 @@ 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
+     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

testsuite/tests/typing-modules/extension_constructors_errors_test.ml

@@ -40,7 +40,7 @@ Error: Signature mismatch:
          type t += private A
        is not included in
          type t += A
-       A private type would be revealed.
+       Private extension constructor(s) would be revealed.
 |}];;
 
 module M2 : sig type t += A end = struct type t += private A | B end;;
@@ -57,5 +57,5 @@ Error: Signature mismatch:
          type t += private A
        is not included in
          type t += A
-       A private type would be revealed.
+       Private extension constructor(s) would be revealed.
 |}];;

testsuite/tests/typing-modules/inclusion_errors.ml

@@ -526,7 +526,7 @@ 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
+     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
 |}];;
@@ -615,6 +615,7 @@ Error: Signature mismatch:
          val f : s -> s
        The type < m : int > -> < m : int > is not compatible with the type
          s -> s
+       Type < m : int > is not compatible with type s = < m : int; .. >
        The second object type has an abstract row, it cannot be closed
 |}];;
 
@@ -660,8 +661,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
+       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;;
@@ -682,7 +683,7 @@ 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 '_weak3 list ref is not compatible with the type t list ref
        The type constructor t would escape its scope
 |}];;
 
@@ -725,8 +726,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:
+       The type '_weak4 list ref is not compatible with the type T.s list ref
+       Type '_weak4 is not compatible with type T.s = T.t
+       This instance of T.t is ambiguous:
        it would escape the scope of its equation
 |}];;
 
@@ -1251,7 +1253,7 @@ Error: Signature mismatch:
          type t = private [ `A | `B ]
        is not included in
          type t = [ `A | `B ]
-       A private type would be revealed.
+       A private type abbreviation would be revealed
 |}];;
 
 module M : sig
@@ -1354,7 +1356,7 @@ Error: Signature mismatch:
 type w = float
 type q = (int * w)
 type u = private (int * q)
-module M : sig (* Confussing error message :( *)
+module M : sig
   type t = private (int * (int * int))
 end = struct
   type t = private u
@@ -1377,7 +1379,8 @@ Error: Signature mismatch:
        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 q = int * w is not equal to type int * int
+       Type w = float is not equal to type int
 |}];;
 
 type s = private int
@@ -1424,7 +1427,7 @@ Error: Signature mismatch:
          type t = private A
        is not included in
          type t = A
-       A private type would be revealed.
+       Private variant constructor(s) would be revealed
 |}];;
 
 module M : sig
@@ -1446,7 +1449,7 @@ Error: Signature mismatch:
          type t = private A | B
        is not included in
          type t = A | B
-       A private type would be revealed.
+       Private variant constructor(s) would be revealed
 |}];;
 
 module M : sig
@@ -1468,7 +1471,7 @@ Error: Signature mismatch:
          type t = private A of { x : int; y : bool; }
        is not included in
          type t = A of { x : int; y : bool; }
-       A private type would be revealed.
+       Private variant constructor(s) would be revealed
 |}];;
 
 module M : sig
@@ -1490,7 +1493,7 @@ Error: Signature mismatch:
          type t = private { x : int; y : bool; }
        is not included in
          type t = { x : int; y : bool; }
-       A private type would be revealed.
+       A private record constructor would be revealed
 |}];;
 
 module M : sig
@@ -1512,7 +1515,7 @@ Error: Signature mismatch:
          type t = private A | B
        is not included in
          type t = A
-       A private type would be revealed.
+       Private variant constructor(s) would be revealed
 |}];;
 
 module M : sig
@@ -1534,9 +1537,11 @@ Error: Signature mismatch:
          type t = private A
        is not included in
          type t = A | B
-       A private type would be revealed.
+       Private variant constructor(s) would be revealed
 |}];;
 
+(* ASZ: Add mismatched records *)
+
 module M : sig
   type t = { x : int }
 end = struct
@@ -1556,7 +1561,7 @@ Error: Signature mismatch:
          type t = private { x : int; y : bool; }
        is not included in
          type t = { x : int; }
-       A private type would be revealed.
+       A private record constructor would be revealed
 |}];;
 
 module M : sig
@@ -1578,7 +1583,7 @@ Error: Signature mismatch:
          type t = private { x : int; }
        is not included in
          type t = { x : int; y : bool; }
-       A private type would be revealed.
+       A private record constructor would be revealed
 |}];;
 
 module M : sig
@@ -1600,7 +1605,7 @@ Error: Signature mismatch:
          type t = private { x : int; y : bool; }
        is not included in
          type t = A | B
-       A private type would be revealed.
+       Their kinds differ.
 |}];;
 
 module M : sig
@@ -1622,7 +1627,7 @@ Error: Signature mismatch:
          type t = private A | B
        is not included in
          type t = { x : int; y : bool; }
-       A private type would be revealed.
+       Their kinds differ.
 |}];;
 
 module M : sig
@@ -1644,7 +1649,7 @@ Error: Signature mismatch:
          type t = private [> `A | `B ]
        is not included in
          type t = [ `A ]
-       A private type would be revealed.
+       A private row type would be revealed
 |}];;
 
 module M : sig
@@ -1666,7 +1671,7 @@ Error: Signature mismatch:
          type t = private [< `A | `B ]
        is not included in
          type t = [ `A ]
-       A private type would be revealed.
+       A private row type would be revealed
 |}];;
 
 module M : sig
@@ -1688,7 +1693,7 @@ Error: Signature mismatch:
          type t = private [< `A | `B > `A ]
        is not included in
          type t = [ `A ]
-       A private type would be revealed.
+       A private row type would be revealed
 |}];;
 
 module M : sig
@@ -1710,5 +1715,5 @@ Error: Signature mismatch:
          type t = private < m : int; .. >
        is not included in
          type t = < m : int >
-       A private type would be revealed.
+       A private row type would be revealed
 |}];;

testsuite/tests/typing-modules/pr7818.ml

@@ -327,5 +327,6 @@ Error: This variant or record definition does not match that of type M.t
          E of (MkT(Desc).t, MkT(Desc).t) eq
        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
+       Type MkT(M.T).t = Set.Make(M.Term0).t is not equal to type
+         MkT(Desc).t = Set.Make(Desc).t
 |}]

testsuite/tests/typing-modules/pr7851.ml

@@ -31,7 +31,7 @@ Error: This variant or record definition does not match that of type M1.t
          E of M1.x
        is not the same as:
          E of M1.y
-       The type M1.x is not equal to the type M1.y
+       The type M1.x = int is not equal to the type M1.y = bool
 |}]
 
 let bool_of_int x =
@@ -84,5 +84,5 @@ Error: This variant or record definition does not match that of type M1.t
        is not the same as:
          E of (M1.x, M1.y) eq
        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
+       Type M1.x = int is not equal to type M1.y = bool
 |}]

testsuite/tests/typing-objects/Tests.ml

@@ -702,7 +702,10 @@ 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
+       The type (#c as 'a) -> 'a is not compatible with the type
+         'a -> (#c as 'b)
+       Type 'a = < m : 'a; .. > is not compatible with type
+         'b = < m : 'b; .. >
        Type 'a is not compatible with type 'b
 |}];;
 

testsuite/tests/typing-polyvariants-bugs/pr7817_bad.ml

@@ -26,9 +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
+       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
+       Type _[< `A of '_weak2 | `B of '_weak3 ] as 'a
        is not compatible with type [< `A of string | `B of int ] as 'b
 |}]

testsuite/tests/typing-private/private.compilers.principal.reference

@@ -92,7 +92,7 @@ Line 3, characters 4-27:
 3 |     type t = M.t = T of int
         ^^^^^^^^^^^^^^^^^^^^^^^
 Error: This variant or record definition does not match that of type M.t
-       A private type would be revealed.
+       Private variant constructor(s) would be revealed
 module M5 : sig type t = M.t = private T of int val mk : int -> t end
 module M6 : sig type t = private T of int val mk : int -> t end
 module M' :

testsuite/tests/typing-private/private.compilers.reference

@@ -92,7 +92,7 @@ Line 3, characters 4-27:
 3 |     type t = M.t = T of int
         ^^^^^^^^^^^^^^^^^^^^^^^
 Error: This variant or record definition does not match that of type M.t
-       A private type would be revealed.
+       Private variant constructor(s) would be revealed
 module M5 : sig type t = M.t = private T of int val mk : int -> t end
 module M6 : sig type t = private T of int val mk : int -> t end
 module M' :