Maintain more structural information in type-checking errors

This commit refactors the types that make up type-checking errors to
maintain more structural information.  Most significantly, we split
out the errors we get from unification, moregen, and type equality in
`Ctype` into three distinct exceptions, and retain the sorts of
information we keep during unification in the other two cases as well
(no more `Unify []`).  We also maintain more information in
`Includecore` about mismatches of primitives, manifests, and private
objects and variants

This commit doesn't make a lot of changes to the user-visible error
messages yet, only what's necessary to support the type changes, but
it enables a forthcoming patch where we use this improvement to
produce more informative error messages.

This commit includes existing work by Mekhrubon Tuarev, who did all
the early development.  I (Antal Spector-Zabusky) came and built the
layer of types on top.

9 files changed, 14 insertions, 41 deletions

diff --git a/testsuite/tests/typing-misc/constraints.ml b/testsuite/tests/typing-misc/constraints.ml
index 3ef0414d11..1faab200e1 100644
--- a/testsuite/tests/typing-misc/constraints.ml
+++ b/testsuite/tests/typing-misc/constraints.ml
@@ -213,7 +213,7 @@ Line 1, characters 0-59:
 1 | type 'a t = <a : 'a; b : 'b> constraint <a : 'a; ..> = 'b t;;
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: A type variable is unbound in this type declaration.
-In method b: 'b the variable 'b is unbound
+       In method b: 'b the variable 'b is unbound
 |}]
 
 module rec M : sig type 'a t = 'b constraint 'a = 'b t end = M;;
@@ -267,7 +267,7 @@ Line 3, characters 13-23:
 3 |   constraint 'a = float
                  ^^^^^^^^^^
 Error: The type constraints are not consistent.
-Type int is not compatible with type float
+       Type int is not compatible with type float
 |}]
 
 type ('a,'b) t = T
@@ -279,8 +279,8 @@ Line 4, characters 13-20:
 4 |   constraint 'a = 'b
                  ^^^^^^^
 Error: The type constraints are not consistent.
-Type int -> float is not compatible with type bool -> char
-Type int is not compatible with type bool
+       Type int -> float is not compatible with type bool -> char
+       Type int is not compatible with type bool
 |}]
 
 class type ['a, 'b] a = object
@@ -293,6 +293,6 @@ Line 4, characters 2-31:
 4 |   constraint 'b = float * float
       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: The class constraints are not consistent.
-Type int * int is not compatible with type float * float
-Type int is not compatible with type float
+       Type int * int is not compatible with type float * float
+       Type int is not compatible with type float
 |}]
diff --git a/testsuite/tests/typing-misc/pr6416.ml b/testsuite/tests/typing-misc/pr6416.ml
index af9cf7157b..943c0d6bd7 100644
--- a/testsuite/tests/typing-misc/pr6416.ml
+++ b/testsuite/tests/typing-misc/pr6416.ml
@@ -308,8 +308,7 @@ Error: Signature mismatch:
          class type c = object method m : t/2 end
        does not match
          class type c = object method m : t/1 end
-       The method m has type t/2 but is expected to have type t/1
-       Type t/2 is not compatible with type t/1 = K.t
+       The method m has type t/2 but is expected to have type t/1 = K.t
        Line 12, characters 4-10:
          Definition of type t/1
        Line 9, characters 2-8:
diff --git a/testsuite/tests/typing-misc/pr7937.ml b/testsuite/tests/typing-misc/pr7937.ml
index 3c1063a201..1b6a6e9e0b 100644
--- a/testsuite/tests/typing-misc/pr7937.ml
+++ b/testsuite/tests/typing-misc/pr7937.ml
@@ -12,7 +12,6 @@ Line 3, characters 35-39:
                                        ^^^^
 Error: This expression has type bool but an expression was expected of type
          ([< `X of int & 'a ] as 'a) r
-       Types for tag `X are incompatible
 |}, Principal{|
 type 'a r = 'a constraint 'a = [< `X of int & 'a ]
 Line 3, characters 35-39:
@@ -20,7 +19,6 @@ Line 3, characters 35-39:
                                        ^^^^
 Error: This expression has type bool but an expression was expected of type
          ([< `X of 'b & 'a & 'c ] as 'a) r
-       Types for tag `X are incompatible
 |}]
 
 let g: 'a. 'a r -> 'a r = fun x -> { contents = 0 };;
@@ -30,7 +28,6 @@ Line 1, characters 35-51:
                                        ^^^^^^^^^^^^^^^^
 Error: This expression has type int ref
        but an expression was expected of type ([< `X of int & 'a ] as 'a) r
-       Types for tag `X are incompatible
 |}, Principal{|
 Line 1, characters 35-51:
 1 | let g: 'a. 'a r -> 'a r = fun x -> { contents = 0 };;
@@ -38,7 +35,6 @@ Line 1, characters 35-51:
 Error: This expression has type int ref
        but an expression was expected of type
          ([< `X of 'b & 'a & 'c ] as 'a) r
-       Types for tag `X are incompatible
 |}]
 
 let h: 'a. 'a r -> _ = function true | false -> ();;
diff --git a/testsuite/tests/typing-misc/unbound_type_variables.ml b/testsuite/tests/typing-misc/unbound_type_variables.ml
index ec7184a0d1..c00d036079 100644
--- a/testsuite/tests/typing-misc/unbound_type_variables.ml
+++ b/testsuite/tests/typing-misc/unbound_type_variables.ml
@@ -37,7 +37,7 @@ Line 1, characters 0-25:
 1 | type polyvariant = [> `C]
     ^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: A type variable is unbound in this type declaration.
-In type [> `C ] as 'a the variable 'a is unbound
+       In type [> `C ] as 'a the variable 'a is unbound
 |}]
 
 type 'a only_one = 'a * 'b
diff --git a/testsuite/tests/typing-objects-bugs/pr3968_bad.compilers.reference b/testsuite/tests/typing-objects-bugs/pr3968_bad.compilers.reference
index a5685448b5..9bf6524d6b 100644
--- a/testsuite/tests/typing-objects-bugs/pr3968_bad.compilers.reference
+++ b/testsuite/tests/typing-objects-bugs/pr3968_bad.compilers.reference
@@ -47,3 +47,4 @@ Error: The class type
        Type exp = < eval : (string, exp) Hashtbl.t -> expr >
        is not compatible with type
          expr = [ `Abs of string * expr | `App of expr * expr ] 
+       Types for tag `App are incompatible
diff --git a/testsuite/tests/typing-objects-bugs/pr4018_bad.compilers.reference b/testsuite/tests/typing-objects-bugs/pr4018_bad.compilers.reference
index 68b176658e..ad3ea965b4 100644
--- a/testsuite/tests/typing-objects-bugs/pr4018_bad.compilers.reference
+++ b/testsuite/tests/typing-objects-bugs/pr4018_bad.compilers.reference
@@ -16,25 +16,5 @@ Error: This type entity = < destroy_subject : id subject; entity_id : id >
        Type (id subject, id) observer = < notify : id subject -> id -> unit >
        is not compatible with type
          'a entity_container =
-           < add_entity : (< destroy_subject : < add_observer : 'a
-                                                                entity_container ->
-                                                                'f;
-                                                 .. >
-                                               as 'e;
-                             .. >
-                           as 'd) ->
-                          'f;
-             notify : 'd -> id -> unit > 
-       Type entity = < destroy_subject : id subject; entity_id : id >
-       is not compatible with type < destroy_subject : 'e; .. > as 'd 
-       Type
-         id subject =
-           < add_observer : (id subject, id) observer -> unit;
-             notify_observers : id -> unit >
-       is not compatible with type
-         < add_observer : 'a entity_container -> 'f; .. > as 'e 
-       Type (id subject, id) observer = < notify : id subject -> id -> unit >
-       is not compatible with type
-         'a entity_container =
-           < add_entity : 'd -> 'f; notify : 'd -> id -> unit > 
-       The first object type has no method add_entity
+           < add_entity : 'a -> 'c; notify : 'a -> id -> unit > 
+       Types for method add_observer are incompatible
diff --git a/testsuite/tests/typing-poly/poly.ml b/testsuite/tests/typing-poly/poly.ml
index ec013528e1..92fb99d33d 100644
--- a/testsuite/tests/typing-poly/poly.ml
+++ b/testsuite/tests/typing-poly/poly.ml
@@ -976,6 +976,7 @@ Line 3, characters 13-29:
                  ^^^^^^^^^^^^^^^^
 Error: Constraints are not satisfied in this type.
        Type (float, string) t should be an instance of (int, int) t
+       Type float is not compatible with type int
 |}]
 
 (* Example of wrong expansion *)
diff --git a/testsuite/tests/typing-poly/pr9603.ml b/testsuite/tests/typing-poly/pr9603.ml
index 9052a1a43f..02f1e921b9 100644
--- a/testsuite/tests/typing-poly/pr9603.ml
+++ b/testsuite/tests/typing-poly/pr9603.ml
@@ -29,8 +29,5 @@ Error: This expression has type
          < m : 'left 'right. < left : 'left; right : 'right > pair >
        but an expression was expected of type
          < m : 'left 'right. < left : 'left; right : 'right > pair >
-       Type < left : 'left; right : 'right > pair = 'a * 'b
-       is not compatible with type < left : 'left0; right : 'right0 > pair
-       The method left has type 'a, but the expected method type was 'left
-       The universal variable 'left would escape its scope
+       Types for method m are incompatible
 |}]
diff --git a/testsuite/tests/typing-polyvariants-bugs-2/pr3918c.compilers.reference b/testsuite/tests/typing-polyvariants-bugs-2/pr3918c.compilers.reference
index 411578cf64..82ba615155 100644
--- a/testsuite/tests/typing-polyvariants-bugs-2/pr3918c.compilers.reference
+++ b/testsuite/tests/typing-polyvariants-bugs-2/pr3918c.compilers.reference
@@ -1,6 +1,5 @@
 File "pr3918c.ml", line 24, characters 11-12:
 24 | let f x = (x : 'a vlist :> 'b vlist)
                 ^
-Error: This expression has type 'b Pr3918b.vlist = 'a
+Error: This expression has type 'b Pr3918b.vlist
        but an expression was expected of type 'b Pr3918b.vlist
-       The type variable 'a occurs inside ('d * 'c) Pr3918a.voption as 'c