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-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,17 @@ 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
+  (* Arrow types cross uniqueness axis. Therefore, when user writes an
+  A -> B -> C (to be used as constraint on something), we should make
+  (B -> C) shared. A proper way to do this is via modal kinds. *)
+  {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

@@ -211,6 +211,7 @@ val prim_mode :
 val instance_prim:
         Primitive.description -> type_expr ->
         type_expr * Mode.Locality.lr option * Jkind.Sort.t option
+val curry_mode : Alloc.Const.t -> Alloc.Const.t -> Alloc.Const.t
 
 val apply:
         ?use_current_level:bool ->

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