flambda-backend: mode crossing of LHS of arrow types by coercing (#1701)

* mode crossing of LHS of arrow types by coercing

* address comment

* quick fix

* mode crossing more complete.

Author: riaqn

testsuite/tests/typing-local/crossing.ml

@@ -358,3 +358,82 @@ type _ t_gadt = Int : int t_gadt
 type 'a t_rec = { fld : 'a; }
 val f : 'a t_gadt -> 'a -> 'a = <fun>
 |}]
+
+(* Mode crossing in coercing arrow types *)
+let foo : int -> int = fun x -> x
+[%%expect{|
+val foo : int -> int = <fun>
+|}]
+
+let foo' : int -> local_ int = fun x -> local_ x
+[%%expect{|
+val foo' : int -> local_ int = <fun>
+|}]
+
+
+
+let bar (f : local_ int -> int) = f 42
+[%%expect{|
+val bar : (local_ int -> int) -> int = <fun>
+|}]
+
+(* Implicit mode crossing is not good enough *)
+let _ = bar foo
+[%%expect{|
+Line 1, characters 12-15:
+1 | let _ = bar foo
+                ^^^
+Error: This expression has type int -> int
+       but an expression was expected of type local_ int -> int
+|}]
+
+let _ = bar (foo :> local_ int -> int)
+[%%expect{|
+- : int = 42
+|}]
+
+let _ = bar (foo : int -> int :> local_ int -> int)
+[%%expect{|
+- : int = 42
+|}]
+
+(* Only the RHS type of :> is looked at for mode crossing *)
+let _ = bar (foo : int -> int :> local_ _ -> _)
+[%%expect{|
+Line 1, characters 12-47:
+1 | let _ = bar (foo : int -> int :> local_ _ -> _)
+                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: Type int -> int is not a subtype of local_ 'a -> 'b
+|}]
+
+
+(* An example: the RHS allows mode crossing but the LHS doesn't *)
+let foo = function
+  | `A -> ()
+  | `B (s : string) -> ()
+[%%expect{|
+val foo : [< `A | `B of string ] -> unit = <fun>
+|}]
+
+let foo_ = (foo : [`A | `B of string] -> unit :> local_ [`A] -> unit)
+[%%expect{|
+val foo_ : local_ [ `A ] -> unit = <fun>
+|}]
+
+let foo_ = (foo : [`A | `B of string] -> unit :> local_ [`B of string] -> unit)
+[%%expect{|
+Line 1, characters 11-79:
+1 | let foo_ = (foo : [`A | `B of string] -> unit :> local_ [`B of string] -> unit)
+               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: Type [ `A | `B of string ] -> unit is not a subtype of
+         local_ [ `B of string ] -> unit
+|}]
+
+(* You can't erase the info that a function might allocate in parent region *)
+let _ = bar (foo' :> local_ int -> int)
+[%%expect{|
+Line 1, characters 12-39:
+1 | let _ = bar (foo' :> local_ int -> int)
+                ^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: Type int -> local_ int is not a subtype of local_ int -> int
+|}]

typing/ctype.ml

@@ -2114,6 +2114,9 @@ let unification_layout_check env ty layout =
   | Delay_checks r -> r := (ty,layout) :: !r
   | Skip_checks -> ()
 
+let is_principal ty =
+  not !Clflags.principal || get_level ty = generic_level
+
 let is_always_global env ty =
   let perform_check () =
     Result.is_ok (check_type_layout env ty
@@ -2129,6 +2132,9 @@ let is_always_global env ty =
   else
     perform_check ()
 
+let mode_cross env (ty : type_expr) =
+  is_principal ty && is_always_global env ty
+
 (* Recursively expand the head of a type.
    Also expand #-types.
 
@@ -5341,7 +5347,17 @@ let rec build_subtype env (visited : transient_expr list)
       let (t1', c1) = build_subtype env visited loops (not posi) level t1 in
       let (t2', c2) = build_subtype env visited loops posi level t2 in
       let (a', c3) =
-        if level > 2 then build_submode (not posi) a else a, Unchanged
+        if level > 2 then begin
+          (* If posi, then t1' >= t1, and we pick t1; otherwise we pick t1'. In
+            either case we pick the smaller type which is the "real" type of
+            runtime values, and easier to cross modes (and thus making the
+            mode-crossing more complete). *)
+          let t1 = if posi then t1 else t1' in
+          if is_always_global env t1 then
+            Mode.Alloc.newvar (), Changed
+          else
+            build_submode (not posi) a
+          end else a, Unchanged
       in
       let (r', c4) =
         if level > 2 then build_submode posi r else r, Unchanged
@@ -5557,7 +5573,10 @@ let rec subtype_rec env trace t1 t2 cstrs =
             t2 t1
             cstrs
         in
-        subtype_alloc_mode env trace a2 a1;
+        if not (is_always_global env t2) then
+          subtype_alloc_mode env trace a2 a1;
+        (* RHS mode of arrow types indicates allocation in the parent region
+           and is not subject to mode crossing *)
         subtype_alloc_mode env trace r1 r2;
         subtype_rec
           env

typing/ctype.mli

@@ -520,11 +520,15 @@ val check_type_layout :
 val constrain_type_layout :
   Env.t -> type_expr -> layout -> (unit, Layout.Violation.t) result
 
+val is_principal : type_expr -> bool
+
 (* True if a type is always global (i.e., it mode crosses for local).  This is
    true for all immediate and immediate64 types.  To make it sound for
    immediate64, we've disabled stack allocation on 32-bit builds. *)
 val is_always_global : Env.t -> type_expr -> bool
 
+val mode_cross : Env.t -> type_expr -> bool
+
 (* For use with ocamldebug *)
 type global_state
 val global_state : global_state

typing/typecore.ml

@@ -709,9 +709,6 @@ let extract_label_names env ty =
   | Record_type (_, _,fields, _) -> List.map (fun l -> l.Types.ld_id) fields
   | Not_a_record_type | Maybe_a_record_type -> assert false
 
-let is_principal ty =
-  not !Clflags.principal || get_level ty = generic_level
-
 let has_local_attr loc attrs =
   match Builtin_attributes.has_local attrs with
   | Ok l -> l
@@ -733,9 +730,6 @@ let has_poly_constraint spat =
     end
   | _ -> false
 
-let mode_cross env (ty : type_expr) =
-  is_principal ty && is_always_global env ty
-
 let mode_cross_to_min env ty mode =
   if mode_cross env ty then
     Value.min_mode