RequirementMachine: Two more fixes for -requirement-machine-protocol-signatures=verify

lib/AST/RequirementMachine/PropertyMap.cpp

@@ -304,7 +304,6 @@ void PropertyMap::clear() {
 
   Trie.clear();
   Entries.clear();
-  ConcreteTypeInDomainMap.clear();
 }
 
 /// Build the property map from all rules of the form T.[p] => T, where
@@ -340,7 +339,11 @@ PropertyMap::buildPropertyMap(unsigned maxIterations,
     if (rule.isSimplified())
       continue;
 
-    if (rule.isPermanent())
+    // Identity conformances ([P].[P] => [P]) are permanent rules, but we
+    // keep them around to ensure that concrete conformance introduction
+    // works in the case where the protocol's Self type is itself subject
+    // to a superclass or concrete type requirement.
+    if (rule.isPermanent() && !rule.isIdentityConformanceRule())
       continue;
 
     // Collect all rules of the form T.[p] => T where T is canonical.
@@ -371,10 +374,6 @@ PropertyMap::buildPropertyMap(unsigned maxIterations,
   // Now, check for conflicts between superclass and concrete type rules.
   checkConcreteTypeRequirements(inducedRules);
 
-  // We collect terms with fully concrete types so that we can re-use them
-  // to tie off recursion in the next step.
-  computeConcreteTypeInDomainMap();
-
   // Now, we merge concrete type rules with conformance rules, by adding
   // relations between associated type members of type parameters with
   // the concrete type witnesses in the concrete type's conformance.

lib/AST/RequirementMachine/PropertyMap.h

@@ -117,7 +117,7 @@ class PropertyBag {
     return Superclass.hasValue();
   }
 
-  Type getSuperclassBound() const {
+  CanType getSuperclassBound() const {
     return Superclass->getSuperclass();
   }
 
@@ -130,7 +130,7 @@ class PropertyBag {
     return ConcreteType.hasValue();
   }
 
-  Type getConcreteType() const {
+  CanType getConcreteType() const {
     return ConcreteType->getConcreteType();
   }
 
@@ -165,9 +165,6 @@ class PropertyMap {
   std::vector<PropertyBag *> Entries;
   Trie<PropertyBag *, MatchKind::Longest> Trie;
 
-  using ConcreteTypeInDomain = std::pair<CanType, ArrayRef<const ProtocolDecl *>>;
-  llvm::DenseMap<ConcreteTypeInDomain, Term> ConcreteTypeInDomainMap;
-
   // Building the property map introduces new induced rules, which
   // runs another round of Knuth-Bendix completion, which rebuilds the
   // property map again.
@@ -235,7 +232,6 @@ class PropertyMap {
   void checkConcreteTypeRequirements(
                    SmallVectorImpl<InducedRule> &inducedRules);
 
-  void computeConcreteTypeInDomainMap();
   void concretizeNestedTypesFromConcreteParents(
                    SmallVectorImpl<InducedRule> &inducedRules);
 

lib/AST/RequirementMachine/PropertyUnification.cpp

@@ -578,33 +578,6 @@ void PropertyMap::checkConcreteTypeRequirements(
   }
 }
 
-/// For each fully-concrete type, find the shortest term having that concrete type.
-/// This is later used by computeConstraintTermForTypeWitness().
-void PropertyMap::computeConcreteTypeInDomainMap() {
-  for (auto *props : Entries) {
-    if (!props->isConcreteType())
-      continue;
-
-    auto concreteType = props->ConcreteType->getConcreteType();
-    if (concreteType->hasTypeParameter())
-      continue;
-
-    assert(props->ConcreteType->getSubstitutions().empty());
-
-    auto domain = props->Key.getRootProtocols();
-    auto concreteTypeKey = std::make_pair(concreteType, domain);
-
-    auto found = ConcreteTypeInDomainMap.find(concreteTypeKey);
-    if (found != ConcreteTypeInDomainMap.end())
-      continue;
-
-    auto inserted = ConcreteTypeInDomainMap.insert(
-        std::make_pair(concreteTypeKey, props->Key));
-    assert(inserted.second);
-    (void) inserted;
-  }
-}
-
 void PropertyMap::concretizeNestedTypesFromConcreteParents(
     SmallVectorImpl<InducedRule> &inducedRules) {
   for (auto *props : Entries) {
@@ -945,6 +918,39 @@ MutableTerm PropertyMap::computeConstraintTermForTypeWitness(
     return result;
   }
 
+  // If the type witness is completely concrete, check if one of our prefix
+  // types has the same concrete type, and if so, introduce a same-type
+  // requirement between the subject type and the prefix.
+  if (!typeWitness->hasTypeParameter()) {
+    auto begin = key.begin();
+    auto end = key.end();
+
+    while (begin != end) {
+      MutableTerm prefix(begin, end);
+      if (auto *props = lookUpProperties(prefix)) {
+        if (props->isConcreteType() &&
+            props->getConcreteType() == typeWitness) {
+          auto result = props->getKey();
+
+          RewriteSystem::TypeWitness witness(Term::get(subjectType, Context),
+                                             result);
+          unsigned witnessID = System.recordTypeWitness(witness);
+          path.add(RewriteStep::forAbstractTypeWitness(
+              witnessID, /*inverse=*/false));
+
+          if (Debug.contains(DebugFlags::ConcretizeNestedTypes)) {
+             llvm::dbgs() << "^^ Type witness can re-use property bag of "
+                          << result << "\n";
+          }
+
+          return MutableTerm(result);
+        }
+      }
+
+      --end;
+    }
+  }
+
   // Otherwise the type witness is concrete, but may contain type
   // parameters in structural position.
 
@@ -970,9 +976,6 @@ MutableTerm PropertyMap::computeConstraintTermForTypeWitness(
   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";
     }
@@ -995,29 +998,6 @@ MutableTerm PropertyMap::computeConstraintTermForTypeWitness(
     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();
-    auto concreteTypeKey = std::make_pair(typeWitness, domain);
-
-    auto found = ConcreteTypeInDomainMap.find(concreteTypeKey);
-    if (found != ConcreteTypeInDomainMap.end()) {
-      MutableTerm result(found->second);
-      if (result != subjectType) {
-        if (Debug.contains(DebugFlags::ConcretizeNestedTypes)) {
-          llvm::dbgs() << "^^ Type witness can re-use property bag of "
-                       << found->second << "\n";
-        }
-
-        // FIXME: Record a rewrite path.
-        return result;
-      }
-    }
-  }
-
   // Otherwise, add a concrete type requirement for the type witness.
   //
   // Add a rule:

lib/AST/RequirementMachine/RequirementLowering.cpp

@@ -1003,6 +1003,7 @@ void RuleBuilder::collectRulesFromReferencedProtocols() {
       llvm::dbgs() << "protocol " << proto->getName() << " {\n";
     }
 
+    // Add the identity conformance rule [P].[P] => [P].
     MutableTerm lhs;
     lhs.add(Symbol::forProtocol(proto, Context));
     lhs.add(Symbol::forProtocol(proto, Context));

test/Generics/circular_protocol_superclass.swift

@@ -0,0 +1,11 @@
+// RUN: not %target-swift-frontend -typecheck %s -debug-generic-signatures -requirement-machine-protocol-signatures=on 2>&1 | %FileCheck %s
+
+// CHECK-LABEL: circular_protocol_superclass.(file).A@
+// CHECK-NEXT: Requirement signature: <Self where Self : a>
+protocol A : a {
+  associatedtype e : a
+}
+
+class a : A {
+  typealias e = a
+}

test/Generics/rdar79564324.swift

@@ -38,6 +38,7 @@ public func test<T : P>(_ t: T) where T == T.A {
 // CHECK-NEXT: Rewrite loops: {
 // CHECK:      }
 // CHECK-NEXT: Property map: {
+// CHECK-NEXT:   [P] => { conforms_to: [P] }
 // CHECK-NEXT:   [P:A] => { conforms_to: [P] }
 // CHECK-NEXT:   τ_0_1 => { conforms_to: [P] }
 // CHECK-NEXT:   τ_0_0 => { conforms_to: [P] }

test/Generics/unify_nested_types_4.swift

@@ -37,20 +37,28 @@ struct G<T : P1 & P2> {}
 // we solve this by merging the repeated types with T.A or T.B:
 //
 // T.A.A => T.A
-// T.A.B => T.B
 // T.B.A => T.B
-// T.B.B => T.A
 // ...
 
 // CHECK-LABEL: Requirement machine for <τ_0_0 where τ_0_0 : P1, τ_0_0 : P2>
 // CHECK-LABEL: Rewrite system: {
+// CHECK: - τ_0_0.[P1&P2:A].[concrete: S1 : P1] => τ_0_0.[P1&P2:A]
 // CHECK: - τ_0_0.[P1&P2:A].[P1:A] => τ_0_0.[P1&P2:A]
-// CHECK: - τ_0_0.[P1&P2:A].[P1:B] => τ_0_0.[P1&P2:B]
+// CHECK: - τ_0_0.[P1&P2:A].[P1:B].[concrete: S2] => τ_0_0.[P1&P2:A].[P1:B]
+// CHECK: - τ_0_0.[P1&P2:B].[concrete: S2 : P1] => τ_0_0.[P1&P2:B]
 // CHECK: - τ_0_0.[P1&P2:B].[P1:A] => τ_0_0.[P1&P2:B]
-// CHECK: - τ_0_0.[P1&P2:B].[P1:B] => τ_0_0.[P1&P2:A]
+// CHECK: - τ_0_0.[P1&P2:B].[P1:B].[concrete: S1] => τ_0_0.[P1&P2:B].[P1:B]
+// CHECK: - τ_0_0.[P1&P2:A].[P1:B].[concrete: S2 : P1] => τ_0_0.[P1&P2:A].[P1:B]
+// CHECK: - τ_0_0.[P1&P2:A].[P1:B].[P1:A] => τ_0_0.[P1&P2:A].[P1:B]
+// CHECK: - τ_0_0.[P1&P2:A].[P1:B].[P1:B] => τ_0_0.[P1&P2:A]
+// CHECK: - τ_0_0.[P1&P2:B].[P1:B].[concrete: S1 : P1] => τ_0_0.[P1&P2:B].[P1:B]
+// CHECK: - τ_0_0.[P1&P2:B].[P1:B].[P1:A] => τ_0_0.[P1&P2:B].[P1:B]
+// CHECK: - τ_0_0.[P1&P2:B].[P1:B].[P1:B] => τ_0_0.[P1&P2:B]
 // CHECK: }
 // CHECK-LABEL: Property map: {
 // CHECK: τ_0_0.[P1&P2:A] => { conforms_to: [P1] concrete_type: [concrete: S1] }
 // CHECK: τ_0_0.[P1&P2:B] => { conforms_to: [P1] concrete_type: [concrete: S2] }
+// CHECK: τ_0_0.[P1&P2:A].[P1:B] => { conforms_to: [P1] concrete_type: [concrete: S2] }
+// CHECK: τ_0_0.[P1&P2:B].[P1:B] => { conforms_to: [P1] concrete_type: [concrete: S1] }
 // CHECK: }
 // CHECK: }

test/Generics/unify_superclass_types_1.swift

@@ -26,6 +26,6 @@ extension P where Self : Derived {
 // CHECK-NEXT: Rewrite loops: {
 // CHECK:      }
 // CHECK-NEXT: Property map: {
-// CHECK-NEXT:   [P] => { layout: _NativeClass superclass: [superclass: Base] }
+// CHECK-NEXT:   [P] => { conforms_to: [P] layout: _NativeClass superclass: [superclass: Base] }
 // CHECK-NEXT:   τ_0_0 => { conforms_to: [P] layout: _NativeClass superclass: [superclass: Derived] }
 // CHECK-NEXT: }

test/Generics/unify_superclass_types_2.swift

@@ -44,6 +44,8 @@ func unifySuperclassTest<T : P1 & P2>(_: T) {
 // CHECK-NEXT: Rewrite loops: {
 // CHECK:      }
 // CHECK-NEXT: Property map: {
+// CHECK-NEXT:   [P1] => { conforms_to: [P1] }
+// CHECK-NEXT:   [P2] => { conforms_to: [P2] }
 // CHECK-NEXT:   [P1:X] => { layout: _NativeClass superclass: [superclass: Generic<Int, τ_0_0, τ_0_1> with <[P1:A1], [P1:B1]>] }
 // CHECK-NEXT:   [P2:X] => { layout: _NativeClass superclass: [superclass: Generic<τ_0_0, String, τ_0_1> with <[P2:A2], [P2:B2]>] }
 // CHECK-NEXT:   τ_0_0 => { conforms_to: [P1 P2] }

test/Generics/unify_superclass_types_3.swift

@@ -48,6 +48,8 @@ func unifySuperclassTest<T : P1 & P2>(_: T) {
 // CHECK-NEXT: Rewrite loops: {
 // CHECK:      }
 // CHECK-NEXT: Property map: {
+// CHECK-NEXT:   [P1] => { conforms_to: [P1] }
+// CHECK-NEXT:   [P2] => { conforms_to: [P2] }
 // CHECK-NEXT:   [P1:X] => { layout: _NativeClass superclass: [superclass: Derived<τ_0_0, τ_0_1> with <[P1:A1], [P1:B1]>] }
 // CHECK-NEXT:   [P2:X] => { layout: _NativeClass superclass: [superclass: Generic<τ_0_0, String, τ_0_1> with <[P2:A2], [P2:B2]>] }
 // CHECK-NEXT:   τ_0_0 => { conforms_to: [P1 P2] }

test/Generics/unify_superclass_types_4.swift

@@ -47,6 +47,9 @@ func unifySuperclassTest<T : P1 & P2>(_: T) {
 // CHECK-NEXT: Rewrite loops: {
 // CHECK:      }
 // CHECK-NEXT: Property map: {
+// CHECK-NEXT:   [P1] => { conforms_to: [P1] }
+// CHECK-NEXT:   [P2] => { conforms_to: [P2] }
+// CHECK-NEXT:   [Q] => { conforms_to: [Q] }
 // CHECK-NEXT:   [P1:X] => { layout: _NativeClass superclass: [superclass: Base<τ_0_0> with <[P1:A1]>] }
 // CHECK-NEXT:   [P2:A2] => { conforms_to: [Q] }
 // CHECK-NEXT:   [P2:X] => { layout: _NativeClass superclass: [superclass: Derived<τ_0_0> with <[P2:A2]>] }