Fix soundness bug of uniqueness analysis on immutable array patterns (o…

…caml-flambda#3247)

* Fix soundness bug of uniqueness analysis on immutable array patterns

* Review feedback: determine mutable modality in array_index

testsuite/tests/typing-unique/unique.ml

@@ -640,3 +640,27 @@ Line 2, characters 11-19:
                ^^^^^^^^
 
 |}]
+
+let array_pats (arr : int option array) =
+  match arr with
+  | [| o |] -> let _ = unique_id arr in aliased_id o
+  | _ -> None
+[%%expect{|
+val array_pats : int option array @ unique -> int option = <fun>
+|}]
+
+let array_pats (arr : int option iarray) =
+  match arr with
+  | [: o :] -> let _ = unique_id arr in unique_id o
+  | _ -> None
+[%%expect{|
+Line 3, characters 50-51:
+3 |   | [: o :] -> let _ = unique_id arr in unique_id o
+                                                      ^
+Error: This value is used here,
+       but it is part of a value that has already been used as unique:
+Line 3, characters 33-36:
+3 |   | [: o :] -> let _ = unique_id arr in unique_id o
+                                     ^^^
+
+|}]

typing/uniqueness_analysis.ml

@@ -459,6 +459,7 @@ module Projection : sig
     | Record_field of string
     | Construct_field of string * int
     | Variant_field of label
+    | Array_index of int
     | Memory_address (* this is rendered as clubsuit in the ICFP'24 paper *)
 
   module Map : Map.S with type key = t
@@ -469,6 +470,7 @@ end = struct
       | Record_field of string
       | Construct_field of string * int
       | Variant_field of label
+      | Array_index of int
       | Memory_address
 
     let compare t1 t2 =
@@ -478,24 +480,31 @@ end = struct
       | Construct_field (l1, i), Construct_field (l2, j) -> (
         match String.compare l1 l2 with 0 -> Int.compare i j | i -> i)
       | Variant_field l1, Variant_field l2 -> String.compare l1 l2
+      | Array_index i, Array_index j -> Int.compare i j
       | Memory_address, Memory_address -> 0
       | ( Tuple_field _,
-          (Record_field _ | Construct_field _ | Variant_field _ | Memory_address)
-        ) ->
+          ( Record_field _ | Construct_field _ | Variant_field _ | Array_index _
+          | Memory_address ) ) ->
         -1
-      | ( (Record_field _ | Construct_field _ | Variant_field _ | Memory_address),
+      | ( ( Record_field _ | Construct_field _ | Variant_field _ | Array_index _
+          | Memory_address ),
           Tuple_field _ ) ->
         1
-      | Record_field _, (Construct_field _ | Variant_field _ | Memory_address)
-        ->
+      | ( Record_field _,
+          (Construct_field _ | Variant_field _ | Array_index _ | Memory_address)
+        ) ->
+        -1
+      | ( (Construct_field _ | Variant_field _ | Array_index _ | Memory_address),
+          Record_field _ ) ->
+        1
+      | Construct_field _, (Variant_field _ | Array_index _ | Memory_address) ->
         -1
-      | (Construct_field _ | Variant_field _ | Memory_address), Record_field _
-        ->
+      | (Variant_field _ | Array_index _ | Memory_address), Construct_field _ ->
         1
-      | Construct_field _, (Variant_field _ | Memory_address) -> -1
-      | (Variant_field _ | Memory_address), Construct_field _ -> 1
-      | Variant_field _, Memory_address -> -1
-      | Memory_address, Variant_field _ -> 1
+      | Variant_field _, (Array_index _ | Memory_address) -> -1
+      | (Array_index _ | Memory_address), Variant_field _ -> 1
+      | Array_index _, Memory_address -> -1
+      | Memory_address, Array_index _ -> 1
   end
 
   include T
@@ -774,6 +783,10 @@ module Paths : sig
   (** [variant_field s t] is [child (Projection.Variant_field s) t]. *)
   val variant_field : string -> t -> t
 
+  (** [array_index mut i t] is [modal_child gf (Projection.Array_index i) t]
+      where [gf] is the appropriate modality for mutability [mut]. *)
+  val array_index : Types.mutability -> int -> t -> t
+
   (** [memory_address t] is [child Projection.Memory_address t]. *)
   val memory_address : t -> t
 
@@ -820,6 +833,10 @@ end = struct
 
   let variant_field s t = child (Projection.Variant_field s) t
 
+  let array_index mut i t =
+    let modality = Typemode.transl_modalities ~maturity:Stable mut [] [] in
+    modal_child modality (Projection.Array_index i) t
+
   let memory_address t = child Projection.Memory_address t
 
   let mark usage t = UF.chooses (List.map (UF.singleton usage) t)
@@ -1106,12 +1123,12 @@ and pattern_match_single pat paths : Ienv.Extension.t * UF.t =
       |> conjuncts_pattern_match
     in
     ext, UF.par uf_read uf_pats
-  | Tpat_array (_, _, pats) ->
+  | Tpat_array (mut, _, pats) ->
     let uf_read = borrow_memory_address () in
     let ext, uf_pats =
-      List.map
-        (fun pat ->
-          let paths = Paths.fresh () in
+      List.mapi
+        (fun idx pat ->
+          let paths = Paths.array_index mut idx paths in
           pattern_match_single pat paths)
         pats
       |> conjuncts_pattern_match