diff --git a/common/fuzzing/carbon.proto b/common/fuzzing/carbon.proto
index e0a82ec0af01..dbc7565a9de6 100644
--- a/common/fuzzing/carbon.proto
+++ b/common/fuzzing/carbon.proto
@@ -353,6 +353,12 @@ message VariableDeclaration {
   optional Expression initializer = 2;
 }
 
+message LetDeclaration {
+  optional Pattern pattern = 1;
+  // TODO: Add `optional Expression initializer = 2;` once explorer supports
+  // `let` declarations in general.
+}
+
 message InterfaceDeclaration {
   optional string name = 1;
   repeated Declaration members = 2;
@@ -386,6 +392,7 @@ message Declaration {
     InterfaceDeclaration interface = 5;
     ImplDeclaration impl = 6;
     AliasDeclaration alias = 7;
+    LetDeclaration let = 8;
   }
 }
 
diff --git a/common/fuzzing/proto_to_carbon.cpp b/common/fuzzing/proto_to_carbon.cpp
index 1d5b840eba1c..f2c59b854cbf 100644
--- a/common/fuzzing/proto_to_carbon.cpp
+++ b/common/fuzzing/proto_to_carbon.cpp
@@ -721,6 +721,22 @@ static auto DeclarationToCarbon(const Fuzzing::Declaration& declaration,
       break;
     }
 
+    case Fuzzing::Declaration::kLet: {
+      const auto& let = declaration.let();
+      out << "let ";
+      PatternToCarbon(let.pattern(), out);
+
+      // TODO: Print out the initializer once it's supported.
+      /*
+      if (let.has_initializer()) {
+        out << " = ";
+        ExpressionToCarbon(let.initializer(), out);
+      }
+      */
+      out << ";";
+      break;
+    }
+
     case Fuzzing::Declaration::kInterface: {
       const auto& interface = declaration.interface();
       out << "interface ";
diff --git a/explorer/ast/ast_rtti.txt b/explorer/ast/ast_rtti.txt
index 81af103afde5..2289ce0ff986 100644
--- a/explorer/ast/ast_rtti.txt
+++ b/explorer/ast/ast_rtti.txt
@@ -19,6 +19,7 @@ abstract class Declaration : AstNode;
   class ChoiceDeclaration : Declaration;
   class VariableDeclaration : Declaration;
   class InterfaceDeclaration : Declaration;
+  class AssociatedConstantDeclaration : Declaration;
   class ImplDeclaration : Declaration;
   class AliasDeclaration : Declaration;
 class ImplBinding : AstNode;
diff --git a/explorer/ast/declaration.cpp b/explorer/ast/declaration.cpp
index a52dccaaa077..5f82e8a5aa1e 100644
--- a/explorer/ast/declaration.cpp
+++ b/explorer/ast/declaration.cpp
@@ -74,6 +74,11 @@ void Declaration::Print(llvm::raw_ostream& out) const {
       break;
     }
 
+    case DeclarationKind::AssociatedConstantDeclaration:
+      PrintID(out);
+      out << ";\n";
+      break;
+
     case DeclarationKind::SelfDeclaration: {
       out << "Self";
       break;
@@ -130,6 +135,12 @@ void Declaration::PrintID(llvm::raw_ostream& out) const {
       break;
     }
 
+    case DeclarationKind::AssociatedConstantDeclaration: {
+      const auto& let = cast<AssociatedConstantDeclaration>(*this);
+      out << "let " << let.binding();
+      break;
+    }
+
     case DeclarationKind::SelfDeclaration: {
       out << "Self";
       break;
@@ -156,6 +167,8 @@ auto GetName(const Declaration& declaration)
       return cast<InterfaceDeclaration>(declaration).name();
     case DeclarationKind::VariableDeclaration:
       return cast<VariableDeclaration>(declaration).binding().name();
+    case DeclarationKind::AssociatedConstantDeclaration:
+      return cast<AssociatedConstantDeclaration>(declaration).binding().name();
     case DeclarationKind::ImplDeclaration:
       return std::nullopt;
     case DeclarationKind::SelfDeclaration:
diff --git a/explorer/ast/declaration.h b/explorer/ast/declaration.h
index 3daebee2c505..ad5820b1aa7d 100644
--- a/explorer/ast/declaration.h
+++ b/explorer/ast/declaration.h
@@ -351,6 +351,26 @@ class InterfaceDeclaration : public Declaration {
   std::vector<Nonnull<Declaration*>> members_;
 };
 
+class AssociatedConstantDeclaration : public Declaration {
+ public:
+  AssociatedConstantDeclaration(SourceLocation source_loc,
+                                Nonnull<GenericBinding*> binding)
+      : Declaration(AstNodeKind::AssociatedConstantDeclaration, source_loc),
+        binding_(binding) {}
+
+  static auto classof(const AstNode* node) -> bool {
+    return InheritsFromAssociatedConstantDeclaration(node->kind());
+  }
+
+  auto binding() const -> const GenericBinding& { return *binding_; }
+  auto binding() -> GenericBinding& { return *binding_; }
+
+  auto value_category() const -> ValueCategory { return ValueCategory::Let; }
+
+ private:
+  Nonnull<GenericBinding*> binding_;
+};
+
 enum class ImplKind { InternalImpl, ExternalImpl };
 
 class ImplDeclaration : public Declaration {
diff --git a/explorer/fuzzing/ast_to_proto.cpp b/explorer/fuzzing/ast_to_proto.cpp
index ee301fc2fd02..9d18ad8ea6d8 100644
--- a/explorer/fuzzing/ast_to_proto.cpp
+++ b/explorer/fuzzing/ast_to_proto.cpp
@@ -609,6 +609,13 @@ static auto DeclarationToProto(const Declaration& declaration)
       break;
     }
 
+    case DeclarationKind::AssociatedConstantDeclaration: {
+      const auto& assoc = cast<AssociatedConstantDeclaration>(declaration);
+      auto* let_proto = declaration_proto.mutable_let();
+      *let_proto->mutable_pattern() = PatternToProto(assoc.binding());
+      break;
+    }
+
     case DeclarationKind::InterfaceDeclaration: {
       const auto& interface = cast<InterfaceDeclaration>(declaration);
       auto* interface_proto = declaration_proto.mutable_interface();
diff --git a/explorer/interpreter/field_path.h b/explorer/interpreter/field_path.h
index 1c30592cf358..07e973c6a18a 100644
--- a/explorer/interpreter/field_path.h
+++ b/explorer/interpreter/field_path.h
@@ -15,6 +15,7 @@
 
 namespace Carbon {
 
+class InterfaceType;
 class Witness;
 
 // Given some initial Value, a FieldPath identifies a sub-Value within it,
@@ -40,13 +41,19 @@ class FieldPath {
   class Component {
    public:
     explicit Component(Member member) : member_(member) {}
-    Component(Member member, std::optional<Nonnull<const Witness*>> witness)
-        : member_(member), witness_(witness) {}
+    Component(Member member,
+              std::optional<Nonnull<const InterfaceType*>> interface,
+              std::optional<Nonnull<const Witness*>> witness)
+        : member_(member), interface_(interface), witness_(witness) {}
 
     auto member() const -> Member { return member_; }
 
     auto name() const -> std::string_view { return member_.name(); }
 
+    auto interface() const -> std::optional<Nonnull<const InterfaceType*>> {
+      return interface_;
+    }
+
     auto witness() const -> std::optional<Nonnull<const Witness*>> {
       return witness_;
     }
@@ -55,6 +62,7 @@ class FieldPath {
 
    private:
     Member member_;
+    std::optional<Nonnull<const InterfaceType*>> interface_;
     std::optional<Nonnull<const Witness*>> witness_;
   };
 
diff --git a/explorer/interpreter/impl_scope.cpp b/explorer/interpreter/impl_scope.cpp
index 3bf73c5b6f1a..d2ec601e8280 100644
--- a/explorer/interpreter/impl_scope.cpp
+++ b/explorer/interpreter/impl_scope.cpp
@@ -26,15 +26,24 @@ void ImplScope::Add(Nonnull<const Value*> iface,
                     llvm::ArrayRef<Nonnull<const ImplBinding*>> impl_bindings,
                     Nonnull<Expression*> impl_expr,
                     const TypeChecker& type_checker) {
-  if (auto* constraint = dyn_cast<ConstraintType>(iface)) {
+  if (auto* orig_constraint = dyn_cast<ConstraintType>(iface)) {
     BindingMap map;
-    map[constraint->self_binding()] = type;
+    map[orig_constraint->self_binding()] = type;
+    const ConstraintType* constraint =
+        cast<ConstraintType>(type_checker.Substitute(map, orig_constraint));
     for (size_t i = 0; i != constraint->impl_constraints().size(); ++i) {
       ConstraintType::ImplConstraint impl = constraint->impl_constraints()[i];
-      Add(cast<InterfaceType>(type_checker.Substitute(map, impl.interface)),
-          deduced, type_checker.Substitute(map, impl.type), impl_bindings,
+      Add(impl.interface, deduced, impl.type, impl_bindings,
           type_checker.MakeConstraintWitnessAccess(impl_expr, i), type_checker);
     }
+    // A paremterized impl declaration doesn't contribute any equality
+    // constraints to the scope. Instead, we'll resolve the equality
+    // constraints by resolving a witness when needed.
+    if (deduced.empty()) {
+      for (auto& equality_constraint : constraint->equality_constraints()) {
+        equalities_.push_back(&equality_constraint);
+      }
+    }
     return;
   }
 
@@ -77,6 +86,22 @@ auto ImplScope::Resolve(Nonnull<const Value*> constraint_type,
   CARBON_FATAL() << "expected a constraint, not " << *constraint_type;
 }
 
+auto ImplScope::VisitEqualValues(
+    Nonnull<const Value*> value,
+    llvm::function_ref<bool(Nonnull<const Value*>)> visitor) const -> bool {
+  for (Nonnull<const ConstraintType::EqualityConstraint*> eq : equalities_) {
+    if (!eq->VisitEqualValues(value, visitor)) {
+      return false;
+    }
+  }
+  for (Nonnull<const ImplScope*> parent : parent_scopes_) {
+    if (!parent->VisitEqualValues(value, visitor)) {
+      return false;
+    }
+  }
+  return true;
+}
+
 auto ImplScope::ResolveInterface(Nonnull<const InterfaceType*> iface_type,
                                  Nonnull<const Value*> type,
                                  SourceLocation source_loc,
@@ -147,6 +172,13 @@ void ImplScope::Print(llvm::raw_ostream& out) const {
   for (const Impl& impl : impls_) {
     out << sep << *(impl.type) << " as " << *(impl.interface);
   }
+  for (Nonnull<const ConstraintType::EqualityConstraint*> eq : equalities_) {
+    out << sep;
+    llvm::ListSeparator equal(" == ");
+    for (Nonnull<const Value*> value : eq->values) {
+      out << equal << *value;
+    }
+  }
   out << "\n";
   for (const Nonnull<const ImplScope*>& parent : parent_scopes_) {
     out << *parent;
diff --git a/explorer/interpreter/impl_scope.h b/explorer/interpreter/impl_scope.h
index 60fbd0ffa96e..123b1eecdb87 100644
--- a/explorer/interpreter/impl_scope.h
+++ b/explorer/interpreter/impl_scope.h
@@ -6,12 +6,11 @@
 #define CARBON_EXPLORER_INTERPRETER_IMPL_SCOPE_H_
 
 #include "explorer/ast/declaration.h"
+#include "explorer/interpreter/value.h"
 
 namespace Carbon {
 
-class Value;
 class TypeChecker;
-class InterfaceType;
 
 // The `ImplScope` class is responsible for mapping a type and
 // interface to the location of the witness table for the `impl` for
@@ -38,6 +37,9 @@ class InterfaceType;
 //  impl is visible in the body of `bar`. In contrast, the call to
 //  `x.foo` in `baz` is not valid because there is no visible impl for
 //  `U` and `Fooable` in that scope.
+//
+// `ImplScope` also tracks the type equalities that are known in a particular
+// scope.
 class ImplScope {
  public:
   // Associates `iface` and `type` with the `impl` in this scope.
@@ -51,6 +53,11 @@ class ImplScope {
            llvm::ArrayRef<Nonnull<const ImplBinding*>> impl_bindings,
            Nonnull<Expression*> impl, const TypeChecker& type_checker);
 
+  // Add a type equality constraint.
+  void AddEqualityConstraint(Nonnull<const EqualityConstraint*> equal) {
+    equalities_.push_back(equal);
+  }
+
   // Make `parent` a parent of this scope.
   // REQUIRES: `parent` is not already a parent of this scope.
   void AddParent(Nonnull<const ImplScope*> parent);
@@ -62,6 +69,16 @@ class ImplScope {
                SourceLocation source_loc, const TypeChecker& type_checker) const
       -> ErrorOr<Nonnull<Expression*>>;
 
+  // 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.
+  //
+  // Stops and returns `false` if any call to the visitor returns `false`,
+  // otherwise returns `true`.
+  auto VisitEqualValues(
+      Nonnull<const Value*> value,
+      llvm::function_ref<bool(Nonnull<const Value*>)> visitor) const -> bool;
+
   void Print(llvm::raw_ostream& out) const;
 
   // The `Impl` struct is a key-value pair where the key is the
@@ -114,6 +131,7 @@ class ImplScope {
       -> ErrorOr<std::optional<Nonnull<Expression*>>>;
 
   std::vector<Impl> impls_;
+  std::vector<Nonnull<const EqualityConstraint*>> equalities_;
   std::vector<Nonnull<const ImplScope*>> parent_scopes_;
 };
 
diff --git a/explorer/interpreter/interpreter.cpp b/explorer/interpreter/interpreter.cpp
index 57abc415a915..d936d35b52da 100644
--- a/explorer/interpreter/interpreter.cpp
+++ b/explorer/interpreter/interpreter.cpp
@@ -99,6 +99,23 @@ class Interpreter {
   auto EvalExpRecursively(Nonnull<const Expression*> exp)
       -> ErrorOr<Nonnull<const Value*>>;
 
+  // Evaluate an associated constant by evaluating its witness and looking
+  // inside the impl for the corresponding value.
+  //
+  // TODO: This approach doesn't provide values that are known because they
+  // appear in constraints:
+  //
+  //   interface Iface { let N:! i32; }
+  //   fn PickType(N: i32) -> Type { return i32; }
+  //   fn F[T:! Iface where .N == 5](x: T) {
+  //     var x: PickType(T.N) = 0;
+  //   }
+  //
+  // ... will fail because we can't resolve T.N to 5 at compile time.
+  auto EvalAssociatedConstant(Nonnull<const AssociatedConstant*> assoc,
+                              SourceLocation source_loc)
+      -> ErrorOr<Nonnull<const Value*>>;
+
   // Instantiate a type by replacing all type variables that occur inside the
   // type by the current values of those variables.
   //
@@ -181,7 +198,7 @@ auto Interpreter::EvalPrim(Operator op, Nonnull<const Value*> static_type,
       return arena_->New<BoolValue>(cast<BoolValue>(*args[0]).value() ||
                                     cast<BoolValue>(*args[1]).value());
     case Operator::Eq:
-      return arena_->New<BoolValue>(ValueEqual(args[0], args[1]));
+      return arena_->New<BoolValue>(ValueEqual(args[0], args[1], std::nullopt));
     case Operator::Ptr:
       return arena_->New<PointerType>(args[0]);
     case Operator::Deref:
@@ -309,7 +326,7 @@ auto PatternMatch(Nonnull<const Value*> p, Nonnull<const Value*> v,
       // on the typechecker to ensure that `v` is a type.
       return true;
     default:
-      return ValueEqual(p, v);
+      return ValueEqual(p, v, std::nullopt);
   }
 }
 
@@ -454,6 +471,51 @@ auto Interpreter::EvalExpRecursively(Nonnull<const Expression*> exp)
   return result;
 }
 
+auto Interpreter::EvalAssociatedConstant(
+    Nonnull<const AssociatedConstant*> assoc, SourceLocation source_loc)
+    -> ErrorOr<Nonnull<const Value*>> {
+  // Find the witness.
+  Nonnull<const Value*> witness = &assoc->witness();
+  if (auto* sym = dyn_cast<SymbolicWitness>(witness)) {
+    CARBON_ASSIGN_OR_RETURN(witness,
+                            EvalExpRecursively(&sym->impl_expression()));
+  }
+  if (!isa<ImplWitness>(witness)) {
+    CARBON_CHECK(phase() == Phase::CompileTime)
+        << "symbolic witnesses should only be formed at compile time";
+    return CompilationError(source_loc)
+           << "value of associated constant " << *assoc << " is not known";
+  }
+
+  auto& impl_witness = cast<ImplWitness>(*witness);
+  Nonnull<const ConstraintType*> constraint =
+      impl_witness.declaration().constraint_type();
+  Nonnull<const Value*> expected = arena_->New<AssociatedConstant>(
+      &constraint->self_binding()->value(), &assoc->interface(),
+      &assoc->constant(), &impl_witness);
+  std::optional<Nonnull<const Value*>> result;
+  constraint->VisitEqualValues(expected,
+                               [&](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.
+                                 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;
+                               });
+  if (!result) {
+    CARBON_FATAL() << impl_witness.declaration()
+                   << " is missing value for associated constant " << *assoc;
+  }
+  return *result;
+}
+
 auto Interpreter::InstantiateType(Nonnull<const Value*> type,
                                   SourceLocation source_loc)
     -> ErrorOr<Nonnull<const Value*>> {
@@ -475,6 +537,12 @@ auto Interpreter::InstantiateType(Nonnull<const Value*> type,
           InstantiateBindings(&class_type.bindings(), source_loc));
       return arena_->New<NominalClassType>(&class_type.declaration(), bindings);
     }
+    case Value::Kind::AssociatedConstant: {
+      CARBON_ASSIGN_OR_RETURN(
+          Nonnull<const Value*> type_value,
+          EvalAssociatedConstant(cast<AssociatedConstant>(type), source_loc));
+      return InstantiateType(type_value, source_loc);
+    }
     default:
       return type;
   }
@@ -566,7 +634,7 @@ auto Interpreter::Convert(Nonnull<const Value*> value,
           return arena_->New<StructValue>(std::move(new_elements));
         }
         case Value::Kind::NominalClassType: {
-          // Instantiate the `destintation_type` to obtain the runtime
+          // Instantiate the `destination_type` to obtain the runtime
           // type of the object.
           CARBON_ASSIGN_OR_RETURN(
               Nonnull<const Value*> inst_dest,
@@ -621,6 +689,12 @@ auto Interpreter::Convert(Nonnull<const Value*> value,
       }
       return arena_->New<TupleValue>(std::move(new_elements));
     }
+    case Value::Kind::AssociatedConstant: {
+      CARBON_ASSIGN_OR_RETURN(
+          Nonnull<const Value*> value,
+          EvalAssociatedConstant(cast<AssociatedConstant>(value), source_loc));
+      return Convert(value, destination_type, source_loc);
+    }
   }
 }
 
@@ -854,6 +928,14 @@ auto Interpreter::StepExp() -> ErrorOr<Success> {
             std::make_unique<ExpressionAction>(access.impl().value()));
       } else {
         // Finally, produce the result.
+        std::optional<Nonnull<const InterfaceType*>> found_in_interface =
+            access.found_in_interface();
+        if (found_in_interface) {
+          CARBON_ASSIGN_OR_RETURN(
+              Nonnull<const Value*> instantiated,
+              InstantiateType(*found_in_interface, exp.source_loc()));
+          found_in_interface = cast<InterfaceType>(instantiated);
+        }
         if (const auto* member_name_type =
                 dyn_cast<TypeOfMemberName>(&access.static_type())) {
           // The result is a member name, such as in `Type.field_name`. Form a
@@ -864,9 +946,8 @@ auto Interpreter::StepExp() -> ErrorOr<Success> {
           if (!isa<InterfaceType, ConstraintType>(act.results()[0])) {
             type_result = act.results()[0];
           }
-          MemberName* member_name =
-              arena_->New<MemberName>(type_result, access.found_in_interface(),
-                                      member_name_type->member());
+          MemberName* member_name = arena_->New<MemberName>(
+              type_result, found_in_interface, member_name_type->member());
           return todo_.FinishAction(member_name);
         } else {
           // The result is the value of the named field, such as in
@@ -875,7 +956,8 @@ auto Interpreter::StepExp() -> ErrorOr<Success> {
           if (access.impl().has_value()) {
             witness = cast<Witness>(act.results()[1]);
           }
-          FieldPath::Component member(access.member(), witness);
+          FieldPath::Component member(access.member(), found_in_interface,
+                                      witness);
           const Value* aggregate;
           if (const auto* lvalue = dyn_cast<LValue>(act.results()[0])) {
             CARBON_ASSIGN_OR_RETURN(
@@ -907,6 +989,14 @@ auto Interpreter::StepExp() -> ErrorOr<Success> {
             std::make_unique<ExpressionAction>(access.impl().value()));
       } else {
         // Finally, produce the result.
+        std::optional<Nonnull<const InterfaceType*>> found_in_interface =
+            access.member().interface();
+        if (found_in_interface) {
+          CARBON_ASSIGN_OR_RETURN(
+              Nonnull<const Value*> instantiated,
+              InstantiateType(*found_in_interface, exp.source_loc()));
+          found_in_interface = cast<InterfaceType>(instantiated);
+        }
         if (forming_member_name) {
           // If we're forming a member name, we must be in the outer evaluation
           // in `Type.(Interface.method)`. Produce the same method name with
@@ -917,8 +1007,7 @@ auto Interpreter::StepExp() -> ErrorOr<Success> {
               << "compound member access forming a member name should be "
                  "performing impl lookup";
           auto* member_name = arena_->New<MemberName>(
-              act.results()[0], access.member().interface(),
-              access.member().member());
+              act.results()[0], found_in_interface, access.member().member());
           return todo_.FinishAction(member_name);
         } else {
           // Access the object to find the named member.
@@ -933,7 +1022,8 @@ auto Interpreter::StepExp() -> ErrorOr<Success> {
                 object, Convert(object, *access.member().base_type(),
                                 exp.source_loc()));
           }
-          FieldPath::Component field(access.member().member(), witness);
+          FieldPath::Component field(access.member().member(),
+                                     found_in_interface, witness);
           CARBON_ASSIGN_OR_RETURN(Nonnull<const Value*> member,
                                   object->GetMember(arena_, FieldPath(field),
                                                     exp.source_loc(), object));
@@ -1504,6 +1594,7 @@ auto Interpreter::StepDeclaration() -> ErrorOr<Success> {
     case DeclarationKind::ClassDeclaration:
     case DeclarationKind::ChoiceDeclaration:
     case DeclarationKind::InterfaceDeclaration:
+    case DeclarationKind::AssociatedConstantDeclaration:
     case DeclarationKind::ImplDeclaration:
     case DeclarationKind::SelfDeclaration:
     case DeclarationKind::AliasDeclaration:
diff --git a/explorer/interpreter/resolve_control_flow.cpp b/explorer/interpreter/resolve_control_flow.cpp
index 199b2703649f..f8db8469f581 100644
--- a/explorer/interpreter/resolve_control_flow.cpp
+++ b/explorer/interpreter/resolve_control_flow.cpp
@@ -165,6 +165,7 @@ auto ResolveControlFlow(Nonnull<Declaration*> declaration) -> ErrorOr<Success> {
     }
     case DeclarationKind::ChoiceDeclaration:
     case DeclarationKind::VariableDeclaration:
+    case DeclarationKind::AssociatedConstantDeclaration:
     case DeclarationKind::SelfDeclaration:
     case DeclarationKind::AliasDeclaration:
       // do nothing
diff --git a/explorer/interpreter/resolve_names.cpp b/explorer/interpreter/resolve_names.cpp
index a9e3e7fa3487..6ab750f12c40 100644
--- a/explorer/interpreter/resolve_names.cpp
+++ b/explorer/interpreter/resolve_names.cpp
@@ -62,6 +62,14 @@ static auto AddExposedNames(const Declaration& declaration,
       }
       break;
     }
+    case DeclarationKind::AssociatedConstantDeclaration: {
+      auto& let = cast<AssociatedConstantDeclaration>(declaration);
+      if (let.binding().name() != AnonymousName) {
+        CARBON_RETURN_IF_ERROR(
+            enclosing_scope.Add(let.binding().name(), &let.binding()));
+      }
+      break;
+    }
     case DeclarationKind::SelfDeclaration: {
       auto& self = cast<SelfDeclaration>(declaration);
       CARBON_RETURN_IF_ERROR(enclosing_scope.Add("Self", &self));
@@ -566,6 +574,11 @@ static auto ResolveNames(Declaration& declaration, StaticScope& enclosing_scope,
       }
       break;
     }
+    case DeclarationKind::AssociatedConstantDeclaration: {
+      auto& let = cast<AssociatedConstantDeclaration>(declaration);
+      CARBON_RETURN_IF_ERROR(ResolveNames(let.binding(), enclosing_scope));
+      break;
+    }
 
     case DeclarationKind::SelfDeclaration: {
       CARBON_FATAL() << "Unreachable: resolving names for `Self` declaration";
diff --git a/explorer/interpreter/type_checker.cpp b/explorer/interpreter/type_checker.cpp
index 7bcb71369cf5..53120be5354c 100644
--- a/explorer/interpreter/type_checker.cpp
+++ b/explorer/interpreter/type_checker.cpp
@@ -30,6 +30,93 @@ 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) {}
+
+  // Attempt to resolve the witness for the given associated constant in the
+  // in-scope `impl`s.
+  auto TryResolveWitness(Nonnull<const AssociatedConstant*> assoc,
+                         SourceLocation source_loc) const
+      -> ErrorOr<Nonnull<const ImplWitness*>> {
+    auto* impl_witness = dyn_cast<ImplWitness>(&assoc->witness());
+    if (impl_witness) {
+      return impl_witness;
+    }
+
+    CARBON_ASSIGN_OR_RETURN(
+        Nonnull<const Expression*> witness_expr,
+        impl_scope_->Resolve(&assoc->interface(), &assoc->base(), source_loc,
+                             *type_checker_));
+    CARBON_ASSIGN_OR_RETURN(Nonnull<const Value*> witness_value,
+                            InterpExp(witness_expr, type_checker_->arena_,
+                                      type_checker_->trace_stream_));
+    impl_witness = dyn_cast<ImplWitness>(witness_value);
+    if (impl_witness) {
+      return impl_witness;
+    }
+    return CompilationError(source_loc)
+           << "value of associated constant " << *assoc
+           << " depends on a generic parameter";
+  }
+
+  // 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.
+      SourceLocation source_loc("", 0);
+      ErrorOr<Nonnull<const ImplWitness*>> impl_witness =
+          TryResolveWitness(assoc, source_loc);
+      if (impl_witness.ok()) {
+        // Instantiate the impl to find the concrete constraint it implements.
+        Nonnull<const ConstraintType*> constraint =
+            (*impl_witness)->declaration().constraint_type();
+        BindingMap bindings = (*impl_witness)->type_args();
+        bindings[constraint->self_binding()] = &assoc->base();
+        constraint = cast<ConstraintType>(
+            type_checker_->Substitute(bindings, constraint));
+
+        // 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 << ": "
+              << impl_witness.error() << "\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
@@ -40,11 +127,14 @@ static void SetValue(Nonnull<Pattern*> pattern, Nonnull<const Value*> value) {
   }
 }
 
-static auto ExpectExactType(SourceLocation source_loc,
-                            const std::string& context,
-                            Nonnull<const Value*> expected,
-                            Nonnull<const Value*> actual) -> ErrorOr<Success> {
-  if (!TypeEqual(expected, actual)) {
+auto TypeChecker::ExpectExactType(SourceLocation source_loc,
+                                  const std::string& context,
+                                  Nonnull<const Value*> expected,
+                                  Nonnull<const Value*> actual,
+                                  const ImplScope& impl_scope) const
+    -> ErrorOr<Success> {
+  SingleStepEqualityContext equality_ctx(this, &impl_scope);
+  if (!TypeEqual(expected, actual, &equality_ctx)) {
     return CompilationError(source_loc) << "type error in " << context << "\n"
                                         << "expected: " << *expected << "\n"
                                         << "actual: " << *actual;
@@ -56,6 +146,7 @@ static auto ExpectPointerType(SourceLocation source_loc,
                               const std::string& context,
                               Nonnull<const Value*> actual)
     -> ErrorOr<Success> {
+  // TODO: Try to resolve in equality context.
   if (actual->kind() != Value::Kind::PointerType) {
     return CompilationError(source_loc) << "type error in " << context << "\n"
                                         << "expected a pointer type\n"
@@ -105,6 +196,7 @@ static auto IsTypeOfType(Nonnull<const Value*> value) -> bool {
       return false;
     case Value::Kind::AutoType:
     case Value::Kind::VariableType:
+    case Value::Kind::AssociatedConstant:
       // A value of one of these types could be a type, but isn't known to be.
       return false;
     case Value::Kind::TypeType:
@@ -180,6 +272,15 @@ static auto IsType(Nonnull<const Value*> value, bool concrete = false) -> bool {
     case Value::Kind::PointerType: {
       return IsType(&cast<PointerType>(*value).type(), concrete);
     }
+    case Value::Kind::AssociatedConstant: {
+      // An associated type is an associated constant whose type is a
+      // type-of-type.
+      const auto& assoc = cast<AssociatedConstant>(*value);
+      // TODO: Should we substitute in the arguments? Given
+      //   interface I(T:! Type) { let V:! T; }
+      // ... is T.(I(Type).V) considered to be a type?
+      return IsTypeOfType(&assoc.constant().static_type());
+    }
   }
 }
 
@@ -226,7 +327,8 @@ static auto FindField(llvm::ArrayRef<NamedValue> fields,
 
 auto TypeChecker::FieldTypesImplicitlyConvertible(
     llvm::ArrayRef<NamedValue> source_fields,
-    llvm::ArrayRef<NamedValue> destination_fields) const -> bool {
+    llvm::ArrayRef<NamedValue> destination_fields,
+    const ImplScope& impl_scope) const -> bool {
   if (source_fields.size() != destination_fields.size()) {
     return false;
   }
@@ -235,12 +337,12 @@ auto TypeChecker::FieldTypesImplicitlyConvertible(
         FindField(destination_fields, source_field.name);
     if (!destination_field.has_value() ||
         !IsImplicitlyConvertible(source_field.value,
-                                 destination_field.value().value,
+                                 destination_field.value().value, impl_scope,
                                  // TODO: We don't have a way to perform
                                  // user-defined conversions of a struct field
                                  // yet, because we can't write a suitable impl
                                  // for ImplicitAs.
-                                 std::nullopt)) {
+                                 /*allow_user_defined_conversions=*/false)) {
       return false;
     }
   }
@@ -269,29 +371,33 @@ auto TypeChecker::FieldTypes(const NominalClassType& class_type) const
 
 auto TypeChecker::IsImplicitlyConvertible(
     Nonnull<const Value*> source, Nonnull<const Value*> destination,
-    std::optional<Nonnull<const ImplScope*>> impl_scope) const -> bool {
+    const ImplScope& impl_scope, bool allow_user_defined_conversions) const
+    -> bool {
   // Check for an exact match or for an implicit conversion.
   // TODO: `impl`s of `ImplicitAs` should be provided to cover these
   // conversions.
   CARBON_CHECK(IsConcreteType(source));
   CARBON_CHECK(IsConcreteType(destination));
-  if (TypeEqual(source, destination)) {
+  SingleStepEqualityContext equality_ctx(this, &impl_scope);
+  if (TypeEqual(source, destination, &equality_ctx)) {
     return true;
   }
+
   switch (source->kind()) {
     case Value::Kind::StructType:
       switch (destination->kind()) {
         case Value::Kind::StructType:
           if (FieldTypesImplicitlyConvertible(
                   cast<StructType>(*source).fields(),
-                  cast<StructType>(*destination).fields())) {
+                  cast<StructType>(*destination).fields(), impl_scope)) {
             return true;
           }
           break;
         case Value::Kind::NominalClassType:
           if (FieldTypesImplicitlyConvertible(
                   cast<StructType>(*source).fields(),
-                  FieldTypes(cast<NominalClassType>(*destination)))) {
+                  FieldTypes(cast<NominalClassType>(*destination)),
+                  impl_scope)) {
             return true;
           }
           break;
@@ -310,9 +416,9 @@ auto TypeChecker::IsImplicitlyConvertible(
           }
           bool all_ok = true;
           for (size_t i = 0; i < source_tuple.elements().size(); ++i) {
-            if (!IsImplicitlyConvertible(source_tuple.elements()[i],
-                                         destination_tuple.elements()[i],
-                                         impl_scope)) {
+            if (!IsImplicitlyConvertible(
+                    source_tuple.elements()[i], destination_tuple.elements()[i],
+                    impl_scope, /*allow_user_defined_conversions=*/false)) {
               all_ok = false;
               break;
             }
@@ -329,9 +435,9 @@ auto TypeChecker::IsImplicitlyConvertible(
           }
           bool all_ok = true;
           for (Nonnull<const Value*> source_element : source_tuple.elements()) {
-            if (!IsImplicitlyConvertible(source_element,
-                                         &destination_array.element_type(),
-                                         impl_scope)) {
+            if (!IsImplicitlyConvertible(
+                    source_element, &destination_array.element_type(),
+                    impl_scope, /*allow_user_defined_conversions=*/false)) {
               all_ok = false;
               break;
             }
@@ -344,8 +450,9 @@ auto TypeChecker::IsImplicitlyConvertible(
         case Value::Kind::TypeType: {
           bool all_types = true;
           for (Nonnull<const Value*> source_element : source_tuple.elements()) {
-            if (!IsImplicitlyConvertible(source_element, destination,
-                                         impl_scope)) {
+            if (!IsImplicitlyConvertible(
+                    source_element, destination, impl_scope,
+                    /*allow_user_defined_conversions=*/false)) {
               all_types = false;
               break;
             }
@@ -382,8 +489,8 @@ auto TypeChecker::IsImplicitlyConvertible(
       break;
   }
 
-  // If we weren't given an impl scope, only look for builtin conversions.
-  if (!impl_scope.has_value()) {
+  // If we're not supposed to look for a user-defined conversion, we're done.
+  if (!allow_user_defined_conversions) {
     return false;
   }
 
@@ -393,7 +500,7 @@ auto TypeChecker::IsImplicitlyConvertible(
   ErrorOr<Nonnull<const InterfaceType*>> iface_type = GetBuiltinInterfaceType(
       source_loc, BuiltinInterfaceName{Builtins::ImplicitAs, destination});
   return iface_type.ok() &&
-         (*impl_scope)->Resolve(*iface_type, source, source_loc, *this).ok();
+         impl_scope.Resolve(*iface_type, source, source_loc, *this).ok();
 }
 
 auto TypeChecker::ImplicitlyConvert(const std::string& context,
@@ -401,13 +508,14 @@ auto TypeChecker::ImplicitlyConvert(const std::string& context,
                                     Nonnull<Expression*> source,
                                     Nonnull<const Value*> destination)
     -> ErrorOr<Nonnull<Expression*>> {
+  Nonnull<const Value*> source_type = &source->static_type();
   // TODO: If a builtin conversion works, for now we don't create any
   // expression to do the conversion and rely on the interpreter to know how to
   // do it.
   // TODO: This doesn't work for cases of combined built-in and user-defined
   // conversion, such as converting a struct element via an `ImplicitAs` impl.
-  if (IsImplicitlyConvertible(&source->static_type(), destination,
-                              std::nullopt)) {
+  if (IsImplicitlyConvertible(source_type, destination, impl_scope,
+                              /*allow_user_defined_conversions=*/false)) {
     return source;
   }
   ErrorOr<Nonnull<Expression*>> converted = BuildBuiltinMethodCall(
@@ -418,8 +526,8 @@ auto TypeChecker::ImplicitlyConvert(const std::string& context,
     // We couldn't find a matching `impl`.
     return CompilationError(source->source_loc())
            << "type error in " << context << ": "
-           << "'" << source->static_type()
-           << "' is not implicitly convertible to '" << *destination << "'";
+           << "'" << *source_type << "' is not implicitly convertible to '"
+           << *destination << "'";
   }
   return *converted;
 }
@@ -488,12 +596,14 @@ auto TypeChecker::BuildBuiltinMethodCall(const ImplScope& impl_scope,
   return {call};
 }
 
-auto TypeChecker::ExpectType(
-    SourceLocation source_loc, const std::string& context,
-    Nonnull<const Value*> expected, Nonnull<const Value*> actual,
-    std::optional<Nonnull<const ImplScope*>> impl_scope) const
+auto TypeChecker::ExpectType(SourceLocation source_loc,
+                             const std::string& context,
+                             Nonnull<const Value*> expected,
+                             Nonnull<const Value*> actual,
+                             const ImplScope& impl_scope) const
     -> ErrorOr<Success> {
-  if (!IsImplicitlyConvertible(actual, expected, impl_scope)) {
+  if (!IsImplicitlyConvertible(actual, expected, impl_scope,
+                               /*allow_user_defined_conversions=*/true)) {
     return CompilationError(source_loc)
            << "type error in " << context << ": "
            << "'" << *actual << "' is not implicitly convertible to '"
@@ -534,8 +644,9 @@ auto TypeChecker::ArgumentDeduction(
     const Value* subst_param_type = Substitute(deduced, param);
     return allow_implicit_conversion
                ? ExpectType(source_loc, context, subst_param_type, arg,
-                            &impl_scope)
-               : ExpectExactType(source_loc, context, subst_param_type, arg);
+                            impl_scope)
+               : ExpectExactType(source_loc, context, subst_param_type, arg,
+                                 impl_scope);
   };
 
   switch (param->kind()) {
@@ -545,9 +656,17 @@ auto TypeChecker::ArgumentDeduction(
                     &var_type.binding()) != bindings_to_deduce.end()) {
         auto [it, success] = deduced.insert({&var_type.binding(), arg});
         if (!success) {
-          // All deductions are required to produce the same value.
-          CARBON_RETURN_IF_ERROR(ExpectExactType(
-              source_loc, "repeated argument deduction", it->second, arg));
+          // All deductions are required to produce the same value. Note that
+          // we intentionally don't consider type equality here; we need the
+          // same symbolic type, otherwise it would be ambiguous which spelling
+          // should be used, and we'd need to check all pairs of types for
+          // equality because our notion of equality is non-transitive.
+          if (!TypeEqual(it->second, arg, std::nullopt)) {
+            return CompilationError(source_loc)
+                   << "deduced multiple different values for "
+                   << var_type.binding() << ":\n  " << *it->second << "\n  "
+                   << *arg;
+          }
         }
       } else {
         return handle_non_deduced_type();
@@ -704,6 +823,7 @@ auto TypeChecker::ArgumentDeduction(
     case Value::Kind::ContinuationType:
     case Value::Kind::ChoiceType:
     case Value::Kind::ConstraintType:
+    case Value::Kind::AssociatedConstant:
     case Value::Kind::IntType:
     case Value::Kind::BoolType:
     case Value::Kind::TypeType:
@@ -736,7 +856,8 @@ auto TypeChecker::ArgumentDeduction(
       // 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.
-      if (!ValueEqual(param, arg)) {
+      // TODO: Consider in-scope value equalities here.
+      if (!ValueEqual(param, arg, std::nullopt)) {
         return CompilationError(source_loc)
                << "mismatch in non-type values, `" << *arg << "` != `" << *param
                << "`";
@@ -756,73 +877,42 @@ auto TypeChecker::ArgumentDeduction(
 class ConstraintTypeBuilder {
  public:
   ConstraintTypeBuilder(Nonnull<Arena*> arena, SourceLocation source_loc)
-      : self_binding_(arena->New<GenericBinding>(
-            source_loc, ".Self", arena->New<TypeTypeLiteral>(source_loc))) {}
+      : self_binding_(MakeSelfBinding(arena, source_loc)) {}
   ConstraintTypeBuilder(Nonnull<const GenericBinding*> self_binding)
       : self_binding_(self_binding) {}
 
   // Produce a type that refers to the `.Self` type of the constraint.
-  auto MakeSelfType(Nonnull<Arena*> arena) const
-      -> Nonnull<const VariableType*> {
-    return arena->New<VariableType>(self_binding_);
+  auto GetSelfType(Nonnull<Arena*> arena) const -> Nonnull<const Value*> {
+    return &self_binding_->value();
   }
 
   // Add an `impl` constraint -- `T is C` if not already present.
   void AddImplConstraint(ConstraintType::ImplConstraint impl) {
     for (ConstraintType::ImplConstraint existing : impl_constraints_) {
-      if (TypeEqual(existing.type, impl.type) &&
-          TypeEqual(existing.interface, impl.interface)) {
+      if (TypeEqual(existing.type, impl.type, std::nullopt) &&
+          TypeEqual(existing.interface, impl.interface, std::nullopt)) {
         return;
       }
     }
     impl_constraints_.push_back(std::move(impl));
   }
 
-  // Add an `impl` constraint -- `A == B`, merging as necessary.
+  // Add an equality constraint -- `A == B`.
   void AddEqualityConstraint(ConstraintType::EqualityConstraint equal) {
-    // Check to see if any of the given values are already part of an equality
-    // constraint. If so, discard the value and note that we'll merge that
-    // constraint into the new one.
-    llvm::SmallDenseSet<size_t> merged_constraints;
-    {
-      size_t kept = 0;
-      for (size_t i = 0; i != equal.values.size(); ++i) {
-        if (std::optional<size_t> found_in =
-                FindInEqualityConstraints(equal.values[i])) {
-          merged_constraints.insert(*found_in);
-        } else {
-          equal.values[kept++] = equal.values[i];
-        }
-      }
-      equal.values.resize(kept);
-    }
+    CARBON_CHECK(equal.values.size() >= 2) << "degenerate equality constraint";
 
-    // Merge and discard any constraints that overlapped `equal`.
-    if (!merged_constraints.empty()) {
-      size_t kept = 0;
-      for (size_t i = 0; i != equality_constraints_.size(); ++i) {
-        if (merged_constraints.contains(i)) {
-          equal.values.insert(equal.values.end(),
-                              equality_constraints_[i].values.begin(),
-                              equality_constraints_[i].values.end());
-        } else {
-          if (kept != i) {
-            equality_constraints_[kept] = std::move(equality_constraints_[i]);
-          }
-          ++kept;
-        }
-      }
-      equality_constraints_[kept++] = std::move(equal);
-      equality_constraints_.resize(kept);
-    } else {
-      equality_constraints_.push_back(std::move(equal));
-    }
+    // TODO: Check to see if this constraint is already present and deduplicate
+    // if so. We could also look for a superset / subset and keep the larger
+    // one. We could in theory detect `A == B and B == C and C == A` and merge
+    // into a single `A == B == C` constraint, but that's more work than it's
+    // worth doing here.
+    equality_constraints_.push_back(std::move(equal));
   }
 
   // Add a context for qualified name lookup, if not already present.
   void AddLookupContext(ConstraintType::LookupContext context) {
     for (ConstraintType::LookupContext existing : lookup_contexts_) {
-      if (ValueEqual(existing.context, context.context)) {
+      if (ValueEqual(existing.context, context.context, std::nullopt)) {
         return;
       }
     }
@@ -855,17 +945,16 @@ class ConstraintTypeBuilder {
   }
 
  private:
-  // Find the given value in the equality constraints, returning the index of
-  // the constraint that contains it, if any.
-  auto FindInEqualityConstraints(const Value* value) -> std::optional<size_t> {
-    for (size_t i = 0; i != equality_constraints_.size(); ++i) {
-      for (const Value* v : equality_constraints_[i].values) {
-        if (ValueEqual(value, v)) {
-          return i;
-        }
-      }
-    }
-    return std::nullopt;
+  // Make a generic binding to serve as the `.Self` of this constraint type.
+  static auto MakeSelfBinding(Nonnull<Arena*> arena, SourceLocation source_loc)
+      -> Nonnull<const GenericBinding*> {
+    Nonnull<GenericBinding*> self_binding = arena->New<GenericBinding>(
+        source_loc, ".Self", arena->New<TypeTypeLiteral>(source_loc));
+    Nonnull<const Value*> self = arena->New<VariableType>(self_binding);
+    // TODO: Do we really need both of these?
+    self_binding->set_symbolic_identity(self);
+    self_binding->set_value(self);
+    return self_binding;
   }
 
  private:
@@ -896,6 +985,15 @@ auto TypeChecker::Substitute(
         return it->second;
       }
     }
+    case Value::Kind::AssociatedConstant: {
+      const auto& assoc = cast<AssociatedConstant>(*type);
+      Nonnull<const Value*> base = Substitute(dict, &assoc.base());
+      Nonnull<const Value*> interface = Substitute(dict, &assoc.interface());
+      Nonnull<const Value*> witness = Substitute(dict, &assoc.witness());
+      return arena_->New<AssociatedConstant>(
+          base, cast<InterfaceType>(interface), &assoc.constant(),
+          cast<Witness>(witness));
+    }
     case Value::Kind::TupleValue: {
       std::vector<Nonnull<const Value*>> elts;
       for (const auto& elt : cast<TupleValue>(*type).elements()) {
@@ -1001,7 +1099,7 @@ auto TypeChecker::Substitute(
         for (const Value* value : equality_constraint.values) {
           // Ensure we don't create any duplicates through substitution.
           if (std::find_if(values.begin(), values.end(), [&](const Value* v) {
-                return ValueEqual(v, value);
+                return ValueEqual(v, value, std::nullopt);
               }) == values.end()) {
             values.push_back(Substitute(dict, value));
           }
@@ -1173,7 +1271,7 @@ auto TypeChecker::MakeConstraintForInterface(
     -> Nonnull<const ConstraintType*> {
   ConstraintTypeBuilder builder(arena_, source_loc);
   builder.AddImplConstraint(
-      {.type = builder.MakeSelfType(arena_), .interface = iface_type});
+      {.type = builder.GetSelfType(arena_), .interface = iface_type});
   builder.AddLookupContext({.context = iface_type});
   return std::move(builder).Build(arena_);
 }
@@ -1183,7 +1281,7 @@ auto TypeChecker::CombineConstraints(
     llvm::ArrayRef<Nonnull<const ConstraintType*>> constraints)
     -> Nonnull<const ConstraintType*> {
   ConstraintTypeBuilder builder(arena_, source_loc);
-  auto* self = builder.MakeSelfType(arena_);
+  auto* self = builder.GetSelfType(arena_);
   for (Nonnull<const ConstraintType*> constraint : constraints) {
     BindingMap map;
     map[constraint->self_binding()] = self;
@@ -1274,14 +1372,14 @@ auto TypeChecker::DeduceCallBindings(
 struct ConstraintLookupResult {
   Nonnull<const InterfaceType*> interface;
   Nonnull<const Declaration*> member;
-  Nonnull<const Expression*> impl;
 };
 
 /// Look up a member name in a constraint, which might be a single interface or
 /// a compound constraint.
 static auto LookupInConstraint(SourceLocation source_loc,
+                               std::string_view lookup_kind,
                                Nonnull<const Value*> type,
-                               const std::string& member_name)
+                               std::string_view member_name)
     -> ErrorOr<ConstraintLookupResult> {
   // Find the set of lookup contexts.
   llvm::ArrayRef<ConstraintType::LookupContext> lookup_contexts;
@@ -1310,14 +1408,14 @@ static auto LookupInConstraint(SourceLocation source_loc,
             FindMember(member_name, iface_type.declaration().members());
         member.has_value()) {
       if (found.has_value()) {
-        if (ValueEqual(found->interface, &iface_type)) {
+        if (ValueEqual(found->interface, &iface_type, std::nullopt)) {
           continue;
         }
         // TODO: If we resolve to the same member either way, this
         // is not ambiguous.
         return CompilationError(source_loc)
-               << "ambiguous member access, " << member_name << " found in "
-               << *found->interface << " and " << iface_type;
+               << "ambiguous " << lookup_kind << ", " << member_name
+               << " found in " << *found->interface << " and " << iface_type;
       }
       found = {.interface = &iface_type, .member = member.value()};
     }
@@ -1326,10 +1424,10 @@ static auto LookupInConstraint(SourceLocation source_loc,
   if (!found) {
     if (isa<TypeType>(type)) {
       return CompilationError(source_loc)
-             << "member access into unconstrained type";
+             << lookup_kind << " in unconstrained type";
     }
     return CompilationError(source_loc)
-           << "member access, " << member_name << " not in " << *type;
+           << lookup_kind << ", " << member_name << " not in " << *type;
   }
   return found.value();
 }
@@ -1361,9 +1459,10 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
       switch (object_type.kind()) {
         case Value::Kind::TupleValue: {
           const auto& tuple_type = cast<TupleValue>(object_type);
-          CARBON_RETURN_IF_ERROR(ExpectExactType(
-              index.offset().source_loc(), "tuple index",
-              arena_->New<IntType>(), &index.offset().static_type()));
+          CARBON_RETURN_IF_ERROR(
+              ExpectExactType(index.offset().source_loc(), "tuple index",
+                              arena_->New<IntType>(),
+                              &index.offset().static_type(), impl_scope));
           CARBON_ASSIGN_OR_RETURN(
               auto offset_value,
               InterpExp(&index.offset(), arena_, trace_stream_));
@@ -1378,9 +1477,10 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
           return Success();
         }
         case Value::Kind::StaticArrayType: {
-          CARBON_RETURN_IF_ERROR(ExpectExactType(
-              index.offset().source_loc(), "array index",
-              arena_->New<IntType>(), &index.offset().static_type()));
+          CARBON_RETURN_IF_ERROR(
+              ExpectExactType(index.offset().source_loc(), "array index",
+                              arena_->New<IntType>(),
+                              &index.offset().static_type(), impl_scope));
           index.set_static_type(
               &cast<StaticArrayType>(object_type).element_type());
           index.set_value_category(index.object().value_category());
@@ -1473,7 +1573,7 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
                                  &func_decl->me_pattern().static_type());
                   CARBON_RETURN_IF_ERROR(ExpectType(
                       e->source_loc(), "method access, receiver type", me_type,
-                      &access.object().static_type(), &impl_scope));
+                      &access.object().static_type(), impl_scope));
                   if (access.object().value_category() != ValueCategory::Var) {
                     return CompilationError(e->source_loc())
                            << "method " << access.member_name()
@@ -1504,7 +1604,7 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
               cast<VariableType>(object_type).binding().static_type();
           CARBON_ASSIGN_OR_RETURN(
               ConstraintLookupResult result,
-              LookupInConstraint(e->source_loc(), &typeof_var,
+              LookupInConstraint(e->source_loc(), "member access", &typeof_var,
                                  access.member_name()));
 
           const Value& member_type = result.member->static_type();
@@ -1538,7 +1638,7 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
               InterpExp(&access.object(), arena_, trace_stream_));
           CARBON_ASSIGN_OR_RETURN(
               ConstraintLookupResult result,
-              LookupInConstraint(e->source_loc(), &object_type,
+              LookupInConstraint(e->source_loc(), "member access", &object_type,
                                  access.member_name()));
           CARBON_ASSIGN_OR_RETURN(Nonnull<Expression*> impl,
                                   impl_scope.Resolve(result.interface, type,
@@ -1547,30 +1647,41 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
           access.set_impl(impl);
           access.set_found_in_interface(result.interface);
 
+          bool is_instance_member;
           switch (result.member->kind()) {
-            case DeclarationKind::FunctionDeclaration: {
-              const auto& func = cast<FunctionDeclaration>(*result.member);
-              if (func.is_method()) {
-                break;
-              }
-              const Value& member_type = func.static_type();
-              BindingMap binding_map = result.interface->args();
-              binding_map[result.interface->declaration().self()] = type;
-              Nonnull<const Value*> inst_member_type =
-                  Substitute(binding_map, &member_type);
-              access.set_static_type(inst_member_type);
-              return Success();
-            }
+            case DeclarationKind::FunctionDeclaration:
+              is_instance_member =
+                  cast<FunctionDeclaration>(*result.member).is_method();
+              break;
+            case DeclarationKind::AssociatedConstantDeclaration:
+              is_instance_member = false;
+              break;
             default:
+              CARBON_FATAL()
+                  << "unexpected kind for interface member " << *result.member;
               break;
           }
-          // TODO: Consider setting the static type of all interface member
-          // declarations and instance member declarations to be member name
-          // types, rather than special-casing member accesses that name
-          // them.
-          access.set_static_type(
-              arena_->New<TypeOfMemberName>(Member(result.member)));
-          access.set_value_category(ValueCategory::Let);
+
+          if (is_instance_member) {
+            // This is a member name denoting an instance member.
+            // TODO: Consider setting the static type of all instance member
+            // declarations to be member name types, rather than special-casing
+            // member accesses that name them.
+            access.set_static_type(
+                arena_->New<TypeOfMemberName>(Member(result.member)));
+            access.set_value_category(ValueCategory::Let);
+          } else {
+            // This is a non-instance member whose value is found directly via
+            // the witness table, such as a non-method function or an
+            // associated constant.
+            const Value& member_type = result.member->static_type();
+            BindingMap binding_map = result.interface->args();
+            binding_map[result.interface->declaration().self()] = type;
+            Nonnull<const Value*> inst_member_type =
+                Substitute(binding_map, &member_type);
+            access.set_static_type(inst_member_type);
+            access.set_value_category(ValueCategory::Let);
+          }
           return Success();
         }
         case Value::Kind::TypeType:
@@ -1654,9 +1765,10 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
             }
             case Value::Kind::InterfaceType:
             case Value::Kind::ConstraintType: {
-              CARBON_ASSIGN_OR_RETURN(ConstraintLookupResult result,
-                                      LookupInConstraint(e->source_loc(), type,
-                                                         access.member_name()));
+              CARBON_ASSIGN_OR_RETURN(
+                  ConstraintLookupResult result,
+                  LookupInConstraint(e->source_loc(), "member access", type,
+                                     access.member_name()));
               access.set_member(Member(result.member));
               access.set_found_in_interface(result.interface);
               access.set_static_type(
@@ -1765,6 +1877,10 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
           }
           break;
         }
+        case DeclarationKind::AssociatedConstantDeclaration:
+          access.set_static_type(SubstituteIntoMemberType());
+          access.set_value_category(access.object().value_category());
+          return Success();
         default:
           CARBON_FATAL() << "member " << member_name
                          << " is not a field or method";
@@ -1820,64 +1936,72 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
       }
       switch (op.op()) {
         case Operator::Neg:
-          CARBON_RETURN_IF_ERROR(ExpectExactType(
-              e->source_loc(), "negation", arena_->New<IntType>(), ts[0]));
+          CARBON_RETURN_IF_ERROR(ExpectExactType(e->source_loc(), "negation",
+                                                 arena_->New<IntType>(), ts[0],
+                                                 impl_scope));
           op.set_static_type(arena_->New<IntType>());
           op.set_value_category(ValueCategory::Let);
           return Success();
         case Operator::Add:
-          CARBON_RETURN_IF_ERROR(ExpectExactType(
-              e->source_loc(), "addition(1)", arena_->New<IntType>(), ts[0]));
-          CARBON_RETURN_IF_ERROR(ExpectExactType(
-              e->source_loc(), "addition(2)", arena_->New<IntType>(), ts[1]));
+          CARBON_RETURN_IF_ERROR(ExpectExactType(e->source_loc(), "addition(1)",
+                                                 arena_->New<IntType>(), ts[0],
+                                                 impl_scope));
+          CARBON_RETURN_IF_ERROR(ExpectExactType(e->source_loc(), "addition(2)",
+                                                 arena_->New<IntType>(), ts[1],
+                                                 impl_scope));
           op.set_static_type(arena_->New<IntType>());
           op.set_value_category(ValueCategory::Let);
           return Success();
         case Operator::Sub:
           CARBON_RETURN_IF_ERROR(
               ExpectExactType(e->source_loc(), "subtraction(1)",
-                              arena_->New<IntType>(), ts[0]));
+                              arena_->New<IntType>(), ts[0], impl_scope));
           CARBON_RETURN_IF_ERROR(
               ExpectExactType(e->source_loc(), "subtraction(2)",
-                              arena_->New<IntType>(), ts[1]));
+                              arena_->New<IntType>(), ts[1], impl_scope));
           op.set_static_type(arena_->New<IntType>());
           op.set_value_category(ValueCategory::Let);
           return Success();
         case Operator::Mul:
           CARBON_RETURN_IF_ERROR(
               ExpectExactType(e->source_loc(), "multiplication(1)",
-                              arena_->New<IntType>(), ts[0]));
+                              arena_->New<IntType>(), ts[0], impl_scope));
           CARBON_RETURN_IF_ERROR(
               ExpectExactType(e->source_loc(), "multiplication(2)",
-                              arena_->New<IntType>(), ts[1]));
+                              arena_->New<IntType>(), ts[1], impl_scope));
           op.set_static_type(arena_->New<IntType>());
           op.set_value_category(ValueCategory::Let);
           return Success();
         case Operator::And:
-          CARBON_RETURN_IF_ERROR(ExpectExactType(
-              e->source_loc(), "&&(1)", arena_->New<BoolType>(), ts[0]));
-          CARBON_RETURN_IF_ERROR(ExpectExactType(
-              e->source_loc(), "&&(2)", arena_->New<BoolType>(), ts[1]));
+          CARBON_RETURN_IF_ERROR(ExpectExactType(e->source_loc(), "&&(1)",
+                                                 arena_->New<BoolType>(), ts[0],
+                                                 impl_scope));
+          CARBON_RETURN_IF_ERROR(ExpectExactType(e->source_loc(), "&&(2)",
+                                                 arena_->New<BoolType>(), ts[1],
+                                                 impl_scope));
           op.set_static_type(arena_->New<BoolType>());
           op.set_value_category(ValueCategory::Let);
           return Success();
         case Operator::Or:
-          CARBON_RETURN_IF_ERROR(ExpectExactType(
-              e->source_loc(), "||(1)", arena_->New<BoolType>(), ts[0]));
-          CARBON_RETURN_IF_ERROR(ExpectExactType(
-              e->source_loc(), "||(2)", arena_->New<BoolType>(), ts[1]));
+          CARBON_RETURN_IF_ERROR(ExpectExactType(e->source_loc(), "||(1)",
+                                                 arena_->New<BoolType>(), ts[0],
+                                                 impl_scope));
+          CARBON_RETURN_IF_ERROR(ExpectExactType(e->source_loc(), "||(2)",
+                                                 arena_->New<BoolType>(), ts[1],
+                                                 impl_scope));
           op.set_static_type(arena_->New<BoolType>());
           op.set_value_category(ValueCategory::Let);
           return Success();
         case Operator::Not:
-          CARBON_RETURN_IF_ERROR(ExpectExactType(
-              e->source_loc(), "!", arena_->New<BoolType>(), ts[0]));
+          CARBON_RETURN_IF_ERROR(ExpectExactType(e->source_loc(), "!",
+                                                 arena_->New<BoolType>(), ts[0],
+                                                 impl_scope));
           op.set_static_type(arena_->New<BoolType>());
           op.set_value_category(ValueCategory::Let);
           return Success();
         case Operator::Eq:
           CARBON_RETURN_IF_ERROR(
-              ExpectExactType(e->source_loc(), "==", ts[0], ts[1]));
+              ExpectExactType(e->source_loc(), "==", ts[0], ts[1], impl_scope));
           op.set_static_type(arena_->New<BoolType>());
           op.set_value_category(ValueCategory::Let);
           return Success();
@@ -1890,7 +2014,7 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
         case Operator::Ptr:
           CARBON_RETURN_IF_ERROR(ExpectType(e->source_loc(), "*",
                                             arena_->New<TypeType>(), ts[0],
-                                            &impl_scope));
+                                            impl_scope));
           op.set_static_type(arena_->New<TypeType>());
           op.set_value_category(ValueCategory::Let);
           return Success();
@@ -2041,7 +2165,7 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
           CARBON_RETURN_IF_ERROR(ExpectExactType(
               e->source_loc(), "__intrinsic_print argument",
               arena_->New<StringType>(),
-              &intrinsic_exp.args().fields()[0]->static_type()));
+              &intrinsic_exp.args().fields()[0]->static_type(), impl_scope));
           e->set_static_type(TupleValue::Empty());
           e->set_value_category(ValueCategory::Let);
           return Success();
@@ -2091,10 +2215,10 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
           TypeCheckExp(&if_expr.then_expression(), impl_scope));
       CARBON_RETURN_IF_ERROR(
           TypeCheckExp(&if_expr.else_expression(), impl_scope));
-      CARBON_RETURN_IF_ERROR(
-          ExpectExactType(e->source_loc(), "expression of `if` expression",
-                          &if_expr.then_expression().static_type(),
-                          &if_expr.else_expression().static_type()));
+      CARBON_RETURN_IF_ERROR(ExpectExactType(
+          e->source_loc(), "expression of `if` expression",
+          &if_expr.then_expression().static_type(),
+          &if_expr.else_expression().static_type(), impl_scope));
       e->set_static_type(&if_expr.then_expression().static_type());
       e->set_value_category(ValueCategory::Let);
       return Success();
@@ -2128,7 +2252,7 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
       ConstraintTypeBuilder builder(&where.self_binding());
       if (base) {
         BindingMap map;
-        map[(*base)->self_binding()] = builder.MakeSelfType(arena_);
+        map[(*base)->self_binding()] = builder.GetSelfType(arena_);
         builder.Add(cast<ConstraintType>(Substitute(map, *base)));
       }
 
@@ -2171,7 +2295,7 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
             CARBON_ASSIGN_OR_RETURN(
                 Nonnull<const Value*> rhs,
                 InterpExp(&equals_clause.rhs(), arena_, trace_stream_));
-            if (!ValueEqual(lhs, rhs)) {
+            if (!ValueEqual(lhs, rhs, std::nullopt)) {
               builder.AddEqualityConstraint({.values = {lhs, rhs}});
             }
             break;
@@ -2193,10 +2317,10 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
 
       CARBON_RETURN_IF_ERROR(
           TypeCheckExp(&array_literal.size_expression(), impl_scope));
-      CARBON_RETURN_IF_ERROR(
-          ExpectExactType(array_literal.size_expression().source_loc(),
-                          "array size", arena_->New<IntType>(),
-                          &array_literal.size_expression().static_type()));
+      CARBON_RETURN_IF_ERROR(ExpectExactType(
+          array_literal.size_expression().source_loc(), "array size",
+          arena_->New<IntType>(),
+          &array_literal.size_expression().static_type(), impl_scope));
       CARBON_ASSIGN_OR_RETURN(
           Nonnull<const Value*> size_value,
           InterpExp(&array_literal.size_expression(), arena_, trace_stream_));
@@ -2298,10 +2422,21 @@ auto TypeChecker::TypeCheckWhereClause(Nonnull<WhereClause*> clause,
       auto& equals_clause = cast<EqualsWhereClause>(*clause);
       CARBON_RETURN_IF_ERROR(TypeCheckExp(&equals_clause.lhs(), impl_scope));
       CARBON_RETURN_IF_ERROR(TypeCheckExp(&equals_clause.rhs(), impl_scope));
-      CARBON_RETURN_IF_ERROR(ExpectExactType(
-          clause->source_loc(), "values in `where ==` constraint",
-          &equals_clause.lhs().static_type(),
-          &equals_clause.rhs().static_type()));
+
+      // TODO: It's not clear what level of type compatibility is required
+      // between the operands. For now we require a builtin no-op implicit
+      // conversion.
+      Nonnull<const Value*> lhs_type = &equals_clause.lhs().static_type();
+      Nonnull<const Value*> rhs_type = &equals_clause.rhs().static_type();
+      if (!IsImplicitlyConvertible(lhs_type, rhs_type, impl_scope,
+                                   /*allow_user_defined_conversions=*/false) &&
+          !IsImplicitlyConvertible(rhs_type, lhs_type, impl_scope,
+                                   /*allow_user_defined_conversions=*/false)) {
+        return CompilationError(clause->source_loc())
+               << "type mismatch between values in `where LHS == RHS`\n"
+               << "  LHS type: " << *lhs_type << "\n"
+               << "  RHS type: " << *rhs_type;
+      }
       return Success();
     }
   }
@@ -2342,7 +2477,7 @@ auto TypeChecker::TypeCheckPattern(
       if (expected) {
         if (IsConcreteType(type)) {
           CARBON_RETURN_IF_ERROR(ExpectType(p->source_loc(), "name binding",
-                                            type, *expected, &impl_scope));
+                                            type, *expected, impl_scope));
         } else {
           BindingMap generic_args;
           if (!PatternMatch(type, *expected, binding.type().source_loc(),
@@ -2442,7 +2577,7 @@ auto TypeChecker::TypeCheckPattern(
       if (expected) {
         CARBON_RETURN_IF_ERROR(ExpectType(alternative.source_loc(),
                                           "alternative pattern", &choice_type,
-                                          *expected, &impl_scope));
+                                          *expected, impl_scope));
       }
       std::optional<Nonnull<const Value*>> parameter_types =
           choice_type.FindAlternative(alternative.alternative_name());
@@ -2534,9 +2669,10 @@ auto TypeChecker::TypeCheckStmt(Nonnull<Statement*> s,
           // that's not the same type as the scrutinee, we will convert the
           // scrutinee. We might want to instead allow a different conversion
           // to be performed for each pattern.
-          CARBON_RETURN_IF_ERROR(ExpectExactType(
-              clause.pattern().source_loc(), "`match` pattern type",
-              expected_type.value(), &clause.pattern().static_type()));
+          CARBON_RETURN_IF_ERROR(
+              ExpectExactType(clause.pattern().source_loc(),
+                              "`match` pattern type", expected_type.value(),
+                              &clause.pattern().static_type(), impl_scope));
         } else {
           expected_type = &clause.pattern().static_type();
         }
@@ -2636,10 +2772,12 @@ auto TypeChecker::TypeCheckStmt(Nonnull<Statement*> s,
       if (return_term.is_auto()) {
         return_term.set_static_type(&ret.value_node().static_type());
       } else {
+        // TODO: Consider using `ExpectExactType` here.
         CARBON_CHECK(IsConcreteType(&return_term.static_type()));
         CARBON_CHECK(IsConcreteType(&ret.value_node().static_type()));
+        SingleStepEqualityContext equality_ctx(this, &impl_scope);
         if (!TypeEqual(&return_term.static_type(),
-                       &ret.value_node().static_type())) {
+                       &ret.value_node().static_type(), &equality_ctx)) {
           return CompilationError(ret.value_node().base().source_loc())
                  << "type of returned var `" << ret.value_node().static_type()
                  << "` does not match return type `"
@@ -2846,9 +2984,10 @@ auto TypeChecker::DeclareFunctionDeclaration(Nonnull<FunctionDeclaration*> f,
       return CompilationError(f->return_term().source_loc())
              << "`Main` must have an explicit return type";
     }
-    CARBON_RETURN_IF_ERROR(ExpectExactType(
-        f->return_term().source_loc(), "return type of `Main`",
-        arena_->New<IntType>(), &f->return_term().static_type()));
+    CARBON_RETURN_IF_ERROR(
+        ExpectExactType(f->return_term().source_loc(), "return type of `Main`",
+                        arena_->New<IntType>(), &f->return_term().static_type(),
+                        function_scope));
     // TODO: Check that main doesn't have any parameters.
   }
 
@@ -2986,6 +3125,7 @@ auto TypeChecker::DeclareInterfaceDeclaration(
   ImplScope iface_scope;
   iface_scope.AddParent(scope_info.innermost_scope);
 
+  Nonnull<InterfaceType*> iface_type;
   if (iface_decl->params().has_value()) {
     CARBON_RETURN_IF_ERROR(TypeCheckPattern(*iface_decl->params(), std::nullopt,
                                             iface_scope, ValueCategory::Let));
@@ -2998,8 +3138,21 @@ auto TypeChecker::DeclareInterfaceDeclaration(
     SetConstantValue(iface_decl, param_name);
     iface_decl->set_static_type(
         arena_->New<TypeOfParameterizedEntityName>(param_name));
+
+    // Form the full symbolic type of the interface. This is used as part of
+    // the value of associated constants, if they're referenced within the
+    // interface itself.
+    std::vector<Nonnull<const GenericBinding*>> bindings = scope_info.bindings;
+    CollectGenericBindingsInPattern(*iface_decl->params(), bindings);
+    BindingMap generic_args;
+    for (auto* binding : bindings) {
+      generic_args[binding] = *binding->symbolic_identity();
+    }
+    iface_type = arena_->New<InterfaceType>(
+        iface_decl,
+        arena_->New<Bindings>(std::move(generic_args), Bindings::NoWitnesses));
   } else {
-    Nonnull<InterfaceType*> iface_type = arena_->New<InterfaceType>(iface_decl);
+    iface_type = arena_->New<InterfaceType>(iface_decl);
     SetConstantValue(iface_decl, iface_type);
     iface_decl->set_static_type(arena_->New<TypeOfInterfaceType>(iface_type));
   }
@@ -3011,6 +3164,15 @@ auto TypeChecker::DeclareInterfaceDeclaration(
   ScopeInfo iface_scope_info = ScopeInfo::ForNonClassScope(&iface_scope);
   for (Nonnull<Declaration*> m : iface_decl->members()) {
     CARBON_RETURN_IF_ERROR(DeclareDeclaration(m, iface_scope_info));
+
+    if (auto* assoc = dyn_cast<AssociatedConstantDeclaration>(m)) {
+      // TODO: The witness should be optional in AssociatedConstant.
+      Nonnull<const Expression*> witness_expr =
+          arena_->New<DotSelfExpression>(iface_decl->source_loc());
+      assoc->binding().set_symbolic_identity(arena_->New<AssociatedConstant>(
+          &iface_decl->self()->value(), iface_type, assoc,
+          arena_->New<SymbolicWitness>(witness_expr)));
+    }
   }
   if (trace_stream_) {
     **trace_stream_ << "** finished declaring interface " << iface_decl->name()
@@ -3069,29 +3231,75 @@ auto TypeChecker::CheckImplIsDeducible(
 
 auto TypeChecker::CheckImplIsComplete(Nonnull<const InterfaceType*> iface_type,
                                       Nonnull<const ImplDeclaration*> impl_decl,
-                                      Nonnull<const Value*> self_type)
+                                      Nonnull<const Value*> self_type,
+                                      const ImplScope& impl_scope)
     -> ErrorOr<Success> {
   const auto& iface_decl = iface_type->declaration();
   for (Nonnull<Declaration*> m : iface_decl.members()) {
-    std::optional<std::string_view> mem_name = GetName(*m);
-    CARBON_CHECK(mem_name.has_value()) << "unnamed interface member " << *m;
+    if (auto* assoc = dyn_cast<AssociatedConstantDeclaration>(m)) {
+      // An associated constant must be given exactly one value.
+      Nonnull<const GenericBinding*> symbolic_self =
+          impl_decl->constraint_type()->self_binding();
+      Nonnull<const Value*> expected = arena_->New<AssociatedConstant>(
+          &symbolic_self->value(), iface_type, assoc,
+          arena_->New<ImplWitness>(impl_decl));
 
-    std::optional<Nonnull<const Declaration*>> mem =
-        FindMember(*mem_name, impl_decl->members());
-    if (!mem.has_value()) {
-      return CompilationError(impl_decl->source_loc())
-             << "implementation missing " << *mem_name;
+      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 CompilationError(impl_decl->source_loc())
+               << "implementation missing " << *expected;
+      } 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 {}
+        return CompilationError(impl_decl->source_loc())
+               << "implementation doesn't provide a concrete value for "
+               << *expected;
+      } else if (second_value) {
+        return CompilationError(impl_decl->source_loc())
+               << "implementation provides multiple values for " << *expected
+               << ": " << **found_value << " and " << **second_value;
+      }
+    } else {
+      // Every member function must be declared.
+      std::optional<std::string_view> mem_name = GetName(*m);
+      CARBON_CHECK(mem_name.has_value()) << "unnamed interface member " << *m;
+
+      std::optional<Nonnull<const Declaration*>> mem =
+          FindMember(*mem_name, impl_decl->members());
+      if (!mem.has_value()) {
+        return CompilationError(impl_decl->source_loc())
+               << "implementation missing " << *mem_name;
+      }
+
+      BindingMap binding_map = iface_type->args();
+      binding_map[iface_decl.self()] = self_type;
+      Nonnull<const Value*> iface_mem_type =
+          Substitute(binding_map, &m->static_type());
+      // TODO: How should the signature in the implementation be permitted
+      // to differ from the signature in the interface?
+      CARBON_RETURN_IF_ERROR(
+          ExpectExactType((*mem)->source_loc(), "member of implementation",
+                          iface_mem_type, &(*mem)->static_type(), impl_scope));
     }
-
-    BindingMap binding_map = iface_type->args();
-    binding_map[iface_decl.self()] = self_type;
-    Nonnull<const Value*> iface_mem_type =
-        Substitute(binding_map, &m->static_type());
-    // TODO: How should the signature in the implementation be permitted
-    // to differ from the signature in the interface?
-    CARBON_RETURN_IF_ERROR(
-        ExpectExactType((*mem)->source_loc(), "member of implementation",
-                        iface_mem_type, &(*mem)->static_type()));
   }
   return Success();
 }
@@ -3114,18 +3322,32 @@ auto TypeChecker::CheckAndAddImplBindings(
       impl_decl->source_loc(), arena_->New<ImplWitness>(impl_decl),
       arena_->New<TypeType>(), ValueCategory::Let);
 
+  // Form the resolved constraint type by substituting `Self` for `.Self`.
+  Nonnull<const Value*> self = *impl_decl->self()->constant_value();
+  BindingMap constraint_self_map;
+  constraint_self_map[impl_decl->constraint_type()->self_binding()] = self;
+  Nonnull<const ConstraintType*> constraint = cast<ConstraintType>(
+      Substitute(constraint_self_map, impl_decl->constraint_type()));
+
   // Each interface that is a lookup context is required to be implemented by
   // the impl members. Other constraints are required to be satisfied by
   // either those impls or impls available elsewhere.
-  const ConstraintType* constraint = impl_decl->constraint_type();
   for (auto lookup : constraint->lookup_contexts()) {
     if (auto* iface_type = dyn_cast<InterfaceType>(lookup.context)) {
       CARBON_RETURN_IF_ERROR(
           CheckImplIsDeducible(impl_decl->source_loc(), impl_type, iface_type,
                                deduced_bindings, *scope_info.innermost_scope));
 
+      // Bring the associated constant values for this interface into scope. We
+      // know that if the methods of this interface are used, they will use
+      // these values.
+      ImplScope iface_scope;
+      iface_scope.AddParent(scope_info.innermost_scope);
+      BringAssociatedConstantsIntoScope(cast<ConstraintType>(constraint), self,
+                                        iface_type, iface_scope);
+
       CARBON_RETURN_IF_ERROR(
-          CheckImplIsComplete(iface_type, impl_decl, impl_type));
+          CheckImplIsComplete(iface_type, impl_decl, impl_type, iface_scope));
 
       scope_info.innermost_non_class_scope->Add(
           iface_type, deduced_bindings, impl_type, impl_decl->impl_bindings(),
@@ -3209,18 +3431,64 @@ auto TypeChecker::DeclareImplDeclaration(Nonnull<ImplDeclaration*> impl_decl,
   return Success();
 }
 
+void TypeChecker::BringAssociatedConstantsIntoScope(
+    Nonnull<const ConstraintType*> constraint, Nonnull<const Value*> self,
+    Nonnull<const InterfaceType*> interface, ImplScope& scope) {
+  std::set<Nonnull<const AssociatedConstantDeclaration*>> assocs_in_interface;
+  for (Nonnull<Declaration*> m : interface->declaration().members()) {
+    if (auto* assoc = dyn_cast<AssociatedConstantDeclaration>(m)) {
+      assocs_in_interface.insert(assoc);
+    }
+  }
+
+  for (const auto& eq : constraint->equality_constraints()) {
+    for (Nonnull<const Value*> value : eq.values) {
+      if (auto* assoc = dyn_cast<AssociatedConstant>(value)) {
+        if (assocs_in_interface.count(&assoc->constant()) &&
+            ValueEqual(&assoc->base(), self, std::nullopt) &&
+            ValueEqual(&assoc->interface(), interface, std::nullopt)) {
+          // This equality constraint mentions an associated constant that is
+          // part of interface. Bring it into scope.
+          scope.AddEqualityConstraint(&eq);
+          break;
+        }
+      }
+    }
+  }
+}
+
 auto TypeChecker::TypeCheckImplDeclaration(Nonnull<ImplDeclaration*> impl_decl,
                                            const ImplScope& enclosing_scope)
     -> ErrorOr<Success> {
   if (trace_stream_) {
     **trace_stream_ << "checking " << *impl_decl << "\n";
   }
+
+  // Form the resolved constraint type by substituting `Self` for `.Self`.
+  Nonnull<const Value*> self = *impl_decl->self()->constant_value();
+  BindingMap constraint_self_map;
+  constraint_self_map[impl_decl->constraint_type()->self_binding()] = self;
+  Nonnull<const ConstraintType*> constraint = cast<ConstraintType>(
+      Substitute(constraint_self_map, impl_decl->constraint_type()));
+
   // Bring the impls from the parameters into scope.
   ImplScope impl_scope;
   impl_scope.AddParent(&enclosing_scope);
   BringImplsIntoScope(impl_decl->impl_bindings(), impl_scope);
   for (Nonnull<Declaration*> m : impl_decl->members()) {
-    CARBON_RETURN_IF_ERROR(TypeCheckDeclaration(m, impl_scope));
+    CARBON_ASSIGN_OR_RETURN(
+        ConstraintLookupResult result,
+        LookupInConstraint(m->source_loc(), "member impl declaration",
+                           constraint, GetName(*m).value()));
+
+    // Bring the associated constant values for the interface that this method
+    // implements part of into scope.
+    ImplScope member_scope;
+    member_scope.AddParent(&impl_scope);
+    BringAssociatedConstantsIntoScope(constraint, self, result.interface,
+                                      member_scope);
+
+    CARBON_RETURN_IF_ERROR(TypeCheckDeclaration(m, member_scope));
   }
   if (trace_stream_) {
     **trace_stream_ << "finished checking impl\n";
@@ -3287,6 +3555,7 @@ static bool IsValidTypeForAliasTarget(Nonnull<const Value*> type) {
     case Value::Kind::ChoiceType:
     case Value::Kind::ContinuationType:
     case Value::Kind::StringType:
+    case Value::Kind::AssociatedConstant:
       return false;
 
     case Value::Kind::FunctionType:
@@ -3389,6 +3658,8 @@ auto TypeChecker::TypeCheckDeclaration(Nonnull<Declaration*> d,
       }
       return Success();
     }
+    case DeclarationKind::AssociatedConstantDeclaration:
+      return Success();
     case DeclarationKind::SelfDeclaration: {
       CARBON_FATAL() << "Unreachable TypeChecker `Self` declaration";
     }
@@ -3451,6 +3722,17 @@ auto TypeChecker::DeclareDeclaration(Nonnull<Declaration*> d,
       break;
     }
 
+    case DeclarationKind::AssociatedConstantDeclaration: {
+      auto& let = cast<AssociatedConstantDeclaration>(*d);
+      CARBON_ASSIGN_OR_RETURN(
+          Nonnull<const Value*> type,
+          TypeCheckTypeExp(&let.binding().type(), *scope_info.innermost_scope));
+      let.binding().set_static_type(type);
+      let.set_static_type(type);
+      // The symbolic identity is set by DeclareInterfaceDeclaration.
+      break;
+    }
+
     case DeclarationKind::SelfDeclaration: {
       CARBON_FATAL() << "Unreachable TypeChecker declare `Self` declaration";
     }
diff --git a/explorer/interpreter/type_checker.h b/explorer/interpreter/type_checker.h
index efc2deda99fd..78ded625aa70 100644
--- a/explorer/interpreter/type_checker.h
+++ b/explorer/interpreter/type_checker.h
@@ -78,6 +78,8 @@ class TypeChecker {
       -> Nonnull<Expression*>;
 
  private:
+  struct SingleStepEqualityContext;
+
   // Information about the currently enclosing scopes.
   struct ScopeInfo {
     static auto ForNonClassScope(Nonnull<ImplScope*> impl_scope) -> ScopeInfo {
@@ -194,7 +196,8 @@ class TypeChecker {
   // interface is present in the given `impl`.
   auto CheckImplIsComplete(Nonnull<const InterfaceType*> iface_type,
                            Nonnull<const ImplDeclaration*> impl_decl,
-                           Nonnull<const Value*> self_type) -> ErrorOr<Success>;
+                           Nonnull<const Value*> self_type,
+                           const ImplScope& impl_scope) -> ErrorOr<Success>;
 
   // Check that an `impl` declaration satisfies its constraints and add the
   // corresponding `ImplBinding`s to the impl scope.
@@ -261,6 +264,12 @@ class TypeChecker {
                                      const ImplScope& impl_scope)
       -> ErrorOr<Success>;
 
+  // Bring the associated constants in `constraint` that constrain the
+  // implementation of `interface` for `self` into `scope`.
+  void BringAssociatedConstantsIntoScope(
+      Nonnull<const ConstraintType*> constraint, Nonnull<const Value*> self,
+      Nonnull<const InterfaceType*> interface, ImplScope& scope);
+
   // Type check all the members of the implementation.
   auto TypeCheckImplDeclaration(Nonnull<ImplDeclaration*> impl_decl,
                                 const ImplScope& impl_scope)
@@ -296,13 +305,20 @@ class TypeChecker {
   // must be types.
   auto FieldTypesImplicitlyConvertible(
       llvm::ArrayRef<NamedValue> source_fields,
-      llvm::ArrayRef<NamedValue> destination_fields) const -> bool;
+      llvm::ArrayRef<NamedValue> destination_fields,
+      const ImplScope& impl_scope) const -> bool;
 
   // Returns true if *source is implicitly convertible to *destination. *source
   // and *destination must be concrete types.
-  auto IsImplicitlyConvertible(
-      Nonnull<const Value*> source, Nonnull<const Value*> destination,
-      std::optional<Nonnull<const ImplScope*>> impl_scope) const -> bool;
+  //
+  // If allow_user_defined_conversions, conversions requiring a user-defined
+  // `ImplicitAs` implementation are not considered, and only builtin
+  // conversions will be allowed.
+  auto IsImplicitlyConvertible(Nonnull<const Value*> source,
+                               Nonnull<const Value*> destination,
+                               const ImplScope& impl_scope,
+                               bool allow_user_defined_conversions) const
+      -> bool;
 
   // Attempt to implicitly convert type-checked expression `source` to the type
   // `destination`.
@@ -315,16 +331,18 @@ class TypeChecker {
   // Check whether `actual` is implicitly convertible to `expected`
   // and halt with a fatal compilation error if it is not.
   //
-  // If `impl_scope` is `std::nullopt`, only built-in conversions are
-  // considered.
-  // TODO: Remove this behavior.
-  //
   // TODO: Does not actually perform the conversion if a user-defined
   // conversion is needed. Should be used very rarely for that reason.
   auto ExpectType(SourceLocation source_loc, const std::string& context,
                   Nonnull<const Value*> expected, Nonnull<const Value*> actual,
-                  std::optional<Nonnull<const ImplScope*>> impl_scope) const
-      -> ErrorOr<Success>;
+                  const ImplScope& impl_scope) const -> ErrorOr<Success>;
+
+  // Check whether `actual` is the same type as `expected` and halt with a
+  // fatal compilation error if it is not.
+  auto ExpectExactType(SourceLocation source_loc, const std::string& context,
+                       Nonnull<const Value*> expected,
+                       Nonnull<const Value*> actual,
+                       const ImplScope& impl_scope) const -> ErrorOr<Success>;
 
   // The name of a builtin interface, with any arguments.
   struct BuiltinInterfaceName {
diff --git a/explorer/interpreter/value.cpp b/explorer/interpreter/value.cpp
index 7f7c37aa7145..fd9991da3146 100644
--- a/explorer/interpreter/value.cpp
+++ b/explorer/interpreter/value.cpp
@@ -10,6 +10,7 @@
 #include "explorer/common/arena.h"
 #include "explorer/common/error_builders.h"
 #include "explorer/interpreter/action.h"
+#include "llvm/ADT/STLExtras.h"
 #include "llvm/ADT/StringExtras.h"
 #include "llvm/Support/Casting.h"
 #include "llvm/Support/Error.h"
@@ -18,6 +19,8 @@ namespace Carbon {
 
 using llvm::cast;
 using llvm::dyn_cast;
+using llvm::dyn_cast_or_null;
+using llvm::isa;
 
 auto StructValue::FindField(std::string_view name) const
     -> std::optional<Nonnull<const Value*>> {
@@ -37,6 +40,16 @@ static auto GetMember(Nonnull<Arena*> arena, Nonnull<const Value*> v,
 
   if (field.witness().has_value()) {
     Nonnull<const Witness*> witness = cast<Witness>(*field.witness());
+
+    // Associated constants.
+    if (auto* assoc_const = dyn_cast_or_null<AssociatedConstantDeclaration>(
+            field.member().declaration().value_or(nullptr))) {
+      CARBON_CHECK(field.interface()) << "have witness but no interface";
+      return arena->New<AssociatedConstant>(v, *field.interface(), assoc_const,
+                                            witness);
+    }
+
+    // Associated functions.
     switch (witness->kind()) {
       case Value::Kind::ImplWitness: {
         auto* impl_witness = cast<ImplWitness>(witness);
@@ -156,10 +169,10 @@ static auto SetFieldImpl(
   switch (value->kind()) {
     case Value::Kind::StructValue: {
       std::vector<NamedValue> elements = cast<StructValue>(*value).elements();
-      auto it = std::find_if(elements.begin(), elements.end(),
-                             [path_begin](const NamedValue& element) {
-                               return element.name == (*path_begin).name();
-                             });
+      auto it =
+          llvm::find_if(elements, [path_begin](const NamedValue& element) {
+            return element.name == (*path_begin).name();
+          });
       if (it == elements.end()) {
         return RuntimeError(source_loc)
                << "field " << (*path_begin).name() << " not in " << *value;
@@ -397,7 +410,7 @@ void Value::Print(llvm::raw_ostream& out) const {
         out << combine << *ctx.context;
       }
       out << " where ";
-      llvm::ListSeparator sep;
+      llvm::ListSeparator sep(" and ");
       for (const ConstraintType::ImplConstraint& impl :
            constraint.impl_constraints()) {
         // TODO: Skip cases where `impl.type` is `.Self` and the interface is
@@ -453,6 +466,11 @@ void Value::Print(llvm::raw_ostream& out) const {
     case Value::Kind::VariableType:
       out << cast<VariableType>(*this).binding();
       break;
+    case Value::Kind::AssociatedConstant: {
+      const auto& assoc = cast<AssociatedConstant>(*this);
+      out << "(" << assoc.base() << ")." << assoc.constant().binding().name();
+      break;
+    }
     case Value::Kind::ContinuationValue: {
       out << cast<ContinuationValue>(*this).stack();
       break;
@@ -540,30 +558,36 @@ void ContinuationValue::StackFragment::Print(llvm::raw_ostream& out) const {
 
 // Check whether two binding maps, which are assumed to have the same keys, are
 // equal.
-static auto BindingMapEqual(const BindingMap& map1, const BindingMap& map2)
-    -> bool {
+static auto BindingMapEqual(
+    const BindingMap& map1, const BindingMap& map2,
+    std::optional<Nonnull<const EqualityContext*>> equality_ctx) -> bool {
   CARBON_CHECK(map1.size() == map2.size()) << "maps should have same keys";
   for (const auto& [key, value] : map1) {
-    if (!ValueEqual(value, map2.at(key))) {
+    if (!ValueEqual(value, map2.at(key), equality_ctx)) {
       return false;
     }
   }
   return true;
 }
 
-auto TypeEqual(Nonnull<const Value*> t1, Nonnull<const Value*> t2) -> bool {
+auto TypeEqual(Nonnull<const Value*> t1, Nonnull<const Value*> t2,
+               std::optional<Nonnull<const EqualityContext*>> equality_ctx)
+    -> bool {
   if (t1->kind() != t2->kind()) {
+    if (isa<AssociatedConstant>(t1) || isa<AssociatedConstant>(t2)) {
+      return ValueEqual(t1, t2, equality_ctx);
+    }
     return false;
   }
   switch (t1->kind()) {
     case Value::Kind::PointerType:
       return TypeEqual(&cast<PointerType>(*t1).type(),
-                       &cast<PointerType>(*t2).type());
+                       &cast<PointerType>(*t2).type(), equality_ctx);
     case Value::Kind::FunctionType: {
       const auto& fn1 = cast<FunctionType>(*t1);
       const auto& fn2 = cast<FunctionType>(*t2);
-      return TypeEqual(&fn1.parameters(), &fn2.parameters()) &&
-             TypeEqual(&fn1.return_type(), &fn2.return_type());
+      return TypeEqual(&fn1.parameters(), &fn2.parameters(), equality_ctx) &&
+             TypeEqual(&fn1.return_type(), &fn2.return_type(), equality_ctx);
     }
     case Value::Kind::StructType: {
       const auto& struct1 = cast<StructType>(*t1);
@@ -573,7 +597,8 @@ auto TypeEqual(Nonnull<const Value*> t1, Nonnull<const Value*> t2) -> bool {
       }
       for (size_t i = 0; i < struct1.fields().size(); ++i) {
         if (struct1.fields()[i].name != struct2.fields()[i].name ||
-            !TypeEqual(struct1.fields()[i].value, struct2.fields()[i].value)) {
+            !TypeEqual(struct1.fields()[i].value, struct2.fields()[i].value,
+                       equality_ctx)) {
           return false;
         }
       }
@@ -583,14 +608,18 @@ auto TypeEqual(Nonnull<const Value*> t1, Nonnull<const Value*> t2) -> bool {
       const auto& class1 = cast<NominalClassType>(*t1);
       const auto& class2 = cast<NominalClassType>(*t2);
       return class1.declaration().name() == class2.declaration().name() &&
-             BindingMapEqual(class1.type_args(), class2.type_args());
+             BindingMapEqual(class1.type_args(), class2.type_args(),
+                             equality_ctx);
     }
     case Value::Kind::InterfaceType: {
       const auto& iface1 = cast<InterfaceType>(*t1);
       const auto& iface2 = cast<InterfaceType>(*t2);
       return iface1.declaration().name() == iface2.declaration().name() &&
-             BindingMapEqual(iface1.args(), iface2.args());
+             BindingMapEqual(iface1.args(), iface2.args(), equality_ctx);
     }
+    case Value::Kind::AssociatedConstant:
+      // Associated constants are sometimes types.
+      return ValueEqual(t1, t2, equality_ctx);
     case Value::Kind::ConstraintType: {
       const auto& constraint1 = cast<ConstraintType>(*t1);
       const auto& constraint2 = cast<ConstraintType>(*t2);
@@ -605,8 +634,8 @@ auto TypeEqual(Nonnull<const Value*> t1, Nonnull<const Value*> t2) -> bool {
       for (size_t i = 0; i < constraint1.impl_constraints().size(); ++i) {
         const auto& impl1 = constraint1.impl_constraints()[i];
         const auto& impl2 = constraint2.impl_constraints()[i];
-        if (!TypeEqual(impl1.type, impl2.type) ||
-            !TypeEqual(impl1.interface, impl2.interface)) {
+        if (!TypeEqual(impl1.type, impl2.type, equality_ctx) ||
+            !TypeEqual(impl1.interface, impl2.interface, equality_ctx)) {
           return false;
         }
       }
@@ -617,7 +646,8 @@ auto TypeEqual(Nonnull<const Value*> t1, Nonnull<const Value*> t2) -> bool {
           return false;
         }
         for (size_t j = 0; j < equality1.values.size(); ++j) {
-          if (!ValueEqual(equality1.values[i], equality2.values[i])) {
+          if (!ValueEqual(equality1.values[i], equality2.values[i],
+                          equality_ctx)) {
             return false;
           }
         }
@@ -625,7 +655,7 @@ auto TypeEqual(Nonnull<const Value*> t1, Nonnull<const Value*> t2) -> bool {
       for (size_t i = 0; i < constraint1.lookup_contexts().size(); ++i) {
         const auto& context1 = constraint1.lookup_contexts()[i];
         const auto& context2 = constraint2.lookup_contexts()[i];
-        if (!TypeEqual(context1.context, context2.context)) {
+        if (!TypeEqual(context1.context, context2.context, equality_ctx)) {
           return false;
         }
       }
@@ -640,7 +670,7 @@ auto TypeEqual(Nonnull<const Value*> t1, Nonnull<const Value*> t2) -> bool {
         return false;
       }
       for (size_t i = 0; i < tup1.elements().size(); ++i) {
-        if (!TypeEqual(tup1.elements()[i], tup2.elements()[i])) {
+        if (!TypeEqual(tup1.elements()[i], tup2.elements()[i], equality_ctx)) {
           return false;
         }
       }
@@ -657,20 +687,24 @@ auto TypeEqual(Nonnull<const Value*> t1, Nonnull<const Value*> t2) -> bool {
              &cast<VariableType>(*t2).binding();
     case Value::Kind::TypeOfClassType:
       return TypeEqual(&cast<TypeOfClassType>(*t1).class_type(),
-                       &cast<TypeOfClassType>(*t2).class_type());
+                       &cast<TypeOfClassType>(*t2).class_type(), equality_ctx);
     case Value::Kind::TypeOfInterfaceType:
       return TypeEqual(&cast<TypeOfInterfaceType>(*t1).interface_type(),
-                       &cast<TypeOfInterfaceType>(*t2).interface_type());
+                       &cast<TypeOfInterfaceType>(*t2).interface_type(),
+                       equality_ctx);
     case Value::Kind::TypeOfConstraintType:
       return TypeEqual(&cast<TypeOfConstraintType>(*t1).constraint_type(),
-                       &cast<TypeOfConstraintType>(*t2).constraint_type());
+                       &cast<TypeOfConstraintType>(*t2).constraint_type(),
+                       equality_ctx);
     case Value::Kind::TypeOfChoiceType:
       return TypeEqual(&cast<TypeOfChoiceType>(*t1).choice_type(),
-                       &cast<TypeOfChoiceType>(*t2).choice_type());
+                       &cast<TypeOfChoiceType>(*t2).choice_type(),
+                       equality_ctx);
     case Value::Kind::StaticArrayType: {
       const auto& array1 = cast<StaticArrayType>(*t1);
       const auto& array2 = cast<StaticArrayType>(*t2);
-      return TypeEqual(&array1.element_type(), &array2.element_type()) &&
+      return TypeEqual(&array1.element_type(), &array2.element_type(),
+                       equality_ctx) &&
              array1.size() == array2.size();
     }
     case Value::Kind::IntValue:
@@ -704,10 +738,11 @@ auto TypeEqual(Nonnull<const Value*> t1, Nonnull<const Value*> t2) -> bool {
   }
 }
 
-// Returns true if the two values are equal and returns false otherwise.
-//
-// This function implements the `==` operator of Carbon.
-auto ValueEqual(Nonnull<const Value*> v1, Nonnull<const Value*> v2) -> bool {
+// Returns true if the two values are known to be equal and are written in the
+// same way at the top level.
+auto ValueStructurallyEqual(
+    Nonnull<const Value*> v1, Nonnull<const Value*> v2,
+    std::optional<Nonnull<const EqualityContext*>> equality_ctx) -> bool {
   if (v1->kind() != v2->kind()) {
     return false;
   }
@@ -729,7 +764,7 @@ auto ValueEqual(Nonnull<const Value*> v1, Nonnull<const Value*> v2) -> bool {
       const auto& m2 = cast<BoundMethodValue>(*v2);
       std::optional<Nonnull<const Statement*>> body1 = m1.declaration().body();
       std::optional<Nonnull<const Statement*>> body2 = m2.declaration().body();
-      return ValueEqual(m1.receiver(), m2.receiver()) &&
+      return ValueEqual(m1.receiver(), m2.receiver(), equality_ctx) &&
              body1.has_value() == body2.has_value() &&
              (!body1.has_value() || *body1 == *body2);
     }
@@ -742,7 +777,7 @@ auto ValueEqual(Nonnull<const Value*> v1, Nonnull<const Value*> v2) -> bool {
         return false;
       }
       for (size_t i = 0; i < elements1.size(); ++i) {
-        if (!ValueEqual(elements1[i], elements2[i])) {
+        if (!ValueEqual(elements1[i], elements2[i], equality_ctx)) {
           return false;
         }
       }
@@ -756,7 +791,7 @@ auto ValueEqual(Nonnull<const Value*> v1, Nonnull<const Value*> v2) -> bool {
         CARBON_CHECK(struct_v1.elements()[i].name ==
                      struct_v2.elements()[i].name);
         if (!ValueEqual(struct_v1.elements()[i].value,
-                        struct_v2.elements()[i].value)) {
+                        struct_v2.elements()[i].value, equality_ctx)) {
           return false;
         }
       }
@@ -773,6 +808,14 @@ auto ValueEqual(Nonnull<const Value*> v1, Nonnull<const Value*> v2) -> bool {
           << "parameterized name refers to unnamed declaration";
       return *name1 == *name2;
     }
+    case Value::Kind::AssociatedConstant: {
+      // The witness value is not part of determining value equality.
+      const auto& assoc1 = cast<AssociatedConstant>(*v1);
+      const auto& assoc2 = cast<AssociatedConstant>(*v2);
+      return &assoc1.constant() == &assoc2.constant() &&
+             TypeEqual(&assoc1.base(), &assoc2.base(), equality_ctx) &&
+             TypeEqual(&assoc1.interface(), &assoc2.interface(), equality_ctx);
+    }
     case Value::Kind::IntType:
     case Value::Kind::BoolType:
     case Value::Kind::TypeType:
@@ -796,7 +839,7 @@ auto ValueEqual(Nonnull<const Value*> v1, Nonnull<const Value*> v2) -> bool {
     case Value::Kind::TypeOfParameterizedEntityName:
     case Value::Kind::TypeOfMemberName:
     case Value::Kind::StaticArrayType:
-      return TypeEqual(v1, v2);
+      return TypeEqual(v1, v2, equality_ctx);
     case Value::Kind::NominalClassValue:
     case Value::Kind::AlternativeValue:
     case Value::Kind::BindingPlaceholderValue:
@@ -813,6 +856,78 @@ auto ValueEqual(Nonnull<const Value*> v1, Nonnull<const Value*> v2) -> bool {
   }
 }
 
+// Returns true if the two values are equal and returns false otherwise.
+//
+// This function implements the `==` operator of Carbon.
+auto ValueEqual(Nonnull<const Value*> v1, Nonnull<const Value*> v2,
+                std::optional<Nonnull<const EqualityContext*>> equality_ctx)
+    -> bool {
+  // If we're given an equality context, check to see if it knows these values
+  // are equal. Only perform the check if one or the other value is an
+  // 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)) {
+      auto visitor = [&](Nonnull<const Value*> maybe_v2) {
+        return !ValueStructurallyEqual(v2, maybe_v2, equality_ctx);
+      };
+      if (!(*equality_ctx)->VisitEqualValues(v1, visitor)) {
+        return true;
+      }
+    }
+    if (isa<AssociatedConstant>(v2)) {
+      auto visitor = [&](Nonnull<const Value*> maybe_v1) {
+        return !ValueStructurallyEqual(v1, maybe_v1, equality_ctx);
+      };
+      if (!(*equality_ctx)->VisitEqualValues(v2, visitor)) {
+        return true;
+      }
+    }
+  }
+
+  return ValueStructurallyEqual(v1, v2, equality_ctx);
+}
+
+auto EqualityConstraint::VisitEqualValues(
+    Nonnull<const Value*> value,
+    llvm::function_ref<bool(Nonnull<const Value*>)> visitor) const -> bool {
+  // See if the given value is part of this constraint.
+  auto first_equal = llvm::find_if(values, [value](Nonnull<const Value*> val) {
+    return ValueEqual(value, val, std::nullopt);
+  });
+  if (first_equal == values.end()) {
+    return true;
+  }
+
+  // The value is in this group; pass all non-identical values in the group
+  // to the visitor. First visit the values we already compared.
+  for (auto* val : llvm::make_range(values.begin(), first_equal)) {
+    if (!visitor(val)) {
+      return false;
+    }
+  }
+  // Then visit any remaining non-identical values, skipping the one we already
+  // found was identical.
+  ++first_equal;
+  for (auto* val : llvm::make_range(first_equal, values.end())) {
+    if (!ValueEqual(value, val, std::nullopt) && !visitor(val)) {
+      return false;
+    }
+  }
+  return true;
+}
+
+auto ConstraintType::VisitEqualValues(
+    Nonnull<const Value*> value,
+    llvm::function_ref<bool(Nonnull<const Value*>)> visitor) const -> bool {
+  for (const auto& eq : equality_constraints()) {
+    if (!eq.VisitEqualValues(value, visitor)) {
+      return false;
+    }
+  }
+  return true;
+}
+
 auto ChoiceType::FindAlternative(std::string_view name) const
     -> std::optional<Nonnull<const Value*>> {
   for (const NamedValue& alternative : alternatives_) {
diff --git a/explorer/interpreter/value.h b/explorer/interpreter/value.h
index 0f381f7f2072..8b9772127804 100644
--- a/explorer/interpreter/value.h
+++ b/explorer/interpreter/value.h
@@ -24,6 +24,7 @@
 namespace Carbon {
 
 class Action;
+class ImplScope;
 
 // Abstract base class of all AST nodes representing values.
 //
@@ -61,6 +62,7 @@ class Value {
     ChoiceType,
     ContinuationType,  // The type of a continuation.
     VariableType,      // e.g., generic type parameters.
+    AssociatedConstant,
     ParameterizedEntityName,
     MemberName,
     BindingPlaceholderValue,
@@ -113,6 +115,26 @@ class Value {
   const Kind kind_;
 };
 
+// Base class for types holding contextual information by which we can
+// determine whether values are equal.
+class EqualityContext {
+ public:
+  virtual auto VisitEqualValues(
+      Nonnull<const Value*> value,
+      llvm::function_ref<bool(Nonnull<const Value*>)> visitor) const
+      -> bool = 0;
+
+ protected:
+  ~EqualityContext() = default;
+};
+
+auto TypeEqual(Nonnull<const Value*> t1, Nonnull<const Value*> t2,
+               std::optional<Nonnull<const EqualityContext*>> equality_ctx)
+    -> bool;
+auto ValueEqual(Nonnull<const Value*> v1, Nonnull<const Value*> v2,
+                std::optional<Nonnull<const EqualityContext*>> equality_ctx)
+    -> bool;
+
 // An integer value.
 class IntValue : public Value {
  public:
@@ -631,6 +653,23 @@ class InterfaceType : public Value {
   Nonnull<const Bindings*> bindings_ = Bindings::None();
 };
 
+// A collection of values that are known to be the same.
+struct EqualityConstraint {
+  // Visit the values in this equality constraint that are a single step away
+  // from the given value according to this equality constraint. That is: if
+  // `value` is identical to a value in `values`, then call the visitor on all
+  // values in `values` that are not identical to `value`. Otherwise, do not
+  // call the visitor.
+  //
+  // Stops and returns `false` if any call to the visitor returns `false`,
+  // otherwise returns `true`.
+  auto VisitEqualValues(
+      Nonnull<const Value*> value,
+      llvm::function_ref<bool(Nonnull<const Value*>)> visitor) const -> bool;
+
+  std::vector<Nonnull<const Value*>> values;
+};
+
 // A type-of-type for an unknown constrained type.
 //
 // These types are formed by the `&` operator that combines constraints and by
@@ -655,10 +694,7 @@ class ConstraintType : public Value {
     Nonnull<const InterfaceType*> interface;
   };
 
-  // A collection of values that are known to be the same.
-  struct EqualityConstraint {
-    std::vector<Nonnull<const Value*>> values;
-  };
+  using EqualityConstraint = Carbon::EqualityConstraint;
 
   // A context in which we might look up a name.
   struct LookupContext {
@@ -696,6 +732,17 @@ class ConstraintType : public Value {
     return lookup_contexts_;
   }
 
+  // Visit the values in that are a single step away from the given value
+  // according to equality constraints in this constraint type, that is, the
+  // values `v` that are not identical to `value` but for which we have a
+  // `value == v` equality constraint in this constraint type.
+  //
+  // Stops and returns `false` if any call to the visitor returns `false`,
+  // otherwise returns `true`.
+  auto VisitEqualValues(
+      Nonnull<const Value*> value,
+      llvm::function_ref<bool(Nonnull<const Value*>)> visitor) const -> bool;
+
  private:
   Nonnull<const GenericBinding*> self_binding_;
   std::vector<ImplConstraint> impl_constraints_;
@@ -882,6 +929,47 @@ class MemberName : public Value {
   Member member_;
 };
 
+// A symbolic value representing an associated constant.
+//
+// This is a value of the form `A.B` or `A.B.C` or similar, where `A` is a
+// `VariableType`.
+class AssociatedConstant : public Value {
+ public:
+  explicit AssociatedConstant(
+      Nonnull<const Value*> base, Nonnull<const InterfaceType*> interface,
+      Nonnull<const AssociatedConstantDeclaration*> constant,
+      Nonnull<const Witness*> witness)
+      : Value(Kind::AssociatedConstant),
+        base_(base),
+        interface_(interface),
+        constant_(constant),
+        witness_(witness) {}
+
+  static auto classof(const Value* value) -> bool {
+    return value->kind() == Kind::AssociatedConstant;
+  }
+
+  // The type for which we denote an associated constant.
+  auto base() const -> const Value& { return *base_; }
+
+  // The interface within which the constant was declared.
+  auto interface() const -> const InterfaceType& { return *interface_; }
+
+  // The associated constant whose value is being denoted.
+  auto constant() const -> const AssociatedConstantDeclaration& {
+    return *constant_;
+  }
+
+  // Witness within which the constant's value can be found.
+  auto witness() const -> const Witness& { return *witness_; }
+
+ private:
+  Nonnull<const Value*> base_;
+  Nonnull<const InterfaceType*> interface_;
+  Nonnull<const AssociatedConstantDeclaration*> constant_;
+  Nonnull<const Witness*> witness_;
+};
+
 // A first-class continuation representation of a fragment of the stack.
 // A continuation value behaves like a pointer to the underlying stack
 // fragment, which is exposed by `Stack()`.
@@ -1100,9 +1188,6 @@ class StaticArrayType : public Value {
   size_t size_;
 };
 
-auto TypeEqual(Nonnull<const Value*> t1, Nonnull<const Value*> t2) -> bool;
-auto ValueEqual(Nonnull<const Value*> v1, Nonnull<const Value*> v2) -> bool;
-
 }  // namespace Carbon
 
 #endif  // CARBON_EXPLORER_INTERPRETER_VALUE_H_
diff --git a/explorer/syntax/parser.ypp b/explorer/syntax/parser.ypp
index 17357e7e099a..ea1746ab62c2 100644
--- a/explorer/syntax/parser.ypp
+++ b/explorer/syntax/parser.ypp
@@ -1034,6 +1034,12 @@ interface_body:
       $$ = $1;
       $$.push_back($2);
     }
+| interface_body LET generic_binding SEMICOLON
+    {
+      $$ = $1;
+      $$.push_back(
+          arena->New<AssociatedConstantDeclaration>(context.source_loc(), $3));
+    }
 ;
 impl_body:
   // Empty
diff --git a/explorer/testdata/assoc_const/fail_anonymous.carbon b/explorer/testdata/assoc_const/fail_anonymous.carbon
new file mode 100644
index 000000000000..8264bf7587c8
--- /dev/null
+++ b/explorer/testdata/assoc_const/fail_anonymous.carbon
@@ -0,0 +1,18 @@
+// 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 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+interface Iface {
+  // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_anonymous.carbon:[[@LINE+1]]: syntax error, unexpected UNDERSCORE, expecting identifier
+  let _:! Type;
+}
+
+fn Main() -> i32 { return 0; }
diff --git a/explorer/testdata/assoc_const/fail_incomplete_impl_1.carbon b/explorer/testdata/assoc_const/fail_incomplete_impl_1.carbon
new file mode 100644
index 000000000000..f933a915e517
--- /dev/null
+++ b/explorer/testdata/assoc_const/fail_incomplete_impl_1.carbon
@@ -0,0 +1,22 @@
+// 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 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+interface HasThreeTypes {
+  let A:! Type;
+  let B:! Type;
+  let C:! Type;
+}
+
+// CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_incomplete_impl_1.carbon:[[@LINE+1]]: implementation missing (.Self:! 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
new file mode 100644
index 000000000000..c45857f2d5a3
--- /dev/null
+++ b/explorer/testdata/assoc_const/fail_incomplete_impl_2.carbon
@@ -0,0 +1,22 @@
+// 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 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+interface HasThreeTypes {
+  let A:! Type;
+  let B:! Type;
+  let C:! Type;
+}
+
+// CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_incomplete_impl_2.carbon:[[@LINE+1]]: implementation doesn't provide a concrete value for (.Self:! HasThreeTypes).B
+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
new file mode 100644
index 000000000000..9620c4ae4f78
--- /dev/null
+++ b/explorer/testdata/assoc_const/fail_indirectly_equal.carbon
@@ -0,0 +1,36 @@
+// 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 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+interface A {
+  let T:! Type;
+}
+
+fn F1[T:! A where .T == i32](x: T.T) -> i32 {
+  // OK: one equality.
+  return x;
+}
+
+fn F2[U:! A where .T == i32](x: i32) -> U.T {
+  // OK: one equality.
+  return x;
+}
+
+fn F3[T:! A where .T == i32, U:! A where .T == i32](x: T.T) -> U.T {
+  // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_indirectly_equal.carbon:[[@LINE+1]]: type error in return value: '(T:! A where .Self.T == i32).T' is not implicitly convertible to '(U:! A where .Self.T == i32).T'
+  return x;
+}
+
+external impl i32 as A where .T == i32 {}
+
+fn Main() -> i32 {
+  return F3(0);
+}
diff --git a/explorer/testdata/assoc_const/fail_match_in_deduction.carbon b/explorer/testdata/assoc_const/fail_match_in_deduction.carbon
new file mode 100644
index 000000000000..b6b96f6bdf10
--- /dev/null
+++ b/explorer/testdata/assoc_const/fail_match_in_deduction.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 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+// TODO: Should this work?
+
+package ExplorerTest api;
+
+interface Vector {
+  let Dim:! i32;
+}
+external impl (i32, i32, i32) as Vector where .Dim == 3 {}
+
+class Point(Scalar:! Type, Dim:! i32) {}
+
+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: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_match_in_deduction.carbon:[[@LINE+1]]: mismatch in non-type values, `(V:! Vector where .Self.Dim == 3).Dim` != `3`
+  G(p);
+}
+
+fn Main() -> i32 {
+  var p: Point(i32, 3) = {};
+  // Deduce Point(Scalar, V.Dim) from Point(i32, 3).
+  F(p, (0, 0, 0));
+  // Deduce Point(Scalar, 3) from Point(i32, V.Dim).
+  H((0, 0, 0));
+  return 0;
+}
diff --git a/explorer/testdata/assoc_const/fail_multi_impl_scoping.carbon b/explorer/testdata/assoc_const/fail_multi_impl_scoping.carbon
new file mode 100644
index 000000000000..4b18ce1a9f93
--- /dev/null
+++ b/explorer/testdata/assoc_const/fail_multi_impl_scoping.carbon
@@ -0,0 +1,46 @@
+// 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 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+interface A {
+  let TA:! Type;
+  fn FA() -> TA;
+}
+interface B {
+  let TB:! Type;
+  fn FB() -> TB;
+}
+
+class C(T:! Type) {
+  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;
+      let w: i32 = v;
+      return w;
+    }
+    fn FB() -> i32 {
+      // OK, know that TB is i32 here.
+      let v: Self.(B.TB) = 2;
+      // TODO: Don't know that TA is i32. It could be specialized.
+      // We should reject this once we support specialization.
+      let w: Self.(A.TA) = 3;
+      return v + w;
+    }
+  }
+}
+
+external impl C(i32) as B where .TB == () {
+  fn FB() -> () { return (); }
+// CHECK: 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
new file mode 100644
index 000000000000..7c36edf00848
--- /dev/null
+++ b/explorer/testdata/assoc_const/fail_multiple_deduction.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 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+interface HasThreeTypes {
+  let A:! Type;
+  let B:! Type;
+  let C:! Type;
+  fn Make[me: Self]() -> (A, B, C);
+}
+fn F[T:! Type](x: (T, T, T));
+fn G[X:! HasThreeTypes where .A == .B and .B == .C and .C == .A](x: X) {
+  // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_multiple_deduction.carbon:[[@LINE+3]]: deduced multiple different values for T:! Type:
+  // CHECK:   (X:! HasThreeTypes where .Self.A == .Self.B and .Self.B == .Self.C and .Self.C == .Self.A).A
+  // CHECK:   (X:! HasThreeTypes where .Self.A == .Self.B and .Self.B == .Self.C and .Self.C == .Self.A).B
+  F(x.Make());
+}
+
+fn Main() -> i32 { return 0; }
diff --git a/explorer/testdata/assoc_const/fail_overspecified_impl.carbon b/explorer/testdata/assoc_const/fail_overspecified_impl.carbon
new file mode 100644
index 000000000000..122443b221e7
--- /dev/null
+++ b/explorer/testdata/assoc_const/fail_overspecified_impl.carbon
@@ -0,0 +1,20 @@
+// 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 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+interface HasType {
+  let T:! Type;
+}
+
+// CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_overspecified_impl.carbon:[[@LINE+1]]: implementation provides multiple values for (.Self:! HasType).T: i32 and {.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_redefined.carbon b/explorer/testdata/assoc_const/fail_redefined.carbon
new file mode 100644
index 000000000000..25a9afd9943e
--- /dev/null
+++ b/explorer/testdata/assoc_const/fail_redefined.carbon
@@ -0,0 +1,19 @@
+// 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 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+interface Iface {
+  let T:! Type;
+  // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_redefined.carbon:[[@LINE+1]]: Duplicate name `T` also found at {{.*}}/explorer/testdata/assoc_const/fail_redefined.carbon:14
+  let T:! Type;
+}
+
+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
new file mode 100644
index 000000000000..81ade90902b2
--- /dev/null
+++ b/explorer/testdata/assoc_const/fail_unknown_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 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+interface Iface { let N:! i32; }
+
+fn PickType(N: i32) -> Type { return i32; }
+
+fn F[T:! Iface](x: T) -> i32 {
+  // CHECK: 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 {}
+
+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
new file mode 100644
index 000000000000..999b6c0b6e06
--- /dev/null
+++ b/explorer/testdata/assoc_const/fail_unknown_value_specified_in_constraint.carbon
@@ -0,0 +1,28 @@
+// 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 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+interface Iface { let N:! i32; }
+
+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: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_unknown_value_specified_in_constraint.carbon:[[@LINE+1]]: value of associated constant (T:! Iface where .Self.N == 5).N is not known
+  var x: PickType(T.N) = 0;
+  return x;
+}
+
+impl i32 as Iface where .N == 5 {}
+
+fn Main() -> i32 {
+  return F(0);
+}
diff --git a/explorer/testdata/assoc_const/impl_lookup.carbon b/explorer/testdata/assoc_const/impl_lookup.carbon
new file mode 100644
index 000000000000..542fa80daec6
--- /dev/null
+++ b/explorer/testdata/assoc_const/impl_lookup.carbon
@@ -0,0 +1,40 @@
+// 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 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK: result: 1
+
+package ExplorerTest api;
+
+interface Frob {
+  let Result:! Type;
+  fn F[me: Self]() -> Result;
+}
+
+fn Use[T:! Frob](x: T) -> T.Result {
+  var v: T.Result = x.F();
+  return v;
+}
+
+class AlmostI32 {
+  var val: i32;
+  impl as ImplicitAs(i32) {
+    fn Convert[me: Self]() -> i32 { return me.val; }
+  }
+}
+
+impl i32 as Frob where .Result == AlmostI32 {
+  fn F[me: Self]() -> AlmostI32 { return {.val = me}; }
+}
+
+fn Main() -> i32 {
+  // Ensure that lookup for
+  //   i32.(Frob.Result) as ImplicitAs(i32)
+  // finds `impl AlmostI32 as ImplicitAs(i32)`.
+  return Use(1);
+}
diff --git a/explorer/testdata/assoc_const/implement.carbon b/explorer/testdata/assoc_const/implement.carbon
new file mode 100644
index 000000000000..8becf1f49ed3
--- /dev/null
+++ b/explorer/testdata/assoc_const/implement.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: %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK: result: 2
+
+package ExplorerTest api;
+
+interface Vector {
+  let Dim:! i32;
+}
+
+class Point {
+  var x: i32;
+  var y: i32;
+  impl as Vector where .Dim == 2 {}
+}
+
+fn Main() -> i32 {
+  var a: Point = {.x = 2, .y = 1};
+  return a.(Vector.Dim);
+}
diff --git a/explorer/testdata/assoc_const/simple_constraint.carbon b/explorer/testdata/assoc_const/simple_constraint.carbon
new file mode 100644
index 000000000000..e6998b8e86bc
--- /dev/null
+++ b/explorer/testdata/assoc_const/simple_constraint.carbon
@@ -0,0 +1,30 @@
+// 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 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK: result: 3
+
+package ExplorerTest api;
+
+interface Frob {
+  let Result:! Type;
+  fn F[me: Self]() -> Result;
+}
+
+fn Use[T:! Frob where .Result == .Self](x: T) -> T {
+  var v: T = x.F();
+  return v;
+}
+
+impl i32 as Frob where .Result == i32 {
+  fn F[me: Self]() -> i32 { return me + 1; }
+}
+
+fn Main() -> i32 {
+  return Use(2);
+}
diff --git a/explorer/testdata/assoc_const/simple_equality.carbon b/explorer/testdata/assoc_const/simple_equality.carbon
new file mode 100644
index 000000000000..25736ebda1b3
--- /dev/null
+++ b/explorer/testdata/assoc_const/simple_equality.carbon
@@ -0,0 +1,30 @@
+// 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 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK: result: 0
+
+package ExplorerTest api;
+
+interface Frob {
+  let Result:! Type;
+  fn F[me: Self]() -> Result;
+}
+
+fn Use[T:! Frob](x: T) -> T.Result {
+  var v: T.Result = x.F();
+  return v;
+}
+
+impl i32 as Frob where .Result == i32 {
+  fn F[me: Self]() -> i32 { return 0; }
+}
+
+fn Main() -> i32 {
+  return Use(0);
+}
diff --git a/explorer/testdata/constraint/fail_where_equals_different_types.carbon b/explorer/testdata/constraint/fail_where_equals_different_types.carbon
index ccd0a04d6f83..d8257a1e33dd 100644
--- a/explorer/testdata/constraint/fail_where_equals_different_types.carbon
+++ b/explorer/testdata/constraint/fail_where_equals_different_types.carbon
@@ -12,9 +12,9 @@ package ExplorerTest api;
 
 interface A {}
 
-// CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/constraint/fail_where_equals_different_types.carbon:[[@LINE+3]]: type error in values in `where ==` constraint
-// CHECK: expected: i32
-// CHECK: actual: Type
+// CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/constraint/fail_where_equals_different_types.carbon:[[@LINE+3]]: type mismatch between values in `where LHS == RHS`
+// CHECK:   LHS type: i32
+// CHECK:   RHS type: Type
 alias B = A where 4 == i32;
 
 fn Main() -> i32 { return 0; }
diff --git a/explorer/testdata/constraint/missing_member.carbon b/explorer/testdata/constraint/missing_member.carbon
index aeffa6877ad2..f8dda156cd10 100644
--- a/explorer/testdata/constraint/missing_member.carbon
+++ b/explorer/testdata/constraint/missing_member.carbon
@@ -13,7 +13,7 @@ package ExplorerTest api;
 interface A { fn F() -> i32; }
 interface B { fn G() -> i32; }
 
-// CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/constraint/missing_member.carbon:[[@LINE+1]]: member access, H not in constraint interface A & interface B where .Self:! Type is interface A, .Self:! Type is interface B
+// CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/constraint/missing_member.carbon:[[@LINE+1]]: member access, H not in constraint interface A & interface B where .Self:! Type is interface A and .Self:! Type is interface B
 fn Get[T:! A & B](n: T) -> i32 { return n.H(); }
 
 impl i32 as A {
diff --git a/explorer/testdata/constraint/combine_equality.carbon b/explorer/testdata/constraint/no_combine_equality.carbon
similarity index 78%
rename from explorer/testdata/constraint/combine_equality.carbon
rename to explorer/testdata/constraint/no_combine_equality.carbon
index 67aca89c7651..7ff785ec031d 100644
--- a/explorer/testdata/constraint/combine_equality.carbon
+++ b/explorer/testdata/constraint/no_combine_equality.carbon
@@ -15,7 +15,7 @@ impl i32 as I {}
 
 fn F(A:! i32, B:! i32, C:! i32, D:! i32, E:! i32,
      T:! I where A == B and C == D and C == E and B == D) {
-  // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/constraint/combine_equality.carbon:[[@LINE+1]]: member access, F not in constraint interface I where .Self:! I is interface I, A:! i32 == B:! i32 == E:! i32 == C:! i32 == D:! i32
+  // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/constraint/no_combine_equality.carbon:[[@LINE+1]]: member access, F not in constraint interface I where .Self:! I is interface I and A:! i32 == B:! i32 and C:! i32 == D:! i32 and C:! i32 == E:! i32 and B:! i32 == D:! i32
   T.F();
 }
 
diff --git a/explorer/testdata/generic_class/fail_argument_deduction.carbon b/explorer/testdata/generic_class/fail_argument_deduction.carbon
index a5b253804c4e..4157657ef361 100644
--- a/explorer/testdata/generic_class/fail_argument_deduction.carbon
+++ b/explorer/testdata/generic_class/fail_argument_deduction.carbon
@@ -22,8 +22,8 @@ fn FirstOfTwoPoints[T:! Type](a: Point(T), b: Point(T)) -> Point(T) {
 fn Main() -> i32 {
   var p: Point(i32) = {.x = 0, .y = 1};
   var q: Point(Bool) = {.x = true, .y = false};
-  // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/generic_class/fail_argument_deduction.carbon:[[@LINE+3]]: type error in repeated argument deduction
-  // CHECK: expected: i32
-  // CHECK: actual: Bool
+  // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/generic_class/fail_argument_deduction.carbon:[[@LINE+3]]: deduced multiple different values for T:! Type:
+  // CHECK:   i32
+  // CHECK:   Bool
   return FirstOfTwoPoints(p, q).x;
 }
diff --git a/explorer/testdata/generic_class/fail_field_access_on_generic.carbon b/explorer/testdata/generic_class/fail_field_access_on_generic.carbon
index e36cc590ba93..5006628c9b67 100644
--- a/explorer/testdata/generic_class/fail_field_access_on_generic.carbon
+++ b/explorer/testdata/generic_class/fail_field_access_on_generic.carbon
@@ -11,7 +11,7 @@
 package ExplorerTest api;
 
 fn BadSimpleMemberAccess[T:! Type](a: T) -> T {
-  // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/generic_class/fail_field_access_on_generic.carbon:[[@LINE+1]]: member access into unconstrained type
+  // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/generic_class/fail_field_access_on_generic.carbon:[[@LINE+1]]: member access in unconstrained type
   return a.x;
 }
 
diff --git a/explorer/testdata/generic_function/fail_type_deduction_mismatch.carbon b/explorer/testdata/generic_function/fail_type_deduction_mismatch.carbon
index 66080c6a4cc2..88204d995359 100644
--- a/explorer/testdata/generic_function/fail_type_deduction_mismatch.carbon
+++ b/explorer/testdata/generic_function/fail_type_deduction_mismatch.carbon
@@ -15,8 +15,8 @@ fn fst[T:! Type](x: T, y: T) -> T {
 }
 
 fn Main() -> i32 {
-  // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/generic_function/fail_type_deduction_mismatch.carbon:[[@LINE+3]]: type error in repeated argument deduction
-  // CHECK: expected: i32
-  // CHECK: actual: Bool
+  // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/generic_function/fail_type_deduction_mismatch.carbon:[[@LINE+3]]: deduced multiple different values for T:! Type:
+  // CHECK:   i32
+  // CHECK:   Bool
   return fst(0, true);
 }
diff --git a/explorer/testdata/impl/impl_constraint.carbon b/explorer/testdata/impl/impl_constraint.carbon
index b900e31efd77..49b5f6cc216f 100644
--- a/explorer/testdata/impl/impl_constraint.carbon
+++ b/explorer/testdata/impl/impl_constraint.carbon
@@ -7,7 +7,7 @@
 // RUN: %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
 // RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
 // AUTOUPDATE: %{explorer} %s
-// CHECK: result: 1232
+// CHECK: result: 1234
 
 package ExplorerTest api;
 
@@ -19,20 +19,20 @@ interface B {
   fn G() -> i32;
 }
 interface C(T:! Type) {
-  fn F() -> T;
+  fn H() -> T;
 }
 
 external impl i32 as A {
   fn F() -> i32 { return 1; }
 }
 
-// TODO: Use `where .Self is A` once `.Self` support lands.
-external impl i32 as B & C(i32) where i32 is A {
+external impl i32 as B & C(i32) where .Self is A {
   fn F() -> i32 { return 2; }
   fn G() -> i32 { return 3; }
+  fn H() -> i32 { return 4; }
 }
 
 fn Main() -> i32 {
   let n: i32 = 0;
-  return n.(A.F)() * 1000 + n.(B.F)() * 100 + n.(B.G)() * 10 + n.(C(i32).F)();
+  return n.(A.F)() * 1000 + n.(B.F)() * 100 + n.(B.G)() * 10 + n.(C(i32).H)();
 }
diff --git a/explorer/testdata/interface/fail_bad_member_kind.carbon b/explorer/testdata/interface/fail_bad_member_kind.carbon
index 012bb230975d..1bc89c0ff81c 100644
--- a/explorer/testdata/interface/fail_bad_member_kind.carbon
+++ b/explorer/testdata/interface/fail_bad_member_kind.carbon
@@ -11,7 +11,7 @@
 package ExplorerTest api;
 
 interface Bad {
-  // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/interface/fail_bad_member_kind.carbon:[[@LINE+1]]: syntax error, unexpected VAR, expecting FN or RIGHT_CURLY_BRACE
+  // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/interface/fail_bad_member_kind.carbon:[[@LINE+1]]: syntax error, unexpected VAR, expecting FN or LET or RIGHT_CURLY_BRACE
   var V: i32;
 }