From 14e1d4328f70aa5b6680586a6aae79167f4aa37e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= <wojciech@lean-fro.org>
Date: Fri, 20 Feb 2026 14:38:15 +0000
Subject: [PATCH] fix: prevent `cbv` crash on dependent projections with
 `@[cbv_eval]` rewrites (#12612)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR fixes a crash in the `cbv` tactic's `handleProj` simproc when
processing a dependent projection (e.g. `Sigma.snd`) whose struct is
rewritten via `@[cbv_eval]` to a non-definitionally-equal term that
cannot be further reduced.

- Previously, `handleProj` returned `.rfl (done := false)`, causing the
`.proj` expression to flow into `simpStep` which throws "unexpected
kernel projection term"
- The fix marks the result as `done := true` so that `cbv` gracefully
gets stuck instead of crashing
- Adds regression tests for dependent projections on `Sigma`, custom
structures, and `Subtype`

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

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

diff --git a/src/Lean/Meta/Tactic/Cbv/Main.lean b/src/Lean/Meta/Tactic/Cbv/Main.lean
index fed44282d7..ba3197e76c 100644
--- a/src/Lean/Meta/Tactic/Cbv/Main.lean
+++ b/src/Lean/Meta/Tactic/Cbv/Main.lean
@@ -121,7 +121,7 @@ def handleProj : Simproc := fun e => do
         unless (← isDefEq struct e') do
           -- If we rewrote the projection body using something that holds up to propositional equality, then there is nothing we can do.
           -- TODO: Check if there is a need to report this to a user, or shall we fail silently.
-          return .rfl
+          return .rfl (done := true)
         let hcongr ← mkHCongr congrArgFun
         let newProof := mkApp3 (hcongr.proof) struct e' proof
         -- We have already checked if `struct` and `e'` are defEq, so we can skip the check.
diff --git a/tests/lean/run/cbv_dep_proj.lean b/tests/lean/run/cbv_dep_proj.lean
new file mode 100644
index 0000000000..ddb4448fd1
--- /dev/null
+++ b/tests/lean/run/cbv_dep_proj.lean
@@ -0,0 +1,73 @@
+set_option cbv.warning false
+
+/-! Tests for `cbv` handling of dependent projections.
+
+When a struct is rewritten (e.g. via `@[cbv_eval]`) but the projection is
+dependent and the original struct can't be reduced, `cbv` should gracefully
+get stuck rather than crash.
+-/
+
+-- Sigma: .1 is non-dependent, .2 is dependent
+def myPair : Σ n : Nat, Fin (n + 1) := ⟨5, ⟨3, by omega⟩⟩
+axiom otherPair : Σ n : Nat, Fin (n + 1)
+@[cbv_eval ←] axiom otherPair_eq : myPair = otherPair
+
+example : otherPair.1 = 5 := by cbv
+
+/--
+error: unsolved goals
+⊢ otherPair.2.1 = 3
+-/
+#guard_msgs in
+example : otherPair.2.val = 3 := by cbv
+
+-- Custom structure with a dependent field
+structure DepPkg where
+  n : Nat
+  val : Fin (n + 1)
+
+def concretePkg : DepPkg := ⟨5, ⟨3, by omega⟩⟩
+axiom opaquePkg : DepPkg
+@[cbv_eval ←] axiom opaquePkg_eq : concretePkg = opaquePkg
+
+example : opaquePkg.n = 5 := by cbv
+
+/--
+error: unsolved goals
+⊢ opaquePkg.2.1 = 3
+-/
+#guard_msgs in
+example : opaquePkg.val.val = 3 := by cbv
+
+-- Subtype: .val is non-dependent, so the rewrite goes through
+def concreteSubtype : { n : Nat // n > 0 } := ⟨5, by omega⟩
+axiom opaqueSubtype : { n : Nat // n > 0 }
+@[cbv_eval ←] axiom opaqueSubtype_eq : concreteSubtype = opaqueSubtype
+
+example : opaqueSubtype.val = 5 := by cbv
+
+-- Non-dependent projections: function projected from a structure and applied
+structure FnStruct where
+  fn : Nat → Nat
+
+def myFnStruct : FnStruct := ⟨fun n => n + 1⟩
+example : myFnStruct.fn 5 = 6 := by cbv
+
+-- Nested non-dependent projections
+structure Layer1 where val : Nat
+structure Layer2 where inner : Layer1
+structure Layer3 where inner : Layer2
+
+def nested : Layer3 := ⟨⟨⟨42⟩⟩⟩
+example : nested.inner.inner.val = 42 := by cbv
+
+-- Double projection through a product
+structure FnPairS where
+  fst : Nat → Nat
+  snd : Nat → Nat
+
+def fnPairPair : FnPairS × FnPairS :=
+  (⟨fun n => n + 1, fun n => n + 2⟩, ⟨fun n => n + 3, fun n => n + 4⟩)
+
+example : fnPairPair.1.fst 5 = 6 := by cbv
+example : fnPairPair.2.snd 5 = 9 := by cbv