From e356119d5f71dd3098aa5e687cc5f5da839cc4f2 Mon Sep 17 00:00:00 2001 From: Antal Spector-Zabusky Date: Fri, 7 May 2021 16:43:51 -0400 Subject: [PATCH] Use the new structured errors (#10170) for better error messages We now produce more detailed error messages during various kinds of module inclusion, taking advantage of the new structured error trace generation from #10170. Previously, these errors were "shallow", ending as soon as there was an incompatibility; this patch makes them "deep", reporting the *reasons* for those problems. For example, consider the following module: module M : sig val x : bool * int end = struct let x = false , "not an int" end This now produces the following error: Error: Signature mismatch: Modules do not match: sig val x : bool * string end is not included in sig val x : bool * int end Values do not match: 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 The last two lines are new in this patch. Previously, the error message stopped two lines earlier, omitting the key detail that the reason there is an error is specifically that `string` is not equal to `int`. --- .depend | 2 + Changes | 4 + .../tests/printing-types/disambiguation.ml | 6 +- .../tests/typing-extensions/extensions.ml | 16 +- .../tests/typing-extensions/open_types.ml | 3 +- testsuite/tests/typing-gadts/ambiguity.ml | 6 + testsuite/tests/typing-gadts/pr7160.ml | 5 +- testsuite/tests/typing-gadts/pr7378.ml | 5 +- testsuite/tests/typing-misc/deep.ml | 10 + .../tests/typing-misc/enrich_typedecl.ml | 10 +- testsuite/tests/typing-misc/pr6416.ml | 20 +- testsuite/tests/typing-misc/pr6634.ml | 6 +- testsuite/tests/typing-misc/pr7668_bad.ml | 5 + testsuite/tests/typing-misc/records.ml | 9 +- testsuite/tests/typing-misc/variant.ml | 10 +- .../pr7414_2_bad.compilers.reference | 3 + .../pr7414_bad.compilers.reference | 3 + testsuite/tests/typing-modules/Test.ml | 12 +- .../applicative_functor_type.ml | 1 + .../extension_constructors_errors_test.ml | 2 +- testsuite/tests/typing-modules/functors.ml | 10 +- .../tests/typing-modules/inclusion_errors.ml | 132 +++++- .../module_type_substitution.ml | 4 +- .../typing-modules/nondep_private_abbrev.ml | 3 + testsuite/tests/typing-modules/pr10399.ml | 2 + testsuite/tests/typing-modules/pr6394.ml | 1 + testsuite/tests/typing-modules/pr7818.ml | 6 +- testsuite/tests/typing-modules/pr7851.ml | 9 +- .../typing-modules/records_errors_test.ml | 8 +- .../typing-modules/variants_errors_test.ml | 24 +- .../pr3968_bad.compilers.reference | 22 +- testsuite/tests/typing-objects/Tests.ml | 2 + testsuite/tests/typing-poly/poly.ml | 11 + .../typing-polyvariants-bugs/pr7817_bad.ml | 5 + .../private.compilers.principal.reference | 8 +- .../private.compilers.reference | 8 +- .../short-paths.compilers.reference | 1 + .../test_locations.compilers.reference | 6 + testsuite/tests/typing-unboxed/test.ml | 24 ++ testsuite/tests/typing-warnings/pr6587.ml | 3 + toplevel/topdirs.ml | 38 +- typing/ctype.ml | 378 +++++++++++------- typing/ctype.mli | 28 +- typing/errortrace.ml | 16 + typing/errortrace.mli | 25 ++ typing/includeclass.ml | 20 +- typing/includecore.ml | 217 ++++++---- typing/includecore.mli | 32 +- typing/includemod.ml | 6 +- typing/includemod.mli | 3 +- typing/includemod_errorprinter.ml | 25 +- typing/printtyp.ml | 312 +++++++++------ typing/printtyp.mli | 15 +- typing/typeclass.ml | 104 ++--- typing/typeclass.mli | 12 +- typing/typecore.ml | 148 +++---- typing/typecore.mli | 20 +- typing/typedecl.ml | 99 +++-- typing/typedecl.mli | 12 +- typing/typetexp.ml | 38 +- typing/typetexp.mli | 4 +- utils/misc.ml | 8 + utils/misc.mli | 6 + 63 files changed, 1289 insertions(+), 704 deletions(-) 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 = 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 - "@[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 - (report_label_mismatch first second) err + (report_label_mismatch first second env) err | Label_names (n, name1, name2) -> pr "@[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 - "@[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 - (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 "@[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 - (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 - "@[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 "@[@[%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 "@[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 "@[The definition of %s contains a cycle:@ %a@]" s Printtyp.type_expr ty - | Definition_mismatch (ty, None) -> + | Definition_mismatch (ty, _env, None) -> fprintf ppf "@[@[%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 "@[@[%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 "@[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 "@[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 "@[@[%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 =