Adjust delayed layout checks in typedecl to fix a kind inference bug. (#2246)

Author: ccasin

ocaml/boot/ocamlc

@@ -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.
 |}];;
 

ocaml/testsuite/tests/typing-layouts-float64/basics.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

ocaml/testsuite/tests/typing-layouts/annots.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.
+|}]

ocaml/testsuite/tests/typing-layouts/basics.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. *)

ocaml/testsuite/tests/typing-layouts/basics_alpha.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.
 |}]
 

ocaml/testsuite/tests/typing-layouts/datatypes.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.
 |}]
 

ocaml/testsuite/tests/typing-layouts/datatypes_alpha.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
-    "@[<v>Layout mismatch in final type declaration consistency check.@ \
+    "@[<v>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,16 +2756,17 @@ 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 "@[<v>Constraints are not satisfied in this type.@ ";
       Printtyp.report_unification_error ppf env err
         (fun ppf -> fprintf ppf "Type")
         (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];

ocaml/typing/typedecl.ml

@@ -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