fix: centralise the module-system Array/Vector kernel-reduction workarounds - #9044
Merged
Conversation
…rounds This PR replaces the per-module `import all Init.Data.Array.DecidableEq` workaround with two shared shims in `HexBasic`, and records the full upstream picture so the eventual removal is mechanical. `HexBasic.ArrayDecEq` supplies higher-priority `DecidableEq` instances for `Array` and `Vector` that route through the fully exposed `List` equality, so `decide` and `rfl` over them reduce in the kernel under the module system. Twenty-six modules across `HexBerlekampZassenhaus`, `HexRealRoots`, `HexRCF`, and `HexBerlekampZassenhausMathlib` now import it instead of carrying their own copy of the workaround and its four-line explanation. `HexPoly.Dense` keeps its local instance, since `hex-poly` has no dependencies and cannot import `HexBasic`; its comment now says so. `HexBasic.OfFn` supplies `Array.ofFn'` and `Vector.ofFn'`, which go through `List.ofFn` and reduce, with `ofFn'_eq_ofFn` proving them equal to the core versions. The core `Array.ofFn` delegates to an unexposed `ofFn.go`, and `Vector.ofFn` inherits that, so neither reduces downstream. Chasing the `Vector` case turned up two further instances of the same defect beyond the known `Array.instDecidableEqImpl` one: every `deriving DecidableEq` instance is opaque across a module boundary, which is how `Vector` gets its instance and which has no consumer-side workaround, and `Array.ofFn` delegates to an unexposed auxiliary. All three are fixed upstream by leanprover/lean4#14270. `progress/lean4-array-decidableeq-module-repro.md` now records all three with minimal repros and carries the cleanup checklist for when that lands. Progress file: progress/2026-07-28T10-40-00Z.md Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0188fgvPvjbcXhvTYVSATLhv
`(List.ofFn f).toArray` is the shape the kernel can reduce, and the wrong shape
for compiled code, which wants to fill an array of known capacity rather than
build a linked list and convert. A `@[csimp]` redirect back to `Array.ofFn` /
`Vector.ofFn` means the `List` route is paid only in the kernel.
`@[csimp]` requires a literal `@f = @g`, so `Vector.ofFn'` takes its implicits
in core's order (`{n} {α}`, which is the opposite of `Array.ofFn`'s `{α} {n}`).
Also drops `scratch-mvpoly-bench/` from the branch, which `git add -A` had swept
in, and ignores `scratch-*/` so it cannot recur.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0188fgvPvjbcXhvTYVSATLhv
…ry tests Follow-up to review of the shim. The `DecidableEq` instances are now `scoped`, so they apply only inside `namespace Hex` or after `open scoped Hex`. As global instances they overrode core's for every downstream consumer, including consumers of the released libraries that depend on `hex-basic`, which is far too much reach for a workaround that exists to be deleted. A module that forgets to activate them now gets a stuck `decide`, which is loud. Compiled equality regressed the same way `ofFn'` did: routing through `List` means an `O(n)` conversion that allocates both lists in full before comparison starts and loses early exit. Both instances now carry a `@[csimp]` redirect back to the core deciders, proved by `Subsingleton.elim`, so the `List` route is paid only in the kernel. `HexBasic/ModuleBoundaryTests.lean` exercises all three gaps from a separate module, which is the only place they are observable: the defect is that a callee's body is unavailable across a module boundary, so a same-module test passes whether or not the workaround is present. The removal checklist in the repro note was self-contradictory (claiming `ofFn` had no workaround while providing one) and unordered. It now runs call sites before deletions, uses `rg` assertions that must return nothing, names the exact `DensePoly` replacement, and drops `Array.back?`, which is a related exposure gap that #14270 does not fix. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0188fgvPvjbcXhvTYVSATLhv
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 replaces the per-module
import all Init.Data.Array.DecidableEqworkaround with two shared shims inHexBasic, and records the full upstream picture so the eventual removal is mechanical.HexBasic.ArrayDecEqsupplies higher-priorityDecidableEqinstances forArrayandVectorthat route through the fully exposedListequality, sodecideandrflover them reduce in the kernel under the module system. Twenty-six modules acrossHexBerlekampZassenhaus,HexRealRoots,HexRCF, andHexBerlekampZassenhausMathlibnow import it instead of carrying their own copy of the workaround and its four-line explanation.HexPoly.Densekeeps its local instance, sincehex-polyhas no dependencies and cannot importHexBasic; its comment now says so.HexBasic.OfFnsuppliesArray.ofFn'andVector.ofFn', which go throughList.ofFnand reduce, withofFn'_eq_ofFnproving them equal to the core versions. The coreArray.ofFndelegates to an unexposedofFn.go, andVector.ofFninherits that, so neither reduces downstream.Chasing the
Vectorcase turned up two further instances of the same defect beyond the knownArray.instDecidableEqImplone. Everyderiving DecidableEqinstance is opaque across a module boundary, which is howVectorgets its instance and which has no consumer-side workaround at all, since@[expose]cannot be attached to a structure or added retroactively. AndArray.ofFndelegates to an unexposed auxiliary. All three are fixed upstream by leanprover/lean4#14270, which has been reopened, rebased, and extended to cover them.progress/lean4-array-decidableeq-module-repro.mdnow records all three with minimal repros and carries the cleanup checklist for when that lands.Full
lake buildis green locally.🤖 Prepared with Claude Code