From 8f508e3c9199a39d17914989856fea6ea575cce7 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Mon, 18 May 2026 22:47:19 +1000
Subject: [PATCH] fix: include `zetaUnused` in `Meta.Config` cache key (#13772)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR closes https://github.com/leanprover/lean4/issues/13770 by
including `Config.zetaUnused` in `Config.toKey`. Without this, two
configs that differ only in `zetaUnused` share a `WHNF`/`isDefEq` cache
key, so reductions performed under one setting can be returned for the
other. The new bit sits at position 22, immediately above `zetaHave`.

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 src/Lean/Meta/Basic.lean |  3 ++-
 tests/elab/13770.lean    | 16 ++++++++++++++++
 2 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100644 tests/elab/13770.lean

diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index d49738bac8..dc4f4e5d37 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -213,7 +213,8 @@ private def Config.toKey (c : Config) : UInt64 :=
   (c.univApprox.toUInt64 <<< 16) |||
   (c.etaStruct.toUInt64 <<< 17) |||
   (c.proj.toUInt64 <<< 19) |||
-  (c.zetaHave.toUInt64 <<< 21)
+  (c.zetaHave.toUInt64 <<< 21) |||
+  (c.zetaUnused.toUInt64 <<< 22)
 
 /-- Configuration with key produced by `Config.toKey`. -/
 structure ConfigWithKey where
diff --git a/tests/elab/13770.lean b/tests/elab/13770.lean
new file mode 100644
index 0000000000..3bbf3ee176
--- /dev/null
+++ b/tests/elab/13770.lean
@@ -0,0 +1,16 @@
+module
+
+import Lean
+
+/-!
+Regression test for https://github.com/leanprover/lean4/issues/13770.
+
+`Meta.Config.zetaUnused` controls `whnfCore`/`isDefEqQuick` reduction of unused `let`/`have`
+bindings, so two configs differing only in `zetaUnused` must produce distinct cache keys.
+-/
+
+open Lean Meta
+
+#guard
+  ({ zetaUnused := false } : Meta.Config).toConfigWithKey.key !=
+  ({ zetaUnused := true  } : Meta.Config).toConfigWithKey.key