mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
5d86aa4032
This PR fixes a gap in how `@[implicit_reducible]` is assigned to parent projections during structure elaboration. When `class C extends P₁, P₂` has diamond inheritance, some ancestor structures become constructor subobject fields even though they aren't direct parents. For example, in `Monoid extends Semigroup, MulOneClass`, `One` becomes a constructor subobject of `Monoid` — its field `one` doesn't overlap with `Semigroup`'s fields, and `inSubobject?` is `none` during `MulOneClass` flattening. `mkProjections` creates the projection `Monoid.toOne` but defers reducibility to `addParentInstances` (guarded by `if !instImplicit`). However, `addParentInstances` only processes direct parents from the `extends` clause. Grandparent subobject projections fall through the gap and stay `semireducible`. This causes defeq failures when `backward.isDefEq.respectTransparency` is enabled (#12179): at `.instances` transparency, the semireducible grandparent projection can't unfold, so two paths to the same ancestor structure aren't recognized as definitionally equal. Fix: before `addParentInstances`, iterate over all `.subobject` fields and set `implicitReducible` on those whose parent is a class. 🤖 Prepared with Claude Code --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>