From 73751bbb276616fca774b7d19d5cfeefc664f1ae Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 20 Feb 2026 08:37:11 -0800
Subject: [PATCH] fix: interaction between `simp` and
 `backward.whnf.reducibleClassField` (#12622)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR fixes a bug where `simp` made no progress on class projection
reductions when `backward.whnf.reducibleClassField` is `true`.

- In `reduceProjFn?`, for class projections applied to constructor
instances (`Class.projFn (Class.mk ...)`), the code called
`reduceProjCont? (← unfoldDefinitionAny? e)`. The helper
`reduceProjCont?` expects the unfolded result to have a `.proj` head so
it can apply `reduceProj?`. However, when `reducibleClassField` is
enabled, `unfoldDefault` in WHNF.lean already reduces the `.proj` node
during unfolding, so `reduceProjCont?` discards the fully-reduced
result.
- The fix uses `unfoldDefinitionAny?` directly, bypassing
`reduceProjCont?`. The dsimp traversal revisits the result (via
`.visit`) and handles any remaining `.proj` nodes naturally.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
---
 src/Lean/Meta/Tactic/Simp/Main.lean          | 12 +++++++++++-
 tests/lean/run/simp_reducibleClassField.lean |  9 +++++++++
 2 files changed, 20 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/simp_reducibleClassField.lean

diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index a91d398537..11b32b9b36 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -109,7 +109,17 @@ private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
           let major := e.getArg! projInfo.numParams
           unless (← isConstructorApp major) do
             return none
-          reduceProjCont? (← unfoldDefinitionAny? e)
+          if backward.whnf.reducibleClassField.get (← getOptions) then
+            /-
+            When `backward.whnf.reducibleClassField` is `true`, `unfoldDefault` (in WHNF.lean)
+            already reduces the `.proj` node during `unfoldDefinitionAny?`, so `reduceProjCont?`
+            would discard the fully-reduced result because it expects a `.proj` head.
+            We return the unfolded result directly; the dsimp traversal will revisit it
+            (via `.visit`) and handle any remaining `.proj` nodes naturally.
+            -/
+            unfoldDefinitionAny? e
+          else
+            reduceProjCont? (← unfoldDefinitionAny? e)
       else
         -- `structure` projections
         reduceProjCont? (← unfoldDefinition? e)
diff --git a/tests/lean/run/simp_reducibleClassField.lean b/tests/lean/run/simp_reducibleClassField.lean
new file mode 100644
index 0000000000..047e698f22
--- /dev/null
+++ b/tests/lean/run/simp_reducibleClassField.lean
@@ -0,0 +1,9 @@
+set_option backward.whnf.reducibleClassField true in
+example [Ord α] {a b : α} :
+    (letI : Ord α := ⟨fun a b => compare b a⟩; compare a b) = compare b a := by
+  simp only
+
+set_option backward.whnf.reducibleClassField true in
+example [Ord α] {a b : α} :
+    (letI : Ord α := ⟨fun a b => compare b a⟩; compare a b) = compare b a := by
+  simp