fix: include zetaUnused in Meta.Config cache key (#13772)

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

@@ -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

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