RequirementMachine: Go back to doing three passes in homotopy reduction

First pass:
- Eliminate rules with unresolved name symbols in LHS
- Eliminate simplified non-conformance rules

Second pass:
- Eliminate non-minimal conformance rules

Third pass:
- Eliminate all other non-conformance rules

If you have a concrete requirement with a non-canonical substitution, like

    A : P, A == G<B.T>

We add an induced rule for the abstract type witness,

    A.T == B.T

This rule has a rewrite path in terms of the previous two rules, but we
want to try to eliminate the other two rules first.

This new ordering ensures we eliminate the simplified rule A == G<B.T> and
compute minimal conformances before we get around to considering A.T == B.T,
which can no longer be eliminated by that point.

If we eliminate A.T == B.T first, we end up with simplified concrete
type and concrete conformance rules which cannot be eliminated:

    A.[concrete: G<B.T>] => A
    A.[concrete: G<B.T> : P] => A

This changes the minimized signature in an incompatible way in two test cases.

In Generics/rdar83308672.swift, the signature becomes equivalent to what the
GSB used to output.

In Generics/sr10532.swift, the GSB would output an invalid signature anyway,
so it doesn't matter.

Author: slavapestov

lib/AST/RequirementMachine/HomotopyReduction.cpp

@@ -335,57 +335,6 @@ bool RewritePath::replaceRuleWithPath(unsigned ruleID,
   return true;
 }
 
-/// Check if a rewrite rule is a candidate for deletion in this pass of the
-/// minimization algorithm.
-bool RewriteSystem::
-isCandidateForDeletion(unsigned ruleID,
-                       const llvm::DenseSet<unsigned> *redundantConformances) const {
-  const auto &rule = getRule(ruleID);
-
-  // We should not find a rule that has already been marked redundant
-  // here; it should have already been replaced with a rewrite path
-  // in all homotopy generators.
-  assert(!rule.isRedundant());
-
-  // Associated type introduction rules are 'permanent'. They're
-  // not worth eliminating since they are re-added every time; it
-  // is better to find other candidates to eliminate in the same
-  // loop instead.
-  if (rule.isPermanent())
-    return false;
-
-  // Other rules involving unresolved name symbols are derived from an
-  // associated type introduction rule together with a conformance rule.
-  // They are eliminated in the first pass.
-  if (rule.getLHS().containsUnresolvedSymbols())
-    return true;
-
-  // Protocol conformance rules are eliminated via a different
-  // algorithm which computes "minimal conformances". This runs between
-  // two passes of homotopy reduction.
-  //
-  // The first pass skips protocol conformance rules.
-  //
-  // The second pass eliminates any protocol conformance rule which is
-  // redundant according to both homotopy reduction and the minimal
-  // conformances algorithm.
-  //
-  // Later on, we verify that any conformance redundant via minimal
-  // conformances was also redundant via homotopy reduction. This
-  // means that the set of minimal conformances is always a superset
-  // (or equal to) of the set of minimal protocol conformance
-  // requirements that homotopy reduction alone would produce.
-  if (rule.isAnyConformanceRule()) {
-    if (!redundantConformances)
-      return false;
-
-    if (!redundantConformances->count(ruleID))
-      return false;
-  }
-
-  return true;
-}
-
 /// Find a rule to delete by looking through all loops for rewrite rules appearing
 /// once in empty context. Returns a redundant rule to delete if one was found,
 /// otherwise returns None.
@@ -401,7 +350,7 @@ isCandidateForDeletion(unsigned ruleID,
 /// \p redundantConformances equal to the set of conformance rules that are
 ///    not minimal conformances.
 Optional<unsigned> RewriteSystem::
-findRuleToDelete(const llvm::DenseSet<unsigned> *redundantConformances,
+findRuleToDelete(llvm::function_ref<bool(unsigned)> isRedundantRuleFn,
                  RewritePath &replacementPath) {
   SmallVector<std::pair<unsigned, unsigned>, 2> redundancyCandidates;
   for (unsigned loopID : indices(Loops)) {
@@ -423,15 +372,28 @@ findRuleToDelete(const llvm::DenseSet<unsigned> *redundantConformances,
 
   for (const auto &pair : redundancyCandidates) {
     unsigned ruleID = pair.second;
-    if (!isCandidateForDeletion(ruleID, redundantConformances))
+    const auto &rule = getRule(ruleID);
+
+    // We should not find a rule that has already been marked redundant
+    // here; it should have already been replaced with a rewrite path
+    // in all homotopy generators.
+    assert(!rule.isRedundant());
+
+    // Associated type introduction rules are 'permanent'. They're
+    // not worth eliminating since they are re-added every time; it
+    // is better to find other candidates to eliminate in the same
+    // loop instead.
+    if (rule.isPermanent())
+      continue;
+
+    if (!isRedundantRuleFn(ruleID))
       continue;
 
     if (!found) {
       found = pair;
       continue;
     }
 
-    const auto &rule = getRule(ruleID);
     const auto &otherRule = getRule(found->second);
 
     // Prefer to delete "less canonical" rules.
@@ -495,10 +457,10 @@ void RewriteSystem::deleteRule(unsigned ruleID,
 }
 
 void RewriteSystem::performHomotopyReduction(
-    const llvm::DenseSet<unsigned> *redundantConformances) {
+    llvm::function_ref<bool(unsigned)> isRedundantRuleFn) {
   while (true) {
     RewritePath replacementPath;
-    auto optRuleID = findRuleToDelete(redundantConformances,
+    auto optRuleID = findRuleToDelete(isRedundantRuleFn,
                                       replacementPath);
 
     // If no redundant rules remain which can be eliminated by this pass, stop.
@@ -524,8 +486,24 @@ void RewriteSystem::minimizeRewriteSystem() {
 
   propagateExplicitBits();
 
-  // First pass: Eliminate all redundant rules that are not conformance rules.
-  performHomotopyReduction(/*redundantConformances=*/nullptr);
+  // First pass:
+  // - Eliminate all simplified non-conformance rules.
+  // - Eliminate all rules with unresolved symbols.
+  performHomotopyReduction([&](unsigned ruleID) -> bool {
+    const auto &rule = getRule(ruleID);
+
+    if (rule.isSimplified() &&
+        !rule.isAnyConformanceRule())
+      return true;
+
+    // Other rules involving unresolved name symbols are derived from an
+    // associated type introduction rule together with a conformance rule.
+    // They are eliminated in the first pass.
+    if (rule.getLHS().containsUnresolvedSymbols())
+      return true;
+
+    return false;
+  });
 
   // Now compute a set of minimal conformances.
   //
@@ -537,8 +515,26 @@ void RewriteSystem::minimizeRewriteSystem() {
   llvm::DenseSet<unsigned> redundantConformances;
   computeMinimalConformances(redundantConformances);
 
-  // Second pass: Eliminate all redundant conformance rules.
-  performHomotopyReduction(/*redundantConformances=*/&redundantConformances);
+  // Second pass: Eliminate all non-minimal conformance rules.
+  performHomotopyReduction([&](unsigned ruleID) -> bool {
+    const auto &rule = getRule(ruleID);
+
+    if (rule.isAnyConformanceRule() &&
+        redundantConformances.count(ruleID))
+      return true;
+
+    return false;
+  });
+
+  // Third pass: Eliminate all other redundant non-conformance rules.
+  performHomotopyReduction([&](unsigned ruleID) -> bool {
+    const auto &rule = getRule(ruleID);
+
+    if (!rule.isAnyConformanceRule())
+      return true;
+
+    return false;
+  });
 
   // Check invariants after homotopy reduction.
   verifyRewriteLoops();

lib/AST/RequirementMachine/RewriteSystem.h

@@ -427,18 +427,14 @@ class RewriteSystem final {
 
   void propagateExplicitBits();
 
-  bool
-  isCandidateForDeletion(unsigned ruleID,
-                         const llvm::DenseSet<unsigned> *redundantConformances) const;
-
   Optional<unsigned>
-  findRuleToDelete(const llvm::DenseSet<unsigned> *redundantConformances,
+  findRuleToDelete(llvm::function_ref<bool(unsigned)> isRedundantRuleFn,
                    RewritePath &replacementPath);
 
   void deleteRule(unsigned ruleID, const RewritePath &replacementPath);
 
   void performHomotopyReduction(
-      const llvm::DenseSet<unsigned> *redundantConformances);
+      llvm::function_ref<bool(unsigned)> isRedundantRuleFn);
 
   void computeMinimalConformances(
       llvm::DenseSet<unsigned> &redundantConformances);

test/Generics/abstract_type_witnesses_in_protocols.swift

@@ -0,0 +1,62 @@
+// RUN: %target-swift-frontend -typecheck %s -debug-generic-signatures -requirement-machine-protocol-signatures=on 2>&1 | %FileCheck %s
+
+protocol P {
+  associatedtype T
+}
+
+struct G<T> : P {}
+
+
+protocol Q {
+  associatedtype A : P
+}
+
+protocol R {}
+
+// CHECK-LABEL: abstract_type_witnesses_in_protocols.(file).Q1@
+// CHECK-NEXT: Requirement signature: <Self where Self : Q, Self.A == G<Self.A.T>, Self.B : P, Self.A.T == Self.B.T>
+
+// GSB: Non-canonical requirement
+protocol Q1 : Q {
+  associatedtype B : P where A == G<B.T>
+}
+
+// CHECK-LABEL: abstract_type_witnesses_in_protocols.(file).Q1a@
+// CHECK-NEXT: Requirement signature: <Self where Self : Q, Self.A == G<Self.A.T>, Self.B : P, Self.A.T : R, Self.A.T == Self.B.T>
+
+// GSB: Missing requirement
+protocol Q1a : Q {
+  associatedtype B : P where A.T : R, A == G<B.T>
+}
+
+// CHECK-LABEL: abstract_type_witnesses_in_protocols.(file).Q1b@
+// CHECK-NEXT: Requirement signature: <Self where Self : Q, Self.A == G<Self.A.T>, Self.B : P, Self.A.T : R, Self.A.T == Self.B.T>
+
+// GSB: Non-canonical requirement
+protocol Q1b : Q {
+  associatedtype B : P where B.T : R, A == G<B.T>
+}
+
+// CHECK-LABEL: abstract_type_witnesses_in_protocols.(file).Q2@
+// CHECK-NEXT: Requirement signature: <Self where Self : Q, Self.A == G<Self.A.T>, Self.B : P, Self.A.T == Self.B.T>
+
+// GSB: Missing requirement
+protocol Q2 : Q {
+  associatedtype B : P where A.T == B.T, A == G<B.T>
+}
+
+// CHECK-LABEL: abstract_type_witnesses_in_protocols.(file).Q3@
+// CHECK-NEXT: Requirement signature: <Self where Self : Q, Self.A == G<Self.A.T>, Self.B : P, Self.A.T == Self.B.T>
+
+// GSB: Unsupported recursive requirement
+protocol Q3 : Q {
+  associatedtype B : P where A == G<A.T>, A.T == B.T
+}
+
+// CHECK-LABEL: abstract_type_witnesses_in_protocols.(file).Q4@
+// CHECK-NEXT: Requirement signature: <Self where Self : Q, Self.A == G<Self.A.T>, Self.B : P, Self.A.T == Self.B.T>
+
+// GSB: Unsupported recursive requirement
+protocol Q4 : Q {
+  associatedtype B : P where A.T == B.T, A == G<A.T>
+}

test/Generics/rdar83308672.swift

@@ -32,25 +32,25 @@ protocol B {
 // we can drop one requirement but not both.
 
 // CHECK: rdar83308672.(file).G1@
-// CHECK-NEXT: Requirement signature: <Self where Self.T : A, Self.T : B>
+// CHECK-NEXT: Requirement signature: <Self where Self.T : A, Self.T.X == Self.T.Y>
 protocol G1 {
   associatedtype T : A where T.X == T.Y
 }
 
 // CHECK: rdar83308672.(file).G2@
-// CHECK-NEXT: Requirement signature: <Self where Self.T : A, Self.T : B>
+// CHECK-NEXT: Requirement signature: <Self where Self.T : A, Self.T.X == Self.T.Y>
 protocol G2 {
   associatedtype T : A where T : B, T.X == T.Y
 }
 
 // CHECK: rdar83308672.(file).G3@
-// CHECK-NEXT: Requirement signature: <Self where Self.T : A, Self.T : B>
+// CHECK-NEXT: Requirement signature: <Self where Self.T : A, Self.T.X == Self.T.Y>
 protocol G3 {
   associatedtype T : A where T.X == T.Y, T : B
 }
 
 // CHECK: rdar83308672.(file).G4@
-// CHECK-NEXT: Requirement signature: <Self where Self.T : A, Self.T : B>
+// CHECK-NEXT: Requirement signature: <Self where Self.T : A, Self.T.X == Self.T.Y>
 protocol G4 {
   associatedtype T : A where T : B
 }

test/Generics/sr10532.swift

@@ -15,7 +15,7 @@ public protocol ScalarMultiplicative {
 public protocol MapReduceArithmetic : ScalarMultiplicative, Collection where Element : ScalarMultiplicative, Scalar == Element.Scalar { }
 
 // CHECK: sr10532.(file).Tensor@
-// CHECK-NEXT: Requirement signature: <Self where Self : MapReduceArithmetic, Self.Element : BinaryFloatingPoint, Self.Element : ScalarProtocol>
+// CHECK-NEXT: Requirement signature: <Self where Self : MapReduceArithmetic, Self.Element : BinaryFloatingPoint, Self.Element == Self.Scalar>
 public protocol Tensor : MapReduceArithmetic where Scalar : BinaryFloatingPoint, Element == Scalar {
   var magnitude: Scalar { get set }
 }