Consider modalities when adding baggage to with-kinds (#3401)

* Add modalities to With in the parsetree

Parse and represent optional modalities on `with` in jkind annotations. This
supports jkind annotations like:

    value mod portable many uncontended with 'a @@ uncontended with int

* Consider modalities when adding baggage to with-kinds

If a field has a constant modality, or a type is annotated with a constant
modality, then skip that type when adding it as baggage to the kind, both when
converting user-written kind annotations and inferring kinds on types.

The guts of this is a big, ugly pattern match on Jkind_axis and
Modes.Modality.Const.axis, which ideally can go away or get much simpler with a
refactor to unify these two types, but I decided to do it this way for now to
get something working that's known-correct, and refactor under green

Co-authored-by: Richard Eisenberg <[email protected]>

parsing/ast_helper.ml

@@ -142,7 +142,7 @@ module Typ = struct
         | Default as x -> x
         | Abbreviation _ as x -> x
         | Mod (jkind, modes) -> Mod (loop_jkind jkind, modes)
-        | With (jkind, typ) -> With (loop_jkind jkind, loop typ)
+        | With (jkind, typ, modalities) -> With (loop_jkind jkind, loop typ, modalities)
         | Kind_of typ -> Kind_of (loop typ)
         | Product jkinds -> Product (List.map loop_jkind jkinds)
       in

parsing/ast_iterator.ml

@@ -842,9 +842,10 @@ let default_iterator =
          | Mod (t, mode_list) ->
              this.jkind_annotation this t;
              this.modes this mode_list
-         | With (t, ty) ->
+         | With (t, ty, modalities) ->
              this.jkind_annotation this t;
-             this.typ this ty
+             this.typ this ty;
+             this.modalities this modalities
          | Kind_of ty -> this.typ this ty
          | Product ts -> List.iter (this.jkind_annotation this) ts);
 

parsing/ast_mapper.ml

@@ -946,8 +946,8 @@ let default_mapper =
         | Abbreviation (s : string) -> Abbreviation s
         | Mod (t, mode_list) ->
           Mod (this.jkind_annotation this t, this.modes this mode_list)
-        | With (t, ty) ->
-          With (this.jkind_annotation this t, this.typ this ty)
+        | With (t, ty, modalities) ->
+          With (this.jkind_annotation this t, this.typ this ty, this.modalities this modalities)
         | Kind_of ty -> Kind_of (this.typ this ty)
         | Product ts -> Product (List.map (this.jkind_annotation this) ts)
       in

parsing/depend.ml

@@ -139,9 +139,9 @@ and add_jkind bv (jkind : jkind_annotation) =
   | Default -> ()
   | Abbreviation _ -> ()
   | Mod (jkind, (_ : modes)) -> add_jkind bv jkind
-  | With (jkind, typ) ->
+  | With (jkind, typ, (_ : modalities)) ->
       add_jkind bv jkind;
-      add_type bv typ
+      add_type bv typ;
   | Kind_of typ ->
       add_type bv typ
   | Product jkinds ->

parsing/parser.mly

@@ -3980,9 +3980,8 @@ jkind_desc:
       in
       Mod ($1, modes)
     }
-  (* CR layouts v2.8: The types should be separated by AND, not WITH *)
-  | jkind_annotation WITH core_type {
-      With ($1, $3)
+  | jkind_annotation WITH core_type optional_atat_modalities_expr {
+      With ($1, $3, $4)
     }
   | ident {
       Abbreviation $1

parsing/parsetree.mli

@@ -1299,7 +1299,7 @@ and jkind_annotation_desc =
   (* CR layouts v2.8: [mod] can have only layouts on the left, not
      full kind annotations. We may want to narrow this type some. *)
   | Mod of jkind_annotation * modes
-  | With of jkind_annotation * core_type
+  | With of jkind_annotation * core_type * modalities
   | Kind_of of core_type
   | Product of jkind_annotation list
 

parsing/pprintast.ml

@@ -463,11 +463,13 @@ and jkind_annotation ?(nested = false) ctxt f k = match k.pjkind_desc with
           (pp_print_list ~pp_sep:pp_print_space mode) modes
       ) f (t, modes)
     end
-  | With (t, ty) ->
-    Misc.pp_parens_if nested (fun f (t, ty) ->
-      pp f "%a with %a" (jkind_annotation ~nested:true ctxt) t (core_type ctxt)
-        ty
-    ) f (t, ty)
+  | With (t, ty, modalities) ->
+    Misc.pp_parens_if nested (fun f (t, ty, modalities) ->
+      pp f "%a with %a%a"
+        (jkind_annotation ~nested:true ctxt) t
+        (core_type ctxt) ty
+        optional_space_atat_modalities modalities;
+    ) f (t, ty, modalities)
   | Kind_of ty -> pp f "kind_of_ %a" (core_type ctxt) ty
   | Product ts ->
     Misc.pp_parens_if nested (fun f ts ->

parsing/printast.ml

@@ -506,10 +506,11 @@ and jkind_annotation i ppf (jkind : jkind_annotation) =
       line i ppf "Mod\n";
       jkind_annotation (i+1) ppf jkind;
       modes (i+1) ppf m
-  | With (jkind, type_) ->
+  | With (jkind, type_, modalities_) ->
       line i ppf "With\n";
       jkind_annotation (i+1) ppf jkind;
-      core_type (i+1) ppf type_
+      core_type (i+1) ppf type_;
+      modalities (i+1) ppf modalities_
   | Kind_of type_ ->
       line i ppf "Kind_of\n";
       core_type (i+1) ppf type_

printer/printast_with_mappings.ml

@@ -532,10 +532,11 @@ and jkind_annotation i ppf (jkind : jkind_annotation) =
       line i ppf "Mod\n";
       jkind_annotation (i+1) ppf jkind;
       modes (i+1) ppf m
-  | With (jkind, type_) ->
+  | With (jkind, type_, modalities) ->
       line i ppf "With\n";
       jkind_annotation (i+1) ppf jkind;
-      core_type (i+1) ppf type_
+      core_type (i+1) ppf type_;
+      list i modality ppf modalities
   | Kind_of type_ ->
       line i ppf "Kind_of\n";
       core_type (i+1) ppf type_

testsuite/tests/language-extensions/pprintast_unconditional.ml

@@ -17,6 +17,7 @@ let () = Language_extension.set_universe_and_enable_all
 module Example = struct
   open Parsetree
   open Parse
+  open Asttypes
   open struct
     let loc = Location.none
     let located =  Location.mknoloc
@@ -31,6 +32,10 @@ module Example = struct
   let structure        = parse implementation "include functor F"
   let module_expr      = parse module_expr "struct include functor F end"
   let toplevel_phrase  = parse toplevel_phrase "#2.17;;"
+  let modality         = { txt = Modality "uncontended"
+                         ; loc
+                         }
+  let modalities       = [ modality ]
   let class_field      = { pcf_desc = Pcf_initializer expression
                          ; pcf_loc = loc
                          ; pcf_attributes = []
@@ -98,7 +103,9 @@ module Example = struct
           ( { pjkind_loc = loc;
               pjkind_desc = Abbreviation "value";
             }
-          , core_type );
+          , core_type
+          , modalities
+          );
     }
 
   let mode = { Location.txt = (Parsetree.Mode "global"); loc }

testsuite/tests/language-extensions/pprintast_unconditional.reference

@@ -57,7 +57,7 @@ tyvar_of_name: 'no_tyvars_require_extensions
 
 tyvar: 'no_tyvars_require_extensions
 
-jkind: value with local_ ('a : value) -> unit
+jkind: value with local_ ('a : value) -> unit @@ uncontended
 
 mode: global
 
@@ -122,7 +122,7 @@ tyvar_of_name: 'no_tyvars_require_extensions
 
 tyvar: 'no_tyvars_require_extensions
 
-jkind: value with local_ ('a : value) -> unit
+jkind: value with local_ ('a : value) -> unit @@ uncontended
 
 mode: global
 

testsuite/tests/parsetree/source_jane_street.ml

@@ -1109,18 +1109,38 @@ val inc : 'a with_idx -> 'a with_idx = <fun>
 (***************)
 (* Modal kinds *)
 
+(* supported *)
+type 'a list : immutable_data with 'a
+type ('a, 'b) either : immutable_data with 'a * 'b
+type 'a contended : immutable_data with 'a @@ contended
+type 'a contended_with_int : immutable_data with 'a @@ contended with int
+
+[%%expect{|
+type 'a list
+  : value mod many with 'a uncontended with 'a portable with 'a
+              unyielding with 'a
+type ('a, 'b) either
+  : value mod many with 'a * 'b uncontended with 'a * 'b
+              portable with 'a * 'b unyielding with 'a * 'b
+type 'a contended
+  : value mod many with 'a uncontended portable with 'a unyielding with 'a
+type 'a contended_with_int
+  : value mod many with int
+'a uncontended with int portable with int
+'a
+              unyielding with int
+'a
+|}]
+
+(* not yet supported *)
 module _ : sig
-  type 'a list : immutable_data with 'a
-  type ('a, 'b) either : immutable_data with 'a * 'b
   type 'a gel : kind_of_ 'a mod global
   type 'a t : _
   kind_abbrev_ immediate = value mod global unique many sync uncontended
   kind_abbrev_ immutable_data = value mod sync uncontended many
   kind_abbrev_ immutable = value mod uncontended
   kind_abbrev_ data = value mod sync many
 end = struct
-  type 'a list : immutable_data with 'a
-  type ('a, 'b) either : immutable_data with 'a * 'b
   type 'a gel : kind_of_ 'a mod global
   type 'a t : _
   kind_abbrev_ immediate = value mod global unique many sync uncontended
@@ -1133,9 +1153,9 @@ end
    supported. *)
 
 [%%expect{|
-Line 13, characters 16-27:
-13 |   type 'a gel : kind_of_ 'a mod global
-                     ^^^^^^^^^^^
+Line 9, characters 16-27:
+9 |   type 'a gel : kind_of_ 'a mod global
+                    ^^^^^^^^^^^
 Error: Unimplemented kind syntax
 |}]
 

testsuite/tests/typing-jkind-bounds/basics.ml

@@ -1212,16 +1212,21 @@ Error: The kind of type "t" is value mod external_
 (* CR layouts v2.8: this should be accepted *)
 
 type 'a t : value mod many = { x : 'a @@ many }
-type 'a t : value mod uncontended = { x : 'a @@ uncontended }
+type 'a t : value mod uncontended = { x : 'a @@ contended }
 type 'a t : value mod portable = { x : 'a @@ portable }
 [%%expect {|
-Line 1, characters 0-47:
-1 | type 'a t : value mod many = { x : 'a @@ many }
-    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is immutable_data
-         because it's a boxed record type.
-       But the kind of type "t" must be a subkind of value mod many
-         because of the annotation on the declaration of the type t.
+type 'a t = { x : 'a @@ many; }
+type 'a t = { x : 'a @@ contended; }
+type 'a t = { x : 'a @@ portable; }
+|}]
+
+type 'a t : immutable_data with 'a @@ many = { x : 'a @@ many }
+type 'a t : immutable_data with 'a @@ contended = { x : 'a @@ contended }
+type 'a t : immutable_data with 'a @@ portable = { x : 'a @@ portable }
+[%%expect{|
+type 'a t = { x : 'a @@ many; }
+type 'a t = { x : 'a @@ contended; }
+type 'a t = { x : 'a @@ portable; }
 |}]
 
 type 'a t : value mod unique = { x : 'a @@ unique }