Merge branch 'main' into fix-failing-array-tests

Author: Mikah-Kainen

src/Array/Mutable.hs

@@ -117,8 +117,8 @@ set (Array lo'@(GHC.I# lo) hi !arr) i'@(GHC.I# i) !a =
 
 {-# INLINE copy #-}
 copy :: HasPrim a => Array a -> Int -> Array a -> Int -> Int -> Array a
-copy s@(Array lo1'@(GHC.I# lo1) _hi1 src) (GHC.I# src_offset)
-     d@(Array      (GHC.I# lo2) _hi2 dst) (GHC.I# dst_offset)
+copy s@(Array (GHC.I# lo1) _hi1 src) (GHC.I# src_offset)
+     d@(Array (GHC.I# lo2) _hi2 dst) (GHC.I# dst_offset)
      (GHC.I# n) =
 #ifdef PRIM_MUTABLE_ARRAYS
   case copy# (get# src lo1) src (lo1 GHC.+# src_offset) dst (lo2 GHC.+# dst_offset) n of

src/ArrayOperations.hs

@@ -59,7 +59,9 @@ swap xs i j = let !xi   = get xs i
               in xs''
 #endif
 
-
+-- For correctness, the strictness annotations on !xi and !xj are crucial.
+--   Due to laziness, there's otherwise nothing preventing `setLin i xj xs2`
+--   from executing before `get2 i xs`. Same with `swap` above.
 {-@ swap2 :: { i:Int | 0 <= i }
           -> { j:Int | 0 <= j } -> { xs:(Array a) | i < size xs && j < size xs }
           -> { ys:(Array a) | size xs == size ys && token xs == token ys &&