Allow parameter modes to be relaxed in type_argument

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

@@ -777,6 +777,45 @@ Line 2, characters 20-45:
 Error: This function is local-returning, but was expected otherwise
 |}]
 
+(*
+ * Modification of parameter modes in argument position
+ *)
+
+let use_local (local_ f : _ -> _ -> _) x y =
+  f x y
+let use_global (f : _ -> _ -> _) x y = f x y
+
+let foo x y = x +. y
+let bar (local_ x) (local_ y) = let _ = x +. y in ()
+
+let result = use_local foo 1. 2.
+[%%expect{|
+val use_local : local_ ('a -> 'b -> 'c) -> 'a -> 'b -> 'c = <fun>
+val use_global : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c = <fun>
+val foo : float -> float -> float = <fun>
+val bar : local_ float -> local_ float -> unit = <fun>
+val result : float = 3.
+|}]
+
+let result = use_local bar 1. 2.
+[%%expect{|
+val result : unit = ()
+|}]
+
+let result = use_global foo 1. 2.
+[%%expect{|
+val result : float = 3.
+|}]
+
+let result = use_global bar 1. 2.
+[%%expect{|
+Line 1, characters 24-27:
+1 | let result = use_global bar 1. 2.
+                            ^^^
+Error: This expression has type local_ float -> local_ float -> unit
+       but an expression was expected of type local_ 'a -> ('b -> 'c)
+|}]
+
 
 (*
  * Closures and context locks
@@ -2124,24 +2163,31 @@ let foo f = ignore (f :> string -> float); ()
 val foo : (string -> float) -> unit = <fun>
 |}]
 
-let local_to_global (local_ _s : string) = 42.0
+let global_to_global_to_global (f : float -> string) = f 42.0
 
-let foo f = ignore (f :> string -> float); [f; local_to_global]
+let foo f =
+  ignore (f :> (local_ float -> string) -> string);
+  [f; global_to_global_to_global]
 [%%expect{|
-val local_to_global : local_ string -> float = <fun>
-val foo : (local_ string -> float) -> (local_ string -> float) list = <fun>
+val global_to_global_to_global : (float -> string) -> string = <fun>
+val foo : ((float -> string) -> string) -> ((float -> string) -> string) list =
+  <fun>
 |}]
 
-let global_to_local (_s : string) = local_ 42.0
+let local_to_global_to_global (f : local_ float -> string) = f 42.0
 
-let foo f = ignore (f :> string -> float); [f; global_to_local]
+let foo f =
+  ignore (f :> (float -> string) -> string);
+  [f; local_to_global_to_global]
 [%%expect{|
-val global_to_local : string -> local_ float = <fun>
-Line 3, characters 47-62:
-3 | let foo f = ignore (f :> string -> float); [f; global_to_local]
-                                                   ^^^^^^^^^^^^^^^
-Error: This expression has type string -> local_ float
-       but an expression was expected of type string -> float
+val local_to_global_to_global : (local_ float -> string) -> string = <fun>
+Line 5, characters 6-31:
+5 |   [f; local_to_global_to_global]
+          ^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This expression has type (local_ float -> string) -> string
+       but an expression was expected of type (float -> string) -> string
+       Type local_ float -> string is not compatible with type
+         float -> string
 |}]
 
 (* Submoding during module inclusion *)

ocaml/testsuite/tests/typing-poly/poly_params.ml

@@ -279,7 +279,7 @@ Line 1, characters 24-25:
 1 | let foo (f : p1) : p2 = f
                             ^
 Error: This expression has type p1 = ('a. 'a -> 'a) -> int
-       but an expression was expected of type p2 = ('a 'b. 'a -> 'b) -> int
+       but an expression was expected of type ('a 'b. 'a -> 'b) -> int
        Type 'a is not compatible with type 'b
 |}];;
 
@@ -328,13 +328,13 @@ Line 4, characters 24-25:
 4 | let foo (x : p1) : p2 = x
                             ^
 Error: This expression has type p1 = (bool -> bool) -> int
-       but an expression was expected of type p2 = ('a. 'a -> 'a) -> int
+       but an expression was expected of type ('a. 'a -> 'a) -> int
        Type bool is not compatible with type 'a
 |}];;
 
 let foo x = (x : p1 :> p2)
 [%%expect {|
-val foo : p1 -> p2 = <fun>
+val foo : ((bool -> bool) -> int) -> p2 = <fun>
 |}];;
 
 module Foo (X : sig val f : p1 end) : sig val f : p2 end = X

ocaml/typing/typecore.ml

@@ -6598,7 +6598,7 @@ and type_argument ?explanation ?recarg env (mode : expected_mode) sarg
     not tvar && List.for_all ((=) Nolabel) ls
   in
   let inferred = is_inferred sarg in
-  let rec loosen_ret_modes ty' ty =
+  let rec loosen_arrow_modes ty' ty =
     let expty = expand_head env ty in
     let expty' = expand_head env ty' in
     let lv = get_level expty in
@@ -6607,9 +6607,10 @@ and type_argument ?explanation ?recarg env (mode : expected_mode) sarg
     | Tarrow((l, marg, mret), ty_arg', ty_res', _),
       Tarrow(_, ty_arg,  ty_res,  _)
       when lv' = generic_level || not !Clflags.principal ->
-      let ty_res', ty_res, changed = loosen_ret_modes ty_res' ty_res in
+      let ty_res', ty_res, changed = loosen_arrow_modes ty_res' ty_res in
       let mret, changed' = Alloc.newvar_below_comonadic mret in
-      if changed || changed' then
+      let marg, changed'' = Alloc_mode.newvar_above marg in
+      if changed || changed' || changed'' then
         newty2 ~level:lv' (Tarrow((l, marg, mret), ty_arg', ty_res', commu_ok)),
         newty2 ~level:lv  (Tarrow((l, marg, mret), ty_arg,  ty_res,  commu_ok)),
         true
@@ -6626,7 +6627,7 @@ and type_argument ?explanation ?recarg env (mode : expected_mode) sarg
         then Some (Btype.snapshot ())
         else None
       in
-      let t', t, changed = loosen_ret_modes ty_expected' ty_expected in
+      let t', t, changed = loosen_arrow_modes ty_expected' ty_expected in
       if not changed then Option.iter Btype.backtrack snap;
       t', t
     else