RequirementMachine: Support DependentMemberTypes in remapConcreteSubstitutionSchema()

When concretizing nested types, we need to be able to normalize a concrete type
containing DependentMemberTypes to our 'concrete substitution schema' form where
all type parameter structural sub-components are actually just generic parameters.

Author: slavapestov

lib/AST/RequirementMachine/EquivalenceClassMap.cpp

@@ -204,23 +204,30 @@ static MutableTerm getRelativeTermForType(CanType typeWitness,
   return result;
 }
 
-/// Given a concrete type that is a structural sub-component of a concrete
-/// type produced by RewriteSystemBuilder::getConcreteSubstitutionSchema(),
-/// collect the subset of referenced substitutions and renumber the generic
-/// parameters in the type.
+/// This method takes a concrete type that was derived from a concrete type
+/// produced by RewriteSystemBuilder::getConcreteSubstitutionSchema(),
+/// either by extracting a structural sub-component or performing a (Swift AST)
+/// substitution using subst(). It returns a new concrete substitution schema
+/// and a new list of substitution terms.
 ///
 /// For example, suppose we start with the concrete type
 ///
 ///   Dictionary<τ_0_0, Array<τ_0_1>> with substitutions {X.Y, Z}
 ///
 /// We can extract out the structural sub-component Array<τ_0_1>. If we wish
-/// to turn this into a new concrete substitution schema, we call this method
-/// with Array<τ_0_1> and the original substitutions {X.Y, Z}. This will
-/// return the type Array<τ_0_0> and the substitutions {Z}.
-CanType
+/// to build a new concrete substitution schema, we call this method with
+/// Array<τ_0_1> and the original substitutions {X.Y, Z}. This will produce
+/// the new schema Array<τ_0_0> with substitutions {Z}.
+///
+/// As another example, consider we start with the schema Bar<τ_0_0> with
+/// original substitutions {X.Y}, and perform a Swift AST subst() to get
+/// Foo<τ_0_0.A.B>. We can then call this method with Foo<τ_0_0.A.B> and
+/// the original substitutions {X.Y} to produce the new schema Foo<τ_0_0>
+/// with substitutions {X.Y.A.B}.
+static CanType
 remapConcreteSubstitutionSchema(CanType concreteType,
                                 ArrayRef<Term> substitutions,
-                                ASTContext &ctx,
+                                RewriteContext &ctx,
                                 SmallVectorImpl<Term> &result) {
   assert(!concreteType->isTypeParameter() && "Must have a concrete type here");
 
@@ -229,16 +236,16 @@ remapConcreteSubstitutionSchema(CanType concreteType,
 
   return CanType(concreteType.transformRec(
     [&](Type t) -> Optional<Type> {
-      assert(!t->is<DependentMemberType>());
-
-      if (!t->is<GenericTypeParamType>())
+      if (!t->isTypeParameter())
         return None;
 
-      unsigned oldIndex = getGenericParamIndex(t);
+      auto term = getRelativeTermForType(CanType(t), substitutions, ctx);
+
       unsigned newIndex = result.size();
-      result.push_back(substitutions[oldIndex]);
+      result.push_back(Term::get(term, ctx));
 
-      return CanGenericTypeParamType::get(/*depth=*/0, newIndex, ctx);
+      return CanGenericTypeParamType::get(/*depth=*/0, newIndex,
+                                          ctx.getASTContext());
     }));
 }
 
@@ -326,8 +333,7 @@ static Atom unifyConcreteTypes(
         SmallVector<Term, 3> result;
         auto concreteType = remapConcreteSubstitutionSchema(CanType(secondType),
                                                             rhsSubstitutions,
-                                                            ctx.getASTContext(),
-                                                            result);
+                                                            ctx, result);
 
         MutableTerm constraintTerm(subjectTerm);
         constraintTerm.add(Atom::forConcreteType(concreteType, result, ctx));
@@ -350,8 +356,7 @@ static Atom unifyConcreteTypes(
         SmallVector<Term, 3> result;
         auto concreteType = remapConcreteSubstitutionSchema(CanType(firstType),
                                                             lhsSubstitutions,
-                                                            ctx.getASTContext(),
-                                                            result);
+                                                            ctx, result);
 
         MutableTerm constraintTerm(subjectTerm);
         constraintTerm.add(Atom::forConcreteType(concreteType, result, ctx));
@@ -676,12 +681,10 @@ void EquivalenceClassMap::concretizeNestedTypesFromConcreteParent(
         // The type witness is a concrete type.
         constraintType = subjectType;
 
-        // FIXME: Handle dependent member types here
         SmallVector<Term, 3> result;
         auto typeWitnessSchema =
             remapConcreteSubstitutionSchema(typeWitness, substitutions,
-                                            Context.getASTContext(),
-                                            result);
+                                            Context, result);
 
         // Add a rule T.[P:A].[concrete: Foo.A] => T.[P:A].
         constraintType.add(

test/Generics/unify_nested_types_3.swift

@@ -0,0 +1,38 @@
+// RUN: %target-typecheck-verify-swift -enable-requirement-machine -debug-requirement-machine 2>&1 | %FileCheck %s
+
+protocol P1 {
+  associatedtype T : P1
+}
+
+protocol P2 {
+  associatedtype T
+}
+
+struct X<A : P1> : P2 {
+  typealias T = X<A.T>
+}
+
+protocol P2a {
+  associatedtype T : P2
+}
+
+protocol P3a {
+  associatedtype T where T == X<U>
+  associatedtype U : P1
+}
+
+struct G<T : P2a & P3a> {}
+
+// X.T has a DependentMemberType in it; make sure that we build the
+// correct substitution schema.
+
+// CHECK-LABEL: Requirement machine for <τ_0_0 where τ_0_0 : P2a, τ_0_0 : P3a>
+// CHECK-LABEL: Rewrite system: {
+// CHECK: - τ_0_0.[P2a&P3a:T].[concrete: X<τ_0_0> with <τ_0_0.[P3a:U]>] => τ_0_0.[P2a&P3a:T]
+// CHECK: - τ_0_0.[P2a&P3a:T].[P2:T].[concrete: X<τ_0_0> with <τ_0_0.[P3a:U].[P1:T]>] => τ_0_0.[P2a&P3a:T].[P2:T]
+// CHECK: }
+// CHECK-LABEL: Equivalence class map: {
+// CHECK: τ_0_0.[P2a&P3a:T] => { conforms_to: [P2] concrete_type: [concrete: X<τ_0_0> with <τ_0_0.[P3a:U]>] }
+// CHECK: τ_0_0.[P2a&P3a:T].[P2:T] => { concrete_type: [concrete: X<τ_0_0> with <τ_0_0.[P3a:U].[P1:T]>] }
+// CHECK: }
+// CHECK: }