RequirementMachine: Fix introduction of same-type requirement for recursive concrete witness

Author: slavapestov

lib/AST/RequirementMachine/ConcreteTypeWitness.cpp

@@ -314,6 +314,14 @@ MutableTerm PropertyMap::computeConstraintTermForTypeWitness(
     return result;
   }
 
+  // Compute the concrete type symbol [concrete: C.X].
+  SmallVector<Term, 3> result;
+  auto typeWitnessSchema =
+      Context.getRelativeSubstitutionSchemaFromType(typeWitness, substitutions,
+                                                    result);
+  auto typeWitnessSymbol =
+      Symbol::forConcreteType(typeWitnessSchema, result, Context);
+
   // 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.
@@ -326,10 +334,14 @@ MutableTerm PropertyMap::computeConstraintTermForTypeWitness(
       if (auto *props = lookUpProperties(prefix)) {
         if (props->isConcreteType() &&
             props->getConcreteType() == typeWitness) {
-          auto result = props->getKey();
+          // Record a relation U.[concrete: C.X] =>> U.V.[concrete: C : P].[P:X]
+          // where U is the parent such that U.[concrete: C:X] => U.
+          MutableTerm result(props->getKey());
+          result.add(typeWitnessSymbol);
 
           unsigned relationID = System.recordRelation(
-              result, Term::get(subjectType, Context));
+              Term::get(result, Context),
+              Term::get(subjectType, Context));
           path.add(RewriteStep::forRelation(
               /*startOffset=*/0, relationID,
               /*inverse=*/false));
@@ -339,7 +351,7 @@ MutableTerm PropertyMap::computeConstraintTermForTypeWitness(
                           << result << "\n";
           }
 
-          return MutableTerm(result);
+          return result;
         }
       }
 
@@ -350,14 +362,6 @@ MutableTerm PropertyMap::computeConstraintTermForTypeWitness(
   // 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 =
-      Context.getRelativeSubstitutionSchemaFromType(typeWitness, substitutions,
-                                                    result);
-  auto typeWitnessSymbol =
-      Symbol::forConcreteType(typeWitnessSchema, result, Context);
-
   auto concreteConformanceSymbol = *(subjectType.end() - 2);
   auto associatedTypeSymbol = *(subjectType.end() - 1);
 

test/Generics/abstract_type_witnesses_in_protocols_2.swift

@@ -0,0 +1,27 @@
+// RUN: %target-swift-frontend -typecheck %s -debug-generic-signatures -requirement-machine-inferred-signatures=on 2>&1 | %FileCheck %s
+
+protocol P1 {
+  associatedtype X
+}
+
+protocol P2 {
+  associatedtype Y
+}
+
+protocol P3: P2 {
+  associatedtype Z: P1 where Z.X == C
+}
+
+struct C: P3 {
+  typealias Y = C
+
+  struct Z: P1 {
+    typealias X = C
+  }
+}
+
+// CHECK-LABEL: ExtensionDecl line={{.*}} base=P1
+// CHECK-NEXT: Generic signature: <Self where Self : P1, Self.[P1]X : P2, Self.[P1]X.[P2]Y == C>
+extension P1 where X: P2, X.Y : P3, X.Y == C {
+  func foo(_ x: X.Y) -> C { return x }
+}