diff --git a/common/fuzzing/carbon.proto b/common/fuzzing/carbon.proto
index 4cd5a5177781..019e07938bb1 100644
--- a/common/fuzzing/carbon.proto
+++ b/common/fuzzing/carbon.proto
@@ -139,10 +139,16 @@ message EqualsWhereClause {
   optional Expression rhs = 2;
 }
 
+message RewriteWhereClause {
+  optional string member_name = 1;
+  optional Expression replacement = 2;
+}
+
 message WhereClause {
   oneof kind {
     IsWhereClause is = 1;
     EqualsWhereClause equals = 2;
+    RewriteWhereClause rewrite = 3;
   }
 }
 
diff --git a/common/fuzzing/proto_to_carbon.cpp b/common/fuzzing/proto_to_carbon.cpp
index ede4bed6e8f5..9360ea260d48 100644
--- a/common/fuzzing/proto_to_carbon.cpp
+++ b/common/fuzzing/proto_to_carbon.cpp
@@ -409,6 +409,10 @@ static auto ExpressionToCarbon(const Fuzzing::Expression& expression,
             out << " == ";
             ExpressionToCarbon(clause.equals().rhs(), out);
             break;
+          case Fuzzing::WhereClause::kRewrite:
+            out << "." << clause.rewrite().member_name() << " = ";
+            ExpressionToCarbon(clause.rewrite().replacement(), out);
+            break;
           case Fuzzing::WhereClause::KIND_NOT_SET:
             // Arbitrary default to avoid invalid syntax.
             out << ".Self == .Self";
diff --git a/explorer/ast/ast_rtti.txt b/explorer/ast/ast_rtti.txt
index 52e4dc42996a..e78df7302b97 100644
--- a/explorer/ast/ast_rtti.txt
+++ b/explorer/ast/ast_rtti.txt
@@ -75,3 +75,4 @@ abstract class Expression : AstNode;
 abstract class WhereClause : AstNode;
   class IsWhereClause : WhereClause;
   class EqualsWhereClause : WhereClause;
+  class RewriteWhereClause : WhereClause;
diff --git a/explorer/ast/declaration.h b/explorer/ast/declaration.h
index 1fadf27858c8..5955c94aed8b 100644
--- a/explorer/ast/declaration.h
+++ b/explorer/ast/declaration.h
@@ -500,12 +500,27 @@ class InterfaceDeclaration : public Declaration {
 
   auto value_category() const -> ValueCategory { return ValueCategory::Let; }
 
+  // Get the constraint type corresponding to this interface, or nullopt if
+  // this interface is incomplete.
+  auto constraint_type() const
+      -> std::optional<Nonnull<const ConstraintType*>> {
+    return constraint_type_;
+  }
+
+  // Set the constraint type corresponding to this interface. Can only be set
+  // once, by type-checking.
+  void set_constraint_type(Nonnull<const ConstraintType*> constraint_type) {
+    CARBON_CHECK(!constraint_type_);
+    constraint_type_ = constraint_type;
+  }
+
  private:
   std::string name_;
   std::optional<Nonnull<TuplePattern*>> params_;
   Nonnull<SelfDeclaration*> self_type_;
   Nonnull<GenericBinding*> self_;
   std::vector<Nonnull<Declaration*>> members_;
+  std::optional<Nonnull<const ConstraintType*>> constraint_type_;
 };
 
 class AssociatedConstantDeclaration : public Declaration {
@@ -570,6 +585,8 @@ class ImplDeclaration : public Declaration {
   auto constraint_type() const -> Nonnull<const ConstraintType*> {
     return *constraint_type_;
   }
+  // Returns the deduced parameters specified on the impl declaration. This
+  // does not include any generic parameters from enclosing scopes.
   auto deduced_parameters() const
       -> llvm::ArrayRef<Nonnull<const GenericBinding*>> {
     return deduced_parameters_;
diff --git a/explorer/ast/expression.cpp b/explorer/ast/expression.cpp
index 37aa80e48110..a87e91a2e224 100644
--- a/explorer/ast/expression.cpp
+++ b/explorer/ast/expression.cpp
@@ -360,6 +360,11 @@ void WhereClause::Print(llvm::raw_ostream& out) const {
       out << clause.lhs() << " == " << clause.rhs();
       break;
     }
+    case WhereClauseKind::RewriteWhereClause: {
+      auto& clause = cast<RewriteWhereClause>(*this);
+      out << "." << clause.member_name() << " = " << clause.replacement();
+      break;
+    }
   }
 }
 
diff --git a/explorer/ast/expression.h b/explorer/ast/expression.h
index e80d1924c5e7..3355a0d65528 100644
--- a/explorer/ast/expression.h
+++ b/explorer/ast/expression.h
@@ -93,6 +93,33 @@ class Expression : public AstNode {
   std::optional<ValueCategory> value_category_;
 };
 
+// A mixin for expressions that can be rewritten to a different expression by
+// type-checking.
+template <typename Base>
+class RewritableMixin : public Base {
+ public:
+  using Base::Base;
+
+  // Set the rewritten form of this expression. Can only be called during type
+  // checking.
+  auto set_rewritten_form(const Expression* rewritten_form) -> void {
+    CARBON_CHECK(!rewritten_form_.has_value()) << "rewritten form set twice";
+    rewritten_form_ = rewritten_form;
+    this->set_static_type(&rewritten_form->static_type());
+    this->set_value_category(rewritten_form->value_category());
+  }
+
+  // Get the rewritten form of this expression. A rewritten form is used when
+  // the expression is rewritten as a function call on an interface. A
+  // rewritten form is not used when providing built-in operator semantics.
+  auto rewritten_form() const -> std::optional<Nonnull<const Expression*>> {
+    return rewritten_form_;
+  }
+
+ private:
+  std::optional<Nonnull<const Expression*>> rewritten_form_;
+};
+
 // A FieldInitializer represents the initialization of a single struct field.
 class FieldInitializer {
  public:
@@ -246,10 +273,26 @@ class MemberAccessExpression : public Expression {
     impl_ = impl;
   }
 
+  // Returns the constant value of this expression, if one has been set. This
+  // value will be used instead of accessing a member. Even if this is present,
+  // the operand of the member access expression must still be evaluated, in
+  // case it has side effects.
+  auto constant_value() const -> std::optional<Nonnull<const Value*>> {
+    return constant_value_;
+  }
+
+  // Sets the value returned by constant_value(). Can only be called once,
+  // during typechecking.
+  void set_constant_value(Nonnull<const Value*> value) {
+    CARBON_CHECK(!constant_value_.has_value());
+    constant_value_ = value;
+  }
+
  private:
   Nonnull<Expression*> object_;
   bool is_type_access_ = false;
   std::optional<Nonnull<const Witness*>> impl_;
+  std::optional<Nonnull<const Value*>> constant_value_;
 };
 
 class SimpleMemberAccessExpression : public MemberAccessExpression {
@@ -511,11 +554,11 @@ class StructTypeLiteral : public Expression {
   std::vector<FieldInitializer> fields_;
 };
 
-class OperatorExpression : public Expression {
+class OperatorExpression : public RewritableMixin<Expression> {
  public:
   explicit OperatorExpression(SourceLocation source_loc, Operator op,
                               std::vector<Nonnull<Expression*>> arguments)
-      : Expression(AstNodeKind::OperatorExpression, source_loc),
+      : RewritableMixin(AstNodeKind::OperatorExpression, source_loc),
         op_(op),
         arguments_(std::move(arguments)) {}
 
@@ -531,25 +574,9 @@ class OperatorExpression : public Expression {
     return arguments_;
   }
 
-  // Set the rewritten form of this expression. Can only be called during type
-  // checking.
-  auto set_rewritten_form(const Expression* rewritten_form) -> void {
-    CARBON_CHECK(!rewritten_form_.has_value()) << "rewritten form set twice";
-    rewritten_form_ = rewritten_form;
-    set_static_type(&rewritten_form->static_type());
-    set_value_category(rewritten_form->value_category());
-  }
-  // Get the rewritten form of this expression. A rewritten form is used when
-  // the expression is rewritten as a function call on an interface. A
-  // rewritten form is not used when providing built-in operator semantics.
-  auto rewritten_form() const -> std::optional<Nonnull<const Expression*>> {
-    return rewritten_form_;
-  }
-
  private:
   Operator op_;
   std::vector<Nonnull<Expression*>> arguments_;
-  std::optional<Nonnull<const Expression*>> rewritten_form_;
 };
 
 class CallExpression : public Expression {
@@ -839,6 +866,33 @@ class EqualsWhereClause : public WhereClause {
   Nonnull<Expression*> rhs_;
 };
 
+// An `=` where clause.
+//
+// For example, `Constraint where .Type = i32` specifies that the associated
+// type `.Type` is rewritten to `i32` whenever used.
+class RewriteWhereClause : public WhereClause {
+ public:
+  explicit RewriteWhereClause(SourceLocation source_loc,
+                              std::string member_name,
+                              Nonnull<Expression*> replacement)
+      : WhereClause(WhereClauseKind::RewriteWhereClause, source_loc),
+        member_name_(member_name),
+        replacement_(replacement) {}
+
+  static auto classof(const AstNode* node) {
+    return InheritsFromRewriteWhereClause(node->kind());
+  }
+
+  auto member_name() const -> std::string_view { return member_name_; }
+
+  auto replacement() const -> const Expression& { return *replacement_; }
+  auto replacement() -> Expression& { return *replacement_; }
+
+ private:
+  std::string member_name_;
+  Nonnull<Expression*> replacement_;
+};
+
 // A `where` expression: `AddableWith(i32) where .Result == i32`.
 //
 // The first operand is rewritten to a generic binding, for example
diff --git a/explorer/data/prelude.carbon b/explorer/data/prelude.carbon
index 594794cdf88f..dbb26ef641a4 100644
--- a/explorer/data/prelude.carbon
+++ b/explorer/data/prelude.carbon
@@ -332,22 +332,22 @@ interface ModWith(U:! Type) {
 // TODO: constraint Mod { ... }
 
 // Note, these impls use the builtin addition for i32.
-external impl i32 as Negate where .Result == i32 {
+external impl i32 as Negate where .Result = i32 {
   fn Op[me: i32]() -> i32 { return -me; }
 }
-external impl i32 as AddWith(i32) where .Result == i32 {
+external impl i32 as AddWith(i32) where .Result = i32 {
   fn Op[me: i32](other: i32) -> i32 { return me + other; }
 }
-external impl i32 as SubWith(i32) where .Result == i32 {
+external impl i32 as SubWith(i32) where .Result = i32 {
   fn Op[me: i32](other: i32) -> i32 { return me - other; }
 }
-external impl i32 as MulWith(i32) where .Result == i32 {
+external impl i32 as MulWith(i32) where .Result = i32 {
   fn Op[me: i32](other: i32) -> i32 { return me * other; }
 }
-external impl i32 as DivWith(i32) where .Result == i32 {
+external impl i32 as DivWith(i32) where .Result = i32 {
   fn Op[me: i32](other: i32) -> i32 { return me / other; }
 }
-external impl i32 as ModWith(i32) where .Result == i32 {
+external impl i32 as ModWith(i32) where .Result = i32 {
   fn Op[me: i32](other: i32) -> i32 { return me % other; }
 }
 
@@ -370,7 +370,7 @@ interface BitAndWith(U:! Type) {
 }
 // TODO:
 // constraint BitAnd {
-//   extends BitAndWith(Self) where .Result == Self;
+//   extends BitAndWith(Self) where .Result = Self;
 // }
 
 // Binary `|`.
@@ -381,7 +381,7 @@ interface BitOrWith(U:! Type) {
 }
 // TODO:
 // constraint BitOr {
-//   extends BitOrWith(Self) where .Result == Self;
+//   extends BitOrWith(Self) where .Result = Self;
 // }
 
 // Binary `^`.
@@ -392,7 +392,7 @@ interface BitXorWith(U:! Type) {
 }
 // TODO:
 // constraint BitXor {
-//   extends BitXorWith(Self) where .Result == Self;
+//   extends BitXorWith(Self) where .Result = Self;
 // }
 
 // Binary `<<`.
@@ -403,7 +403,7 @@ interface LeftShiftWith(U:! Type) {
 }
 // TODO:
 // constraint LeftShift {
-//   extends LeftShiftWith(Self) where .Result == Self;
+//   extends LeftShiftWith(Self) where .Result = Self;
 // }
 
 // Binary `>>`.
@@ -414,35 +414,35 @@ interface RightShiftWith(U:! Type) {
 }
 // TODO:
 // constraint RightShift {
-//   extends RightShiftWith(Self) where .Result == Self;
+//   extends RightShiftWith(Self) where .Result = Self;
 // }
 
-external impl i32 as BitComplement where .Result == i32 {
+external impl i32 as BitComplement where .Result = i32 {
   fn Op[me: i32]() -> i32 {
     return __intrinsic_int_bit_complement(me);
   }
 }
-external impl i32 as BitAndWith(i32) where .Result == i32 {
+external impl i32 as BitAndWith(i32) where .Result = i32 {
   fn Op[me: i32](other: i32) -> i32 {
     return __intrinsic_int_bit_and(me, other);
   }
 }
-external impl i32 as BitOrWith(i32) where .Result == i32 {
+external impl i32 as BitOrWith(i32) where .Result = i32 {
   fn Op[me: i32](other: i32) -> i32 {
     return __intrinsic_int_bit_or(me, other);
   }
 }
-external impl i32 as BitXorWith(i32) where .Result == i32 {
+external impl i32 as BitXorWith(i32) where .Result = i32 {
   fn Op[me: i32](other: i32) -> i32 {
     return __intrinsic_int_bit_xor(me, other);
   }
 }
-external impl i32 as LeftShiftWith(i32) where .Result == i32 {
+external impl i32 as LeftShiftWith(i32) where .Result = i32 {
   fn Op[me: i32](other: i32) -> i32 {
     return __intrinsic_int_left_shift(me, other);
   }
 }
-external impl i32 as RightShiftWith(i32) where .Result == i32 {
+external impl i32 as RightShiftWith(i32) where .Result = i32 {
   fn Op[me: i32](other: i32) -> i32 {
     return __intrinsic_int_right_shift(me, other);
   }
diff --git a/explorer/fuzzing/ast_to_proto.cpp b/explorer/fuzzing/ast_to_proto.cpp
index f0553a419b46..89795d82920b 100644
--- a/explorer/fuzzing/ast_to_proto.cpp
+++ b/explorer/fuzzing/ast_to_proto.cpp
@@ -237,6 +237,14 @@ static auto ExpressionToProto(const Expression& expression)
                 ExpressionToProto(cast<EqualsWhereClause>(where)->rhs());
             break;
           }
+          case WhereClauseKind::RewriteWhereClause: {
+            auto* rewrite = clause_proto.mutable_rewrite();
+            rewrite->set_member_name(
+                std::string(cast<RewriteWhereClause>(where)->member_name()));
+            *rewrite->mutable_replacement() = ExpressionToProto(
+                cast<RewriteWhereClause>(where)->replacement());
+            break;
+          }
         }
         *where_proto->add_clauses() = clause_proto;
       }
diff --git a/explorer/interpreter/impl_scope.cpp b/explorer/interpreter/impl_scope.cpp
index e75a1629604a..f6a4342c5c41 100644
--- a/explorer/interpreter/impl_scope.cpp
+++ b/explorer/interpreter/impl_scope.cpp
@@ -11,6 +11,7 @@
 
 using llvm::cast;
 using llvm::dyn_cast;
+using llvm::isa;
 
 namespace Carbon {
 
@@ -67,9 +68,12 @@ void ImplScope::AddParent(Nonnull<const ImplScope*> parent) {
 auto ImplScope::Resolve(Nonnull<const Value*> constraint_type,
                         Nonnull<const Value*> impl_type,
                         SourceLocation source_loc,
-                        const TypeChecker& type_checker) const
+                        const TypeChecker& type_checker,
+                        const Bindings& bindings) const
     -> ErrorOr<Nonnull<const Witness*>> {
   if (const auto* iface_type = dyn_cast<InterfaceType>(constraint_type)) {
+    iface_type =
+        cast<InterfaceType>(type_checker.Substitute(bindings, iface_type));
     return ResolveInterface(iface_type, impl_type, source_loc, type_checker);
   }
   if (const auto* constraint = dyn_cast<ConstraintType>(constraint_type)) {
@@ -89,13 +93,13 @@ auto ImplScope::Resolve(Nonnull<const Value*> constraint_type,
         witness = type_checker.MakeConstraintWitness(*constraint, witnesses,
                                                      source_loc);
       }
-      Bindings bindings;
-      bindings.Add(constraint->self_binding(), impl_type, witness);
+      Bindings local_bindings = bindings;
+      local_bindings.Add(constraint->self_binding(), impl_type, witness);
       CARBON_ASSIGN_OR_RETURN(
           Nonnull<const Witness*> result,
           ResolveInterface(cast<InterfaceType>(type_checker.Substitute(
-                               bindings, impl.interface)),
-                           type_checker.Substitute(bindings, impl.type),
+                               local_bindings, impl.interface)),
+                           type_checker.Substitute(local_bindings, impl.type),
                            source_loc, type_checker));
       witnesses.push_back(result);
     }
@@ -137,6 +141,42 @@ auto ImplScope::ResolveInterface(Nonnull<const InterfaceType*> iface_type,
   return *result;
 }
 
+// Combines the results of two impl lookups. In the event of a tie, arbitrarily
+// prefer `a` over `b`.
+static auto CombineResults(Nonnull<const InterfaceType*> iface_type,
+                           Nonnull<const Value*> type,
+                           SourceLocation source_loc,
+                           std::optional<Nonnull<const Witness*>> a,
+                           std::optional<Nonnull<const Witness*>> b)
+    -> ErrorOr<std::optional<Nonnull<const Witness*>>> {
+  // If only one lookup succeeded, return that.
+  if (!b) {
+    return a;
+  }
+  if (!a) {
+    return b;
+  }
+  // If either of them was a symbolic result, then they'll end up being
+  // equivalent. In that case, pick `a`.
+  auto* impl_a = dyn_cast<ImplWitness>(*a);
+  auto* impl_b = dyn_cast<ImplWitness>(*b);
+  if (!impl_b) {
+    return a;
+  }
+  if (!impl_a) {
+    return b;
+  }
+  // If they refer to the same `impl` declaration, it doesn't matter which one
+  // we pick, so we pick `a`.
+  // TODO: Compare the identities of the `impl`s, not the declarations.
+  if (&impl_a->declaration() == &impl_b->declaration()) {
+    return a;
+  }
+  // TODO: Order the `impl`s based on type structure.
+  return ProgramError(source_loc)
+         << "ambiguous implementations of " << *iface_type << " for " << *type;
+}
+
 auto ImplScope::TryResolve(Nonnull<const InterfaceType*> iface_type,
                            Nonnull<const Value*> type,
                            SourceLocation source_loc,
@@ -151,14 +191,8 @@ auto ImplScope::TryResolve(Nonnull<const InterfaceType*> iface_type,
         std::optional<Nonnull<const Witness*>> parent_result,
         parent->TryResolve(iface_type, type, source_loc, original_scope,
                            type_checker));
-    if (parent_result.has_value()) {
-      if (result.has_value()) {
-        return ProgramError(source_loc) << "ambiguous implementations of "
-                                        << *iface_type << " for " << *type;
-      } else {
-        result = *parent_result;
-      }
-    }
+    CARBON_ASSIGN_OR_RETURN(result, CombineResults(iface_type, type, source_loc,
+                                                   result, parent_result));
   }
   return result;
 }
@@ -173,14 +207,8 @@ auto ImplScope::ResolveHere(Nonnull<const InterfaceType*> iface_type,
   for (const Impl& impl : impls_) {
     std::optional<Nonnull<const Witness*>> m = type_checker.MatchImpl(
         *iface_type, impl_type, impl, original_scope, source_loc);
-    if (m.has_value()) {
-      if (result.has_value()) {
-        return ProgramError(source_loc) << "ambiguous implementations of "
-                                        << *iface_type << " for " << *impl_type;
-      } else {
-        result = *m;
-      }
-    }
+    CARBON_ASSIGN_OR_RETURN(
+        result, CombineResults(iface_type, impl_type, source_loc, result, m));
   }
   return result;
 }
diff --git a/explorer/interpreter/impl_scope.h b/explorer/interpreter/impl_scope.h
index 5f23d1a2aed0..417fcc406e22 100644
--- a/explorer/interpreter/impl_scope.h
+++ b/explorer/interpreter/impl_scope.h
@@ -76,8 +76,15 @@ class ImplScope {
   // Returns the associated impl for the given `constraint` and `type` in
   // the ancestor graph of this scope, or reports a compilation error
   // at `source_loc` there isn't exactly one matching impl.
+  //
+  // If any substitutions should be made into the constraint before resolving
+  // it, those should be passed in `bindings`. The witness returned will be for
+  // `constraint`, not for the result of substituting the bindings into the
+  // constraint. The substituted type might in general have a different shape
+  // of witness due to deduplication.
   auto Resolve(Nonnull<const Value*> constraint, Nonnull<const Value*> type,
-               SourceLocation source_loc, const TypeChecker& type_checker) const
+               SourceLocation source_loc, const TypeChecker& type_checker,
+               const Bindings& bindings = {}) const
       -> ErrorOr<Nonnull<const Witness*>>;
 
   // Visits the values that are a single step away from `value` according to an
diff --git a/explorer/interpreter/interpreter.cpp b/explorer/interpreter/interpreter.cpp
index 80cee73db03d..9fc9ddacb165 100644
--- a/explorer/interpreter/interpreter.cpp
+++ b/explorer/interpreter/interpreter.cpp
@@ -400,17 +400,22 @@ auto Interpreter::StepLvalue() -> ErrorOr<Success> {
       return todo_.FinishAction(value);
     }
     case ExpressionKind::SimpleMemberAccessExpression: {
+      const auto& access = cast<SimpleMemberAccessExpression>(exp);
       if (act.pos() == 0) {
         //    { {e.f :: C, E, F} :: S, H}
         // -> { e :: [].f :: C, E, F} :: S, H}
-        return todo_.Spawn(std::make_unique<LValAction>(
-            &cast<SimpleMemberAccessExpression>(exp).object()));
+        return todo_.Spawn(std::make_unique<LValAction>(&access.object()));
       } else {
+        if (auto constant_value = access.constant_value()) {
+          CARBON_ASSIGN_OR_RETURN(
+              Nonnull<const Value*> instantiated,
+              InstantiateType(*constant_value, access.source_loc()));
+          return todo_.FinishAction(instantiated);
+        }
         //    { v :: [].f :: C, E, F} :: S, H}
         // -> { { &v.f :: C, E, F} :: S, H }
         Address object = cast<LValue>(*act.results()[0]).address();
-        Address member = object.SubobjectAddress(
-            cast<SimpleMemberAccessExpression>(exp).member());
+        Address member = object.SubobjectAddress(access.member());
         return todo_.FinishAction(arena_->New<LValue>(member));
       }
     }
@@ -419,6 +424,12 @@ auto Interpreter::StepLvalue() -> ErrorOr<Success> {
       if (act.pos() == 0) {
         return todo_.Spawn(std::make_unique<LValAction>(&access.object()));
       } else {
+        if (auto constant_value = access.constant_value()) {
+          CARBON_ASSIGN_OR_RETURN(
+              Nonnull<const Value*> instantiated,
+              InstantiateType(*constant_value, access.source_loc()));
+          return todo_.FinishAction(instantiated);
+        }
         CARBON_CHECK(!access.member().interface().has_value())
             << "unexpected lvalue interface member";
         CARBON_ASSIGN_OR_RETURN(
@@ -976,6 +987,12 @@ auto Interpreter::StepExp() -> ErrorOr<Success> {
             std::make_unique<WitnessAction>(access.impl().value()));
       } else {
         // Finally, produce the result.
+        if (auto constant_value = access.constant_value()) {
+          CARBON_ASSIGN_OR_RETURN(
+              Nonnull<const Value*> instantiated,
+              InstantiateType(*constant_value, access.source_loc()));
+          return todo_.FinishAction(instantiated);
+        }
         std::optional<Nonnull<const InterfaceType*>> found_in_interface =
             access.found_in_interface();
         if (found_in_interface) {
@@ -1041,6 +1058,12 @@ auto Interpreter::StepExp() -> ErrorOr<Success> {
             std::make_unique<WitnessAction>(access.impl().value()));
       } else {
         // Finally, produce the result.
+        if (auto constant_value = access.constant_value()) {
+          CARBON_ASSIGN_OR_RETURN(
+              Nonnull<const Value*> instantiated,
+              InstantiateType(*constant_value, access.source_loc()));
+          return todo_.FinishAction(instantiated);
+        }
         std::optional<Nonnull<const InterfaceType*>> found_in_interface =
             access.member().interface();
         if (found_in_interface) {
diff --git a/explorer/interpreter/resolve_names.cpp b/explorer/interpreter/resolve_names.cpp
index 0abe7d1f2c89..fa34340f3b74 100644
--- a/explorer/interpreter/resolve_names.cpp
+++ b/explorer/interpreter/resolve_names.cpp
@@ -292,6 +292,12 @@ static auto ResolveNames(WhereClause& clause,
           ResolveNames(equals_clause.rhs(), enclosing_scope));
       break;
     }
+    case WhereClauseKind::RewriteWhereClause: {
+      auto& rewrite_clause = cast<RewriteWhereClause>(clause);
+      CARBON_RETURN_IF_ERROR(
+          ResolveNames(rewrite_clause.replacement(), enclosing_scope));
+      break;
+    }
   }
   return Success();
 }
diff --git a/explorer/interpreter/type_checker.cpp b/explorer/interpreter/type_checker.cpp
index dcbdff636e78..fac38e499da6 100644
--- a/explorer/interpreter/type_checker.cpp
+++ b/explorer/interpreter/type_checker.cpp
@@ -21,6 +21,7 @@
 #include "explorer/interpreter/value.h"
 #include "llvm/ADT/DenseSet.h"
 #include "llvm/ADT/StringExtras.h"
+#include "llvm/ADT/TinyPtrVector.h"
 #include "llvm/Support/Casting.h"
 #include "llvm/Support/Error.h"
 
@@ -37,33 +38,6 @@ struct TypeChecker::SingleStepEqualityContext : public EqualityContext {
                             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;
-    }
-    if (type_checker_->trace_stream_) {
-      **type_checker_->trace_stream_ << "found symbolic witness "
-                                     << assoc->witness()
-                                     << "; performing impl scope lookup\n";
-    }
-
-    CARBON_ASSIGN_OR_RETURN(
-        Nonnull<const Witness*> witness,
-        impl_scope_->Resolve(&assoc->interface(), &assoc->base(), source_loc,
-                             *type_checker_));
-    impl_witness = dyn_cast<ImplWitness>(witness);
-    if (impl_witness) {
-      return impl_witness;
-    }
-    return ProgramError(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
@@ -86,15 +60,12 @@ struct TypeChecker::SingleStepEqualityContext : public EqualityContext {
     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()) {
+      if (auto* impl_witness = dyn_cast<ImplWitness>(&assoc->witness())) {
         // Instantiate the impl to find the concrete constraint it implements.
         Nonnull<const ConstraintType*> constraint =
-            (*impl_witness)->declaration().constraint_type();
+            impl_witness->declaration().constraint_type();
         constraint = cast<ConstraintType>(
-            type_checker_->Substitute((*impl_witness)->bindings(), constraint));
+            type_checker_->Substitute(impl_witness->bindings(), constraint));
         if (type_checker_->trace_stream_) {
           **type_checker_->trace_stream_ << "found constraint " << *constraint
                                          << " for associated constant "
@@ -109,7 +80,8 @@ struct TypeChecker::SingleStepEqualityContext : public EqualityContext {
         if (type_checker_->trace_stream_) {
           **type_checker_->trace_stream_
               << "Could not resolve associated constant " << *assoc << ": "
-              << impl_witness.error() << "\n";
+              << "witness " << assoc->witness()
+              << " depends on a generic parameter\n";
         }
       }
     }
@@ -140,7 +112,7 @@ auto TypeChecker::IsSameType(Nonnull<const Value*> type1,
 }
 
 auto TypeChecker::ExpectExactType(SourceLocation source_loc,
-                                  const std::string& context,
+                                  std::string_view context,
                                   Nonnull<const Value*> expected,
                                   Nonnull<const Value*> actual,
                                   const ImplScope& impl_scope) const
@@ -154,7 +126,7 @@ auto TypeChecker::ExpectExactType(SourceLocation source_loc,
 }
 
 static auto ExpectPointerType(SourceLocation source_loc,
-                              const std::string& context,
+                              std::string_view context,
                               Nonnull<const Value*> actual)
     -> ErrorOr<Success> {
   // TODO: Try to resolve in equality context.
@@ -526,7 +498,7 @@ auto TypeChecker::IsImplicitlyConvertible(
          impl_scope.Resolve(*iface_type, source, source_loc, *this).ok();
 }
 
-auto TypeChecker::ImplicitlyConvert(const std::string& context,
+auto TypeChecker::ImplicitlyConvert(std::string_view context,
                                     const ImplScope& impl_scope,
                                     Nonnull<Expression*> source,
                                     Nonnull<const Value*> destination)
@@ -621,7 +593,7 @@ auto TypeChecker::BuildBuiltinMethodCall(const ImplScope& impl_scope,
 }
 
 auto TypeChecker::ExpectType(SourceLocation source_loc,
-                             const std::string& context,
+                             std::string_view context,
                              Nonnull<const Value*> expected,
                              Nonnull<const Value*> actual,
                              const ImplScope& impl_scope) const
@@ -637,21 +609,96 @@ auto TypeChecker::ExpectType(SourceLocation source_loc,
   }
 }
 
-auto TypeChecker::ArgumentDeduction(
-    SourceLocation source_loc, const std::string& context,
-    llvm::ArrayRef<Nonnull<const GenericBinding*>> bindings_to_deduce,
-    BindingMap& deduced, Nonnull<const Value*> param, Nonnull<const Value*> arg,
-    bool allow_implicit_conversion, const ImplScope& impl_scope) const
+// Argument deduction matches two values and attempts to find a set of
+// substitutions into deduced bindings in one of them that would result in the
+// other.
+class TypeChecker::ArgumentDeduction {
+ public:
+  ArgumentDeduction(
+      SourceLocation source_loc, std::string_view context,
+      llvm::ArrayRef<Nonnull<const GenericBinding*>> bindings_to_deduce,
+      std::optional<Nonnull<llvm::raw_ostream*>> trace_stream)
+      : source_loc_(source_loc),
+        context_(context),
+        deduced_bindings_in_order_(bindings_to_deduce),
+        trace_stream_(trace_stream) {
+    if (trace_stream_) {
+      **trace_stream_ << "performing argument deduction for bindings: ";
+      llvm::ListSeparator sep;
+      for (auto* binding : bindings_to_deduce) {
+        **trace_stream_ << sep << *binding;
+      }
+      **trace_stream_ << "\n";
+    }
+    for (auto* binding : bindings_to_deduce) {
+      deduced_values_.insert({binding, {}});
+    }
+  }
+
+  // Deduces the values of deduced bindings in `param` from the corresponding
+  // values in `arg`. `allow_implicit_conversion` specifies whether implicit
+  // conversions are permitted from the argument to the parameter type.
+  auto Deduce(Nonnull<const Value*> param, Nonnull<const Value*> arg,
+              bool allow_implicit_conversion) -> ErrorOr<Success>;
+
+  // Finds a binding to deduce that has not been deduced, if any exist.
+  auto FindUndeducedBinding() const
+      -> std::optional<Nonnull<const GenericBinding*>> {
+    for (auto* binding : deduced_bindings_in_order_) {
+      llvm::ArrayRef<Nonnull<const Value*>> values =
+          deduced_values_.find(binding)->second;
+      if (values.empty()) {
+        return binding;
+      }
+    }
+    return std::nullopt;
+  }
+
+  // Adds a value for a binding that is not deduced but still participates in
+  // substitution. For example, the `T` parameter in `fn F(T:! Type, x: T)`.
+  void AddNonDeducedBindingValue(Nonnull<const GenericBinding*> binding,
+                                 Nonnull<Expression*> argument) {
+    non_deduced_values_.push_back({binding, argument});
+  }
+
+  // Finishes deduction and forms a set of substitutions that transform `param`
+  // into `arg`.
+  auto Finish(TypeChecker& type_checker, const ImplScope& impl_scope) const
+      -> ErrorOr<Bindings>;
+
+ private:
+  SourceLocation source_loc_;
+  std::string_view context_;
+  llvm::ArrayRef<Nonnull<const GenericBinding*>> deduced_bindings_in_order_;
+  std::optional<Nonnull<llvm::raw_ostream*>> trace_stream_;
+
+  // Values for deduced bindings.
+  std::map<Nonnull<const GenericBinding*>,
+           llvm::TinyPtrVector<Nonnull<const Value*>>>
+      deduced_values_;
+  // Values for non-deduced bindings, such as parameters with corresponding
+  // argument expressions.
+  std::vector<std::pair<Nonnull<const GenericBinding*>, Nonnull<Expression*>>>
+      non_deduced_values_;
+
+  // Non-deduced mismatches that we deferred until we could perform
+  // substitutions into them.
+  struct NonDeducedMismatch {
+    Nonnull<const Value*> param;
+    Nonnull<const Value*> arg;
+    bool allow_implicit_conversion;
+  };
+  std::vector<NonDeducedMismatch> non_deduced_mismatches_;
+};
+
+auto TypeChecker::ArgumentDeduction::Deduce(Nonnull<const Value*> param,
+                                            Nonnull<const Value*> arg,
+                                            bool allow_implicit_conversion)
     -> ErrorOr<Success> {
   if (trace_stream_) {
     **trace_stream_ << "deducing " << *param << " from " << *arg << "\n";
-    **trace_stream_ << "bindings: ";
-    llvm::ListSeparator sep;
-    for (auto binding : bindings_to_deduce) {
-      **trace_stream_ << sep << *binding;
-    }
-    **trace_stream_ << "\n";
   }
+
   // Handle the case where we can't perform deduction, either because the
   // parameter is a primitive type or because the parameter and argument have
   // different forms. In this case, we require an implicit conversion to exist,
@@ -661,54 +708,30 @@ auto TypeChecker::ArgumentDeduction(
       // Parameter type contains a nested `auto` and argument type isn't the
       // same kind of type.
       // TODO: This seems like something we should be able to accept.
-      return ProgramError(source_loc) << "type error in " << context << "\n"
-                                      << "expected: " << *param << "\n"
-                                      << "actual: " << *arg;
+      return ProgramError(source_loc_) << "type error in " << context_ << "\n"
+                                       << "expected: " << *param << "\n"
+                                       << "actual: " << *arg;
     }
-    // TODO: Compute or deduce witnesses.
-    Bindings bindings(deduced, Bindings::NoWitnesses);
-    const Value* subst_param_type = Substitute(bindings, 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);
+
+    if (ValueEqual(param, arg, std::nullopt)) {
+      return Success();
+    }
+
+    // Defer checking until we can substitute into the parameter and see if it
+    // actually matches.
+    non_deduced_mismatches_.push_back(
+        {.param = param,
+         .arg = arg,
+         .allow_implicit_conversion = allow_implicit_conversion});
+    return Success();
   };
 
   switch (param->kind()) {
     case Value::Kind::VariableType: {
-      const auto& var_type = cast<VariableType>(*param);
       const auto& binding = cast<VariableType>(*param).binding();
-      if (binding.has_static_type()) {
-        // TODO: Compute or deduce witnesses.
-        Bindings bindings(deduced, Bindings::NoWitnesses);
-        const Value* binding_type =
-            Substitute(bindings, &binding.static_type());
-        if (!IsTypeOfType(binding_type)) {
-          if (!IsImplicitlyConvertible(arg, binding_type, impl_scope, false)) {
-            return ProgramError(source_loc)
-                   << "cannot convert deduced value " << *arg << " for "
-                   << binding.name() << " to parameter type " << *binding_type;
-          }
-        }
-      }
-
-      if (std::find(bindings_to_deduce.begin(), bindings_to_deduce.end(),
-                    &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. 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 ProgramError(source_loc)
-                   << "deduced multiple different values for "
-                   << var_type.binding() << ":\n  " << *it->second << "\n  "
-                   << *arg;
-          }
-        }
+      if (auto it = deduced_values_.find(&binding);
+          it != deduced_values_.end()) {
+        it->second.push_back(arg);
       } else {
         return handle_non_deduced_type();
       }
@@ -721,16 +744,15 @@ auto TypeChecker::ArgumentDeduction(
       const auto& param_tup = cast<TupleValue>(*param);
       const auto& arg_tup = cast<TupleValue>(*arg);
       if (param_tup.elements().size() != arg_tup.elements().size()) {
-        return ProgramError(source_loc)
+        return ProgramError(source_loc_)
                << "mismatch in tuple sizes, expected "
                << param_tup.elements().size() << " but got "
                << arg_tup.elements().size();
       }
       for (size_t i = 0; i < param_tup.elements().size(); ++i) {
-        CARBON_RETURN_IF_ERROR(
-            ArgumentDeduction(source_loc, context, bindings_to_deduce, deduced,
-                              param_tup.elements()[i], arg_tup.elements()[i],
-                              allow_implicit_conversion, impl_scope));
+        CARBON_RETURN_IF_ERROR(Deduce(param_tup.elements()[i],
+                                      arg_tup.elements()[i],
+                                      allow_implicit_conversion));
       }
       return Success();
     }
@@ -745,7 +767,7 @@ auto TypeChecker::ArgumentDeduction(
                                         bool missing_from_source) -> Error {
         static constexpr const char* SourceOrDestination[2] = {"source",
                                                                "destination"};
-        return ProgramError(source_loc)
+        return ProgramError(source_loc_)
                << "mismatch in field names, "
                << SourceOrDestination[missing_from_source ? 1 : 0] << " field `"
                << field.name << "` not in "
@@ -768,14 +790,13 @@ auto TypeChecker::ArgumentDeduction(
           }
           arg_field = arg_struct.fields()[i];
           if (param_field.name != arg_field.name) {
-            return ProgramError(source_loc)
+            return ProgramError(source_loc_)
                    << "mismatch in field names, `" << param_field.name
                    << "` != `" << arg_field.name << "`";
           }
         }
-        CARBON_RETURN_IF_ERROR(ArgumentDeduction(
-            source_loc, context, bindings_to_deduce, deduced, param_field.value,
-            arg_field.value, allow_implicit_conversion, impl_scope));
+        CARBON_RETURN_IF_ERROR(Deduce(param_field.value, arg_field.value,
+                                      allow_implicit_conversion));
       }
       if (param_struct.fields().size() != arg_struct.fields().size()) {
         CARBON_CHECK(allow_implicit_conversion)
@@ -797,24 +818,21 @@ auto TypeChecker::ArgumentDeduction(
       const auto& param_fn = cast<FunctionType>(*param);
       const auto& arg_fn = cast<FunctionType>(*arg);
       // TODO: handle situation when arg has deduced parameters.
-      CARBON_RETURN_IF_ERROR(
-          ArgumentDeduction(source_loc, context, bindings_to_deduce, deduced,
-                            &param_fn.parameters(), &arg_fn.parameters(),
-                            /*allow_implicit_conversion=*/false, impl_scope));
-      CARBON_RETURN_IF_ERROR(
-          ArgumentDeduction(source_loc, context, bindings_to_deduce, deduced,
-                            &param_fn.return_type(), &arg_fn.return_type(),
-                            /*allow_implicit_conversion=*/false, impl_scope));
+      CARBON_RETURN_IF_ERROR(Deduce(&param_fn.parameters(),
+                                    &arg_fn.parameters(),
+                                    /*allow_implicit_conversion=*/false));
+      CARBON_RETURN_IF_ERROR(Deduce(&param_fn.return_type(),
+                                    &arg_fn.return_type(),
+                                    /*allow_implicit_conversion=*/false));
       return Success();
     }
     case Value::Kind::PointerType: {
       if (arg->kind() != Value::Kind::PointerType) {
         return handle_non_deduced_type();
       }
-      return ArgumentDeduction(source_loc, context, bindings_to_deduce, deduced,
-                               &cast<PointerType>(*param).type(),
-                               &cast<PointerType>(*arg).type(),
-                               /*allow_implicit_conversion=*/false, impl_scope);
+      return Deduce(&cast<PointerType>(*param).type(),
+                    &cast<PointerType>(*arg).type(),
+                    /*allow_implicit_conversion=*/false);
     }
     // Nothing to do in the case for `auto`.
     case Value::Kind::AutoType: {
@@ -833,10 +851,9 @@ auto TypeChecker::ArgumentDeduction(
         return handle_non_deduced_type();
       }
       for (const auto& [ty, param_ty] : param_class_type.type_args()) {
-        CARBON_RETURN_IF_ERROR(
-            ArgumentDeduction(source_loc, context, bindings_to_deduce, deduced,
-                              param_ty, arg_class_type.type_args().at(ty),
-                              /*allow_implicit_conversion=*/false, impl_scope));
+        CARBON_RETURN_IF_ERROR(Deduce(param_ty,
+                                      arg_class_type.type_args().at(ty),
+                                      /*allow_implicit_conversion=*/false));
       }
       return Success();
     }
@@ -851,10 +868,8 @@ auto TypeChecker::ArgumentDeduction(
         return handle_non_deduced_type();
       }
       for (const auto& [ty, param_ty] : param_iface_type.args()) {
-        CARBON_RETURN_IF_ERROR(
-            ArgumentDeduction(source_loc, context, bindings_to_deduce, deduced,
-                              param_ty, arg_iface_type.args().at(ty),
-                              /*allow_implicit_conversion=*/false, impl_scope));
+        CARBON_RETURN_IF_ERROR(Deduce(param_ty, arg_iface_type.args().at(ty),
+                                      /*allow_implicit_conversion=*/false));
       }
       return Success();
     }
@@ -904,8 +919,8 @@ auto TypeChecker::ArgumentDeduction(
       // TODO: Deduce within the values where possible.
       // TODO: Consider in-scope value equalities here.
       if (!ValueEqual(param, arg, std::nullopt)) {
-        return ProgramError(source_loc) << "mismatch in non-type values, `"
-                                        << *arg << "` != `" << *param << "`";
+        return ProgramError(source_loc_) << "mismatch in non-type values, `"
+                                         << *arg << "` != `" << *param << "`";
       }
       return Success();
     }
@@ -915,6 +930,126 @@ auto TypeChecker::ArgumentDeduction(
   }
 }
 
+auto TypeChecker::ArgumentDeduction::Finish(TypeChecker& type_checker,
+                                            const ImplScope& impl_scope) const
+    -> ErrorOr<Bindings> {
+  // Check deduced values and build our resulting `Bindings` set. We do this in
+  // declaration order so that any bindings used in the type of a later binding
+  // have known values before we check that binding.
+  Bindings bindings;
+  for (auto* binding : deduced_bindings_in_order_) {
+    llvm::ArrayRef<Nonnull<const Value*>> values =
+        deduced_values_.find(binding)->second;
+    if (values.empty()) {
+      return ProgramError(source_loc_)
+             << "could not deduce type argument for type parameter "
+             << binding->name() << " in " << context_;
+    }
+
+    const Value* binding_type =
+        type_checker.Substitute(bindings, &binding->static_type());
+    const Value* substituted_type =
+        type_checker.Substitute(bindings, binding_type);
+    auto* first_value = values[0];
+    for (auto* value : values) {
+      // TODO: It's not clear that conversions are or should be possible here.
+      // If they are permitted, we should allow user-defined conversions, and
+      // actually perform the conversion.
+      if (!IsTypeOfType(substituted_type) &&
+          !type_checker.IsImplicitlyConvertible(value, substituted_type,
+                                                impl_scope, false)) {
+        return ProgramError(source_loc_)
+               << "cannot convert deduced value " << *value << " for "
+               << binding->name() << " to parameter type " << *substituted_type;
+      }
+
+      // All deductions are required to produce the same value. Note that we
+      // intentionally don't consider equality constraints 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 (!ValueEqual(first_value, value, std::nullopt)) {
+        return ProgramError(source_loc_)
+               << "deduced multiple different values for " << *binding
+               << ":\n  " << *first_value << "\n  " << *value;
+      }
+    }
+
+    // Find a witness for the binding if needed.
+    std::optional<Nonnull<const Witness*>> witness;
+    if (binding->impl_binding()) {
+      CARBON_ASSIGN_OR_RETURN(
+          witness, impl_scope.Resolve(binding_type, first_value, source_loc_,
+                                      type_checker, bindings));
+    }
+
+    bindings.Add(binding, first_value, witness);
+  }
+
+  // Evaluate and add non-deduced values. These are assumed to lexically follow
+  // the deduced bindings, so any bindings the type might reference are now
+  // known.
+  // TODO: This is not the case for `fn F(T:! Type, u: (V:! ImplicitAs(T)))`.
+  // However, we intend to disallow that.
+  for (auto [binding, arg] : non_deduced_values_) {
+    // Form the binding's resolved type and convert the argument expression to
+    // it.
+    const Value* binding_type = &binding->static_type();
+    const Value* substituted_type =
+        type_checker.Substitute(bindings, binding_type);
+    if (!IsTypeOfType(substituted_type)) {
+      CARBON_ASSIGN_OR_RETURN(
+          arg, type_checker.ImplicitlyConvert(context_, impl_scope, arg,
+                                              substituted_type));
+    }
+
+    // Evaluate the argument to get the value.
+    CARBON_ASSIGN_OR_RETURN(Nonnull<const Value*> value,
+                            InterpExp(arg, type_checker.arena_, trace_stream_));
+    if (trace_stream_) {
+      **trace_stream_ << "evaluated generic parameter " << *binding << " as "
+                      << *value << "\n";
+    }
+
+    // Find a witness for the binding if needed.
+    std::optional<Nonnull<const Witness*>> witness;
+    if (binding->impl_binding()) {
+      CARBON_ASSIGN_OR_RETURN(
+          witness, impl_scope.Resolve(binding_type, value, source_loc_,
+                                      type_checker, bindings));
+    }
+
+    bindings.Add(binding, value, witness);
+  }
+
+  // Check non-deduced potential mismatches now we can substitute into them.
+  for (auto& mismatch : non_deduced_mismatches_) {
+    const Value* subst_param_type =
+        type_checker.Substitute(bindings, mismatch.param);
+    CARBON_RETURN_IF_ERROR(
+        mismatch.allow_implicit_conversion
+            ? type_checker.ExpectType(source_loc_, context_, subst_param_type,
+                                      mismatch.arg, impl_scope)
+            : type_checker.ExpectExactType(source_loc_, context_,
+                                           subst_param_type, mismatch.arg,
+                                           impl_scope));
+  }
+
+  if (trace_stream_) {
+    **trace_stream_ << "deduction succeeded with results: {";
+    llvm::ListSeparator sep;
+    for (const auto& [binding, val] : bindings.args()) {
+      **trace_stream_ << sep << *binding << " = " << *val;
+    }
+    for (const auto& [binding, val] : bindings.witnesses()) {
+      **trace_stream_ << sep << *binding << " = " << *val;
+    }
+    **trace_stream_ << "}\n";
+  }
+
+  return std::move(bindings);
+}
+
 // Builder for constraint types.
 //
 // This type supports incrementally building a constraint type by adding
@@ -922,7 +1057,7 @@ auto TypeChecker::ArgumentDeduction(
 //
 // TODO: The deduplication here is very inefficient. We should use value
 // canonicalization or hashing or similar to speed this up.
-class ConstraintTypeBuilder {
+class TypeChecker::ConstraintTypeBuilder {
  public:
   ConstraintTypeBuilder(Nonnull<Arena*> arena, SourceLocation source_loc)
       : ConstraintTypeBuilder(arena, MakeSelfBinding(arena, source_loc)) {}
@@ -930,6 +1065,10 @@ class ConstraintTypeBuilder {
                         Nonnull<GenericBinding*> self_binding)
       : self_binding_(PrepareSelfBinding(arena, self_binding)),
         impl_binding_(AddImplBinding(arena, self_binding_)) {}
+  ConstraintTypeBuilder(Nonnull<Arena*> arena,
+                        Nonnull<GenericBinding*> self_binding,
+                        Nonnull<ImplBinding*> impl_binding)
+      : self_binding_(self_binding), impl_binding_(impl_binding) {}
 
   // Produces a type that refers to the `.Self` type of the constraint.
   auto GetSelfType() const -> Nonnull<const Value*> {
@@ -958,7 +1097,11 @@ class ConstraintTypeBuilder {
 
   // Adds an equality constraint -- `A == B`.
   void AddEqualityConstraint(ConstraintType::EqualityConstraint equal) {
-    CARBON_CHECK(equal.values.size() >= 2) << "degenerate equality constraint";
+    if (equal.values.size() < 2) {
+      // There's no need to track degenerate equality constraints. These can be
+      // formed by rewrites.
+      return;
+    }
 
     // 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
@@ -968,6 +1111,31 @@ class ConstraintTypeBuilder {
     equality_constraints_.push_back(std::move(equal));
   }
 
+  auto AddRewriteConstraint(SourceLocation source_loc,
+                            ConstraintType::RewriteConstraint rewrite)
+      -> ErrorOr<Success> {
+    for (ConstraintType::RewriteConstraint existing : rewrite_constraints_) {
+      if (ValueEqual(existing.interface, rewrite.interface, std::nullopt) &&
+          // TODO: Want a "declares same entity" check.
+          GetName(*existing.constant) == GetName(*rewrite.constant)) {
+        if (ValueEqual(&existing.replacement->value(),
+                       &rewrite.replacement->value(), std::nullopt) &&
+            TypeEqual(&existing.replacement->static_type(),
+                      &rewrite.replacement->static_type(), std::nullopt)) {
+          return Success();
+        }
+        return ProgramError(source_loc)
+               << "multiple different rewrites for `.("
+               << *rewrite.interface << "." << *GetName(*rewrite.constant)
+               << ")`:\n"
+               << "  " << *existing.replacement << "\n"
+               << "  " << *rewrite.replacement;
+      }
+    }
+    rewrite_constraints_.push_back(std::move(rewrite));
+    return Success();
+  }
+
   // Add a context for qualified name lookup, if not already present.
   void AddLookupContext(ConstraintType::LookupContext context) {
     for (ConstraintType::LookupContext existing : lookup_contexts_) {
@@ -983,11 +1151,12 @@ class ConstraintTypeBuilder {
   // constraint's self binding. The `self_witness` is the witness for the
   // resulting constraint, and can be `GetSelfWitness()`. The `bindings`
   // parameter specifies any additional substitutions to perform.
-  void AddAndSubstitute(const TypeChecker& type_checker,
+  auto AddAndSubstitute(const TypeChecker& type_checker,
                         Nonnull<const ConstraintType*> constraint,
                         Nonnull<const Value*> self,
                         Nonnull<const Witness*> self_witness,
-                        const Bindings& bindings, bool add_lookup_contexts) {
+                        const Bindings& bindings, bool add_lookup_contexts)
+      -> ErrorOr<Success> {
     // First substitute into the impl bindings to form the full witness for
     // the constraint type.
     std::vector<Nonnull<const Witness*>> witnesses;
@@ -1014,6 +1183,24 @@ class ConstraintTypeBuilder {
                            *constraint, std::move(witnesses),
                            constraint->self_binding()->source_loc()));
 
+    // TODO: What happens if these rewrites appear in the impl constraints?
+    // TODO: What happens if these rewrites appear in each other?
+    for (const auto& rewrite_constraint : constraint->rewrite_constraints()) {
+      auto* interface = cast<InterfaceType>(type_checker.Substitute(
+          local_bindings, rewrite_constraint.interface));
+      Nonnull<const Value*> value = type_checker.Substitute(
+          local_bindings, &rewrite_constraint.replacement->value());
+      Nonnull<const Value*> type = type_checker.Substitute(
+          local_bindings, &rewrite_constraint.replacement->static_type());
+      auto* replacement = type_checker.arena_->New<ValueLiteral>(
+          rewrite_constraint.replacement->source_loc(), value, type,
+          ValueCategory::Let);
+      CARBON_RETURN_IF_ERROR(AddRewriteConstraint(
+          replacement->source_loc(), {.interface = interface,
+                                      .constant = rewrite_constraint.constant,
+                                      .replacement = replacement}));
+    }
+
     for (const auto& equality_constraint : constraint->equality_constraints()) {
       std::vector<Nonnull<const Value*>> values;
       for (const Value* value : equality_constraint.values) {
@@ -1033,6 +1220,8 @@ class ConstraintTypeBuilder {
                               local_bindings, lookup_context.context)});
       }
     }
+
+    return Success();
   }
 
   // Brings all the `impl`s accumulated so far into the given impl scope.
@@ -1045,10 +1234,33 @@ class ConstraintTypeBuilder {
   // Converts the builder into a ConstraintType. Note that this consumes the
   // builder.
   auto Build(Nonnull<Arena*> arena_) && -> Nonnull<const ConstraintType*> {
+    // Rewrite `Self.X is Y` to `Replacement is Y` if we have a rewrite for
+    // `Self.X`.
+    // TODO: Properly apply rewrites throughout all the constraints. Check for
+    // cycles. This is just a very short-term hack.
+    for (auto& impl_constraint : impl_constraints_) {
+      bool performed_rewrite;
+      do {
+        performed_rewrite = false;
+        if (auto* assoc = dyn_cast<AssociatedConstant>(impl_constraint.type);
+            assoc && ValueEqual(&assoc->base(), GetSelfType(), std::nullopt)) {
+          for (const auto& rewrite : rewrite_constraints_) {
+            if (&assoc->constant() == rewrite.constant &&
+                ValueEqual(&assoc->interface(), rewrite.interface,
+                           std::nullopt)) {
+              impl_constraint.type = &rewrite.replacement->value();
+              performed_rewrite = true;
+            }
+          }
+        }
+      } while (performed_rewrite);
+    }
+
     // Create the new type.
     auto* result = arena_->New<ConstraintType>(
         self_binding_, std::move(impl_constraints_),
-        std::move(equality_constraints_), std::move(lookup_contexts_));
+        std::move(equality_constraints_), std::move(rewrite_constraints_),
+        std::move(lookup_contexts_));
     // Update the impl binding to denote the constraint type itself.
     impl_binding_->set_interface(result);
     return result;
@@ -1094,6 +1306,7 @@ class ConstraintTypeBuilder {
   Nonnull<ImplBinding*> impl_binding_;
   std::vector<ConstraintType::ImplConstraint> impl_constraints_;
   std::vector<ConstraintType::EqualityConstraint> equality_constraints_;
+  std::vector<ConstraintType::RewriteConstraint> rewrite_constraints_;
   std::vector<ConstraintType::LookupContext> lookup_contexts_;
 };
 
@@ -1159,6 +1372,12 @@ class TypeChecker::SubstitutedGenericBindings {
 auto TypeChecker::Substitute(const Bindings& bindings,
                              Nonnull<const Value*> type) const
     -> Nonnull<const Value*> {
+  // Don't waste time recursively rebuilding a type if we have nothing to
+  // substitute.
+  if (bindings.empty()) {
+    return type;
+  }
+
   auto SubstituteIntoBindings =
       [&](Nonnull<const Bindings*> inner_bindings) -> Nonnull<const Bindings*> {
     BindingMap values;
@@ -1180,6 +1399,10 @@ auto TypeChecker::Substitute(const Bindings& bindings,
     case Value::Kind::VariableType: {
       auto it = bindings.args().find(&cast<VariableType>(*type).binding());
       if (it == bindings.args().end()) {
+        if (trace_stream_) {
+          **trace_stream_ << "substitution: no value for binding " << *type
+                          << ", leaving alone\n";
+        }
         return type;
       } else {
         return it->second;
@@ -1188,12 +1411,22 @@ auto TypeChecker::Substitute(const Bindings& bindings,
     case Value::Kind::AssociatedConstant: {
       const auto& assoc = cast<AssociatedConstant>(*type);
       Nonnull<const Value*> base = Substitute(bindings, &assoc.base());
-      Nonnull<const Value*> interface =
-          Substitute(bindings, &assoc.interface());
-      Nonnull<const Value*> witness = Substitute(bindings, &assoc.witness());
-      return arena_->New<AssociatedConstant>(
-          base, cast<InterfaceType>(interface), &assoc.constant(),
-          cast<Witness>(witness));
+      const auto* interface =
+          cast<InterfaceType>(Substitute(bindings, &assoc.interface()));
+      // If we're substituting into an associated constant, we may now be able
+      // to rewrite it to a concrete value.
+      if (std::optional<const ValueLiteral*> rewritten_value =
+              LookupRewriteInTypeOf(base, interface, &assoc.constant())) {
+        return &rewritten_value.value()->value();
+      }
+      const auto* witness =
+          cast<Witness>(Substitute(bindings, &assoc.witness()));
+      if (std::optional<const ValueLiteral*> rewritten_value =
+              LookupRewriteInWitness(witness, interface, &assoc.constant())) {
+        return &rewritten_value.value()->value();
+      }
+      return arena_->New<AssociatedConstant>(base, interface, &assoc.constant(),
+                                             witness);
     }
     case Value::Kind::TupleValue: {
       std::vector<Nonnull<const Value*>> elts;
@@ -1259,11 +1492,39 @@ auto TypeChecker::Substitute(const Bindings& bindings,
     }
     case Value::Kind::ConstraintType: {
       const auto& constraint = cast<ConstraintType>(*type);
+      if (auto it = bindings.args().find(constraint.self_binding());
+          it != bindings.args().end()) {
+        // This happens when we substitute into the parameter type of a
+        // function that takes a `T:! Constraint` parameter. In this case we
+        // produce the new type-of-type of the replacement type.
+        Nonnull<const Value*> type_of_type;
+        if (auto* var_type = dyn_cast<VariableType>(it->second)) {
+          type_of_type = &var_type->binding().static_type();
+        } else if (auto* assoc_type =
+                       dyn_cast<AssociatedConstant>(it->second)) {
+          type_of_type = GetTypeForAssociatedConstant(assoc_type);
+        } else {
+          type_of_type = arena_->New<TypeType>();
+        }
+        if (trace_stream_) {
+          **trace_stream_ << "substitution: self of constraint " << constraint
+                          << " is substituted, new type of type is "
+                          << *type_of_type << "\n";
+        }
+        // TODO: Should we keep any part of the old constraint -- rewrites,
+        // equality constraints, etc?
+        return type_of_type;
+      }
       ConstraintTypeBuilder builder(arena_,
                                     constraint.self_binding()->source_loc());
-      builder.AddAndSubstitute(*this, &constraint, builder.GetSelfType(),
-                               builder.GetSelfWitness(), bindings,
-                               /*add_lookup_contexts=*/true);
+      ErrorOr<Success> result =
+          builder.AddAndSubstitute(*this, &constraint, builder.GetSelfType(),
+                                   builder.GetSelfWitness(), bindings,
+                                   /*add_lookup_contexts=*/true);
+      // TODO: This appears to theoretically be possible, and should be handled
+      // better.
+      CARBON_CHECK(result.ok()) << "substitution into " << constraint
+                                << " failed: " << result.error();
       Nonnull<const ConstraintType*> new_constraint =
           std::move(builder).Build(arena_);
       if (trace_stream_) {
@@ -1281,6 +1542,10 @@ auto TypeChecker::Substitute(const Bindings& bindings,
       auto it =
           bindings.witnesses().find(cast<BindingWitness>(*type).binding());
       if (it == bindings.witnesses().end()) {
+        if (trace_stream_) {
+          **trace_stream_ << "substitution: no value for binding " << *type
+                          << ", leaving alone\n";
+        }
         return type;
       } else {
         return it->second;
@@ -1353,6 +1618,14 @@ auto TypeChecker::MatchImpl(const InterfaceType& iface,
                             const ImplScope& impl_scope,
                             SourceLocation source_loc) const
     -> std::optional<Nonnull<const Witness*>> {
+  // Avoid cluttering the trace output with matches that could obviously never
+  // have worked.
+  // TODO: Eventually, ImplScope should filter by type structure before calling
+  // into here.
+  if (impl.interface->declaration().name() != iface.declaration().name()) {
+    return std::nullopt;
+  }
+
   if (trace_stream_) {
     **trace_stream_ << "MatchImpl: looking for " << *impl_type << " as "
                     << iface << "\n";
@@ -1360,11 +1633,10 @@ auto TypeChecker::MatchImpl(const InterfaceType& iface,
                     << *impl.interface << "\n";
   }
 
-  BindingMap deduced_args;
-
-  if (ErrorOr<Success> e = ArgumentDeduction(
-          source_loc, "match", impl.deduced, deduced_args, impl.type, impl_type,
-          /*allow_implicit_conversion=*/false, impl_scope);
+  ArgumentDeduction deduction(source_loc, "match", impl.deduced, trace_stream_);
+  if (ErrorOr<Success> e =
+          deduction.Deduce(impl.type, impl_type,
+                           /*allow_implicit_conversion=*/false);
       !e.ok()) {
     if (trace_stream_) {
       **trace_stream_ << "type does not match: " << e.error() << "\n";
@@ -1372,9 +1644,8 @@ auto TypeChecker::MatchImpl(const InterfaceType& iface,
     return std::nullopt;
   }
 
-  if (ErrorOr<Success> e = ArgumentDeduction(
-          source_loc, "match", impl.deduced, deduced_args, impl.interface,
-          &iface, /*allow_implicit_conversion=*/false, impl_scope);
+  if (ErrorOr<Success> e = deduction.Deduce(
+          impl.interface, &iface, /*allow_implicit_conversion=*/false);
       !e.ok()) {
     if (trace_stream_) {
       **trace_stream_ << "interface does not match: " << e.error() << "\n";
@@ -1382,43 +1653,21 @@ auto TypeChecker::MatchImpl(const InterfaceType& iface,
     return std::nullopt;
   }
 
-  if (trace_stream_) {
-    **trace_stream_ << "match results: {";
-    llvm::ListSeparator sep;
-    for (const auto& [binding, val] : deduced_args) {
-      **trace_stream_ << sep << *binding << " = " << *val;
-    }
-    **trace_stream_ << "}\n";
-  }
-
-  CARBON_CHECK(impl.deduced.size() == deduced_args.size())
-      << "failed to deduce all expected deduced arguments";
-
-  // Ensure the constraints on the `impl` are satisfied by the deduced
-  // arguments.
-  ImplWitnessMap impls;
-  if (ErrorOr<Success> e = SatisfyImpls(impl.impl_bindings, impl_scope,
-                                        source_loc, deduced_args, impls);
-      !e.ok()) {
+  if (ErrorOr<Bindings> bindings_or_error =
+          deduction.Finish(const_cast<TypeChecker&>(*this), impl_scope);
+      !bindings_or_error.ok()) {
     if (trace_stream_) {
-      **trace_stream_ << "missing required impl: " << e.error() << "\n";
+      **trace_stream_ << "impl does not match: " << bindings_or_error.error()
+                      << "\n";
     }
     return std::nullopt;
+  } else {
+    if (trace_stream_) {
+      **trace_stream_ << "matched with " << *impl.type << " as "
+                      << *impl.interface << "\n\n";
+    }
+    return cast<Witness>(Substitute(*bindings_or_error, impl.witness));
   }
-
-  if (trace_stream_) {
-    **trace_stream_ << "matched with " << *impl.type << " as "
-                    << *impl.interface << "\n\n";
-  }
-  if (deduced_args.empty()) {
-    return impl.witness;
-  }
-
-  // Only ImplWitnesses can be parameterized.
-  const ImplWitness* impl_witness = cast<ImplWitness>(impl.witness);
-  return arena_->New<ImplWitness>(
-      &impl_witness->declaration(),
-      arena_->New<Bindings>(std::move(deduced_args), std::move(impls)));
 }
 
 auto TypeChecker::MakeConstraintWitness(
@@ -1434,47 +1683,37 @@ auto TypeChecker::MakeConstraintWitnessAccess(Nonnull<const Witness*> witness,
   return ConstraintImplWitness::Make(arena_, witness, impl_offset);
 }
 
-auto TypeChecker::SatisfyImpls(
-    llvm::ArrayRef<Nonnull<const ImplBinding*>> impl_bindings,
-    const ImplScope& impl_scope, SourceLocation source_loc,
-    const BindingMap& deduced_type_args, ImplWitnessMap& impls) const
-    -> ErrorOr<Success> {
-  for (Nonnull<const ImplBinding*> impl_binding : impl_bindings) {
-    // TODO: Presumably we will need to accumuate witnesses as we go.
-    Bindings bindings(deduced_type_args, Bindings::NoWitnesses);
-    Nonnull<const Value*> interface =
-        Substitute(bindings, impl_binding->interface());
-    CARBON_CHECK(deduced_type_args.find(impl_binding->type_var()) !=
-                 deduced_type_args.end());
-    CARBON_ASSIGN_OR_RETURN(
-        Nonnull<const Value*> impl,
-        impl_scope.Resolve(interface,
-                           deduced_type_args.at(impl_binding->type_var()),
-                           source_loc, *this));
-    impls.insert({impl_binding, impl});
-  }
-  return Success();
-}
-
 auto TypeChecker::MakeConstraintForInterface(
     SourceLocation source_loc, Nonnull<const InterfaceType*> iface_type)
-    -> Nonnull<const ConstraintType*> {
+    -> ErrorOr<Nonnull<const ConstraintType*>> {
+  auto constraint_type = iface_type->declaration().constraint_type();
+  if (!constraint_type) {
+    return ProgramError(source_loc)
+           << "use of " << *iface_type << " before it is completely defined";
+  }
+
+  if (iface_type->bindings().empty()) {
+    return *constraint_type;
+  }
+
   ConstraintTypeBuilder builder(arena_, source_loc);
-  builder.AddImplConstraint(
-      {.type = builder.GetSelfType(), .interface = iface_type});
-  builder.AddLookupContext({.context = iface_type});
+  CARBON_RETURN_IF_ERROR(
+      builder.AddAndSubstitute(*this, *constraint_type, builder.GetSelfType(),
+                               builder.GetSelfWitness(), iface_type->bindings(),
+                               /*add_lookup_contexts=*/true));
   return std::move(builder).Build(arena_);
 }
 
 auto TypeChecker::CombineConstraints(
     SourceLocation source_loc,
     llvm::ArrayRef<Nonnull<const ConstraintType*>> constraints)
-    -> Nonnull<const ConstraintType*> {
+    -> ErrorOr<Nonnull<const ConstraintType*>> {
   ConstraintTypeBuilder builder(arena_, source_loc);
   for (Nonnull<const ConstraintType*> constraint : constraints) {
-    builder.AddAndSubstitute(*this, constraint, builder.GetSelfType(),
-                             builder.GetSelfWitness(), Bindings(),
-                             /*add_lookup_contexts=*/true);
+    CARBON_RETURN_IF_ERROR(
+        builder.AddAndSubstitute(*this, constraint, builder.GetSelfType(),
+                                 builder.GetSelfWitness(), Bindings(),
+                                 /*add_lookup_contexts=*/true));
   }
   return std::move(builder).Build(arena_);
 }
@@ -1487,73 +1726,47 @@ auto TypeChecker::DeduceCallBindings(
     const ImplScope& impl_scope) -> ErrorOr<Success> {
   llvm::ArrayRef<Nonnull<const Value*>> params =
       cast<TupleValue>(*params_type).elements();
-  llvm::ArrayRef<Nonnull<const Expression*>> args =
+  llvm::ArrayRef<Nonnull<Expression*>> args =
       cast<TupleLiteral>(call.argument()).fields();
   if (params.size() != args.size()) {
     return ProgramError(call.source_loc())
            << "wrong number of arguments in function call, expected "
            << params.size() << " but got " << args.size();
   }
-  // Bindings for deduced parameters and generic parameters.
-  BindingMap generic_bindings;
+
+  // Deductions performed for deduced parameters and generic parameters.
+  ArgumentDeduction deduction(call.source_loc(), "call", deduced_bindings,
+                              trace_stream_);
 
   // Deduce and/or convert each argument to the corresponding
   // parameter.
   for (size_t i = 0; i < params.size(); ++i) {
     const Value* param = params[i];
-    const Expression* arg = args[i];
-    CARBON_RETURN_IF_ERROR(
-        ArgumentDeduction(arg->source_loc(), "call", deduced_bindings,
-                          generic_bindings, param, &arg->static_type(),
-                          /*allow_implicit_conversion=*/true, impl_scope));
-    // If the parameter is a `:!` binding, evaluate and collect its
-    // value for use in later parameters and in the function body.
+    Expression* arg = args[i];
     if (!generic_params.empty() && generic_params.front().index == i) {
-      CARBON_ASSIGN_OR_RETURN(Nonnull<const Value*> arg_value,
-                              InterpExp(arg, arena_, trace_stream_));
-      if (trace_stream_) {
-        **trace_stream_ << "evaluated generic parameter "
-                        << *generic_params.front().binding << " as "
-                        << *arg_value << "\n";
-      }
-      bool newly_added =
-          generic_bindings.insert({generic_params.front().binding, arg_value})
-              .second;
-      CARBON_CHECK(newly_added) << "generic parameter should not be deduced";
+      // The parameter is a `:!` binding. Collect its argument so we can
+      // evaluate it when we're done with deduction.
+      deduction.AddNonDeducedBindingValue(generic_params.front().binding, arg);
       generic_params = generic_params.drop_front();
+    } else {
+      // Otherwise deduce its type from the corresponding argument.
+      CARBON_RETURN_IF_ERROR(
+          deduction.Deduce(param, &arg->static_type(),
+                           /*allow_implicit_conversion=*/true));
     }
   }
   CARBON_CHECK(generic_params.empty())
       << "did not find all generic parameters in parameter list";
 
-  for (Nonnull<const GenericBinding*> deduced_param : deduced_bindings) {
-    // TODO: change the following to a CHECK once the real checking
-    // has been added to the type checking of function signatures.
-    if (auto it = generic_bindings.find(deduced_param);
-        it == generic_bindings.end()) {
-      return ProgramError(call.source_loc())
-             << "could not deduce type argument for type parameter "
-             << deduced_param->name() << "\n"
-             << "in " << call;
-    }
-  }
-
-  // Find impls for all the required impl bindings.
-  ImplWitnessMap impls;
-  CARBON_RETURN_IF_ERROR(SatisfyImpls(
-      impl_bindings, impl_scope, call.source_loc(), generic_bindings, impls));
-  call.set_bindings(Bindings(std::move(generic_bindings), std::move(impls)));
-
-  // TODO: Ensure any equality constraints are satisfied.
-
-  // Convert the arguments to the parameter type.
-  Nonnull<const Value*> param_type = Substitute(call.bindings(), params_type);
+  CARBON_ASSIGN_OR_RETURN(Bindings bindings,
+                          deduction.Finish(*this, impl_scope));
+  call.set_bindings(std::move(bindings));
 
   // Convert the arguments to the deduced and substituted parameter type.
+  Nonnull<const Value*> param_type = Substitute(call.bindings(), params_type);
   CARBON_ASSIGN_OR_RETURN(
       Nonnull<Expression*> converted_argument,
       ImplicitlyConvert("call", impl_scope, &call.argument(), param_type));
-
   call.set_argument(converted_argument);
 
   return Success();
@@ -1577,6 +1790,7 @@ static auto LookupInConstraint(SourceLocation source_loc,
   if (const auto* iface_type = dyn_cast<InterfaceType>(type)) {
     // For an interface, look into that interface alone.
     // TODO: Also look into any interfaces extended by it.
+    // TODO: Maybe just convert to a constraint type to reduce duplication?
     interface_context[0].context = iface_type;
     lookup_contexts = interface_context;
   } else if (const auto* constraint_type = dyn_cast<ConstraintType>(type)) {
@@ -1619,9 +1833,95 @@ static auto LookupInConstraint(SourceLocation source_loc,
     return ProgramError(source_loc)
            << lookup_kind << ", " << member_name << " not in " << *type;
   }
+
   return found.value();
 }
 
+// Look for a rewrite to use when naming the given interface member in a type
+// declared with the given type-of-type.
+static auto LookupRewrite(Nonnull<const Value*> type_of_type,
+                          Nonnull<const InterfaceType*> interface,
+                          Nonnull<const Declaration*> member)
+    -> std::optional<const ValueLiteral*> {
+  if (!isa<AssociatedConstantDeclaration>(member)) {
+    return std::nullopt;
+  }
+
+  // Find the set of rewrites. Only ConstraintTypes have rewrites.
+  llvm::ArrayRef<ConstraintType::RewriteConstraint> rewrites;
+  if (const auto* constraint_type = dyn_cast<ConstraintType>(type_of_type)) {
+    rewrites = constraint_type->rewrite_constraints();
+  }
+
+  for (ConstraintType::RewriteConstraint rewrite : rewrites) {
+    if (ValueEqual(interface, rewrite.interface, std::nullopt) &&
+        // TODO: Using name comparison here seems brittle.
+        GetName(*member) == GetName(*rewrite.constant)) {
+      // A ConstraintType can only have one rewrite per (interface, member)
+      // pair, so we don't need to check the rest.
+      return rewrite.replacement;
+    }
+  }
+
+  return std::nullopt;
+}
+
+auto TypeChecker::GetTypeForAssociatedConstant(
+    Nonnull<const AssociatedConstant*> assoc) const -> Nonnull<const Value*> {
+  auto* assoc_type = &assoc->constant().static_type();
+  Bindings bindings = assoc->interface().bindings();
+  bindings.Add(assoc->interface().declaration().self(), &assoc->base(),
+               &assoc->witness());
+  return Substitute(bindings, assoc_type);
+}
+
+auto TypeChecker::LookupRewriteInTypeOf(
+    Nonnull<const Value*> type, Nonnull<const InterfaceType*> interface,
+    Nonnull<const Declaration*> member) const
+    -> std::optional<const ValueLiteral*> {
+  // Given `(T:! C).Y`, look in `C` for rewrites.
+  if (auto* var_type = dyn_cast<VariableType>(type)) {
+    if (!var_type->binding().has_static_type()) {
+      // We looked for a rewrite before we finished type-checking the generic
+      // binding. This happens when forming the type of a generic binding. Just
+      // say there are no rewrites yet.
+      return std::nullopt;
+    }
+    return LookupRewrite(&var_type->binding().static_type(), interface, member);
+  }
+
+  // Given `(T.U).Y` for an associated type `U`, substitute into the type of
+  // `U` to find rewrites.
+  // TODO: This substitution can lead to infinite recursion.
+  if (auto* assoc_const = dyn_cast<AssociatedConstant>(type)) {
+    return LookupRewrite(GetTypeForAssociatedConstant(assoc_const), interface,
+                         member);
+  }
+
+  return std::nullopt;
+}
+
+auto TypeChecker::LookupRewriteInWitness(
+    Nonnull<const Witness*> witness, Nonnull<const InterfaceType*> interface,
+    Nonnull<const Declaration*> member) const
+    -> std::optional<const ValueLiteral*> {
+  if (auto* impl_witness = dyn_cast<ImplWitness>(witness)) {
+    Nonnull<const Value*> constraint =
+        Substitute(impl_witness->bindings(),
+                   impl_witness->declaration().constraint_type());
+    return LookupRewrite(constraint, interface, member);
+  }
+  return std::nullopt;
+}
+
+// Rewrites a member access expression to produce the given constant value.
+static void RewriteMemberAccess(Nonnull<MemberAccessExpression*> access,
+                                Nonnull<const ValueLiteral*> value) {
+  access->set_static_type(&value->static_type());
+  access->set_value_category(value->value_category());
+  access->set_constant_value(&value->value());
+}
+
 // Determine whether the given member declaration declares an instance member.
 static auto IsInstanceMember(Member member) {
   if (!member.declaration()) {
@@ -1804,26 +2104,44 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
                    << " does not have a field named " << access.member_name();
           }
         }
-        case Value::Kind::VariableType: {
-          // This case handles access to a method on a receiver whose type
-          // is a type variable. For example, `x.foo` where the type of
-          // `x` is `T` and `foo` and `T` implements an interface that
-          // includes `foo`.
-          const Value& typeof_var =
-              cast<VariableType>(object_type).binding().static_type();
+        case Value::Kind::VariableType:
+        case Value::Kind::AssociatedConstant: {
+          // This case handles access to a method on a receiver whose type is a
+          // type variable or associated constant. For example, `x.foo` where
+          // the type of `x` is `T` and `T` implements an interface that
+          // includes `foo`, or `x.y().foo` where the type of `x` is `T` and
+          // the return type of `y()` is an associated constant from `T`'s
+          // constraint.
+          Nonnull<const Value*> constraint;
+          if (auto* var_type = dyn_cast<VariableType>(&object_type)) {
+            constraint = &var_type->binding().static_type();
+          } else {
+            constraint = GetTypeForAssociatedConstant(
+                cast<AssociatedConstant>(&object_type));
+          }
           CARBON_ASSIGN_OR_RETURN(
               ConstraintLookupResult result,
-              LookupInConstraint(e->source_loc(), "member access", &typeof_var,
+              LookupInConstraint(e->source_loc(), "member access", constraint,
                                  access.member_name()));
+          if (auto replacement =
+                  LookupRewrite(constraint, result.interface, result.member)) {
+            RewriteMemberAccess(&access, *replacement);
+            return Success();
+          }
           // Compute a witness that the variable type implements this
           // interface. This will typically be either a reference to its
           // `ImplBinding` or, for a constraint, to a witness for an impl
           // constraint within it.
           // TODO: We should only need to look at the impl binding for this
-          // variable, not everything in the impl scope, to find the witness.
+          // variable or witness for this associated constant, not everything in
+          // the impl scope, to find the witness.
+          CARBON_ASSIGN_OR_RETURN(
+              Nonnull<const ConstraintType*> iface_constraint,
+              MakeConstraintForInterface(access.source_loc(),
+                                         result.interface));
           CARBON_ASSIGN_OR_RETURN(
               Nonnull<const Witness*> witness,
-              impl_scope.Resolve(result.interface, &object_type,
+              impl_scope.Resolve(iface_constraint, &object_type,
                                  e->source_loc(), *this));
 
           Bindings bindings = result.interface->bindings();
@@ -1838,6 +2156,9 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
           access.set_is_type_access(!IsInstanceMember(access.member()));
           access.set_static_type(inst_member_type);
 
+          // TODO: This is just a ConstraintImplWitness into the
+          // iface_constraint. If we can compute the right index, we can avoid
+          // re-resolving it.
           CARBON_ASSIGN_OR_RETURN(
               Nonnull<const Witness*> impl,
               impl_scope.Resolve(result.interface, &object_type,
@@ -1862,6 +2183,18 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
               ConstraintLookupResult result,
               LookupInConstraint(e->source_loc(), "member access", &object_type,
                                  access.member_name()));
+          if (auto replacement = LookupRewrite(&object_type, result.interface,
+                                               result.member)) {
+            RewriteMemberAccess(&access, *replacement);
+            return Success();
+          }
+          CARBON_ASSIGN_OR_RETURN(
+              Nonnull<const ConstraintType*> iface_constraint,
+              MakeConstraintForInterface(access.source_loc(),
+                                         result.interface));
+          CARBON_ASSIGN_OR_RETURN(Nonnull<const Witness*> witness,
+                                  impl_scope.Resolve(iface_constraint, type,
+                                                     e->source_loc(), *this));
           CARBON_ASSIGN_OR_RETURN(Nonnull<const Witness*> impl,
                                   impl_scope.Resolve(result.interface, type,
                                                      e->source_loc(), *this));
@@ -1883,7 +2216,7 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
             // associated constant.
             const Value& member_type = result.member->static_type();
             Bindings bindings = result.interface->bindings();
-            bindings.Add(result.interface->declaration().self(), type, impl);
+            bindings.Add(result.interface->declaration().self(), type, witness);
             Nonnull<const Value*> inst_member_type =
                 Substitute(bindings, &member_type);
             access.set_static_type(inst_member_type);
@@ -1990,6 +2323,8 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
               return Success();
             }
             default:
+              // TODO: We should handle VariableType and AssociatedConstant
+              // here.
               return ProgramError(access.source_loc())
                      << "unsupported member access into type " << *type;
           }
@@ -2044,12 +2379,33 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
       }
       access.set_is_type_access(has_instance && !is_instance_member);
 
-      // Perform impl selection if necessary.
-      if (std::optional<Nonnull<const Value*>> iface =
+      // Perform associated constant rewriting and impl selection if necessary.
+      std::optional<Nonnull<const Witness*>> witness;
+      if (std::optional<Nonnull<const InterfaceType*>> iface =
               member_name.interface()) {
+        // If we're naming an associated constant, we might have a rewrite for
+        // it that we can apply immediately.
+        if (auto replacement = LookupRewriteInTypeOf(
+                *base_type, *iface, *member_name.member().declaration())) {
+          RewriteMemberAccess(&access, *replacement);
+          return Success();
+        }
+
+        CARBON_ASSIGN_OR_RETURN(
+            Nonnull<const ConstraintType*> iface_constraint,
+            MakeConstraintForInterface(access.source_loc(), *iface));
+        CARBON_ASSIGN_OR_RETURN(witness,
+                                impl_scope.Resolve(iface_constraint, *base_type,
+                                                   e->source_loc(), *this));
         CARBON_ASSIGN_OR_RETURN(
             Nonnull<const Witness*> impl,
             impl_scope.Resolve(*iface, *base_type, e->source_loc(), *this));
+        if (std::optional<Nonnull<const ValueLiteral*>> replacement =
+                LookupRewriteInWitness(impl, *iface,
+                                       *member_name.member().declaration())) {
+          RewriteMemberAccess(&access, *replacement);
+          return Success();
+        }
         access.set_impl(impl);
       }
 
@@ -2058,8 +2414,7 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
         if (member_name.interface()) {
           Nonnull<const InterfaceType*> iface_type = *member_name.interface();
           Bindings bindings = iface_type->bindings();
-          bindings.Add(iface_type->declaration().self(), *base_type,
-                       access.impl());
+          bindings.Add(iface_type->declaration().self(), *base_type, witness);
           return Substitute(bindings, member_type);
         }
         if (auto* class_type = dyn_cast<NominalClassType>(base_type.value())) {
@@ -2241,8 +2596,10 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
             for (int i : {0, 1}) {
               if (auto* iface_type_type =
                       dyn_cast<TypeOfInterfaceType>(ts[i])) {
-                constraints[i] = MakeConstraintForInterface(
-                    e->source_loc(), &iface_type_type->interface_type());
+                CARBON_ASSIGN_OR_RETURN(
+                    constraints[i],
+                    MakeConstraintForInterface(
+                        e->source_loc(), &iface_type_type->interface_type()));
               } else if (auto* constraint_type_type =
                              dyn_cast<TypeOfConstraintType>(ts[i])) {
                 constraints[i] = &constraint_type_type->constraint_type();
@@ -2252,9 +2609,11 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
                        << " should be a constraint, found `" << *ts[i] << "`";
               }
             }
-            op.set_static_type(
-                arena_->New<TypeOfConstraintType>(CombineConstraints(
-                    e->source_loc(), {*constraints[0], *constraints[1]})));
+            CARBON_ASSIGN_OR_RETURN(
+                Nonnull<const ConstraintType*> result,
+                CombineConstraints(e->source_loc(),
+                                   {*constraints[0], *constraints[1]}));
+            op.set_static_type(arena_->New<TypeOfConstraintType>(result));
             op.set_value_category(ValueCategory::Let);
             return Success();
           }
@@ -2679,7 +3038,8 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
       if (auto* constraint_type = dyn_cast<ConstraintType>(base_type)) {
         base = constraint_type;
       } else if (auto* interface_type = dyn_cast<InterfaceType>(base_type)) {
-        base = MakeConstraintForInterface(e->source_loc(), interface_type);
+        CARBON_ASSIGN_OR_RETURN(
+            base, MakeConstraintForInterface(e->source_loc(), interface_type));
       } else if (isa<TypeType>(base_type)) {
         // Start with an unconstrained type.
       } else {
@@ -2691,9 +3051,10 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
       // Start with the given constraint, if any.
       ConstraintTypeBuilder builder(arena_, &self);
       if (base) {
-        builder.AddAndSubstitute(*this, *base, builder.GetSelfType(),
-                                 builder.GetSelfWitness(), Bindings(),
-                                 /*add_lookup_contexts=*/true);
+        CARBON_RETURN_IF_ERROR(
+            builder.AddAndSubstitute(*this, *base, builder.GetSelfType(),
+                                     builder.GetSelfWitness(), Bindings(),
+                                     /*add_lookup_contexts=*/true));
         // Constraints from the LHS of `where` are in scope in the RHS. But
         // constraints from earlier `where` clauses are not in scope in later
         // clauses.
@@ -2721,9 +3082,10 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
               // Transform `where .B is (C where .D is E)` into
               // `where .B is C and .B.D is E` then add all the resulting
               // constraints.
-              builder.AddAndSubstitute(*this, constraint_type, type,
-                                       builder.GetSelfWitness(), Bindings(),
-                                       /*add_lookup_contexts=*/false);
+              CARBON_RETURN_IF_ERROR(
+                  builder.AddAndSubstitute(*this, constraint_type, type,
+                                           builder.GetSelfWitness(), Bindings(),
+                                           /*add_lookup_contexts=*/false));
             } else {
               return ProgramError(is_clause.constraint().source_loc())
                      << "expression after `is` does not resolve to a "
@@ -2746,6 +3108,45 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
             }
             break;
           }
+          case WhereClauseKind::RewriteWhereClause: {
+            const auto& rewrite_clause = cast<RewriteWhereClause>(*clause);
+            CARBON_ASSIGN_OR_RETURN(
+                ConstraintLookupResult result,
+                LookupInConstraint(clause->source_loc(),
+                                   "rewrite constraint lookup", base_type,
+                                   rewrite_clause.member_name()));
+            const auto* constant =
+                dyn_cast<AssociatedConstantDeclaration>(result.member);
+            if (!constant) {
+              return ProgramError(clause->source_loc())
+                     << "in rewrite constraint lookup, `"
+                     << rewrite_clause.member_name()
+                     << "` does not name an associated constant";
+            }
+            // TODO: Decide what type constraints we want to impose on the
+            // replacement. Given
+            //
+            //   interface A {
+            //     let N:! i32;
+            //   }
+            //   fn F[T:! A where .N = (i32, i32)]() {}
+            //
+            // ... no call can ever succeed. Should we reject? We want to
+            // preserve the type of the replacement in the case where it is a
+            // constraint type containing further rewrites.
+            CARBON_ASSIGN_OR_RETURN(Nonnull<const Value*> replacement_value,
+                                    InterpExp(&rewrite_clause.replacement(),
+                                              arena_, trace_stream_));
+            auto* replacement = arena_->New<ValueLiteral>(
+                rewrite_clause.source_loc(), replacement_value,
+                &rewrite_clause.replacement().static_type(),
+                ValueCategory::Let);
+            CARBON_RETURN_IF_ERROR(builder.AddRewriteConstraint(
+                rewrite_clause.source_loc(), {.interface = result.interface,
+                                              .constant = constant,
+                                              .replacement = replacement}));
+            break;
+          }
         }
       }
 
@@ -2878,6 +3279,12 @@ auto TypeChecker::TypeCheckWhereClause(Nonnull<WhereClause*> clause,
       }
       return Success();
     }
+    case WhereClauseKind::RewriteWhereClause: {
+      auto& rewrite_clause = cast<RewriteWhereClause>(*clause);
+      CARBON_RETURN_IF_ERROR(
+          TypeCheckExp(&rewrite_clause.replacement(), impl_scope));
+      return Success();
+    }
   }
 }
 
@@ -2959,7 +3366,11 @@ auto TypeChecker::TypeCheckPattern(
       SetValue(&binding, val);
 
       // Create an impl binding if we have a constraint.
-      if (isa<InterfaceType, ConstraintType>(type)) {
+      if (auto* iface_type = dyn_cast<InterfaceType>(type)) {
+        CARBON_ASSIGN_OR_RETURN(
+            type, MakeConstraintForInterface(binding.source_loc(), iface_type));
+      }
+      if (auto* constraint = dyn_cast<ConstraintType>(type)) {
         Nonnull<ImplBinding*> impl_binding = arena_->New<ImplBinding>(
             binding.source_loc(), &binding, std::nullopt);
         auto* witness = arena_->New<BindingWitness>(impl_binding);
@@ -2969,13 +3380,11 @@ auto TypeChecker::TypeCheckPattern(
         // Substitute the VariableType as `.Self` of the constraint to form the
         // resolved type of the binding. Eg, `T:! X where .Self is Y` resolves
         // to `T:! <constraint T is X and T is Y>`.
-        if (auto* constraint = dyn_cast<ConstraintType>(type)) {
-          ConstraintTypeBuilder builder(arena_, binding.source_loc());
-          builder.AddAndSubstitute(*this, constraint, val, witness, Bindings(),
-                                   /*add_lookup_contexts=*/true);
-          type = std::move(builder).Build(arena_);
-        }
-        impl_binding->set_interface(type);
+        ConstraintTypeBuilder builder(arena_, &binding, impl_binding);
+        CARBON_RETURN_IF_ERROR(builder.AddAndSubstitute(
+            *this, constraint, val, witness, Bindings(),
+            /*add_lookup_contexts=*/true));
+        type = std::move(builder).Build(arena_);
 
         BringImplIntoScope(impl_binding, impl_scope);
       }
@@ -3787,21 +4196,51 @@ auto TypeChecker::DeclareInterfaceDeclaration(
   self_type->set_static_type(arena_->New<TypeType>());
   self_type->set_constant_value(iface_type);
 
-  // Process the Self parameter.
-  CARBON_RETURN_IF_ERROR(TypeCheckPattern(iface_decl->self(), std::nullopt,
-                                          iface_scope, ValueCategory::Let));
-  auto* self_witness = cast<Witness>(
-      iface_decl->self()->impl_binding().value()->symbolic_identity().value());
+  // Build a constraint corresponding to this interface.
+  ConstraintTypeBuilder builder(arena_, iface_decl->self());
+  iface_decl->self()->set_static_type(iface_type);
+
+  // The impl constraint says only that the direct members of the interface are
+  // available. For any indirect constraints, we need to add separate entries
+  // to the constraint type. This ensures that all indirect constraints are
+  // lifted to the top level so they can be accessed directly and resolved
+  // independently if necessary.
+  int index = builder.AddImplConstraint(
+      {.type = builder.GetSelfType(), .interface = iface_type});
+  builder.AddLookupContext({.context = iface_type});
+  auto* impl_witness =
+      MakeConstraintWitnessAccess(builder.GetSelfWitness(), index);
 
   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)) {
-      assoc->binding().set_symbolic_identity(arena_->New<AssociatedConstant>(
-          &iface_decl->self()->value(), iface_type, assoc, self_witness));
+      auto* assoc_value = arena_->New<AssociatedConstant>(
+          &iface_decl->self()->value(), iface_type, assoc, impl_witness);
+      assoc->binding().set_symbolic_identity(assoc_value);
+
+      // The type specified for the associated constant becomes a constraint
+      // for the interface: `let X:! Interface` adds a `Self.X is Interface`
+      // constraint that `impl`s must satisfy and users of the interface can
+      // rely on.
+      Nonnull<const Value*> constraint = &assoc->static_type();
+      if (auto* interface_type = dyn_cast<InterfaceType>(constraint)) {
+        CARBON_ASSIGN_OR_RETURN(
+            constraint,
+            MakeConstraintForInterface(assoc->source_loc(), interface_type));
+      }
+      if (auto* constraint_type = dyn_cast<ConstraintType>(constraint)) {
+        CARBON_RETURN_IF_ERROR(
+            builder.AddAndSubstitute(*this, constraint_type, assoc_value,
+                                     builder.GetSelfWitness(), Bindings(),
+                                     /*add_lookup_contexts=*/false));
+      }
     }
   }
+
+  iface_decl->set_constraint_type(std::move(builder).Build(arena_));
+
   if (trace_stream_) {
     **trace_stream_ << "** finished declaring interface " << iface_decl->name()
                     << "\n";
@@ -3838,21 +4277,16 @@ auto TypeChecker::CheckImplIsDeducible(
     Nonnull<const InterfaceType*> impl_iface,
     llvm::ArrayRef<Nonnull<const GenericBinding*>> deduced_bindings,
     const ImplScope& impl_scope) -> ErrorOr<Success> {
-  BindingMap deduced_args;
-  CARBON_RETURN_IF_ERROR(ArgumentDeduction(
-      source_loc, "impl", deduced_bindings, deduced_args, impl_type, impl_type,
-      /*allow_implicit_conversion=*/false, impl_scope));
-  CARBON_RETURN_IF_ERROR(ArgumentDeduction(source_loc, "impl", deduced_bindings,
-                                           deduced_args, impl_iface, impl_iface,
-                                           /*allow_implicit_conversion=*/false,
-                                           impl_scope));
-  for (auto* expected_deduced : deduced_bindings) {
-    if (!deduced_args.count(expected_deduced)) {
-      return ProgramError(source_loc)
-             << "parameter `" << *expected_deduced
-             << "` is not deducible from `impl " << *impl_type << " as "
-             << *impl_iface << "`";
-    }
+  ArgumentDeduction deduction(source_loc, "impl", deduced_bindings,
+                              trace_stream_);
+  CARBON_RETURN_IF_ERROR(deduction.Deduce(impl_type, impl_type,
+                                          /*allow_implicit_conversion=*/false));
+  CARBON_RETURN_IF_ERROR(deduction.Deduce(impl_iface, impl_iface,
+                                          /*allow_implicit_conversion=*/false));
+  if (auto not_deduced = deduction.FindUndeducedBinding()) {
+    return ProgramError(source_loc)
+           << "parameter `" << **not_deduced << "` is not deducible from `impl "
+           << *impl_type << " as " << *impl_iface << "`";
   }
   return Success();
 }
@@ -3861,12 +4295,19 @@ auto TypeChecker::CheckImplIsComplete(Nonnull<const InterfaceType*> iface_type,
                                       Nonnull<const ImplDeclaration*> impl_decl,
                                       Nonnull<const Value*> self_type,
                                       Nonnull<const Witness*> self_witness,
+                                      Nonnull<const Witness*> iface_witness,
                                       const ImplScope& impl_scope)
     -> ErrorOr<Success> {
   const auto& iface_decl = iface_type->declaration();
   for (Nonnull<Declaration*> m : iface_decl.members()) {
     if (auto* assoc = dyn_cast<AssociatedConstantDeclaration>(m)) {
       // An associated constant must be given exactly one value.
+      if (LookupRewrite(impl_decl->constraint_type(), iface_type, assoc)) {
+        // OK, named by `=` constraint.
+        continue;
+      }
+
+      // TODO: Remove the rest of this and just reject if there's no `=`.
       Nonnull<const Value*> expected = arena_->New<AssociatedConstant>(
           self_type, iface_type, assoc, self_witness);
 
@@ -3918,7 +4359,7 @@ auto TypeChecker::CheckImplIsComplete(Nonnull<const InterfaceType*> iface_type,
       }
 
       Bindings bindings = iface_type->bindings();
-      bindings.Add(iface_decl.self(), self_type, self_witness);
+      bindings.Add(iface_decl.self(), self_type, iface_witness);
       Nonnull<const Value*> iface_mem_type =
           Substitute(bindings, &m->static_type());
       // TODO: How should the signature in the implementation be permitted
@@ -3933,16 +4374,9 @@ auto TypeChecker::CheckImplIsComplete(Nonnull<const InterfaceType*> iface_type,
 
 auto TypeChecker::CheckAndAddImplBindings(
     Nonnull<const ImplDeclaration*> impl_decl, Nonnull<const Value*> impl_type,
-    Nonnull<const Witness*> self_witness, const ScopeInfo& scope_info)
-    -> ErrorOr<Success> {
-  // The deduced bindings are the parameters for all enclosing classes followed
-  // by any deduced parameters written on the `impl` declaration itself.
-  std::vector<Nonnull<const GenericBinding*>> deduced_bindings =
-      scope_info.bindings;
-  deduced_bindings.insert(deduced_bindings.end(),
-                          impl_decl->deduced_parameters().begin(),
-                          impl_decl->deduced_parameters().end());
-
+    Nonnull<const Witness*> self_witness, Nonnull<const Witness*> impl_witness,
+    llvm::ArrayRef<Nonnull<const GenericBinding*>> deduced_bindings,
+    const ScopeInfo& scope_info) -> ErrorOr<Success> {
   // 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.
@@ -3961,8 +4395,27 @@ auto TypeChecker::CheckAndAddImplBindings(
       BringAssociatedConstantsIntoScope(constraint, impl_type, iface_type,
                                         iface_scope);
 
-      CARBON_RETURN_IF_ERROR(CheckImplIsComplete(
-          iface_type, impl_decl, impl_type, self_witness, iface_scope));
+      // Compute a witness that the implementing type implements this interface
+      // by resolving the interface constraint in a context where this `impl`
+      // is used for it. We don't actually want the whole `impl` to be in
+      // scope, though, because it could be partially specialized.
+      Nonnull<const Witness*> iface_witness;
+      {
+        ImplScope impl_scope;
+        impl_scope.AddParent(&iface_scope);
+        impl_scope.Add(impl_decl->constraint_type(), impl_type, impl_witness,
+                       *this);
+        CARBON_ASSIGN_OR_RETURN(
+            Nonnull<const ConstraintType*> iface_constraint,
+            MakeConstraintForInterface(impl_decl->source_loc(), iface_type));
+        CARBON_ASSIGN_OR_RETURN(
+            iface_witness, impl_scope.Resolve(iface_constraint, impl_type,
+                                              impl_decl->source_loc(), *this));
+      }
+
+      CARBON_RETURN_IF_ERROR(CheckImplIsComplete(iface_type, impl_decl,
+                                                 impl_type, self_witness,
+                                                 iface_witness, iface_scope));
 
       // TODO: We should do this either before checking any interface or after
       // checking all of them, so that the order of lookup contexts doesn't
@@ -3988,10 +4441,13 @@ auto TypeChecker::DeclareImplDeclaration(Nonnull<ImplDeclaration*> impl_decl,
   }
   ImplScope impl_scope;
   impl_scope.AddParent(scope_info.innermost_scope);
+  std::vector<Nonnull<const GenericBinding*>> generic_bindings =
+      scope_info.bindings;
   std::vector<Nonnull<const ImplBinding*>> impl_bindings;
 
   // Bring the deduced parameters into scope.
   for (Nonnull<GenericBinding*> deduced : impl_decl->deduced_parameters()) {
+    generic_bindings.push_back(deduced);
     CARBON_RETURN_IF_ERROR(TypeCheckPattern(deduced, std::nullopt, impl_scope,
                                             ValueCategory::Let));
     CollectImplBindingsInPattern(deduced, impl_bindings);
@@ -4007,39 +4463,57 @@ auto TypeChecker::DeclareImplDeclaration(Nonnull<ImplDeclaration*> impl_decl,
   // processing the interface, in case the interface expression uses `Self`.
   Nonnull<SelfDeclaration*> self = impl_decl->self();
   self->set_constant_value(impl_type_value);
-  // Static type set in call to `TypeCheckExp(...)` above.
   self->set_static_type(&impl_decl->impl_type()->static_type());
 
   // Check and interpret the interface.
   CARBON_ASSIGN_OR_RETURN(
-      Nonnull<const Value*> constraint_type,
+      Nonnull<const Value*> implemented_type,
       TypeCheckTypeExp(&impl_decl->interface(), impl_scope));
-  if (auto* iface_type = dyn_cast<InterfaceType>(constraint_type)) {
-    constraint_type = MakeConstraintForInterface(
-        impl_decl->interface().source_loc(), iface_type);
+  if (auto* iface_type = dyn_cast<InterfaceType>(implemented_type)) {
+    CARBON_ASSIGN_OR_RETURN(
+        implemented_type, MakeConstraintForInterface(
+                              impl_decl->interface().source_loc(), iface_type));
   }
-  if (!isa<ConstraintType>(constraint_type)) {
+  if (!isa<ConstraintType>(implemented_type)) {
     return ProgramError(impl_decl->interface().source_loc())
            << "expected constraint after `as`, found value of type "
-           << *constraint_type;
+           << *implemented_type;
   }
 
-  // Build the self-witness. This is the witness used to demonstrate that this
-  // impl implements its constraint.
-  auto* self_witness = arena_->New<ImplWitness>(
-      impl_decl,
-      Bindings::SymbolicIdentity(arena_, impl_decl->deduced_parameters()));
-
   // Substitute the given type for `.Self` to form the resolved constraint that
   // this `impl` implements.
+  Nonnull<const ConstraintType*> constraint_type;
   {
     ConstraintTypeBuilder builder(arena_, impl_decl->source_loc());
-    builder.AddAndSubstitute(*this, cast<ConstraintType>(constraint_type),
-                             impl_type_value, self_witness, Bindings(),
-                             /*add_lookup_contexts=*/true);
-    auto* resolved = std::move(builder).Build(arena_);
-    impl_decl->set_constraint_type(cast<ConstraintType>(resolved));
-    constraint_type = resolved;
+    CARBON_RETURN_IF_ERROR(builder.AddAndSubstitute(
+        *this, cast<ConstraintType>(implemented_type), impl_type_value,
+        builder.GetSelfWitness(), Bindings(),
+        /*add_lookup_contexts=*/true));
+    constraint_type = std::move(builder).Build(arena_);
+    impl_decl->set_constraint_type(constraint_type);
+  }
+
+  // Build the self witness. This is the witness used to demonstrate that
+  // this impl implements its lookup contexts.
+  auto* self_witness = arena_->New<ImplWitness>(
+      impl_decl, Bindings::SymbolicIdentity(arena_, generic_bindings));
+
+  // Compute a witness that the impl implements its constraint.
+  Nonnull<const Witness*> impl_witness;
+  {
+    ImplScope self_impl_scope;
+    self_impl_scope.AddParent(&impl_scope);
+    // For each interface we're going to implement, this impl is the witness
+    // that that interface is implemented.
+    for (auto lookup : constraint_type->lookup_contexts()) {
+      if (auto* iface_type = dyn_cast<InterfaceType>(lookup.context)) {
+        self_impl_scope.Add(iface_type, impl_type_value, self_witness, *this);
+      }
+    }
+    // Ensure that's enough for our interface to be satisfied.
+    CARBON_ASSIGN_OR_RETURN(
+        impl_witness, self_impl_scope.Resolve(constraint_type, impl_type_value,
+                                              impl_decl->source_loc(), *this));
   }
 
   // Declare the impl members.
@@ -4050,14 +4524,8 @@ auto TypeChecker::DeclareImplDeclaration(Nonnull<ImplDeclaration*> impl_decl,
 
   // Create the implied impl bindings.
   CARBON_RETURN_IF_ERROR(CheckAndAddImplBindings(impl_decl, impl_type_value,
-                                                 self_witness, scope_info));
-
-  // Check the constraint is satisfied by the `impl`s we just created. This
-  // serves a couple of purposes:
-  //  - It ensures that any constraints in a `ConstraintType` are met.
-  //  - It rejects `impl`s that immediately introduce ambiguity.
-  CARBON_RETURN_IF_ERROR(impl_scope.Resolve(constraint_type, impl_type_value,
-                                            impl_decl->source_loc(), *this));
+                                                 self_witness, impl_witness,
+                                                 generic_bindings, scope_info));
 
   if (trace_stream_) {
     **trace_stream_ << "** finished declaring impl " << *impl_decl->impl_type()
diff --git a/explorer/interpreter/type_checker.h b/explorer/interpreter/type_checker.h
index 6b8e7868ec0b..e53a87be4c2e 100644
--- a/explorer/interpreter/type_checker.h
+++ b/explorer/interpreter/type_checker.h
@@ -37,24 +37,6 @@ class TypeChecker {
   // processed.
   auto TypeCheck(AST& ast) -> ErrorOr<Success>;
 
-  // Perform type argument deduction, matching the parameter value `param`
-  // against the argument value `arg`. Whenever there is an VariableType in the
-  // parameter, it is deduced to be the corresponding type inside the argument
-  // type. The argument and parameter will typically be types, but can be
-  // non-type values when deduction recurses into the arguments of a
-  // parameterized type.
-  // The `deduced` parameter is an accumulator, that is, it holds the
-  // results so-far.
-  // `allow_implicit_conversion` specifies whether implicit conversions are
-  // permitted from the argument to the parameter type. If so, an `impl_scope`
-  // must be provided.
-  auto ArgumentDeduction(
-      SourceLocation source_loc, const std::string& context,
-      llvm::ArrayRef<Nonnull<const GenericBinding*>> bindings_to_deduce,
-      BindingMap& deduced, Nonnull<const Value*> param,
-      Nonnull<const Value*> arg, bool allow_implicit_conversion,
-      const ImplScope& impl_scope) const -> ErrorOr<Success>;
-
   // Construct a type that is the same as `type` except that occurrences
   // of type variables (aka. `GenericBinding` and references to `ImplBinding`)
   // are replaced by their corresponding type or witness in `dict`.
@@ -98,7 +80,9 @@ class TypeChecker {
 
  private:
   struct SingleStepEqualityContext;
+  class ConstraintTypeBuilder;
   class SubstitutedGenericBindings;
+  class ArgumentDeduction;
 
   // Information about the currently enclosing scopes.
   struct ScopeInfo {
@@ -221,14 +205,17 @@ class TypeChecker {
                            Nonnull<const ImplDeclaration*> impl_decl,
                            Nonnull<const Value*> self_type,
                            Nonnull<const Witness*> self_witness,
+                           Nonnull<const Witness*> iface_witness,
                            const ImplScope& impl_scope) -> ErrorOr<Success>;
 
   // Check that an `impl` declaration satisfies its constraints and add the
   // corresponding `ImplBinding`s to the impl scope.
-  auto CheckAndAddImplBindings(Nonnull<const ImplDeclaration*> impl_decl,
-                               Nonnull<const Value*> impl_type,
-                               Nonnull<const Witness*> self_witness,
-                               const ScopeInfo& scope_info) -> ErrorOr<Success>;
+  auto CheckAndAddImplBindings(
+      Nonnull<const ImplDeclaration*> impl_decl,
+      Nonnull<const Value*> impl_type, Nonnull<const Witness*> self_witness,
+      Nonnull<const Witness*> impl_witness,
+      llvm::ArrayRef<Nonnull<const GenericBinding*>> deduced_bindings,
+      const ScopeInfo& scope_info) -> ErrorOr<Success>;
 
   auto DeclareImplDeclaration(Nonnull<ImplDeclaration*> impl_decl,
                               const ScopeInfo& scope_info) -> ErrorOr<Success>;
@@ -359,8 +346,7 @@ class TypeChecker {
 
   // Attempt to implicitly convert type-checked expression `source` to the type
   // `destination`.
-  auto ImplicitlyConvert(const std::string& context,
-                         const ImplScope& impl_scope,
+  auto ImplicitlyConvert(std::string_view context, const ImplScope& impl_scope,
                          Nonnull<Expression*> source,
                          Nonnull<const Value*> destination)
       -> ErrorOr<Nonnull<Expression*>>;
@@ -377,13 +363,13 @@ class TypeChecker {
   //
   // 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,
+  auto ExpectType(SourceLocation source_loc, std::string_view context,
                   Nonnull<const Value*> expected, Nonnull<const Value*> actual,
                   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,
+  auto ExpectExactType(SourceLocation source_loc, std::string_view context,
                        Nonnull<const Value*> expected,
                        Nonnull<const Value*> actual,
                        const ImplScope& impl_scope) const -> ErrorOr<Success>;
@@ -413,25 +399,35 @@ class TypeChecker {
                                BuiltinInterfaceName interface) const
       -> ErrorOr<Nonnull<const InterfaceType*>>;
 
-  // Find impls that satisfy all of the `impl_bindings`, but with the
-  // type variables in the `impl_bindings` replaced by the argument
-  // type in `deduced_type_args`.  The results are placed in the
-  // `impls` map.
-  auto SatisfyImpls(llvm::ArrayRef<Nonnull<const ImplBinding*>> impl_bindings,
-                    const ImplScope& impl_scope, SourceLocation source_loc,
-                    const BindingMap& deduced_type_args,
-                    ImplWitnessMap& impls) const -> ErrorOr<Success>;
-
-  // Given an interface type, form a corresponding constraint type.
+  // Given an interface type, form a corresponding constraint type. The
+  // interface must be a complete type.
   auto MakeConstraintForInterface(SourceLocation source_loc,
                                   Nonnull<const InterfaceType*> iface_type)
-      -> Nonnull<const ConstraintType*>;
+      -> ErrorOr<Nonnull<const ConstraintType*>>;
 
   // Given a list of constraint types, form the combined constraint.
   auto CombineConstraints(
       SourceLocation source_loc,
       llvm::ArrayRef<Nonnull<const ConstraintType*>> constraints)
-      -> Nonnull<const ConstraintType*>;
+      -> ErrorOr<Nonnull<const ConstraintType*>>;
+
+  // Gets the type for the given associated constant.
+  auto GetTypeForAssociatedConstant(
+      Nonnull<const AssociatedConstant*> assoc) const -> Nonnull<const Value*>;
+
+  // Given `type.(interface.member)`, look for a rewrite in the declared type
+  // of `type`.
+  auto LookupRewriteInTypeOf(Nonnull<const Value*> type,
+                             Nonnull<const InterfaceType*> interface,
+                             Nonnull<const Declaration*> member) const
+      -> std::optional<const ValueLiteral*>;
+
+  // Given a witness value, look for a rewrite for the given associated
+  // constant.
+  auto LookupRewriteInWitness(Nonnull<const Witness*> witness,
+                              Nonnull<const InterfaceType*> interface,
+                              Nonnull<const Declaration*> member) const
+      -> std::optional<const ValueLiteral*>;
 
   /*
   ** Adds a member of a declaration to collected_members_
diff --git a/explorer/interpreter/value.cpp b/explorer/interpreter/value.cpp
index b5e4109e2ea7..a0bc3a7dcda5 100644
--- a/explorer/interpreter/value.cpp
+++ b/explorer/interpreter/value.cpp
@@ -45,6 +45,7 @@ static auto GetMember(Nonnull<Arena*> arena, Nonnull<const Value*> v,
     if (auto* assoc_const = dyn_cast_or_null<AssociatedConstantDeclaration>(
             field.member().declaration().value_or(nullptr))) {
       CARBON_CHECK(field.interface()) << "have witness but no interface";
+      // TODO: Use witness to find the value of the constant.
       return arena->New<AssociatedConstant>(v, *field.interface(), assoc_const,
                                             witness);
     }
@@ -431,6 +432,12 @@ void Value::Print(llvm::raw_ostream& out) const {
       }
       out << " where ";
       llvm::ListSeparator sep(" and ");
+      for (const ConstraintType::RewriteConstraint& rewrite :
+           constraint.rewrite_constraints()) {
+        out << sep << ".(" << *rewrite.interface << "."
+            << *GetName(*rewrite.constant)
+            << ") = " << rewrite.replacement->value();
+      }
       for (const ConstraintType::ImplConstraint& impl :
            constraint.impl_constraints()) {
         // TODO: Skip cases where `impl.type` is `.Self` and the interface is
@@ -439,6 +446,7 @@ void Value::Print(llvm::raw_ostream& out) const {
       }
       for (const ConstraintType::EqualityConstraint& equality :
            constraint.equality_constraints()) {
+        // TODO: Skip cases matching something in `rewrite_constraints()`.
         out << sep;
         llvm::ListSeparator equal(" == ");
         for (Nonnull<const Value*> value : equality.values) {
@@ -617,6 +625,9 @@ static auto BindingMapEqual(
 auto TypeEqual(Nonnull<const Value*> t1, Nonnull<const Value*> t2,
                std::optional<Nonnull<const EqualityContext*>> equality_ctx)
     -> bool {
+  if (t1 == t2) {
+    return true;
+  }
   if (t1->kind() != t2->kind()) {
     if (isa<AssociatedConstant>(t1) || isa<AssociatedConstant>(t2)) {
       return ValueEqual(t1, t2, equality_ctx);
@@ -793,6 +804,9 @@ auto TypeEqual(Nonnull<const Value*> t1, Nonnull<const Value*> t2,
 auto ValueStructurallyEqual(
     Nonnull<const Value*> v1, Nonnull<const Value*> v2,
     std::optional<Nonnull<const EqualityContext*>> equality_ctx) -> bool {
+  if (v1 == v2) {
+    return true;
+  }
   if (v1->kind() != v2->kind()) {
     return false;
   }
@@ -919,6 +933,10 @@ auto ValueStructurallyEqual(
 auto ValueEqual(Nonnull<const Value*> v1, Nonnull<const Value*> v2,
                 std::optional<Nonnull<const EqualityContext*>> equality_ctx)
     -> bool {
+  if (v1 == v2) {
+    return true;
+  }
+
   // 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
diff --git a/explorer/interpreter/value.h b/explorer/interpreter/value.h
index 037826c2d1aa..7da7d32c7a49 100644
--- a/explorer/interpreter/value.h
+++ b/explorer/interpreter/value.h
@@ -775,6 +775,14 @@ class ConstraintType : public Value {
 
   using EqualityConstraint = Carbon::EqualityConstraint;
 
+  // A constraint indicating that access to an associated constant should be
+  // replaced by another value.
+  struct RewriteConstraint {
+    Nonnull<const InterfaceType*> interface;
+    Nonnull<const AssociatedConstantDeclaration*> constant;
+    Nonnull<const ValueLiteral*> replacement;
+  };
+
   // A context in which we might look up a name.
   struct LookupContext {
     Nonnull<const Value*> context;
@@ -784,11 +792,13 @@ class ConstraintType : public Value {
   explicit ConstraintType(Nonnull<const GenericBinding*> self_binding,
                           std::vector<ImplConstraint> impl_constraints,
                           std::vector<EqualityConstraint> equality_constraints,
+                          std::vector<RewriteConstraint> rewrite_constraints,
                           std::vector<LookupContext> lookup_contexts)
       : Value(Kind::ConstraintType),
         self_binding_(self_binding),
         impl_constraints_(std::move(impl_constraints)),
         equality_constraints_(std::move(equality_constraints)),
+        rewrite_constraints_(std::move(rewrite_constraints)),
         lookup_contexts_(std::move(lookup_contexts)) {}
 
   static auto classof(const Value* value) -> bool {
@@ -807,6 +817,10 @@ class ConstraintType : public Value {
     return equality_constraints_;
   }
 
+  auto rewrite_constraints() const -> llvm::ArrayRef<RewriteConstraint> {
+    return rewrite_constraints_;
+  }
+
   auto lookup_contexts() const -> llvm::ArrayRef<LookupContext> {
     return lookup_contexts_;
   }
@@ -826,6 +840,7 @@ class ConstraintType : public Value {
   Nonnull<const GenericBinding*> self_binding_;
   std::vector<ImplConstraint> impl_constraints_;
   std::vector<EqualityConstraint> equality_constraints_;
+  std::vector<RewriteConstraint> rewrite_constraints_;
   std::vector<LookupContext> lookup_contexts_;
 };
 
@@ -916,6 +931,8 @@ class ConstraintImplWitness : public Witness {
   // element.
   static auto Make(Nonnull<Arena*> arena, Nonnull<const Witness*> witness,
                    int index) -> Nonnull<const Witness*> {
+    CARBON_CHECK(!llvm::isa<ImplWitness>(witness))
+        << "impl witness has no components to access";
     if (auto* constraint_witness = llvm::dyn_cast<ConstraintWitness>(witness)) {
       return constraint_witness->witnesses()[index];
     }
diff --git a/explorer/syntax/parser.ypp b/explorer/syntax/parser.ypp
index b68b6355cba2..5f73eb132d11 100644
--- a/explorer/syntax/parser.ypp
+++ b/explorer/syntax/parser.ypp
@@ -683,6 +683,9 @@ where_clause:
     { $$ = arena->New<IsWhereClause>(context.source_loc(), $1, $3); }
 | comparison_operand EQUAL_EQUAL comparison_operand
     { $$ = arena->New<EqualsWhereClause>(context.source_loc(), $1, $3); }
+// TODO: .(expression) = expression
+| designator EQUAL comparison_operand
+    { $$ = arena->New<RewriteWhereClause>(context.source_loc(), $1, $3); }
 ;
 where_clause_list:
   where_clause
diff --git a/explorer/testdata/assoc_const/lookup_in_rewrite.carbon b/explorer/testdata/assoc_const/lookup_in_rewrite.carbon
new file mode 100644
index 000000000000..21b92280fdfd
--- /dev/null
+++ b/explorer/testdata/assoc_const/lookup_in_rewrite.carbon
@@ -0,0 +1,94 @@
+// 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 | %{FileCheck-strict} %s
+// RUN: %{explorer-trace} %s 2>&1 | %{FileCheck-allow-unmatched} %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK:1
+// CHECK:i32.Hash
+// CHECK:0
+// CHECK:Potato.(Hashable.Hash)
+// CHECK:1
+// CHECK:Potato.Hash
+// CHECK:2
+// CHECK:Potato.Hash
+// CHECK:2
+// CHECK:result: 0
+
+package ExplorerTest api;
+
+interface Hashable {
+  fn Hash[me: Self]() -> i32;
+}
+
+class Potato {
+  external impl as Hashable {
+    fn Hash[me: Self]() -> i32 {
+      Print("Potato.(Hashable.Hash)");
+      return 1;
+    }
+  }
+
+  fn Hash[me: Self]() -> i32 {
+    Print("Potato.Hash");
+    return 2;
+  }
+}
+
+interface Maker {
+  let Result:! Hashable;
+  fn Make() -> Result;
+}
+
+external impl i32 as Hashable {
+  fn Hash[me: Self]() -> i32 {
+    Print("i32.Hash");
+    return me;
+  }
+}
+
+fn F[T:! Maker where .Result = i32](x: T) -> i32 {
+  // OK, can treat T.Make() as an i32.
+  return T.Make() + 1;
+}
+
+fn G[T:! Maker](x: T) -> i32 {
+  // OK, Potato.(Hashable.Hash), not Potato.Hash.
+  return T.Make().Hash();
+}
+
+fn H[T:! Maker where .Result = Potato](x: T) -> i32 {
+  // OK, Potato.Hash, not Potato.(Hashable.Hash).
+  return T.Make().Hash();
+}
+
+fn I[T:! Maker where .Result = Potato](x: T) -> i32 {
+  var p: Potato = {};
+  // OK, Potato.Hash, not Potato.(Hashable.Hash), even though we know Potato is
+  // Hashable here.
+  return p.Hash();
+}
+
+class IntFactory {
+  impl as Maker where .Result = i32 {
+    fn Make() -> i32 { return 0; }
+  }
+}
+
+class PotatoFactory {
+  impl as Maker where .Result = Potato {
+    fn Make() -> Potato { return {}; }
+  }
+}
+
+fn Main() -> i32 {
+  var f: IntFactory = {};
+  var g: PotatoFactory = {};
+  Print("{0}", F(f));
+  Print("{0}", G(f));
+  Print("{0}", G(g));
+  Print("{0}", H(g));
+  Print("{0}", I(g));
+  return 0;
+}
diff --git a/explorer/testdata/comparison/builtin_equality.carbon b/explorer/testdata/comparison/builtin_equality.carbon
index 0a12b1d34bc3..e6f4168dba3b 100644
--- a/explorer/testdata/comparison/builtin_equality.carbon
+++ b/explorer/testdata/comparison/builtin_equality.carbon
@@ -38,12 +38,12 @@ fn CompareEqualValues[T:! EqWith(.Self)](format: String, a: T, b: T) {
   Print(format, if a != b then 0 else 1);
 }
 
-fn CompareDifferentValues[T:! EqWith(.Self)](format: String, a: T, b: T) {
+fn CompareDifferentValues[U:! EqWith(.Self)](format: String, a: U, b: U) {
   Print(format, if a == b then 0 else 1);
   Print(format, if a != b then 1 else 0);
 }
 
-fn CompareAll[T:! EqWith(.Self)](format: String, a: T, b: T) {
+fn CompareAll[V:! EqWith(.Self)](format: String, a: V, b: V) {
   CompareEqualValues(format, a, a);
   CompareEqualValues(format, b, b);
   CompareDifferentValues(format, a, b);
diff --git a/explorer/testdata/comparison/fail_empty_struct.carbon b/explorer/testdata/comparison/fail_empty_struct.carbon
index b7a71614724b..be08bc4373f7 100644
--- a/explorer/testdata/comparison/fail_empty_struct.carbon
+++ b/explorer/testdata/comparison/fail_empty_struct.carbon
@@ -9,7 +9,7 @@
 package ExplorerTest api;
 
 // TODO: This should work
-// CHECK:COMPILATION ERROR: {{.*}}/explorer/testdata/comparison/fail_empty_struct.carbon:[[@LINE+1]]: type error in call: '{}' is not implicitly convertible to 'Type'
+// CHECK:COMPILATION ERROR: {{.*}}/explorer/testdata/comparison/fail_empty_struct.carbon:[[@LINE+1]]: type error in call: '({})' is not implicitly convertible to '(Type)'
 external impl {} as EqWith({}) {
   fn Equal[me: Self](other: Self) -> bool {
     return true;
diff --git a/explorer/testdata/constraint/rewrite.carbon b/explorer/testdata/constraint/rewrite.carbon
new file mode 100644
index 000000000000..62d0cf994e70
--- /dev/null
+++ b/explorer/testdata/constraint/rewrite.carbon
@@ -0,0 +1,32 @@
+// 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 | %{FileCheck-strict} %s
+// RUN: %{explorer-trace} %s 2>&1 | %{FileCheck-allow-unmatched} %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK:result: 12
+
+package ExplorerTest api;
+
+interface HasAssoc {
+  let Assoc:! Type;
+  let AssocVal:! i32;
+}
+class X {
+  external impl as HasAssoc where .Assoc = i32 and .AssocVal = 2 {}
+}
+
+fn F[T:! HasAssoc where .Assoc = i32](x: T) -> i32 {
+  var a: T.Assoc = 1;
+  return a;
+}
+
+fn G[T:! HasAssoc where .AssocVal = 2](x: T) -> i32 {
+  return x.AssocVal;
+}
+
+fn Main() -> i32 {
+  var x: X = {};
+  return F(x) * 10 + G(x);
+}
diff --git a/explorer/testdata/constraint/rewrite_compound.carbon b/explorer/testdata/constraint/rewrite_compound.carbon
new file mode 100644
index 000000000000..d00ee89a5933
--- /dev/null
+++ b/explorer/testdata/constraint/rewrite_compound.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 | %{FileCheck-strict} %s
+// RUN: %{explorer-trace} %s 2>&1 | %{FileCheck-allow-unmatched} %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK:result: 1
+
+package ExplorerTest api;
+
+interface HasAssoc {
+  let Assoc:! Type;
+}
+class X {
+  external impl as HasAssoc where .Assoc = i32 {}
+}
+
+alias WithoutRewrite = HasAssoc where .Assoc == i32;
+alias WithRewrite = HasAssoc where .Assoc = i32;
+
+fn F[T:! WithRewrite](x: T) -> i32 {
+  var a: T.(WithoutRewrite.Assoc) = 1;
+  return a;
+}
+
+fn Main() -> i32 {
+  var x: X = {};
+  return F(x);
+}
diff --git a/explorer/testdata/constraint/rewrite_compound_2.carbon b/explorer/testdata/constraint/rewrite_compound_2.carbon
new file mode 100644
index 000000000000..7558caa2f569
--- /dev/null
+++ b/explorer/testdata/constraint/rewrite_compound_2.carbon
@@ -0,0 +1,29 @@
+// 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 | %{FileCheck-strict} %s
+// RUN: %{explorer-trace} %s 2>&1 | %{FileCheck-allow-unmatched} %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK:result: 1
+
+package ExplorerTest api;
+
+interface HasAssoc {
+  let Assoc:! i32;
+}
+class X {
+  external impl as HasAssoc where .Assoc = 1 {}
+}
+
+alias WithoutRewrite = HasAssoc where .Assoc == 1;
+alias WithRewrite = HasAssoc where .Assoc = 1;
+
+fn F[T:! WithRewrite](x: T) -> i32 {
+  return x.(WithoutRewrite.Assoc);
+}
+
+fn Main() -> i32 {
+  var x: X = {};
+  return F(x);
+}
diff --git a/explorer/testdata/constraint/rewrite_in_qualifier.carbon b/explorer/testdata/constraint/rewrite_in_qualifier.carbon
new file mode 100644
index 000000000000..ee5233a1730a
--- /dev/null
+++ b/explorer/testdata/constraint/rewrite_in_qualifier.carbon
@@ -0,0 +1,31 @@
+// 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 | %{FileCheck-strict} %s
+// RUN: %{explorer-trace} %s 2>&1 | %{FileCheck-allow-unmatched} %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK:result: 2
+
+package ExplorerTest api;
+
+interface HasAssoc {
+  let Assoc:! Type;
+}
+class X {
+  external impl as HasAssoc where .Assoc = i32 {}
+}
+
+alias WithoutRewrite = HasAssoc where .Assoc == i32;
+alias WithRewrite = HasAssoc where .Assoc = i32;
+
+fn G[T:! WithoutRewrite](x: T) -> i32 {
+  // TODO: We should reject this once `==` isn't applied automatically.
+  var a: T.(WithRewrite.Assoc) = 2;
+  return a;
+}
+
+fn Main() -> i32 {
+  var x: X = {};
+  return G(x);
+}
diff --git a/explorer/testdata/constraint/rewrite_in_qualifier_and_type.carbon b/explorer/testdata/constraint/rewrite_in_qualifier_and_type.carbon
new file mode 100644
index 000000000000..19ce6cd0773f
--- /dev/null
+++ b/explorer/testdata/constraint/rewrite_in_qualifier_and_type.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: %{explorer} %s 2>&1 | %{FileCheck-strict} %s
+// RUN: %{explorer-trace} %s 2>&1 | %{FileCheck-allow-unmatched} %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK:result: 3
+
+package ExplorerTest api;
+
+interface HasAssoc {
+  let Assoc:! Type;
+}
+class X {
+  external impl as HasAssoc where .Assoc = i32 {}
+}
+
+fn H[T:! HasAssoc where .Assoc = i32, U:! Type where .Self == i32](a: T, b: U) -> i32 {
+  var a: T.((HasAssoc where .Assoc = U).Assoc) = 3;
+  return a;
+}
+
+fn Main() -> i32 {
+  var x: X = {};
+  var y: i32 = 0;
+  return H(x, y);
+}
diff --git a/explorer/testdata/generic_class/parameter_type_conversion.carbon b/explorer/testdata/generic_class/parameter_type_conversion.carbon
new file mode 100644
index 000000000000..306484cad452
--- /dev/null
+++ b/explorer/testdata/generic_class/parameter_type_conversion.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 | %{FileCheck-strict} %s
+// RUN: %{explorer-trace} %s 2>&1 | %{FileCheck-allow-unmatched} %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK:result: 4
+
+package ExplorerTest api;
+
+class Holder(N:! i32) {
+  fn Get() -> i32 {
+    return N;
+  }
+}
+
+class IntLike {
+  impl as ImplicitAs(i32) {
+    fn Convert[me: Self]() -> i32 { return 4; }
+  }
+  fn Make() -> IntLike { return {}; }
+}
+
+fn Main() -> i32 {
+  return Holder(IntLike.Make()).Get();
+}
diff --git a/explorer/testdata/generic_function/fail_type_deduction_unused.carbon b/explorer/testdata/generic_function/fail_type_deduction_unused.carbon
index 5a6069b72e6d..6d71da40791a 100644
--- a/explorer/testdata/generic_function/fail_type_deduction_unused.carbon
+++ b/explorer/testdata/generic_function/fail_type_deduction_unused.carbon
@@ -13,7 +13,6 @@ fn id[T:! Type](x: i32) -> i32 {
 }
 
 fn Main() -> i32 {
-  // CHECK:COMPILATION ERROR: {{.*}}/explorer/testdata/generic_function/fail_type_deduction_unused.carbon:[[@LINE+2]]: could not deduce type argument for type parameter T
-  // CHECK:in id(0)
+  // CHECK:COMPILATION ERROR: {{.*}}/explorer/testdata/generic_function/fail_type_deduction_unused.carbon:[[@LINE+1]]: could not deduce type argument for type parameter T in call
   return id(0);
 }
diff --git a/explorer/testdata/interface/fail_interface_missing_member.carbon b/explorer/testdata/interface/fail_interface_missing_member.carbon
index 60da98fb2c18..c5294fd3203f 100644
--- a/explorer/testdata/interface/fail_interface_missing_member.carbon
+++ b/explorer/testdata/interface/fail_interface_missing_member.carbon
@@ -13,7 +13,7 @@ interface Vector {
 }
 
 fn ScaleGeneric[T:! Vector](a: T, s: i32) -> T {
-  // CHECK:COMPILATION ERROR: {{.*}}/explorer/testdata/interface/fail_interface_missing_member.carbon:[[@LINE+1]]: member access, Scale not in interface Vector
+  // CHECK:COMPILATION ERROR: {{.*}}/explorer/testdata/interface/fail_interface_missing_member.carbon:[[@LINE+1]]: member access, Scale not in constraint interface Vector where T is interface Vector
   return a.Scale(s);
 }
 
diff --git a/explorer/testdata/interface/fail_use_symbolic_member.carbon b/explorer/testdata/interface/fail_use_symbolic_member.carbon
index 7491b5ace047..803a696724d0 100644
--- a/explorer/testdata/interface/fail_use_symbolic_member.carbon
+++ b/explorer/testdata/interface/fail_use_symbolic_member.carbon
@@ -12,7 +12,7 @@ interface X {
   fn F() -> Type;
 }
 
-// CHECK:COMPILATION ERROR: {{.*}}/explorer/testdata/interface/fail_use_symbolic_member.carbon:[[@LINE+1]]: member lookup for F in symbolic witness for T:! X
+// CHECK:COMPILATION ERROR: {{.*}}/explorer/testdata/interface/fail_use_symbolic_member.carbon:[[@LINE+1]]: member lookup for F in symbolic witness 0 of witness for T:! X
 fn G[T:! X]() -> T.F() {
   return {};
 }