RequirementMachine: A better trick to tie off type witness recursion

This will replace the 'concrete type in domain' hack. Instead of
finding some other type parameter with the same concrete type and a
compatible starting symbol, this finds a prefix of the original
term. This allows the induced same-type requirement to be described
with a rewrite path.

Author: slavapestov

lib/AST/RequirementMachine/PropertyUnification.cpp

@@ -945,6 +945,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.
 

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: }