RequirementMachine: New elimination order based on projection count

We want to prefer to eliminate rules that are not concrete type rules,
unless non-concrete type rule in question is a projection. For example,
suppose that this rule comes from a protocol:

    T.T == G<T.U, T.V>

And these three rules are in our minimization domain:

    a) T.T == G<Int, W>
    b) T.U == Int
    c) T.V == W

Then a) implies both b) and c), and vice versa.

In this case, we want to keep T.U == Int and T.V == W, and eliminate
T.T == G<Int, W>.

T.T == G<Int, W> is concrete and T.V == W is not, but because T.V == W
is defined by a projection, we still prefer to eliminate T.T == G<Int, W>
over T.V == W.

Author: slavapestov

lib/AST/RequirementMachine/HomotopyReduction.cpp

@@ -425,26 +425,42 @@ findRuleToDelete(llvm::function_ref<bool(unsigned)> isRedundantRuleFn) {
     // we've found so far.
     const auto &otherRule = getRule(found->second);
 
-    unsigned ruleNesting = rule.getNesting();
-    unsigned otherRuleNesting = otherRule.getNesting();
+    const auto &loop = Loops[pair.first];
+    const auto &otherLoop = Loops[found->first];
 
-    // If both rules are concrete type requirements, first compare nesting
-    // depth. This breaks the tie when we have two rules that each imply
-    // the other via an induced rule that comes from a protocol.
+    // If one of the rules was a concrete unification projection, prefer to
+    // eliminate the *other* rule.
     //
-    // For example,
+    // For example, if 'X.T == G<U, V>' is implied by the conformance on X,
+    // and the following three rules are defined in the current protocol:
     //
-    //    T == G<Int>
-    //    U == Int
+    //    X.T == G<Int, W>
+    //    X.U == Int
+    //    X.V == W
     //
-    // Where T == G<U> is implied elsewhere.
-    if (ruleNesting > 0 && otherRuleNesting > 0) {
-      if (ruleNesting > otherRuleNesting) {
+    // Then we can either eliminate a) alone, or b) and c). Since b) and c)
+    // are projections, they are "simpler", and we would rather keep both and
+    // eliminate a).
+    unsigned projectionCount = loop.getProjectionCount(*this);
+    unsigned otherProjectionCount = otherLoop.getProjectionCount(*this);
+
+    if (projectionCount != otherProjectionCount) {
+      if (projectionCount < otherProjectionCount)
         found = pair;
-        continue;
-      } else if (otherRuleNesting > ruleNesting) {
-        continue;
-      }
+
+      continue;
+    }
+
+    // If one of the rules is a concrete type requirement, prefer to
+    // eliminate the *other* rule.
+    bool ruleIsConcrete = rule.getLHS().back().hasSubstitutions();
+    bool otherRuleIsConcrete = otherRule.getRHS().back().hasSubstitutions();
+
+    if (ruleIsConcrete != otherRuleIsConcrete) {
+      if (otherRuleIsConcrete)
+        found = pair;
+
+      continue;
     }
 
     // Otherwise, perform a shortlex comparison on (LHS, RHS).

test/Generics/concrete_conformance_minimization.swift

@@ -14,4 +14,20 @@ struct G2<T : SIMD> {}
 
 // CHECK-LABEL: ExtensionDecl line={{[0-9]+}} base=G2
 // CHECK-NEXT: Generic signature: <T where T == SIMD2<Double>>
-extension G2 where T == SIMD2<Double> {}
+extension G2 where T == SIMD2<Double> {}
+
+struct G3<T: SIMD> where T.Scalar: FixedWidthInteger & SignedInteger {}
+
+// CHECK-LABEL: ExtensionDecl line={{[0-9]+}} base=G3
+// CHECK-NEXT: Generic signature: <T where T == SIMD2<Int8>>
+extension G3 where T == SIMD2<Int8> {}
+
+struct G4<T : StringProtocol> {}
+
+// CHECK-LABEL: ExtensionDecl line={{[0-9]+}} base=G4
+// CHECK-NEXT: Generic signature: <T where T == String>
+extension G4 where T == String {}
+
+// CHECK-LABEL: ExtensionDecl line={{[0-9]+}} base=G4
+// CHECK-NEXT: Generic signature: <T where T == Substring>
+extension G4 where T == Substring {}

test/Generics/concrete_conformance_rule_simplified.swift

@@ -0,0 +1,33 @@
+// RUN: %target-swift-frontend -typecheck %s -debug-generic-signatures -requirement-machine-inferred-signatures=on 2>&1 | %FileCheck %s
+
+protocol P1 {}
+
+protocol P2 {
+  associatedtype T: P1
+}
+
+protocol P3: P1 {}
+
+protocol P4: P3 {}
+
+protocol P5: P2 {
+  associatedtype U: P5 where U.T: P4
+}
+
+protocol P6: P1 {
+  associatedtype V: P6 & P4
+}
+
+struct C: P6 & P4 {
+  typealias V = C
+}
+
+struct G1<T: P6>: P5 {
+  typealias U = G1<T.V>
+}
+
+struct G2<T: P5> where T.T: P4 {}
+
+// CHECK-LABEL: ExtensionDecl line={{.*}} base=G2
+// CHECK-NEXT: Generic signature: <T where T == G1<C>>
+extension G2 where T == G1<C> {}

test/Generics/concrete_nesting_elimination_order.swift

@@ -0,0 +1,47 @@
+// RUN: %target-swift-frontend -typecheck %s -debug-generic-signatures -requirement-machine-protocol-signatures=verify 2>&1 | %FileCheck %s
+
+protocol P1 {
+  associatedtype T
+}
+
+protocol P2 {}
+
+protocol P3 {
+  associatedtype T : P2, P3
+}
+
+protocol P4 : P3 {}
+
+protocol P5 : P4 {}
+
+struct C : P2, P5 {
+  typealias T = C
+}
+
+struct G<T: P5> : P1 {}
+
+// CHECK-LABEL: concrete_nesting_elimination_order.(file).P6@
+// CHECK-NEXT: Requirement signature: <Self where Self.[P6]X : P1, Self.[P6]Y : P5, Self.[P6]Y == Self.[P6]Z.[P1]T, Self.[P6]Z : P1>
+
+protocol P6 {
+  associatedtype X : P1
+  associatedtype Y : P5
+  associatedtype Z : P1 where Z.T == Y
+}
+
+// CHECK-LABEL: concrete_nesting_elimination_order.(file).P7@
+// CHECK-NEXT: Requirement signature: <Self where Self : P6, Self.[P6]X == G<Self.[P6]Y>, Self.[P6]Z == G<Self.[P6]Y>>
+
+protocol P7 : P6 where X == G<Y>, X == Z {}
+
+// CHECK-LABEL: concrete_nesting_elimination_order.(file).P8a@
+// CHECK-NEXT: Requirement signature: <Self where Self : P7, Self.[P6]Y == C>
+
+protocol P8a : P7 where Y == C {}
+
+// CHECK-LABEL: concrete_nesting_elimination_order.(file).P8b@
+// CHECK-NEXT: Requirement signature: <Self where Self : P7, Self.[P6]Y == C>
+
+protocol P8b : P7 where Y == C {}
+
+// Make sure we pick 'Y == C' and not 'Y == G<C>' here.

test/Generics/concrete_nesting_elimination_order_2.swift

@@ -0,0 +1,44 @@
+// RUN: %target-swift-frontend -typecheck %s -debug-generic-signatures -requirement-machine-protocol-signatures=on 2>&1 | %FileCheck %s
+
+protocol P1 {
+  associatedtype T
+}
+
+protocol P2 {
+  associatedtype X : P2 where X.X == X
+  associatedtype Y : P1 where Y.T == A
+}
+
+struct A : P2 {
+  typealias X = A
+  struct Y : P1 {
+    typealias T = A
+  }
+}
+
+struct B : P2 {
+  typealias X = A
+  struct Y : P1 {
+    typealias T = A
+  }
+}
+
+// CHECK-LABEL: concrete_nesting_elimination_order_2.(file).P3a@
+// CHECK-NEXT: Requirement signature: <Self where Self : P2, Self.[P2]X == A, Self.[P2]Y == B.Y>
+
+protocol P3a : P2 where X == A,     Y == B.Y {}
+
+// CHECK-LABEL: concrete_nesting_elimination_order_2.(file).P3b@
+// CHECK-NEXT: Requirement signature: <Self where Self : P2, Self.[P2]X == A, Self.[P2]Y == B.Y>
+
+protocol P3b : P2 where X == X.Y.T, Y == B.Y {}
+
+// CHECK-LABEL: concrete_nesting_elimination_order_2.(file).P3ab@
+// CHECK-NEXT: Requirement signature: <Self where Self : P2, Self.[P2]X == A, Self.[P2]Y == B.Y>
+
+protocol P3ab : P2 where X == A,     X == X.Y.T, Y == B.Y {}
+
+// CHECK-LABEL: concrete_nesting_elimination_order_2.(file).P3ba@
+// CHECK-NEXT: Requirement signature: <Self where Self : P2, Self.[P2]X == A, Self.[P2]Y == B.Y>
+
+protocol P3ba : P2 where X == X.Y.T, X == A,     Y == B.Y {}