flambda-backend: Use modal kinds to do mode crossing (#2310)

* Move and rename Sub_result

* Use Le_result in Mode

* Rename functions in jkind to match Mode

* Add modal upper bounds to kinds

* Test mode crossing

* Fix dynlink tests

* More modal kinds tests, for expected modes

* mode_cross_left

* Mode-crossing the expected mode

* Checkpoint in killing off immediate

* Kill off unused immediacy checks

* Refactor constrain_type_jkind

* check_type_externality

* Use modal kinds for the transl immediacy check

* Remove Gc_ignorable_check reason

* bootstrap

* Renaming in jkind

* Move comment

* Localize less_or_equal to jkind

* mode crossing in enlarge_type

* Comments about immediate64 mode crossing

* Comments in [mode_cross_right]

* Migrate new alloc_mode_cross_to_max_min to new setup

* bootstrap

---------

Co-authored-by: Zesen Qian <[email protected]>

.depend

@@ -1094,6 +1094,7 @@ typing/includemod_errorprinter.cmi : \
 typing/jkind.cmo : \
     typing/path.cmi \
     parsing/parsetree.cmi \
+    typing/mode.cmi \
     utils/misc.cmi \
     parsing/location.cmi \
     utils/language_extension.cmi \
@@ -1105,6 +1106,7 @@ typing/jkind.cmo : \
 typing/jkind.cmx : \
     typing/path.cmx \
     parsing/parsetree.cmi \
+    typing/mode.cmx \
     utils/misc.cmx \
     parsing/location.cmx \
     utils/language_extension.cmx \
@@ -1116,6 +1118,7 @@ typing/jkind.cmx : \
 typing/jkind.cmi : \
     typing/path.cmi \
     parsing/parsetree.cmi \
+    typing/mode.cmi \
     parsing/location.cmi \
     parsing/jane_asttypes.cmi \
     typing/ident.cmi
@@ -1135,7 +1138,8 @@ typing/mode.cmi : \
     typing/mode_intf.cmi
 typing/mode_intf.cmi : \
     typing/solver_intf.cmi \
-    typing/solver.cmi
+    typing/solver.cmi \
+    utils/misc.cmi
 typing/mtype.cmo : \
     typing/types.cmi \
     typing/subst.cmi \
@@ -4172,11 +4176,13 @@ lambda/transl_array_comprehension.cmi : \
     lambda/debuginfo.cmi
 lambda/transl_comprehension_utils.cmo : \
     utils/targetint.cmi \
+    typing/primitive.cmi \
     lambda/lambda.cmi \
     typing/ident.cmi \
     lambda/transl_comprehension_utils.cmi
 lambda/transl_comprehension_utils.cmx : \
     utils/targetint.cmx \
+    typing/primitive.cmx \
     lambda/lambda.cmx \
     typing/ident.cmx \
     lambda/transl_comprehension_utils.cmi

compilerlibs/Makefile.compilerlibs

@@ -84,10 +84,10 @@ PARSING_CMI = \
 TYPING = \
   typing/solver.cmo \
   typing/path.cmo \
+  typing/mode.cmo \
   typing/jkind.cmo \
   typing/primitive.cmo \
   typing/shape.cmo \
-  typing/mode.cmo \
   typing/types.cmo \
   typing/btype.cmo \
   typing/oprint.cmo \

lambda/matching.ml

@@ -109,7 +109,7 @@ let dbg = false
 (* CR layouts v5: When we're ready to allow non-values, these can be deleted or
    changed to check for void. *)
 let jkind_layout_must_be_value loc jkind =
-  match Jkind.(sub jkind (value ~why:V1_safety_check)) with
+  match Jkind.(sub_or_error jkind (value ~why:V1_safety_check)) with
   | Ok _ -> ()
   | Error e -> raise (Error (loc, Non_value_layout e))
 

otherlibs/dynlink/dune

@@ -80,12 +80,12 @@
     ident
     path
     shape
-    jkind
-    primitive
     solver_intf
     solver
     mode_intf
     mode
+    jkind
+    primitive
     types
     btype
     lazy_backtrack
@@ -351,9 +351,9 @@
       .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Builtin_attributes.cmo
       .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Load_path.cmo
       .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Ast_mapper.cmo
-      .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Jkind.cmo
       .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Solver.cmo
       .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Mode.cmo
+      .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Jkind.cmo
       .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Types.cmo
       .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Btype.cmo
       .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Subst.cmo
@@ -431,9 +431,9 @@
       .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Ast_iterator.cmx
       .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Builtin_attributes.cmx
       .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Ast_mapper.cmx
-      .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Jkind.cmx
       .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Solver.cmx
       .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Mode.cmx
+      .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Jkind.cmx
       .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Types.cmx
       .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Btype.cmx
       .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Subst.cmx

testsuite/tests/typing-layouts-err-msg/immediate.ml

@@ -66,5 +66,3 @@ Error: This expression has type [ `A | `B ]
          of the definition of t at line 1, characters 0-22.
 |}]
 
-(* Gc_ignorable_check *)
-(* Only used within [Result.is_ok] and not thrown as an exception *)

testsuite/tests/typing-layouts-err-msg/immediate64.ml

@@ -6,11 +6,5 @@
 (*****************************)
 (* Immediate64 layout errors *)
 
-(* Local_mode_cross_check *)
-(* Only used within [Result.is_ok] and not thrown as an exception *)
-
-(* Gc_ignorable_check *)
-(* Only used within [Result.is_ok] and not thrown as an exception *)
-
 (* Separability_check *)
 (* Only used within [Result.is_ok] and not thrown as an exception *)

testsuite/tests/typing-local/crossing.ml

@@ -347,7 +347,7 @@ val f : local_ M.t -> M.t = <fun>
 val f : local_ t2 -> t2 = <fun>
 |}]
 
-(* This test needs the snapshotting in [is_immediate] to prevent a type error
+(* This test needs the snapshotting in [type_jkind_purely] to prevent a type error
    from the use of the gadt equation in the inner scope. *)
 type _ t_gadt = Int : int t_gadt
 type 'a t_rec = { fld : 'a }
@@ -440,6 +440,28 @@ Line 1, characters 12-39:
 Error: Type int -> local_ int is not a subtype of local_ int -> int
 |}]
 
+(* Testing mode crossing in [enlarge_type] *)
+module M : sig
+  val foo : (int -> unit) -> (local_ int -> unit)
+end = struct
+  let foo f = (f :> local_ int -> unit)
+end
+[%%expect{|
+module M : sig val foo : (int -> unit) -> local_ int -> unit end
+|}]
+
+(* Same, but in opposite variance.
+   The following coercion is still strenghthening *)
+module M : sig
+  val foo : ((local_ int -> int) -> unit) -> ((int -> int) -> unit)
+end = struct
+  let foo f = (f :> (int -> int) -> unit)
+end
+[%%expect{|
+module M :
+  sig val foo : ((local_ int -> int) -> unit) -> (int -> int) -> unit end
+|}]
+
 (* Mode crossing at identifiers - in the following, x and y are added to the
 environment at mode local, but they cross to global when they are refered to
 again. Note that ref is polymorphic and thus doesn't trigger crossing. *)

testsuite/tests/typing-local/local.ml

@@ -1815,6 +1815,12 @@ let foo (local_ x) =
   | _ -> ()
 [%%expect{|
 val foo : local_ int -> unit = <fun>
+|}, Principal{|
+Line 3, characters 21-22:
+3 |   | 0 as y -> escape y
+                         ^
+Error: This value escapes its region
+  Hint: This argument cannot be local, because it is an argument in a tail call
 |}]
 
 let foo (local_ x) =
@@ -1823,6 +1829,12 @@ let foo (local_ x) =
   | _ -> ()
 [%%expect{|
 val foo : local_ char -> unit = <fun>
+|}, Principal{|
+Line 3, characters 28-29:
+3 |   | 'a'..'e' as y -> escape y
+                                ^
+Error: This value escapes its region
+  Hint: This argument cannot be local, because it is an argument in a tail call
 |}]
 
 let foo (local_ x) =