RequirementMachine: Redo concrete contraction after splitting concrete equivalence classes #61199
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 fixes an edge case where we start with the following requirements:
and end up with the following set of minimal rules (where the type witness for [P]A in the conformance G : P is C):
Since U.[P]A and T.[P]A are concrete, we split the abstract same-type requirement into two requirements, and re-run minimization:
The concrete conformance rule T.[concrete: G : P] => T does not correspond to a requirement, so it was simply dropped, and the above rules violate post-contraction invariants; T.[P]A is not a valid type parameter because there is no conformance requirement T : P in the minimized signature.
We can fix this by re-running concrete contraction after splitting concrete equivalence classes. After contraction, the above requirements turn into
Which correctly minimizes to
Both concrete contraction and concrete equivalence class splitting are hacks, and we should think of a way to directly express the transformations they perform with the rewrite system.
Fixes #61192.