diff --git a/ocaml/boot/ocamlc b/ocaml/boot/ocamlc index d08a0b33b7d..049e1b831a1 100755 Binary files a/ocaml/boot/ocamlc and b/ocaml/boot/ocamlc differ diff --git a/ocaml/testsuite/tests/typing-layouts-float64/basics.ml b/ocaml/testsuite/tests/typing-layouts-float64/basics.ml index 365433d74d8..fa1e307a5b0 100644 --- a/ocaml/testsuite/tests/typing-layouts-float64/basics.ml +++ b/ocaml/testsuite/tests/typing-layouts-float64/basics.ml @@ -290,7 +290,7 @@ Error: Layout mismatch in final type declaration consistency check. of the definition of t_float64_id at line 2, characters 0-37. But the layout of 'a must overlap with value, because it instantiates an unannotated type parameter of t5_11, defaulted to layout value. - The fix will likely be to add a layout annotation on a parameter to + A good next step is to add a layout annotation on a parameter to the declaration where this error is reported. |}];; diff --git a/ocaml/testsuite/tests/typing-layouts/annots.ml b/ocaml/testsuite/tests/typing-layouts/annots.ml index 8347e3a0997..8f3425f7580 100644 --- a/ocaml/testsuite/tests/typing-layouts/annots.ml +++ b/ocaml/testsuite/tests/typing-layouts/annots.ml @@ -358,7 +358,7 @@ Error: Layout mismatch in final type declaration consistency check. of the annotation on the universal variable 'a. But the layout of 'a must be a sublayout of immediate, because of the definition of t_imm at line 1, characters 0-27. - The fix will likely be to add a layout annotation on a parameter to + A good next step is to add a layout annotation on a parameter to the declaration where this error is reported. |}] (* CR layouts v1.5: the location on that message is wrong. But it's hard diff --git a/ocaml/testsuite/tests/typing-layouts/basics.ml b/ocaml/testsuite/tests/typing-layouts/basics.ml index 1db5ed5b956..d7d15aa2cce 100644 --- a/ocaml/testsuite/tests/typing-layouts/basics.ml +++ b/ocaml/testsuite/tests/typing-layouts/basics.ml @@ -1026,7 +1026,7 @@ Line 3, characters 2-27: Error: The layout of 'a s is float64, because of the annotation on 'a in the declaration of the type s. - But the layout of 'a s must overlap with value, because + But the layout of 'a s must be a sublayout of value, because it's the type of an object field. |}];; @@ -1838,7 +1838,7 @@ Error: Layout mismatch in final type declaration consistency check. of the annotation on the universal variable 'a. But the layout of 'a must be a sublayout of immediate, because of the definition of t2_imm at line 1, characters 0-28. - The fix will likely be to add a layout annotation on a parameter to + A good next step is to add a layout annotation on a parameter to the declaration where this error is reported. |}] @@ -2330,3 +2330,72 @@ Error: This expression has type t_float64 But the layout of t_float64 must be a sublayout of value, because of the definition of t40 at line 1, characters 0-16. |}] + +(**********************************************************************) +(* Test 41: constraints in manifests in mutually recursive typedecls. *) + +(* This example must be rejected. *) +type t1 = string t2 as (_ : immediate) +and 'a t2 = 'a + +[%%expect{| +Line 2, characters 0-14: +2 | and 'a t2 = 'a + ^^^^^^^^^^^^^^ +Error: Layout mismatch in checking consistency of mutually recursive groups. + This is most often caused by the fact that type inference is not + clever enough to propagate layouts through variables in different + declarations. It is also not clever enough to produce a good error + message, so we'll say this instead: + The layout of 'a t2 is value, because + it instantiates an unannotated type parameter of t2, defaulted to layout value. + But the layout of 'a t2 must be a sublayout of immediate, because + of the annotation on the wildcard _ at line 1, characters 28-37. + A good next step is to add a layout annotation on a parameter to + the declaration where this error is reported. +|}] + +(* This example is unfortunately rejected as a consequence of the fix for the + above in typedecl. If we ever change that so that the below starts working, + make sure [t1]'s parameter is immediate! Previously this was allowed and t1's + parameter was just value (a bug). *) +type 'a t1 = 'a t2 as (_ : immediate) +and 'a t2 = 'a + +[%%expect{| +Line 2, characters 0-14: +2 | and 'a t2 = 'a + ^^^^^^^^^^^^^^ +Error: Layout mismatch in checking consistency of mutually recursive groups. + This is most often caused by the fact that type inference is not + clever enough to propagate layouts through variables in different + declarations. It is also not clever enough to produce a good error + message, so we'll say this instead: + The layout of 'a t2/2 is value, because + it instantiates an unannotated type parameter of t2, defaulted to layout value. + But the layout of 'a t2/2 must be a sublayout of immediate, because + of the annotation on the wildcard _ at line 1, characters 27-36. + A good next step is to add a layout annotation on a parameter to + the declaration where this error is reported. +|}] + +(* This one also unfortunately rejected for the same reason. *) +type t1 = int t2 as (_ : immediate) +and 'a t2 = 'a + +[%%expect{| +Line 2, characters 0-14: +2 | and 'a t2 = 'a + ^^^^^^^^^^^^^^ +Error: Layout mismatch in checking consistency of mutually recursive groups. + This is most often caused by the fact that type inference is not + clever enough to propagate layouts through variables in different + declarations. It is also not clever enough to produce a good error + message, so we'll say this instead: + The layout of 'a t2/3 is value, because + it instantiates an unannotated type parameter of t2, defaulted to layout value. + But the layout of 'a t2/3 must be a sublayout of immediate, because + of the annotation on the wildcard _ at line 1, characters 25-34. + A good next step is to add a layout annotation on a parameter to + the declaration where this error is reported. +|}] diff --git a/ocaml/testsuite/tests/typing-layouts/basics_alpha.ml b/ocaml/testsuite/tests/typing-layouts/basics_alpha.ml index 36c4c52274d..5d5442e955a 100644 --- a/ocaml/testsuite/tests/typing-layouts/basics_alpha.ml +++ b/ocaml/testsuite/tests/typing-layouts/basics_alpha.ml @@ -864,7 +864,7 @@ Line 3, characters 2-24: Error: The layout of 'a s is void, because of the annotation on 'a in the declaration of the type s. - But the layout of 'a s must overlap with value, because + But the layout of 'a s must be a sublayout of value, because it's the type of an object field. |}];; @@ -1892,3 +1892,8 @@ Error: This expression has type t_any but an expression was expected of type (* Test 40: unannotated type parameter defaults to layout value *) (* Doesn't need layouts_alpha. *) + +(**********************************************************************) +(* Test 41: constraints in manifests in mutually recursive typedecls. *) + +(* Doesn't need layouts_alpha. *) diff --git a/ocaml/testsuite/tests/typing-layouts/datatypes.ml b/ocaml/testsuite/tests/typing-layouts/datatypes.ml index 885e572180d..9e6557d67c1 100644 --- a/ocaml/testsuite/tests/typing-layouts/datatypes.ml +++ b/ocaml/testsuite/tests/typing-layouts/datatypes.ml @@ -392,7 +392,7 @@ Error: Layout mismatch in final type declaration consistency check. of the definition of float64_t at line 2, characters 0-29. But the layout of 'a must overlap with value, because it instantiates an unannotated type parameter of t8_5, defaulted to layout value. - The fix will likely be to add a layout annotation on a parameter to + A good next step is to add a layout annotation on a parameter to the declaration where this error is reported. |}] diff --git a/ocaml/testsuite/tests/typing-layouts/datatypes_alpha.ml b/ocaml/testsuite/tests/typing-layouts/datatypes_alpha.ml index a407f0f5242..f9d5e197da3 100644 --- a/ocaml/testsuite/tests/typing-layouts/datatypes_alpha.ml +++ b/ocaml/testsuite/tests/typing-layouts/datatypes_alpha.ml @@ -388,7 +388,7 @@ Error: Layout mismatch in final type declaration consistency check. of the definition of void_t at line 1, characters 0-23. But the layout of 'a must overlap with value, because it instantiates an unannotated type parameter of t8_5, defaulted to layout value. - The fix will likely be to add a layout annotation on a parameter to + A good next step is to add a layout annotation on a parameter to the declaration where this error is reported. |}] @@ -410,7 +410,7 @@ Error: Layout mismatch in final type declaration consistency check. it instantiates an unannotated type parameter of t10, defaulted to layout value. But the layout of 'a must be a sublayout of immediate, because of the definition of imm_t at line 1, characters 0-27. - The fix will likely be to add a layout annotation on a parameter to + A good next step is to add a layout annotation on a parameter to the declaration where this error is reported. |}] @@ -430,7 +430,7 @@ Error: Layout mismatch in final type declaration consistency check. it is the primitive float64 type float#. But the layout of float# must be a sublayout of void, because of the annotation on the universal variable 'b. - The fix will likely be to add a layout annotation on a parameter to + A good next step is to add a layout annotation on a parameter to the declaration where this error is reported. |}] diff --git a/ocaml/typing/typedecl.ml b/ocaml/typing/typedecl.ml index 3a5ce37b854..c239e26b205 100644 --- a/ocaml/typing/typedecl.ml +++ b/ocaml/typing/typedecl.ml @@ -37,6 +37,10 @@ and reaching_type_step = | Expands_to of type_expr * type_expr | Contains of type_expr * type_expr +type bad_jkind_inference_location = + | Check_constraints + | Delayed_checks + type error = Repeated_parameter | Duplicate_constructor of string @@ -73,7 +77,8 @@ type error = | Deep_unbox_or_untag_attribute of native_repr_kind | Jkind_mismatch_of_type of type_expr * Jkind.Violation.t | Jkind_mismatch_of_path of Path.t * Jkind.Violation.t - | Jkind_mismatch_in_check_constraints of type_expr * Jkind.Violation.t + | Jkind_mismatch_due_to_bad_inference of + type_expr * Jkind.Violation.t * bad_jkind_inference_location | Jkind_sort of { kloc : jkind_sort_loc ; typ : type_expr @@ -853,9 +858,12 @@ let rec check_constraints_rec env loc visited ty = | Unification_failure err -> raise (Error(loc, Constraint_failed (env, err))) | Jkind_mismatch { original_jkind; inferred_jkind; ty } -> - raise (Error(loc, Jkind_mismatch_in_check_constraints (ty, - (Jkind.Violation.of_ (Not_a_subjkind - (original_jkind, inferred_jkind)))))) + let violation = + Jkind.Violation.of_ + (Not_a_subjkind (original_jkind, inferred_jkind)) + in + raise (Error(loc, Jkind_mismatch_due_to_bad_inference + (ty, violation, Check_constraints))) | All_good -> () end; List.iter (check_constraints_rec env loc visited) args @@ -1757,11 +1765,29 @@ let transl_type_decl env rec_flag sdecl_list = jkind checks *) List.iter (fun (checks,loc) -> List.iter (fun (ty,jkind) -> - match Ctype.constrain_type_jkind new_env ty jkind with + (* The use [check_type_jkind] rather than [constrain_type_jkind] here is + conservative. It ensures that the delayed checks don't succeed by + mutating type variables from the [temp_env] in a way that won't be + reflected in the final type decls and may be incompatible with them. + An alternative would be to beef up [check_constraints] and really make + sure we re-check any kind constraint that could arise from translating + the typedecl RHSs, for example by looking at Typedtree instead of + what's just in the type environment. See Test 41 in + [tests/typing-layouts/basics.ml] for a subtle example. *) + match Ctype.check_type_jkind new_env ty jkind with | Ok _ -> () | Error err -> - let err = Errortrace.unification_error ~trace:[Bad_jkind (ty,err)] in - raise (Error (loc, Type_clash (new_env, err)))) + (* This inner match is just here to detect when we're rejecting this + program because we're being conservative in the sense of the previous + comment, and issue an error admitting to it. *) + begin match Ctype.constrain_type_jkind new_env ty jkind with + | Error _ -> + let err = Errortrace.unification_error ~trace:[Bad_jkind (ty,err)] in + raise (Error (loc, Type_clash (new_env, err))) + | Ok _ -> + raise (Error (loc, Jkind_mismatch_due_to_bad_inference + (ty, err, Delayed_checks))) + end) checks) delayed_jkind_checks; (* Check that all type variables are closed; this also defaults any remaining @@ -2662,15 +2688,23 @@ module Reaching_path = struct pp path end -let report_jkind_mismatch_in_check_constraints ppf ty violation = +let report_jkind_mismatch_due_to_bad_inference ppf ty violation loc = + let loc = + match loc with + | Check_constraints -> + "final type declaration consistency check" + | Delayed_checks -> + "checking consistency of mutually recursive groups" + in fprintf ppf - "@[Layout mismatch in final type declaration consistency check.@ \ + "@[Layout mismatch in %s.@ \ This is most often caused by the fact that type inference is not@ \ clever enough to propagate layouts through variables in different@ \ declarations. It is also not clever enough to produce a good error@ \ message, so we'll say this instead:@;<1 2>@[%a@]@ \ - The fix will likely be to add a layout annotation on a parameter to@ \ + A good next step is to add a layout annotation on a parameter to@ \ the declaration where this error is reported.@]" + loc (Jkind.Violation.report_with_offender ~offender:(fun ppf -> Printtyp.type_expr ppf ty)) violation @@ -2722,7 +2756,8 @@ let report_error ppf = function in begin match List.find_map get_jkind_error err.trace with | Some (ty, violation) -> - report_jkind_mismatch_in_check_constraints ppf ty violation + report_jkind_mismatch_due_to_bad_inference ppf ty violation + Check_constraints | None -> fprintf ppf "@[Constraints are not satisfied in this type.@ "; Printtyp.report_unification_error ppf env err @@ -2730,8 +2765,8 @@ let report_error ppf = function (fun ppf -> fprintf ppf "should be an instance of"); fprintf ppf "@]" end - | Jkind_mismatch_in_check_constraints (ty, violation) -> - report_jkind_mismatch_in_check_constraints ppf ty violation + | Jkind_mismatch_due_to_bad_inference (ty, violation, loc) -> + report_jkind_mismatch_due_to_bad_inference ppf ty violation loc | Non_regular { definition; used_as; defined_as; reaching_path } -> let reaching_path = Reaching_path.simplify reaching_path in Printtyp.prepare_for_printing [used_as; defined_as]; diff --git a/ocaml/typing/typedecl.mli b/ocaml/typing/typedecl.mli index 3041651cd29..d3ccef0d572 100644 --- a/ocaml/typing/typedecl.mli +++ b/ocaml/typing/typedecl.mli @@ -78,6 +78,10 @@ and reaching_type_step = | Expands_to of type_expr * type_expr | Contains of type_expr * type_expr +type bad_jkind_inference_location = + | Check_constraints + | Delayed_checks + type error = Repeated_parameter | Duplicate_constructor of string @@ -114,7 +118,8 @@ type error = | Deep_unbox_or_untag_attribute of native_repr_kind | Jkind_mismatch_of_type of type_expr * Jkind.Violation.t | Jkind_mismatch_of_path of Path.t * Jkind.Violation.t - | Jkind_mismatch_in_check_constraints of type_expr * Jkind.Violation.t + | Jkind_mismatch_due_to_bad_inference of + type_expr * Jkind.Violation.t * bad_jkind_inference_location | Jkind_sort of { kloc : jkind_sort_loc ; typ : type_expr