All the pieces are now in place so that the RuleBuilder can assemble
a confluent rewrite system for downstream protocol dependencies,
instead of building rules from protocol requirement signatures.
Completion adds this rule when a same-type requirement equates the Self of P
with some other type parameter conforming to P; one example is something like this:
protocol P {
associatedtype T : P where T.T == Self
}
The initial rewrite system looks like this:
(1) [P].T => [P:T]
(2) [P:T].[P] => [P:T]
(3) [P:T].[P:T] => [P]
Rules (2) and (3) overlap on the term
[P:T].[P:T].[P]
Simplifying the overlapped term with rule (2) produces
[P:T].[P:T]
Which further reduces to
[P]
Simplifying the overlapped term with rule (3) produces
[P].[P]
So we get a new rule
[P].[P] => [P]
This is not a "real" conformance rule, and homotopy reduction wastes work
unraveling it in rewrite loops where this rule occurs. Instead, it's better
to introduce it as a permanent rule that is not subject to homotopy reduction
for every protocol.
I have a lot more known-failing GSB test cases, but the limiting factor
now is the GSB's minimization algorithm, which runs first before the
requirement machine gets to see anything. Replacing that with a new
algorithm based on the rewrite system is the next step here.
