Maintain more structural information in type-checking errors

.depend

@@ -506,6 +506,7 @@ typing/ctype.cmo : \
     parsing/location.cmi \
     utils/local_store.cmi \
     typing/ident.cmi \
+    typing/errortrace.cmi \
     typing/env.cmi \
     utils/clflags.cmi \
     typing/btype.cmi \
@@ -522,6 +523,7 @@ typing/ctype.cmx : \
     parsing/location.cmx \
     utils/local_store.cmx \
     typing/ident.cmx \
+    typing/errortrace.cmx \
     typing/env.cmx \
     utils/clflags.cmx \
     typing/btype.cmx \
@@ -534,6 +536,7 @@ typing/ctype.cmi : \
     parsing/longident.cmi \
     parsing/location.cmi \
     typing/ident.cmi \
+    typing/errortrace.cmi \
     typing/env.cmi \
     parsing/asttypes.cmi
 typing/datarepr.cmo : \
@@ -632,6 +635,20 @@ typing/envaux.cmi : \
     typing/subst.cmi \
     typing/path.cmi \
     typing/env.cmi
+typing/errortrace.cmo : \
+    typing/types.cmi \
+    typing/path.cmi \
+    parsing/asttypes.cmi \
+    typing/errortrace.cmi
+typing/errortrace.cmx : \
+    typing/types.cmx \
+    typing/path.cmx \
+    parsing/asttypes.cmi \
+    typing/errortrace.cmi
+typing/errortrace.cmi : \
+    typing/types.cmi \
+    typing/path.cmi \
+    parsing/asttypes.cmi
 typing/ident.cmo : \
     utils/misc.cmi \
     utils/local_store.cmi \
@@ -670,8 +687,10 @@ typing/includecore.cmo : \
     typing/typedtree.cmi \
     typing/type_immediacy.cmi \
     typing/printtyp.cmi \
+    typing/primitive.cmi \
     typing/path.cmi \
     typing/ident.cmi \
+    typing/errortrace.cmi \
     typing/env.cmi \
     typing/ctype.cmi \
     parsing/builtin_attributes.cmi \
@@ -683,8 +702,10 @@ typing/includecore.cmx : \
     typing/typedtree.cmx \
     typing/type_immediacy.cmx \
     typing/printtyp.cmx \
+    typing/primitive.cmx \
     typing/path.cmx \
     typing/ident.cmx \
+    typing/errortrace.cmx \
     typing/env.cmx \
     typing/ctype.cmx \
     parsing/builtin_attributes.cmx \
@@ -698,8 +719,8 @@ typing/includecore.cmi : \
     typing/path.cmi \
     parsing/location.cmi \
     typing/ident.cmi \
-    typing/env.cmi \
-    typing/ctype.cmi
+    typing/errortrace.cmi \
+    typing/env.cmi
 typing/includemod.cmo : \
     typing/types.cmi \
     typing/typedtree.cmi \
@@ -1024,6 +1045,7 @@ typing/printtyp.cmo : \
     parsing/longident.cmi \
     parsing/location.cmi \
     typing/ident.cmi \
+    typing/errortrace.cmi \
     typing/env.cmi \
     typing/ctype.cmi \
     utils/clflags.cmi \
@@ -1044,6 +1066,7 @@ typing/printtyp.cmx : \
     parsing/longident.cmx \
     parsing/location.cmx \
     typing/ident.cmx \
+    typing/errortrace.cmx \
     typing/env.cmx \
     typing/ctype.cmx \
     utils/clflags.cmx \
@@ -1057,8 +1080,8 @@ typing/printtyp.cmi : \
     parsing/longident.cmi \
     parsing/location.cmi \
     typing/ident.cmi \
+    typing/errortrace.cmi \
     typing/env.cmi \
-    typing/ctype.cmi \
     parsing/asttypes.cmi
 typing/printtyped.cmo : \
     typing/types.cmi \
@@ -1211,6 +1234,7 @@ typing/typeclass.cmo : \
     parsing/location.cmi \
     typing/includeclass.cmi \
     typing/ident.cmi \
+    typing/errortrace.cmi \
     typing/env.cmi \
     typing/ctype.cmi \
     file_formats/cmt_format.cmi \
@@ -1238,6 +1262,7 @@ typing/typeclass.cmx : \
     parsing/location.cmx \
     typing/includeclass.cmx \
     typing/ident.cmx \
+    typing/errortrace.cmx \
     typing/env.cmx \
     typing/ctype.cmx \
     file_formats/cmt_format.cmx \
@@ -1254,6 +1279,7 @@ typing/typeclass.cmi : \
     parsing/longident.cmi \
     parsing/location.cmi \
     typing/ident.cmi \
+    typing/errortrace.cmi \
     typing/env.cmi \
     typing/ctype.cmi \
     parsing/asttypes.cmi
@@ -1278,6 +1304,7 @@ typing/typecore.cmo : \
     parsing/longident.cmi \
     parsing/location.cmi \
     typing/ident.cmi \
+    typing/errortrace.cmi \
     typing/env.cmi \
     typing/ctype.cmi \
     file_formats/cmt_format.cmi \
@@ -1308,6 +1335,7 @@ typing/typecore.cmx : \
     parsing/longident.cmx \
     parsing/location.cmx \
     typing/ident.cmx \
+    typing/errortrace.cmx \
     typing/env.cmx \
     typing/ctype.cmx \
     file_formats/cmt_format.cmx \
@@ -1325,8 +1353,8 @@ typing/typecore.cmi : \
     parsing/longident.cmi \
     parsing/location.cmi \
     typing/ident.cmi \
+    typing/errortrace.cmi \
     typing/env.cmi \
-    typing/ctype.cmi \
     parsing/asttypes.cmi
 typing/typedecl.cmo : \
     utils/warnings.cmi \
@@ -1351,6 +1379,7 @@ typing/typedecl.cmo : \
     parsing/location.cmi \
     typing/includecore.cmi \
     typing/ident.cmi \
+    typing/errortrace.cmi \
     typing/env.cmi \
     typing/ctype.cmi \
     utils/config.cmi \
@@ -1385,6 +1414,7 @@ typing/typedecl.cmx : \
     parsing/location.cmx \
     typing/includecore.cmx \
     typing/ident.cmx \
+    typing/errortrace.cmx \
     typing/env.cmx \
     typing/ctype.cmx \
     utils/config.cmx \
@@ -1408,8 +1438,8 @@ typing/typedecl.cmi : \
     parsing/location.cmi \
     typing/includecore.cmi \
     typing/ident.cmi \
+    typing/errortrace.cmi \
     typing/env.cmi \
-    typing/ctype.cmi \
     parsing/asttypes.cmi
 typing/typedecl_immediacy.cmo : \
     typing/types.cmi \
@@ -1712,6 +1742,7 @@ typing/typetexp.cmo : \
     utils/misc.cmi \
     parsing/longident.cmi \
     parsing/location.cmi \
+    typing/errortrace.cmi \
     typing/env.cmi \
     typing/ctype.cmi \
     utils/clflags.cmi \
@@ -1732,6 +1763,7 @@ typing/typetexp.cmx : \
     utils/misc.cmx \
     parsing/longident.cmx \
     parsing/location.cmx \
+    typing/errortrace.cmx \
     typing/env.cmx \
     typing/ctype.cmx \
     utils/clflags.cmx \
@@ -1747,8 +1779,8 @@ typing/typetexp.cmi : \
     parsing/parsetree.cmi \
     parsing/longident.cmi \
     parsing/location.cmi \
+    typing/errortrace.cmi \
     typing/env.cmi \
-    typing/ctype.cmi \
     parsing/asttypes.cmi
 typing/untypeast.cmo : \
     typing/typedtree.cmi \

Changes

@@ -337,6 +337,13 @@ Working version
 - #8936: Per-function environment for Emit
   (Greta Yorsh, review by Vincent Laviron and Florian Angeletti)
 
+- #10170: Maintain more structural information in type-checking errors
+  A mostly-internal change that preserves more information in errors
+  during type checking; most significantly, it split the errors from
+  unification, moregen, and type equality into three different types.
+  (Antal Spector-Zabusky and Mekhrubon Tuarev, review by Leo White,
+  Florian Angeletti, and Jacques Garrigue)
+
 ### Build system:
 
 - #9191, #10091, #10182: take the LDFLAGS variable into account, except on

compilerlibs/Makefile.compilerlibs

@@ -84,6 +84,7 @@ TYPING = \
   file_formats/cmi_format.cmo \
   typing/persistent_env.cmo \
   typing/env.cmo \
+  typing/errortrace.cmo \
   typing/typedtree.cmo \
   typing/printtyped.cmo \
   typing/ctype.cmo \

lambda/lambda.ml

@@ -181,14 +181,7 @@ and raise_kind =
   | Raise_reraise
   | Raise_notrace
 
-let equal_boxed_integer x y =
-  match x, y with
-  | Pnativeint, Pnativeint
-  | Pint32, Pint32
-  | Pint64, Pint64 ->
-    true
-  | (Pnativeint | Pint32 | Pint64), _ ->
-    false
+let equal_boxed_integer = Primitive.equal_boxed_integer
 
 let equal_primitive =
   (* Should be implemented like [equal_value_kind] of [equal_boxed_integer],

testsuite/tests/typing-misc/constraints.ml

@@ -156,7 +156,6 @@ Here is an example of a case that is not matched:
 Exception: Match_failure ("", 6, 23).
 |}]
 
-
 (* #9866, #9873 *)
 
 type 'a t = 'b  constraint 'a = 'b t;;
@@ -214,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;;
@@ -259,3 +258,41 @@ struct
   type !'a t = 'b constraint 'a = 'b s
 end
 *)
+
+type 'a t = T
+  constraint 'a = int
+  constraint 'a = float
+[%%expect{|
+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 ('a,'b) t = T
+  constraint 'a = int -> float
+  constraint 'b = bool -> char
+  constraint 'a = 'b
+[%%expect{|
+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
+|}]
+
+class type ['a, 'b] a = object
+  constraint 'a = 'b
+  constraint 'a = int * int
+  constraint 'b = float * float
+end;;
+[%%expect{|
+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
+|}]

testsuite/tests/typing-misc/pr6416.ml

@@ -309,7 +309,7 @@ Error: Signature mismatch:
        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
+       Type t/2 is not equal to type t/1 = K.t
        Line 12, characters 4-10:
          Definition of type t/1
        Line 9, characters 2-8:

testsuite/tests/typing-misc/pr7937.ml

@@ -12,15 +12,13 @@ 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:
 3 | let f: 'a. 'a r -> 'a r = fun x -> true;;
                                        ^^^^
 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,15 +28,13 @@ 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 };;
                                        ^^^^^^^^^^^^^^^^
 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 -> ();;