diff --git a/explorer/interpreter/BUILD b/explorer/interpreter/BUILD
index 41897e7b11f2..acdfa10046ec 100644
--- a/explorer/interpreter/BUILD
+++ b/explorer/interpreter/BUILD
@@ -208,11 +208,13 @@ cc_library(
     srcs = [
         "builtins.cpp",
         "impl_scope.cpp",
+        "matching_impl_set.cpp",
         "type_checker.cpp",
     ],
     hdrs = [
         "builtins.h",
         "impl_scope.h",
+        "matching_impl_set.h",
         "type_checker.h",
     ],
     deps = [
diff --git a/explorer/interpreter/impl_scope.cpp b/explorer/interpreter/impl_scope.cpp
index c3f8c6b114a4..6a215d239ab2 100644
--- a/explorer/interpreter/impl_scope.cpp
+++ b/explorer/interpreter/impl_scope.cpp
@@ -65,18 +65,17 @@ void ImplScope::AddParent(Nonnull<const ImplScope*> parent) {
   parent_scopes_.push_back(parent);
 }
 
-// Checks that `a_evaluated == b_evaluated` for the purpose of an equality
-// constraint. Produces an error if not.
-static auto CheckEqualOrDiagnose(SourceLocation source_loc,
-                                 Nonnull<const Value*> a_written,
-                                 Nonnull<const Value*> a_evaluated,
-                                 Nonnull<const Value*> b_written,
-                                 Nonnull<const Value*> b_evaluated,
-                                 Nonnull<const EqualityContext*> equality_ctx)
-    -> ErrorOr<Success> {
-  if (ValueEqual(a_evaluated, b_evaluated, equality_ctx)) {
-    return Success();
-  }
+// Diagnose that `a_evaluated != b_evaluated` for the purpose of an equality
+// constraint.
+static auto DiagnoseUnequalValues(SourceLocation source_loc,
+                                  Nonnull<const Value*> a_written,
+                                  Nonnull<const Value*> a_evaluated,
+                                  Nonnull<const Value*> b_written,
+                                  Nonnull<const Value*> b_evaluated,
+                                  Nonnull<const EqualityContext*> equality_ctx)
+    -> Error {
+  CARBON_CHECK(!ValueEqual(a_evaluated, b_evaluated, equality_ctx))
+      << "expected unequal values";
   auto error = ProgramError(source_loc);
   error << "constraint requires that " << *a_written;
   if (!ValueEqual(a_written, a_evaluated, std::nullopt)) {
@@ -96,10 +95,26 @@ auto ImplScope::Resolve(Nonnull<const Value*> constraint_type,
                         const TypeChecker& type_checker,
                         const Bindings& bindings) const
     -> ErrorOr<Nonnull<const Witness*>> {
+  CARBON_ASSIGN_OR_RETURN(
+      std::optional<Nonnull<const Witness*>> witness,
+      TryResolve(constraint_type, impl_type, source_loc, type_checker, bindings,
+                 /*diagnose_missing_impl=*/true));
+  CARBON_CHECK(witness) << "should have diagnosed missing impl";
+  return *witness;
+}
+
+auto ImplScope::TryResolve(Nonnull<const Value*> constraint_type,
+                           Nonnull<const Value*> impl_type,
+                           SourceLocation source_loc,
+                           const TypeChecker& type_checker,
+                           const Bindings& bindings,
+                           bool diagnose_missing_impl) const
+    -> ErrorOr<std::optional<Nonnull<const Witness*>>> {
   if (const auto* iface_type = dyn_cast<InterfaceType>(constraint_type)) {
     iface_type =
         cast<InterfaceType>(type_checker.Substitute(bindings, iface_type));
-    return ResolveInterface(iface_type, impl_type, source_loc, type_checker);
+    return TryResolveInterface(iface_type, impl_type, source_loc, type_checker,
+                               diagnose_missing_impl);
   }
   if (const auto* constraint = dyn_cast<ConstraintType>(constraint_type)) {
     std::vector<Nonnull<const Witness*>> witnesses;
@@ -120,12 +135,16 @@ auto ImplScope::Resolve(Nonnull<const Value*> constraint_type,
       Bindings local_bindings = bindings;
       local_bindings.Add(constraint->self_binding(), impl_type, witness);
       CARBON_ASSIGN_OR_RETURN(
-          Nonnull<const Witness*> result,
-          ResolveInterface(cast<InterfaceType>(type_checker.Substitute(
-                               local_bindings, impl.interface)),
-                           type_checker.Substitute(local_bindings, impl.type),
-                           source_loc, type_checker));
-      witnesses.push_back(result);
+          std::optional<Nonnull<const Witness*>> result,
+          TryResolveInterface(
+              cast<InterfaceType>(
+                  type_checker.Substitute(local_bindings, impl.interface)),
+              type_checker.Substitute(local_bindings, impl.type), source_loc,
+              type_checker, diagnose_missing_impl));
+      if (!result) {
+        return {std::nullopt};
+      }
+      witnesses.push_back(*result);
     }
 
     // Check that all intrinsic, equality, and rewrite constraints
@@ -155,6 +174,9 @@ auto ImplScope::Resolve(Nonnull<const Value*> constraint_type,
               type_checker.Substitute(local_bindings, argument));
         }
         if (!type_checker.IsIntrinsicConstraintSatisfied(converted, *this)) {
+          if (!diagnose_missing_impl) {
+            return {std::nullopt};
+          }
           return ProgramError(source_loc)
                  << "constraint requires that " << converted;
         }
@@ -166,9 +188,13 @@ auto ImplScope::Resolve(Nonnull<const Value*> constraint_type,
         for (; it != equal.values.end(); ++it) {
           Nonnull<const Value*> current =
               type_checker.Substitute(local_bindings, *it);
-          CARBON_RETURN_IF_ERROR(
-              CheckEqualOrDiagnose(source_loc, equal.values.front(), first, *it,
-                                   current, &equality_ctx));
+          if (!ValueEqual(first, current, &equality_ctx)) {
+            if (!diagnose_missing_impl) {
+              return {std::nullopt};
+            }
+            return DiagnoseUnequalValues(source_loc, equal.values.front(),
+                                         first, *it, current, &equality_ctx);
+          }
         }
       }
       for (const auto& rewrite : rewrites) {
@@ -176,12 +202,17 @@ auto ImplScope::Resolve(Nonnull<const Value*> constraint_type,
             type_checker.Substitute(local_bindings, rewrite.constant);
         Nonnull<const Value*> value = type_checker.Substitute(
             local_bindings, rewrite.converted_replacement);
-        CARBON_RETURN_IF_ERROR(CheckEqualOrDiagnose(
-            source_loc, rewrite.constant, constant,
-            rewrite.converted_replacement, value, &equality_ctx));
+        if (!ValueEqual(constant, value, &equality_ctx)) {
+          if (!diagnose_missing_impl) {
+            return {std::nullopt};
+          }
+          return DiagnoseUnequalValues(source_loc, rewrite.constant, constant,
+                                       rewrite.converted_replacement, value,
+                                       &equality_ctx);
+        }
       }
     }
-    return type_checker.MakeConstraintWitness(std::move(witnesses));
+    return {type_checker.MakeConstraintWitness(std::move(witnesses))};
   }
   CARBON_FATAL() << "expected a constraint, not " << *constraint_type;
 }
@@ -202,19 +233,21 @@ auto ImplScope::VisitEqualValues(
   return true;
 }
 
-auto ImplScope::ResolveInterface(Nonnull<const InterfaceType*> iface_type,
-                                 Nonnull<const Value*> type,
-                                 SourceLocation source_loc,
-                                 const TypeChecker& type_checker) const
-    -> ErrorOr<Nonnull<const Witness*>> {
+auto ImplScope::TryResolveInterface(Nonnull<const InterfaceType*> iface_type,
+                                    Nonnull<const Value*> type,
+                                    SourceLocation source_loc,
+                                    const TypeChecker& type_checker,
+                                    bool diagnose_missing_impl) const
+    -> ErrorOr<std::optional<Nonnull<const Witness*>>> {
   CARBON_ASSIGN_OR_RETURN(
       std::optional<Nonnull<const Witness*>> result,
-      TryResolve(iface_type, type, source_loc, *this, type_checker));
-  if (!result.has_value()) {
+      TryResolveInterfaceRecursively(iface_type, type, source_loc, *this,
+                                     type_checker));
+  if (!result.has_value() && diagnose_missing_impl) {
     return ProgramError(source_loc) << "could not find implementation of "
                                     << *iface_type << " for " << *type;
   }
-  return *result;
+  return result;
 }
 
 // Combines the results of two impl lookups. In the event of a tie, arbitrarily
@@ -273,36 +306,36 @@ static auto CombineResults(Nonnull<const InterfaceType*> iface_type,
          << "ambiguous implementations of " << *iface_type << " for " << *type;
 }
 
-auto ImplScope::TryResolve(Nonnull<const InterfaceType*> iface_type,
-                           Nonnull<const Value*> type,
-                           SourceLocation source_loc,
-                           const ImplScope& original_scope,
-                           const TypeChecker& type_checker) const
+auto ImplScope::TryResolveInterfaceRecursively(
+    Nonnull<const InterfaceType*> iface_type, Nonnull<const Value*> type,
+    SourceLocation source_loc, const ImplScope& original_scope,
+    const TypeChecker& type_checker) const
     -> ErrorOr<std::optional<Nonnull<const Witness*>>> {
   CARBON_ASSIGN_OR_RETURN(
       std::optional<Nonnull<const Witness*>> result,
-      ResolveHere(iface_type, type, source_loc, original_scope, type_checker));
+      TryResolveInterfaceHere(iface_type, type, source_loc, original_scope,
+                              type_checker));
   for (Nonnull<const ImplScope*> parent : parent_scopes_) {
     CARBON_ASSIGN_OR_RETURN(
         std::optional<Nonnull<const Witness*>> parent_result,
-        parent->TryResolve(iface_type, type, source_loc, original_scope,
-                           type_checker));
+        parent->TryResolveInterfaceRecursively(iface_type, type, source_loc,
+                                               original_scope, type_checker));
     CARBON_ASSIGN_OR_RETURN(result, CombineResults(iface_type, type, source_loc,
                                                    result, parent_result));
   }
   return result;
 }
 
-auto ImplScope::ResolveHere(Nonnull<const InterfaceType*> iface_type,
-                            Nonnull<const Value*> impl_type,
-                            SourceLocation source_loc,
-                            const ImplScope& original_scope,
-                            const TypeChecker& type_checker) const
+auto ImplScope::TryResolveInterfaceHere(
+    Nonnull<const InterfaceType*> iface_type, Nonnull<const Value*> impl_type,
+    SourceLocation source_loc, const ImplScope& original_scope,
+    const TypeChecker& type_checker) const
     -> ErrorOr<std::optional<Nonnull<const Witness*>>> {
   std::optional<Nonnull<const Witness*>> result = std::nullopt;
   for (const Impl& impl : impls_) {
-    std::optional<Nonnull<const Witness*>> m = type_checker.MatchImpl(
-        *iface_type, impl_type, impl, original_scope, source_loc);
+    CARBON_ASSIGN_OR_RETURN(std::optional<Nonnull<const Witness*>> m,
+                            type_checker.MatchImpl(*iface_type, impl_type, impl,
+                                                   original_scope, source_loc));
     CARBON_ASSIGN_OR_RETURN(
         result, CombineResults(iface_type, impl_type, source_loc, result, m));
   }
diff --git a/explorer/interpreter/impl_scope.h b/explorer/interpreter/impl_scope.h
index 5e1a425df490..f615e53a5c80 100644
--- a/explorer/interpreter/impl_scope.h
+++ b/explorer/interpreter/impl_scope.h
@@ -87,6 +87,16 @@ class ImplScope {
                const Bindings& bindings = {}) const
       -> ErrorOr<Nonnull<const Witness*>>;
 
+  // Same as Resolve, except that failure due to a missing implementation of a
+  // constraint produces `nullopt` instead of an error if
+  // `diagnose_missing_impl` is `false`. This is intended for cases where we're
+  // selecting between options based on whether constraints are satisfied, such
+  // as during `impl` selection.
+  auto TryResolve(Nonnull<const Value*> constraint, Nonnull<const Value*> type,
+                  SourceLocation source_loc, const TypeChecker& type_checker,
+                  const Bindings& bindings, bool diagnose_missing_impl) const
+      -> ErrorOr<std::optional<Nonnull<const Witness*>>>;
+
   // Visits the values that are a single step away from `value` according to an
   // equality constraint that is in scope. That is, the values `v` such that we
   // have a `value == v` equality constraint in scope.
@@ -117,12 +127,15 @@ class ImplScope {
 
  private:
   // Returns the associated impl for the given `iface` and `type` in
-  // the ancestor graph of this scope, or reports a compilation error
-  // at `source_loc` there isn't exactly one matching impl.
-  auto ResolveInterface(Nonnull<const InterfaceType*> iface,
-                        Nonnull<const Value*> type, SourceLocation source_loc,
-                        const TypeChecker& type_checker) const
-      -> ErrorOr<Nonnull<const Witness*>>;
+  // the ancestor graph of this scope. Reports a compilation error
+  // at `source_loc` if there's an ambiguity, or if `diagnose_missing_impl` is
+  // set and there's no matching impl.
+  auto TryResolveInterface(Nonnull<const InterfaceType*> iface,
+                           Nonnull<const Value*> type,
+                           SourceLocation source_loc,
+                           const TypeChecker& type_checker,
+                           bool diagnose_missing_impl) const
+      -> ErrorOr<std::optional<Nonnull<const Witness*>>>;
 
   // Returns the associated impl for the given `iface` and `type` in
   // the ancestor graph of this scope, returns std::nullopt if there
@@ -130,10 +143,11 @@ class ImplScope {
   // specific impl for the given `iface` and `type`.
   // Use `original_scope` to satisfy requirements of any generic impl
   // that matches `iface` and `type`.
-  auto TryResolve(Nonnull<const InterfaceType*> iface_type,
-                  Nonnull<const Value*> type, SourceLocation source_loc,
-                  const ImplScope& original_scope,
-                  const TypeChecker& type_checker) const
+  auto TryResolveInterfaceRecursively(Nonnull<const InterfaceType*> iface_type,
+                                      Nonnull<const Value*> type,
+                                      SourceLocation source_loc,
+                                      const ImplScope& original_scope,
+                                      const TypeChecker& type_checker) const
       -> ErrorOr<std::optional<Nonnull<const Witness*>>>;
 
   // Returns the associated impl for the given `iface` and `type` in
@@ -142,10 +156,11 @@ class ImplScope {
   // given `iface` and `type`.
   // Use `original_scope` to satisfy requirements of any generic impl
   // that matches `iface` and `type`.
-  auto ResolveHere(Nonnull<const InterfaceType*> iface_type,
-                   Nonnull<const Value*> impl_type, SourceLocation source_loc,
-                   const ImplScope& original_scope,
-                   const TypeChecker& type_checker) const
+  auto TryResolveInterfaceHere(Nonnull<const InterfaceType*> iface_type,
+                               Nonnull<const Value*> impl_type,
+                               SourceLocation source_loc,
+                               const ImplScope& original_scope,
+                               const TypeChecker& type_checker) const
       -> ErrorOr<std::optional<Nonnull<const Witness*>>>;
 
   std::vector<Impl> impls_;
diff --git a/explorer/interpreter/matching_impl_set.cpp b/explorer/interpreter/matching_impl_set.cpp
new file mode 100644
index 000000000000..8a92106de356
--- /dev/null
+++ b/explorer/interpreter/matching_impl_set.cpp
@@ -0,0 +1,168 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#include "common/check.h"
+#include "common/error.h"
+#include "explorer/ast/declaration.h"
+#include "explorer/common/error_builders.h"
+#include "explorer/common/nonnull.h"
+#include "explorer/common/source_location.h"
+#include "explorer/interpreter/type_checker.h"
+#include "explorer/interpreter/value.h"
+
+namespace Carbon {
+
+// A visitor for type values that collects leaf 'labels', such as class names,
+// and adds them to the signature of a `Match` object.
+class MatchingImplSet::LeafCollector {
+ public:
+  LeafCollector(Match* match) : match_(match) {}
+
+  void Collect(const Value* value) {
+    value->Visit<void>(
+        [&](const auto* derived_value) { VisitValue(derived_value); });
+  }
+
+  void Collect(Label label) { ++match_->signature_[label]; }
+
+ private:
+  // Most kinds of value don't contribute to the signature.
+  void VisitValue(const Value*) {}
+
+  void VisitValue(const TupleType* tuple) {
+    for (auto* elem : tuple->elements()) {
+      Collect(elem);
+    }
+  }
+
+  void VisitValue(const TypeType*) { Collect(Label::TypeType); }
+
+  void VisitValue(const BoolType*) { Collect(Label::BoolType); }
+
+  void VisitValue(const IntType*) { Collect(Label::IntType); }
+
+  void VisitValue(const StringType*) { Collect(Label::StringType); }
+
+  void VisitValue(const StaticArrayType* array) {
+    Collect(Label::ArrayType);
+    Collect(&array->element_type());
+  }
+
+  void VisitValue(const PointerType* pointer) {
+    Collect(Label::PointerType);
+    Collect(&pointer->pointee_type());
+  }
+
+  void VisitValue(const StructType* struct_type) {
+    for (auto [name, type] : struct_type->fields()) {
+      Collect(type);
+    }
+  }
+
+  void VisitValue(const NominalClassType* class_type) {
+    VisitDeclarationAndArgs(class_type->declaration(), class_type->bindings());
+  }
+
+  void VisitValue(const MixinPseudoType* mixin_type) {
+    VisitDeclarationAndArgs(mixin_type->declaration(), mixin_type->bindings());
+  }
+
+  void VisitValue(const InterfaceType* iface_type) {
+    VisitDeclarationAndArgs(iface_type->declaration(), iface_type->bindings());
+  }
+
+  void VisitValue(const NamedConstraintType* constraint_type) {
+    VisitDeclarationAndArgs(constraint_type->declaration(),
+                            constraint_type->bindings());
+  }
+
+  void VisitValue(const ChoiceType* choice_type) {
+    VisitDeclarationAndArgs(choice_type->declaration(),
+                            choice_type->bindings());
+  }
+
+  void VisitDeclarationAndArgs(const Declaration& declaration,
+                               const Bindings& bindings) {
+    Collect(match_->parent_->GetLabelForDeclaration(declaration));
+    for (auto [key, value] : bindings.args()) {
+      Collect(value);
+    }
+  }
+
+ private:
+  Match* match_;
+};
+
+auto MatchingImplSet::GetLabelForDeclaration(const Declaration& declaration)
+    -> Label {
+  auto [it, added] = declaration_labels_.insert(
+      {&declaration,
+       Label(int(Label::FirstDeclarationLabel) + declaration_labels_.size())});
+  return it->second;
+}
+
+MatchingImplSet::Match::Match(Nonnull<MatchingImplSet*> parent,
+                              Nonnull<const ImplScope::Impl*> impl,
+                              Nonnull<const Value*> type,
+                              Nonnull<const Value*> interface)
+    : parent_(parent), impl_(impl), type_(type), interface_(interface) {
+  // Build our signature.
+  LeafCollector collector(this);
+  collector.Collect(type);
+  collector.Collect(interface);
+
+  parent_->matches_.push_back(this);
+}
+
+MatchingImplSet::Match::~Match() {
+  CARBON_CHECK(parent_->matches_.back() == this) << "match stack broken";
+  parent_->matches_.pop_back();
+}
+
+auto MatchingImplSet::Match::DiagnosePotentialCycle(SourceLocation source_loc)
+    -> ErrorOr<Success> {
+  for (auto* match : parent_->matches_) {
+    if (match != this && match->impl_ == impl_) {
+      // Whether all labels appear a greater or equal number of times in this
+      // match than in `match`.
+      bool all_greater_or_equal = true;
+      // Whether any label appears strictly more times in this match than in
+      // `match`.
+      bool any_greater = false;
+
+      for (auto [key, value] : signature_) {
+        int other_value = match->signature_.lookup(key);
+        if (value < other_value) {
+          all_greater_or_equal = false;
+          break;
+        }
+        if (value > other_value) {
+          any_greater = true;
+        }
+      }
+
+      if (all_greater_or_equal) {
+        if (any_greater) {
+          return ProgramError(source_loc)
+                 << "impl matching recursively performed a more complex match "
+                    "using the same impl\n"
+                 << "  outer match: " << *match->type_ << " as "
+                 << *match->interface_ << "\n"
+                 << "  inner match: " << *type_ << " as " << *interface_;
+        }
+        if (ValueEqual(match->type_, type_, std::nullopt) &&
+            ValueEqual(match->interface_, interface_, std::nullopt)) {
+          return ProgramError(source_loc)
+                 << "impl matching for " << *type_ << " as " << *interface_
+                 << " recursively performed a match for the same type and "
+                    "interface";
+        }
+      }
+    }
+  }
+
+  return Success();
+}
+
+}  // namespace Carbon
diff --git a/explorer/interpreter/matching_impl_set.h b/explorer/interpreter/matching_impl_set.h
new file mode 100644
index 000000000000..b79d2268f059
--- /dev/null
+++ b/explorer/interpreter/matching_impl_set.h
@@ -0,0 +1,129 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#ifndef CARBON_EXPLORER_INTERPRETER_MATCHING_IMPL_SET_H_
+#define CARBON_EXPLORER_INTERPRETER_MATCHING_IMPL_SET_H_
+
+#include <vector>
+
+#include "common/ostream.h"
+#include "explorer/ast/declaration.h"
+#include "explorer/common/nonnull.h"
+#include "explorer/interpreter/impl_scope.h"
+#include "explorer/interpreter/value.h"
+#include "llvm/ADT/DenseMap.h"
+
+namespace Carbon {
+
+// A set of impl matches that we're currently performing. Each `Match`
+// represents an attempt to match a `type as interface` query against an `impl`
+// declaration. This is used to detect and reject non-termination when impl
+// matching recursively triggers further impl matching.
+//
+// The language rule we use to detect potential non-termination is to count the
+// number of times each "label" appears within the type and interface, where a
+// label is the name of a declared entity such as a class or interface, or a
+// primitive like `type` or `bool`. For example, `Optional(i32*)` contains the
+// labels for `Optional`, `i32`, and `*` (built-in pointer type) once each. If
+// we ever try matching the same `impl` twice, where the inner match contains
+// at least as many appearances of each label as the outer match, we reject the
+// program as invalid. We also reject if a query results in the exact same
+// query being performed again.
+//
+// This class is an implementation detail of `TypeChecker::MatchImpl`.
+class MatchingImplSet {
+ private:
+  class LeafCollector;
+  enum class Label : int;
+
+ public:
+  // An RAII type that tracks an impl match that we're currently performing.
+  // One instance of this class will exist for each in-progress call to
+  // `MatchImpl`.
+  class Match {
+   public:
+    explicit Match(Nonnull<MatchingImplSet*> parent,
+                   Nonnull<const ImplScope::Impl*> impl,
+                   Nonnull<const Value*> type, Nonnull<const Value*> interface);
+    ~Match();
+
+    Match(const Match&) = delete;
+    Match& operator=(const Match&) = delete;
+
+    // Check to see if this match duplicates any prior one within the same set,
+    // or if there's a simpler form of this match in the set. If so, returns a
+    // suitable error. This should be delayed until we know that the impl
+    // structurally matches the type and interface.
+    auto DiagnosePotentialCycle(SourceLocation source_loc) -> ErrorOr<Success>;
+
+   private:
+    friend class LeafCollector;
+
+    // The set that this match is part of.
+    Nonnull<MatchingImplSet*> parent_;
+    // The `impl` that is being matched against.
+    Nonnull<const ImplScope::Impl*> impl_;
+    // The type that is being matched against the impl.
+    Nonnull<const Value*> type_;
+    // The interface that is being matched against the impl.
+    Nonnull<const Value*> interface_;
+    // The number of times each label appears in the type or interface.
+    llvm::DenseMap<Label, int> signature_;
+  };
+
+ private:
+  friend class llvm::DenseMapInfo<Label>;
+
+  // An opaque integer used to identify a particular label appearing in a type,
+  // such as a class name. The named enumerators represent builtins, and values
+  // >= `FirstDeclarationLabel` represent declarations from the program.
+  enum class Label : int {
+    // Label for `type` type constant.
+    TypeType,
+    // Label for `bool` type constant.
+    BoolType,
+    // Label for `i32` type constant.
+    IntType,
+    // Label for `String` type constant.
+    StringType,
+    // Label for `[_;_]` type constructor.
+    ArrayType,
+    // Label for `_*` type constructor.
+    PointerType,
+    // First Label value corresponding to a Declaration. Must be kept at the
+    // end of the enum.
+    FirstDeclarationLabel
+  };
+
+  // Get the Label that represents a given declaration.
+  auto GetLabelForDeclaration(const Declaration& declaration) -> Label;
+
+  // The known declarations and their labels.
+  llvm::DenseMap<const Declaration*, Label> declaration_labels_;
+
+  // The matches that are currently being performed, in order from outermost to
+  // innermost.
+  std::vector<Match*> matches_;
+};
+
+}  // namespace Carbon
+
+// Support use of Label as a DenseMap key.
+template <>
+struct llvm::DenseMapInfo<Carbon::MatchingImplSet::Label> {
+  using Base = llvm::DenseMapInfo<int>;
+  using Label = Carbon::MatchingImplSet::Label;
+  static inline auto getEmptyKey() -> Label {
+    return Label(Base::getEmptyKey());
+  }
+  static inline auto getTombstoneKey() -> Label {
+    return Label(Base::getTombstoneKey());
+  }
+  static inline auto getHashValue(Label label) -> unsigned {
+    return Base::getHashValue(int(label));
+  }
+  static auto isEqual(Label a, Label b) -> bool { return a == b; }
+};
+
+#endif  // CARBON_EXPLORER_INTERPRETER_MATCHING_IMPL_SET_H_
diff --git a/explorer/interpreter/type_checker.cpp b/explorer/interpreter/type_checker.cpp
index bc4cfcc4fb1d..1a1347bdb0e2 100644
--- a/explorer/interpreter/type_checker.cpp
+++ b/explorer/interpreter/type_checker.cpp
@@ -611,6 +611,7 @@ auto TypeChecker::IsImplicitlyConvertible(
   SourceLocation source_loc = SourceLocation::DiagnosticsIgnored();
   ErrorOr<Nonnull<const InterfaceType*>> iface_type = GetBuiltinInterfaceType(
       source_loc, BuiltinInterfaceName{Builtins::ImplicitAs, destination});
+  // TODO: If the Resolve call fails with a hard error, don't swallow it.
   return iface_type.ok() &&
          impl_scope.Resolve(*iface_type, source, source_loc, *this).ok();
 }
@@ -909,8 +910,9 @@ class TypeChecker::ArgumentDeduction {
 
   // Finishes deduction and forms a set of substitutions that transform `param`
   // into `arg`.
-  auto Finish(TypeChecker& type_checker, const ImplScope& impl_scope) const
-      -> ErrorOr<Bindings>;
+  auto Finish(TypeChecker& type_checker, const ImplScope& impl_scope,
+              bool diagnose_deduction_failure) const
+      -> ErrorOr<std::optional<Bindings>>;
 
  private:
   SourceLocation source_loc_;
@@ -945,11 +947,20 @@ auto TypeChecker::ArgumentDeduction::Deduce(Nonnull<const Value*> param,
     **trace_stream_ << "deducing " << *param << " from " << *arg << "\n";
   }
 
+  // If param is the name of a variable we're deducing, then deduce it.
+  if (auto* var_type = dyn_cast<VariableType>(param)) {
+    const auto& binding = var_type->binding();
+    if (auto it = deduced_values_.find(&binding); it != deduced_values_.end()) {
+      it->second.push_back(arg);
+      return Success();
+    }
+  }
+
   // Handle the case where we can't perform deduction, either because the
   // parameter is a primitive type or because the parameter and argument have
   // different forms. In this case, we require an implicit conversion to exist,
   // or for an exact type match if implicit conversions are not permitted.
-  auto handle_non_deduced_type = [&]() -> ErrorOr<Success> {
+  auto handle_non_deduced_value = [&]() -> ErrorOr<Success> {
     if (ValueEqual(param, arg, std::nullopt)) {
       return Success();
     }
@@ -963,21 +974,33 @@ auto TypeChecker::ArgumentDeduction::Deduce(Nonnull<const Value*> param,
     return Success();
   };
 
-  switch (param->kind()) {
-    case Value::Kind::VariableType: {
-      const auto& binding = cast<VariableType>(*param).binding();
-      if (auto it = deduced_values_.find(&binding);
-          it != deduced_values_.end()) {
-        it->second.push_back(arg);
-      } else {
-        return handle_non_deduced_type();
-      }
-      return Success();
+  // Handle the case where we know we can't have an exact match, but there
+  // might still be an implicit conversion.
+  auto handle_non_matching_value = [&]() -> ErrorOr<Success> {
+    if (!allow_implicit_conversion) {
+      return ProgramError(source_loc_)
+             << "type mismatch in argument deduction\n"
+             << "expected: " << *param << "\n"
+             << "actual: " << *arg;
     }
+    return handle_non_deduced_value();
+  };
+
+  // If either parameter or argument is an unknown kind of value, we can't
+  // perform any deduction. Keep track of them so we can check they're the same
+  // later.
+  if (IsValueKindDependent(param) || IsValueKindDependent(arg)) {
+    return handle_non_deduced_value();
+  }
+
+  // If the values have different non-dependent kinds, they can't possibly
+  // match after substitution.
+  if (param->kind() != arg->kind()) {
+    return handle_non_matching_value();
+  }
+
+  switch (param->kind()) {
     case Value::Kind::TupleType: {
-      if (arg->kind() != Value::Kind::TupleType) {
-        return handle_non_deduced_type();
-      }
       const auto& param_tup = cast<TupleType>(*param);
       const auto& arg_tup = cast<TupleType>(*arg);
       if (param_tup.elements().size() != arg_tup.elements().size()) {
@@ -994,9 +1017,6 @@ auto TypeChecker::ArgumentDeduction::Deduce(Nonnull<const Value*> param,
       return Success();
     }
     case Value::Kind::StructType: {
-      if (arg->kind() != Value::Kind::StructType) {
-        return handle_non_deduced_type();
-      }
       const auto& param_struct = cast<StructType>(*param);
       const auto& arg_struct = cast<StructType>(*arg);
       auto diagnose_missing_field = [&](const StructType& struct_type,
@@ -1049,9 +1069,6 @@ auto TypeChecker::ArgumentDeduction::Deduce(Nonnull<const Value*> param,
       return Success();
     }
     case Value::Kind::FunctionType: {
-      if (arg->kind() != Value::Kind::FunctionType) {
-        return handle_non_deduced_type();
-      }
       const auto& param_fn = cast<FunctionType>(*param);
       const auto& arg_fn = cast<FunctionType>(*arg);
       // TODO: handle situation when arg has deduced parameters.
@@ -1064,9 +1081,6 @@ auto TypeChecker::ArgumentDeduction::Deduce(Nonnull<const Value*> param,
       return Success();
     }
     case Value::Kind::PointerType: {
-      if (arg->kind() != Value::Kind::PointerType) {
-        return handle_non_deduced_type();
-      }
       const auto& param_pointee = cast<PointerType>(param)->pointee_type();
       const auto& arg_pointee = cast<PointerType>(arg)->pointee_type();
       if (allow_implicit_conversion) {
@@ -1087,15 +1101,10 @@ auto TypeChecker::ArgumentDeduction::Deduce(Nonnull<const Value*> param,
     }
     case Value::Kind::NominalClassType: {
       const auto& param_class_type = cast<NominalClassType>(*param);
-      if (arg->kind() != Value::Kind::NominalClassType) {
-        // TODO: We could determine the parameters of the class from field
-        // types in a struct argument.
-        return handle_non_deduced_type();
-      }
       const auto& arg_class_type = cast<NominalClassType>(*arg);
       if (!DeclaresSameEntity(param_class_type.declaration(),
                               arg_class_type.declaration())) {
-        return handle_non_deduced_type();
+        return handle_non_matching_value();
       }
       for (const auto& [ty, param_ty] : param_class_type.type_args()) {
         CARBON_RETURN_IF_ERROR(Deduce(param_ty,
@@ -1106,13 +1115,10 @@ auto TypeChecker::ArgumentDeduction::Deduce(Nonnull<const Value*> param,
     }
     case Value::Kind::InterfaceType: {
       const auto& param_iface_type = cast<InterfaceType>(*param);
-      if (arg->kind() != Value::Kind::InterfaceType) {
-        return handle_non_deduced_type();
-      }
       const auto& arg_iface_type = cast<InterfaceType>(*arg);
       if (!DeclaresSameEntity(param_iface_type.declaration(),
                               arg_iface_type.declaration())) {
-        return handle_non_deduced_type();
+        return handle_non_matching_value();
       }
       for (const auto& [ty, param_ty] : param_iface_type.args()) {
         CARBON_RETURN_IF_ERROR(Deduce(param_ty, arg_iface_type.args().at(ty),
@@ -1122,13 +1128,10 @@ auto TypeChecker::ArgumentDeduction::Deduce(Nonnull<const Value*> param,
     }
     case Value::Kind::NamedConstraintType: {
       const auto& param_constraint_type = cast<NamedConstraintType>(*param);
-      if (arg->kind() != Value::Kind::NamedConstraintType) {
-        return handle_non_deduced_type();
-      }
       const auto& arg_constraint_type = cast<NamedConstraintType>(*arg);
       if (!DeclaresSameEntity(param_constraint_type.declaration(),
                               arg_constraint_type.declaration())) {
-        return handle_non_deduced_type();
+        return handle_non_matching_value();
       }
       for (const auto& [ty, param_ty] :
            param_constraint_type.bindings().args()) {
@@ -1139,10 +1142,14 @@ auto TypeChecker::ArgumentDeduction::Deduce(Nonnull<const Value*> param,
       return Success();
     }
     // For the following cases, we check the type matches.
+    case Value::Kind::VariableType:
+      // We handled deduced variables above; this case covers variables that
+      // are not deduced as part of this deduction step.
     case Value::Kind::StaticArrayType:
       // TODO: We could deduce the array type from an array or tuple argument.
     case Value::Kind::ContinuationType:
     case Value::Kind::ChoiceType:
+      // TODO: Choice types should be handled like other named declarations.
     case Value::Kind::ConstraintType:
     case Value::Kind::AssociatedConstant:
     case Value::Kind::IntType:
@@ -1152,7 +1159,7 @@ auto TypeChecker::ArgumentDeduction::Deduce(Nonnull<const Value*> param,
     case Value::Kind::TypeOfParameterizedEntityName:
     case Value::Kind::TypeOfMemberName:
     case Value::Kind::TypeOfNamespaceName: {
-      return handle_non_deduced_type();
+      return handle_non_deduced_value();
     }
     case Value::Kind::ImplWitness:
     case Value::Kind::BindingWitness:
@@ -1180,12 +1187,7 @@ auto TypeChecker::ArgumentDeduction::Deduce(Nonnull<const Value*> param,
       // Argument deduction within the parameters of a parameterized class type
       // or interface type can compare values, rather than types.
       // TODO: Deduce within the values where possible.
-      // TODO: Consider in-scope value equalities here.
-      if (!ValueEqual(param, arg, std::nullopt)) {
-        return ProgramError(source_loc_) << "mismatch in non-type values, `"
-                                         << *arg << "` != `" << *param << "`";
-      }
-      return Success();
+      return handle_non_deduced_value();
     }
     case Value::Kind::MixinPseudoType:
     case Value::Kind::TypeOfMixinPseudoType:
@@ -1193,9 +1195,9 @@ auto TypeChecker::ArgumentDeduction::Deduce(Nonnull<const Value*> param,
   }
 }
 
-auto TypeChecker::ArgumentDeduction::Finish(TypeChecker& type_checker,
-                                            const ImplScope& impl_scope) const
-    -> ErrorOr<Bindings> {
+auto TypeChecker::ArgumentDeduction::Finish(
+    TypeChecker& type_checker, const ImplScope& impl_scope,
+    bool diagnose_deduction_failure) const -> ErrorOr<std::optional<Bindings>> {
   // Check deduced values and build our resulting `Bindings` set. We do this in
   // declaration order so that any bindings used in the type of a later binding
   // have known values before we check that binding.
@@ -1204,6 +1206,9 @@ auto TypeChecker::ArgumentDeduction::Finish(TypeChecker& type_checker,
     llvm::ArrayRef<Nonnull<const Value*>> values =
         deduced_values_.find(binding)->second;
     if (values.empty()) {
+      if (!diagnose_deduction_failure) {
+        return {std::nullopt};
+      }
       return ProgramError(source_loc_)
              << "could not deduce type argument for type parameter "
              << binding->name() << " in " << context_;
@@ -1232,6 +1237,9 @@ auto TypeChecker::ArgumentDeduction::Finish(TypeChecker& type_checker,
       // should be used, and we'd need to check all pairs of types for equality
       // because our notion of equality is non-transitive.
       if (!ValueEqual(first_value, value, std::nullopt)) {
+        if (!diagnose_deduction_failure) {
+          return {std::nullopt};
+        }
         return ProgramError(source_loc_)
                << "deduced multiple different values for " << *binding
                << ":\n  " << *first_value << "\n  " << *value;
@@ -1242,8 +1250,12 @@ auto TypeChecker::ArgumentDeduction::Finish(TypeChecker& type_checker,
     std::optional<Nonnull<const Witness*>> witness;
     if (binding->impl_binding()) {
       CARBON_ASSIGN_OR_RETURN(
-          witness, impl_scope.Resolve(binding_type, first_value, source_loc_,
-                                      type_checker, bindings));
+          witness, impl_scope.TryResolve(binding_type, first_value, source_loc_,
+                                         type_checker, bindings,
+                                         diagnose_deduction_failure));
+      if (!witness) {
+        return {std::nullopt};
+      }
     }
 
     bindings.Add(binding, first_value, witness);
@@ -1276,8 +1288,12 @@ auto TypeChecker::ArgumentDeduction::Finish(TypeChecker& type_checker,
     std::optional<Nonnull<const Witness*>> witness;
     if (binding->impl_binding()) {
       CARBON_ASSIGN_OR_RETURN(
-          witness, impl_scope.Resolve(binding_type, value, source_loc_,
-                                      type_checker, bindings));
+          witness,
+          impl_scope.TryResolve(binding_type, value, source_loc_, type_checker,
+                                bindings, diagnose_deduction_failure));
+      if (!witness) {
+        return {std::nullopt};
+      }
     }
 
     bindings.Add(binding, value, witness);
@@ -1285,15 +1301,30 @@ auto TypeChecker::ArgumentDeduction::Finish(TypeChecker& type_checker,
 
   // Check non-deduced potential mismatches now we can substitute into them.
   for (const auto& mismatch : non_deduced_mismatches_) {
-    const Value* subst_param_type =
+    const Value* subst_param =
         type_checker.Substitute(bindings, mismatch.param);
-    CARBON_RETURN_IF_ERROR(
-        mismatch.allow_implicit_conversion
-            ? type_checker.ExpectType(source_loc_, context_, subst_param_type,
-                                      mismatch.arg, impl_scope)
-            : type_checker.ExpectExactType(source_loc_, context_,
-                                           subst_param_type, mismatch.arg,
-                                           impl_scope));
+
+    bool type = IsType(subst_param) && IsType(mismatch.arg);
+    if (type && mismatch.allow_implicit_conversion) {
+      if (!type_checker.IsImplicitlyConvertible(mismatch.arg, subst_param,
+                                                impl_scope, true)) {
+        if (!diagnose_deduction_failure) {
+          return {std::nullopt};
+        }
+        return ProgramError(source_loc_)
+               << "mismatch in non-deduced types, `" << *mismatch.arg
+               << "` is not implicitly convertible to `" << *subst_param << "`";
+      }
+    } else {
+      if (!ValueEqual(subst_param, mismatch.arg, std::nullopt)) {
+        if (!diagnose_deduction_failure) {
+          return {std::nullopt};
+        }
+        return ProgramError(source_loc_)
+               << "mismatch in non-deduced " << (type ? "types" : "values")
+               << ", `" << *mismatch.arg << "` != `" << *subst_param << "`";
+      }
+    }
   }
 
   if (trace_stream_) {
@@ -1308,7 +1339,7 @@ auto TypeChecker::ArgumentDeduction::Finish(TypeChecker& type_checker,
     **trace_stream_ << "}\n";
   }
 
-  return std::move(bindings);
+  return {std::move(bindings)};
 }
 
 // Look for a rewrite to use when naming the given interface member in a type
@@ -2073,6 +2104,8 @@ auto TypeChecker::RefineWitness(Nonnull<const Witness*> witness,
   }
 
   // Attempt to look for an impl witness in the top-level impl scope.
+  // TODO: This can fail due to non-terminating impl matching. That should
+  // result in a hard error.
   if (auto refined_witness =
           (*top_level_impl_scope_)
               ->Resolve(constraint, type, SourceLocation::DiagnosticsIgnored(),
@@ -2093,15 +2126,18 @@ auto TypeChecker::MatchImpl(const InterfaceType& iface,
                             const ImplScope::Impl& impl,
                             const ImplScope& impl_scope,
                             SourceLocation source_loc) const
-    -> std::optional<Nonnull<const Witness*>> {
+    -> ErrorOr<std::optional<Nonnull<const Witness*>>> {
   // Avoid cluttering the trace output with matches that could obviously never
   // have worked.
   // TODO: Eventually, ImplScope should filter by type structure before calling
   // into here.
   if (!DeclaresSameEntity(impl.interface->declaration(), iface.declaration())) {
-    return std::nullopt;
+    return {std::nullopt};
   }
 
+  // Track that we're matching this impl.
+  MatchingImplSet::Match match(&matching_impl_set_, &impl, impl_type, &iface);
+
   if (trace_stream_) {
     **trace_stream_ << "MatchImpl: looking for " << *impl_type << " as "
                     << iface << "\n";
@@ -2117,7 +2153,7 @@ auto TypeChecker::MatchImpl(const InterfaceType& iface,
     if (trace_stream_) {
       **trace_stream_ << "type does not match: " << e.error() << "\n";
     }
-    return std::nullopt;
+    return {std::nullopt};
   }
 
   if (ErrorOr<Success> e = deduction.Deduce(
@@ -2126,23 +2162,29 @@ auto TypeChecker::MatchImpl(const InterfaceType& iface,
     if (trace_stream_) {
       **trace_stream_ << "interface does not match: " << e.error() << "\n";
     }
-    return std::nullopt;
+    return {std::nullopt};
   }
 
-  if (ErrorOr<Bindings> bindings_or_error =
-          deduction.Finish(const_cast<TypeChecker&>(*this), impl_scope);
-      !bindings_or_error.ok()) {
+  // This impl seems to match. Reject if we're already matching this or a
+  // simpler version of it, before we recursively try to satisfy its
+  // constraints.
+  CARBON_RETURN_IF_ERROR(match.DiagnosePotentialCycle(source_loc));
+
+  CARBON_ASSIGN_OR_RETURN(
+      std::optional<Bindings> bindings_or_error,
+      deduction.Finish(const_cast<TypeChecker&>(*this), impl_scope,
+                       /*diagnose_deduction_failure=*/false));
+  if (!bindings_or_error) {
     if (trace_stream_) {
-      **trace_stream_ << "impl does not match: " << bindings_or_error.error()
-                      << "\n";
+      **trace_stream_ << "impl does not match\n";
     }
-    return std::nullopt;
+    return {std::nullopt};
   } else {
     if (trace_stream_) {
       **trace_stream_ << "matched with " << *impl.type << " as "
                       << *impl.interface << "\n\n";
     }
-    return cast<Witness>(Substitute(*bindings_or_error, impl.witness));
+    return {cast<Witness>(Substitute(*bindings_or_error, impl.witness))};
   }
 }
 
@@ -2240,9 +2282,11 @@ auto TypeChecker::DeduceCallBindings(
   CARBON_CHECK(generic_params.empty())
       << "did not find all generic parameters in parameter list";
 
-  CARBON_ASSIGN_OR_RETURN(Bindings bindings,
-                          deduction.Finish(*this, impl_scope));
-  call.set_bindings(std::move(bindings));
+  CARBON_ASSIGN_OR_RETURN(
+      std::optional<Bindings> bindings,
+      deduction.Finish(*this, impl_scope, /*diagnose_deduction_failure=*/true));
+  CARBON_CHECK(bindings) << "should have diagnosed deduction failure";
+  call.set_bindings(std::move(*bindings));
 
   // Convert the arguments to the deduced and substituted parameter type.
   Nonnull<const Value*> param_type = Substitute(call.bindings(), params_type);
diff --git a/explorer/interpreter/type_checker.h b/explorer/interpreter/type_checker.h
index 7cbcac9d4b96..99a9a6487c6a 100644
--- a/explorer/interpreter/type_checker.h
+++ b/explorer/interpreter/type_checker.h
@@ -21,6 +21,7 @@
 #include "explorer/interpreter/dictionary.h"
 #include "explorer/interpreter/impl_scope.h"
 #include "explorer/interpreter/interpreter.h"
+#include "explorer/interpreter/matching_impl_set.h"
 #include "explorer/interpreter/value.h"
 
 namespace Carbon {
@@ -63,7 +64,7 @@ class TypeChecker {
   auto MatchImpl(const InterfaceType& iface, Nonnull<const Value*> type,
                  const ImplScope::Impl& impl, const ImplScope& impl_scope,
                  SourceLocation source_loc) const
-      -> std::optional<Nonnull<const Witness*>>;
+      -> ErrorOr<std::optional<Nonnull<const Witness*>>>;
 
   // Return the declaration of the member with the given name and the class type
   // that owns it, from the class and its parents
@@ -525,6 +526,12 @@ class TypeChecker {
   // Constraint types that are currently being resolved. These may have
   // rewrites that are not yet visible in any type.
   std::vector<ConstraintTypeBuilder*> partial_constraint_types_;
+
+  // A set of impls we're currently matching.
+  // TODO: This is `mutable` because `MatchImpl` is `const`. We need to remove
+  // the `const`s from everywhere that transitively does `impl` matching to get
+  // rid of this `mutable`.
+  mutable MatchingImplSet matching_impl_set_;
 };
 
 }  // namespace Carbon
diff --git a/explorer/testdata/assoc_const/fail_match_in_deduction.carbon b/explorer/testdata/assoc_const/fail_match_in_deduction.carbon
index 27c056dfbceb..eb89db97b09d 100644
--- a/explorer/testdata/assoc_const/fail_match_in_deduction.carbon
+++ b/explorer/testdata/assoc_const/fail_match_in_deduction.carbon
@@ -22,7 +22,7 @@ fn F[Scalar:! type, V:! Vector where .Dim == 3](p: Point(Scalar, V.Dim), v: V) {
 fn G[Scalar:! type](p: Point(Scalar, 3)) {}
 fn H[V:! Vector where .Dim == 3](v: V) {
   var p: Point(i32, V.Dim) = {};
-  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_match_in_deduction.carbon:[[@LINE+1]]: mismatch in non-type values, `(V).(Vector.Dim)` != `3`
+  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_match_in_deduction.carbon:[[@LINE+1]]: mismatch in non-deduced values, `(V).(Vector.Dim)` != `3`
   G(p);
 }
 
diff --git a/explorer/testdata/generic_class/fail_value_param_mismatch.carbon b/explorer/testdata/generic_class/fail_value_param_mismatch.carbon
index 202521da6cd9..d081782c6846 100644
--- a/explorer/testdata/generic_class/fail_value_param_mismatch.carbon
+++ b/explorer/testdata/generic_class/fail_value_param_mismatch.carbon
@@ -14,7 +14,7 @@ fn F(x: HasI32Param(1)) {}
 
 fn Main() -> i32 {
   var n: HasI32Param(0) = {};
-  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/generic_class/fail_value_param_mismatch.carbon:[[@LINE+1]]: mismatch in non-type values, `0` != `1`
+  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/generic_class/fail_value_param_mismatch.carbon:[[@LINE+1]]: mismatch in non-deduced values, `0` != `1`
   F(n);
   return 0;
 }
diff --git a/explorer/testdata/impl_match/build_tree.carbon b/explorer/testdata/impl_match/build_tree.carbon
new file mode 100644
index 000000000000..93c30c3b297a
--- /dev/null
+++ b/explorer/testdata/impl_match/build_tree.carbon
@@ -0,0 +1,35 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// AUTOUPDATE
+// RUN: %{explorer-run}
+// RUN: %{explorer-run-trace}
+// CHECK:STDOUT: result: 0
+
+package ExplorerTest api;
+
+class S(T:! type) {}
+class Z {}
+
+class Tree(L:! type, R:! type) {}
+class Leaf {}
+
+interface Foo(T:! type) {}
+
+impl forall [U:! type, T:! Foo(Tree(U, U))] S(T) as Foo(U) {}
+
+alias Level1 = Tree(Leaf, Leaf);
+alias Level2 = Tree(Level1, Level1);
+alias Level3 = Tree(Level2, Level2);
+alias Level4 = Tree(Level3, Level3);
+alias Level5 = Tree(Level4, Level4);
+
+impl Z as Foo(Level5) {}
+
+fn F[T:! Foo(Leaf)](x: T) {}
+fn Main() -> i32 {
+  var n: S(S(S(S(S(Z))))) = {};
+  F(n);
+  return 0;
+}
diff --git a/explorer/testdata/impl_match/fail_self_recurse.carbon b/explorer/testdata/impl_match/fail_self_recurse.carbon
new file mode 100644
index 000000000000..2360f73bdf99
--- /dev/null
+++ b/explorer/testdata/impl_match/fail_self_recurse.carbon
@@ -0,0 +1,23 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// AUTOUPDATE
+// RUN: %{not} %{explorer-run}
+// RUN: %{not} %{explorer-run-trace}
+
+package ExplorerTest api;
+
+interface Foo {}
+
+impl forall [T:! type where .Self* is Foo] T as Foo {}
+
+fn F[T:! Foo](x: T) {}
+
+fn Main() -> i32 {
+  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/impl_match/fail_self_recurse.carbon:[[@LINE+3]]: impl matching recursively performed a more complex match using the same impl
+  // CHECK:STDERR:   outer match: i32 as interface Foo
+  // CHECK:STDERR:   inner match: i32* as interface Foo
+  F(0);
+  return 0;
+}
diff --git a/explorer/testdata/impl_match/fail_self_recurse_with_match.carbon b/explorer/testdata/impl_match/fail_self_recurse_with_match.carbon
new file mode 100644
index 000000000000..d5f96801e45d
--- /dev/null
+++ b/explorer/testdata/impl_match/fail_self_recurse_with_match.carbon
@@ -0,0 +1,24 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// AUTOUPDATE
+// RUN: %{not} %{explorer-run}
+// RUN: %{not} %{explorer-run-trace}
+
+package ExplorerTest api;
+
+interface Foo {}
+
+impl i32* as Foo {}
+impl forall [T:! type where .Self* is Foo] T as Foo {}
+
+fn F[T:! Foo](x: T) {}
+
+fn Main() -> i32 {
+  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/impl_match/fail_self_recurse_with_match.carbon:[[@LINE+3]]: impl matching recursively performed a more complex match using the same impl
+  // CHECK:STDERR:   outer match: i32 as interface Foo
+  // CHECK:STDERR:   inner match: i32* as interface Foo
+  F(0);
+  return 0;
+}
diff --git a/explorer/testdata/impl_match/fail_self_recurse_with_match_first.carbon b/explorer/testdata/impl_match/fail_self_recurse_with_match_first.carbon
new file mode 100644
index 000000000000..c96c96efebef
--- /dev/null
+++ b/explorer/testdata/impl_match/fail_self_recurse_with_match_first.carbon
@@ -0,0 +1,27 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// AUTOUPDATE
+// RUN: %{not} %{explorer-run}
+// RUN: %{not} %{explorer-run-trace}
+
+package ExplorerTest api;
+
+interface Foo {}
+
+__match_first {
+  impl i32* as Foo {}
+  impl forall [T:! type where .Self* is Foo] T as Foo {}
+}
+
+fn F[T:! Foo](x: T) {}
+
+fn Main() -> i32 {
+  // TODO: We should decide whether we want to accept this.
+  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/impl_match/fail_self_recurse_with_match_first.carbon:[[@LINE+3]]: impl matching recursively performed a more complex match using the same impl
+  // CHECK:STDERR:   outer match: i32 as interface Foo
+  // CHECK:STDERR:   inner match: i32* as interface Foo
+  F(0);
+  return 0;
+}
diff --git a/explorer/testdata/impl_match/fail_simple_self_recurse.carbon b/explorer/testdata/impl_match/fail_simple_self_recurse.carbon
new file mode 100644
index 000000000000..4775e8facbae
--- /dev/null
+++ b/explorer/testdata/impl_match/fail_simple_self_recurse.carbon
@@ -0,0 +1,21 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// AUTOUPDATE
+// RUN: %{not} %{explorer-run}
+// RUN: %{not} %{explorer-run-trace}
+
+package ExplorerTest api;
+
+interface Foo {}
+
+impl forall [T:! Foo] T as Foo {}
+
+fn F[T:! Foo](x: T) {}
+
+fn Main() -> i32 {
+  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/impl_match/fail_simple_self_recurse.carbon:[[@LINE+1]]: impl matching for i32 as interface Foo recursively performed a match for the same type and interface
+  F(0);
+  return 0;
+}
diff --git a/explorer/testdata/impl_match/fail_three_step_recurse.carbon b/explorer/testdata/impl_match/fail_three_step_recurse.carbon
new file mode 100644
index 000000000000..3b1e587110d7
--- /dev/null
+++ b/explorer/testdata/impl_match/fail_three_step_recurse.carbon
@@ -0,0 +1,27 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// AUTOUPDATE
+// RUN: %{not} %{explorer-run}
+// RUN: %{not} %{explorer-run-trace}
+
+package ExplorerTest api;
+
+interface A {}
+interface B {}
+interface C {}
+
+impl forall [T:! type where .Self* is A] T as B {}
+impl forall [T:! type where .Self* is B] T as C {}
+impl forall [T:! type where .Self* is C] T as A {}
+
+fn F[T:! A](x: T) {}
+
+fn Main() -> i32 {
+  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/impl_match/fail_three_step_recurse.carbon:[[@LINE+3]]: impl matching recursively performed a more complex match using the same impl
+  // CHECK:STDERR:   outer match: i32 as interface A
+  // CHECK:STDERR:   inner match: i32*** as interface A
+  F(0);
+  return 0;
+}
diff --git a/explorer/testdata/mixin/fail_self_substitution.carbon b/explorer/testdata/mixin/fail_self_substitution.carbon
index 27af0f21e7bc..3782a00531f2 100644
--- a/explorer/testdata/mixin/fail_self_substitution.carbon
+++ b/explorer/testdata/mixin/fail_self_substitution.carbon
@@ -36,7 +36,7 @@ class Complex {
 fn Main() -> i32 {
   var p: Point = Point.Origin();
   var c: Complex = {.r = 42, .i = 1};
-  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/mixin/fail_self_substitution.carbon:[[@LINE+1]]: type error in call: 'class Complex' is not implicitly convertible to 'class Point'
+  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/mixin/fail_self_substitution.carbon:[[@LINE+1]]: mismatch in non-deduced types, `class Complex` is not implicitly convertible to `class Point`
   var p1: Point = p.F(c);
 
   return p1.x - 42;