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.

Author: slavapestov

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);
 

lib/AST/RequirementMachine/RewriteSystem.h

@@ -323,6 +323,11 @@ class RewritePath {
     Steps.append(other.begin(), other.end());
   }
 
+  void resize(unsigned newSize) {
+    assert(newSize <= size());
+    Steps.erase(Steps.begin() + newSize, Steps.end());
+  }
+
   decltype(Steps)::const_iterator begin() const {
     return Steps.begin();
   }
@@ -495,6 +500,8 @@ class RewriteSystem final {
 
   bool simplify(MutableTerm &term, RewritePath *path=nullptr) const;
 
+  void simplifySubstitutions(MutableTerm &term, RewritePath &path) const;
+
   //////////////////////////////////////////////////////////////////////////////
   ///
   /// Completion

test/Generics/simplify_concrete_substitutions.swift

@@ -0,0 +1,27 @@
+// RUN: %target-swift-frontend -typecheck %s -debug-generic-signatures -requirement-machine-protocol-signatures=on 2>&1 | %FileCheck %s
+
+// The rule
+//
+//   [P:Y].[concrete: G<τ_0_0, τ_0_1> with <[P:Z1], [P:Z2]>] => [P:Y]
+//
+// overlaps with [P].[P:Y] => [P], which applies the adjustment prepending
+// [P] to [P:Z1] and [P:Z2], respectively.
+//
+// This produces the rule
+//
+//   [P:Y].[concrete: G<τ_0_0, τ_0_1> with <[P].[P:Z1], [P].[P:Z2]>] => [P:Y]
+//
+// When adding the rule, we have to simplify the concrete substitutions to
+// reduce [P].[P:Z1] to [P:Z1] and [P].[P:Z2] to [P:Z2], respectively.
+
+// CHECK-LABEL: simplify_concrete_substitutions.(file).P@
+// CHECK-LABEL: Requirement signature: <Self where Self == Self.X.X, Self.X : P, Self.Y == G<Self.Z1, Self.Z2>>
+
+protocol P {
+  associatedtype X : P where X.X == Self
+  associatedtype Y where Y == G<Z1, Z2>
+  associatedtype Z1
+  associatedtype Z2
+}
+
+struct G<T, U> {}