Fix a "bug" in Ctype.constrain_type_jkind (#2671)

ocaml/typing/ctype.ml

@@ -1658,6 +1658,9 @@ let instance_prim_layout (desc : Primitive.description) ty =
   else
   let new_sort_and_jkind = ref None in
   let get_jkind () =
+    (* CR layouts v2.8: This should replace only the layout component of the
+       jkind. It's possible that we might want a primitive that accepts a
+       mode-crossing, layout-polymorphic parameter. *)
     match !new_sort_and_jkind with
     | Some (_, jkind) ->
       jkind
@@ -1675,10 +1678,10 @@ let instance_prim_layout (desc : Primitive.description) ty =
          from an outer scope *)
       if level = generic_level && try_mark_node ty then begin
         begin match get_desc ty with
-        | Tvar ({ jkind; _ } as r) when Jkind.is_any jkind ->
+        | Tvar ({ jkind; _ } as r) when Jkind.has_layout_any jkind ->
           For_copy.redirect_desc copy_scope ty
             (Tvar {r with jkind = get_jkind ()})
-        | Tunivar ({ jkind; _ } as r) when Jkind.is_any jkind ->
+        | Tunivar ({ jkind; _ } as r) when Jkind.has_layout_any jkind ->
           For_copy.redirect_desc copy_scope ty
             (Tunivar {r with jkind = get_jkind ()})
         | _ -> ()
@@ -2205,7 +2208,7 @@ let constrain_type_jkind ~fixed env ty jkind =
 let constrain_type_jkind ~fixed env ty jkind =
   (* An optimization to avoid doing any work if we're checking against
      any. *)
-  if Jkind.is_any jkind then Ok ()
+  if Jkind.is_max jkind then Ok ()
   else constrain_type_jkind ~fixed env ty jkind
 
 let check_type_jkind env ty jkind =

ocaml/typing/jkind.ml

@@ -1232,7 +1232,12 @@ let is_void_defaulting = function
   | { jkind = { layout = Sort s; _ }; _ } -> Sort.is_void_defaulting s
   | _ -> false
 
-let is_any jkind = match jkind.jkind.layout with Any -> true | _ -> false
+(* This doesn't do any mutation because mutating a sort variable can't make it
+   any, and modal upper bounds are constant. *)
+let is_max jkind = sub any_dummy_jkind jkind
+
+let has_layout_any jkind =
+  match jkind.jkind.layout with Any -> true | _ -> false
 
 (*********************************)
 (* debugging *)

ocaml/typing/jkind.mli

@@ -346,8 +346,12 @@ val sub_or_error : t -> t -> (unit, Violation.t) result
 (** Like [sub], but returns the subjkind with an updated history. *)
 val sub_with_history : t -> t -> (t, Violation.t) result
 
-(** Checks to see whether a jkind is any. Never does any mutation. *)
-val is_any : t -> bool
+(** Checks to see whether a jkind is the maximum jkind. Never does any
+    mutation. *)
+val is_max : t -> bool
+
+(** Checks to see whether a jkind is has layout. Never does any mutation. *)
+val has_layout_any : t -> bool
 
 (*********************************)
 (* debugging *)

ocaml/typing/primitive.ml

@@ -700,7 +700,7 @@ let prim_has_valid_reprs ~loc prim =
     raise (Error (loc,
             Invalid_native_repr_for_primitive (prim.prim_name)))
 
-let prim_can_contain_jkind_any prim =
+let prim_can_contain_layout_any prim =
   match prim.prim_name with
   | "%array_length"
   | "%array_safe_get"

ocaml/typing/primitive.mli

@@ -119,10 +119,10 @@ val native_name_is_external : description -> bool
     fails. *)
 val prim_has_valid_reprs : loc:Location.t -> description -> unit
 
-(** Check if a primitive can have jkind [any] anywhere within its type
+(** Check if a primitive can have layout [any] anywhere within its type
     declaration. Returns [false] for built-in primitives that inspect
     the layout of type parameters ([%array_length] for example). *)
-val prim_can_contain_jkind_any : description -> bool
+val prim_can_contain_layout_any : description -> bool
 
 type error =
   | Old_style_float_with_native_repr_attribute

ocaml/typing/typedecl.ml

@@ -131,7 +131,7 @@ type error =
   | Nonrec_gadt
   | Invalid_private_row_declaration of type_expr
   | Local_not_enabled
-  | Unexpected_jkind_any_in_primitive of string
+  | Unexpected_layout_any_in_primitive of string
   | Useless_layout_poly
   | Modalities_on_value_description
   | Zero_alloc_attr_unsupported of Builtin_attributes.zero_alloc_attribute
@@ -2653,7 +2653,7 @@ let make_native_repr env core_type ty ~global_repr ~is_layout_poly ~why =
   error_if_has_deep_native_repr_attributes core_type;
   let sort_or_poly =
     match get_desc (Ctype.get_unboxed_type_approximation env ty) with
-    (* This only captures tvars with jkind [any] explicitly quantified within
+    (* This only captures tvars with layout [any] explicitly quantified within
        the declaration.
 
        This is sufficient since [transl_type_scheme] promises that:
@@ -2662,7 +2662,7 @@ let make_native_repr env core_type ty ~global_repr ~is_layout_poly ~why =
          transl)
     *)
     | Tvar {jkind} when is_layout_poly
-                      && Jkind.is_any jkind
+                      && Jkind.has_layout_any jkind
                       && get_level ty = Btype.generic_level -> Poly
     | _ ->
       let sort =
@@ -2793,18 +2793,18 @@ let check_unboxable env loc ty =
     all_unboxable_types
     ()
 
-let has_ty_var_with_jkind_any env ty =
+let has_ty_var_with_layout_any env ty =
   List.exists
-    (fun ty -> Jkind.is_any (Ctype.estimate_type_jkind env ty))
+    (fun ty -> Jkind.has_layout_any (Ctype.estimate_type_jkind env ty))
     (Ctype.free_variables ty)
 
-let unexpected_jkind_any_check prim env cty ty =
-  if Primitive.prim_can_contain_jkind_any prim ||
+let unexpected_layout_any_check prim env cty ty =
+  if Primitive.prim_can_contain_layout_any prim ||
      prim.prim_is_layout_poly then ()
   else
-  if has_ty_var_with_jkind_any env ty then
+  if has_ty_var_with_layout_any env ty then
     raise(Error (cty.ctyp_loc,
-            Unexpected_jkind_any_in_primitive(prim.prim_name)))
+            Unexpected_layout_any_in_primitive(prim.prim_name)))
 
 (* Note regarding jkind checks on external declarations
 
@@ -2852,13 +2852,14 @@ let unexpected_jkind_any_check prim env cty ty =
       point to the source of the mistake which is, in fact, the external
       declaration.
 
-      For this reason, we have [unexpected_jkind_any_check].  It's here to point
-      out this type of mistake early and suggest the use of [@layout_poly].
+      For this reason, we have [unexpected_layout_any_check].  It's here to
+      point out this type of mistake early and suggest the use of
+      [@layout_poly].
 
       An exception is raised if any of these checks fails. *)
 let error_if_containing_unexpected_jkind prim env cty ty =
   Primitive.prim_has_valid_reprs ~loc:cty.ctyp_loc prim;
-  unexpected_jkind_any_check prim env cty ty
+  unexpected_layout_any_check prim env cty ty
 
 (* Translate a value declaration *)
 let transl_value_decl env loc valdecl =
@@ -2918,7 +2919,7 @@ let transl_value_decl env loc valdecl =
         Builtin_attributes.has_layout_poly valdecl.pval_attributes
       in
       if is_layout_poly &&
-         not (has_ty_var_with_jkind_any env ty) then
+         not (has_ty_var_with_layout_any env ty) then
         raise(Error(valdecl.pval_type.ptyp_loc, Useless_layout_poly));
       let native_repr_args, native_repr_res =
         parse_native_repr_attributes
@@ -3688,7 +3689,7 @@ let report_error ppf = function
   | Local_not_enabled ->
       fprintf ppf "@[The local extension is disabled@ \
                    To enable it, pass the '-extension local' flag@]"
-  | Unexpected_jkind_any_in_primitive name ->
+  | Unexpected_layout_any_in_primitive name ->
       fprintf ppf
         "@[The primitive [%s] doesn't work well with type variables of@ \
            layout any. Consider using [@@layout_poly].@]" name

ocaml/typing/typedecl.mli

@@ -171,7 +171,7 @@ type error =
   | Nonrec_gadt
   | Invalid_private_row_declaration of type_expr
   | Local_not_enabled
-  | Unexpected_jkind_any_in_primitive of string
+  | Unexpected_layout_any_in_primitive of string
   | Useless_layout_poly
   | Modalities_on_value_description
   | Zero_alloc_attr_unsupported of Builtin_attributes.zero_alloc_attribute