fix: expose Array equality for kernel reduction

src/Init/Data/Array/Basic.lean

@@ -290,7 +290,7 @@ Examples:
 def isEmpty (xs : Array α) : Bool :=
   xs.size = 0
 
-@[specialize]
+@[specialize, expose]
 def isEqvAux (xs ys : Array α) (hsz : xs.size = ys.size) (p : α → α → Bool) :
     ∀ (i : Nat) (_ : i ≤ xs.size), Bool
   | 0, _ => true
@@ -307,7 +307,7 @@ Examples:
 * `#[1, 2, 3].isEqv #[2, 2, 4] (· < ·) = false`
 * `#[1, 2, 3].isEqv #[2, 3] (· < ·) = false`
 -/
-@[inline] def isEqv (xs ys : Array α) (p : α → α → Bool) : Bool :=
+@[inline, expose] def isEqv (xs ys : Array α) (p : α → α → Bool) : Bool :=
   if h : xs.size = ys.size then
     isEqvAux xs ys h p xs.size (Nat.le_refl xs.size)
   else

src/Init/Data/Array/DecidableEq.lean

@@ -96,6 +96,8 @@ theorem isEqv_self_beq [BEq α] [ReflBEq α] (xs : Array α) : Array.isEqv xs xs
 theorem isEqv_self [DecidableEq α] (xs : Array α) : Array.isEqv xs xs (· = ·) = true := by
   simp [isEqv, isEqvAux_self]
 
+-- Exposed so that `Array` equality reduces across module boundaries.
+@[expose]
 def instDecidableEqImpl [DecidableEq α] : DecidableEq (Array α) := fun xs ys =>
   match h:isEqv xs ys (fun a b => a = b) with
   | true  => isTrue (eq_of_isEqv xs ys h)

tests/elab/array_decidable_eq_module.lean

@@ -0,0 +1,15 @@
+module
+
+/-!
+Tests kernel reduction of `Array` equality across a module boundary.
+-/
+
+example : (#[0, 1] : Array Nat) ≠ #[1] := by decide
+example : (#[2, 3] : Array Nat) = #[2, 3] := by decide
+example : ¬ ((#[0, 1] : Array Nat) = #[1, 0]) := by decide
+example : decide ((#[0, 1] : Array Nat) = #[0, 1]) = true := by rfl
+example : (#[1, 2, 3] : Array Nat) ≠ #[1, 2, 4] := by decide +kernel
+
+-- Empty cases already reduced before the nonempty implementation was exposed.
+example : (#[] : Array Nat) = #[] := by decide
+example : (#[] : Array Nat) ≠ #[1] := by decide