Slava Pestov 658ba01741 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 https://github.com/apple/swift/issues/61192.

2022-09-19 23:50:21 -04:00

37 KiB

Raw Blame History

View Raw