Refactor arrow modes printing

ocaml/testsuite/tests/typing-implicit-source-positions/invalid_usages.ml

@@ -44,7 +44,7 @@ Line 1, characters 14-15:
                   ^
 Error: This expression has type call_pos:[%call_pos] -> unit -> unit
        but an expression was expected of type
-         call_pos:Lexing.position -> (unit -> 'a)
+         call_pos:Lexing.position -> unit -> 'a
 |}]
 
 let h ?(call_pos:[%call_pos]) () = ()

ocaml/testsuite/tests/typing-modal-kinds/basics.ml

@@ -573,3 +573,13 @@ Line 2, characters 71-72:
                                                                            ^
 
 |}]
+
+(* CR layouts: this should succeed. *)
+let foo : (string -> string) -> (string -> string) @ unique
+  = fun f -> f
+[%%expect{|
+Line 2, characters 13-14:
+2 |   = fun f -> f
+                 ^
+Error: Found a shared value where a unique value was expected
+|}]

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

@@ -161,18 +161,18 @@ Error: Found a shared value where a unique value was expected
 (* arrow types *)
 type r = local_ string @ unique once -> unique_ string @ local once
 [%%expect{|
-type r = local_ unique_ once_ string -> local_ unique_ once_ string
+type r = local_ once_ unique_ string -> local_ once_ unique_ string
 |}]
 
 type r = local_ string * y:string @ unique once -> local_ string * w:string @ once
 [%%expect{|
-type r = local_ unique_ once_ string * string -> local_ once_ string * string
+type r = local_ once_ unique_ string * string -> local_ once_ string * string
 |}]
 
 type r = x:local_ string * y:string @ unique once -> local_ string * w:string @ once
 [%%expect{|
 type r =
-    x:local_ unique_ once_ string * string -> local_ once_ string * string
+    x:local_ once_ unique_ string * string -> local_ once_ string * string
 |}]
 
 
@@ -250,12 +250,12 @@ type r = { global_ x : string; }
 
 let foo ?(local_ x @ unique once = 42) () = ()
 [%%expect{|
-val foo : ?x:local_ unique_ once_ int -> unit -> unit = <fun>
+val foo : ?x:local_ once_ unique_ int -> unit -> unit = <fun>
 |}]
 
 let foo ?(local_ x : _ @@ unique once = 42) () = ()
 [%%expect{|
-val foo : ?x:local_ unique_ once_ int -> unit -> unit = <fun>
+val foo : ?x:local_ once_ unique_ int -> unit -> unit = <fun>
 |}]
 
 let foo ?(local_ x : 'a. 'a -> 'a @@ unique once) = ()
@@ -268,12 +268,12 @@ Error: Optional parameters cannot be polymorphic
 
 let foo ?x:(local_ (x,y) @ unique once = (42, 42)) () = ()
 [%%expect{|
-val foo : ?x:local_ unique_ once_ int * int -> unit -> unit = <fun>
+val foo : ?x:local_ once_ unique_ int * int -> unit -> unit = <fun>
 |}]
 
 let foo ?x:(local_ (x,y) : _ @@ unique once = (42, 42)) () = ()
 [%%expect{|
-val foo : ?x:local_ unique_ once_ int * int -> unit -> unit = <fun>
+val foo : ?x:local_ once_ unique_ int * int -> unit -> unit = <fun>
 |}]
 
 let foo ?x:(local_ (x,y) : 'a.'a->'a @@ unique once) () = ()

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

@@ -37,9 +37,9 @@ Lines 3-4, characters 0-68:
 4 | = 'a -> unique_ 'b -> unique_ once_ ('c -> unique_ once_ ('d -> 'e))
 Error: The type constraints are not consistent.
        Type 'a -> unique_ 'b -> 'c -> 'd -> 'e is not compatible with type
-         'a -> unique_ 'b -> unique_ once_ ('c -> unique_ once_ ('d -> 'e))
+         'a -> unique_ 'b -> once_ unique_ ('c -> once_ unique_ ('d -> 'e))
        Type unique_ 'b -> 'c -> 'd -> 'e is not compatible with type
-         unique_ 'b -> unique_ once_ ('c -> unique_ once_ ('d -> 'e))
+         unique_ 'b -> once_ unique_ ('c -> once_ unique_ ('d -> 'e))
 |}]
 
 type distinct_sarg = unit constraint unique_ int -> int = int -> int

ocaml/typing/ctype.ml

@@ -1588,6 +1588,27 @@ let with_locality locality m =
   Alloc.submode_exn (Alloc.meet_with (Comonadic Areality) Locality.Const.min m) m';
   m'
 
+let curry_mode alloc arg : Alloc.Const.t =
+  let acc =
+    Alloc.Const.join
+      (Alloc.Const.close_over arg)
+      (Alloc.Const.partial_apply alloc)
+  in
+  (* For A -> B -> C, we always interpret (B -> C) to be of shared. This is the
+    legacy mode which helps with legacy compatibility. Arrow types cross
+    uniqueness so we are not losing too much expressvity here. One
+    counter-example is:
+
+    let g : (A -> B -> C) = ...
+    let f (g : A -> unique_ (B -> C)) = ...
+
+    And [f g] would not work, as mode crossing doesn't work deeply into arrows.
+    Our answer to this issue is that, the author of f shouldn't ask B -> C to be
+    unique_. Instead, they should leave it as default which is shared, and mode
+    crossing it to unique at the location where B -> C is a real value (instead
+    of the return of a function). *)
+  {acc with uniqueness=Uniqueness.Const.Shared}
+
 let rec instance_prim_locals locals mvar macc finalret ty =
   match locals, get_desc ty with
   | l :: locals, Tarrow ((lbl,marg,mret),arg,ret,commu) ->

ocaml/typing/ctype.mli

@@ -212,6 +212,11 @@ val instance_prim:
         Primitive.description -> type_expr ->
         type_expr * Mode.Locality.lr option * Jkind.Sort.t option
 
+(** Given (a @ m1 -> b -> c) @ m0, where [m0] and [m1] are modes expressed by
+    user-syntax, [curry_mode m0 m1] gives the mode we implicitly interpret b->c
+    to have. *)
+val curry_mode : Alloc.Const.t -> Alloc.Const.t -> Alloc.Const.t
+
 val apply:
         ?use_current_level:bool ->
         Env.t -> type_expr list -> type_expr -> type_expr list -> type_expr

ocaml/typing/mode.ml

@@ -2108,6 +2108,13 @@ module Alloc = struct
         { locality; uniqueness; linearity }
     end
 
+    let diff m0 m1 =
+      let diff le a0 a1 = if le a0 a1 && le a1 a0 then None else Some a0 in
+      let locality = diff Locality.Const.le m0.locality m1.locality in
+      let linearity = diff Linearity.Const.le m0.linearity m1.linearity in
+      let uniqueness = diff Uniqueness.Const.le m0.uniqueness m1.uniqueness in
+      { locality; linearity; uniqueness }
+
     (** See [Alloc.close_over] for explanation. *)
     let close_over m =
       let { monadic; comonadic } = split m in

ocaml/typing/mode_intf.mli

@@ -358,6 +358,10 @@ module type S = sig
         val value : t -> default:some -> some
       end
 
+      (** [diff a b] returns [None] for axes where [a] and [b] match, and [Some
+      a0] for axes where [a] is [a0] and [b] isn't. *)
+      val diff : t -> t -> Option.t
+
       (** Similar to [Alloc.close_over] but for constants *)
       val close_over : t -> t