RequirementMachine: Simplify concrete substitutions when adding a new rule

Suppose we have these rules:

  (1) [P].[P] => [P]
  (2) [P].[P:X] => [P:X]
  (3) [P].[P:Y] => [P:Y]
  (4) [P:X].[concrete: G<τ_0_0> with <[P:Y]>]

Rule (2) and (4) overlap on the following term, which has had the concrete
type adjustment applied:

  [P].[P:X].[concrete: G<τ_0_0> with <[P].[P:Y]>]

The critical pair is obtained by applying rule (2) to both sides of the
branching is

  [P:X].[concrete: G<τ_0_0> with <[P].[P:Y]>] => [P:X]

Note that this is a distinct rule from (4), and again this new rule overlaps
with (2), producing another rule

  [P:X].[concrete: G<τ_0_0> with <[P].[P].[P:Y]>] => [P:X]

This process doesn't terminate. The root cause of this problem is the
existence of rule (1), which appears when there are multiple non-trivial
conformance paths witnessing the conformance Self : P. This occurs when a
same-type requirement is defined between Self and some other type conforming
to P.

To make this work, we need to simplify concrete substitutions when adding a
new rule in completion. Now that rewrite paths can represent this form of
simplification, this is easy to add.

lib/AST/RequirementMachine/RewriteSystem.cpp

@@ -136,6 +136,77 @@ void RewriteSystem::initialize(
     addRule(rule.first, rule.second);
 }
 
+/// Simplify terms appearing in the substitutions of the last symbol of \p term,
+/// which must be a superclass or concrete type symbol.
+void RewriteSystem::simplifySubstitutions(MutableTerm &term,
+                                          RewritePath &path) const {
+  auto symbol = term.back();
+  assert(symbol.isSuperclassOrConcreteType());
+
+  auto substitutions = symbol.getSubstitutions();
+  if (substitutions.empty())
+    return;
+
+  // Save the original rewrite path length so that we can reset if if we don't
+  // find anything to simplify.
+  unsigned oldSize = path.size();
+
+  // The term is on the A stack. Push all substitutions onto the A stack.
+  path.add(RewriteStep::forDecompose(substitutions.size(), /*inverse=*/false));
+
+  // Move all substitutions but the first one to the B stack.
+  for (unsigned i = 1; i < substitutions.size(); ++i)
+    path.add(RewriteStep::forShift(/*inverse=*/false));
+
+  // Simplify and collect substitutions.
+  SmallVector<Term, 2> newSubstitutions;
+  newSubstitutions.reserve(substitutions.size());
+
+  bool first = true;
+  bool anyChanged = false;
+  for (auto substitution : substitutions) {
+    // Move the next substitution from the B stack to the A stack.
+    if (!first)
+      path.add(RewriteStep::forShift(/*inverse=*/true));
+    first = false;
+
+    // The current substitution is at the top of the A stack; simplify it.
+    MutableTerm mutTerm(substitution);
+    anyChanged |= simplify(mutTerm, &path);
+
+    // Record the new substitution.
+    newSubstitutions.push_back(Term::get(mutTerm, Context));
+  }
+
+  // All simplified substitutions are now on the A stack. Collect them to
+  // produce the new term.
+  path.add(RewriteStep::forDecompose(substitutions.size(), /*inverse=*/true));
+
+  // If nothing changed, we don't have to rebuild the symbol.
+  if (!anyChanged) {
+    // The rewrite path should consist of a Decompose, followed by a number
+    // of Shifts, followed by a Compose.
+#ifndef NDEBUG
+    for (auto iter = path.begin() + oldSize; iter < path.end(); ++iter) {
+      assert(iter->Kind == RewriteStep::Shift ||
+             iter->Kind == RewriteStep::Decompose);
+    }
+#endif
+
+    path.resize(oldSize);
+    return;
+  }
+
+  // Build the new symbol with simplified substitutions.
+  auto newSymbol = (symbol.getKind() == Symbol::Kind::Superclass
+                    ? Symbol::forSuperclass(symbol.getSuperclass(),
+                                            newSubstitutions, Context)
+                    : Symbol::forConcreteType(symbol.getConcreteType(),
+                                              newSubstitutions, Context));
+
+  term.back() = newSymbol;
+}
+
 /// Adds a rewrite rule, returning true if the new rule was non-trivial.
 ///
 /// If both sides simplify to the same term, the rule is trivial and discarded,
@@ -163,6 +234,12 @@ bool RewriteSystem::addRule(MutableTerm lhs, MutableTerm rhs,
   RewritePath lhsPath;
   RewritePath rhsPath;
 
+  if (lhs.back().isSuperclassOrConcreteType())
+    simplifySubstitutions(lhs, lhsPath);
+
+  if (rhs.back().isSuperclassOrConcreteType())
+    simplifySubstitutions(rhs, rhsPath);
+
   simplify(lhs, &lhsPath);
   simplify(rhs, &rhsPath);