Add a new attribute for allowing any mode crossing

[glittershark]

Replace the [@@unsafe_allow_any_kind_in_{impl,intf}] attributes with a new [@@unsafe_allow_any_mode_crossing] attribute. This is different in that it:

1. Works on the type declaration, not the inclusion check, so is more powerful - it can be used to illegally mode cross types defined in the same module, or illegally mode cross non-abstract types in interfaces. The latter especially is necessary to fully subsume -allow-illegal-crossing in stdlib
2. Only allows changing the modal bounds of a kind, not the layout - it's unclear that anyone should ever want to unsafely change the layout of a kind; I personally can't think of any sound reason to do so.

Some past discussion on the specific syntax for this attribute suggested specifying the bounds directly on the attribute, rather than using the jkind annotation, but I and others (@tdelvecchio-jsc, @ccasin) feel that this approach is a better design for the sake of consistency and ease-of-use.

[dkalinichenko-js]

Only allows changing the modal bounds of a kind, not the layout - it's unclear that anyone should ever want to unsafely change the layout of a kind; I personally can't think of any sound reason to do so.

We might have those reasons when we have gc_ignorable, but the change to accommodate that can happen later.

[goldfirere]

I continue to think this is not quite the right implementation for this feature. For one, it allows (I think) a type to have a lower kind than its manifest. (Maybe not? The narrow_to_manifest_jkind comes after this, so maybe it's ok -- but subtle.) Another problem is that the new kind is not checked in the inclusion check. That is, I think something like this might be accepted:

module M : sig
  type t : value mod contended = { mutable x : int } [@@unsafe_allow_any_mode_crossing]
end = struct
  type t = { mutable x : int }
end

Maybe that's OK? But it's pretty strange.

Instead of this approach, I really think it would be better to put the mode-crossing behavior in the type_kind. The syntax for this is anyone's design -- I'm fine just ripping the mode crossing from the existing jkind annotation (and erroring if that jkind annotation doesn't exist). (My proposal for putting this in the type_kind wasn't about syntax, but only about semantics.) Yet the mode-crossing behavior is really part of the concrete definition of this type, which is what the type_kind is meant to represent. I think it should be needed only for records and variants, not abstract or open kinds.

[glittershark]

I continue to think this is not quite the right implementation for this feature. For one, it allows (I think) a type to have a lower kind than its manifest. (Maybe not? The narrow_to_manifest_jkind comes after this, so maybe it's ok -- but subtle.)

yeah, I think that's reasonable; at the very least we should test that this doesn't allow crossing more than the manifest (though I could see us wanting that!)

Another problem is that the new kind is not checked in the inclusion check. That is, I think something like this might be accepted:

module M : sig
  type t : value mod contended = { mutable x : int } [@@unsafe_allow_any_mode_crossing]
end = struct
  type t = { mutable x : int }
end

Maybe that's OK? But it's pretty strange.

I think this is ok, and don't necessarily also feel that it's strange - but I'm happy to defer to you on this; it's easy enough to check

Instead of this approach, I really think it would be better to put the mode-crossing behavior in the type_kind. The syntax for this is anyone's design -- I'm fine just ripping the mode crossing from the existing jkind annotation (and erroring if that jkind annotation doesn't exist). (My proposal for putting this in the type_kind wasn't about syntax, but only about semantics.) Yet the mode-crossing behavior is really part of the concrete definition of this type, which is what the type_kind is meant to represent. I think it should be needed only for records and variants, not abstract or open kinds.

If we do something like:

diff --git a/typing/types.ml b/typing/types.ml
index b9f363f2cc..e02d59e526 100644
--- a/typing/types.ml
+++ b/typing/types.ml
@@ -275,12 +275,15 @@ type type_declaration =
 and type_decl_kind =
   (label_declaration, label_declaration, constructor_declaration) type_kind
 
+and unsafe_mode_crossing =
+  { modal_upper_bounds : Mode.Alloc.Const.t }
+
 and ('lbl, 'lbl_flat, 'cstr) type_kind =
     Type_abstract of type_origin
-  | Type_record of 'lbl list * record_representation
+  | Type_record of 'lbl list * record_representation * unsafe_mode_crossing option
   | Type_record_unboxed_product of
-      'lbl_flat list * record_unboxed_product_representation
-  | Type_variant of 'cstr list * variant_representation
+      'lbl_flat list * record_unboxed_product_representation * unsafe_mode_crossing option
+  | Type_variant of 'cstr list * variant_representation * unsafe_mode_crossing option
   | Type_open
 
 and tag = Ordinary of {src_index: int;     (* Unique name (per type) *)

then the process of figuring out the "full" kind of a type_declaration involves looking at its type_jkind, then also looking at its type_kind, and maybe applying the bounds from that. that seems a litttle finicky (and easy to forget to do, though maybe this only happens in estimate_type_jkind anyway?). Maybe it's still worth doing for the reasons you listed (or for other reasons), though - or maybe I'm misunderstanding what you mean by "put mode-crossing behavior in the type_kind"?

[goldfirere]

Putting this in the type_kind does not mean "don't put it in the type_jkind" (though I understand how you might think so). For all type_kinds other than Type_abstract, the type_jkind is essentially just a cache -- an imperfect one that might be improved through expansion. An earlier implementation of this all didn't even have type_jkind; it just had a jkind field in Type_abstract. (I moved to have type_jkind. There's a chance I was wrong, as I've learned more about how this all works.)

So my thought is to make the change you've proposed above (with unsafe_mode_crossing), but still put the right jkind in type_jkind. The reason to put stuff into the type_kind is that the inclusion check looks at type_kinds and makes sure they're the same. Much of the challenge around the current illegal-crossing story is that the type_kind has insufficient information. Or, put another way: if a type has at least one = sign, then its jkind should be completely determined by what's after an =. Yet I mean this semantically, not syntactically, so e.g. type t : value mod uncontended = { mutable x : int } [@@unsafe_allow_any_more_crossing] has the full jkind specified to the right of the =, because the value mod uncontended is stored as part of the type_kind.

Yet another way to think about this: if there is at least one =, any jkind annotation is purely a check and is then forgotten. (Again, I mean semantically, not necessarily syntactically, if you're opposed to writing the kind in the attribute.)

Does that add up for you?

As for

module M : sig
  type t : value mod contended = { mutable x : int } [@@unsafe_allow_any_mode_crossing]
end = struct
  type t = { mutable x : int }
end

let me rephrase it a bit:

module type S = sig
  type t : value mod contended = { mutable x : int } [@@unsafe_allow_any_mode_crossing]
end

module M = struct
    type t = { mutable x : int }
end

module _ = (M : S)   (* should this be accepted? I think it shouldn't *)
module type S2 = S with type t = M.t  (* should this be accepted? I think it shouldn't *)

I believe the old implementation here accepts the first but not the second, which strikes me as strange.

[glittershark]

I'm convinced. That change is now done (in the last commit, which is the only new one after a rebase on main)

[goldfirere]

Timing out. More later.

[goldfirere]

OK. Done reviewing (including the two commits that arrived between review parts).

[glittershark]

two more commits that need review:

• 5119479
• 249ce25

[goldfirere]

Back to you @glittershark. Nearly there!