RequirementMachine: Try harder to ensure completion only introduces property-like rules

When computing an overlap between a property-like rule (T.[p] => T for some
property symbol [p]) and another rule, try harder to ensure that the new
rule is a property-like rule.

In a conformance-valid rewrite system, all rules that are not LHS- or RHS-
simplified will eventually either be property-like or same-type rules, but
we need to maintain this invariant for that rules that become simplified
as well, to ensure that rewrite loops have a certain structure that is
important for the minimal conformances algorithm.

I don't quite understand why to be honest, but I'm close to figuring it
out.

Fixes rdar://problem/91232987.

Author: slavapestov

lib/AST/RequirementMachine/KnuthBendix.cpp

@@ -157,8 +157,66 @@ RewriteSystem::computeCriticalPair(ArrayRef<Symbol>::const_iterator from,
       return false;
     }
 
-    // Add the pair (X, TYV).
-    pairs.emplace_back(x, tyv, path);
+    // If X == TUW for some W, then the critical pair is (TUW, TYV),
+    // and we have
+    // - lhs == (TUV => TUW)
+    // - rhs == (U => Y).
+    //
+    // We explicitly apply the rewrite step (Y => U) to the beginning of the
+    // rewrite path, transforming the critical pair to (TYW, TYV).
+    //
+    // In particular, if V == W.[P] for some protocol P, then we in fact have
+    // a property rule and a same-type rule:
+    //
+    // - lhs == (TUW.[P] => TUW)
+    // - rhs == (U => Y)
+    //
+    // Without this hack, the critical pair would be:
+    //
+    // (TUW => TYW.[P])
+    //
+    // With this hack, the critical pair becomes:
+    //
+    // (TYW.[P] => TYW)
+    //
+    // This ensures that the newly-added rule is itself a property rule;
+    // otherwise, this would only be the case if addRule() reduced TUW
+    // into TYW without immediately reducing some subterm of TUW first.
+    //
+    // While completion will eventually simplify all such rules down into
+    // property rules, their existance in the first place breaks subtle
+    // invariants in the minimal conformances algorithm, which expects
+    // homotopy generators describing redundant protocol conformance rules
+    // to have a certain structure.
+    if (t.size() + rhs.getLHS().size() <= x.size() &&
+        std::equal(rhs.getLHS().begin(),
+                   rhs.getLHS().end(),
+                   x.begin() + t.size())) {
+      // We have a path from TUW to TYV. Invert to get a path from TYV to
+      // TUW.
+      path.invert();
+
+      // Compute the term W.
+      MutableTerm w(x.begin() + t.size() + rhs.getLHS().size(), x.end());
+
+      // Now add a rewrite step T.(U => Y).W to get a path from TYV to
+      // TYW.
+      path.add(RewriteStep::forRewriteRule(/*startOffset=*/t.size(),
+                                           /*endOffset=*/w.size(),
+                                           getRuleID(rhs),
+                                           /*inverse=*/false));
+
+      // Compute the term TYW.
+      MutableTerm tyw(t);
+      tyw.append(rhs.getRHS());
+      tyw.append(w);
+
+      // Add the pair (TYV, TYW).
+      pairs.emplace_back(tyv, tyw, path);
+    } else {
+      // Add the pair (X, TYV).
+      pairs.emplace_back(x, tyv, path);
+    }
   } else {
     // lhs == TU -> X, rhs == UV -> Y.
 
@@ -217,7 +275,7 @@ RewriteSystem::computeCriticalPair(ArrayRef<Symbol>::const_iterator from,
     // - lhs == (TU -> X)
     // - rhs == (UV -> UW).
     //
-    // We explicitly apply the rewrite step (TU = X) to the rewrite path,
+    // We explicitly apply the rewrite step (TU => X) to the rewrite path,
     // transforming the critical pair to (XV, XW).
     //
     // In particular, if T == X, U == [P] for some protocol P, and
@@ -229,15 +287,15 @@ RewriteSystem::computeCriticalPair(ArrayRef<Symbol>::const_iterator from,
     //
     // Without this hack, the critical pair would be:
     //
-    // (T.w.[p] => T.[P].w)
+    // (T.W.[p] => T.[P].W)
     //
     // With this hack, the critical pair becomes:
     //
-    // (T.w.[p] => T.w)
+    // (T.W.[p] => T.W)
     //
     // This ensures that the newly-added rule is itself a property rule;
-    // otherwise, this would only be the case if addRule() reduced T.[P].w
-    // into T.w without immediately reducing some subterm of T first.
+    // otherwise, this would only be the case if addRule() reduced T.[P].W
+    // into T.W without immediately reducing some subterm of T first.
     //
     // While completion will eventually simplify all such rules down into
     // property rules, their existance in the first place breaks subtle

test/Generics/rdar91232987.swift

@@ -0,0 +1,91 @@
+// RUN: %target-swift-frontend -typecheck %s -debug-generic-signatures 2>&1 | %FileCheck %s
+
+// CHECK-LABEL: rdar91232987.(file).P1@
+// CHECK-NEXT: Requirement signature: <Self where Self.[P1]A1 : Decodable, Self.[P1]A1 : Encodable, Self.[P1]A1 : P2, Self.[P1]A1.[P2]A3.[P5]A6 : Decodable, Self.[P1]A1.[P2]A3.[P5]A6 : Encodable>
+protocol P1 {
+  associatedtype A1: P2 where A1: Codable, A1.A3.A6: Codable
+}
+
+// CHECK-LABEL: rdar91232987.(file).P2@
+// CHECK-NEXT: Requirement signature: <Self where Self : P3, Self.[P2]A2 : P4, Self.[P2]A3 : P5>
+protocol P2: P3 {
+  associatedtype A2: P4
+  associatedtype A3: P5
+}
+
+// CHECK-LABEL: rdar91232987.(file).P3@
+// CHECK-NEXT: Requirement signature: <Self>
+protocol P3 {}
+
+// CHECK-LABEL: rdar91232987.(file).P4@
+// CHECK-NEXT: Requirement signature: <Self where Self.[P4]A4 : P11, Self.[P4]A5 : P9>
+protocol P4 {
+  associatedtype A4: P11
+  associatedtype A5: P9
+
+}
+
+// CHECK-LABEL: rdar91232987.(file).P5@
+// CHECK-NEXT: Requirement signature: <Self where Self.[P5]A6 : P6>
+protocol P5 {
+  associatedtype A6: P6
+}
+
+// CHECK-LABEL: rdar91232987.(file).P6@
+// CHECK-NEXT: Requirement signature: <Self where Self : P10, Self : P7, Self.[P6]A7 : Decodable, Self.[P6]A7 : Encodable, Self.[P6]A7 : Hashable, Self.[P6]A7 : RawRepresentable, Self.[P6]A7.[RawRepresentable]RawValue == String>
+protocol P6: P7, P10 {
+  associatedtype A7: Hashable, Codable, RawRepresentable where A7.RawValue == String
+}
+
+// CHECK-LABEL: rdar91232987.(file).P7@
+// CHECK-NEXT: Requirement signature: <Self where Self : Equatable, Self : P8>
+protocol P7: Equatable, P8 {}
+
+// CHECK-LABEL: rdar91232987.(file).P8@
+// CHECK-NEXT: Requirement signature: <Self>
+protocol P8 {}
+
+// CHECK-LABEL: rdar91232987.(file).P9@
+// CHECK-NEXT: Requirement signature: <Self>
+protocol P9 {
+  associatedtype A8
+}
+
+// CHECK-LABEL: rdar91232987.(file).P10@
+// CHECK-NEXT: Requirement signature: <Self>
+protocol P10 {}
+
+// CHECK-LABEL: rdar91232987.(file).P11@
+// CHECK-NEXT: Requirement signature: <Self where Self.[P11]A10 : P13, Self.[P11]A9 : P12>
+protocol P11 {
+  associatedtype A9: P12
+  associatedtype A10: P13
+}
+
+// CHECK-LABEL: rdar91232987.(file).P12@
+// CHECK-NEXT: Requirement signature: <Self where Self : Decodable, Self : Encodable, Self : Equatable>
+protocol P12: Codable, Equatable {}
+
+// CHECK-LABEL: rdar91232987.(file).P13@
+// CHECK-NEXT: Requirement signature: <Self>
+protocol P13 {}
+
+// CHECK-LABEL: rdar91232987.(file).P14@
+// CHECK-NEXT: Requirement signature: <Self where Self : P16, Self.[P14]A1 : P2>
+protocol P14: P16 {
+  associatedtype A1: P2
+}
+
+// CHECK-LABEL: rdar91232987.(file).P15@
+// CHECK-NEXT: Requirement signature: <Self where Self.[P15]A6 : P6>
+protocol P15 {
+  associatedtype A6: P6
+}
+
+// CHECK-LABEL: rdar91232987.(file).P16@
+// CHECK-NEXT: Requirement signature: <Self>
+protocol P16 {}
+
+// CHECK-LABEL: rdar91232987.(file).C@
+// CHECK-NEXT: Generic signature: <X, Y where X : P14, Y : P15, X.[P14]A1 : Decodable, X.[P14]A1 : Encodable, Y.[P15]A6 : Decodable, Y.[P15]A6 : Encodable, Y.[P15]A6 == X.[P14]A1.[P2]A3.[P5]A6>
+class C<X: P14, Y: P15> where X.A1: Codable, X.A1.A3.A6: Codable, X.A1.A3.A6 == Y.A6 {}