fix: extend sym canonicalizer reductions to value positions#13272
Merged
Conversation
This PR extends the sym canonicalizer to apply reductions (projection, match/ite/cond, Nat arithmetic) in all positions, not just inside types. Previously, a value `v` appearing in a type `T(v)` could remain unreduced while `T(v)` was normalized, breaking the invariant that definitionally equal types are structurally identical after canonicalization. This also adds `canonInstDecCore` to properly handle `Decidable` instances in `if-then-else` expressions, and suppresses issue reporting for propositional and decidable instances that cannot be resynthesized (common with `haveI`-provided instances). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
volodeyka
pushed a commit
that referenced
this pull request
Apr 16, 2026
This PR extends the sym canonicalizer to apply reductions (projection, match/ite/cond, Nat arithmetic) in all positions, not just inside types. Previously, a value `v` appearing in a type `T(v)` could remain unreduced while `T(v)` was normalized, breaking the invariant that definitionally equal types are structurally identical after canonicalization. Changes: - Remove `insideType` guards from `canonApp` and `canonProj`, so reductions apply unconditionally (eta reduction remains type-only, to preserve lambda structure for `grind`) - Add `canonInstDecCore` to handle `Decidable` instances in `if-then-else` expressions, dispatching `Grind.nestedDecidable` to `canonInstDec` and falling back silently for other instances - Add `report` parameter to `canonInstCore`/`canonInst'`/`canonInst` to allow suppressing issue reporting for propositional and decidable instances that cannot be resynthesized (common with `haveI`-provided instances that propagate into types through forward dependencies) - Update module documentation to reflect the new reduction scope and the `haveI` reporting tradeoff Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
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 extends the sym canonicalizer to apply reductions (projection, match/ite/cond, Nat
arithmetic) in all positions, not just inside types. Previously, a value
vappearing in atype
T(v)could remain unreduced whileT(v)was normalized, breaking the invariant thatdefinitionally equal types are structurally identical after canonicalization.
Changes:
insideTypeguards fromcanonAppandcanonProj, so reductions apply unconditionally(eta reduction remains type-only, to preserve lambda structure for
grind)canonInstDecCoreto handleDecidableinstances inif-then-elseexpressions, dispatchingGrind.nestedDecidabletocanonInstDecand falling back silently for other instancesreportparameter tocanonInstCore/canonInst'/canonInstto allow suppressing issuereporting for propositional and decidable instances that cannot be resynthesized (common with
haveI-provided instances that propagate into types through forward dependencies)haveIreporting tradeoff