RequirementMachine: Preserve replacement paths for redundant rules

lib/AST/RequirementMachine/Debug.h

@@ -59,6 +59,12 @@ enum class DebugFlags : unsigned {
 
   /// Print debug output from generic signature minimization.
   Minimization = (1<<12),
+
+  /// Print redundant rules and their replacement paths.
+  RedundantRules = (1<<13),
+
+  /// Print more detail about redundant rules.
+  RedundantRulesDetail = (1<<14)
 };
 
 using DebugOptions = OptionSet<DebugFlags>;

lib/AST/RequirementMachine/HomotopyReduction.cpp

@@ -420,11 +420,17 @@ findRuleToDelete(llvm::function_ref<bool(unsigned)> isRedundantRuleFn) {
     // Homotopy reduction runs multiple passes with different filters to
     // prioritize the deletion of certain rules ahead of others. Apply
     // the filter now.
-    if (!isRedundantRuleFn(ruleID))
+    if (!isRedundantRuleFn(ruleID)) {
+      if (Debug.contains(DebugFlags::HomotopyReductionDetail)) {
+        llvm::dbgs() << "** Skipping rule " << rule << " from loop #"
+                     << pair.first << "\n";
+      }
+
       continue;
+    }
 
     if (Debug.contains(DebugFlags::HomotopyReductionDetail)) {
-      llvm::dbgs() << "** Candidate " << rule << " from loop #"
+      llvm::dbgs() << "** Candidate rule " << rule << " from loop #"
                    << pair.first << "\n";
     }
 
@@ -552,6 +558,12 @@ findRuleToDelete(llvm::function_ref<bool(unsigned)> isRedundantRuleFn) {
 /// occurrences of the rule in all loops with the replacement path.
 void RewriteSystem::deleteRule(unsigned ruleID,
                                const RewritePath &replacementPath) {
+  // Replace all occurrences of the rule with the replacement path in
+  // all redundant rule paths recorded so far.
+  for (auto &pair : RedundantRules) {
+    (void) pair.second.replaceRuleWithPath(ruleID, replacementPath);
+  }
+
   // Replace all occurrences of the rule with the replacement path in
   // all remaining rewrite loops.
   for (unsigned loopID : indices(Loops)) {
@@ -573,6 +585,9 @@ void RewriteSystem::deleteRule(unsigned ruleID,
       llvm::dbgs() << "\n";
     }
   }
+
+  // Record the redundant rule along with its replacement path.
+  RedundantRules.emplace_back(ruleID, replacementPath);
 }
 
 void RewriteSystem::performHomotopyReduction(
@@ -702,6 +717,26 @@ void RewriteSystem::minimizeRewriteSystem() {
   verifyRewriteLoops();
   verifyRedundantConformances(redundantConformances);
   verifyMinimizedRules(redundantConformances);
+
+  if (Debug.contains(DebugFlags::RedundantRules)) {
+    llvm::dbgs() << "\nRedundant rules:\n";
+    for (const auto &pair : RedundantRules) {
+      const auto &rule = getRule(pair.first);
+      llvm::dbgs() << "- " << rule << " ::== ";
+
+      MutableTerm lhs(rule.getLHS());
+      pair.second.dump(llvm::dbgs(), lhs, *this);
+
+      llvm::dbgs() << "\n";
+
+      if (Debug.contains(DebugFlags::RedundantRulesDetail)) {
+        llvm::dbgs() << "\n";
+        pair.second.dumpLong(llvm::dbgs(), lhs, *this);
+
+        llvm::dbgs() << "\n\n";
+      }
+    }
+  }
 }
 
 /// In a conformance-valid rewrite system, any rule with unresolved symbols on
@@ -826,6 +861,8 @@ void RewriteSystem::verifyRedundantConformances(
 void RewriteSystem::verifyMinimizedRules(
     const llvm::DenseSet<unsigned> &redundantConformances) const {
 #ifndef NDEBUG
+  unsigned redundantRuleCount = 0;
+
   for (unsigned ruleID : indices(Rules)) {
     const auto &rule = getRule(ruleID);
 
@@ -845,8 +882,11 @@ void RewriteSystem::verifyMinimizedRules(
       continue;
     }
 
+    if (rule.isRedundant())
+      ++redundantRuleCount;
+
     // LHS-simplified rules should be redundant, unless they're protocol
-    // conformance rules, which unfortunately might no be redundant, because
+    // conformance rules, which unfortunately might not be redundant, because
     // we try to keep them in the original protocol definition for
     // compatibility with the GenericSignatureBuilder's minimization algorithm.
     if (rule.isLHSSimplified() &&
@@ -877,5 +917,22 @@ void RewriteSystem::verifyMinimizedRules(
       abort();
     }
   }
+
+  if (RedundantRules.size() != redundantRuleCount) {
+    llvm::errs() << "Expected " << RedundantRules.size() << " redundant rules "
+                 << "but counted " << redundantRuleCount << "\n";
+    dump(llvm::errs());
+    abort();
+  }
+
+  for (const auto &pair : RedundantRules) {
+    const auto &rule = getRule(pair.first);
+    if (!rule.isRedundant()) {
+      llvm::errs() << "Recorded replacement path for non-redundant rule "
+                   << rule << "\n";
+      dump(llvm::errs());
+      abort();
+    }
+  }
 #endif
 }

lib/AST/RequirementMachine/PropertyUnification.cpp

@@ -269,14 +269,14 @@ void PropertyMap::addSuperclassProperty(
     recordRelation(key, ruleID, layoutSymbol, System, debug);
   }
 
-  if (debug) {
-    llvm::dbgs() << "% New superclass " << superclassDecl->getName()
-                 << " for " << key << " is ";
-  }
-
   // If this is the first superclass requirement we've seen for this term,
   // just record it and we're done.
   if (!props->SuperclassDecl) {
+    if (debug) {
+      llvm::dbgs() << "% New superclass " << superclassDecl->getName()
+                   << " for " << key << "\n";
+    }
+
     props->SuperclassDecl = superclassDecl;
 
     assert(props->Superclasses.empty());
@@ -290,6 +290,11 @@ void PropertyMap::addSuperclassProperty(
     return;
   }
 
+  if (debug) {
+    llvm::dbgs() << "% New superclass " << superclassDecl->getName()
+                 << " for " << key << " is ";
+  }
+
   // Otherwise, we compare it against the existing superclass requirement.
   assert(!props->Superclasses.empty());
 

lib/AST/RequirementMachine/RewriteContext.cpp

@@ -40,6 +40,8 @@ static DebugOptions parseDebugFlags(StringRef debugFlags) {
       .Case("minimal-conformances", DebugFlags::MinimalConformances)
       .Case("protocol-dependencies", DebugFlags::ProtocolDependencies)
       .Case("minimization", DebugFlags::Minimization)
+      .Case("redundant-rules", DebugFlags::RedundantRules)
+      .Case("redundant-rules-detail", DebugFlags::RedundantRulesDetail)
       .Default(None);
     if (!flag) {
       llvm::errs() << "Unknown debug flag in -debug-requirement-machine "

lib/AST/RequirementMachine/RewriteLoop.cpp

@@ -188,6 +188,20 @@ void RewritePath::dump(llvm::raw_ostream &out,
   }
 }
 
+void RewritePath::dumpLong(llvm::raw_ostream &out,
+                           MutableTerm term,
+                           const RewriteSystem &system) const {
+  RewritePathEvaluator evaluator(term);
+
+  for (const auto &step : Steps) {
+    evaluator.dump(out);
+    evaluator.apply(step, system);
+    out << "\n";
+  }
+
+  evaluator.dump(out);
+}
+
 void RewriteLoop::verify(const RewriteSystem &system) const {
 #ifndef NDEBUG
   RewritePathEvaluator evaluator(Basepoint);
@@ -220,13 +234,17 @@ void RewriteLoop::dump(llvm::raw_ostream &out,
 }
 
 void RewritePathEvaluator::dump(llvm::raw_ostream &out) const {
-  out << "Primary stack:\n";
-  for (const auto &term : Primary) {
-    out << term << "\n";
+  for (unsigned i = 0, e = Primary.size(); i < e; ++i) {
+    if (i == Primary.size() - 1)
+      out << "-> ";
+    else
+      out << "   ";
+
+    out << Primary[i] << "\n";
   }
-  out << "\nSecondary stack:\n";
-  for (const auto &term : Secondary) {
-    out << term << "\n";
+
+  for (unsigned i = 0, e = Secondary.size(); i < e; ++i) {
+    out << "   " << Secondary[Secondary.size() - i - 1] << "\n";
   }
 }
 

lib/AST/RequirementMachine/RewriteLoop.h

@@ -409,6 +409,10 @@ class RewritePath {
   void dump(llvm::raw_ostream &out,
             MutableTerm term,
             const RewriteSystem &system) const;
+
+  void dumpLong(llvm::raw_ostream &out,
+                MutableTerm term,
+                const RewriteSystem &system) const;
 };
 
 /// Information about protocol conformance rules appearing in a rewrite loop.

lib/AST/RequirementMachine/RewriteSystem.h

@@ -453,6 +453,10 @@ class RewriteSystem final {
   /// algorithms.
   std::vector<RewriteLoop> Loops;
 
+  /// A list of pairs where the first element is a rule number and the second
+  /// element is an equivalent rewrite path in terms of non-redundant rules.
+  std::vector<std::pair<unsigned, RewritePath>> RedundantRules;
+
   void propagateExplicitBits();
 
   Optional<std::pair<unsigned, unsigned>>

lib/AST/RequirementMachine/Symbol.cpp

@@ -637,23 +637,25 @@ Symbol Symbol::transformConcreteSubstitutions(
 
 /// Print the symbol using our mnemonic representation.
 void Symbol::dump(llvm::raw_ostream &out) const {
-  auto dumpSubstitutions = [&]() {
-    if (getSubstitutions().size() > 0) {
-      out << " with <";
-
-      bool first = true;
-      for (auto substitution : getSubstitutions()) {
-        if (first) {
-          first = false;
-        } else {
-          out << ", ";
-        }
-        substitution.dump(out);
-      }
+  llvm::DenseMap<CanType, Identifier> substitutionNames;
+  if (hasSubstitutions()) {
+    auto &ctx = getConcreteType()->getASTContext();
+
+    for (unsigned index : indices(getSubstitutions())) {
+      Term substitution = getSubstitutions()[index];
+
+      std::string s;
+      llvm::raw_string_ostream os(s);
+      os << substitution;
 
-      out << ">";
+      auto key = CanType(GenericTypeParamType::get(
+          /*isTypeSequence=*/false, 0, index, ctx));
+      substitutionNames[key] = ctx.getIdentifier(s);
     }
-  };
+  }
+
+  PrintOptions opts;
+  opts.AlternativeTypeNames = &substitutionNames;
 
   switch (getKind()) {
   case Kind::Name:
@@ -680,20 +682,20 @@ void Symbol::dump(llvm::raw_ostream &out) const {
     return;
 
   case Kind::Superclass:
-    out << "[superclass: " << getConcreteType();
-    dumpSubstitutions();
+    out << "[superclass: ";
+    getConcreteType().print(out, opts);
     out << "]";
     return;
 
   case Kind::ConcreteType:
-    out << "[concrete: " << getConcreteType();
-    dumpSubstitutions();
+    out << "[concrete: ";
+    getConcreteType().print(out, opts);
     out << "]";
     return;
 
   case Kind::ConcreteConformance:
-    out << "[concrete: " << getConcreteType();
-    dumpSubstitutions();
+    out << "[concrete: ";
+    getConcreteType().print(out, opts);
     out << " : ";
     out << getProtocol()->getName();
     out << "]";

test/Generics/generic_objc_superclass.swift

@@ -13,9 +13,9 @@ func foo<T : Generic<U>, U>(_: T, _: U) {
 
 // CHECK-LABEL: Requirement machine for <τ_0_0, τ_0_1 where τ_0_0 : Generic<τ_0_1>>
 // CHECK-NEXT: Rewrite system: {
-// CHECK-NEXT: - τ_0_0.[superclass: Generic<τ_0_0> with <τ_0_1>] => τ_0_0
+// CHECK-NEXT: - τ_0_0.[superclass: Generic<τ_0_1>] => τ_0_0
 // CHECK-NEXT: - τ_0_0.[layout: AnyObject] => τ_0_0
 // CHECK-NEXT: }
 // CHECK: Property map: {
-// CHECK-NEXT:   τ_0_0 => { layout: AnyObject superclass: [superclass: Generic<τ_0_0> with <τ_0_1>] }
+// CHECK-NEXT:   τ_0_0 => { layout: AnyObject superclass: [superclass: Generic<τ_0_1>] }
 // CHECK-NEXT: }

test/Generics/infinite_concrete_type.swift

@@ -3,7 +3,7 @@
 class G<T> {}
 
 protocol P1 { // expected-error {{cannot build rewrite system for protocol; concrete nesting limit exceeded}}
-// expected-note@-1 {{failed rewrite rule is [P1:A].[concrete: G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<τ_0_0>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> with <[P1:A]>] => [P1:A]}}
+// expected-note@-1 {{failed rewrite rule is [P1:A].[concrete: G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<[P1:A]>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>] => [P1:A]}}
   associatedtype A where A == G<B>
   associatedtype B where B == G<A>
 }

test/Generics/non_confluent.swift

@@ -45,7 +45,7 @@ struct S<U : P1> : P1 {
 
 protocol P3 {
 // expected-error@-1 {{cannot build rewrite system for protocol; rule length limit exceeded}}
-// expected-note@-2 {{failed rewrite rule is [P3:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[concrete: S<S<S<S<S<S<S<S<S<S<S<S<τ_0_0>>>>>>>>>>>> with <[P3:U]>] => [P3:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T]}}
+// expected-note@-2 {{failed rewrite rule is [P3:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[concrete: S<S<S<S<S<S<S<S<S<S<S<S<[P3:U]>>>>>>>>>>>>] => [P3:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T]}}
 
   associatedtype T : P1 where T == S<U>
 // expected-error@-1 {{type 'Self.U' does not conform to protocol 'P1'}}

test/Generics/sr12531.swift

@@ -1,4 +1,4 @@
-// RUN: %target-typecheck-verify-swift
+// RUN: %target-typecheck-verify-swift -requirement-machine-protocol-signatures=verify -requirement-machine-inferred-signatures=verify
 
 protocol AnyPropertyProtocol {
     associatedtype Root = Any
@@ -8,15 +8,21 @@ protocol AnyPropertyProtocol {
     var value: Value { get }
 }
 
+// CHECK-LABEL: .PartialPropertyProtocol@
+// CHECK-NEXT: Requirement signature: <Self where Self : AnyPropertyProtocol, Self.[AnyPropertyProtocol]KP : PartialKeyPath<Self.[AnyPropertyProtocol]Root>
 protocol PartialPropertyProtocol: AnyPropertyProtocol
 where KP: PartialKeyPath<Root> {
 }
 
+// CHECK-LABEL: .PropertyProtocol@
+// CHECK-NEXT: Requirement signature: <Self where Self : PartialPropertyProtocol, Self.[AnyPropertyProtocol]KP : WritableKeyPath<Self.[AnyPropertyProtocol]Root, Self.[AnyPropertyProtocol]Value>
 protocol PropertyProtocol: PartialPropertyProtocol
 where KP: WritableKeyPath<Root, Value> {
 }
 
 extension Dictionary where Value: AnyPropertyProtocol {
+    // CHECK-LABEL: .subscript@
+    // CHECK-NEXT: Generic signature: <R, V, P where P : PropertyProtocol, P.[AnyPropertyProtocol]Root == R, P.[AnyPropertyProtocol]Value == V>
     subscript<R, V, P>(key: Key, path: WritableKeyPath<R, V>) -> P? where P: PropertyProtocol, P.Root == R, P.Value == V {
         return self[key] as? P
     }

test/Generics/unify_concrete_types_1.swift

@@ -25,7 +25,7 @@ struct MergeTest<G : P1 & P2> {
 // CHECK: - τ_0_0.[P2:Z2] => τ_0_0.[P1:Z1]
 // CHECK: }
 // CHECK-LABEL: Property map: {
-// CHECK:  [P1:X] => { concrete_type: [concrete: Foo<τ_0_0, τ_0_1> with <[P1:Y1], [P1:Z1]>] }
-// CHECK:  [P2:X] => { concrete_type: [concrete: Foo<τ_0_0, τ_0_1> with <[P2:Y2], [P2:Z2]>] }
+// CHECK:  [P1:X] => { concrete_type: [concrete: Foo<[P1:Y1], [P1:Z1]>] }
+// CHECK:  [P2:X] => { concrete_type: [concrete: Foo<[P2:Y2], [P2:Z2]>] }
 // CHECK:  τ_0_0 => { conforms_to: [P1 P2] }
 // CHECK: }

test/Generics/unify_nested_types_2.swift

@@ -25,7 +25,7 @@ struct G<T : P1 & P2> {}
 // CHECK-LABEL: Adding generic signature <τ_0_0 where τ_0_0 : P1, τ_0_0 : P2> {
 // CHECK-LABEL: Rewrite system: {
 // CHECK: - [P1:T].T => [P1:T].[P1:T]
-// CHECK: - τ_0_0.[P1:T].[concrete: X<τ_0_0> with <τ_0_0.[P2:U]>] => τ_0_0.[P1:T]
+// CHECK: - τ_0_0.[P1:T].[concrete: X<τ_0_0.[P2:U]>] => τ_0_0.[P1:T]
 // CHECK: - τ_0_0.[P1:T].[P1:T] => τ_0_0.[P1:T]
 // CHECK: }
 // CHECK: }

test/Generics/unify_nested_types_3.swift

@@ -28,11 +28,11 @@ struct G<T : P2a & P3a> {}
 
 // CHECK-LABEL: Requirement machine for <τ_0_0 where τ_0_0 : P2a, τ_0_0 : P3a>
 // CHECK-LABEL: Rewrite system: {
-// CHECK: - τ_0_0.[P2a:T].[concrete: X<τ_0_0> with <τ_0_0.[P3a:U]>] => τ_0_0.[P2a:T]
-// CHECK: - τ_0_0.[P2a:T].[P2:T].[concrete: X<τ_0_0> with <τ_0_0.[P3a:U].[P1:T]>] => τ_0_0.[P2a:T].[P2:T]
+// CHECK: - τ_0_0.[P2a:T].[concrete: X<τ_0_0.[P3a:U]>] => τ_0_0.[P2a:T]
+// CHECK: - τ_0_0.[P2a:T].[P2:T].[concrete: X<τ_0_0.[P3a:U].[P1:T]>] => τ_0_0.[P2a:T].[P2:T]
 // CHECK: }
 // CHECK-LABEL: Property map: {
-// CHECK: τ_0_0.[P2a:T] => { conforms_to: [P2] concrete_type: [concrete: X<τ_0_0> with <τ_0_0.[P3a:U]>] }
-// CHECK: τ_0_0.[P2a:T].[P2:T] => { concrete_type: [concrete: X<τ_0_0> with <τ_0_0.[P3a:U].[P1:T]>] }
+// CHECK: τ_0_0.[P2a:T] => { conforms_to: [P2] concrete_type: [concrete: X<τ_0_0.[P3a:U]>] }
+// CHECK: τ_0_0.[P2a:T].[P2:T] => { concrete_type: [concrete: X<τ_0_0.[P3a:U].[P1:T]>] }
 // CHECK: }
 // CHECK: }