RequirementMachine: Implement minimization for concrete nested type requirements

lib/AST/RequirementMachine/GeneratingConformances.cpp

@@ -137,6 +137,8 @@ void RewriteLoop::findProtocolConformanceRules(
       case RewriteStep::Decompose:
       case RewriteStep::ConcreteConformance:
       case RewriteStep::SuperclassConformance:
+      case RewriteStep::ConcreteTypeWitness:
+      case RewriteStep::SameTypeWitness:
         break;
       }
     }

lib/AST/RequirementMachine/HomotopyReduction.cpp

@@ -92,6 +92,8 @@ RewriteLoop::findRulesAppearingOnceInEmptyContext(
     case RewriteStep::Decompose:
     case RewriteStep::ConcreteConformance:
     case RewriteStep::SuperclassConformance:
+    case RewriteStep::ConcreteTypeWitness:
+    case RewriteStep::SameTypeWitness:
       break;
     }
 
@@ -208,6 +210,8 @@ RewritePath RewritePath::splitCycleAtRule(unsigned ruleID) const {
     case RewriteStep::Decompose:
     case RewriteStep::ConcreteConformance:
     case RewriteStep::SuperclassConformance:
+    case RewriteStep::ConcreteTypeWitness:
+    case RewriteStep::SameTypeWitness:
       break;
     }
 
@@ -306,6 +310,8 @@ bool RewritePath::replaceRuleWithPath(unsigned ruleID,
     case RewriteStep::Decompose:
     case RewriteStep::ConcreteConformance:
     case RewriteStep::SuperclassConformance:
+    case RewriteStep::ConcreteTypeWitness:
+    case RewriteStep::SameTypeWitness:
       newSteps.push_back(step);
       break;
     }

lib/AST/RequirementMachine/PropertyMap.h

@@ -227,8 +227,11 @@ class PropertyMap {
                    SmallVectorImpl<InducedRule> &inducedRules) const;
 
   MutableTerm computeConstraintTermForTypeWitness(
-      Term key, CanType concreteType, CanType typeWitness,
-      const MutableTerm &subjectType, ArrayRef<Term> substitutions) const;
+      Term key, RequirementKind requirementKind,
+      CanType concreteType, CanType typeWitness,
+      const MutableTerm &subjectType,
+      ArrayRef<Term> substitutions,
+      RewritePath &path) const;
 
   void recordConcreteConformanceRule(
     unsigned concreteRuleID,

lib/AST/RequirementMachine/PropertyUnification.cpp

@@ -614,42 +614,63 @@ void PropertyMap::concretizeTypeWitnessInConformance(
 
   MutableTerm constraintType;
 
-  auto simplify = [&](CanType t) -> CanType {
-    return CanType(t.transformRec([&](Type t) -> Optional<Type> {
-      if (!t->isTypeParameter())
-        return None;
-
-      auto term = Context.getRelativeTermForType(t->getCanonicalType(),
-                                                 substitutions);
-      System.simplify(term);
-      return Context.getTypeForTerm(term, { });
-    }));
-  };
-
-  if (simplify(concreteType) == simplify(typeWitness) &&
-      requirementKind == RequirementKind::SameType) {
-    // FIXME: ConcreteTypeInDomainMap should support substitutions so
-    // that we can remove this.
-
-    if (Debug.contains(DebugFlags::ConcretizeNestedTypes)) {
-      llvm::dbgs() << "^^ Type witness is the same as the concrete type\n";
-    }
+  RewritePath path;
 
-    // Add a rule T.[P:A] => T.
-    constraintType = MutableTerm(key);
-  } else {
-    constraintType = computeConstraintTermForTypeWitness(
-        key, concreteType, typeWitness, subjectType,
-        substitutions);
-  }
+  constraintType = computeConstraintTermForTypeWitness(
+      key, requirementKind, concreteType, typeWitness, subjectType,
+      substitutions, path);
 
-  inducedRules.emplace_back(subjectType, constraintType);
+  inducedRules.emplace_back(constraintType, subjectType, path);
   if (Debug.contains(DebugFlags::ConcretizeNestedTypes)) {
     llvm::dbgs() << "^^ Induced rule " << constraintType
                  << " => " << subjectType << "\n";
   }
 }
 
+RewriteSystem::ConcreteTypeWitness::ConcreteTypeWitness(
+    Symbol concreteConformance,
+    Symbol assocType,
+    Symbol concreteType)
+  : ConcreteConformance(concreteConformance),
+    AssocType(assocType),
+    ConcreteType(concreteType) {
+  assert(concreteConformance.getKind() == Symbol::Kind::ConcreteConformance);
+  assert(assocType.getKind() == Symbol::Kind::AssociatedType);
+  assert(concreteType.getKind() == Symbol::Kind::ConcreteType);
+  assert(assocType.getProtocols().size() == 1);
+  assert(assocType.getProtocols()[0] == concreteConformance.getProtocol());
+}
+
+bool swift::rewriting::operator==(
+    const RewriteSystem::ConcreteTypeWitness &lhs,
+    const RewriteSystem::ConcreteTypeWitness &rhs) {
+  return (lhs.ConcreteConformance == rhs.ConcreteConformance &&
+          lhs.AssocType == rhs.AssocType &&
+          lhs.ConcreteType == rhs.ConcreteType);
+}
+
+unsigned RewriteSystem::recordConcreteTypeWitness(
+    RewriteSystem::ConcreteTypeWitness witness) {
+  auto key = std::make_pair(witness.ConcreteConformance,
+                            witness.AssocType);
+  unsigned index = ConcreteTypeWitnesses.size();
+  auto inserted = ConcreteTypeWitnessMap.insert(std::make_pair(key, index));
+
+  if (!inserted.second) {
+    index = inserted.first->second;
+  } else {
+    ConcreteTypeWitnesses.push_back(witness);
+  }
+
+  assert(ConcreteTypeWitnesses[index] == witness);
+  return index;
+}
+
+const RewriteSystem::ConcreteTypeWitness &
+RewriteSystem::getConcreteTypeWitness(unsigned index) const {
+  return ConcreteTypeWitnesses[index];
+}
+
 /// Given the key of a property bag known to have \p concreteType,
 /// together with a \p typeWitness from a conformance on that concrete
 /// type, return the right hand side of a rewrite rule to relate
@@ -675,8 +696,72 @@ void PropertyMap::concretizeTypeWitnessInConformance(
 ///
 ///        T.[P:A] => V
 MutableTerm PropertyMap::computeConstraintTermForTypeWitness(
-    Term key, CanType concreteType, CanType typeWitness,
-    const MutableTerm &subjectType, ArrayRef<Term> substitutions) const {
+    Term key, RequirementKind requirementKind,
+    CanType concreteType, CanType typeWitness,
+    const MutableTerm &subjectType,
+    ArrayRef<Term> substitutions,
+    RewritePath &path) const {
+  // If the type witness is abstract, introduce a same-type requirement
+  // between two type parameters.
+  if (typeWitness->isTypeParameter()) {
+    // The type witness is a type parameter of the form τ_0_n.X.Y...Z,
+    // where 'n' is an index into the substitution array.
+    //
+    // Add a rule:
+    //
+    // T.[concrete: C : P].[P:X] => S[n].X.Y...Z
+    //
+    // Where S[n] is the nth substitution term.
+
+    // FIXME: Record a rewrite path.
+    return Context.getRelativeTermForType(typeWitness, substitutions);
+  }
+
+  // Otherwise the type witness is concrete, but may contain type
+  // parameters in structural position.
+
+  // Compute the concrete type symbol [concrete: C.X].
+  SmallVector<Term, 3> result;
+  auto typeWitnessSchema =
+      remapConcreteSubstitutionSchema(typeWitness, substitutions,
+                                      Context, result);
+  auto typeWitnessSymbol =
+      Symbol::forConcreteType(typeWitnessSchema, result, Context);
+  System.simplifySubstitutions(typeWitnessSymbol);
+
+  auto concreteConformanceSymbol = *(subjectType.end() - 2);
+  auto assocTypeSymbol = *(subjectType.end() - 1);
+
+  RewriteSystem::ConcreteTypeWitness witness(concreteConformanceSymbol,
+                                             assocTypeSymbol,
+                                             typeWitnessSymbol);
+  unsigned witnessID = System.recordConcreteTypeWitness(witness);
+
+  // If it is equal to the parent type, introduce a same-type requirement
+  // between the two parameters.
+  if (requirementKind == RequirementKind::SameType &&
+      typeWitnessSymbol.getConcreteType() == concreteType &&
+      typeWitnessSymbol.getSubstitutions() == substitutions) {
+    // FIXME: ConcreteTypeInDomainMap should support substitutions so
+    // that we can remove this.
+
+    if (Debug.contains(DebugFlags::ConcretizeNestedTypes)) {
+      llvm::dbgs() << "^^ Type witness is the same as the concrete type\n";
+    }
+
+    // Add a rule T.[concrete: C : P].[P:X] => T.[concrete: C : P].
+    MutableTerm result(key);
+    result.add(concreteConformanceSymbol);
+
+    path.add(RewriteStep::forSameTypeWitness(
+        witnessID, /*inverse=*/true));
+
+    return result;
+  }
+
+  // If the type witness is completely concrete, try to introduce a
+  // same-type requirement with another representative type parameter,
+  // if we have one.
   if (!typeWitness->hasTypeParameter()) {
     // Check if we have a shorter representative we can use.
     auto domain = key.getRootProtocols();
@@ -690,38 +775,23 @@ MutableTerm PropertyMap::computeConstraintTermForTypeWitness(
           llvm::dbgs() << "^^ Type witness can re-use property bag of "
                        << found->second << "\n";
         }
+
+        // FIXME: Record a rewrite path.
         return result;
       }
     }
   }
 
-  if (typeWitness->isTypeParameter()) {
-    // The type witness is a type parameter of the form τ_0_n.X.Y...Z,
-    // where 'n' is an index into the substitution array.
-    //
-    // Add a rule:
-    //
-    // T.[concrete: C : P].[P:X] => S[n].X.Y...Z
-    //
-    // Where S[n] is the nth substitution term.
-    return Context.getRelativeTermForType(typeWitness, substitutions);
-  }
-
-  // The type witness is a concrete type.
+  // Otherwise, add a concrete type requirement for the type witness.
   //
   // Add a rule:
   //
-  // T.[concrete: C : P].[P:X].[concrete: Foo.A] => T.[concrete: C : P].[P:A].
+  // T.[concrete: C : P].[P:X].[concrete: C.X] => T.[concrete: C : P].[P:X].
   MutableTerm constraintType = subjectType;
+  constraintType.add(typeWitnessSymbol);
 
-  SmallVector<Term, 3> result;
-  auto typeWitnessSchema =
-      remapConcreteSubstitutionSchema(typeWitness, substitutions,
-                                      Context, result);
-
-  constraintType.add(
-      Symbol::forConcreteType(
-          typeWitnessSchema, result, Context));
+  path.add(RewriteStep::forConcreteTypeWitness(
+      witnessID, /*inverse=*/false));
 
   return constraintType;
 }

lib/AST/RequirementMachine/RequirementMachineRequests.cpp

@@ -79,7 +79,9 @@ void ConnectedComponent::buildRequirements(Type subjectType,
                         subjectType, constraintType);
       subjectType = constraintType;
     }
-  } else {
+  } else if (!ConcreteType->hasError()) {
+    // For compatibility with the old GenericSignatureBuilder, drop requirements
+    // containing ErrorTypes.
     reqs.emplace_back(RequirementKind::SameType,
                       subjectType, ConcreteType);
 
@@ -120,14 +122,20 @@ RequirementMachine::buildRequirementsFromRules(
                           prop->getLayoutConstraint());
         return;
 
-      case Symbol::Kind::Superclass:
+      case Symbol::Kind::Superclass: {
+        // For compatibility with the old GenericSignatureBuilder, drop requirements
+        // containing ErrorTypes.
+        auto superclassType = Context.getTypeFromSubstitutionSchema(
+                                prop->getSuperclass(),
+                                prop->getSubstitutions(),
+                                genericParams, MutableTerm());
+        if (superclassType->hasError())
+          return;
+
         reqs.emplace_back(RequirementKind::Superclass,
-                          subjectType,
-                          Context.getTypeFromSubstitutionSchema(
-                              prop->getSuperclass(),
-                              prop->getSubstitutions(),
-                              genericParams, MutableTerm()));
+                          subjectType, superclassType);
         return;
+      }
 
       case Symbol::Kind::ConcreteType: {
         auto concreteType = Context.getTypeFromSubstitutionSchema(