From 64a4d834fdb0d16c0153633cd5accfe5f1d17caf Mon Sep 17 00:00:00 2001 From: Antal Spector-Zabusky Date: Fri, 30 Apr 2021 21:44:13 -0400 Subject: [PATCH] Start using the structured errors (#10170) for better error messages --- .depend | 5 ++ .../tests/typing-extensions/extensions.ml | 16 ++-- testsuite/tests/typing-gadts/pr7160.ml | 4 +- testsuite/tests/typing-gadts/pr7378.ml | 4 +- .../tests/typing-misc/enrich_typedecl.ml | 4 +- .../tests/typing-misc/includeclass_errors.ml | 2 +- testsuite/tests/typing-misc/pr6416.ml | 11 ++- testsuite/tests/typing-misc/records.ml | 6 +- testsuite/tests/typing-misc/variant.ml | 6 +- testsuite/tests/typing-modules/Test.ml | 12 +-- .../extension_constructors_errors_test.ml | 2 +- testsuite/tests/typing-modules/functors.ml | 10 +-- .../tests/typing-modules/inclusion_errors.ml | 10 ++- .../module_type_substitution.ml | 4 +- testsuite/tests/typing-modules/pr7818.ml | 4 +- testsuite/tests/typing-modules/pr7851.ml | 8 +- .../typing-modules/records_errors_test.ml | 6 +- .../typing-modules/variants_errors_test.ml | 24 +++--- typing/ctype.ml | 74 +++++++++---------- typing/ctype.mli | 19 ++--- typing/errortrace.ml | 10 +++ typing/errortrace.mli | 10 +++ typing/includeclass.ml | 20 ++--- typing/includecore.ml | 63 ++++++++-------- typing/includecore.mli | 14 ++-- typing/printtyp.ml | 28 ++++--- typing/printtyp.mli | 2 +- typing/typedecl.ml | 4 +- 28 files changed, 204 insertions(+), 178 deletions(-) diff --git a/.depend b/.depend index 2e3c320932e..3e5403a93f2 100644 --- a/.depend +++ b/.depend @@ -638,16 +638,19 @@ typing/envaux.cmi : \ typing/errortrace.cmo : \ typing/types.cmi \ typing/path.cmi \ + typing/env.cmi \ parsing/asttypes.cmi \ typing/errortrace.cmi typing/errortrace.cmx : \ typing/types.cmx \ typing/path.cmx \ + typing/env.cmx \ parsing/asttypes.cmi \ typing/errortrace.cmi typing/errortrace.cmi : \ typing/types.cmi \ typing/path.cmi \ + typing/env.cmi \ parsing/asttypes.cmi typing/ident.cmo : \ utils/misc.cmi \ @@ -667,6 +670,7 @@ typing/includeclass.cmo : \ typing/types.cmi \ typing/printtyp.cmi \ typing/path.cmi \ + typing/errortrace.cmi \ typing/ctype.cmi \ parsing/builtin_attributes.cmi \ typing/includeclass.cmi @@ -674,6 +678,7 @@ typing/includeclass.cmx : \ typing/types.cmx \ typing/printtyp.cmx \ typing/path.cmx \ + typing/errortrace.cmx \ typing/ctype.cmx \ parsing/builtin_attributes.cmx \ typing/includeclass.cmi diff --git a/testsuite/tests/typing-extensions/extensions.ml b/testsuite/tests/typing-extensions/extensions.ml index 259712b21b5..beea8d031c5 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-gadts/pr7160.ml b/testsuite/tests/typing-gadts/pr7160.ml index a615a462821..15b27c54f5c 100644 --- a/testsuite/tests/typing-gadts/pr7160.ml +++ b/testsuite/tests/typing-gadts/pr7160.ml @@ -20,7 +20,7 @@ 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 is not equal to the type 'l1 |}];; diff --git a/testsuite/tests/typing-gadts/pr7378.ml b/testsuite/tests/typing-gadts/pr7378.ml index 9252b43ddbc..be82796f87e 100644 --- a/testsuite/tests/typing-gadts/pr7378.ml +++ b/testsuite/tests/typing-gadts/pr7378.ml @@ -21,9 +21,9 @@ 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 is not equal to the type 'b |}] (* would segfault diff --git a/testsuite/tests/typing-misc/enrich_typedecl.ml b/testsuite/tests/typing-misc/enrich_typedecl.ml index 295cab1ef28..3fae8159062 100644 --- a/testsuite/tests/typing-misc/enrich_typedecl.ml +++ b/testsuite/tests/typing-misc/enrich_typedecl.ml @@ -254,7 +254,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/includeclass_errors.ml b/testsuite/tests/typing-misc/includeclass_errors.ml index 9d1b8be4e5e..f7cec952364 100644 --- a/testsuite/tests/typing-misc/includeclass_errors.ml +++ b/testsuite/tests/typing-misc/includeclass_errors.ml @@ -107,7 +107,7 @@ Error: Signature mismatch: class ['a] c : object end does not match class ['a] c : object constraint 'a = int end - A type parameter has type 'a but is expected to have type int + A type parameter has type 'a0 but is expected to have type int |}] module M: sig diff --git a/testsuite/tests/typing-misc/pr6416.ml b/testsuite/tests/typing-misc/pr6416.ml index 7464356b6db..cbb245b1457 100644 --- a/testsuite/tests/typing-misc/pr6416.ml +++ b/testsuite/tests/typing-misc/pr6416.ml @@ -52,9 +52,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 +121,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: @@ -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 equal to 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/records.ml b/testsuite/tests/typing-misc/records.ml index 51623ef2cf5..132bcd2b3b3 100644 --- a/testsuite/tests/typing-misc/records.ml +++ b/testsuite/tests/typing-misc/records.ml @@ -221,7 +221,7 @@ Line 2, characters 0-37: Error: This variant or record definition does not match that of type d Fields do not match: y : int; - is not compatible with: + is not the same as: mutable y : int; This is mutable and the original is not. |}] @@ -243,9 +243,9 @@ Line 1, characters 0-31: Error: This variant or record definition does not match that of type d Fields do not match: x : int; - is not compatible with: + is not the same as: x : float; - The types are not equal. + The type int is not equal to the type float |}] type unboxed = d = {x:float} [@@unboxed] diff --git a/testsuite/tests/typing-misc/variant.ml b/testsuite/tests/typing-misc/variant.ml index d8356cd819e..32d284c8f16 100644 --- a/testsuite/tests/typing-misc/variant.ml +++ b/testsuite/tests/typing-misc/variant.ml @@ -98,9 +98,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 +143,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/Test.ml b/testsuite/tests/typing-modules/Test.ml index 6287a6e6f60..f87fa521d15 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/extension_constructors_errors_test.ml b/testsuite/tests/typing-modules/extension_constructors_errors_test.ml index fb4b914f1d9..63b59f33dbe 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 9319829018a..1459c66a08b 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 a20566f5591..fb3a4971ec1 100644 --- a/testsuite/tests/typing-modules/inclusion_errors.ml +++ b/testsuite/tests/typing-modules/inclusion_errors.ml @@ -138,9 +138,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 @@ -251,9 +251,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 diff --git a/testsuite/tests/typing-modules/module_type_substitution.ml b/testsuite/tests/typing-modules/module_type_substitution.ml index d4a68a3267e..2bcd706d222 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/pr7818.ml b/testsuite/tests/typing-modules/pr7818.ml index 84f7d8f702f..a151702857d 100644 --- a/testsuite/tests/typing-modules/pr7818.ml +++ b/testsuite/tests/typing-modules/pr7818.ml @@ -323,7 +323,7 @@ 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 is not equal to the type MkT(Desc).t |}] diff --git a/testsuite/tests/typing-modules/pr7851.ml b/testsuite/tests/typing-modules/pr7851.ml index bcd3281bedc..6318266cc78 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,7 @@ 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 is not equal to the type M1.y |}] diff --git a/testsuite/tests/typing-modules/records_errors_test.ml b/testsuite/tests/typing-modules/records_errors_test.ml index f85c1e7db9b..16ead91ca07 100644 --- a/testsuite/tests/typing-modules/records_errors_test.ml +++ b/testsuite/tests/typing-modules/records_errors_test.ml @@ -42,9 +42,9 @@ 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 float is not equal to the type int |}];; @@ -88,7 +88,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 a923ebcfa77..d531d36b0ae 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/typing/ctype.ml b/typing/ctype.ml index 827b433b7f8..a4474b2f98a 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -58,7 +58,8 @@ open Local_store (**** Errors ****) exception Unify of unification Errortrace.t -exception Equality of comparison Errortrace.t +exception Equality_core of comparison Errortrace.t +exception Equality of equality_subst * comparison Errortrace.t exception Moregen of comparison Errortrace.t exception Subtype of Errortrace.Subtype.t * unification Errortrace.t @@ -76,9 +77,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 tr) + | Equality -> raise (Equality_core tr) + | Moregen -> raise (Moregen 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 @@ -3699,7 +3700,7 @@ 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_core trace -> raise ( Equality(!subst, 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 +3731,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_core trace -> + raise (Equality(!subst, + Errortrace.incompatible_fields n t1 t2 :: trace))) pairs and eqtype_kind k1 k2 = @@ -3740,7 +3742,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 *) @@ -3797,8 +3799,8 @@ and eqtype_row rename type_pairs subst env row1 row2 = | 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_core err -> + raise (Equality(!subst, Variant (Incompatible_types_for l):: err))) pairs (* Must empty univar_pairs first *) @@ -3819,12 +3821,12 @@ let equal env rename tyl1 tyl2 = let is_equal env rename tyl1 tyl2 = match equal env rename tyl1 tyl2 with | () -> true - | exception Equality _ -> false + | exception Equality(_,_) -> false let rec equal_private env params1 ty1 params2 ty2 = match equal env true (params1 @ [ty1]) (params2 @ [ty2]) with | () -> () - | exception (Equality _ as err) -> + | exception (Equality(_,_) as err) -> match try_expand_safe_opt env (expand_head env ty1) with | ty1' -> equal_private env params1 ty1' params2 ty2 | exception Cannot_expand -> raise err @@ -3833,20 +3835,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 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 moregen_error + | CM_Val_type_mismatch of string * comparison_error + | CM_Meth_type_mismatch of string * comparison_error | CM_Non_mutable_value of string | CM_Non_concrete_value of string | CM_Missing_value of string @@ -3868,7 +3864,8 @@ let rec moregen_clty trace type_pairs env cty1 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)]) + 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 -> @@ -3882,7 +3879,7 @@ let rec moregen_clty trace type_pairs env cty1 cty2 = try moregen true type_pairs env t1 t2 with Moregen trace -> raise (Failure [ CM_Meth_type_mismatch - (CM_Moregen, lab, env, expand_trace env trace)])) + (lab, Moregen_error {env; trace = expand_trace env trace})])) pairs; Vars.iter (fun lab (_mut, _v, ty) -> @@ -3890,7 +3887,7 @@ let rec moregen_clty trace type_pairs env cty1 cty2 = try moregen true type_pairs env ty' ty with Moregen trace -> raise (Failure [ CM_Val_type_mismatch - (CM_Moregen, lab, env, expand_trace env trace)])) + (lab, Moregen_error {env; trace = expand_trace env trace})])) sign2.csig_vars | _ -> raise (Failure []) @@ -4005,17 +4002,19 @@ 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(subst, trace) -> + raise (Failure + [CM_Meth_type_mismatch + (lab, Equality_error {subst; env; 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(subst, trace) -> + raise (Failure + [CM_Val_type_mismatch + (lab, Equality_error {subst; env; trace = expand_trace env trace})])) sign2.csig_vars with Failure error when trace -> @@ -4104,9 +4103,9 @@ 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 -> + try eqtype true type_pairs subst env p s with Equality(subst, trace) -> raise (Failure [CM_Type_parameter_mismatch - (env, expand_trace env trace)])) + {subst; env; 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; @@ -4654,13 +4653,8 @@ 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) - tyl - then tyl else ty::tyl) + if List.exists (fun ty' -> is_equal Env.empty false [ty] [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 7185cdb7e01..05686061eda 100644 --- a/typing/ctype.mli +++ b/typing/ctype.mli @@ -21,7 +21,7 @@ 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 Equality of Errortrace.equality_subst * Errortrace.comparison Errortrace.t exception Moregen of Errortrace.comparison Errortrace.t exception Subtype of Errortrace.Subtype.t * Errortrace.unification Errortrace.t exception Escape of Errortrace.desc Errortrace.escape @@ -234,22 +234,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 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 Errortrace.moregen_error + | CM_Val_type_mismatch of string * Errortrace.comparison_error + | CM_Meth_type_mismatch of string * Errortrace.comparison_error | CM_Non_mutable_value of string | CM_Non_concrete_value of string | CM_Missing_value of string @@ -259,6 +251,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 6a2543a321b..37c12c9fc90 100644 --- a/typing/errortrace.ml +++ b/typing/errortrace.ml @@ -106,6 +106,16 @@ type ('a, 'variety) elt = type 'variety t = (desc, 'variety) elt list +type equality_subst = (type_expr * type_expr) list + +type unification_error = { trace : unification t } +type equality_error = { trace : comparison t; env : Env.t; subst : equality_subst; } +type moregen_error = { trace : comparison t; env : Env.t } + +type comparison_error = + | Equality_error of equality_error + | Moregen_error of moregen_error + let diff got expected = Diff (map_diff short { got; expected }) let map_elt (type variety) f : ('a, variety) elt -> ('b, variety) elt = function diff --git a/typing/errortrace.mli b/typing/errortrace.mli index 9eea3dc2fc4..fb7150a2d88 100644 --- a/typing/errortrace.mli +++ b/typing/errortrace.mli @@ -86,6 +86,16 @@ type ('a, 'variety) elt = type 'variety t = (desc, 'variety) elt list +type equality_subst = (type_expr * type_expr) list + +type unification_error = { trace : unification t } +type equality_error = { trace : comparison t; env : Env.t; subst : equality_subst; } +type moregen_error = { trace : comparison t; env : Env.t } + +type comparison_error = + | Equality_error of equality_error + | Moregen_error of moregen_error + val diff : type_expr -> type_expr -> (desc, _) elt (** [flatten f trace] flattens all elements of type {!desc} in diff --git a/typing/includeclass.ml b/typing/includeclass.ml index 2f0c057ff9e..f23843f2ac2 100644 --- a/typing/includeclass.ml +++ b/typing/includeclass.ml @@ -49,9 +49,9 @@ 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 report_comparison_error ppf = function + | Errortrace.Equality_error {subst; env; trace} -> Printtyp.report_equality_error ppf subst env trace + | Errortrace.Moregen_error {env; trace} -> Printtyp.report_moregen_error ppf env trace let include_err ppf = function @@ -60,8 +60,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 {subst; env; trace} -> + Printtyp.report_equality_error ppf subst env trace (function ppf -> fprintf ppf "A type parameter has type") (function ppf -> @@ -73,20 +73,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) -> + | CM_Parameter_mismatch {env; trace} -> Printtyp.report_moregen_error ppf env trace (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, err) -> + report_comparison_error ppf 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, err) -> + report_comparison_error ppf err (function ppf -> fprintf ppf "The method %s@ has type" lab) (function ppf -> diff --git a/typing/includecore.ml b/typing/includecore.ml index 20aa7493bf4..535dee63e00 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 trace -> raise (Dont_match (Type {env; trace})) | () -> begin match (vd1.val_kind, vd2.val_kind) with | (Val_prim p1, Val_prim p2) -> begin @@ -131,7 +131,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 +143,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 @@ -168,18 +168,18 @@ type private_variant_mismatch = | 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,13 +188,18 @@ type type_mismatch = | Unboxed_representation of position | Immediate of Type_immediacy.Violation.t +let report_type_inequality ppf ({subst; env; trace} : Errortrace.equality_error) = + Printtyp.report_equality_error ppf subst env trace + (fun ppf -> Format.fprintf ppf "The type") + (fun ppf -> Format.fprintf ppf "is not equal to the type") + let report_label_mismatch first second ppf err = - let pr fmt = Format.fprintf ppf fmt in match (err : label_mismatch) with - | Type _ -> pr "The types are not equal." + | Type eq_err -> + report_type_inequality ppf eq_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 = @@ -202,7 +207,7 @@ let report_record_mismatch first second decl ppf err = match err with | Label_mismatch (l1, l2, err) -> pr - "@[Fields do not match:@;<1 2>%a@ is not compatible with:\ + "@[Fields do not match:@;<1 2>%a@ is not the same as:\ @;<1 2>%a@ %a@]" Printtyp.label l1 Printtyp.label l2 @@ -221,7 +226,7 @@ let report_record_mismatch first second decl ppf err = let report_constructor_mismatch first second decl ppf err = let pr fmt = Format.fprintf ppf fmt in match (err : constructor_mismatch) with - | Type _ -> pr "The types are not equal." + | Type eq_err -> report_type_inequality ppf eq_err | Arity -> pr "They have different arities." | Inline_record err -> report_record_mismatch first second decl ppf err | Kind ord -> @@ -238,7 +243,7 @@ let report_variant_mismatch first second decl ppf err = match (err : variant_mismatch) with | Constructor_mismatch (c1, c2, err) -> pr - "@[Constructors do not match:@;<1 2>%a@ is not compatible with:\ + "@[Constructors do not match:@;<1 2>%a@ is not the same as:\ @;<1 2>%a@ %a@]" Printtyp.constructor c1 Printtyp.constructor c2 @@ -255,7 +260,7 @@ let report_extension_constructor_mismatch first second decl ppf err = match (err : extension_constructor_mismatch) with | Constructor_privacy -> pr "A private type would be revealed." | Constructor_mismatch (id, ext1, ext2, err) -> - pr "@[Constructors do not match:@;<1 2>%a@ is not compatible with:\ + pr "@[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 @@ -302,7 +307,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(subst,trace) -> Some (Type {subst; env; trace}) | () -> None end | Types.Cstr_record l1, Types.Cstr_record l2 -> @@ -316,7 +321,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(subst, trace) -> Some (Type {subst; env; trace}) | () -> compare_constructor_arguments ~loc env [r1] [r2] args1 args2 end | Some _, None -> Some (Explicit_return_type First) @@ -357,8 +362,8 @@ 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(subst, trace) -> + Some (Type {subst; env; trace} : label_mismatch) | () -> None end @@ -429,8 +434,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(subst, trace) -> + Some (Types {subst; env; trace} : private_variant_mismatch) | () -> None end | (s, f1, f2) :: pairs -> begin @@ -482,7 +487,7 @@ 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(subst, trace) -> Some (Types {subst; env; trace}) | () -> None end @@ -512,7 +517,7 @@ let type_manifest env ty1 params1 ty2 params2 priv2 = | 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)) + | exception Ctype.Equality(subst, trace) -> Some (Manifest {subst; env; trace}) | () -> None end @@ -530,7 +535,7 @@ 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(subst, trace) -> Some (Constraint {subst; env; trace}) | () -> None end | (Some ty1, Some ty2) -> @@ -541,10 +546,10 @@ let type_declarations ?(equality = false) ~loc env ~mark name 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(subst, trace) -> Some (Constraint {subst; env; trace}) | () -> match Ctype.equal env false [ty1] [ty2] with - | exception Ctype.Equality trace -> Some (Manifest(env, trace)) + | exception Ctype.Equality(subst, trace) -> Some (Manifest {subst; env; trace}) | () -> None in if err <> None then err else @@ -648,8 +653,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(subst, trace) -> + Some (Constructor_mismatch (id, ext1, ext2, Type {subst; env; trace})) | () -> let r = compare_constructors ~loc env diff --git a/typing/includecore.mli b/typing/includecore.mli index 95bcbb23cb9..20ca80afd2f 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 @@ -71,18 +71,18 @@ type private_variant_mismatch = | 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 diff --git a/typing/printtyp.ml b/typing/printtyp.ml index 8668af77f4b..05e2fcebef0 100644 --- a/typing/printtyp.ml +++ b/typing/printtyp.ml @@ -2286,8 +2286,18 @@ 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 = +let rec match_names_for_substs = function + | [] -> () + | ({desc = Tvar _} as l, ({desc = Tvar _} as r)) :: tl -> + match_names_for_substs tl; + let name = name_of_type new_name l in + names := (r, name) :: !names + | _ :: tl -> match_names_for_substs tl + +(* [subst] comes out of equality, and is [[]] otherwise *) +let error trace_format subst env tr txt1 ppf txt2 ty_expect_explanation = reset (); + match_names_for_substs 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 @@ -2316,19 +2326,19 @@ let error trace_format env tr txt1 ppf txt2 ty_expect_explanation = print_labels := true; raise exn -let report_error trace_format ppf env tr +let report_error trace_format ppf subst env tr ?(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 = + report_error Unification ppf [] +let report_equality_error ppf subst = + report_error Equality ppf subst ?type_expected_explanation:None +let report_moregen_error ppf = + report_error Moregen ppf [] ?type_expected_explanation:None module Subtype = struct (* There's a frustrating amount of code duplication between this module and diff --git a/typing/printtyp.mli b/typing/printtyp.mli index 01c76c89c7a..23daa325900 100644 --- a/typing/printtyp.mli +++ b/typing/printtyp.mli @@ -185,7 +185,7 @@ val report_unification_error : unit val report_equality_error : - formatter -> Env.t -> + formatter -> Errortrace.equality_subst -> Env.t -> Errortrace.comparison Errortrace.t -> (formatter -> unit) -> (formatter -> unit) -> unit diff --git a/typing/typedecl.ml b/typing/typedecl.ml index 22960c69d3e..bdb053c4160 100644 --- a/typing/typedecl.ml +++ b/typing/typedecl.ml @@ -585,8 +585,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(subst,trace) -> + Some (Includecore.Constraint {subst; env; trace}) | () -> Includecore.type_declarations ~loc ~equality:true env ~mark:true