From c2ec2ecab1cb66fe97d7107a3cbd9d52eaa99290 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 22 Feb 2026 13:20:33 -0800 Subject: [PATCH] fix: handle class projections in `isNonTrivialRegular` for `backward.whnf.reducibleClassField` (#12639) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR fixes the interaction between `backward.whnf.reducibleClassField` and `isDefEqDelta`'s argument-comparison heuristic. When `backward.whnf.reducibleClassField` is enabled, `unfoldDefault` reduces class field projections past the `.proj` form at `.instances` transparency. This causes `isDefEqDelta` to lose the instance structure that `isDefEqProj` needs to bump transparency for instance-implicit parameters. The fix adds an `.abbrev` branch in `isNonTrivialRegular` that classifies class field projections as nontrivial when the option is enabled, so `tryHeuristic` applies the argument-comparison heuristic (with the correct transparency bump) instead of unfolding. Key insight: all projection functions receive `.abbrev` kernel hints (not `.regular`), regardless of their reducibility status. Structure projections default to `.reducible` status, while class projections default to `.semireducible` status. The old code only handled the `.regular` case and treated everything else (including `.abbrev`) as trivial. Also fixes two minor comment issues in `tryHeuristic`: "non-trivial regular definition" → "non-trivial definition" (since `.abbrev` definitions can now be nontrivial too), and "when `f` is not simple" → "when `f` is simple" (logic inversion in the original comment). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.6 --- src/Lean/Meta/ExprDefEq.lean | 39 ++++++++++++--- tests/lean/run/test_proj_hints.lean | 48 +++++++++++++++++++ tests/lean/run/test_simp_reducible_class.lean | 13 ++++- 3 files changed, 92 insertions(+), 8 deletions(-) create mode 100644 tests/lean/run/test_proj_hints.lean diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 1541a7964a..88015b5206 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -1359,9 +1359,6 @@ private def isDefEqLeftRight (fn : Name) (t s : Expr) : MetaM LBool := do private def isNonTrivialRegular (info : DefinitionVal) : MetaM Bool := do match info.hints with | .regular d => - if (← isProjectionFn info.name) then - -- All projections are considered trivial - return false if d > 2 then -- If definition depth is greater than 2, we claim it is not a trivial definition return true @@ -1369,7 +1366,37 @@ private def isNonTrivialRegular (info : DefinitionVal) : MetaM Bool := do -- Where simple is a bvar/lit/sort/proj or a single application where all arguments are bvar/lit/sort/proj. let val := consumeDefnPreamble info.value return !isSimple val (allowApp := true) - | _ => return false + | .abbrev => + /- + **Note**: All projection functions receive `.abbrev` kernel hints (not `.regular`), regardless of their + reducibility status. Structure projections default to `.reducible` status, while + class projections default to `.semireducible` status. Recall kernel hints and reducibility hints are + two different concepts. + + Projections have `.abbrev` hints and are generally considered trivial. But there is an exception + when the projection is a class field and `backward.whnf.reducibleClassField` is `true`. + In this scenario, `unfoldDefault` reduces past the `.proj` form at `.instances` transparency. + This means the unfolded result may lose the instance structure that `isDefEqProj` needs to bump + transparency. As an example, consider the following declarations + ``` + @[implicit_reducible] def a := 0 + @[implicit_reducible] def b := 0 + class X where x : Nat + instance instX (n : Nat) : X where x := n + attribute [reducible] X.x + ``` + Then, assume `isDefEqDelta` sees `X.x (instX a) =?= X.x (instX b)` and the transparency setting + is `.reducible`. If we assume this kind of projection is trivial, `tryHeuristic` skips the + argument comparison, and `unfoldDefault` reduces `X.x (instX a)` all the way to `a` + (via projection reduction at `.instances`). The resulting `a =?= b` comparison fails at + `.reducible` because both are `@[implicit_reducible]`. + Thus, we classify this kind of projection as nontrivial, and `isDefEqArgs` + compares `instX a =?= instX b` with the correct transparency bump for + instance-implicit parameters, which succeeds. -/ + if let some projInfo ← getProjectionFnInfo? info.name then + return projInfo.fromClass && backward.whnf.reducibleClassField.get (← getOptions) + return false + | .opaque => return false where consumeDefnPreamble (e : Expr) : Expr := match e with @@ -1396,7 +1423,7 @@ private def tryHeuristic (t s : Expr) : MetaM Bool := do let .defnInfo info ← getConstInfo tFn.constName! | return false /- We apply the heuristic in the following cases: - 1- `f` is a non-trivial regular definition (see predicate `isNonTrivialRegular`) + 1- `f` is a non-trivial definition (see predicate `isNonTrivialRegular`) 2- `f` is `match` application. 3- `t` or `s` contain meta-variables. @@ -1404,7 +1431,7 @@ private def tryHeuristic (t s : Expr) : MetaM Bool := do `S.proj ?x =?= S.proj t` without performing delta-reduction. When the conditions 1&2&3 do not hold, we are assuming the heuristic implemented by this method is seldom effective - when `f` is not simple, `t` and `s` do not have metavariables, are not structurally equal. + when `f` is simple, `t` and `s` do not have metavariables, and are not structurally equal. Recall that auxiliary `match` definitions are marked as abbreviations, but we must use the heuristic on them since they will not be unfolded when smartUnfolding is turned on. The abbreviation annotation in this diff --git a/tests/lean/run/test_proj_hints.lean b/tests/lean/run/test_proj_hints.lean new file mode 100644 index 0000000000..d04a21d5e7 --- /dev/null +++ b/tests/lean/run/test_proj_hints.lean @@ -0,0 +1,48 @@ +import Lean + +/-! +# Test: projection functions have `.abbrev` kernel hints + +All projection functions receive `.abbrev` kernel hints at creation time. +Structure projections default to `.reducible` status, while class projections +default to `.semireducible` status. The `@[reducible]` attribute changes the +reducibility status but does **not** change the kernel hint. + +These properties are relied upon by `isNonTrivialRegular` in `ExprDefEq.lean`. +That function uses the `.abbrev` branch to detect class projections and treat +them as nontrivial when `backward.whnf.reducibleClassField` is enabled, so that +`tryHeuristic` applies the argument-comparison heuristic (with the correct +transparency bump for instance-implicit parameters) instead of unfolding past +the `.proj` form. If the kernel hints or default reducibility status for +projections change, `isNonTrivialRegular` must be updated accordingly. +-/ + +structure Y where + x : Nat + +class X where + x : Nat + +open Lean +deriving instance Repr for ReducibilityHints + +def showHintAndReduceAttr (declName : Name) : CoreM Unit := do + let info ← getConstInfo declName + IO.println (repr info.hints) + IO.println (repr (← getReducibilityStatus declName)) + +-- Structure projection: `.abbrev` hint, `.reducible` status +/-- +info: Lean.ReducibilityHints.abbrev +Lean.ReducibilityStatus.reducible +-/ +#guard_msgs in +#eval showHintAndReduceAttr ``Y.x + +-- Class projection: `.abbrev` hint, `.semireducible` status +/-- +info: Lean.ReducibilityHints.abbrev +Lean.ReducibilityStatus.semireducible +-/ +#guard_msgs in +#eval showHintAndReduceAttr ``X.x diff --git a/tests/lean/run/test_simp_reducible_class.lean b/tests/lean/run/test_simp_reducible_class.lean index 868e178562..8251aba767 100644 --- a/tests/lean/run/test_simp_reducible_class.lean +++ b/tests/lean/run/test_simp_reducible_class.lean @@ -24,12 +24,21 @@ instance instX (n : Nat) : X where -- isDefEqArgs bumps to .instances for instance-implicit param of X.x example : (instX a).x = (instX b).x := by simp --- Test 2: plain simp, @[reducible] X.x (BROKEN on master, fixed by isDefEqProj change) --- isDefEqDelta unfolds X.x to .proj form, isDefEqProj needs withInstanceConfig +-- Test 2: plain simp, @[reducible] X.x +-- With backward.whnf.reducibleClassField = false: isDefEqDelta unfolds X.x to .proj form, +-- isDefEqProj bumps to .instances via withInstanceConfig. +-- With backward.whnf.reducibleClassField = true: tryHeuristic in isDefEqDelta applies the +-- argument-comparison heuristic, and isDefEqArgs bumps to .instances for instance-implicit params. set_option allowUnsafeReducibility true in attribute [reducible] X.x in example : (instX a).x = (instX b).x := by simp +-- Test 2b: same as Test 2 with backward.whnf.reducibleClassField explicitly enabled +set_option allowUnsafeReducibility true in +attribute [reducible] X.x in +set_option backward.whnf.reducibleClassField true in +example : (instX a).x = (instX b).x := by simp + -- Test 3: simp [X.x] with semireducible args exposes stuck .proj node -- reduceProjFn? unfolds X.x at .instances, but the .proj can't reduce further -- because instX a' is not a constructor app at .reducible. This is expected: