diff --git a/include/swift/AST/ASTContext.h b/include/swift/AST/ASTContext.h
index b97cf8e2fd9d1..4eae92c7ff74e 100644
--- a/include/swift/AST/ASTContext.h
+++ b/include/swift/AST/ASTContext.h
@@ -1166,7 +1166,7 @@ class ASTContext final {
   /// conformance itself, along with a bit indicating whether this diagnostic
   /// produces an error.
   struct DelayedConformanceDiag {
-    const ValueDecl *Requirement;
+    ValueDecl *Requirement;
     std::function<void()> Callback;
     bool IsError;
   };
diff --git a/include/swift/AST/Decl.h b/include/swift/AST/Decl.h
index 91ae1164268bb..0c3f6093bb3af 100644
--- a/include/swift/AST/Decl.h
+++ b/include/swift/AST/Decl.h
@@ -3513,9 +3513,7 @@ class NominalTypeDecl : public GenericTypeDecl, public IterableDeclContext {
          SmallVectorImpl<ProtocolConformance *> &conformances) const;
 
   /// Retrieve all of the protocols that this nominal type conforms to.
-  ///
-  /// \param sorted Whether to sort the protocols in canonical order.
-  SmallVector<ProtocolDecl *, 2> getAllProtocols(bool sorted = false) const;
+  SmallVector<ProtocolDecl *, 2> getAllProtocols() const;
 
   /// Retrieve all of the protocol conformances for this nominal type.
   SmallVector<ProtocolConformance *, 2> getAllConformances(
diff --git a/lib/AST/ConformanceLookupTable.cpp b/lib/AST/ConformanceLookupTable.cpp
index 9590fd994fede..9a329a695fd42 100644
--- a/lib/AST/ConformanceLookupTable.cpp
+++ b/lib/AST/ConformanceLookupTable.cpp
@@ -1061,8 +1061,8 @@ void ConformanceLookupTable::lookupConformances(
 }
 
 void ConformanceLookupTable::getAllProtocols(
-    NominalTypeDecl *nominal, SmallVectorImpl<ProtocolDecl *> &scratch,
-    bool sorted) {
+       NominalTypeDecl *nominal,
+       SmallVectorImpl<ProtocolDecl *> &scratch) {
   // We need to expand all implied conformances to find the complete
   // set of protocols to which this nominal type conforms.
   updateLookupTable(nominal, ConformanceStage::ExpandedImplied);
@@ -1075,9 +1075,7 @@ void ConformanceLookupTable::getAllProtocols(
     scratch.push_back(conformance.first);
   }
 
-  if (sorted) {
-    llvm::array_pod_sort(scratch.begin(), scratch.end(), TypeDecl::compare);
-  }
+  // FIXME: sort the protocols in some canonical order?
 }
 
 int ConformanceLookupTable::compareProtocolConformances(
diff --git a/lib/AST/ConformanceLookupTable.h b/lib/AST/ConformanceLookupTable.h
index c4f8d16deab86..5f1fbeae79253 100644
--- a/lib/AST/ConformanceLookupTable.h
+++ b/lib/AST/ConformanceLookupTable.h
@@ -451,12 +451,9 @@ class ConformanceLookupTable : public ASTAllocated<ConformanceLookupTable> {
                           SmallVectorImpl<ConformanceDiagnostic> *diagnostics);
 
   /// Retrieve the complete set of protocols to which this nominal
-  /// type conforms (if the set contains a protocol, the same is true for any
-  /// inherited protocols).
-  ///
-  /// \param sorted Whether to sort the protocols in canonical order.
+  /// type conforms.
   void getAllProtocols(NominalTypeDecl *nominal,
-                       SmallVectorImpl<ProtocolDecl *> &scratch, bool sorted);
+                       SmallVectorImpl<ProtocolDecl *> &scratch);
 
   /// Retrieve the complete set of protocol conformances for this
   /// nominal type.
diff --git a/lib/AST/ProtocolConformance.cpp b/lib/AST/ProtocolConformance.cpp
index 06376d0cbae22..c90d5e98bc98c 100644
--- a/lib/AST/ProtocolConformance.cpp
+++ b/lib/AST/ProtocolConformance.cpp
@@ -1322,12 +1322,11 @@ bool NominalTypeDecl::lookupConformance(
            conformances);
 }
 
-SmallVector<ProtocolDecl *, 2>
-NominalTypeDecl::getAllProtocols(bool sorted) const {
+SmallVector<ProtocolDecl *, 2> NominalTypeDecl::getAllProtocols() const {
   prepareConformanceTable();
   SmallVector<ProtocolDecl *, 2> result;
-  ConformanceTable->getAllProtocols(const_cast<NominalTypeDecl *>(this), result,
-                                    sorted);
+  ConformanceTable->getAllProtocols(const_cast<NominalTypeDecl *>(this),
+                                    result);
   return result;
 }
 
diff --git a/lib/Sema/TypeCheckProtocol.cpp b/lib/Sema/TypeCheckProtocol.cpp
index af1a6e13ba2b2..21367407b8fc5 100644
--- a/lib/Sema/TypeCheckProtocol.cpp
+++ b/lib/Sema/TypeCheckProtocol.cpp
@@ -5568,8 +5568,8 @@ void swift::diagnoseConformanceFailure(Type T,
 }
 
 void ConformanceChecker::diagnoseOrDefer(
-    const ValueDecl *requirement, bool isError,
-    std::function<void(NormalProtocolConformance *)> fn) {
+       ValueDecl *requirement, bool isError,
+       std::function<void(NormalProtocolConformance *)> fn) {
   if (isError)
     Conformance->setInvalid();
 
diff --git a/lib/Sema/TypeCheckProtocol.h b/lib/Sema/TypeCheckProtocol.h
index 87fcb8f6255cc..4bb4312b95f35 100644
--- a/lib/Sema/TypeCheckProtocol.h
+++ b/lib/Sema/TypeCheckProtocol.h
@@ -100,6 +100,61 @@ CheckTypeWitnessResult checkTypeWitness(Type type,
                                         const NormalProtocolConformance *Conf,
                                         SubstOptions options = None);
 
+/// Describes the means of inferring an abstract type witness.
+enum class AbstractTypeWitnessKind : uint8_t {
+  /// The type witness was inferred via a same-type-to-concrete constraint
+  /// in a protocol requirement signature.
+  Fixed,
+
+  /// The type witness was inferred via a defaulted associated type.
+  Default,
+
+  /// The type witness was inferred to a generic parameter of the
+  /// conforming type.
+  GenericParam,
+};
+
+/// A type witness inferred without the aid of a specific potential
+/// value witness.
+class AbstractTypeWitness {
+  AbstractTypeWitnessKind Kind;
+  AssociatedTypeDecl *AssocType;
+  Type TheType;
+
+  /// When this is a default type witness, the declaration responsible for it.
+  /// May not necessarilly match \c AssocType.
+  AssociatedTypeDecl *DefaultedAssocType;
+
+  AbstractTypeWitness(AbstractTypeWitnessKind Kind,
+                      AssociatedTypeDecl *AssocType, Type TheType,
+                      AssociatedTypeDecl *DefaultedAssocType)
+      : Kind(Kind), AssocType(AssocType), TheType(TheType),
+        DefaultedAssocType(DefaultedAssocType) {
+    assert(AssocType && TheType);
+  }
+
+public:
+  static AbstractTypeWitness forFixed(AssociatedTypeDecl *assocType, Type type);
+
+  static AbstractTypeWitness forDefault(AssociatedTypeDecl *assocType,
+                                        Type type,
+                                        AssociatedTypeDecl *defaultedAssocType);
+
+  static AbstractTypeWitness forGenericParam(AssociatedTypeDecl *assocType,
+                                             Type type);
+
+public:
+  AbstractTypeWitnessKind getKind() const { return Kind; }
+
+  AssociatedTypeDecl *getAssocType() const { return AssocType; }
+
+  Type getType() const { return TheType; }
+
+  AssociatedTypeDecl *getDefaultedAssocType() const {
+    return DefaultedAssocType;
+  }
+};
+
 /// The set of associated types that have been inferred by matching
 /// the given value witness to its corresponding requirement.
 struct InferredAssociatedTypesByWitness {
@@ -801,8 +856,9 @@ class ConformanceChecker : public WitnessChecker {
   ///
   /// \param fn A function to call to emit the actual diagnostic. If
   /// diagnostics are being deferred,
-  void diagnoseOrDefer(const ValueDecl *requirement, bool isError,
-                       std::function<void(NormalProtocolConformance *)> fn);
+  void diagnoseOrDefer(
+         ValueDecl *requirement, bool isError,
+         std::function<void(NormalProtocolConformance *)> fn);
 
   ArrayRef<MissingWitness> getLocalMissingWitness() {
     return GlobalMissingWitnesses.getArrayRef().
@@ -870,136 +926,6 @@ class ConformanceChecker : public WitnessChecker {
                     llvm::function_ref<bool(AbstractFunctionDecl *)>predicate);
 };
 
-/// A system for recording and probing the intergrity of a type witness solution
-/// for a set of unresolved associated type declarations.
-///
-/// Right now can reason only about abstract type witnesses, i.e., same-type
-/// constraints, default type definitions, and bindings to generic parameters.
-class TypeWitnessSystem final {
-  /// Equivalence classes are used on demand to express equivalences between
-  /// witness candidates and reflect changes to resolved types across their
-  /// members.
-  class EquivalenceClass final {
-    /// The pointer:
-    /// - The resolved type for witness candidates belonging to this equivalence
-    ///   class. The resolved type may be a type parameter, but cannot directly
-    ///   pertain to a name variable in the owning system; instead, witness
-    ///   candidates that should resolve to the same type share an equivalence
-    ///   class.
-    /// The int:
-    /// - A flag indicating whether the resolved type is ambiguous. When set,
-    ///   the resolved type is null.
-    llvm::PointerIntPair<Type, 1, bool> ResolvedTyAndIsAmbiguous;
-
-  public:
-    EquivalenceClass(Type ty) : ResolvedTyAndIsAmbiguous(ty, false) {}
-
-    EquivalenceClass(const EquivalenceClass &) = delete;
-    EquivalenceClass(EquivalenceClass &&) = delete;
-    EquivalenceClass &operator=(const EquivalenceClass &) = delete;
-    EquivalenceClass &operator=(EquivalenceClass &&) = delete;
-
-    Type getResolvedType() const {
-      return ResolvedTyAndIsAmbiguous.getPointer();
-    }
-    void setResolvedType(Type ty);
-
-    bool isAmbiguous() const {
-      return ResolvedTyAndIsAmbiguous.getInt();
-    }
-    void setAmbiguous() {
-      ResolvedTyAndIsAmbiguous = {nullptr, true};
-    }
-  };
-
-  /// A type witness candidate for a name variable.
-  struct TypeWitnessCandidate final {
-    /// The defaulted associated type declaration correlating with this
-    /// candidate, if present.
-    const AssociatedTypeDecl *DefaultedAssocType;
-
-    /// The equivalence class of this candidate.
-    EquivalenceClass *EquivClass;
-  };
-
-  /// The set of equivalence classes in the system.
-  llvm::SmallPtrSet<EquivalenceClass *, 4> EquivalenceClasses;
-
-  /// The mapping from name variables (the names of unresolved associated
-  /// type declarations) to their corresponding type witness candidates.
-  llvm::SmallDenseMap<Identifier, TypeWitnessCandidate, 4> TypeWitnesses;
-
-public:
-  TypeWitnessSystem(ArrayRef<AssociatedTypeDecl *> assocTypes);
-  ~TypeWitnessSystem();
-
-  TypeWitnessSystem(const TypeWitnessSystem &) = delete;
-  TypeWitnessSystem(TypeWitnessSystem &&) = delete;
-  TypeWitnessSystem &operator=(const TypeWitnessSystem &) = delete;
-  TypeWitnessSystem &operator=(TypeWitnessSystem &&) = delete;
-
-  /// Get the resolved type witness for the associated type with the given name.
-  Type getResolvedTypeWitness(Identifier name) const;
-  bool hasResolvedTypeWitness(Identifier name) const;
-
-  /// Get the defaulted associated type relating to the resolved type witness
-  /// for the associated type with the given name, if present.
-  const AssociatedTypeDecl *getDefaultedAssocType(Identifier name) const;
-
-  /// Record a type witness for the given associated type name.
-  ///
-  /// \note This need not lead to the resolution of a type witness, e.g.
-  /// an associated type may be defaulted to another.
-  void addTypeWitness(Identifier name, Type type);
-
-  /// Record a default type witness.
-  ///
-  /// \param defaultedAssocType The specific associated type declaration that
-  /// defines the given default type.
-  ///
-  /// \note This need not lead to the resolution of a type witness.
-  void addDefaultTypeWitness(Type type,
-                             const AssociatedTypeDecl *defaultedAssocType);
-
-  /// Record the given same-type requirement, if regarded of interest to
-  /// the system.
-  ///
-  /// \note This need not lead to the resolution of a type witness.
-  void addSameTypeRequirement(const Requirement &req);
-
-  void dump(llvm::raw_ostream &out,
-            const NormalProtocolConformance *conformance) const;
-
-private:
-  /// Form an equivalence between the given name variables.
-  void addEquivalence(Identifier name1, Identifier name2);
-
-  /// Merge \p equivClass2 into \p equivClass1.
-  ///
-  /// \note This will delete \p equivClass2 after migrating its members to
-  /// \p equivClass1.
-  void mergeEquivalenceClasses(EquivalenceClass *equivClass1,
-                               const EquivalenceClass *equivClass2);
-
-  /// The result of comparing two resolved types targeting a single equivalence
-  /// class, in terms of their relative impact on solving the system.
-  enum class ResolvedTypeComparisonResult {
-    /// The first resolved type is a better choice than the second one.
-    Better,
-
-    /// The first resolved type is an equivalent or worse choice than the
-    /// second one.
-    EquivalentOrWorse,
-
-    /// Both resolved types are concrete and mutually exclusive.
-    Ambiguity
-  };
-
-  /// Compare the given resolved types as targeting a single equivalence class,
-  /// in terms of the their relative impact on solving the system.
-  static ResolvedTypeComparisonResult compareResolvedTypes(Type ty1, Type ty2);
-};
-
 /// Captures the state needed to infer associated types.
 class AssociatedTypeInference {
   /// The type checker we'll need to validate declarations etc.
@@ -1027,7 +953,7 @@ class AssociatedTypeInference {
     typeWitnesses;
 
   /// Information about a failed, defaulted associated type.
-  const AssociatedTypeDecl *failedDefaultedAssocType = nullptr;
+  AssociatedTypeDecl *failedDefaultedAssocType = nullptr;
   Type failedDefaultedWitness;
   CheckTypeWitnessResult failedDefaultedResult;
 
@@ -1076,20 +1002,23 @@ class AssociatedTypeInference {
     ConformanceChecker &checker,
     const llvm::SetVector<AssociatedTypeDecl *> &assocTypes);
 
+  /// Compute a "fixed" type witness for an associated type, e.g.,
+  /// if the refined protocol requires it to be equivalent to some other type.
+  Type computeFixedTypeWitness(AssociatedTypeDecl *assocType);
+
   /// Compute the default type witness from an associated type default,
   /// if there is one.
-  Optional<std::pair<AssociatedTypeDecl *, Type>>
-  computeDefaultTypeWitness(AssociatedTypeDecl *assocType) const;
+  Optional<AbstractTypeWitness>
+  computeDefaultTypeWitness(AssociatedTypeDecl *assocType);
 
   /// Compute the "derived" type witness for an associated type that is
   /// known to the compiler.
   std::pair<Type, TypeDecl *>
   computeDerivedTypeWitness(AssociatedTypeDecl *assocType);
 
-  /// Collect abstract type witnesses and feed them to the given system.
-  void collectAbstractTypeWitnesses(
-      TypeWitnessSystem &system,
-      ArrayRef<AssociatedTypeDecl *> unresolvedAssocTypes) const;
+  /// Compute a type witness without using a specific potential witness.
+  Optional<AbstractTypeWitness>
+  computeAbstractTypeWitness(AssociatedTypeDecl *assocType);
 
   /// Substitute the current type witnesses into the given interface type.
   Type substCurrentTypeWitnesses(Type type);
@@ -1108,12 +1037,14 @@ class AssociatedTypeInference {
   /// requirements of the given constrained extension.
   bool checkConstrainedExtension(ExtensionDecl *ext);
 
-  /// Attempt to infer abstract type witnesses for the given set of associated
-  /// types.
+  /// Validate the current tentative solution represented by \p typeWitnesses
+  /// and attempt to resolve abstract type witnesses for associated types that
+  /// could not be inferred otherwise.
   ///
   /// \returns \c nullptr, or the associated type that failed.
-  AssociatedTypeDecl *inferAbstractTypeWitnesses(
-      ArrayRef<AssociatedTypeDecl *> unresolvedAssocTypes, unsigned reqDepth);
+  AssociatedTypeDecl *
+  completeSolution(ArrayRef<AssociatedTypeDecl *> unresolvedAssocTypes,
+                   unsigned reqDepth);
 
   /// Top-level operation to find solutions for the given unresolved
   /// associated types.
diff --git a/lib/Sema/TypeCheckProtocolInference.cpp b/lib/Sema/TypeCheckProtocolInference.cpp
index f23577740a430..ea0e9a3c0fa0c 100644
--- a/lib/Sema/TypeCheckProtocolInference.cpp
+++ b/lib/Sema/TypeCheckProtocolInference.cpp
@@ -44,6 +44,25 @@ STATISTIC(NumDuplicateSolutionStates,
 
 using namespace swift;
 
+AbstractTypeWitness AbstractTypeWitness::forFixed(AssociatedTypeDecl *assocType,
+                                                  Type type) {
+  return AbstractTypeWitness(AbstractTypeWitnessKind::Fixed, assocType, type,
+                             nullptr);
+}
+
+AbstractTypeWitness
+AbstractTypeWitness::forDefault(AssociatedTypeDecl *assocType, Type type,
+                                AssociatedTypeDecl *defaultedAssocType) {
+  return AbstractTypeWitness(AbstractTypeWitnessKind::Default, assocType, type,
+                             defaultedAssocType);
+}
+
+AbstractTypeWitness
+AbstractTypeWitness::forGenericParam(AssociatedTypeDecl *assocType, Type type) {
+  return AbstractTypeWitness(AbstractTypeWitnessKind::GenericParam, assocType,
+                             type, nullptr);
+}
+
 void InferredAssociatedTypesByWitness::dump() const {
   dump(llvm::errs(), 0);
 }
@@ -798,9 +817,58 @@ AssociatedTypeDecl *AssociatedTypeInference::findDefaultedAssociatedType(
   return results.size() == 1 ? results.front() : nullptr;
 }
 
-Optional<std::pair<AssociatedTypeDecl *, Type>>
+Type AssociatedTypeInference::computeFixedTypeWitness(
+                                            AssociatedTypeDecl *assocType) {
+  Type resultType;
+
+  // Look at all of the inherited protocols to determine whether they
+  // require a fixed type for this associated type.
+  for (auto conformedProto : adoptee->getAnyNominal()->getAllProtocols()) {
+    if (conformedProto != assocType->getProtocol() &&
+        !conformedProto->inheritsFrom(assocType->getProtocol()))
+      continue;
+
+    auto sig = conformedProto->getGenericSignature();
+
+    // FIXME: The RequirementMachine will assert on re-entrant construction.
+    // We should find a more principled way of breaking this cycle.
+    if (ctx.isRecursivelyConstructingRequirementMachine(sig.getCanonicalSignature()) ||
+        ctx.isRecursivelyConstructingRequirementMachine(conformedProto) ||
+        conformedProto->isComputingRequirementSignature())
+      continue;
+
+    auto selfTy = conformedProto->getSelfInterfaceType();
+    if (!sig->requiresProtocol(selfTy, assocType->getProtocol()))
+      continue;
+
+    auto structuralTy = DependentMemberType::get(selfTy, assocType->getName());
+    const auto ty = sig.getCanonicalTypeInContext(structuralTy);
+
+    // A dependent member type with an identical base and name indicates that
+    // the protocol does not same-type constrain it in any way; move on to
+    // the next protocol.
+    if (auto *const memberTy = ty->getAs<DependentMemberType>()) {
+      if (memberTy->getBase()->isEqual(selfTy) &&
+          memberTy->getName() == assocType->getName())
+        continue;
+    }
+
+    if (!resultType) {
+      resultType = ty;
+      continue;
+    }
+
+    // FIXME: Bailing out on ambiguity.
+    if (!resultType->isEqual(ty))
+      return Type();
+  }
+
+  return resultType;
+}
+
+Optional<AbstractTypeWitness>
 AssociatedTypeInference::computeDefaultTypeWitness(
-    AssociatedTypeDecl *assocType) const {
+    AssociatedTypeDecl *assocType) {
   // Go find a default definition.
   auto *const defaultedAssocType = findDefaultedAssociatedType(assocType);
   if (!defaultedAssocType)
@@ -814,7 +882,8 @@ AssociatedTypeInference::computeDefaultTypeWitness(
   if (defaultType->hasError())
     return None;
 
-  return std::make_pair(defaultedAssocType, defaultType);
+  return AbstractTypeWitness::forDefault(assocType, defaultType,
+                                         defaultedAssocType);
 }
 
 std::pair<Type, TypeDecl *>
@@ -845,53 +914,27 @@ AssociatedTypeInference::computeDerivedTypeWitness(
   return result;
 }
 
-void AssociatedTypeInference::collectAbstractTypeWitnesses(
-    TypeWitnessSystem &system,
-    ArrayRef<AssociatedTypeDecl *> unresolvedAssocTypes) const {
-  // First, look at all the protocols the adoptee conforms to and feed the
-  // same-type constraints in their requirement signatures to the system.
-  for (auto *const conformedProto :
-       adoptee->getAnyNominal()->getAllProtocols(/*sorted=*/true)) {
-    // FIXME: The RequirementMachine will assert on re-entrant construction.
-    // We should find a more principled way of breaking this cycle.
-    if (ctx.isRecursivelyConstructingRequirementMachine(
-            conformedProto->getGenericSignature().getCanonicalSignature()) ||
-        ctx.isRecursivelyConstructingRequirementMachine(conformedProto) ||
-        conformedProto->isComputingRequirementSignature())
-      continue;
-
-    for (const auto &req :
-         conformedProto->getRequirementSignature().getRequirements()) {
-      if (req.getKind() != RequirementKind::SameType) {
-        continue;
-      }
-
-      system.addSameTypeRequirement(req);
+Optional<AbstractTypeWitness>
+AssociatedTypeInference::computeAbstractTypeWitness(
+    AssociatedTypeDecl *assocType) {
+  // We don't have a type witness for this associated type, so go
+  // looking for more options.
+  if (Type concreteType = computeFixedTypeWitness(assocType))
+    return AbstractTypeWitness::forFixed(assocType, concreteType);
+
+  // If we can form a default type, do so.
+  if (const auto &typeWitness = computeDefaultTypeWitness(assocType))
+    return typeWitness;
+
+  // If there is a generic parameter of the named type, use that.
+  if (auto genericSig = dc->getGenericSignatureOfContext()) {
+    for (auto gp : genericSig.getInnermostGenericParams()) {
+      if (gp->getName() == assocType->getName())
+        return AbstractTypeWitness::forGenericParam(assocType, gp);
     }
   }
 
-  // If the same-type constraints weren't enough to resolve an associated type,
-  // look for more options.
-  for (auto *const assocType : unresolvedAssocTypes) {
-    if (system.hasResolvedTypeWitness(assocType->getName())) {
-      continue;
-    }
-
-    // If we find a default type definition, feed it to the system.
-    if (const auto declAndType = computeDefaultTypeWitness(assocType)) {
-      system.addDefaultTypeWitness(declAndType->second, declAndType->first);
-    } else {
-      // As a last resort, look for a generic parameter that matches the name
-      // of the associated type.
-      if (auto genericSig = dc->getGenericSignatureOfContext()) {
-        for (auto *gp : genericSig.getInnermostGenericParams()) {
-          if (gp->getName() == assocType->getName()) {
-            system.addTypeWitness(assocType->getName(), gp);
-          }
-        }
-      }
-    }
-  }
+  return None;
 }
 
 Type AssociatedTypeInference::substCurrentTypeWitnesses(Type type) {
@@ -1122,180 +1165,97 @@ bool AssociatedTypeInference::checkConstrainedExtension(ExtensionDecl *ext) {
   llvm_unreachable("unhandled result");
 }
 
-AssociatedTypeDecl *AssociatedTypeInference::inferAbstractTypeWitnesses(
+AssociatedTypeDecl *AssociatedTypeInference::completeSolution(
     ArrayRef<AssociatedTypeDecl *> unresolvedAssocTypes, unsigned reqDepth) {
-  if (unresolvedAssocTypes.empty()) {
-    return nullptr;
-  }
+  // Examine the solution for errors and attempt to compute abstract type
+  // witnesses for associated types that are still lacking an entry.
+  llvm::SmallVector<AbstractTypeWitness, 2> abstractTypeWitnesses;
+  for (auto *const assocType : unresolvedAssocTypes) {
+    const auto typeWitness = typeWitnesses.begin(assocType);
+    if (typeWitness != typeWitnesses.end()) {
+      // The solution contains an error.
+      if (typeWitness->first->hasError()) {
+        return assocType;
+      }
 
-  TypeWitnessSystem system(unresolvedAssocTypes);
-  collectAbstractTypeWitnesses(system, unresolvedAssocTypes);
+      continue;
+    }
 
-  if (ctx.LangOpts.DumpTypeWitnessSystems) {
-    system.dump(llvm::dbgs(), conformance);
-  }
+    // Try to compute the type without the aid of a specific potential witness.
+    if (const auto &typeWitness = computeAbstractTypeWitness(assocType)) {
+      // Record the type witness immediately to make it available
+      // for substitutions into other tentative type witnesses.
+      typeWitnesses.insert(assocType, {typeWitness->getType(), reqDepth});
 
-  // If we couldn't resolve an associated type, bail out.
-  for (auto *assocType : unresolvedAssocTypes) {
-    if (!system.hasResolvedTypeWitness(assocType->getName())) {
-      return assocType;
+      abstractTypeWitnesses.push_back(std::move(typeWitness.getValue()));
+      continue;
     }
-  }
 
-  // Record the tentative type witnesses to make them available during
-  // substitutions.
-  for (auto *assocType : unresolvedAssocTypes) {
-    typeWitnesses.insert(
-        assocType,
-        {system.getResolvedTypeWitness(assocType->getName()), reqDepth});
+    // The solution is incomplete.
+    return assocType;
   }
 
-  // Check each abstract type witness against the generic requirements on the
-  // corresponding associated type.
-  //
-  // FIXME: Consider checking non-dependent type witnesses first. Checking in
-  // default order can lead to the creation and exposure of malformed types in
-  // diagnostics. For example, we would diagnose that 'G<Never>' (!) does not
-  // conform to 'Sequence' in the below.
-  //
-  // struct G<S: Sequence> {}
-  // protocol P {
-  //   associatedtype A: Sequence = G<B>
-  //   associatedtype B: Sequence = Never
-  // }
+  // Check each abstract type witness we computed against the generic
+  // requirements on the corresponding associated type.
   const auto substOptions = getSubstOptionsWithCurrentTypeWitnesses();
-  for (auto *const assocType : unresolvedAssocTypes) {
-    Type type = system.getResolvedTypeWitness(assocType->getName());
-    // Replace type parameters with other known or tentative type witnesses.
+  for (const auto &witness : abstractTypeWitnesses) {
+    Type type = witness.getType();
     if (type->hasTypeParameter()) {
-      // FIXME: We should find a better way to detect and reason about these
-      // cyclic solutions so that we can spot them earlier and express them in
-      // diagnostics.
-      llvm::SmallPtrSet<AssociatedTypeDecl *, 4> circularityCheck;
-      circularityCheck.insert(assocType);
-
-      std::function<Type(Type)> substCurrentTypeWitnesses;
-      substCurrentTypeWitnesses = [&](Type ty) -> Type {
-        if (auto *gp = ty->getAs<GenericTypeParamType>()) {
-          if (isa<ProtocolDecl>(gp->getDecl()->getDeclContext()->getAsDecl())) {
-            return adoptee;
-          }
-
-          return ty;
-        }
-
-        auto *const dmt = ty->getAs<DependentMemberType>();
-        if (!dmt) {
-          return ty;
-        }
-
-        const auto substBase =
-            dmt->getBase().transform(substCurrentTypeWitnesses);
-        if (!substBase) {
-          return nullptr;
-        }
-
-        // If the transformed base has the same nominal as the adoptee, we may
-        // need to look up a tentative type witness. Otherwise, just substitute
-        // the base.
-        if (substBase->getAnyNominal() != adoptee->getAnyNominal()) {
-          return dmt->substBaseType(dc->getParentModule(), substBase);
-        }
-
-        auto *assocTy = dmt->getAssocType();
-        assert(
-            assocTy &&
-            "found structural DependentMemberType in tentative type witness");
-
-        // Intercept recursive solutions.
-        if (!circularityCheck.insert(assocTy).second) {
-          return nullptr;
-        }
-        SWIFT_DEFER { circularityCheck.erase(dmt->getAssocType()); };
-
-        if (assocTy->getProtocol() == proto) {
-          // We have the associated type we need.
-        } else if (proto->inheritsFrom(assocTy->getProtocol())) {
-          // See if there is an associated type with the same name in our
-          // protocol. If there isn't, keep the original associated type:
-          // we'll be falling back to a base substitution.
-          if (auto *decl = proto->getAssociatedType(assocTy->getName())) {
-            assocTy = decl;
-          }
-        }
-
-        // Find the type witness for this associated type.
-        Type tyWitness;
-        if (assocTy->getProtocol() == proto && typeWitnesses.count(assocTy)) {
-          tyWitness = typeWitnesses.begin(assocTy)->first;
-
-          // A tentative type witness may contain a 'Self'-rooted type
-          // parameter,
-          // FIXME: or a weird concrete-type-rooted dependent member type
-          // coming from inference via a value witness. Make sure we sort these
-          // out so that we don't break any subst() invariants.
-          if (tyWitness->hasTypeParameter() ||
-              tyWitness->hasDependentMember()) {
-            tyWitness = tyWitness.transform(substCurrentTypeWitnesses);
-          }
-
-          if (tyWitness) {
-            // HACK: Those inferred via value witnesses are eagerly mapped into
-            // context. For now, do the same for abstract type witnesses and
-            // handle archetypes.
-            if (tyWitness->hasArchetype()) {
-              tyWitness = tyWitness->mapTypeOutOfContext();
-            }
+      if (witness.getKind() == AbstractTypeWitnessKind::GenericParam) {
+        type = type = dc->mapTypeIntoContext(type);
+      } else {
+        // Replace type parameters with other known or tentative type witnesses.
+        type = type.subst(
+            [&](SubstitutableType *type) {
+              if (type->isEqual(proto->getSelfInterfaceType()))
+                return adoptee;
 
-            // If the transformed base is specialized, apply substitutions.
-            if (tyWitness->hasTypeParameter()) {
-              const auto conf = dc->getParentModule()->lookupConformance(
-                  substBase, assocTy->getProtocol(), /*allowMissing=*/true);
-              if (auto *specialized = dyn_cast<SpecializedProtocolConformance>(
-                      conf.getConcrete())) {
-                tyWitness = tyWitness.subst(specialized->getSubstitutionMap());
-              }
-            }
-          }
-        } else {
-          // The associated type has a recorded type witness, or comes from a
-          // different, possibly unrelated protocol; fall back to a base
-          // substitution to find the type witness.
-          tyWitness =
-              DependentMemberType::get(proto->getSelfInterfaceType(), assocTy)
-                  ->substBaseType(dc->getParentModule(), substBase);
+              return Type();
+            },
+            LookUpConformanceInModule(dc->getParentModule()), substOptions);
+
+        // If the substitution produced an error, we're done.
+        if (type->hasError())
+          return witness.getAssocType();
+
+        // FIXME: If mapping into context yields an error, or we still have a
+        // type parameter despite not having a generic environment, then a type
+        // parameter was sent to a tentative type witness that itself is a type
+        // parameter, and the solution is cyclic, e.g. { A := B.A, B := A.B },
+        // or beyond the current algorithm, e.g.
+        // protocol P {
+        //   associatedtype A = B
+        //   associatedtype B = C
+        //   associatedtype C = Int
+        // }
+        // struct Conformer: P {}
+        if (dc->getGenericEnvironmentOfContext()) {
+          type = dc->mapTypeIntoContext(type);
+
+          if (type->hasError())
+            return witness.getAssocType();
+        } else if (type->hasTypeParameter()) {
+          return witness.getAssocType();
         }
-
-        return tyWitness;
-      };
-
-      type = type.transform(substCurrentTypeWitnesses);
-
-      // If substitution failed, give up.
-      if (!type || type->hasError())
-        return assocType;
-
-      type = dc->mapTypeIntoContext(type);
+      }
     }
 
-    if (const auto failed =
-            checkTypeWitness(type, assocType, conformance, substOptions)) {
+    if (const auto &failed = checkTypeWitness(type, witness.getAssocType(),
+                                              conformance, substOptions)) {
       // We failed to satisfy a requirement. If this is a default type
       // witness failure and we haven't seen one already, write it down.
-      auto *defaultedAssocType =
-          system.getDefaultedAssocType(assocType->getName());
-      if (defaultedAssocType && !failedDefaultedAssocType &&
-          !failed.isError()) {
-        failedDefaultedAssocType = defaultedAssocType;
+      if (witness.getKind() == AbstractTypeWitnessKind::Default &&
+          !failedDefaultedAssocType && !failed.isError()) {
+        failedDefaultedAssocType = witness.getDefaultedAssocType();
         failedDefaultedWitness = type;
         failedDefaultedResult = std::move(failed);
       }
 
-      return assocType;
+      return witness.getAssocType();
     }
 
-    // Update the entry for this associated type.
-    typeWitnesses.insert(assocType, {type, reqDepth});
+    // Update the solution entry.
+    typeWitnesses.insert(witness.getAssocType(), {type, reqDepth});
   }
 
   return nullptr;
@@ -1325,28 +1285,9 @@ void AssociatedTypeInference::findSolutionsRec(
     // Introduce a hash table scope; we may add type witnesses here.
     TypeWitnessesScope typeWitnessesScope(typeWitnesses);
 
-    // Filter out the associated types that remain unresolved.
-    SmallVector<AssociatedTypeDecl *, 4> stillUnresolved;
-    for (auto *const assocType : unresolvedAssocTypes) {
-      const auto typeWitness = typeWitnesses.begin(assocType);
-      if (typeWitness == typeWitnesses.end()) {
-        stillUnresolved.push_back(assocType);
-      } else {
-        // If an erroneous type witness has already been recorded for one of
-        // the associated types, give up.
-        if (typeWitness->first->hasError()) {
-          if (!missingTypeWitness)
-            missingTypeWitness = assocType;
-
-          return;
-        }
-      }
-    }
-
-    // Attempt to infer abstract type witnesses for associated types that
-    // could not be resolved otherwise.
+    // Validate and complete the solution.
     if (auto *const assocType =
-            inferAbstractTypeWitnesses(stillUnresolved, reqDepth)) {
+            completeSolution(unresolvedAssocTypes, reqDepth)) {
       // The solution is decisively incomplete; record the associated type
       // we failed on and bail out.
       if (!missingTypeWitness)
@@ -1357,7 +1298,6 @@ void AssociatedTypeInference::findSolutionsRec(
 
     ++NumSolutionStates;
 
-    // Validate and complete the solution.
     // Fold the dependent member types within this type.
     for (auto assocType : proto->getAssociatedTypeMembers()) {
       if (conformance->hasTypeWitness(assocType))
@@ -2153,291 +2093,6 @@ auto AssociatedTypeInference::solve(ConformanceChecker &checker)
   return None;
 }
 
-void TypeWitnessSystem::EquivalenceClass::setResolvedType(Type ty) {
-  assert(ty && "cannot resolve to a null type");
-  assert(!isAmbiguous() && "must not set resolved type when ambiguous");
-
-  ResolvedTyAndIsAmbiguous.setPointer(ty);
-}
-
-TypeWitnessSystem::TypeWitnessSystem(
-    ArrayRef<AssociatedTypeDecl *> assocTypes) {
-  for (auto *assocType : assocTypes) {
-    this->TypeWitnesses.try_emplace(assocType->getName());
-  }
-}
-
-TypeWitnessSystem::~TypeWitnessSystem() {
-  for (auto *equivClass : this->EquivalenceClasses) {
-    delete equivClass;
-  }
-}
-
-bool TypeWitnessSystem::hasResolvedTypeWitness(Identifier name) const {
-  return (bool)getResolvedTypeWitness(name);
-}
-
-Type TypeWitnessSystem::getResolvedTypeWitness(Identifier name) const {
-  assert(this->TypeWitnesses.count(name));
-
-  if (auto *equivClass = this->TypeWitnesses.lookup(name).EquivClass) {
-    return equivClass->getResolvedType();
-  }
-
-  return Type();
-}
-
-const AssociatedTypeDecl *
-TypeWitnessSystem::getDefaultedAssocType(Identifier name) const {
-  assert(this->TypeWitnesses.count(name));
-
-  return this->TypeWitnesses.lookup(name).DefaultedAssocType;
-}
-
-void TypeWitnessSystem::addTypeWitness(Identifier name, Type type) {
-  assert(this->TypeWitnesses.count(name));
-
-  if (const auto *depTy = type->getAs<DependentMemberType>()) {
-    // If the type corresponds to a name variable in the system, form an
-    // equivalence between variables.
-    if (depTy->getBase()->is<GenericTypeParamType>()) {
-      if (this->TypeWitnesses.count(depTy->getName())) {
-        return addEquivalence(name, depTy->getName());
-      }
-    } else {
-      while (depTy->getBase()->is<DependentMemberType>()) {
-        depTy = depTy->getBase()->castTo<DependentMemberType>();
-      }
-
-      // Equivalences of the form 'Self.X == Self.X.*' do not contribute
-      // to solving the system, so just ignore them.
-      if (name == depTy->getName()) {
-        return;
-      }
-    }
-  }
-
-  auto &tyWitness = this->TypeWitnesses[name];
-
-  // Assume that the type resolves the equivalence class.
-  if (tyWitness.EquivClass) {
-    // Nothing else to do if the equivalence class had been marked as ambiguous.
-    if (tyWitness.EquivClass->isAmbiguous()) {
-      return;
-    }
-
-    // If we already have a resolved type, keep going only if the new one is
-    // a better choice.
-    const Type currResolvedTy = tyWitness.EquivClass->getResolvedType();
-    if (currResolvedTy) {
-      switch (compareResolvedTypes(type, currResolvedTy)) {
-      case ResolvedTypeComparisonResult::Better:
-        break;
-      case ResolvedTypeComparisonResult::EquivalentOrWorse:
-        return;
-      case ResolvedTypeComparisonResult::Ambiguity:
-        // Mark the equivalence class as ambiguous and give up.
-        tyWitness.EquivClass->setAmbiguous();
-        return;
-      }
-    }
-  }
-
-  // If we can find an existing equivalence class for this type, use it.
-  for (auto *const equivClass : this->EquivalenceClasses) {
-    if (equivClass->getResolvedType() &&
-        equivClass->getResolvedType()->isEqual(type)) {
-      if (tyWitness.EquivClass) {
-        mergeEquivalenceClasses(equivClass, tyWitness.EquivClass);
-      } else {
-        tyWitness.EquivClass = equivClass;
-      }
-
-      return;
-    }
-  }
-
-  if (tyWitness.EquivClass) {
-    tyWitness.EquivClass->setResolvedType(type);
-  } else {
-    auto *equivClass = new EquivalenceClass(type);
-    this->EquivalenceClasses.insert(equivClass);
-
-    tyWitness.EquivClass = equivClass;
-  }
-}
-
-void TypeWitnessSystem::addDefaultTypeWitness(
-    Type type, const AssociatedTypeDecl *defaultedAssocType) {
-  const auto name = defaultedAssocType->getName();
-  assert(this->TypeWitnesses.count(name));
-
-  auto &tyWitness = this->TypeWitnesses[name];
-  assert(!hasResolvedTypeWitness(name) && "already resolved a type witness");
-  assert(!tyWitness.DefaultedAssocType &&
-         "already recorded a default type witness");
-
-  // Set the defaulted associated type.
-  tyWitness.DefaultedAssocType = defaultedAssocType;
-
-  // Record the type witness.
-  addTypeWitness(name, type);
-}
-
-void TypeWitnessSystem::addSameTypeRequirement(const Requirement &req) {
-  assert(req.getKind() == RequirementKind::SameType);
-
-  auto *const depTy1 = req.getFirstType()->getAs<DependentMemberType>();
-  auto *const depTy2 = req.getSecondType()->getAs<DependentMemberType>();
-
-  // Equivalences other than 'Self.X == ...' (or '... == Self.X'), where
-  // 'X' is a name variable in this system, do not contribute to solving
-  // the system.
-  if (depTy1 && depTy1->getBase()->is<GenericTypeParamType>() &&
-      this->TypeWitnesses.count(depTy1->getName())) {
-    addTypeWitness(depTy1->getName(), req.getSecondType());
-  } else if (depTy2 && depTy2->getBase()->is<GenericTypeParamType>() &&
-             this->TypeWitnesses.count(depTy2->getName())) {
-    addTypeWitness(depTy2->getName(), req.getFirstType());
-  }
-}
-
-void TypeWitnessSystem::dump(
-    llvm::raw_ostream &out,
-    const NormalProtocolConformance *conformance) const {
-  llvm::SmallVector<Identifier, 4> sortedNames;
-  sortedNames.reserve(this->TypeWitnesses.size());
-
-  for (const auto &pair : this->TypeWitnesses) {
-    sortedNames.push_back(pair.first);
-  }
-
-  // Deterministic ordering.
-  llvm::array_pod_sort(sortedNames.begin(), sortedNames.end(),
-                       [](const Identifier *lhs, const Identifier *rhs) -> int {
-                         return lhs->compare(*rhs);
-                       });
-
-  out << "Abstract type witness system for conformance"
-      << " of " << conformance->getType() << " to "
-      << conformance->getProtocol()->getName() << ": {\n";
-
-  for (const auto &name : sortedNames) {
-    out.indent(2) << name << " => ";
-
-    const auto *eqClass = this->TypeWitnesses.lookup(name).EquivClass;
-    if (eqClass) {
-      if (eqClass->getResolvedType()) {
-        out << eqClass->getResolvedType();
-      } else if (eqClass->isAmbiguous()) {
-        out << "(ambiguous)";
-      } else {
-        out << "(unresolved)";
-      }
-    } else {
-      out << "(unresolved)";
-    }
-
-    if (eqClass) {
-      out << ", " << eqClass;
-    }
-    out << "\n";
-  }
-  out << "}\n";
-}
-
-void TypeWitnessSystem::addEquivalence(Identifier name1, Identifier name2) {
-  assert(this->TypeWitnesses.count(name1));
-  assert(this->TypeWitnesses.count(name2));
-
-  if (name1 == name2) {
-    return;
-  }
-
-  auto &tyWitness1 = this->TypeWitnesses[name1];
-  auto &tyWitness2 = this->TypeWitnesses[name2];
-
-  // If both candidates are associated with existing equivalence classes,
-  // merge them.
-  if (tyWitness1.EquivClass && tyWitness2.EquivClass) {
-    mergeEquivalenceClasses(tyWitness1.EquivClass, tyWitness2.EquivClass);
-    return;
-  }
-
-  if (tyWitness1.EquivClass) {
-    tyWitness2.EquivClass = tyWitness1.EquivClass;
-  } else if (tyWitness2.EquivClass) {
-    tyWitness1.EquivClass = tyWitness2.EquivClass;
-  } else {
-    // Neither has an associated equivalence class.
-    auto *equivClass = new EquivalenceClass(nullptr);
-    this->EquivalenceClasses.insert(equivClass);
-
-    tyWitness1.EquivClass = equivClass;
-    tyWitness2.EquivClass = equivClass;
-  }
-}
-
-void TypeWitnessSystem::mergeEquivalenceClasses(
-    EquivalenceClass *equivClass1, const EquivalenceClass *equivClass2) {
-  assert(equivClass1 && equivClass2);
-  if (equivClass1 == equivClass2) {
-    return;
-  }
-
-  // Merge the second equivalence class into the first.
-  if (equivClass1->getResolvedType() && equivClass2->getResolvedType()) {
-    switch (compareResolvedTypes(equivClass2->getResolvedType(),
-                                 equivClass1->getResolvedType())) {
-    case ResolvedTypeComparisonResult::Better:
-      equivClass1->setResolvedType(equivClass2->getResolvedType());
-      break;
-    case ResolvedTypeComparisonResult::EquivalentOrWorse:
-      break;
-    case ResolvedTypeComparisonResult::Ambiguity:
-      equivClass1->setAmbiguous();
-      break;
-    }
-  } else if (equivClass1->isAmbiguous()) {
-    // Ambiguity is retained.
-  } else if (equivClass2->getResolvedType()) {
-    // Carry over the resolved type.
-    equivClass1->setResolvedType(equivClass2->getResolvedType());
-  } else if (equivClass2->isAmbiguous()) {
-    // Carry over ambiguity.
-    equivClass1->setAmbiguous();
-  }
-
-  // Migrate members of the second equivalence class to the first.
-  for (auto &pair : this->TypeWitnesses) {
-    if (pair.second.EquivClass == equivClass2) {
-      pair.second.EquivClass = equivClass1;
-    }
-  }
-
-  // Finally, dispose of the second equivalence class.
-  this->EquivalenceClasses.erase(const_cast<EquivalenceClass *>(equivClass2));
-  delete equivClass2;
-}
-
-TypeWitnessSystem::ResolvedTypeComparisonResult
-TypeWitnessSystem::compareResolvedTypes(Type ty1, Type ty2) {
-  assert(ty1 && ty2);
-  if (!ty1->isTypeParameter()) {
-    if (ty2->isTypeParameter()) {
-      // A concrete type is better than a type parameter.
-      return ResolvedTypeComparisonResult::Better;
-    } else if (!ty1->isEqual(ty2)) {
-      return ResolvedTypeComparisonResult::Ambiguity;
-    }
-  }
-
-  // Anything else is either equivalent (i.e. actually equal concrete types or
-  // type parameter vs. type parameter), or worse (i.e. type parameter vs.
-  // concrete type).
-  return ResolvedTypeComparisonResult::EquivalentOrWorse;
-}
-
 void ConformanceChecker::resolveTypeWitnesses() {
   // Attempt to infer associated type witnesses.
   AssociatedTypeInference inference(getASTContext(), Conformance);
diff --git a/test/decl/protocol/req/associated_type_inference_fixed_type.swift b/test/decl/protocol/req/associated_type_inference_fixed_type.swift
index 58125df977ce2..5bd2ed4ec65cc 100644
--- a/test/decl/protocol/req/associated_type_inference_fixed_type.swift
+++ b/test/decl/protocol/req/associated_type_inference_fixed_type.swift
@@ -1,29 +1,20 @@
 // RUN: %target-typecheck-verify-swift -requirement-machine-protocol-signatures=off
-// RUN: not %target-swift-frontend -typecheck -dump-type-witness-systems %s -requirement-machine-protocol-signatures=off 2>&1 | %FileCheck %s
+// RUN: not %target-swift-frontend -typecheck -dump-type-witness-systems %s -requirement-machine-protocol-signatures=off 2>&1
 
 // TODO: Get this to pass with  -requirement-machine-protocol-signatures=on.
 
 protocol P1 where A == Never {
   associatedtype A
 }
-// CHECK-LABEL: Abstract type witness system for conformance of S1 to P1: {
-// CHECK-NEXT: A => Never,
-// CHECK-NEXT: }
-struct S1: P1 {}
+struct S1: P1 {} // OK, A := Never
 
 protocol P2a {
   associatedtype A
 }
 protocol P2b: P2a where A == Never {}
 protocol P2c: P2b {}
-// CHECK-LABEL: Abstract type witness system for conformance of S2a to P2a: {
-// CHECK-NEXT: A => Never,
-// CHECK-NEXT: }
-struct S2a: P2b {}
-// CHECK-LABEL: Abstract type witness system for conformance of S2b to P2a: {
-// CHECK-NEXT: A => Never,
-// CHECK-NEXT: }
-struct S2b: P2c {}
+struct S2a: P2b {} // OK, A := Never
+struct S2b: P2c {} // OK, A := Never
 
 // Fixed type witnesses can reference dependent members.
 protocol P3a {
@@ -31,34 +22,21 @@ protocol P3a {
   associatedtype B
 }
 protocol P3b: P3a where A == [B] {}
-// CHECK-LABEL: Abstract type witness system for conformance of S3 to P3a: {
-// CHECK-NEXT: A => [Self.B],
-// CHECK-NEXT: }
-struct S3: P3b {
+struct S3: P3b { // OK, A := [Never], B := Never
   typealias B = Never
 }
 
-protocol P4a where A == [B] {
-  associatedtype A
-  associatedtype B
-}
-protocol P4b {}
-extension P4b {
+protocol P4 {}
+extension P4 {
   typealias B = Self
 }
-// CHECK-LABEL: Abstract type witness system for conformance of S4 to P4a: {
-// CHECK-NEXT: A => [Self.B],
-// CHECK-NEXT: }
-struct S4: P4a, P4b {}
+struct S4: P4, P3b {} // OK, A := [S4], B := S4
 
 // Self is a valid fixed type witness.
 protocol P5a {
   associatedtype A
 }
 protocol P5b: P5a where A == Self {}
-// CHECK-LABEL: Abstract type witness system for conformance of S5<X> to P5a: {
-// CHECK-NEXT: A => Self,
-// CHECK-NEXT: }
 struct S5<X>: P5b {} // OK, A := S5<X>
 
 
@@ -67,9 +45,6 @@ protocol P6 where A == Never { // expected-error {{same-type constraint type 'Ne
   // expected-note@+1 {{protocol requires nested type 'A}}
   associatedtype A: P6
 }
-// CHECK-LABEL: Abstract type witness system for conformance of S6 to P6: {
-// CHECK-NEXT: A => (unresolved){{$}}
-// CHECK-NEXT: }
 struct S6: P6 {} // expected-error {{type 'S6' does not conform to protocol 'P6'}}
 
 protocol P7a where A == Never {
@@ -78,25 +53,14 @@ protocol P7a where A == Never {
 // expected-error@+2 {{'Self.A' cannot be equal to both 'Bool' and 'Never'}}
 // expected-note@+1 {{same-type constraint 'Self.A' == 'Never' implied here}}
 protocol P7b: P7a where A == Bool {}
-// CHECK-LABEL: Abstract type witness system for conformance of S7 to P7a: {
-// CHECK-NEXT: A => Never,
-// CHECK-NEXT: }
 struct S7: P7b {}
 
-protocol P8a where A == Never {
-  associatedtype A // expected-note {{protocol requires nested type 'A'; do you want to add it?}}
-}
-protocol P8b where A == Bool {
+protocol P8 where A == Bool {
   associatedtype A
 }
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer to P8a: {
-  // CHECK-NEXT: A => (ambiguous),
-  // CHECK-NEXT: }
-  struct Conformer: P8a, P8b {}
-  // expected-error@-1 {{type 'Conformer' does not conform to protocol 'P8a'}}
-  // expected-error@-2 {{type 'Conformer' does not conform to protocol 'P8b'}}
-}
+// expected-error@+2 {{'P7a' requires the types 'S8.A' (aka 'Bool') and 'Never' be equivalent}}
+// expected-note@+1 {{requirement specified as 'Self.A' == 'Never' [with Self = S8]}}
+struct S8: P8, P7a {}
 
 protocol P9a where A == Never {
   associatedtype A
@@ -104,10 +68,7 @@ protocol P9a where A == Never {
 protocol P9b: P9a {
   associatedtype A
 }
-// CHECK-LABEL: Abstract type witness system for conformance of S9a to P9b: {
-// CHECK-NEXT: A => Never,
-// CHECK-NEXT: }
-struct S9a: P9b {}
+struct S9a: P9b {} // OK, A := Never
 // expected-error@+2 {{'P9a' requires the types 'S9b.A' (aka 'Bool') and 'Never' be equivalent}}
 // expected-note@+1 {{requirement specified as 'Self.A' == 'Never' [with Self = S9b]}}
 struct S9b: P9b {
@@ -118,42 +79,36 @@ struct S9c: P9b { // OK, S9c.A does not contradict Self.A == Never.
   typealias A = Sugar
 }
 
-protocol P10a where A == Never {
-  associatedtype A
-}
-protocol P10b {}
-extension P10b {
+protocol P10 {}
+extension P10 {
   typealias A = Bool
 }
 // FIXME: 'P10 extension.A' should not be considered a viable type witness;
 //  instead, the compiler should infer A := Never and synthesize S10.A.
-// expected-error@+2 {{'P10a' requires the types 'S10.A' (aka 'Bool') and 'Never' be equivalent}}
+// expected-error@+2 {{'P9a' requires the types 'S10.A' (aka 'Bool') and 'Never' be equivalent}}
 // expected-note@+1 {{requirement specified as 'Self.A' == 'Never' [with Self = S10]}}
-struct S10: P10b, P10a {}
+struct S10: P10, P9a {}
 
 protocol P11a {
   associatedtype A
 }
 protocol P11b: P11a where A == Never {}
 protocol Q11 {
-  associatedtype A
-}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer to Q11: {
-  // CHECK-NEXT: A => Never,
-  // CHECK-NEXT: }
-  struct Conformer: Q11, P11b {}
+  associatedtype A // expected-note {{protocol requires nested type 'A'}}
 }
+// FIXME: Unrelated protocols with a matching associated type should
+//  also be considered when computing a fixed type witness.
+// expected-error@+3 {{type 'S11' does not conform to protocol 'Q11'}}
+// expected-error@+2 {{type 'S11' does not conform to protocol 'P11a'}}
+// expected-error@+1 {{type 'S11' does not conform to protocol 'P11b'}}
+struct S11: Q11, P11b {}
 
 protocol P12 where A == B {
   associatedtype A
   associatedtype B
   func foo(arg: A)
 }
-// CHECK-LABEL: Abstract type witness system for conformance of S12 to P12: {
-// CHECK-NEXT: B => Self.A,
-// CHECK-NEXT: }
-struct S12: P12 {
+struct S12: P12 { // OK, A == B == Never
   func foo(arg: Never) {}
 }
 
@@ -165,10 +120,7 @@ protocol P13b {
   associatedtype B
 }
 protocol P13c: P13a, P13b where A == B {}
-// CHECK-LABEL: Abstract type witness system for conformance of S13 to P13b: {
-// CHECK-NEXT: B => Self.A,
-// CHECK-NEXT: }
-struct S13: P13c {
+struct S13: P13c { // OK, A == B == Never
   func foo(arg: Never) {}
 }
 
@@ -176,700 +128,7 @@ protocol P14 {
   associatedtype A = Array<Self>
 }
 do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Outer<Element>.Conformer to P14: {
-  // CHECK-NEXT: A => Array<Self>,
-  // CHECK-NEXT: }
   struct Outer<Element> {
     struct Conformer: P14 {}
   }
 }
-
-protocol P15a {
-  associatedtype A
-  associatedtype B = Never
-}
-protocol P15b: P15a where A == B {}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer to P15a: {
-  // CHECK-NEXT: A => Never, [[EQUIV_CLASS:0x[0-9a-f]+]]
-  // CHECK-NEXT: B => Never, [[EQUIV_CLASS]]
-  // CHECK-NEXT: }
-  struct Conformer: P15b {}
-}
-
-protocol P16a where A == B {
-  associatedtype A
-  associatedtype B = Never
-}
-protocol P16b: P16a {}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer to P16a: {
-  // CHECK-NEXT: A => Never, [[EQUIV_CLASS:0x[0-9a-f]+]]
-  // CHECK-NEXT: B => Never, [[EQUIV_CLASS]]
-  // CHECK-NEXT: }
-  struct Conformer: P16b {}
-}
-
-protocol P17a where A == Never {
-  associatedtype A = B // expected-note {{protocol requires nested type 'A'; do you want to add it?}}
-  associatedtype B // expected-note {{protocol requires nested type 'B'; do you want to add it?}}
-}
-protocol P17b {
-  associatedtype A = B // expected-note {{protocol requires nested type 'A'; do you want to add it?}}
-  associatedtype B // expected-note {{protocol requires nested type 'B'; do you want to add it?}}
-}
-protocol P17c where A == Never {
-  associatedtype A
-  associatedtype B = A
-}
-protocol P17d {
-  associatedtype A = B
-  associatedtype B = Int
-}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer1 to P17a: {
-  // CHECK-NEXT: A => Never,
-  // CHECK-NEXT: B => (unresolved){{$}}
-  // CHECK-NEXT: }
-  struct Conformer1: P17a {} // expected-error {{type 'Conformer1' does not conform to protocol 'P17a'}}
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer2<A> to P17b: {
-  // CHECK-NEXT: A => (unresolved), [[EQUIV_CLASS:0x[0-9a-f]+]]
-  // CHECK-NEXT: B => (unresolved), [[EQUIV_CLASS]]
-  // CHECK-NEXT: }
-  struct Conformer2<A>: P17b {} // expected-error {{type 'Conformer2<A>' does not conform to protocol 'P17b'}}
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer3 to P17c: {
-  // CHECK-NEXT: A => Never, [[EQUIV_CLASS:0x[0-9a-f]+]]
-  // CHECK-NEXT: B => Never, [[EQUIV_CLASS]]
-  // CHECK-NEXT: }
-  struct Conformer3: P17c {}
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer4<A> to P17d: {
-  // CHECK-NEXT: A => Int, [[EQUIV_CLASS:0x[0-9a-f]+]]
-  // CHECK-NEXT: B => Int, [[EQUIV_CLASS]]
-  // CHECK-NEXT: }
-  struct Conformer4<A>: P17d {}
-}
-
-protocol P18 {
-  associatedtype A = B
-  associatedtype B = C
-  associatedtype C = (D) -> D
-  associatedtype D
-}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer<D> to P18: {
-  // CHECK-NEXT: A => (Self.D) -> Self.D, [[EQUIV_CLASS:0x[0-9a-f]+]]
-  // CHECK-NEXT: B => (Self.D) -> Self.D, [[EQUIV_CLASS]]
-  // CHECK-NEXT: C => (Self.D) -> Self.D, [[EQUIV_CLASS]]
-  // CHECK-NEXT: D => D,
-  // CHECK-NEXT: }
-  struct Conformer<D>: P18 {}
-}
-
-protocol P19 where Self == A {
-  associatedtype A
-  associatedtype B = (A, A)
-}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer to P19: {
-  // CHECK-NEXT: A => Self,
-  // CHECK-NEXT: B => (Self.A, Self.A),
-  // CHECK-NEXT: }
-  struct Conformer: P19 {}
-}
-
-protocol P20 where A == B.Element, B == B.SubSequence, C.Element == B.Element {
-  associatedtype A
-  associatedtype B: Collection
-  associatedtype C: Collection = Array<Character>
-}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer to P20: {
-  // CHECK-NEXT: A => Self.B.Element,
-  // CHECK-NEXT: C => Array<Character>,
-  // CHECK-NEXT: }
-  struct Conformer: P20 {
-    typealias B = Substring
-  }
-}
-
-protocol P21 where A == B {
-  associatedtype A
-  associatedtype B = C
-  associatedtype C
-}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer<C> to P21: {
-  // CHECK-NEXT: A => C, [[EQUIV_CLASS:0x[0-9a-f]+]]
-  // CHECK-NEXT: B => C, [[EQUIV_CLASS]]
-  // CHECK-NEXT: C => C, [[EQUIV_CLASS]]
-  // CHECK-NEXT: }
-  struct Conformer<C>: P21 {}
-}
-
-protocol P22 where A == B, C == D {
-  associatedtype A
-  associatedtype B
-  associatedtype C = B
-  associatedtype D
-}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer<A> to P22: {
-  // CHECK-NEXT: A => A, [[EQUIV_CLASS:0x[0-9a-f]+]]
-  // CHECK-NEXT: B => A, [[EQUIV_CLASS]]
-  // CHECK-NEXT: C => A, [[EQUIV_CLASS]]
-  // CHECK-NEXT: D => A, [[EQUIV_CLASS]]
-  // CHECK-NEXT: }
-  struct Conformer<A>: P22 {}
-}
-
-protocol P23 {
-  associatedtype A: P23 = B.A // expected-note 2 {{protocol requires nested type 'A'; do you want to add it?}}
-  associatedtype B: P23 = A.B // expected-note 2 {{protocol requires nested type 'B'; do you want to add it?}}
-}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer to P23: {
-  // CHECK-NEXT: A => Self.B.A,
-  // CHECK-NEXT: B => Self.A.B,
-  // CHECK-NEXT: }
-  struct Conformer: P23 {} // expected-error {{type 'Conformer' does not conform to protocol 'P23'}}
-  // CHECK-LABEL: Abstract type witness system for conformance of ConformerGeneric<T> to P23: {
-  // CHECK-NEXT: A => Self.B.A,
-  // CHECK-NEXT: B => Self.A.B,
-  // CHECK-NEXT: }
-  struct ConformerGeneric<T>: P23 {} // expected-error {{type 'ConformerGeneric<T>' does not conform to protocol 'P23'}}
-}
-
-protocol P24 where A == B.A {
-  associatedtype A: P24 // expected-note 2 {{protocol requires nested type 'A'; do you want to add it?}}
-  associatedtype B: P24 = A.B // expected-note 2 {{protocol requires nested type 'B'; do you want to add it?}}
-}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer to P24: {
-  // CHECK-NEXT: A => Self.B.A,
-  // CHECK-NEXT: B => Self.A.B,
-  // CHECK-NEXT: }
-  struct Conformer: P24 {} // expected-error {{type 'Conformer' does not conform to protocol 'P24'}}
-  // CHECK-LABEL: Abstract type witness system for conformance of ConformerGeneric<T> to P24: {
-  // CHECK-NEXT: A => Self.B.A,
-  // CHECK-NEXT: B => Self.A.B,
-  // CHECK-NEXT: }
-  struct ConformerGeneric<T>: P24 {} // expected-error {{type 'ConformerGeneric<T>' does not conform to protocol 'P24'}}
-}
-
-protocol P25a_1 where A == Int, B == C.Element {
-  associatedtype A
-  associatedtype B
-  associatedtype C: Sequence
-}
-protocol P25a_2 where A == C.Element, B == Int {
-  associatedtype A
-  associatedtype B
-  associatedtype C: Sequence
-}
-protocol P25b where A == B {
-  associatedtype A
-  associatedtype B
-}
-protocol P25c_1: P25a_1, P25b {}
-protocol P25c_2: P25a_2, P25b {}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer1<C> to P25a_1: {
-  // CHECK-NEXT: A => Int, [[EQUIV_CLASS:0x[0-9a-f]+]]
-  // CHECK-NEXT: B => Int, [[EQUIV_CLASS]]
-  // CHECK-NEXT: C => C,
-  // CHECK-NEXT: }
-  struct Conformer1<C: Sequence>: P25c_1 where C.Element == Int {}
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer2<C> to P25a_2: {
-  // CHECK-NEXT: A => Int, [[EQUIV_CLASS:0x[0-9a-f]+]]
-  // CHECK-NEXT: B => Int, [[EQUIV_CLASS]]
-  // CHECK-NEXT: C => C,
-  // CHECK-NEXT: }
-  struct Conformer2<C: Sequence>: P25c_2 where C.Element == Int {}
-}
-
-protocol P26 where C == B, F == G {
-  associatedtype A = Int
-  associatedtype B = A
-  associatedtype C
-
-  associatedtype D
-  associatedtype E = D
-
-  associatedtype F
-  associatedtype G = [B]
-}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer<D> to P26: {
-  // CHECK-NEXT: A => Int, [[EQUIV_CLASS_1:0x[0-9a-f]+]]
-  // CHECK-NEXT: B => Int, [[EQUIV_CLASS_1]]
-  // CHECK-NEXT: C => Int, [[EQUIV_CLASS_1]]
-  // CHECK-NEXT: D => D, [[EQUIV_CLASS_2:0x[0-9a-f]+]]
-  // CHECK-NEXT: E => D, [[EQUIV_CLASS_2]]
-  // CHECK-NEXT: F => [Self.B], [[EQUIV_CLASS_3:0x[0-9a-f]+]]
-  // CHECK-NEXT: G => [Self.B], [[EQUIV_CLASS_3]]
-  // CHECK-NEXT: }
-  struct Conformer<D>: P26 {}
-}
-
-protocol P27a where A == Int {
-  associatedtype A
-}
-protocol P27b where A == B.Element {
-  associatedtype A
-  associatedtype B: Sequence
-}
-protocol P27c_1: P27a, P27b {}
-protocol P27c_2: P27b, P27a {}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer1<B> to P27a: {
-  // CHECK-NEXT: A => Int,
-  // CHECK-NEXT: }
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer1<B> to P27b: {
-  // CHECK-NEXT: B => B,
-  // CHECK-NEXT: }
-  struct Conformer1<B: Sequence>: P27c_1 where B.Element == Int {}
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer2<B> to P27b: {
-  // CHECK-NEXT: A => Int,
-  // CHECK-NEXT: B => B,
-  // CHECK-NEXT: }
-  struct Conformer2<B: Sequence>: P27c_2 where B.Element == Int {}
-}
-
-protocol P28a where A == Int {
-  associatedtype A // expected-note 2 {{protocol requires nested type 'A'; do you want to add it?}}
-}
-protocol P28b where A == Bool {
-  associatedtype A
-}
-protocol P28c where A == Never {
-  associatedtype A
-}
-protocol Q28a: P28a, P28b {}
-// expected-error@-1 {{'Self.A' cannot be equal to both 'Bool' and 'Int'}}
-// expected-note@-2 {{same-type constraint 'Self.A' == 'Int' implied here}}
-protocol Q28b: P28a, P28b, P28c {}
-// expected-error@-1 {{'Self.A' cannot be equal to both 'Bool' and 'Int'}}
-// expected-error@-2 {{'Self.A' cannot be equal to both 'Never' and 'Int'}}
-// expected-note@-3 {{same-type constraint 'Self.A' == 'Int' implied here}}
-// expected-note@-4 {{same-type constraint 'Self.A' == 'Int' implied here}}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer1 to P28a: {
-  // CHECK-NEXT: A => (ambiguous),
-  // CHECK-NEXT: }
-  struct Conformer1: Q28a {}
-  // expected-error@-1 {{type 'Conformer1' does not conform to protocol 'P28a'}}
-  // expected-error@-2 {{type 'Conformer1' does not conform to protocol 'P28b'}}
-
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer2 to P28a: {
-  // CHECK-NEXT: A => (ambiguous),
-  // CHECK-NEXT: }
-  struct Conformer2: Q28b {}
-  // expected-error@-1 {{type 'Conformer2' does not conform to protocol 'P28a'}}
-  // expected-error@-2 {{type 'Conformer2' does not conform to protocol 'P28b'}}
-  // expected-error@-3 {{type 'Conformer2' does not conform to protocol 'P28c'}}
-}
-
-protocol P29a where A == Int {
-  associatedtype A // expected-note {{protocol requires nested type 'A'; do you want to add it?}}
-  associatedtype B // expected-note {{protocol requires nested type 'B'; do you want to add it?}}
-}
-protocol P29b where B == Never {
-  associatedtype B
-}
-protocol P29c where A == B {
-  associatedtype A // expected-note {{protocol requires nested type 'A'; do you want to add it?}}
-  associatedtype B // expected-note {{protocol requires nested type 'B'; do you want to add it?}}
-}
-protocol Q29a: P29a, P29b, P29c {}
-// expected-error@-1 {{'Self.B' cannot be equal to both 'Never' and 'Int'}}
-// expected-note@-2 {{same-type constraint 'Self.A' == 'Int' implied here}}
-protocol Q29b: P29c, P29a, P29b {}
-// expected-error@-1 {{'Self.B' cannot be equal to both 'Never' and 'Int'}}
-// expected-note@-2 {{same-type constraint 'Self.A' == 'Int' implied here}}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer1 to P29a: {
-  // CHECK-NEXT: A => (ambiguous), [[EQUIV_CLASS:0x[0-9a-f]+]]
-  // CHECK-NEXT: B => (ambiguous), [[EQUIV_CLASS]]
-  // CHECK-NEXT: }
-  struct Conformer1: Q29a {}
-  // expected-error@-1 {{type 'Conformer1' does not conform to protocol 'P29a'}}
-  // expected-error@-2 {{type 'Conformer1' does not conform to protocol 'P29b'}}
-  // expected-error@-3 {{type 'Conformer1' does not conform to protocol 'P29c'}}
-
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer2 to P29c: {
-  // CHECK-NEXT: A => (ambiguous), [[EQUIV_CLASS:0x[0-9a-f]+]]
-  // CHECK-NEXT: B => (ambiguous), [[EQUIV_CLASS]]
-  // CHECK-NEXT: }
-  struct Conformer2: Q29b {}
-  // expected-error@-1 {{type 'Conformer2' does not conform to protocol 'P29a'}}
-  // expected-error@-2 {{type 'Conformer2' does not conform to protocol 'P29b'}}
-  // expected-error@-3 {{type 'Conformer2' does not conform to protocol 'P29c'}}
-}
-
-protocol P30a where A == Int {
-  associatedtype A
-}
-protocol P30b where A == Never {
-  associatedtype A
-}
-protocol P30c where A == B {
-  associatedtype A // expected-note {{protocol requires nested type 'A'; do you want to add it?}}
-  associatedtype B // expected-note {{protocol requires nested type 'B'; do you want to add it?}}
-}
-protocol Q30: P30c, P30a, P30b {}
-// expected-error@-1 {{'Self.A' cannot be equal to both 'Never' and 'Int'}}
-// expected-note@-2 {{same-type constraint 'Self.A' == 'Int' implied here}}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer to P30c: {
-  // CHECK-NEXT: A => (ambiguous), [[EQUIV_CLASS:0x[0-9a-f]+]]
-  // CHECK-NEXT: B => (ambiguous), [[EQUIV_CLASS]]
-  // CHECK-NEXT: }
-  struct Conformer: Q30 {}
-  // expected-error@-1 {{type 'Conformer' does not conform to protocol 'P30a'}}
-  // expected-error@-2 {{type 'Conformer' does not conform to protocol 'P30b'}}
-  // expected-error@-3 {{type 'Conformer' does not conform to protocol 'P30c'}}
-}
-
-protocol P31a where B == Int {
-  associatedtype B
-}
-protocol P31b where B == Never {
-  associatedtype B
-}
-protocol P31c where B == A {
-  associatedtype A // expected-note {{protocol requires nested type 'A'; do you want to add it?}}
-  associatedtype B // expected-note {{protocol requires nested type 'B'; do you want to add it?}}
-}
-protocol Q31: P31c, P31a, P31b {}
-// expected-error@-1 {{'Self.B' cannot be equal to both 'Never' and 'Int'}}
-// expected-note@-2 {{same-type constraint 'Self.B' == 'Int' implied here}}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer to P31c: {
-  // CHECK-NEXT: A => (ambiguous), [[EQUIV_CLASS:0x[0-9a-f]+]]
-  // CHECK-NEXT: B => (ambiguous), [[EQUIV_CLASS]]
-  // CHECK-NEXT: }
-  struct Conformer: Q31 {}
-  // expected-error@-1 {{type 'Conformer' does not conform to protocol 'P31a'}}
-  // expected-error@-2 {{type 'Conformer' does not conform to protocol 'P31b'}}
-  // expected-error@-3 {{type 'Conformer' does not conform to protocol 'P31c'}}
-}
-
-protocol P32a where A == Int {
-  associatedtype A
-}
-protocol P32b where A == Bool {
-  associatedtype A
-}
-protocol P32c where B == Void {
-  associatedtype B
-}
-protocol P32d where B == Never {
-  associatedtype B
-}
-protocol P32e where A == B {
-  associatedtype A // expected-note {{protocol requires nested type 'A'; do you want to add it?}}
-  associatedtype B // expected-note {{protocol requires nested type 'B'; do you want to add it?}}
-}
-protocol Q32: P32e, P32a, P32b, P32c, P32d {}
-// expected-error@-1 {{'Self.B' cannot be equal to both 'Never' and 'Int'}}
-// expected-error@-2 {{'Self.B' cannot be equal to both 'Void' and 'Int'}}
-// expected-error@-3 {{'Self.A' cannot be equal to both 'Bool' and 'Int'}}
-// expected-note@-4 3 {{same-type constraint 'Self.A' == 'Int' implied here}}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer to P32e: {
-  // CHECK-NEXT: A => (ambiguous), [[EQUIV_CLASS:0x[0-9a-f]+]]
-  // CHECK-NEXT: B => (ambiguous), [[EQUIV_CLASS]]
-  // CHECK-NEXT: }
-  struct Conformer: Q32 {}
-  // expected-error@-1 {{type 'Conformer' does not conform to protocol 'P32a'}}
-  // expected-error@-2 {{type 'Conformer' does not conform to protocol 'P32b'}}
-  // expected-error@-3 {{type 'Conformer' does not conform to protocol 'P32c'}}
-  // expected-error@-4 {{type 'Conformer' does not conform to protocol 'P32d'}}
-  // expected-error@-5 {{type 'Conformer' does not conform to protocol 'P32e'}}
-}
-
-protocol P33a where A == Int {
-  associatedtype A
-}
-protocol P33b where A == Int {
-  associatedtype A
-}
-protocol Q33: P33a, P33b {}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer to P33a: {
-  // CHECK-NEXT: A => Int,
-  // CHECK-NEXT: }
-  struct Conformer: Q33 {}
-}
-
-protocol P34a {
-  associatedtype A = Void
-}
-protocol P34b {
-  associatedtype A = Never
-}
-protocol Q34a: P34a, P34b {}
-protocol Q34b: P34b, P34a {}
-protocol Q34c: P34a, P34b {
-  associatedtype A // expected-note {{protocol requires nested type 'A'; do you want to add it?}}
-}
-do {
-  // FIXME: should really be ambiguous (source-breaking)?
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer1 to P34a: {
-  // CHECK-NEXT: A => Void,
-  // CHECK-NEXT: }
-  struct Conformer1: Q34a {}
-
-  // FIXME: should really be ambiguous (source-breaking)?
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer2 to P34b: {
-  // CHECK-NEXT: A => Never,
-  // CHECK-NEXT: }
-  struct Conformer2: Q34b {}
-
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer3 to Q34c: {
-  // CHECK-NEXT: A => (unresolved){{$}}
-  // CHECK-NEXT: }
-  struct Conformer3: Q34c {} // expected-error {{type 'Conformer3' does not conform to protocol 'Q34c'}}
-}
-
-protocol P35 {
-  associatedtype A
-  associatedtype B = Array<C>
-  associatedtype C = Array<D>
-  associatedtype D = Array<A>
-}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer to P35: {
-  // CHECK-NEXT: B => Array<Self.C>,
-  // CHECK-NEXT: C => Array<Self.D>,
-  // CHECK-NEXT: D => Array<Self.A>,
-  // CHECK-NEXT: }
-  struct Conformer: P35 {
-    typealias A = Never
-  }
-  // CHECK-LABEL: Abstract type witness system for conformance of ConformerGeneric<A> to P35: {
-  // CHECK-NEXT: A => A,
-  // CHECK-NEXT: B => Array<Self.C>,
-  // CHECK-NEXT: C => Array<Self.D>,
-  // CHECK-NEXT: D => Array<Self.A>,
-  // CHECK-NEXT: }
-  struct ConformerGeneric<A>: P35 {}
-}
-
-struct G36<S: P36> {}
-protocol P36 {
-  // FIXME: Don't create and expose malformed types like 'G36<Never>' -- check
-  // non-dependent type witnesses first.
-  // expected-note@+1 {{default type 'G36<Never>' for associated type 'A' (from protocol 'P36') does not conform to 'P36'}}
-  associatedtype A: P36 = G36<B>
-  associatedtype B: P36 = Never
-}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer to P36: {
-  // CHECK-NEXT: A => G36<Self.B>,
-  // CHECK-NEXT: B => Never,
-  // CHECK-NEXT: }
-  struct Conformer: P36 {} // expected-error {{type 'Conformer' does not conform to protocol 'P36'}}
-}
-
-protocol P37a {
-  associatedtype A
-}
-protocol P37b {
-  associatedtype B : P37a
-  associatedtype C where C == B.A
-}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer1<C> to P37b: {
-  // CHECK-NEXT: C => Self.B.A,
-  // CHECK-NEXT: }
-  struct Conformer1<C>: P37b {
-    struct Inner: P37a { typealias A = C }
-
-    typealias B = Inner
-  }
-
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer2<T> to P37b: {
-  // CHECK-NEXT: C => Self.B.A,
-  // CHECK-NEXT: }
-  struct Conformer2<T>: P37b {
-    struct Inner: P37a { typealias A = T }
-
-    typealias B = Inner
-  }
-}
-
-protocol P38a {
-  associatedtype A
-}
-protocol P38b {
-  associatedtype B
-}
-protocol P38c: P38a, P38b where A == B {}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer<T> to P38b: {
-  // CHECK-NEXT: B => Self.A,
-  // CHECK-NEXT: }
-  struct Conformer<T>: P38c {
-    typealias A = Self
-  }
-}
-
-protocol P39 {
-  associatedtype A: P39
-  associatedtype B = A.C
-  associatedtype C = Never
-}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer to P39: {
-  // CHECK-NEXT: B => Self.A.C,
-  // CHECK-NEXT: C => Never,
-  // CHECK-NEXT: }
-  struct Conformer: P39 {
-    typealias A = Self
-  }
-}
-
-protocol P40a {
-  associatedtype A
-  associatedtype B = (A, A)
-}
-protocol P40b: P40a {
-  override associatedtype A = Int
-}
-protocol P40c: P40b {
-  override associatedtype A
-  override associatedtype B
-}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer to P40c: {
-  // CHECK-NEXT: A => Int,
-  // CHECK-NEXT: B => (Self.A, Self.A),
-  // CHECK-NEXT: }
-  struct Conformer: P40c {}
-}
-
-protocol P41 {
-  associatedtype A where A == B.A // expected-note {{protocol requires nested type 'A'; do you want to add it?}}
-  associatedtype B: P41 = Self // expected-note {{protocol requires nested type 'B'; do you want to add it?}}
-}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer to P41: {
-  // CHECK-NEXT: A => Self.B.A,
-  // CHECK-NEXT: B => Self,
-  // CHECK-NEXT: }
-  struct Conformer: P41 {} // expected-error{{type 'Conformer' does not conform to protocol 'P41'}}
-}
-
-protocol P42a {
-  associatedtype B: P42b
-}
-protocol P42b: P42a {
-  associatedtype A = B.A
-}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer<B> to P42b: {
-  // CHECK-NEXT: A => Self.B.A,
-  // CHECK-NEXT: }
-
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer<B> to P42a: {
-  // CHECK-NEXT: B => B,
-  // CHECK-NEXT: }
-  struct Conformer<B: P42b>: P42b {}
-}
-
-protocol P43a {
-  associatedtype A: P43a
-  associatedtype B
-}
-protocol P43b: P43a {
-  associatedtype C where C == A.B
-}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer<B> to P43b: {
-  // CHECK-NEXT: C => Self.A.B,
-  // CHECK-NEXT: }
-
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer<B> to P43a: {
-  // CHECK-NEXT: B => B,
-  // CHECK-NEXT: }
-  struct Conformer<B: P43a>: P43b {
-    typealias A = Conformer<B.A>
-  }
-}
-
-protocol P44 {
-  associatedtype A: P44
-  associatedtype B
-  associatedtype C where C == A.B
-}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer1<T> to P44: {
-  // CHECK-NEXT: C => Self.A.B,
-  // CHECK-NEXT: }
-  struct Conformer1<T: P44>: P44 {
-    typealias B = T.A
-    typealias A = Conformer1<T.A>
-  }
-
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer2<B> to P44: {
-  // CHECK-NEXT: B => B,
-  // CHECK-NEXT: C => Self.A.B,
-  // CHECK-NEXT: }
-  struct Conformer2<B: P44>: P44 {
-    typealias A = Conformer2<B.A>
-  }
-
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer3<B> to P44: {
-  // CHECK-NEXT: B => B,
-  // CHECK-NEXT: C => Self.A.B,
-  // CHECK-NEXT: }
-  struct Conformer3<B>: P44 {
-    typealias A = Conformer3<Int>
-  }
-}
-
-protocol P45 {
-  associatedtype A
-  associatedtype B: P45 = Conformer45<D>
-  associatedtype C where C == B.A
-  associatedtype D = Never
-}
-// CHECK-LABEL: Abstract type witness system for conformance of Conformer45<A> to P45: {
-// CHECK-NEXT: A => A,
-// CHECK-NEXT: B => Conformer45<Self.D>,
-// CHECK-NEXT: C => Self.B.A,
-// CHECK-NEXT: D => Never,
-// CHECK-NEXT: }
-struct Conformer45<A>: P45 {}
-
-protocol P46 {
-  associatedtype A: P46
-  associatedtype B
-  associatedtype C where C == A.B
-
-  func method(_: B)
-}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Conformer<T> to P46: {
-  // CHECK-NEXT: C => Self.A.B,
-  // CHECK-NEXT: }
-  struct Conformer<T: P46>: P46 {
-    typealias A = Conformer<T.A>
-
-    func method(_: T) {}
-  }
-}
-
-
-protocol P47 {
-  associatedtype A
-}
-do {
-  // CHECK-LABEL: Abstract type witness system for conformance of Outer<A>.Inner to P47: {
-  // CHECK-NEXT: A => A,
-  // CHECK-NEXT: }
-  struct Outer<A> {
-    struct Inner: P47 {}
-  }
-}
diff --git a/validation-test/compiler_crashers_2_fixed/sr11392.swift b/validation-test/compiler_crashers_2_fixed/sr11392.swift
index b8eec346bc921..449615a072272 100644
--- a/validation-test/compiler_crashers_2_fixed/sr11392.swift
+++ b/validation-test/compiler_crashers_2_fixed/sr11392.swift
@@ -1,7 +1,11 @@
 // RUN: %target-swift-frontend -verify -emit-ir %s
 
+// Ideally this would type check successfully; we should be able to
+// infer that X == Int using the same-type constraint 'A.X == X'.
+
 protocol P1 {
     associatedtype X
+    // expected-note@-1 {{protocol requires nested type 'X'; do you want to add it?}}
     associatedtype A: P2 where A.X == X
 }
 
@@ -19,5 +23,6 @@ extension S {
 
 
 extension S: P1 {}
+// expected-error@-1 {{type 'S' does not conform to protocol 'P1'}}
 
 print(S.X.self)