fix: Array.foldlMUnsafe bug

This PR a bug in the optimized and unsafe implementation of
`Array.foldlM`.

Issue was reported here:
https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Array.2Efoldl.20bug.20.28can.20prove.20False.29/near/565077432

src/Init/Data/Array/Basic.lean

@@ -590,7 +590,7 @@ unsafe def foldlMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Mon
     if stop ≤ as.size then
       fold (USize.ofNat start) (USize.ofNat stop) init
     else
-      pure init
+      fold (USize.ofNat start) (USize.ofNat as.size) init
   else
     pure init
 

tests/lean/run/foldlUnsafe_bug.lean

@@ -0,0 +1,23 @@
+/--
+error: Tactic `native_decide` evaluated that the proposition
+  foldl (fun x1 x2 => x1 + x2) 0 #[1, 2, 3] 0 5 = 0
+is false
+-/
+#guard_msgs in
+theorem Array.foldl_broken : False := by
+  let x := #[1,2,3].foldl (. + .) 0 (stop := 5)
+  have : x = 6 := by rfl
+  have : x = 0 := by native_decide -- must fail
+  contradiction
+
+/--
+error: Tactic `native_decide` evaluated that the proposition
+  Array.foldl (fun x1 x2 => x1 + x2) 0 #[1, 2, 3] 0 5 = 0
+is false
+-/
+#guard_msgs in
+example : #[1,2,3].foldl (. + .) 0 (stop := 5) = 0 := by
+  native_decide -- must fail
+
+example : #[1,2,3].foldl (. + .) 0 (stop := 5) = 6 := by
+  native_decide