diff --git a/common/check.h b/common/check.h
index 3441d1182a169..f8ff708b381d7 100644
--- a/common/check.h
+++ b/common/check.h
@@ -21,18 +21,18 @@ namespace Carbon {
 //
 // For example:
 //   CARBON_CHECK(is_valid) << "Data is not valid!";
-#define CARBON_CHECK(condition)                                           \
-  (condition) ? (void)0                                                   \
-              : CARBON_RAW_EXITING_STREAM()                               \
-                    << "CHECK failure at " << __FILE__ << ":" << __LINE__ \
-                    << ": " #condition                                    \
-                    << Carbon::Internal::ExitingStream::AddSeparator()
+#define CARBON_CHECK(...)                                                   \
+  (__VA_ARGS__) ? (void)0                                                   \
+                : CARBON_RAW_EXITING_STREAM()                               \
+                      << "CHECK failure at " << __FILE__ << ":" << __LINE__ \
+                      << ": " #__VA_ARGS__                                  \
+                      << Carbon::Internal::ExitingStream::AddSeparator()
 
 // DCHECK calls CHECK in debug mode, and does nothing otherwise.
 #ifndef NDEBUG
-#define CARBON_DCHECK(condition) CARBON_CHECK(condition)
+#define CARBON_DCHECK(...) CARBON_CHECK(__VA_ARGS__)
 #else
-#define CARBON_DCHECK(condition) CARBON_CHECK(true || (condition))
+#define CARBON_DCHECK(...) CARBON_CHECK(true || (__VA_ARGS__))
 #endif
 
 // This is similar to CHECK, but is unconditional. Writing CARBON_FATAL() is
diff --git a/explorer/data/prelude.carbon b/explorer/data/prelude.carbon
index a8b3be95deab0..492fd22e2924f 100644
--- a/explorer/data/prelude.carbon
+++ b/explorer/data/prelude.carbon
@@ -18,9 +18,21 @@ interface ImplicitAs(T:! Type) {
   extends As(T);
 }
 
-// Every type implicitly converts to itself.
-impl forall [T:! Type] T as ImplicitAs(T) {
-  fn Convert[me: Self]() -> T { return me; }
+// TODO: Should we just use an intrinsic for this?
+interface __EqualConverter {
+  let T:! Type;
+  fn Convert(t: T) -> Self;
+}
+fn __EqualConvert[T:! Type](t: T, U:! __EqualConverter where .T = T) -> U {
+  return U.Convert(t);
+}
+impl forall [U:! Type] U as __EqualConverter where .T = U {
+  fn Convert(u: U) -> U { return u; }
+}
+
+// Every type implicitly converts to single-step-equal types.
+impl forall [T:! Type, U:! Type where .Self == T] T as ImplicitAs(U) {
+  fn Convert[me: Self]() -> U { return __EqualConvert(me, U); }
 }
 
 // TODO: Simplify this once we have variadics.
diff --git a/explorer/interpreter/impl_scope.cpp b/explorer/interpreter/impl_scope.cpp
index f6a4342c5c41a..e76407af954fc 100644
--- a/explorer/interpreter/impl_scope.cpp
+++ b/explorer/interpreter/impl_scope.cpp
@@ -103,7 +103,34 @@ auto ImplScope::Resolve(Nonnull<const Value*> constraint_type,
                            source_loc, type_checker));
       witnesses.push_back(result);
     }
-    // TODO: Check satisfaction of same-type constraints.
+
+    // Check that all equality constraints are satisfied in this scope.
+    if (llvm::ArrayRef<EqualityConstraint> equals =
+            constraint->equality_constraints();
+        !equals.empty()) {
+      std::optional<Nonnull<const Witness*>> witness;
+      if (constraint->self_binding()->impl_binding()) {
+        witness = type_checker.MakeConstraintWitness(*constraint, witnesses,
+                                                     source_loc);
+      }
+      Bindings local_bindings = bindings;
+      local_bindings.Add(constraint->self_binding(), impl_type, witness);
+      SingleStepEqualityContext equality_ctx(this);
+      for (auto& equal : equals) {
+        auto it = equal.values.begin();
+        Nonnull<const Value*> first =
+            type_checker.Substitute(local_bindings, *it++);
+        for (; it != equal.values.end(); ++it) {
+          Nonnull<const Value*> current =
+              type_checker.Substitute(local_bindings, *it);
+          if (!ValueEqual(first, current, &equality_ctx)) {
+            return ProgramError(source_loc)
+                   << "constraint requires that " << *first
+                   << " == " << *current << ", which is not known to be true";
+          }
+        }
+      }
+    }
     return type_checker.MakeConstraintWitness(*constraint, std::move(witnesses),
                                               source_loc);
   }
@@ -233,4 +260,10 @@ void ImplScope::Print(llvm::raw_ostream& out) const {
   }
 }
 
+auto SingleStepEqualityContext::VisitEqualValues(
+    Nonnull<const Value*> value,
+    llvm::function_ref<bool(Nonnull<const Value*>)> visitor) const -> bool {
+  return impl_scope_->VisitEqualValues(value, visitor);
+}
+
 }  // namespace Carbon
diff --git a/explorer/interpreter/impl_scope.h b/explorer/interpreter/impl_scope.h
index 417fcc406e225..0ddef15eef29b 100644
--- a/explorer/interpreter/impl_scope.h
+++ b/explorer/interpreter/impl_scope.h
@@ -153,6 +153,26 @@ class ImplScope {
   std::vector<Nonnull<const ImplScope*>> parent_scopes_;
 };
 
+// An equality context that considers two values to be equal if they are a
+// single step apart according to an equality constraint in the given impl
+// scope.
+struct SingleStepEqualityContext : public EqualityContext {
+ public:
+  SingleStepEqualityContext(Nonnull<const ImplScope*> impl_scope)
+      : impl_scope_(impl_scope) {}
+
+  // Visits the values that are equal to the given value and a single step away
+  // according to an equality constraint that is in the given impl scope. Stops
+  // and returns `false` if the visitor returns `false`, otherwise returns
+  // `true`.
+  auto VisitEqualValues(Nonnull<const Value*> value,
+                        llvm::function_ref<bool(Nonnull<const Value*>)> visitor)
+      const -> bool override;
+
+ private:
+  Nonnull<const ImplScope*> impl_scope_;
+};
+
 }  // namespace Carbon
 
 #endif  // CARBON_EXPLORER_INTERPRETER_IMPL_SCOPE_H_
diff --git a/explorer/interpreter/interpreter.cpp b/explorer/interpreter/interpreter.cpp
index 5696e2c2bd1ef..8840f308c9764 100644
--- a/explorer/interpreter/interpreter.cpp
+++ b/explorer/interpreter/interpreter.cpp
@@ -538,35 +538,47 @@ auto Interpreter::EvalRecursively(std::unique_ptr<Action> action)
 auto Interpreter::EvalAssociatedConstant(
     Nonnull<const AssociatedConstant*> assoc, SourceLocation source_loc)
     -> ErrorOr<Nonnull<const Value*>> {
-  // Find the witness.
+  // Instantiate the associated constant.
+  CARBON_ASSIGN_OR_RETURN(Nonnull<const Value*> base,
+                          InstantiateType(&assoc->base(), source_loc));
+  CARBON_ASSIGN_OR_RETURN(Nonnull<const Value*> interface,
+                          InstantiateType(&assoc->interface(), source_loc));
   CARBON_ASSIGN_OR_RETURN(Nonnull<const Witness*> witness,
                           InstantiateWitness(&assoc->witness()));
-  if (!isa<ImplWitness>(witness)) {
+  Nonnull<const AssociatedConstant*> instantiated_assoc =
+      arena_->New<AssociatedConstant>(base, cast<InterfaceType>(interface),
+                                      &assoc->constant(), witness);
+
+  auto* impl_witness = dyn_cast<ImplWitness>(witness);
+  if (!impl_witness) {
     CARBON_CHECK(phase() == Phase::CompileTime)
         << "symbolic witnesses should only be formed at compile time";
-    return ProgramError(source_loc)
-           << "value of associated constant " << *assoc << " is not known";
+    return instantiated_assoc;
   }
 
-  auto& impl_witness = cast<ImplWitness>(*witness);
+  // We have an impl. Extract the value from it.
   Nonnull<const ConstraintType*> constraint =
-      impl_witness.declaration().constraint_type();
+      impl_witness->declaration().constraint_type();
   std::optional<Nonnull<const Value*>> result;
-  constraint->VisitEqualValues(assoc, [&](Nonnull<const Value*> equal_value) {
-    // TODO: The value might depend on the parameters of the impl. We need to
-    // substitute impl_witness.type_args() into the value or constraint.
-    if (isa<AssociatedConstant>(equal_value)) {
-      return true;
-    }
-    // TODO: This makes an arbitrary choice if there's more than one equal
-    // value. It's not clear how to handle that case.
-    result = equal_value;
-    return false;
-  });
+  // TODO: We should pick the value from the rewrite constraint, not some other
+  // equality constraint that happens to be in the impl's constraint type.
+  constraint->VisitEqualValues(instantiated_assoc,
+                               [&](Nonnull<const Value*> equal_value) {
+                                 // TODO: The value might depend on the
+                                 // parameters of the impl. We need to
+                                 // substitute impl_witness->type_args() into
+                                 // the value or constraint.
+                                 if (isa<AssociatedConstant>(equal_value)) {
+                                   return true;
+                                 }
+                                 result = equal_value;
+                                 return false;
+                               });
   if (!result) {
-    CARBON_FATAL() << impl_witness.declaration() << " with constraint "
+    CARBON_FATAL() << impl_witness->declaration() << " with constraint "
                    << *constraint
-                   << " is missing value for associated constant " << *assoc;
+                   << " is missing value for associated constant "
+                   << *instantiated_assoc;
   }
   return *result;
 }
@@ -585,6 +597,14 @@ auto Interpreter::InstantiateType(Nonnull<const Value*> type,
       }
       return value;
     }
+    case Value::Kind::InterfaceType: {
+      const auto& interface_type = cast<InterfaceType>(*type);
+      CARBON_ASSIGN_OR_RETURN(
+          Nonnull<const Bindings*> bindings,
+          InstantiateBindings(&interface_type.bindings(), source_loc));
+      return arena_->New<InterfaceType>(&interface_type.declaration(),
+                                        bindings);
+    }
     case Value::Kind::NominalClassType: {
       const auto& class_type = cast<NominalClassType>(*type);
       CARBON_ASSIGN_OR_RETURN(
@@ -603,7 +623,7 @@ auto Interpreter::InstantiateType(Nonnull<const Value*> type,
       CARBON_ASSIGN_OR_RETURN(
           Nonnull<const Value*> type_value,
           EvalAssociatedConstant(cast<AssociatedConstant>(type), source_loc));
-      return InstantiateType(type_value, source_loc);
+      return type_value;
     }
     default:
       return type;
@@ -715,9 +735,12 @@ auto Interpreter::Convert(Nonnull<const Value*> value,
               InstantiateType(destination_type, source_loc));
           return arena_->New<NominalClassValue>(inst_dest, value);
         }
-        default:
-          CARBON_FATAL() << "Can't convert value " << *value << " to type "
-                         << *destination_type;
+        default: {
+          CARBON_CHECK(IsValueKindDependent(destination_type))
+              << "Can't convert value " << *value << " to type "
+              << *destination_type;
+          return value;
+        }
       }
     }
     case Value::Kind::StructType: {
@@ -747,9 +770,12 @@ auto Interpreter::Convert(Nonnull<const Value*> value,
                                            &array_type.element_type());
           break;
         }
-        default:
-          CARBON_FATAL() << "Can't convert value " << *value << " to type "
-                         << *destination_type;
+        default: {
+          CARBON_CHECK(IsValueKindDependent(destination_type))
+              << "Can't convert value " << *value << " to type "
+              << *destination_type;
+          return value;
+        }
       }
       CARBON_CHECK(tuple->elements().size() ==
                    destination_element_types.size());
@@ -767,6 +793,10 @@ auto Interpreter::Convert(Nonnull<const Value*> value,
       CARBON_ASSIGN_OR_RETURN(
           Nonnull<const Value*> value,
           EvalAssociatedConstant(cast<AssociatedConstant>(value), source_loc));
+      if (isa<AssociatedConstant>(value)) {
+        return ProgramError(source_loc)
+               << "value of associated constant " << *value << " is not known";
+      }
       return Convert(value, destination_type, source_loc);
     }
   }
diff --git a/explorer/interpreter/type_checker.cpp b/explorer/interpreter/type_checker.cpp
index e17dd28a031ec..95eba1afa6dee 100644
--- a/explorer/interpreter/type_checker.cpp
+++ b/explorer/interpreter/type_checker.cpp
@@ -32,68 +32,6 @@ using llvm::isa;
 
 namespace Carbon {
 
-struct TypeChecker::SingleStepEqualityContext : public EqualityContext {
- public:
-  SingleStepEqualityContext(Nonnull<const TypeChecker*> type_checker,
-                            Nonnull<const ImplScope*> impl_scope)
-      : type_checker_(type_checker), impl_scope_(impl_scope) {}
-
-  // Visits the values that are equal to the given value and a single step away
-  // according to an equality constraint that is either scope or within a final
-  // impl corresponding to an associated constant. Stops and returns `false` if
-  // the visitor returns `false`, otherwise returns `true`.
-  auto VisitEqualValues(Nonnull<const Value*> value,
-                        llvm::function_ref<bool(Nonnull<const Value*>)> visitor)
-      const -> bool override {
-    if (type_checker_->trace_stream_) {
-      **type_checker_->trace_stream_ << "looking for values equal to " << *value
-                                     << " in\n"
-                                     << *impl_scope_;
-    }
-
-    if (!impl_scope_->VisitEqualValues(value, visitor)) {
-      return false;
-    }
-
-    // Also look up and visit the corresponding impl if this is an associated
-    // constant.
-    if (auto* assoc = dyn_cast<AssociatedConstant>(value)) {
-      // Perform an impl lookup to see if we can resolve this constant.
-      // The source location doesn't matter, we're discarding the diagnostics.
-      if (auto* impl_witness = dyn_cast<ImplWitness>(&assoc->witness())) {
-        // Instantiate the impl to find the concrete constraint it implements.
-        Nonnull<const ConstraintType*> constraint =
-            impl_witness->declaration().constraint_type();
-        constraint = cast<ConstraintType>(
-            type_checker_->Substitute(impl_witness->bindings(), constraint));
-        if (type_checker_->trace_stream_) {
-          **type_checker_->trace_stream_ << "found constraint " << *constraint
-                                         << " for associated constant "
-                                         << *assoc << "\n";
-        }
-
-        // Look for the value of this constant within that constraint.
-        if (!constraint->VisitEqualValues(value, visitor)) {
-          return false;
-        }
-      } else {
-        if (type_checker_->trace_stream_) {
-          **type_checker_->trace_stream_
-              << "Could not resolve associated constant " << *assoc << ": "
-              << "witness " << assoc->witness()
-              << " depends on a generic parameter\n";
-        }
-      }
-    }
-
-    return true;
-  }
-
- private:
-  Nonnull<const TypeChecker*> type_checker_;
-  Nonnull<const ImplScope*> impl_scope_;
-};
-
 static void SetValue(Nonnull<Pattern*> pattern, Nonnull<const Value*> value) {
   // TODO: find some way to CHECK that `value` is identical to pattern->value(),
   // if it's already set. Unclear if `ValueEqual` is suitable, because it
@@ -107,8 +45,7 @@ static void SetValue(Nonnull<Pattern*> pattern, Nonnull<const Value*> value) {
 auto TypeChecker::IsSameType(Nonnull<const Value*> type1,
                              Nonnull<const Value*> type2,
                              const ImplScope& impl_scope) const -> bool {
-  SingleStepEqualityContext equality_ctx(this, &impl_scope);
-  return TypeEqual(type1, type2, &equality_ctx);
+  return TypeEqual(type1, type2, std::nullopt);
 }
 
 auto TypeChecker::ExpectExactType(SourceLocation source_loc,
@@ -1223,8 +1160,8 @@ class TypeChecker::ConstraintTypeBuilder {
                << "multiple different rewrites for `.("
                << *rewrite.interface << "." << *GetName(*rewrite.constant)
                << ")`:\n"
-               << "  " << *existing.replacement << "\n"
-               << "  " << *rewrite.replacement;
+               << "  " << existing.replacement->value() << "\n"
+               << "  " << rewrite.replacement->value();
       }
     }
     rewrite_constraints_.push_back(std::move(rewrite));
@@ -1340,6 +1277,7 @@ class TypeChecker::ConstraintTypeBuilder {
     }
     impl_scope->Add(impl_constraints, llvm::None, llvm::None, GetSelfWitness(),
                     type_checker);
+    // TODO: Bring equality constraints into scope too.
   }
 
   // Converts the builder into a ConstraintType. Note that this consumes the
@@ -3156,9 +3094,11 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
       ImplScope inner_impl_scope;
       inner_impl_scope.AddParent(&impl_scope);
 
+      auto& self = where.self_binding();
+      ConstraintTypeBuilder builder(arena_, &self);
+
       // Note, we don't want to call `TypeCheckPattern` here. Most of the setup
       // for the self binding is instead done by the `ConstraintTypeBuilder`.
-      auto& self = where.self_binding();
       CARBON_ASSIGN_OR_RETURN(Nonnull<const Value*> base_type,
                               TypeCheckTypeExp(&self.type(), impl_scope));
       self.set_static_type(base_type);
@@ -3170,7 +3110,6 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
                                   base_type));
 
       // Start with the given constraint.
-      ConstraintTypeBuilder builder(arena_, &self);
       CARBON_RETURN_IF_ERROR(
           builder.AddAndSubstitute(*this, base, builder.GetSelfType(),
                                    builder.GetSelfWitness(), Bindings(),
@@ -3264,6 +3203,16 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
                 rewrite_clause.source_loc(), {.interface = result.interface,
                                               .constant = constant,
                                               .replacement = replacement}));
+            // Also find (or add) `.Self is I`, and add `.Self.T == V`.
+            int index = builder.AddImplConstraint(
+                {.type = builder.GetSelfType(), .interface = result.interface});
+            auto* witness =
+                MakeConstraintWitnessAccess(builder.GetSelfWitness(), index);
+            builder.AddEqualityConstraint(
+                {.values = {arena_->New<AssociatedConstant>(
+                                builder.GetSelfType(), result.interface,
+                                constant, witness),
+                            replacement_value}});
             break;
           }
         }
@@ -3466,6 +3415,13 @@ auto TypeChecker::TypeCheckPattern(
     }
     case PatternKind::GenericBinding: {
       auto& binding = cast<GenericBinding>(*p);
+
+      // The binding can be referred to in its own type via `.Self`, so set up
+      // its symbolic identity before we type-check and interpret the type.
+      auto* val = arena_->New<VariableType>(&binding);
+      binding.set_symbolic_identity(val);
+      SetValue(&binding, val);
+
       CARBON_ASSIGN_OR_RETURN(Nonnull<const Value*> type,
                               TypeCheckTypeExp(&binding.type(), impl_scope));
       if (expected) {
@@ -3479,10 +3435,6 @@ auto TypeChecker::TypeCheckPattern(
                << "`.Self` used in type of non-type binding `" << binding.name()
                << "`";
       }
-      CARBON_ASSIGN_OR_RETURN(Nonnull<const Value*> val,
-                              InterpPattern(&binding, arena_, trace_stream_));
-      binding.set_symbolic_identity(val);
-      SetValue(&binding, val);
 
       // Create an impl binding if we have a constraint.
       if (isa<ConstraintType, InterfaceType>(type)) {
@@ -4477,50 +4429,11 @@ auto TypeChecker::CheckImplIsComplete(Nonnull<const InterfaceType*> iface_type,
   const auto& iface_decl = iface_type->declaration();
   for (Nonnull<Declaration*> m : iface_decl.members()) {
     if (auto* assoc = dyn_cast<AssociatedConstantDeclaration>(m)) {
-      // An associated constant must be given exactly one value.
-      if (LookupRewrite(impl_decl->constraint_type(), iface_type, assoc)) {
-        // OK, named by `=` constraint.
-        continue;
-      }
-
-      // TODO: Remove the rest of this and just reject if there's no `=`.
-      Nonnull<const Value*> expected = arena_->New<AssociatedConstant>(
-          self_type, iface_type, assoc, self_witness);
-
-      bool found_any = false;
-      std::optional<Nonnull<const Value*>> found_value;
-      std::optional<Nonnull<const Value*>> second_value;
-      auto visitor = [&](Nonnull<const Value*> equal_value) {
-        found_any = true;
-        if (!isa<AssociatedConstant>(equal_value)) {
-          if (!found_value ||
-              ValueEqual(equal_value, *found_value, std::nullopt)) {
-            found_value = equal_value;
-          } else {
-            second_value = equal_value;
-            return false;
-          }
-        }
-        return true;
-      };
-      impl_decl->constraint_type()->VisitEqualValues(expected, visitor);
-      if (!found_any) {
-        return ProgramError(impl_decl->source_loc())
-               << "implementation missing " << *expected << "; have "
-               << *impl_decl->constraint_type();
-      } else if (!found_value) {
-        // TODO: It's not clear what the right rule is here. Clearly
-        //   impl T as HasX & HasY where .X == .Y {}
-        // ... is insufficient to establish a value for either X or Y.
-        // But perhaps we can allow
-        //   impl forall [T:! HasX] T as HasY where .Y == .X {}
+      // An associated constant must be given a value.
+      if (!LookupRewrite(impl_decl->constraint_type(), iface_type, assoc)) {
         return ProgramError(impl_decl->source_loc())
                << "implementation doesn't provide a concrete value for "
-               << *expected;
-      } else if (second_value) {
-        return ProgramError(impl_decl->source_loc())
-               << "implementation provides multiple values for " << *expected
-               << ": " << **found_value << " and " << **second_value;
+               << *iface_type << "." << assoc->binding().name();
       }
     } else if (isa<InterfaceImplDeclaration, InterfaceExtendsDeclaration>(m)) {
       // These get translated into constraints so there's nothing we need to
@@ -4685,22 +4598,28 @@ auto TypeChecker::DeclareImplDeclaration(Nonnull<ImplDeclaration*> impl_decl,
         self_impl_scope.Add(iface_type, impl_type_value, self_witness, *this);
       }
     }
+    // This impl also provides all of its equalities.
+    // TODO: Only the ones from rewrite constraints.
+    for (auto& eq : constraint_type->equality_constraints()) {
+      self_impl_scope.AddEqualityConstraint(&eq);
+    }
     // Ensure that's enough for our interface to be satisfied.
     CARBON_ASSIGN_OR_RETURN(
         impl_witness, self_impl_scope.Resolve(constraint_type, impl_type_value,
                                               impl_decl->source_loc(), *this));
   }
 
-  // Declare the impl members.
-  ScopeInfo impl_scope_info = ScopeInfo::ForNonClassScope(&impl_scope);
+  // Declare the impl members. An `impl` behaves like a class scope.
+  ScopeInfo impl_scope_info =
+      ScopeInfo::ForClassScope(scope_info, &impl_scope, generic_bindings);
   for (Nonnull<Declaration*> m : impl_decl->members()) {
     CARBON_RETURN_IF_ERROR(DeclareDeclaration(m, impl_scope_info));
   }
 
   // Create the implied impl bindings.
-  CARBON_RETURN_IF_ERROR(CheckAndAddImplBindings(impl_decl, impl_type_value,
-                                                 self_witness, impl_witness,
-                                                 generic_bindings, scope_info));
+  CARBON_RETURN_IF_ERROR(
+      CheckAndAddImplBindings(impl_decl, impl_type_value, self_witness,
+                              impl_witness, generic_bindings, impl_scope_info));
 
   if (trace_stream_) {
     **trace_stream_ << "** finished declaring impl " << *impl_decl->impl_type()
diff --git a/explorer/interpreter/type_checker.h b/explorer/interpreter/type_checker.h
index 46ba32657b616..8525051841cd0 100644
--- a/explorer/interpreter/type_checker.h
+++ b/explorer/interpreter/type_checker.h
@@ -80,7 +80,6 @@ class TypeChecker {
       -> Nonnull<const Witness*>;
 
  private:
-  struct SingleStepEqualityContext;
   class ConstraintTypeBuilder;
   class SubstitutedGenericBindings;
   class ArgumentDeduction;
diff --git a/explorer/interpreter/value.cpp b/explorer/interpreter/value.cpp
index a0bc3a7dcda57..438f98328d87a 100644
--- a/explorer/interpreter/value.cpp
+++ b/explorer/interpreter/value.cpp
@@ -512,7 +512,10 @@ void Value::Print(llvm::raw_ostream& out) const {
       break;
     case Value::Kind::AssociatedConstant: {
       const auto& assoc = cast<AssociatedConstant>(*this);
-      out << "(" << assoc.base() << ")." << assoc.constant().binding().name();
+      out << "(" << assoc.base() << ").(";
+      PrintNameWithBindings(out, &assoc.interface().declaration(),
+                            assoc.interface().args());
+      out << "." << assoc.constant().binding().name() << ")";
       break;
     }
     case Value::Kind::ContinuationValue: {
@@ -629,7 +632,7 @@ auto TypeEqual(Nonnull<const Value*> t1, Nonnull<const Value*> t2,
     return true;
   }
   if (t1->kind() != t2->kind()) {
-    if (isa<AssociatedConstant>(t1) || isa<AssociatedConstant>(t2)) {
+    if (IsValueKindDependent(t1) || IsValueKindDependent(t2)) {
       return ValueEqual(t1, t2, equality_ctx);
     }
     return false;
@@ -942,7 +945,7 @@ auto ValueEqual(Nonnull<const Value*> v1, Nonnull<const Value*> v2,
   // associated constant; otherwise we should be able to do better by looking
   // at the structures of the values.
   if (equality_ctx) {
-    if (isa<AssociatedConstant>(v1)) {
+    if (IsValueKindDependent(v1)) {
       auto visitor = [&](Nonnull<const Value*> maybe_v2) {
         return !ValueStructurallyEqual(v2, maybe_v2, equality_ctx);
       };
@@ -950,7 +953,7 @@ auto ValueEqual(Nonnull<const Value*> v1, Nonnull<const Value*> v2,
         return true;
       }
     }
-    if (isa<AssociatedConstant>(v2)) {
+    if (IsValueKindDependent(v2)) {
       auto visitor = [&](Nonnull<const Value*> maybe_v1) {
         return !ValueStructurallyEqual(v1, maybe_v1, equality_ctx);
       };
diff --git a/explorer/interpreter/value.h b/explorer/interpreter/value.h
index 7da7d32c7a499..5df5e3e29e06c 100644
--- a/explorer/interpreter/value.h
+++ b/explorer/interpreter/value.h
@@ -121,6 +121,13 @@ class Value {
   const Kind kind_;
 };
 
+// Returns whether the fully-resolved kind that this value will eventually have
+// is currently unknown, because it depends on a generic parameter.
+inline bool IsValueKindDependent(Nonnull<const Value*> type) {
+  return type->kind() == Value::Kind::VariableType ||
+         type->kind() == Value::Kind::AssociatedConstant;
+}
+
 // Base class for types holding contextual information by which we can
 // determine whether values are equal.
 class EqualityContext {
diff --git a/explorer/testdata/assoc_const/fail_different_type.carbon b/explorer/testdata/assoc_const/fail_different_type.carbon
new file mode 100644
index 0000000000000..781c6d780826a
--- /dev/null
+++ b/explorer/testdata/assoc_const/fail_different_type.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
+//
+// RUN: %{not} %{explorer} %s | %{FileCheck-strict} %s
+// RUN: %{not} %{explorer-trace} %s | %{FileCheck-allow-unmatched} %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+interface Iface {
+  let T:! Type;
+}
+
+fn F(T:! Iface where .T == i32) {}
+
+class Good {}
+class Bad {}
+external impl Good as Iface where .T = i32 {}
+external impl Bad as Iface where .T = Bad {}
+
+fn Main() -> i32 {
+  F(Good);
+  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_different_type.carbon:[[@LINE+1]]: constraint requires that class Bad == i32, which is not known to be true
+  F(Bad);
+  return 0;
+}
diff --git a/explorer/testdata/assoc_const/fail_different_value.carbon b/explorer/testdata/assoc_const/fail_different_value.carbon
new file mode 100644
index 0000000000000..03b246fdff430
--- /dev/null
+++ b/explorer/testdata/assoc_const/fail_different_value.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
+//
+// RUN: %{not} %{explorer} %s | %{FileCheck-strict} %s
+// RUN: %{not} %{explorer-trace} %s | %{FileCheck-allow-unmatched} %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+interface Iface {
+  let N:! i32;
+}
+
+fn F(T:! Iface where .N == 5) {}
+
+class Good {}
+class Bad {}
+external impl Good as Iface where .N = 5 {}
+external impl Bad as Iface where .N = 4 {}
+
+fn Main() -> i32 {
+  F(Good);
+  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_different_value.carbon:[[@LINE+1]]: constraint requires that 4 == 5, which is not known to be true
+  F(Bad);
+  return 0;
+}
diff --git a/explorer/testdata/assoc_const/fail_equal_indirectly.carbon b/explorer/testdata/assoc_const/fail_equal_indirectly.carbon
new file mode 100644
index 0000000000000..8fdacf4ea17f9
--- /dev/null
+++ b/explorer/testdata/assoc_const/fail_equal_indirectly.carbon
@@ -0,0 +1,38 @@
+// 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
+//
+// RUN: %{not} %{explorer} %s | %{FileCheck-strict} %s
+// RUN: %{not} %{explorer-trace} %s | %{FileCheck-allow-unmatched} %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+interface Iface {
+  let T:! Type;
+}
+
+fn F[T:! Iface where .T == i32](x: T) {}
+
+class Class {
+  impl as Iface where .T = i32 {}
+}
+
+// OK, constraint on `F` rewritten to `T:! Iface where U == i32`, which we can
+// prove from the constraint on `U`.
+fn G[U:! Type where .Self == i32, T:! Iface where .T = U](x: T, y: U) {
+  F(x);
+}
+
+// Not OK: would require looking through two levels of `==`.
+fn H[U:! Type where .Self == i32, T:! Iface where .T == U](x: T, y: U) {
+  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_equal_indirectly.carbon:[[@LINE+1]]: constraint requires that (T).(Iface.T) == i32, which is not known to be true
+  F(x);
+}
+
+fn Main() -> i32 {
+  var x: Class = {};
+  G(x, 0);
+  H(x, 0);
+  return 0;
+}
diff --git a/explorer/testdata/assoc_const/fail_equal_to_dependent_type.carbon b/explorer/testdata/assoc_const/fail_equal_to_dependent_type.carbon
new file mode 100644
index 0000000000000..aae9fafb1da0e
--- /dev/null
+++ b/explorer/testdata/assoc_const/fail_equal_to_dependent_type.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
+//
+// RUN: %{not} %{explorer} %s | %{FileCheck-strict} %s
+// RUN: %{not} %{explorer-trace} %s | %{FileCheck-allow-unmatched} %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+interface Iface {
+  let T:! Type;
+}
+
+fn F[T:! Iface where .T == i32](x: T) {}
+
+fn G[T:! Iface where .T == i32](x: T) {
+  F(x);
+}
+
+fn H[T:! Iface](x: T) {
+  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_equal_to_dependent_type.carbon:[[@LINE+1]]: constraint requires that (T).(Iface.T) == i32, which is not known to be true
+  F(x);
+}
+
+class Class {
+  impl as Iface where .T = i32 {}
+}
+
+fn Main() -> i32 {
+  var x: Class = {};
+  G(x);
+  H(x);
+  return 0;
+}
diff --git a/explorer/testdata/assoc_const/fail_incomplete_impl_1.carbon b/explorer/testdata/assoc_const/fail_incomplete_impl_1.carbon
index 6961b64677841..a30d59a16f9bb 100644
--- a/explorer/testdata/assoc_const/fail_incomplete_impl_1.carbon
+++ b/explorer/testdata/assoc_const/fail_incomplete_impl_1.carbon
@@ -14,7 +14,7 @@ interface HasThreeTypes {
   let C:! Type;
 }
 
-// CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_incomplete_impl_1.carbon:[[@LINE+1]]: implementation missing (i32).B; have constraint interface HasThreeTypes where i32 is interface HasThreeTypes and (i32).A == i32 and (i32).C == i32
-external impl i32 as HasThreeTypes where .A == i32 and .C == i32 {}
+// CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_incomplete_impl_1.carbon:[[@LINE+1]]: implementation doesn't provide a concrete value for interface HasThreeTypes.B
+external impl i32 as HasThreeTypes where .A = i32 and .C = i32 {}
 
 fn Main() -> i32 { return 0; }
diff --git a/explorer/testdata/assoc_const/fail_incomplete_impl_2.carbon b/explorer/testdata/assoc_const/fail_incomplete_impl_2.carbon
index 2cc63a58e3f2a..ca3c05bb97695 100644
--- a/explorer/testdata/assoc_const/fail_incomplete_impl_2.carbon
+++ b/explorer/testdata/assoc_const/fail_incomplete_impl_2.carbon
@@ -14,7 +14,7 @@ interface HasThreeTypes {
   let C:! Type;
 }
 
-// CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_incomplete_impl_2.carbon:[[@LINE+1]]: implementation doesn't provide a concrete value for (i32).B
-external impl i32 as HasThreeTypes where .A == i32 and .B == .C {}
+// CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_incomplete_impl_2.carbon:[[@LINE+1]]: implementation doesn't provide a concrete value for interface HasThreeTypes.C
+external impl i32 as HasThreeTypes where .A = i32 and .B = .C {}
 
 fn Main() -> i32 { return 0; }
diff --git a/explorer/testdata/assoc_const/fail_indirectly_equal.carbon b/explorer/testdata/assoc_const/fail_indirectly_equal.carbon
index 999b73b0b9c4b..987f0bd821edd 100644
--- a/explorer/testdata/assoc_const/fail_indirectly_equal.carbon
+++ b/explorer/testdata/assoc_const/fail_indirectly_equal.carbon
@@ -23,7 +23,7 @@ fn F2[U:! A where .T == i32](x: i32) -> U.T {
 }
 
 fn F3[T:! A where .T == i32, U:! A where .T == i32](x: T.T) -> U.T {
-  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_indirectly_equal.carbon:[[@LINE+1]]: type error in return value: '(T).T' is not implicitly convertible to '(U).T'
+  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_indirectly_equal.carbon:[[@LINE+1]]: type error in return value: '(T).(A.T)' is not implicitly convertible to '(U).(A.T)'
   return x;
 }
 
diff --git a/explorer/testdata/assoc_const/fail_match_in_deduction.carbon b/explorer/testdata/assoc_const/fail_match_in_deduction.carbon
index b23b0a8f2cc57..6ac562ed1f480 100644
--- a/explorer/testdata/assoc_const/fail_match_in_deduction.carbon
+++ b/explorer/testdata/assoc_const/fail_match_in_deduction.carbon
@@ -13,7 +13,7 @@ package ExplorerTest api;
 interface Vector {
   let Dim:! i32;
 }
-external impl (i32, i32, i32) as Vector where .Dim == 3 {}
+external impl (i32, i32, i32) as Vector where .Dim = 3 {}
 
 class Point(Scalar:! Type, Dim:! i32) {}
 
@@ -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).Dim` != `3`
+  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_match_in_deduction.carbon:[[@LINE+1]]: mismatch in non-type values, `(V).(Vector.Dim)` != `3`
   G(p);
 }
 
diff --git a/explorer/testdata/assoc_const/fail_multi_impl_scoping.carbon b/explorer/testdata/assoc_const/fail_multi_impl_scoping.carbon
index 59c5ac4f58bb3..51a3c624d6798 100644
--- a/explorer/testdata/assoc_const/fail_multi_impl_scoping.carbon
+++ b/explorer/testdata/assoc_const/fail_multi_impl_scoping.carbon
@@ -18,7 +18,7 @@ interface B {
 }
 
 class C(T:! Type) {
-  impl as A & B where .TA == i32 and .TB == i32 {
+  impl as A & B where .TA = i32 and .TB = i32 {
     fn FA() -> i32 {
       // OK, know that TA is i32 here.
       let v: Self.(A.TA) = 1;
@@ -29,10 +29,8 @@ class C(T:! Type) {
       // OK, know that TB is i32 here.
       let v: Self.(B.TB) = 2;
       // Don't know that TA is i32; it could be specialized.
+      // TODO: We should not accept this.
       let w: Self.(A.TA) = 3;
-      // TODO: This error is confusing. We should be diagnosing the previous
-      // line because we don't know that `3` can be converted to `Self.(A.TA)`.
-      // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_multi_impl_scoping.carbon:[[@LINE+1]]: type error in return value: '((class C(T = T)).TB).Result' is not implicitly convertible to 'i32'
       return v + w;
     }
   }
@@ -40,6 +38,7 @@ class C(T:! Type) {
 
 external impl C(i32) as B where .TB == () {
   fn FB() -> () { return (); }
+// CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_multi_impl_scoping.carbon:[[@LINE+1]]: ambiguous implementations of interface B for class C(T = i32)
 }
 
 fn Main() -> i32 { return C(i32).FB(); }
diff --git a/explorer/testdata/assoc_const/fail_multiple_deduction.carbon b/explorer/testdata/assoc_const/fail_multiple_deduction.carbon
index 498f1f8e365bd..5324eb1dfc60e 100644
--- a/explorer/testdata/assoc_const/fail_multiple_deduction.carbon
+++ b/explorer/testdata/assoc_const/fail_multiple_deduction.carbon
@@ -17,8 +17,8 @@ interface HasThreeTypes {
 fn F[T:! Type](x: (T, T, T));
 fn G[X:! HasThreeTypes where .A == .B and .B == .C and .C == .A](x: X) {
   // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_multiple_deduction.carbon:[[@LINE+3]]: deduced multiple different values for T:! Type:
-  // CHECK:STDERR:   (X).A
-  // CHECK:STDERR:   (X).B
+  // CHECK:STDERR:   (X).(HasThreeTypes.A)
+  // CHECK:STDERR:   (X).(HasThreeTypes.B)
   F(x.Make());
 }
 
diff --git a/explorer/testdata/assoc_const/fail_overspecified_impl.carbon b/explorer/testdata/assoc_const/fail_overspecified_impl.carbon
index 23c5068a8fd11..cfbf668f0df0f 100644
--- a/explorer/testdata/assoc_const/fail_overspecified_impl.carbon
+++ b/explorer/testdata/assoc_const/fail_overspecified_impl.carbon
@@ -12,7 +12,9 @@ interface HasType {
   let T:! Type;
 }
 
-// CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_overspecified_impl.carbon:[[@LINE+1]]: implementation provides multiple values for (i32).T: i32 and {.a: i32}
-external impl i32 as HasType where .T == i32 and .T == {.a: i32} {}
+// CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_overspecified_impl.carbon:[[@LINE+3]]: multiple different rewrites for `.(interface HasType.T)`:
+// CHECK:STDERR:   i32
+// CHECK:STDERR:   {.a: i32}
+external impl i32 as HasType where .T = i32 and .T = {.a: i32} {}
 
 fn Main() -> i32 { return 0; }
diff --git a/explorer/testdata/assoc_const/fail_unknown_value.carbon b/explorer/testdata/assoc_const/fail_unknown_value.carbon
index c2dc2874cc8de..5b6412792dad0 100644
--- a/explorer/testdata/assoc_const/fail_unknown_value.carbon
+++ b/explorer/testdata/assoc_const/fail_unknown_value.carbon
@@ -13,12 +13,12 @@ interface Iface { let N:! i32; }
 fn PickType(N: i32) -> Type { return i32; }
 
 fn F[T:! Iface](x: T) -> i32 {
-  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_unknown_value.carbon:[[@LINE+1]]: value of associated constant (T).N is not known
+  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_unknown_value.carbon:[[@LINE+1]]: value of associated constant (T).(Iface.N) is not known
   var x: PickType(T.N) = 0;
   return x;
 }
 
-impl i32 as Iface where .N == 5 {}
+impl i32 as Iface where .N = 5 {}
 
 fn Main() -> i32 {
   return F(0);
diff --git a/explorer/testdata/assoc_const/fail_unknown_value_specified_in_constraint.carbon b/explorer/testdata/assoc_const/fail_unknown_value_specified_in_constraint.carbon
index 4ef7b220ca891..6049deb5f1826 100644
--- a/explorer/testdata/assoc_const/fail_unknown_value_specified_in_constraint.carbon
+++ b/explorer/testdata/assoc_const/fail_unknown_value_specified_in_constraint.carbon
@@ -14,7 +14,7 @@ fn PickType(N: i32) -> Type { return i32; }
 
 fn F[T:! Iface where .N == 5](x: T) -> i32 {
   // TODO: This should be valid: the value of T.N is known to be 5 here.
-  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_unknown_value_specified_in_constraint.carbon:[[@LINE+1]]: value of associated constant (T).N is not known
+  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_unknown_value_specified_in_constraint.carbon:[[@LINE+1]]: value of associated constant (T).(Iface.N) is not known
   var x: PickType(T.N) = 0;
   return x;
 }
diff --git a/explorer/testdata/assoc_const/impl_lookup.carbon b/explorer/testdata/assoc_const/impl_lookup.carbon
index 392e19018fd34..e2362f4839b88 100644
--- a/explorer/testdata/assoc_const/impl_lookup.carbon
+++ b/explorer/testdata/assoc_const/impl_lookup.carbon
@@ -26,7 +26,7 @@ class AlmostI32 {
   }
 }
 
-impl i32 as Frob where .Result == AlmostI32 {
+impl i32 as Frob where .Result = AlmostI32 {
   fn F[me: Self]() -> AlmostI32 { return {.val = me}; }
 }
 
diff --git a/explorer/testdata/assoc_const/implement.carbon b/explorer/testdata/assoc_const/implement.carbon
index db2454e6ef7f4..644b90af61459 100644
--- a/explorer/testdata/assoc_const/implement.carbon
+++ b/explorer/testdata/assoc_const/implement.carbon
@@ -16,7 +16,7 @@ interface Vector {
 class Point {
   var x: i32;
   var y: i32;
-  impl as Vector where .Dim == 2 {}
+  impl as Vector where .Dim = 2 {}
 }
 
 fn Main() -> i32 {
diff --git a/explorer/testdata/assoc_const/member_of_value.carbon b/explorer/testdata/assoc_const/member_of_value.carbon
index fb1506356767d..ee95534951f26 100644
--- a/explorer/testdata/assoc_const/member_of_value.carbon
+++ b/explorer/testdata/assoc_const/member_of_value.carbon
@@ -16,7 +16,7 @@ interface Vector {
 class Point {
   var x: i32;
   var y: i32;
-  impl as Vector where .Dim == 2 {}
+  impl as Vector where .Dim = 2 {}
 }
 
 fn Main() -> i32 {
diff --git a/explorer/testdata/assoc_const/pass_equal_to_rewrite.carbon b/explorer/testdata/assoc_const/pass_equal_to_rewrite.carbon
new file mode 100644
index 0000000000000..47acbdbf695f9
--- /dev/null
+++ b/explorer/testdata/assoc_const/pass_equal_to_rewrite.carbon
@@ -0,0 +1,34 @@
+// 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
+//
+// RUN: %{explorer} %s | %{FileCheck-strict} %s
+// RUN: %{explorer-trace} %s | %{FileCheck-allow-unmatched} %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK:STDOUT: result: 1
+
+package ExplorerTest api;
+
+interface Container {
+  let Element:! Type;
+  fn Front[me: Self]() -> Element;
+}
+
+fn A[T:! Container where .Element = i32](x: T) -> T.Element {
+  return x.Front();
+}
+
+fn B[T:! Container where .Element == i32](x: T) -> T.Element {
+  return A(x);
+}
+
+external impl (i32, i32) as Container where .Element = i32 {
+  fn Front[me: Self]() -> i32 {
+    let (a: i32, b: i32) = me;
+    return a;
+  }
+}
+
+fn Main() -> i32 {
+  return B((1, 2));
+}
diff --git a/explorer/testdata/assoc_const/pass_rewrite_to_equal.carbon b/explorer/testdata/assoc_const/pass_rewrite_to_equal.carbon
new file mode 100644
index 0000000000000..8305026dd8a49
--- /dev/null
+++ b/explorer/testdata/assoc_const/pass_rewrite_to_equal.carbon
@@ -0,0 +1,34 @@
+// 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
+//
+// RUN: %{explorer} %s | %{FileCheck-strict} %s
+// RUN: %{explorer-trace} %s | %{FileCheck-allow-unmatched} %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK:STDOUT: result: 1
+
+package ExplorerTest api;
+
+interface Container {
+  let Element:! Type;
+  fn Front[me: Self]() -> Element;
+}
+
+fn A[T:! Container where .Element == i32](x: T) -> T.Element {
+  return x.Front();
+}
+
+fn B[T:! Container where .Element = i32](x: T) -> T.Element {
+  return A(x);
+}
+
+external impl (i32, i32) as Container where .Element = i32 {
+  fn Front[me: Self]() -> i32 {
+    let (a: i32, b: i32) = me;
+    return a;
+  }
+}
+
+fn Main() -> i32 {
+  return B((1, 2));
+}
diff --git a/explorer/testdata/assoc_const/simple_constraint.carbon b/explorer/testdata/assoc_const/simple_constraint.carbon
index 72c9796959533..090a1b21244d6 100644
--- a/explorer/testdata/assoc_const/simple_constraint.carbon
+++ b/explorer/testdata/assoc_const/simple_constraint.carbon
@@ -14,12 +14,12 @@ interface Frob {
   fn F[me: Self]() -> Result;
 }
 
-fn Use[T:! Frob where .Result == .Self](x: T) -> T {
+fn Use[T:! Frob where .Result = .Self](x: T) -> T {
   var v: T = x.F();
   return v;
 }
 
-impl i32 as Frob where .Result == i32 {
+impl i32 as Frob where .Result = i32 {
   fn F[me: Self]() -> i32 { return me + 1; }
 }
 
diff --git a/explorer/testdata/assoc_const/simple_equality.carbon b/explorer/testdata/assoc_const/simple_equality.carbon
index 11198f5013d08..4cf1a82e7917d 100644
--- a/explorer/testdata/assoc_const/simple_equality.carbon
+++ b/explorer/testdata/assoc_const/simple_equality.carbon
@@ -19,7 +19,7 @@ fn Use[T:! Frob](x: T) -> T.Result {
   return v;
 }
 
-impl i32 as Frob where .Result == i32 {
+impl i32 as Frob where .Result = i32 {
   fn F[me: Self]() -> i32 { return 0; }
 }
 
diff --git a/explorer/testdata/constraint/binding_dot_self_in_constraint.carbon b/explorer/testdata/constraint/binding_dot_self_in_constraint.carbon
new file mode 100644
index 0000000000000..f06d95024dc4e
--- /dev/null
+++ b/explorer/testdata/constraint/binding_dot_self_in_constraint.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
+//
+// RUN: %{explorer} %s | %{FileCheck-strict} %s
+// RUN: %{explorer-trace} %s | %{FileCheck-allow-unmatched} %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK:STDOUT: result: 6
+
+package ExplorerTest api;
+
+// The constraint here resolves to:
+//
+//   MulWith(T) where <ConstraintSelf>.(MulWith(T).Result) == <ConstraintSelf>
+//
+// Note in particular that this involves a member of `MulWith(T)`, so we need
+// `T` to have a symbolic identity when checking its own type.
+fn DoMul[T:! MulWith(.Self) where .Result == .Self](x: T, y: T) -> T {
+  return x * y;
+}
+
+fn Main() -> i32 {
+  return DoMul(2, 3);
+}
diff --git a/explorer/testdata/operators/add.carbon b/explorer/testdata/operators/add.carbon
index 319ec44989ae2..83859cb92e197 100644
--- a/explorer/testdata/operators/add.carbon
+++ b/explorer/testdata/operators/add.carbon
@@ -11,7 +11,7 @@ package ExplorerTest api;
 
 class A { var n: i32; }
 
-external impl A as AddWith(i32) where .Result == A {
+external impl A as AddWith(i32) where .Result = A {
   fn Op[me: Self](rhs: i32) -> A { return {.n = me.n + rhs}; }
 }
 
diff --git a/explorer/testdata/operators/bit_and.carbon b/explorer/testdata/operators/bit_and.carbon
index 799586ca38efe..45256e82518d4 100644
--- a/explorer/testdata/operators/bit_and.carbon
+++ b/explorer/testdata/operators/bit_and.carbon
@@ -11,7 +11,7 @@ package ExplorerTest api;
 
 class A { var n: i32; }
 
-external impl A as BitAndWith(i32) where .Result == A {
+external impl A as BitAndWith(i32) where .Result = A {
   fn Op[me: Self](rhs: i32) -> A { return {.n = me.n & rhs}; }
 }
 
diff --git a/explorer/testdata/operators/bit_complement.carbon b/explorer/testdata/operators/bit_complement.carbon
index 61ac5493ed671..0091914e51fc5 100644
--- a/explorer/testdata/operators/bit_complement.carbon
+++ b/explorer/testdata/operators/bit_complement.carbon
@@ -11,7 +11,7 @@ package ExplorerTest api;
 
 class A { var n: i32; }
 
-external impl A as BitComplement where .Result == A {
+external impl A as BitComplement where .Result = A {
   fn Op[me: Self]() -> A { return {.n = ^me.n}; }
 }
 
diff --git a/explorer/testdata/operators/bit_or.carbon b/explorer/testdata/operators/bit_or.carbon
index d9d27a4f80a73..c418de94412bb 100644
--- a/explorer/testdata/operators/bit_or.carbon
+++ b/explorer/testdata/operators/bit_or.carbon
@@ -11,7 +11,7 @@ package ExplorerTest api;
 
 class A { var n: i32; }
 
-external impl A as BitOrWith(i32) where .Result == A {
+external impl A as BitOrWith(i32) where .Result = A {
   fn Op[me: Self](rhs: i32) -> A { return {.n = me.n | rhs}; }
 }
 
diff --git a/explorer/testdata/operators/bit_xor.carbon b/explorer/testdata/operators/bit_xor.carbon
index d58fd484e6780..36b2965fc6125 100644
--- a/explorer/testdata/operators/bit_xor.carbon
+++ b/explorer/testdata/operators/bit_xor.carbon
@@ -11,7 +11,7 @@ package ExplorerTest api;
 
 class A { var n: i32; }
 
-external impl A as BitXorWith(i32) where .Result == A {
+external impl A as BitXorWith(i32) where .Result = A {
   fn Op[me: Self](rhs: i32) -> A { return {.n = me.n ^ rhs}; }
 }
 
diff --git a/explorer/testdata/operators/div.carbon b/explorer/testdata/operators/div.carbon
index a14ded4a698f2..4bf95ce63d53d 100644
--- a/explorer/testdata/operators/div.carbon
+++ b/explorer/testdata/operators/div.carbon
@@ -11,7 +11,7 @@ package ExplorerTest api;
 
 class A { var n: i32; }
 
-external impl A as DivWith(i32) where .Result == A {
+external impl A as DivWith(i32) where .Result = A {
   fn Op[me: Self](rhs: i32) -> A { return {.n = me.n / rhs}; }
 }
 
diff --git a/explorer/testdata/operators/left_shift.carbon b/explorer/testdata/operators/left_shift.carbon
index a2d603e93590f..a27dfa25dfdc8 100644
--- a/explorer/testdata/operators/left_shift.carbon
+++ b/explorer/testdata/operators/left_shift.carbon
@@ -11,7 +11,7 @@ package ExplorerTest api;
 
 class A { var n: i32; }
 
-external impl A as LeftShiftWith(i32) where .Result == A {
+external impl A as LeftShiftWith(i32) where .Result = A {
   fn Op[me: Self](rhs: i32) -> A { return {.n = me.n << rhs}; }
 }
 
diff --git a/explorer/testdata/operators/mod.carbon b/explorer/testdata/operators/mod.carbon
index d0d2e0276691c..8742ecfee7b21 100644
--- a/explorer/testdata/operators/mod.carbon
+++ b/explorer/testdata/operators/mod.carbon
@@ -11,7 +11,7 @@ package ExplorerTest api;
 
 class A { var n: i32; }
 
-external impl A as ModWith(i32) where .Result == A {
+external impl A as ModWith(i32) where .Result = A {
   fn Op[me: Self](rhs: i32) -> A { return {.n = me.n % rhs}; }
 }
 
diff --git a/explorer/testdata/operators/mul.carbon b/explorer/testdata/operators/mul.carbon
index 9ac8ed5420eb0..248524a872b37 100644
--- a/explorer/testdata/operators/mul.carbon
+++ b/explorer/testdata/operators/mul.carbon
@@ -11,7 +11,7 @@ package ExplorerTest api;
 
 class A { var n: i32; }
 
-external impl A as MulWith(i32) where .Result == A {
+external impl A as MulWith(i32) where .Result = A {
   fn Op[me: Self](rhs: i32) -> A { return {.n = me.n * rhs}; }
 }
 
diff --git a/explorer/testdata/operators/negate.carbon b/explorer/testdata/operators/negate.carbon
index 6b9a6e0b7deb6..59ea6af25cd66 100644
--- a/explorer/testdata/operators/negate.carbon
+++ b/explorer/testdata/operators/negate.carbon
@@ -11,7 +11,7 @@ package ExplorerTest api;
 
 class A { var n: i32; }
 
-external impl A as Negate where .Result == A {
+external impl A as Negate where .Result = A {
   fn Op[me: Self]() -> A { return {.n = -me.n}; }
 }
 
diff --git a/explorer/testdata/operators/right_shift.carbon b/explorer/testdata/operators/right_shift.carbon
index ede1284055fb5..413e524dd7e24 100644
--- a/explorer/testdata/operators/right_shift.carbon
+++ b/explorer/testdata/operators/right_shift.carbon
@@ -11,7 +11,7 @@ package ExplorerTest api;
 
 class A { var n: i32; }
 
-external impl A as RightShiftWith(i32) where .Result == A {
+external impl A as RightShiftWith(i32) where .Result = A {
   fn Op[me: Self](rhs: i32) -> A { return {.n = me.n >> rhs}; }
 }
 
diff --git a/explorer/testdata/operators/sub.carbon b/explorer/testdata/operators/sub.carbon
index f929dabc4f34f..c5c5652b78198 100644
--- a/explorer/testdata/operators/sub.carbon
+++ b/explorer/testdata/operators/sub.carbon
@@ -11,7 +11,7 @@ package ExplorerTest api;
 
 class A { var n: i32; }
 
-external impl A as SubWith(i32) where .Result == A {
+external impl A as SubWith(i32) where .Result = A {
   fn Op[me: Self](rhs: i32) -> A { return {.n = me.n - rhs}; }
 }
 
diff --git a/explorer/testdata/print/associated_constant.carbon b/explorer/testdata/print/associated_constant.carbon
index 49f8e8b9ef22d..f9766ed108d64 100644
--- a/explorer/testdata/print/associated_constant.carbon
+++ b/explorer/testdata/print/associated_constant.carbon
@@ -15,8 +15,8 @@ interface HasName {
     let Name:! String;
 }
 
-external impl i32 as HasName where .Name == "i32" {}
-external impl String as HasName where .Name == "String" {}
+external impl i32 as HasName where .Name = "i32" {}
+external impl String as HasName where .Name = "String" {}
 
 fn Main() -> i32 {
     Print(i32.(HasName.Name));