From 81cf4b00749663f4dfbc4863f3d1b1c418a1e88c Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 1 Sep 2026 13:41:31 +0000
Subject: [PATCH] fix: expose Array equality for kernel reduction

Expose the implementation and its isEqv reduction closure so decide and rfl over nonempty Array equality reduce across module boundaries.
---
 src/Init/Data/Array/Basic.lean            |  4 ++--
 src/Init/Data/Array/DecidableEq.lean      |  2 ++
 tests/elab/array_decidable_eq_module.lean | 15 +++++++++++++++
 3 files changed, 19 insertions(+), 2 deletions(-)
 create mode 100644 tests/elab/array_decidable_eq_module.lean

diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 7d58dee5983a..8cbb4bfd2a94 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/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
diff --git a/src/Init/Data/Array/DecidableEq.lean b/src/Init/Data/Array/DecidableEq.lean
index a4d25cabac4e..539966fd4303 100644
--- a/src/Init/Data/Array/DecidableEq.lean
+++ b/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)
diff --git a/tests/elab/array_decidable_eq_module.lean b/tests/elab/array_decidable_eq_module.lean
new file mode 100644
index 000000000000..17692d11c3a2
--- /dev/null
+++ b/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