Add with-kinds.

jane/doc/extensions/uniqueness/intro.md

@@ -76,9 +76,8 @@ type delayed_free = { id : int; callback : unit -> unit }
 let get_id : delayed_free @ once -> int @ many = fun t -> t.id
 ```
 
-We are working on a feature which will make it possible to use a value as `many`
-if its type prevents it from containing a function. For example, you will then
-be able to use an `int list @ once aliased` as `many` (but not as `unique`).
+This mode-crossing works through container types. For example, you can use an
+`int list @ once aliased` as `many` (but not as `unique`).
 
 ## Checking for Uniqueness
 

jane/doc/proposals/kind-inference.md

@@ -141,7 +141,7 @@ rec {
 q ::= best | not_best   (* quality of an inferred kind; best < not_best *)
 ```
 
-Mode crossing is not covered in this design. 
+Mode crossing is not covered in this design.
 
 However, it may be helpful to know that having e.g. `mod observing` in a kind
 means that `observing` is the upper bound for the locality mode of values whose
@@ -158,14 +158,14 @@ that kind.  Suppose `t : ... mod exclusive`. If a context requires `e` of type
 `exclusive` is sufficient. A requirement of `aliased` (the top mode) is
 completely unaffected.
 
-The key question: if `t : ... mod exclusive` and we have 
+The key question: if `t : ... mod exclusive` and we have
 `type ('a : ... mod aliased) t2`, is `t t2` valid? No! Even though
 `exclusive < aliased`. That's because `mod aliased` puts a *harder* requirement
 on its type (it must be agnostic between all of `unique`, `exclusive`, and
 `aliased`) than `mod exclusive` does (which says the type is agnostic between
 `unique` and `exclusive` only). This means that the subkind relation works
 backwards on monadic axes: `... mod aliased ≤ ... mod exclusive`. For this
-reason, in the presentation above, the monadic axis elements are listed in 
+reason, in the presentation above, the monadic axis elements are listed in
 reverse order: this document does not care about submoding or mode crossing
 directly, and writing the axes in reverse order gives us the right behavior
 on subkinding.
@@ -256,7 +256,7 @@ rec {
 Γ ⊢ jkind with field_types ↠ lay(χ); ⟪Ξ(χ) with types_for(Ξ, field_types)⟫
 ```
 
-In `K_OF`, we produce a kind in terms of `τ`, not just `κ`. This allows us
+In `KS_OF`, we produce a kind in terms of `τ`, not just `κ`. This allows us
 to make use of refinements to `τ` that we learn later, perhaps through
 functor application or GADT refinement.
 

otherlibs/dynlink/dune

@@ -601,8 +601,8 @@
   .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Primitive.cmo
   .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Oprint.cmo
   .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Typemode.cmo
-  .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Jkind.cmo
   .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Btype.cmo
+  .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Jkind.cmo
   .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Subst.cmo
   .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Signature_with_global_bindings.cmo
   .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Bytesections.cmo
@@ -697,8 +697,8 @@
   .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Primitive.cmx
   .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Oprint.cmx
   .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Typemode.cmx
-  .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Jkind.cmx
   .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Btype.cmx
+  .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Jkind.cmx
   .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Subst.cmx
   .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Signature_with_global_bindings.cmx
   .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Bytesections.cmx

parsing/parser.mly

@@ -3964,6 +3964,7 @@ 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)
     }

parsing/parsetree.mli

@@ -1296,6 +1296,8 @@ and module_binding =
 and jkind_annotation_desc =
   | Default
   | Abbreviation of string
+  (* 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
   | Kind_of of core_type

testsuite/tests/typing-immediate/immediate.ml

@@ -160,7 +160,7 @@ end;;
 Line 2, characters 2-41:
 2 |   type t = Foo of int | Bar [@@immediate]
       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data
          because it's a boxed variant type.
        But the kind of type "t" must be a subkind of immediate
          because of the annotation on the declaration of the type t.
@@ -174,7 +174,7 @@ end;;
 Line 2, characters 2-38:
 2 |   type t = { foo : int } [@@immediate]
       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+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 immediate
          because of the annotation on the declaration of the type t.

testsuite/tests/typing-layouts-or-null/reexport.ml

@@ -21,7 +21,9 @@ Lines 2-4, characters 2-16:
 4 |     | This of 'a
 Error: The kind of type "'a or_null" is value_or_null
          because it is the primitive value_or_null type or_null.
-       But the kind of type "'a or_null" must be a subkind of value
+       But the kind of type "'a or_null" must be a subkind of
+         value mod local with 'a aliased with 'a many with 'a
+                   uncontended with 'a portable with 'a internal with 'a
          because of the definition of t at lines 2-4, characters 2-16.
 |}]