Add sort cumulativity for polymorphic inductive types#21770
Closed
JasonGross wants to merge 2 commits into
Closed
Conversation
coqbot-app
Bot
added
the
needs: full CI
JasonGross
added
part: universes
When enabled via the "Polymorphic Inductive Sort Cumulativity" flag,
cumulative polymorphic inductives allow sorts in the same connected
component ({Prop, Type/Set} or {SProp}) to be treated as equivalent
at quality positions with non-Invariant inferred variance.
This is implemented via instance normalization: before comparing
cumulative instances, quality positions with non-Invariant sort
variance where both qualities are in the same connected component
are replaced with a canonical representative (QType), making the
existing quality equality checks pass transparently.
Key changes:
- New fields mind_sort_variance/mind_sec_sort_variance in declarations
- New field mind_entry_sort_variance in entries
- Sort variance inference in inferCumulativity.ml (SortInf module)
- Instance normalization via normalize_sort_cumul_instances in uVars.ml
- sort_cumulative field in PolyFlags.t
- Normalization applied in conversion, typeops, eConstr, evarconv
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
JasonGross
force-pushed
the
sort-cumulativity
branch
from
f9ee6b5 to
378c4f8
Compare
coqbot-app
Bot
removed
request: full CI
Instead of normalizing instances at each call site before comparison, pass sort_variance through the comparison API and normalize internally. - Add sort_variance parameter to compare_cumul_instances callback type - Add ?sort_variance optional param to enforce_eq/leq_variance_instances, compare_cumulative_instances (UnivProblem, Evarutil), and compare_constructor_instances - Remove normalize_sort_cumul_instances calls from call sites (conversion.ml, typeops.ml, eConstr.ml, evarconv.ml) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
coqbot-app
Bot
added
the
needs: full CI
ppedrot
reviewed
Mar 18, 2026
| compare_sorts : conv_pb -> Sorts.t -> Sorts.t -> 'a -> ('a, 'err option) result; | ||
| compare_instances: flex:bool -> UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) result; | ||
| compare_cumul_instances : conv_pb -> UVars.Variance.t array -> | ||
| compare_cumul_instances : conv_pb -> UVars.Variance.t array -> UVars.Variance.t array option -> |
Member
There was a problem hiding this comment.
This shouldn't be an option, and we should probably introduce a type of variances containing both sort and level variances similarly to what we do with Instance.t
Contributor
|
Replaced by #21773 |
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
3 participants
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.
When enabled via the "Polymorphic Inductive Sort Cumulativity" flag, cumulative polymorphic inductives allow sorts in the same connected component ({Prop, Type/Set} or {SProp}) to be treated as equivalent at quality positions with non-Invariant inferred variance.
This is implemented via instance normalization: before comparing cumulative instances, quality positions with non-Invariant sort variance where both qualities are in the same connected component are replaced with a canonical representative (QType), making the existing quality equality checks pass transparently.
Key changes:
Note that I have not looked over the code, creating this PR so @tabareau or @SkySkimmer can review if they want.
Added / updated test-suite.
Added changelog.
Added / updated documentation.