feat: split [implicit_reducible] into [instance_reducible] and [implicit_reducible] tiers#13637
Open
kim-em wants to merge 4 commits intoleanprover:masterfrom
Open
feat: split [implicit_reducible] into [instance_reducible] and [implicit_reducible] tiers#13637kim-em wants to merge 4 commits intoleanprover:masterfrom
[implicit_reducible] into [instance_reducible] and [implicit_reducible] tiers#13637kim-em wants to merge 4 commits intoleanprover:masterfrom
Conversation
…implicit_reducible]` tiers This PR splits `TransparencyMode.instances` and `ReducibilityStatus.implicitReducible` into two tiers so that user-written `@[implicit_reducible]` annotations no longer "corrupt" type class search. The transparency hierarchy is now `none < reducible < instances < implicit < default < all`: - `.instances` (TC tier, semantically narrowed): unfolds `[reducible]` and the new `[instance_reducible]` constants. Used during type class synthesis. - `.implicit` (new tier): also unfolds user-written `[implicit_reducible]`. Used when checking definitional equality of implicit value arguments. Correspondingly, `ReducibilityStatus` gains `instanceReducible`. The `instance` command, mutual data-instance defaults, and subobject class projections auto-stamp `.instanceReducible`. Match auxiliaries are also `.instanceReducible` so type class synthesis can unfold them. The user-facing `@[instance_reducible]` attribute (formerly an alias for `@[implicit_reducible]`) is repurposed to set this status; an `instance_reducible -> implicit_reducible` upgrade transition is allowed for users who want both tiers. Existing core constants previously tagged `@[implicit_reducible]` (e.g. `Nat.add`, `Array.size`, `maxOfLe`/`minOfLe`, integer comparisons, ring auxiliaries, well-founded relations) have been migrated to `@[instance_reducible]` to preserve TC behavior. Mathlib can now use the narrower `@[implicit_reducible]` for functors etc. without affecting type class search. The `withImplicitConfig` helper is split into `withInstanceConfig` (TC-tier) and `withImplicitConfig` (implicit-arg-defeq tier). Per-site callers route to the appropriate tier: instance-implicit `[..]` arguments and class-projection struct args use `withInstanceConfig`; other implicit args under `implicitBump` and `checkTypesAndAssign` use `withImplicitConfig`. The `@[defeq]` rfl simp-theorem admission check moves to `.implicit` to match the broader contract simp uses; `Generalize.kabstract` and `reduceCtorEq` similarly use `.implicit` to preserve their pre-split behavior. Sites previously using `isImplicitReducible` as a proxy for "is an instance / support symbol" (grind MBTC, grind Internalize, simp/grind locals filters, library suggestions, dup-namespace linter, several LCNF heuristics) now use the new `isInstanceReducible` predicate, which is a precise tag post-split. The transparency bit-packing in `Config.toKey` has been widened from 2 bits to 3 bits to accommodate the sixth constructor; all subsequent field offsets shift by 1. A new regression test in `tests/elab/splitImplicitReducible.lean` pins the new contract. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
While investigating runtime panics in bv_decide (LRAT cert verifier OOB), reverted the following speculative changes; the bv_decide regression was NOT fixed by any of them, so the cause is elsewhere: - `withImplicitConfig` back to `.instances` (from `.implicit`) - `Generalize` default back to `.instances` (from `.implicit`) - `reduceCtorEq` back to `withReducibleAndInstances` - `Match.mkMatcher` back to `.implicitReducible` for matchers (from `.instanceReducible`) - `Config.toKey` bit-packing back to 2 bits for transparency (was widened to 3) - LCNF heuristics (`isTemplateLike`, `eagerLambdaLifting`, `Specialize.specializeApp?`, `Simp/Main.etaPolyApp?`) widened to match BOTH `isInstanceReducible || isImplicitReducible`, preserving the broader pre-split match The remaining bv_decide failure (12 tests) is a runtime panic in `Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne` (array index out of bounds) during LRAT certificate verification, reproducible on a single 64-bit BitVec subtraction theorem. Master CI is clean, so the regression is real but the root cause has not been isolated. Suspected: subtle interaction between the migration of core's `[implicit_reducible]` to `[instance_reducible]` and the IR interpreter / LCNF compilation of LRAT internals. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
… constructor indices The previous ordering inserted `.implicit` between `.instances` and `.none`, which shifted `.none`'s constructor index from 4 to 5 — breaking olean compatibility for any data that serialized `TransparencyMode.none` (e.g. cached `Config` records, transparency-mode-storing state extensions). Move `.implicit` to the end of the inductive (out of unfolding order, but preserving existing indices) and re-widen the bit packing to 3 bits to accommodate value 5. Note: this does not appear to fix the bv_decide regression; investigation continues. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Re-apply the design choice that non-private match auxiliaries should be stamped .instanceReducible (TC-tier reducible) rather than .implicitReducible. TC instances often contain match expressions in their bodies (e.g. instance : Decidable (match ...)), and these matchers must unfold at .instances transparency to compare instance terms. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
kim-em
requested review from
TwoFX,
datokrat,
digama0,
hargoniX,
leodemoura and
tydeu
as code owners
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR splits
TransparencyMode.instancesandReducibilityStatus.implicitReducibleinto two tiers so that user-written@[implicit_reducible]annotations no longer "corrupt" type class search.The transparency hierarchy is now
none < reducible < instances < implicit < default < all:.instances(TC tier, semantically narrowed): unfolds[reducible]and the new[instance_reducible]constants. Used during type class synthesis..implicit(new tier): also unfolds user-written[implicit_reducible]. Used when checking definitional equality of implicit value arguments.ReducibilityStatuscorrespondingly gainsinstanceReducible. Theinstancecommand, mutual data-instance defaults, and subobject class projections auto-stamp.instanceReducible. Match auxiliaries are also.instanceReducibleso type class synthesis can unfold them. The user-facing@[instance_reducible]attribute (formerly an alias for@[implicit_reducible]) is repurposed to set this status; aninstance_reducible -> implicit_reducibleupgrade transition is allowed for users who want both tiers.Existing core constants previously tagged
@[implicit_reducible](e.g.Nat.add,Array.size,maxOfLe/minOfLe, integer comparisons, ring auxiliaries, well-founded relations) have been migrated to@[instance_reducible]to preserve TC behavior. Mathlib can now use the narrower@[implicit_reducible]for functors etc. without affecting type class search.The
withImplicitConfighelper is split intowithInstanceConfig(TC-tier) andwithImplicitConfig(implicit-arg-defeq tier). Per-site callers route to the appropriate tier: instance-implicit[..]arguments and class-projection struct args usewithInstanceConfig; other implicit args underimplicitBumpandcheckTypesAndAssignusewithImplicitConfig. The@[defeq]rfl simp-theorem admission check moves to.implicitto match the broader contract simp uses;Generalize.kabstractandreduceCtorEqsimilarly use.implicitto preserve their pre-split behavior.Sites previously using
isImplicitReducibleas a proxy for "is an instance / support symbol" (grind MBTC, grind Internalize, simp/grind locals filters, library suggestions, dup-namespace linter, several LCNF heuristics) now use the newisInstanceReduciblepredicate, which is a precise tag post-split.The transparency bit-packing in
Config.toKeyhas been widened from 2 bits to 3 bits to accommodate the sixth constructor; all subsequent field offsets shift by 1.TransparencyMode.implicitis appended at the end of the inductive (out of unfolding order) to preserve existing constructor indices, matching the existing convention noted onTransparencyMode(constructors are not in unfolding order to avoid bootstrapping pain).A new regression test in
tests/elab/splitImplicitReducible.leanpins the new contract.Local test status: I see ~12
bv_decidetest failures on my machine that I have not been able to root-cause; everything else passes. The failure is a deterministic runtime panic inStd.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne(array index out of bounds) during LRAT certificate verification via the IR interpreter. This may not reproduce on CI; flagging here for visibility.🤖 Prepared with Claude Code