Support mode crossing at identifiers

ocaml/testsuite/tests/typing-local/crossing.ml

@@ -345,7 +345,7 @@ val f : local_ M.t -> M.t = <fun>
 val f : local_ t2 -> t2 = <fun>
 |}]
 
-(* This test needs the snapshotting in is_always_global to prevent a type error
+(* This test needs the snapshotting in [is_immediate] 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 }
@@ -436,4 +436,15 @@ 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
+|}]
+
+(* 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. *)
+let foo () =
+  let x, y = local_ (42, 24) in
+  let _ = ref x, ref y in
+  ()
+[%%expect{|
+val foo : unit -> unit = <fun>
 |}]

ocaml/testsuite/tests/typing-unique/unique.ml

@@ -147,7 +147,7 @@ Error: Found a shared value where a unique value was expected
 |}]
 
 let f =
-  let unique_ a = 3 in
+  let unique_ a = "hello" in
   let g (unique_ a) = a in
   for i = 0 to 5 do
     let _ = g a in ()

ocaml/typing/ctype.ml

@@ -2117,7 +2117,7 @@ let unification_layout_check env ty layout =
 let is_principal ty =
   not !Clflags.principal || get_level ty = generic_level
 
-let is_always_global env ty =
+let is_immediate64 env ty =
   let perform_check () =
     Result.is_ok (check_type_layout env ty
                     (Layout.immediate64 ~why:Local_mode_cross_check))
@@ -2132,8 +2132,13 @@ let is_always_global env ty =
   else
     perform_check ()
 
+(* We will require Int63 to be [global many unique] on 32-bit platforms, so
+   this is fine *)
+let is_immediate = is_immediate64
+
 let mode_cross env (ty : type_expr) =
-  is_principal ty && is_always_global env ty
+  (* immediates can cross all mode axes: locality, uniqueness and linearity *)
+  is_principal ty && is_immediate env ty
 
 (* Recursively expand the head of a type.
    Also expand #-types.
@@ -5353,7 +5358,7 @@ let rec build_subtype env (visited : transient_expr list)
             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
+          if is_immediate env t1 then
             Mode.Alloc.newvar (), Changed
           else
             build_submode (not posi) a
@@ -5573,7 +5578,7 @@ let rec subtype_rec env trace t1 t2 cstrs =
             t2 t1
             cstrs
         in
-        if not (is_always_global env t2) then
+        if not (is_immediate 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 *)

ocaml/typing/ctype.mli

@@ -520,13 +520,14 @@ val check_type_layout :
 val constrain_type_layout :
   Env.t -> type_expr -> layout -> (unit, Layout.Violation.t) result
 
+(* False if running in principal mode and the type is not principal.
+   True otherwise. *)
 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
+(* True if a type is immediate. *)
+val is_immediate : Env.t -> type_expr -> bool
 
+(* True if a type can cross to the minimum on all mode axes. *)
 val mode_cross : Env.t -> type_expr -> bool
 
 (* For use with ocamldebug *)

ocaml/typing/typecore.ml

@@ -1275,7 +1275,7 @@ and build_as_type_aux ~refine ~mode (env : Env.t ref) p =
       end
   | Tpat_constant _ ->
       let mode =
-        if Ctype.is_always_global !env p.pat_type
+        if Ctype.is_immediate !env p.pat_type
         then Value.newvar ()
         else mode
       in
@@ -6026,6 +6026,10 @@ and type_expect_
 
 and type_ident env ?(recarg=Rejected) lid =
   let (path, desc, mode, reason) = Env.lookup_value ~loc:lid.loc lid.txt env in
+  (* Mode crossing here is needed only because of the strange behaviour of
+  [type_let] - it checks the LHS before RHS. Had it checks the RHS before LHS,
+  identifiers would be mode crossed when being added to the environment. *)
+  let mode = mode_cross_to_min env desc.val_type mode in
   let is_recarg =
     match get_desc desc.val_type with
     | Tconstr(p, _, _) -> Path.is_constructor_typath p

ocaml/typing/typedecl.ml

@@ -441,8 +441,8 @@ let make_constructor
       let args, targs =
         transl_constructor_arguments env univars closed sargs
       in
-      let tret_type = 
-        transl_simple_type env ?univars ~closed Mode.Alloc.Const.legacy sret_type 
+      let tret_type =
+        transl_simple_type env ?univars ~closed Mode.Alloc.Const.legacy sret_type
       in
       let ret_type = tret_type.ctyp_type in
       (* TODO add back type_path as a parameter ? *)
@@ -935,7 +935,7 @@ let check_constraints env sdecl (_, decl) =
    [type_layout] with what we computed.
 
    CR layouts: if easy, factor out the shared backtracking logic from here
-   and is_always_global.
+   and is_immediate.
 *)
 let check_coherence env loc dpath decl =
   match decl with