You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
RequirementMachine: Redo concrete contraction after splitting concrete equivalence classes
This fixes an edge case where we start with the following requirements:
- U : P
- T : P
- T.[P]A == C
- T == G<T.[P]A>
- U.[P]A == T.[P]A
and end up with the following set of minimal rules (where the type
witness for [P]A in the conformance G<C> : P is C):
- U.[P] => U
- U.[P:A] => T.[P:A]
- T.[concrete: G<C>] => T
- T.[concrete: G<C> : P] => T
Since U.[P]A and T.[P]A are concrete, we split the abstract same-type
requirement into two requirements, and re-run minimization:
- U : P
- T.[P]A == C
- U.[P]A == C
- T == G<C>
The concrete conformance rule T.[concrete: G<C> : 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
- U : P
- C == C
- U.[P]A == C
- T == G<C>
Which correctly minimizes to
- U : P
- U.[P]A == C
- T == G<C>
Both concrete contraction and concrete equivalence classes are hacks,
and we should think of a way to directly express the transformations
they perform with the rewrite system.
Fixes#61192.
0 commit comments