RequirementMachine: Fix the most embarassing bug of all time

The implementation of Knuth-Bendix completion has had a subtle
bookkeeping bug since I first wrote the code in 2021.

It is possible for two rules to overlap in more than one position,
but the ResolvedOverlaps set was a set of pairs (i, j), where
i and j are the index of the two rules. So overlaps other than
the first were not considered. Fix this by changing ResolvedOverlaps
to a set of triples (i, j, k), where k is the position in the
left-hand side of the first rule.

The end result is that we would incorrectly accept the protocol M3
shown in the test case. I'm pretty sure the monoid that M3 encodes
does not have a complete presentation over any alphabet, so of
course it should not be accepted here.

Author: slavapestov

lib/AST/RequirementMachine/KnuthBendix.cpp

@@ -399,7 +399,8 @@ RewriteSystem::performKnuthBendix(unsigned maxRuleCount,
 
           // We don't have to consider the same pair of rules more than once,
           // since those critical pairs were already resolved.
-          if (!CheckedOverlaps.insert(std::make_pair(i, j)).second)
+          unsigned k = from - lhs.getLHS().begin();
+          if (!CheckedOverlaps.insert(std::make_tuple(i, j, k)).second)
             return;
 
           // Try to repair the confluence violation by adding a new rule.

lib/AST/RequirementMachine/RewriteSystem.h

@@ -219,7 +219,7 @@ class RewriteSystem final {
   //////////////////////////////////////////////////////////////////////////////
 
   /// Pairs of rules which have already been checked for overlap.
-  llvm::DenseSet<std::pair<unsigned, unsigned>> CheckedOverlaps;
+  llvm::DenseSet<std::tuple<unsigned, unsigned, unsigned>> CheckedOverlaps;
 
   std::pair<CompletionResult, unsigned>
   performKnuthBendix(unsigned maxRuleCount, unsigned maxRuleLength);

test/Generics/non_confluent.swift

@@ -99,11 +99,12 @@ protocol M2 {
     where B.A == A.B, C.A == A, A.C == A  // expected-error *{{is not a member type}}
 }
 
-// FIXME: This should be rejected
 protocol M3 {
+// expected-error@-1 {{cannot build rewrite system for protocol; rule length limit exceeded}}
+// expected-note@-2 {{failed rewrite rule is }}
   associatedtype A: M3
   associatedtype B: M3
-    where A.A.A == A, A.B.B.A == B.B
+    where A.A.A == A, A.B.B.A == B.B  // expected-error *{{is not a member type}}
 }
 
 protocol M4 {