Revert "RequirementMachine: Remove completion procedure hacks for old minimal conformances algorithm"

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 existence 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.
 
@@ -212,8 +270,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 existence 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;
@@ -241,7 +347,7 @@ RewriteSystem::computeConfluentCompletion(unsigned maxRuleCount,
   assert(!Minimized);
   assert(!Frozen);
 
-  // 'Complete' might already be set, if we're re-running completion after
+  // Complete might already be set, if we're re-running completion after
   // adding new rules in the property map's concrete type unification procedure.
   Complete = 1;
 
@@ -253,7 +359,7 @@ RewriteSystem::computeConfluentCompletion(unsigned maxRuleCount,
   do {
     ruleCount = Rules.size();
 
-    // For every rule, look for other rules that overlap with this rule.
+    // For every rule, looking for other rules that overlap with this rule.
     for (unsigned i = FirstLocalRule, e = Rules.size(); i < e; ++i) {
       const auto &lhs = getRule(i);
       if (lhs.isLHSSimplified() ||