621c558c13
This PR fixes `processDefDeriving` to propagate the `meta` attribute to instances derived via delta deriving, so that `deriving BEq` inside a `public meta section` produces a meta instance. Previously the derived `instBEqFoo` was not marked meta, and the LCNF visibility checker rejected meta definitions that used `==` on the alias — this came up while bumping verso to v4.30.0-rc1. `processDefDeriving` now computes `isMeta` from two sources: 1. `(← read).isMetaSection` — true inside a `public meta section`, covering the original issue #13313. 2. `isMarkedMeta (← getEnv) declName` — true when the type being derived for was individually marked `meta` (e.g. `meta def Foo := Nat`), via `elabMutualDef` in `src/Lean/Elab/MutualDef.lean`. This value is passed to `wrapInstance` for aux declarations and to the new `addAndCompile (markMeta := ...)` parameter from #13311, matching how the regular command elaboration pipeline handles meta definitions. Existing regression tests `tests/elab/13043.lean` and `tests/elab/12897.lean` already cover meta-section + `wrapInstance` aux def interaction. The new `tests/elab/13313.lean` specifically covers the delta-derived `BEq` + LCNF-use case (the original issue) and an explicit `meta def ... deriving BEq` outside a meta section (motivating the second disjunct). - [ ] depends on: #13311 Closes #13313 🤖 Prepared with Claude Code --------- Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
45 lines
1,019 B
Text
45 lines
1,019 B
Text
module
|
|
|
|
-- Test that `deriving` inside a `public meta section` produces meta instances
|
|
|
|
public meta section
|
|
|
|
-- Delta deriving for definitions
|
|
@[expose] def Foo := Nat
|
|
deriving BEq
|
|
|
|
-- Meta definitions should be able to use the derived instance
|
|
def test (a b : Foo) : Bool := a == b
|
|
|
|
-- Standalone deriving instance for definitions
|
|
@[expose] def Bar := Nat
|
|
deriving instance Hashable for Bar
|
|
|
|
def testBar (a : Bar) : UInt64 := hash a
|
|
|
|
-- Handler-based deriving for inductives
|
|
inductive Baz where
|
|
| a | b
|
|
deriving BEq, Repr, Hashable
|
|
|
|
def testBaz (x y : Baz) : Bool := x == y
|
|
|
|
-- DecidableEq for meta enums
|
|
inductive Qux where
|
|
| x | y | z
|
|
deriving DecidableEq
|
|
|
|
def testDecEq (a b : Qux) : Bool := a == b
|
|
|
|
end
|
|
|
|
-- Outside any `meta section`: explicit `meta def` should also produce meta delta-derived instances.
|
|
-- This exercises the `isMarkedMeta (← getEnv) declName` branch in `processDefDeriving`.
|
|
public section
|
|
|
|
@[expose] meta def Quux := Nat
|
|
deriving BEq
|
|
|
|
meta def testQuux (a b : Quux) : Bool := a == b
|
|
|
|
end
|