Define the relation as
[concrete: C].[P] =>> [concrete: C].[concrete: C : P]
instead of
[concrete: C].[P] =>> [concrete: C : P]
This changes the rewrite loop recorded for a rule T.[concrete: C : P]
to have (T.[concrete: C] => T) appearing twice in context instead of
just once.
We don't ever want a concrete conformance rule to be able to imply a
concrete type rule. This became possible with loop normalization
because the single occurrence of (T.[concrete: C] => T).[P] could
cancel with a subsequent step (T => T.[concrete: C]).[P] in another
rewrite loop after substitution.
See the comment at the top of ConcreteContraction.cpp for a detailed explanation.
This can be turned off with the -disable-requirement-machine-concrete-contraction
pass, mostly meant for testing. A few tests now run with this pass both enabled
and disabled, to exercise code paths which are otherwise trivially avoided by
concrete contraction.
Fixes rdar://problem/88135912.
We want to prefer to eliminate rules that are not concrete type rules,
unless non-concrete type rule in question is a projection. For example,
suppose that this rule comes from a protocol:
T.T == G<T.U, T.V>
And these three rules are in our minimization domain:
a) T.T == G<Int, W>
b) T.U == Int
c) T.V == W
Then a) implies both b) and c), and vice versa.
In this case, we want to keep T.U == Int and T.V == W, and eliminate
T.T == G<Int, W>.
T.T == G<Int, W> is concrete and T.V == W is not, but because T.V == W
is defined by a projection, we still prefer to eliminate T.T == G<Int, W>
over T.V == W.
