Sema: Fix logic error in associated type inference solver

This problem was introduced in 2017 by commit bbaa7f7.

If a protocol requirement has multiple potential witnesses, and one
of those witnesses only introduces tautological type witness bindings,
we would be forced to choose among the remaining witnesses.

However, this did not account for the possibility that the
tautological witness is the correct choice; it's possible that we
will infer the same type witnesses via a different protocol
requirement.

Author: slavapestov

lib/Sema/AssociatedTypeInference.cpp

@@ -599,6 +599,8 @@ void InferredAssociatedTypesByWitness::dump(llvm::raw_ostream &out,
   out.indent(indent) << "(";
   if (Witness) {
     Witness->dumpRef(out);
+  } else {
+    out << "Tautological";
   }
 
   for (const auto &inferred : Inferred) {
@@ -948,12 +950,12 @@ class AssociatedTypeInference {
 
   /// Infer associated type witnesses for the given tentative
   /// requirement/witness match.
-  InferredAssociatedTypesByWitness inferTypeWitnessesViaValueWitness(
+  InferredAssociatedTypesByWitness getPotentialTypeWitnessesByMatchingTypes(
                                      ValueDecl *req,
                                      ValueDecl *witness);
 
   /// Infer associated type witnesses for the given value requirement.
-  InferredAssociatedTypesByWitnesses inferTypeWitnessesViaValueWitnesses(
+  InferredAssociatedTypesByWitnesses getPotentialTypeWitnessesFromRequirement(
                    const llvm::SetVector<AssociatedTypeDecl *> &allUnresolved,
                    ValueDecl *req);
 
@@ -1309,20 +1311,25 @@ static bool isExtensionUsableForInference(const ExtensionDecl *extension,
   if (!checkConformance(proto))
     return false;
 
-  // Source file and module file have different ways to get self bounds.
-  // Source file extension will have trailing where clause which can avoid
-  // computing a generic signature. Module file will not have
-  // trailing where clause, so it will compute generic signature to get
-  // self bounds which might result in slow performance.
+  // In a source file, we perform a syntactic check which avoids computing a
+  // generic signature. In a binary module, we have a generic signature so we
+  // can query it directly.
   SelfBounds bounds;
   if (extension->getParentSourceFile() != nullptr)
     bounds = getSelfBoundsFromWhereClause(extension);
-  else
+  else {
+    LLVM_DEBUG(llvm::dbgs() << "-- extension generic signature: "
+                            << extension->getGenericSignature() << "\n");
     bounds = getSelfBoundsFromGenericSignature(extension);
+  }
   for (auto *decl : bounds.decls) {
     if (auto *proto = dyn_cast<ProtocolDecl>(decl)) {
-      if (!checkConformance(proto))
+      if (!checkConformance(proto)) {
+        LLVM_DEBUG(llvm::dbgs() << "-- " << conformance->getType()
+                                << " does not conform to " << proto->getName()
+                                << "\n");
         return false;
+      }
     }
   }
 
@@ -1431,8 +1438,31 @@ static InferenceCandidateKind checkInferenceCandidate(
   return InferenceCandidateKind::Good;
 }
 
+/// Create an initial constraint system for the associated type inference solver.
+///
+/// Each protocol requirement defines a disjunction, where each disjunction
+/// element is a potential value witness for the requirement.
+///
+/// Each value witness binds some set of type witness candidates, which we
+/// compute by matching the witness type against the requirement.
+///
+/// The solver must pick exactly one value witness for each requirement while
+/// ensuring that the potential type bindings from each value witness are
+/// compatible with each other.
+///
+/// A value witness may be tautological, meaning it does not introduce any
+/// potential type witness bindings, for example, a protocol extension default
+/// `func f(_: Self.A) {}` for a protocol requirement `func f(_: Self.A)` with
+/// associated type A.
+///
+/// We collapse all tautological witnesses into one, since the solver only needs
+/// to explore that part of the solution space at most once. It is also true
+/// that it needs to explore it *at least* once, and we must take care when
+/// skipping potential bindings to distinguish between scenarios where a single
+/// binding is skipped, or the entire value witness must be thrown out because
+/// a binding is unsatisfiable.
 InferredAssociatedTypesByWitnesses
-AssociatedTypeInference::inferTypeWitnessesViaValueWitnesses(
+AssociatedTypeInference::getPotentialTypeWitnessesFromRequirement(
                     const llvm::SetVector<AssociatedTypeDecl *> &allUnresolved,
                     ValueDecl *req) {
   // Conformances constructed by the ClangImporter should have explicit type
@@ -1449,6 +1479,9 @@ AssociatedTypeInference::inferTypeWitnessesViaValueWitnesses(
 
   InferredAssociatedTypesByWitnesses result;
 
+  // Was there at least one witness that does not introduce new bindings?
+  bool hadTautologicalWitness = false;
+
   LLVM_DEBUG(llvm::dbgs() << "Considering requirement:\n";
              req->dump(llvm::dbgs()));
 
@@ -1473,7 +1506,7 @@ AssociatedTypeInference::inferTypeWitnessesViaValueWitnesses(
     }
 
     // Try to resolve the type witness via this value witness.
-    auto witnessResult = inferTypeWitnessesViaValueWitness(req, witness);
+    auto witnessResult = getPotentialTypeWitnessesByMatchingTypes(req, witness);
 
     // Filter out duplicated inferred types as well as inferred types
     // that don't meet the requirements placed on the associated type.
@@ -1493,12 +1526,16 @@ AssociatedTypeInference::inferTypeWitnessesViaValueWitnesses(
       // Filter out errors.
       if (result.second->hasError()) {
         LLVM_DEBUG(llvm::dbgs() << "-- has error type\n");
+        // Skip this binding, but consider others from the same witness.
+        // This might not be strictly correct, but once we have error types
+        // we're diagnosing something anyway.
         REJECT;
       }
 
       // Filter out duplicates.
       if (!known.insert({result.first, result.second->getCanonicalType()})
                 .second) {
+        // Skip this binding, but consider others from the same witness.
         LLVM_DEBUG(llvm::dbgs() << "-- duplicate\n");
         REJECT;
       }
@@ -1517,18 +1554,20 @@ AssociatedTypeInference::inferTypeWitnessesViaValueWitnesses(
 
       case InferenceCandidateKind::Tautological: {
         LLVM_DEBUG(llvm::dbgs() << "-- tautological\n");
+        // Skip this binding because it is immediately satisfied.
         REJECT;
       }
 
       case InferenceCandidateKind::Infinite: {
         LLVM_DEBUG(llvm::dbgs() << "-- infinite\n");
+        // Discard this witness altogether, because it has an unsatisfiable
+        // binding.
         goto next_witness;
       }
       }
 
-      // Check that the type witness doesn't contradict an
-      // explicitly-given type witness. If it does contradict, throw out the
-      // witness completely.
+      // Check that the binding doesn't contradict an explicitly-given type
+      // witness. If it does contradict, throw out the witness completely.
       if (!allUnresolved.count(result.first)) {
         auto existingWitness =
           conformance->getTypeWitness(result.first);
@@ -1560,6 +1599,10 @@ AssociatedTypeInference::inferTypeWitnessesViaValueWitnesses(
           witnessResult.NonViable.push_back(
                           std::make_tuple(result.first,result.second,failed));
           LLVM_DEBUG(llvm::dbgs() << "-- doesn't fulfill requirements\n");
+
+          // By adding an element to NonViable we ensure the witness is rejected
+          // below, so we continue to consider other bindings to generate better
+          // diagnostics later.
           REJECT;
         }
       }
@@ -1569,9 +1612,13 @@ AssociatedTypeInference::inferTypeWitnessesViaValueWitnesses(
     }
 #undef REJECT
 
-    // If no inferred types remain, skip this witness.
-    if (witnessResult.Inferred.empty() && witnessResult.NonViable.empty())
+    // If no viable or non-viable bindings remain, the witness does not
+    // inter anything new, nor contradict any existing bindings. We collapse
+    // all tautological witnesses into a single element of the disjunction.
+    if (witnessResult.Inferred.empty() && witnessResult.NonViable.empty()) {
+      hadTautologicalWitness = true;
       continue;
+    }
 
     // If there were any non-viable inferred associated types, don't
     // infer anything from this witness.
@@ -1582,6 +1629,13 @@ AssociatedTypeInference::inferTypeWitnessesViaValueWitnesses(
 next_witness:;
 }
 
+  if (hadTautologicalWitness && !result.empty()) {
+    // Create a dummy entry, but only if there was at least one other witness;
+    // otherwise, we return an empty disjunction. See the remark in
+    // inferTypeWitnessesViaValueWitnesses() for explanation.
+    result.push_back(InferredAssociatedTypesByWitness());
+  }
+
   return result;
 }
 
@@ -1654,10 +1708,16 @@ AssociatedTypeInference::inferTypeWitnessesViaValueWitnesses(
         continue;
     }
 
-    // Infer associated types from the potential value witnesses for
-    // this requirement.
+    // Collect this requirement's value witnesses and their potential
+    // type witness bindings.
     auto reqInferred =
-      inferTypeWitnessesViaValueWitnesses(assocTypes, req);
+      getPotentialTypeWitnessesFromRequirement(assocTypes, req);
+
+    // An empty disjunction is silently discarded, instead of immediately
+    // refuting the entirely system as it would in a real solver.
+    //
+    // If we find a solution and it so happens that this requirement cannot be
+    // witnessed, we'll diagnose the failure later in value witness checking.
     if (reqInferred.empty())
       continue;
 
@@ -1820,6 +1880,12 @@ AssociatedTypeInference::inferTypeWitnessesViaAssociatedType(
     result.push_back(std::move(inferred));
   }
 
+  if (!result.empty()) {
+    // If we found at least one default candidate, we must allow for the
+    // possibility that no default is chosen by adding a tautological witness
+    // to our disjunction.
+    result.push_back(InferredAssociatedTypesByWitness());
+  }
   return result;
 }
 
@@ -1878,10 +1944,11 @@ getReferencedAssocTypeOfProtocol(Type type, ProtocolDecl *proto) {
   return nullptr;
 }
 
-/// Attempt to resolve a type witness via a specific value witness.
+/// Find a set of potential type witness bindings by matching the interface type
+/// of the requirement against the interface type of a witness.
 InferredAssociatedTypesByWitness
-AssociatedTypeInference::inferTypeWitnessesViaValueWitness(ValueDecl *req,
-                                                           ValueDecl *witness) {
+AssociatedTypeInference::getPotentialTypeWitnessesByMatchingTypes(ValueDecl *req,
+                                                                  ValueDecl *witness) {
   InferredAssociatedTypesByWitness inferred;
   inferred.Witness = witness;
 
@@ -3032,16 +3099,28 @@ void AssociatedTypeInference::findSolutionsRec(
   for (const auto &witnessReq : inferredReq.second) {
     llvm::SaveAndRestore<unsigned> savedNumTypeWitnesses(numTypeWitnesses);
 
-    // If we inferred a type witness via a default, try both with and without
-    // the default.
-    if (isa<TypeDecl>(inferredReq.first)) {
-      // Recurse without considering this type.
+    // If we had at least one tautological witness, we must consider the
+    // possibility that none of the remaining witnesses are chosen.
+    if (witnessReq.Witness == nullptr) {
+      // Count tautological witnesses as if they come from protocol extensions,
+      // which ranks the solution lower than a more constrained one.
+      if (!isa<TypeDecl>(inferredReq.first))
+        ++numValueWitnessesInProtocolExtensions;
       valueWitnesses.push_back({inferredReq.first, nullptr});
       findSolutionsRec(unresolvedAssocTypes, solutions, nonViableSolutions,
                        valueWitnesses, numTypeWitnesses,
                        numValueWitnessesInProtocolExtensions, reqDepth + 1);
       valueWitnesses.pop_back();
+      if (!isa<TypeDecl>(inferredReq.first))
+        --numValueWitnessesInProtocolExtensions;
+      continue;
+    }
 
+    // If we inferred a type witness via a default, we do a slightly simpler
+    // thing.
+    //
+    // FIXME: Why can't we just fold this with the below?
+    if (isa<TypeDecl>(inferredReq.first)) {
       ++numTypeWitnesses;
       for (const auto &typeWitness : witnessReq.Inferred) {
         auto known = typeWitnesses.begin(typeWitness.first);
@@ -3075,6 +3154,7 @@ void AssociatedTypeInference::findSolutionsRec(
                llvm::dbgs() << " := ";
                witnessReq.Witness->dumpRef(llvm::dbgs());
                llvm::dbgs() << "\n";);
+
     valueWitnesses.push_back({inferredReq.first, witnessReq.Witness});
     if (!isa<TypeDecl>(inferredReq.first) &&
         witnessReq.Witness->getDeclContext()->getExtendedProtocolDecl())

test/Generics/associated_type_where_clause.swift

@@ -120,14 +120,14 @@ struct ConcreteInheritsDiffer: Inherits {
     typealias U = ConcreteConforms
     typealias X = ConcreteConforms2
 }
-/*
-FIXME: the sametype requirement gets dropped from the requirement signature
-(enumerateRequirements doesn't yield it), so this doesn't error as it should.
+
 struct BadConcreteInherits: Inherits {
+// expected-error@-1 {{type 'BadConcreteInherits' does not conform to protocol 'Inherits'}}
+// expected-error@-2 {{'Inherits' requires the types 'ConcreteConforms.T' (aka 'Int') and 'ConcreteConformsNonFoo2.T' (aka 'Float') be equivalent}}
+// expected-note@-3 {{requirement specified as 'Self.U.T' == 'Self.X.T' [with Self = BadConcreteInherits]}}
     typealias U = ConcreteConforms
     typealias X = ConcreteConformsNonFoo2
 }
-*/
 
 struct X { }
 

test/decl/protocol/req/associated_type_inference_tautology.swift

@@ -1,6 +1,8 @@
 // RUN: %target-typecheck-verify-swift -disable-experimental-associated-type-inference
 // RUN: %target-typecheck-verify-swift -enable-experimental-associated-type-inference
 
+// A := G<A> is unsatisfiable and not a tautology!
+
 protocol P1 {
   associatedtype A
   associatedtype B
@@ -26,6 +28,8 @@ struct S1: P1 {}
 let x1: String.Type = S1.A.self
 let y1: String.Type = S1.B.self
 
+// Potential witness has innermost generic parameters.
+
 protocol P2 {
   associatedtype A
   associatedtype B
@@ -47,4 +51,27 @@ extension P2 {
 struct S2: P2 {}
 
 let x2: String.Type = S2.A.self
-let y2: String.Type = S2.B.self
+let y2: String.Type = S2.B.self
+
+// If all type witness bindings were tautological, we must still consider the
+// witness as introducing no bindings.
+
+protocol P3 {
+  associatedtype A
+
+  func f(_: A)
+  func g(_: A)
+}
+
+extension P3 {
+  func g(_: A) {}
+
+  // We should not be forced to choose g().
+  func g(_: String) {}
+}
+
+struct S3: P3 {
+  func f(_: Int) {}
+}
+
+let x3: Int.Type = S3.A.self