RequirementMachine: Conditional requirement inference

If a type parameter is subject to both a conformance requirement
and a concrete type requirement, the concrete type might conform
conditionally.

In this case, introduce new requirements to satisfy the conditional
conformance.

Since this can add new hitherto-unseen protocols to the rewrite
system, restrict this feature to top-level generic signatures, and
not protocol requirement signatures. Allowing this to occur in
protocol requirement signatures would change the connectivity of
the protocol dependency graph (and hence the connected components)
during completion, which would be a major complication in the
design. The GSB already enforces this restriction.

I changed the existing conditional_requirement_inference.swift test
to run with -requirement-machine-inferred-signatures=verify. Since
one of the test cases there triggers an unrelated bug in the
Requirement Machine, I split it off into a new file named
conditional_requirement_inference_2.swift which still runs with
the GSB. Once the bug is fixed I'll merge the files again.

lib/AST/RequirementMachine/Debug.h

@@ -38,17 +38,21 @@ enum class DebugFlags : unsigned {
   /// Print debug output when concretizing nested types in the property map.
   ConcretizeNestedTypes = (1<<5),
 
+  /// Print debug output when inferring conditional requirements in the
+  /// property map.
+  ConditionalRequirements = (1<<6),
+
   /// Print debug output from the homotopy reduction algorithm.
-  HomotopyReduction = (1<<6),
+  HomotopyReduction = (1<<7),
 
   /// Print debug output from the minimal conformances algorithm.
-  MinimalConformances = (1<<7),
+  MinimalConformances = (1<<8),
 
   /// Print debug output from the protocol dependency graph.
-  ProtocolDependencies = (1<<8),
+  ProtocolDependencies = (1<<9),
 
   /// Print debug output from generic signature minimization.
-  Minimization = (1<<9),
+  Minimization = (1<<10),
 };
 
 using DebugOptions = OptionSet<DebugFlags>;

lib/AST/RequirementMachine/PropertyMap.h

@@ -264,6 +264,10 @@ private:
                    ProtocolConformance *concrete,
                    AssociatedTypeDecl *assocType) const;
 
+  void inferConditionalRequirements(
+                   ProtocolConformance *concrete,
+                   ArrayRef<Term> substitutions) const;
+
   MutableTerm computeConstraintTermForTypeWitness(
       Term key, RequirementKind requirementKind,
       CanType concreteType, CanType typeWitness,

lib/AST/RequirementMachine/PropertyUnification.cpp

@@ -33,6 +33,7 @@
 #include <vector>
 
 #include "PropertyMap.h"
+#include "RequirementLowering.h"
 
 using namespace swift;
 using namespace rewriting;
@@ -703,15 +704,16 @@ void PropertyMap::concretizeNestedTypesFromConcreteParent(
     recordConcreteConformanceRule(concreteRuleID, conformanceRuleID,
                                   requirementKind, concreteConformanceSymbol);
 
-    auto assocTypes = proto->getAssociatedTypeMembers();
-    if (assocTypes.empty())
-      continue;
-
-    for (auto *assocType : assocTypes) {
+    for (auto *assocType : proto->getAssociatedTypeMembers()) {
       concretizeTypeWitnessInConformance(key, requirementKind,
                                          concreteConformanceSymbol,
                                          concrete, assocType);
     }
+
+    // We only infer conditional requirements in top-level generic signatures,
+    // not in protocol requirement signatures.
+    if (key.getRootProtocols().empty())
+      inferConditionalRequirements(concrete, substitutions);
   }
 }
 
@@ -1002,3 +1004,80 @@ void PropertyMap::recordConcreteConformanceRule(
 
   (void) System.addRule(std::move(lhs), std::move(rhs), &path);
 }
+
+/// If \p key is fixed to a concrete type and is also subject to a conformance
+/// requirement, the concrete type might conform conditionally. In this case,
+/// introduce rules for any conditional requirements in the given conformance.
+void PropertyMap::inferConditionalRequirements(
+    ProtocolConformance *concrete, ArrayRef<Term> substitutions) const {
+
+  auto conditionalRequirements = concrete->getConditionalRequirements();
+
+  if (Debug.contains(DebugFlags::ConditionalRequirements)) {
+    if (conditionalRequirements.empty())
+      llvm::dbgs() << "@@ No conditional requirements from ";
+    else
+      llvm::dbgs() << "@@ Inferring conditional requirements from ";
+
+    llvm::dbgs() << concrete->getType() << " : ";
+    llvm::dbgs() << concrete->getProtocol()->getName() << "\n";
+  }
+
+  if (conditionalRequirements.empty())
+    return;
+
+  SmallVector<Requirement, 2> desugaredRequirements;
+
+  // First, desugar all conditional requirements.
+  for (auto req : conditionalRequirements) {
+    if (Debug.contains(DebugFlags::ConditionalRequirements)) {
+      llvm::dbgs() << "@@@ Original requirement: ";
+      req.dump(llvm::dbgs());
+      llvm::dbgs() << "\n";
+    }
+
+    desugarRequirement(req, desugaredRequirements);
+  }
+
+  // Now, convert desugared conditional requirements to rules.
+  for (auto req : desugaredRequirements) {
+    if (Debug.contains(DebugFlags::ConditionalRequirements)) {
+      llvm::dbgs() << "@@@ Desugared requirement: ";
+      req.dump(llvm::dbgs());
+      llvm::dbgs() << "\n";
+    }
+
+    if (req.getKind() == RequirementKind::Conformance) {
+      auto *proto = req.getProtocolDecl();
+
+      // If we haven't seen this protocol before, add rules for its
+      // requirements.
+      if (!System.isKnownProtocol(proto)) {
+        if (Debug.contains(DebugFlags::ConditionalRequirements)) {
+          llvm::dbgs() << "@@@ Unknown protocol: "<< proto->getName() << "\n";
+        }
+
+        RuleBuilder builder(Context, System.getProtocolMap());
+        builder.addProtocol(proto, /*initialComponent=*/false);
+        builder.collectRulesFromReferencedProtocols();
+
+        for (const auto &rule : builder.PermanentRules)
+          System.addPermanentRule(rule.first, rule.second);
+
+        for (const auto &rule : builder.RequirementRules)
+          System.addExplicitRule(rule.first, rule.second);
+      }
+    }
+
+    auto pair = getRuleForRequirement(req.getCanonical(), /*proto=*/nullptr,
+                                      substitutions, Context);
+
+    if (Debug.contains(DebugFlags::ConditionalRequirements)) {
+      llvm::dbgs() << "@@@ Induced rule from conditional requirement: "
+                   << pair.first << " => " << pair.second << "\n";
+    }
+
+    // FIXME: Do we need a rewrite path here?
+    (void) System.addRule(pair.first, pair.second);
+  }
+}

lib/AST/RequirementMachine/RewriteContext.cpp

@@ -33,6 +33,7 @@ static DebugOptions parseDebugFlags(StringRef debugFlags) {
       .Case("completion", DebugFlags::Completion)
       .Case("concrete-unification", DebugFlags::ConcreteUnification)
       .Case("concretize-nested-types", DebugFlags::ConcretizeNestedTypes)
+      .Case("conditional-requirements", DebugFlags::ConditionalRequirements)
       .Case("homotopy-reduction", DebugFlags::HomotopyReduction)
       .Case("minimal-conformances", DebugFlags::MinimalConformances)
       .Case("protocol-dependencies", DebugFlags::ProtocolDependencies)

test/Generics/conditional_requirement_inference.swift

@@ -1,58 +1,25 @@
 // RUN: %target-typecheck-verify-swift
-// RUN: not %target-swift-frontend -typecheck -debug-generic-signatures %s 2>&1 | %FileCheck %s
+// RUN: %target-swift-frontend -typecheck -debug-generic-signatures -requirement-machine-inferred-signatures=verify %s 2>&1 | %FileCheck %s
 
+protocol Equatable {}
+
+struct Array<Element> {}
+
+extension Array : Equatable where Element : Equatable {}
 
-// Valid example
 struct EquatableBox<T : Equatable> {
   // CHECK: Generic signature: <T, U where T == Array<U>, U : Equatable>
   func withArray<U>(_: U) where T == Array<U> {}
 }
 
-struct EquatableSequenceBox<T : Sequence> where T.Element : Equatable {
-  // CHECK: Generic signature: <T, U where T == Array<Array<U>>, U : Equatable>
-  func withArrayArray<U>(_: U) where T == Array<Array<U>> {}
-}
-
-
-// A very elaborate invalid example (see comment in mergeP1AndP2())
-struct G<T> {}
-
-protocol P {}
-extension G : P where T : P {}
-
-protocol P1 {
-  associatedtype T
-  associatedtype U where U == G<T>
-  associatedtype R : P1
-}
-
-protocol P2 {
-  associatedtype U : P
-  associatedtype R : P2
-}
-
-func takesP<T : P>(_: T.Type) {}
-// expected-note@-1 {{where 'T' = 'T.T'}}
-// expected-note@-2 {{where 'T' = 'T.R.T'}}
-// expected-note@-3 {{where 'T' = 'T.R.R.T'}}
-// expected-note@-4 {{where 'T' = 'T.R.R.R.T'}}
-
-// CHECK: Generic signature: <T where T : P1, T : P2>
-func mergeP1AndP2<T : P1 & P2>(_: T) {
-  // P1 implies that T.(R)*.U == G<T.(R)*.T>, and P2 implies that T.(R)*.U : P.
-  //
-  // These together would seem to imply that G<T.(R)*.T> : P, therefore
-  // the conditional conformance G : P should imply that T.(R)*.T : P.
-  //
-  // However, this would require us to infer an infinite number of
-  // conformance requirements in the signature of mergeP1AndP2() of the
-  // form T.(R)*.T : P.
-  //
-  // Since we're unable to represent that, make sure that a) we don't crash,
-  // b) we reject the conformance T.(R)*.T : P.
-
-  takesP(T.T.self) // expected-error {{global function 'takesP' requires that 'T.T' conform to 'P'}}
-  takesP(T.R.T.self) // expected-error {{global function 'takesP' requires that 'T.R.T' conform to 'P'}}
-  takesP(T.R.R.T.self) // expected-error {{global function 'takesP' requires that 'T.R.R.T' conform to 'P'}}
-  takesP(T.R.R.R.T.self) // expected-error {{global function 'takesP' requires that 'T.R.R.R.T' conform to 'P'}}
+// A conditional requirement with a protocol we haven't seen before.
+protocol First {}
+
+protocol Second {}
+
+extension Array : First where Element : Second {}
+
+struct SillyBox<T : First> {
+  // CHECK: Generic signature: <T, U where T == Array<U>, U : Second>
+  func withArray<U>(_: U) where T == Array<U> {}
 }

test/Generics/conditional_requirement_inference_2.swift

@@ -0,0 +1,20 @@
+// RUN: %target-typecheck-verify-swift
+// RUN: %target-swift-frontend -typecheck -debug-generic-signatures %s 2>&1 | %FileCheck %s
+
+// A more complicated example.
+protocol Equatable {}
+
+struct Array<Element> {}
+
+extension Array : Equatable where Element : Equatable {}
+
+protocol Sequence {
+  associatedtype Element
+}
+
+extension Array : Sequence {}
+
+struct EquatableSequenceBox<T : Sequence> where T.Element : Equatable {
+  // CHECK: Generic signature: <T, U where T == Array<Array<U>>, U : Equatable>
+  func withArrayArray<U>(_: U) where T == Array<Array<U>> {}
+}

test/Generics/conditional_requirement_inference_unsupported.swift

@@ -0,0 +1,44 @@
+// RUN: %target-typecheck-verify-swift
+// RUN: not %target-swift-frontend -typecheck -debug-generic-signatures %s 2>&1 | %FileCheck %s
+
+// A very elaborate invalid example (see comment in mergeP1AndP2())
+struct G<T> {}
+
+protocol P {}
+extension G : P where T : P {}
+
+protocol P1 {
+  associatedtype T
+  associatedtype U where U == G<T>
+  associatedtype R : P1
+}
+
+protocol P2 {
+  associatedtype U : P
+  associatedtype R : P2
+}
+
+func takesP<T : P>(_: T.Type) {}
+// expected-note@-1 {{where 'T' = 'T.R.T'}}
+// expected-note@-2 {{where 'T' = 'T.R.R.T'}}
+// expected-note@-3 {{where 'T' = 'T.R.R.R.T'}}
+
+// CHECK: Generic signature: <T where T : P1, T : P2>
+func mergeP1AndP2<T : P1 & P2>(_: T) {
+  // P1 implies that T.(R)*.U == G<T.(R)*.T>, and P2 implies that T.(R)*.U : P.
+  //
+  // These together would seem to imply that G<T.(R)*.T> : P, therefore
+  // the conditional conformance G : P should imply that T.(R)*.T : P.
+  //
+  // However, this would require us to infer an infinite number of
+  // conformance requirements in the signature of mergeP1AndP2() of the
+  // form T.(R)*.T : P.
+  //
+  // Since we're unable to represent that, make sure that a) we don't crash,
+  // b) we reject the conformance T.(R)*.T : P.
+
+  takesP(T.T.self)
+  takesP(T.R.T.self) // expected-error {{global function 'takesP' requires that 'T.R.T' conform to 'P'}}
+  takesP(T.R.R.T.self) // expected-error {{global function 'takesP' requires that 'T.R.R.T' conform to 'P'}}
+  takesP(T.R.R.R.T.self) // expected-error {{global function 'takesP' requires that 'T.R.R.R.T' conform to 'P'}}
+}