RequirementMachine: Try to avoid introducing rules of the form T.[P] => T.[Q]

These rules would be fine since RHS simplification eliminates them,
but they cause problems for the minimal conformances algorithm.

To avoid introducing such rules, ensure that the critical pair of
two property-like rules is itself a property-like rule instead of
relying on subsequent simplifications sorting it out. See the
new comment in RewriteSystem::computeCriticalPair() for details.

I need to understand this problem better and either fix minimal
conformances or add stronger assertions, but for now this fixes
the last failure with -requirement-machine-abstract-signatures=verify.

Author: slavapestov

lib/AST/RequirementMachine/KnuthBendix.cpp

@@ -212,8 +212,56 @@ RewriteSystem::computeCriticalPair(ArrayRef<Symbol>::const_iterator from,
       return false;
     }
 
-    // Add the pair (XV, TY).
-    pairs.emplace_back(xv, ty, path);
+    // If Y == UW for some W, then the critical pair is (XV, TUW),
+    // and we have
+    // - lhs == (TU -> X)
+    // - rhs == (UV -> UW).
+    //
+    // 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
+    // V == W.[p] for some property symbol p, then we in fact have a pair
+    // of property rules:
+    //
+    // - lhs == (T.[P] => T)
+    // - rhs == ([P].W.[p] => [P].W)
+    //
+    // Without this hack, the critical pair would be:
+    //
+    // (T.w.[p] => T.[P].w)
+    //
+    // With this hack, the critical pair becomes:
+    //
+    // (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.
+    //
+    // 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 (lhs.getLHS().size() <= ty.size() &&
+        std::equal(lhs.getLHS().begin(),
+                   lhs.getLHS().end(),
+                   ty.begin())) {
+      unsigned endOffset = ty.size() - lhs.getLHS().size();
+      path.add(RewriteStep::forRewriteRule(/*startOffset=*/0,
+                                           endOffset,
+                                           getRuleID(lhs),
+                                           /*inverse=*/false));
+
+      // Compute the term XW.
+      MutableTerm xw(lhs.getRHS());
+      xw.append(ty.end() - endOffset, ty.end());
+
+      pairs.emplace_back(xv, xw, path);
+    } else {
+      pairs.emplace_back(xv, ty, path);
+    }
   }
 
   return true;

lib/AST/RequirementMachine/RewriteSystem.cpp

@@ -563,6 +563,10 @@ void RewriteSystem::simplifyRightHandSides() {
 
     unsigned newRuleID = Rules.size();
 
+    if (Debug.contains(DebugFlags::Add)) {
+      llvm::dbgs() << "## RHS simplification adds a rule " << lhs << " => " << rhs << "\n\n";
+    }
+
     // Add a new rule with the simplified right hand side.
     Rules.emplace_back(lhs, Term::get(rhs, Context));
     auto oldRuleID = Trie.insert(lhs.begin(), lhs.end(), newRuleID);

test/Generics/simplify_rhs_elimination_order.swift

@@ -0,0 +1,37 @@
+// RUN: %target-swift-frontend -typecheck %s -debug-generic-signatures -requirement-machine-protocol-signatures=on -requirement-machine-inferred-signatures=on 2>&1 | %FileCheck %s
+
+public protocol P1 {
+  associatedtype T
+}
+
+public protocol P2 : P1 {}
+
+public protocol P3 : P2 {}
+
+public protocol Q1 {}
+
+public protocol Q2 : Q1 {}
+
+public protocol Q3 : Q1 {}
+
+public protocol R {
+  associatedtype U: Q2, Q3
+}
+
+struct G<X: P3, Y: R> where X.T == Y.U {
+  // CHECK-LABEL: .G.Nested0@
+  // CHECK-NEXT: <X, Y, Z where X : P3, Y : R, X.[P1]T == Y.[R]U>
+  struct Nested0<Z> {}
+
+  // CHECK-LABEL: .G.Nested1@
+  // CHECK-NEXT: <X, Y, Z where X : P3, Y : R, X.[P1]T == Y.[R]U>
+  struct Nested1<Z> where X.T : Q1 {}
+
+  // CHECK-LABEL: .G.Nested2@
+  // CHECK-NEXT: <X, Y, Z where X : P3, Y : R, X.[P1]T == Y.[R]U>
+  struct Nested2<Z> where X.T : Q2 {}
+
+  // CHECK-LABEL: .G.Nested3@
+  // CHECK-NEXT: <X, Y, Z where X : P3, Y : R, X.[P1]T == Y.[R]U>
+  struct Nested3<Z> where X.T : Q3 {}
+}