diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean
index 1acc8cefb72c..524b9f50721a 100644
--- a/src/Init/Data/Vector/Basic.lean
+++ b/src/Init/Data/Vector/Basic.lean
@@ -36,7 +36,7 @@ structure Vector (α : Type u) (n : Nat) where
   toArray : Array α
   /-- Array size. -/
   size_toArray : toArray.size = n
-deriving DecidableEq
+deriving @[expose] DecidableEq
 
 attribute [simp, grind =] Vector.size_toArray
 
diff --git a/tests/elab/vector_decidable_eq_module.lean b/tests/elab/vector_decidable_eq_module.lean
new file mode 100644
index 000000000000..d5f052f4df7e
--- /dev/null
+++ b/tests/elab/vector_decidable_eq_module.lean
@@ -0,0 +1,9 @@
+module
+
+/-!
+Tests kernel reduction of derived `Vector` equality across a module boundary.
+-/
+
+example : (#v[] : Vector Nat 0) = #v[] := by decide
+example : decide ((#v[] : Vector Nat 0) = #v[]) = true := by rfl
+example : (#v[] : Vector Nat 0) = #v[] := by decide +kernel