diff --git a/explorer/ast/ast_rtti.txt b/explorer/ast/ast_rtti.txt
index a29ee155a18f..1794faea9fa6 100644
--- a/explorer/ast/ast_rtti.txt
+++ b/explorer/ast/ast_rtti.txt
@@ -71,7 +71,6 @@ abstract class Expression : AstNode;
   class WhereExpression : Expression;
   class UnimplementedExpression : Expression;
   class ArrayTypeLiteral : Expression;
-  class InstantiateImpl : Expression;
 abstract class WhereClause : AstNode;
   class IsWhereClause : WhereClause;
   class EqualsWhereClause : WhereClause;
diff --git a/explorer/ast/bindings.h b/explorer/ast/bindings.h
index ee3c9afa4f46..1fe517685e72 100644
--- a/explorer/ast/bindings.h
+++ b/explorer/ast/bindings.h
@@ -47,6 +47,11 @@ class Bindings {
   // An empty set of bindings.
   static auto None() -> Nonnull<const Bindings*>;
 
+  // Determine whether this is an empty set of bindings.
+  [[nodiscard]] auto empty() const -> bool {
+    return args_.empty() && witnesses_.empty();
+  }
+
  private:
   BindingMap args_;
   ImplWitnessMap witnesses_;
diff --git a/explorer/ast/declaration.h b/explorer/ast/declaration.h
index b359c8790634..1fadf27858c8 100644
--- a/explorer/ast/declaration.h
+++ b/explorer/ast/declaration.h
@@ -461,15 +461,20 @@ class InterfaceDeclaration : public Declaration {
  public:
   using ImplementsCarbonValueNode = void;
 
-  InterfaceDeclaration(SourceLocation source_loc, std::string name,
+  InterfaceDeclaration(Nonnull<Arena*> arena, SourceLocation source_loc,
+                       std::string name,
                        std::optional<Nonnull<TuplePattern*>> params,
-                       Nonnull<GenericBinding*> self,
                        std::vector<Nonnull<Declaration*>> members)
       : Declaration(AstNodeKind::InterfaceDeclaration, source_loc),
         name_(std::move(name)),
         params_(std::move(params)),
-        self_(self),
-        members_(std::move(members)) {}
+        self_type_(arena->New<SelfDeclaration>(source_loc)),
+        members_(std::move(members)) {
+    // `interface X` has `Self:! X`.
+    auto self_type_ref = arena->New<IdentifierExpression>(source_loc, name);
+    self_type_ref->set_value_node(self_type_);
+    self_ = arena->New<GenericBinding>(source_loc, "Self", self_type_ref);
+  }
 
   static auto classof(const AstNode* node) -> bool {
     return InheritsFromInterfaceDeclaration(node->kind());
@@ -480,6 +485,13 @@ class InterfaceDeclaration : public Declaration {
     return params_;
   }
   auto params() -> std::optional<Nonnull<TuplePattern*>> { return params_; }
+  // Get the type of `Self`, which is a reference to the interface itself, with
+  // parameters mapped to their values. For example, in `interface X(T:!
+  // Type)`, the self type is `X(T)`.
+  auto self_type() const -> Nonnull<const SelfDeclaration*> {
+    return self_type_;
+  }
+  auto self_type() -> Nonnull<SelfDeclaration*> { return self_type_; }
   auto self() const -> Nonnull<const GenericBinding*> { return self_; }
   auto self() -> Nonnull<GenericBinding*> { return self_; }
   auto members() const -> llvm::ArrayRef<Nonnull<Declaration*>> {
@@ -491,6 +503,7 @@ class InterfaceDeclaration : public Declaration {
  private:
   std::string name_;
   std::optional<Nonnull<TuplePattern*>> params_;
+  Nonnull<SelfDeclaration*> self_type_;
   Nonnull<GenericBinding*> self_;
   std::vector<Nonnull<Declaration*>> members_;
 };
diff --git a/explorer/ast/expression.cpp b/explorer/ast/expression.cpp
index 0d5522aa1848..43ff49a6622d 100644
--- a/explorer/ast/expression.cpp
+++ b/explorer/ast/expression.cpp
@@ -257,12 +257,6 @@ void Expression::Print(llvm::raw_ostream& out) const {
       }
       break;
     }
-    case ExpressionKind::InstantiateImpl: {
-      // TODO: For layering reasons, we can't print out the witness and
-      // argument values from here.
-      out << "instantiate impl";
-      break;
-    }
     case ExpressionKind::UnimplementedExpression: {
       const auto& unimplemented = cast<UnimplementedExpression>(*this);
       out << "UnimplementedExpression<" << unimplemented.label() << ">(";
@@ -347,7 +341,6 @@ void Expression::PrintID(llvm::raw_ostream& out) const {
     case ExpressionKind::UnimplementedExpression:
     case ExpressionKind::FunctionTypeLiteral:
     case ExpressionKind::ArrayTypeLiteral:
-    case ExpressionKind::InstantiateImpl:
       out << "...";
       break;
   }
diff --git a/explorer/ast/expression.h b/explorer/ast/expression.h
index 72c80205fe00..611d92c53ec7 100644
--- a/explorer/ast/expression.h
+++ b/explorer/ast/expression.h
@@ -853,33 +853,6 @@ class WhereExpression : public Expression {
   std::vector<Nonnull<WhereClause*>> clauses_;
 };
 
-// Instantiate a generic impl.
-class InstantiateImpl : public Expression {
- public:
-  using ImplementsCarbonValueNode = void;
-
-  explicit InstantiateImpl(SourceLocation source_loc,
-                           Nonnull<const Witness*> generic_impl,
-                           Bindings bindings)
-      : Expression(AstNodeKind::InstantiateImpl, source_loc),
-        generic_impl_(generic_impl),
-        bindings_(std::move(bindings)) {}
-
-  static auto classof(const AstNode* node) -> bool {
-    return InheritsFromInstantiateImpl(node->kind());
-  }
-  auto generic_impl() const -> Nonnull<const Witness*> { return generic_impl_; }
-  auto type_args() const -> const BindingMap& { return bindings_.args(); }
-
-  // Maps each of the impl bindings to an expression that constructs
-  // the witness table for that impl.
-  auto impls() const -> const ImplWitnessMap& { return bindings_.witnesses(); }
-
- private:
-  Nonnull<const Witness*> generic_impl_;
-  Bindings bindings_;
-};
-
 // An expression whose semantics have not been implemented. This can be used
 // as a placeholder during development, in order to implement and test parsing
 // of a new expression syntax without having to implement its semantics.
diff --git a/explorer/fuzzing/ast_to_proto.cpp b/explorer/fuzzing/ast_to_proto.cpp
index 02b98c7ac585..f0553a419b46 100644
--- a/explorer/fuzzing/ast_to_proto.cpp
+++ b/explorer/fuzzing/ast_to_proto.cpp
@@ -110,11 +110,11 @@ static auto ExpressionToProto(const Expression& expression)
     -> Fuzzing::Expression {
   Fuzzing::Expression expression_proto;
   switch (expression.kind()) {
-    case ExpressionKind::InstantiateImpl:
     case ExpressionKind::ValueLiteral: {
-      // These do not correspond to source syntax.
+      // This does not correspond to source syntax.
       break;
     }
+
     case ExpressionKind::CallExpression: {
       const auto& call = cast<CallExpression>(expression);
       auto* call_proto = expression_proto.mutable_call();
diff --git a/explorer/interpreter/interpreter.cpp b/explorer/interpreter/interpreter.cpp
index 471bf9efe6f2..562e66f62122 100644
--- a/explorer/interpreter/interpreter.cpp
+++ b/explorer/interpreter/interpreter.cpp
@@ -103,10 +103,10 @@ class Interpreter {
                Nonnull<const Value*> destination_type,
                SourceLocation source_loc) -> ErrorOr<Nonnull<const Value*>>;
 
-  // Evaluate an expression immediately, recursively.
+  // Evaluate an expression immediately, recursively, and return its result.
   //
   // TODO: Stop using this.
-  auto EvalExpRecursively(Nonnull<const Expression*> exp)
+  auto EvalRecursively(std::unique_ptr<Action> action)
       -> ErrorOr<Nonnull<const Value*>>;
 
   // Evaluate an associated constant by evaluating its witness and looking
@@ -133,6 +133,8 @@ class Interpreter {
   //     __Fn (Point(T)) -> Point(U)
   // becomes
   //     __Fn (Point(i32)) -> Point(bool)
+  //
+  // TODO: This should be an Action.
   auto InstantiateType(Nonnull<const Value*> type, SourceLocation source_loc)
       -> ErrorOr<Nonnull<const Value*>>;
 
@@ -142,6 +144,11 @@ class Interpreter {
                            SourceLocation source_loc)
       -> ErrorOr<Nonnull<const Bindings*>>;
 
+  // Instantiate a witness by replacing all type variables and impl binding
+  // references that occur within it by the current values of those variables.
+  auto InstantiateWitness(Nonnull<const Witness*> witness)
+      -> ErrorOr<Nonnull<const Witness*>>;
+
   // Call the function `fun` with the given `arg` and the `witnesses`
   // for the function's impl bindings.
   auto CallFunction(const CallExpression& call, Nonnull<const Value*> fun,
@@ -485,21 +492,20 @@ auto Interpreter::StepLvalue() -> ErrorOr<Success> {
     case ExpressionKind::WhereExpression:
     case ExpressionKind::DotSelfExpression:
     case ExpressionKind::ArrayTypeLiteral:
-    case ExpressionKind::InstantiateImpl:
       CARBON_FATAL() << "Can't treat expression as lvalue: " << exp;
     case ExpressionKind::UnimplementedExpression:
       CARBON_FATAL() << "Unimplemented: " << exp;
   }
 }
 
-auto Interpreter::EvalExpRecursively(Nonnull<const Expression*> exp)
+auto Interpreter::EvalRecursively(std::unique_ptr<Action> action)
     -> ErrorOr<Nonnull<const Value*>> {
   if (trace_stream_) {
-    **trace_stream_ << "--- recursive eval of " << *exp << "\n";
+    **trace_stream_ << "--- recursive eval\n";
     PrintState(**trace_stream_);
   }
   todo_.BeginRecursiveAction();
-  CARBON_RETURN_IF_ERROR(todo_.Spawn(std::make_unique<ExpressionAction>(exp)));
+  CARBON_RETURN_IF_ERROR(todo_.Spawn(std::move(action)));
   // Note that the only `RecursiveAction` we can encounter here is our own --
   // if a nested action begins a recursive action, it will run until that
   // action is finished and popped off the queue before returning to us.
@@ -522,11 +528,8 @@ auto Interpreter::EvalAssociatedConstant(
     Nonnull<const AssociatedConstant*> assoc, SourceLocation source_loc)
     -> ErrorOr<Nonnull<const Value*>> {
   // Find the witness.
-  Nonnull<const Value*> witness = &assoc->witness();
-  if (auto* sym = dyn_cast<SymbolicWitness>(witness)) {
-    CARBON_ASSIGN_OR_RETURN(witness,
-                            EvalExpRecursively(&sym->impl_expression()));
-  }
+  CARBON_ASSIGN_OR_RETURN(Nonnull<const Witness*> witness,
+                          InstantiateWitness(&assoc->witness()));
   if (!isa<ImplWitness>(witness)) {
     CARBON_CHECK(phase() == Phase::CompileTime)
         << "symbolic witnesses should only be formed at compile time";
@@ -605,10 +608,8 @@ auto Interpreter::InstantiateBindings(Nonnull<const Bindings*> bindings,
 
   ImplWitnessMap witnesses = bindings->witnesses();
   for (auto& [bind, witness] : witnesses) {
-    if (auto* sym = dyn_cast<SymbolicWitness>(witness)) {
-      CARBON_ASSIGN_OR_RETURN(witness,
-                              EvalExpRecursively(&sym->impl_expression()));
-    }
+    CARBON_ASSIGN_OR_RETURN(witness,
+                            InstantiateWitness(cast<Witness>(witness)));
   }
 
   if (args == bindings->args() && witnesses == bindings->witnesses()) {
@@ -617,6 +618,14 @@ auto Interpreter::InstantiateBindings(Nonnull<const Bindings*> bindings,
   return arena_->New<Bindings>(std::move(args), std::move(witnesses));
 }
 
+auto Interpreter::InstantiateWitness(Nonnull<const Witness*> witness)
+    -> ErrorOr<Nonnull<const Witness*>> {
+  CARBON_ASSIGN_OR_RETURN(
+      Nonnull<const Value*> value,
+      EvalRecursively(std::make_unique<WitnessAction>(witness)));
+  return cast<Witness>(value);
+}
+
 auto Interpreter::Convert(Nonnull<const Value*> value,
                           Nonnull<const Value*> destination_type,
                           SourceLocation source_loc)
@@ -643,7 +652,9 @@ auto Interpreter::Convert(Nonnull<const Value*> value,
     case Value::Kind::InterfaceType:
     case Value::Kind::ConstraintType:
     case Value::Kind::ImplWitness:
-    case Value::Kind::SymbolicWitness:
+    case Value::Kind::BindingWitness:
+    case Value::Kind::ConstraintWitness:
+    case Value::Kind::ConstraintImplWitness:
     case Value::Kind::ParameterizedEntityName:
     case Value::Kind::ChoiceType:
     case Value::Kind::ContinuationType:
@@ -895,35 +906,6 @@ auto Interpreter::StepExp() -> ErrorOr<Success> {
                     << " (" << exp.source_loc() << ") --->\n";
   }
   switch (exp.kind()) {
-    case ExpressionKind::InstantiateImpl: {
-      const InstantiateImpl& inst_impl = cast<InstantiateImpl>(exp);
-      if (act.pos() == 0) {
-        return todo_.Spawn(
-            std::make_unique<WitnessAction>(inst_impl.generic_impl()));
-      }
-      if (act.pos() == 1 && isa<SymbolicWitness>(act.results()[0])) {
-        return todo_.FinishAction(arena_->New<SymbolicWitness>(&exp));
-      }
-      if (act.pos() - 1 < int(inst_impl.impls().size())) {
-        auto iter = inst_impl.impls().begin();
-        std::advance(iter, act.pos() - 1);
-        return todo_.Spawn(
-            std::make_unique<WitnessAction>(cast<Witness>(iter->second)));
-      } else {
-        Nonnull<const ImplWitness*> generic_witness =
-            cast<ImplWitness>(act.results()[0]);
-        ImplWitnessMap witnesses;
-        int i = 0;
-        for (const auto& [impl_bind, impl_exp] : inst_impl.impls()) {
-          witnesses[impl_bind] = cast<Witness>(act.results()[i + 1]);
-          ++i;
-        }
-        return todo_.FinishAction(arena_->New<ImplWitness>(
-            &generic_witness->declaration(),
-            arena_->New<Bindings>(inst_impl.type_args(),
-                                  std::move(witnesses))));
-      }
-    }
     case ExpressionKind::IndexExpression: {
       if (act.pos() == 0) {
         //    { { e[i] :: C, E, F} :: S, H}
@@ -931,9 +913,6 @@ auto Interpreter::StepExp() -> ErrorOr<Success> {
         return todo_.Spawn(std::make_unique<ExpressionAction>(
             &cast<IndexExpression>(exp).object()));
       } else if (act.pos() == 1) {
-        if (isa<SymbolicWitness>(act.results()[0])) {
-          return todo_.FinishAction(arena_->New<SymbolicWitness>(&exp));
-        }
         return todo_.Spawn(std::make_unique<ExpressionAction>(
             &cast<IndexExpression>(exp).offset()));
       } else {
@@ -1447,12 +1426,58 @@ auto Interpreter::StepWitness() -> ErrorOr<Success> {
                     << ". --->\n";
   }
   switch (witness->kind()) {
-    case Value::Kind::SymbolicWitness:
-      return todo_.ReplaceWith(std::make_unique<ExpressionAction>(
-          &cast<SymbolicWitness>(witness)->impl_expression()));
+    case Value::Kind::BindingWitness: {
+      const ImplBinding* binding = cast<BindingWitness>(witness)->binding();
+      CARBON_ASSIGN_OR_RETURN(
+          Nonnull<const Value*> value,
+          todo_.ValueOfNode(binding, binding->type_var()->source_loc()));
+      if (const auto* lvalue = dyn_cast<LValue>(value)) {
+        // TODO: Why do we store values for impl bindings on the heap?
+        CARBON_ASSIGN_OR_RETURN(
+            value,
+            heap_.Read(lvalue->address(), binding->type_var()->source_loc()));
+      }
+      return todo_.FinishAction(value);
+    }
 
-    case Value::Kind::ImplWitness:
-      return todo_.FinishAction(witness);
+    case Value::Kind::ConstraintWitness: {
+      llvm::ArrayRef<Nonnull<const Witness*>> witnesses =
+          cast<ConstraintWitness>(witness)->witnesses();
+      if (act.pos() < static_cast<int>(witnesses.size())) {
+        return todo_.Spawn(
+            std::make_unique<WitnessAction>(witnesses[act.pos()]));
+      }
+      std::vector<Nonnull<const Witness*>> new_witnesses;
+      new_witnesses.reserve(witnesses.size());
+      for (auto* witness : act.results()) {
+        new_witnesses.push_back(cast<Witness>(witness));
+      }
+      return todo_.FinishAction(
+          arena_->New<ConstraintWitness>(std::move(new_witnesses)));
+    }
+
+    case Value::Kind::ConstraintImplWitness: {
+      auto* constraint_impl = cast<ConstraintImplWitness>(witness);
+      if (act.pos() == 0) {
+        return todo_.Spawn(std::make_unique<WitnessAction>(
+            constraint_impl->constraint_witness()));
+      }
+      return todo_.FinishAction(ConstraintImplWitness::Make(
+          arena_, cast<Witness>(act.results()[0]), constraint_impl->index()));
+    }
+
+    case Value::Kind::ImplWitness: {
+      auto* impl_witness = cast<ImplWitness>(witness);
+      CARBON_ASSIGN_OR_RETURN(
+          Nonnull<const Bindings*> new_bindings,
+          InstantiateBindings(&impl_witness->bindings(),
+                              impl_witness->declaration().source_loc()));
+      return todo_.FinishAction(
+          new_bindings == &impl_witness->bindings()
+              ? impl_witness
+              : arena_->New<ImplWitness>(&impl_witness->declaration(),
+                                         new_bindings));
+    }
 
     default:
       CARBON_FATAL() << "unexpected kind of witness " << *witness;
diff --git a/explorer/interpreter/resolve_names.cpp b/explorer/interpreter/resolve_names.cpp
index 24be26cfc127..53e86d41a7e1 100644
--- a/explorer/interpreter/resolve_names.cpp
+++ b/explorer/interpreter/resolve_names.cpp
@@ -267,7 +267,6 @@ static auto ResolveNames(Expression& expression,
     case ExpressionKind::TypeTypeLiteral:
     case ExpressionKind::ValueLiteral:
       break;
-    case ExpressionKind::InstantiateImpl:  // created after name resolution
     case ExpressionKind::UnimplementedExpression:
       return CompilationError(expression.source_loc()) << "Unimplemented";
   }
@@ -513,6 +512,8 @@ static auto ResolveNames(Declaration& declaration, StaticScope& enclosing_scope,
         CARBON_RETURN_IF_ERROR(ResolveNames(**iface.params(), iface_scope));
       }
       enclosing_scope.MarkUsable(iface.name());
+      // Don't resolve names in the type of the self binding. The
+      // InterfaceDeclaration constructor already did that.
       CARBON_RETURN_IF_ERROR(iface_scope.Add("Self", iface.self()));
       CARBON_RETURN_IF_ERROR(
           ResolveMemberNames(iface.members(), iface_scope, bodies));
diff --git a/explorer/interpreter/resolve_unformed.cpp b/explorer/interpreter/resolve_unformed.cpp
index 0f1c10098428..5c7878208abf 100644
--- a/explorer/interpreter/resolve_unformed.cpp
+++ b/explorer/interpreter/resolve_unformed.cpp
@@ -140,7 +140,6 @@ static auto ResolveUnformed(Nonnull<const Expression*> expression,
     case ExpressionKind::UnimplementedExpression:
     case ExpressionKind::FunctionTypeLiteral:
     case ExpressionKind::ArrayTypeLiteral:
-    case ExpressionKind::InstantiateImpl:
       break;
   }
   return Success();
diff --git a/explorer/interpreter/type_checker.cpp b/explorer/interpreter/type_checker.cpp
index 5fe920ef3de5..e73d3f020718 100644
--- a/explorer/interpreter/type_checker.cpp
+++ b/explorer/interpreter/type_checker.cpp
@@ -180,7 +180,9 @@ static auto IsTypeOfType(Nonnull<const Value*> value) -> bool {
     case Value::Kind::StringValue:
     case Value::Kind::UninitializedValue:
     case Value::Kind::ImplWitness:
-    case Value::Kind::SymbolicWitness:
+    case Value::Kind::BindingWitness:
+    case Value::Kind::ConstraintWitness:
+    case Value::Kind::ConstraintImplWitness:
     case Value::Kind::ParameterizedEntityName:
     case Value::Kind::MemberName:
     case Value::Kind::TypeOfParameterizedEntityName:
@@ -241,7 +243,9 @@ static auto IsType(Nonnull<const Value*> value, bool concrete = false) -> bool {
     case Value::Kind::StringValue:
     case Value::Kind::UninitializedValue:
     case Value::Kind::ImplWitness:
-    case Value::Kind::SymbolicWitness:
+    case Value::Kind::BindingWitness:
+    case Value::Kind::ConstraintWitness:
+    case Value::Kind::ConstraintImplWitness:
     case Value::Kind::ParameterizedEntityName:
     case Value::Kind::MemberName:
       return false;
@@ -864,7 +868,9 @@ auto TypeChecker::ArgumentDeduction(
       return handle_non_deduced_type();
     }
     case Value::Kind::ImplWitness:
-    case Value::Kind::SymbolicWitness:
+    case Value::Kind::BindingWitness:
+    case Value::Kind::ConstraintWitness:
+    case Value::Kind::ConstraintImplWitness:
     case Value::Kind::ParameterizedEntityName:
     case Value::Kind::MemberName:
     case Value::Kind::IntValue:
@@ -1174,7 +1180,9 @@ auto TypeChecker::Substitute(
       // type for it.
       return type;
     case Value::Kind::ImplWitness:
-    case Value::Kind::SymbolicWitness:
+    case Value::Kind::BindingWitness:
+    case Value::Kind::ConstraintWitness:
+    case Value::Kind::ConstraintImplWitness:
     case Value::Kind::ParameterizedEntityName:
     case Value::Kind::MemberName:
     case Value::Kind::IntValue:
@@ -1263,39 +1271,30 @@ auto TypeChecker::MatchImpl(const InterfaceType& iface,
     **trace_stream_ << "matched with " << *impl.type << " as "
                     << *impl.interface << "\n\n";
   }
-  return deduced_args.empty()
-             ? impl.witness
-             : arena_->New<SymbolicWitness>(arena_->New<InstantiateImpl>(
-                   source_loc, impl.witness,
-                   Bindings(std::move(deduced_args), std::move(impls))));
+  if (deduced_args.empty()) {
+    return impl.witness;
+  }
+
+  // Only ImplWitnesses can be parameterized.
+  const ImplWitness* impl_witness = cast<ImplWitness>(impl.witness);
+  CARBON_CHECK(impl_witness->bindings().empty())
+      << "should not deduce arguments for ImplWitness we have already resolved";
+  return arena_->New<ImplWitness>(
+      &impl_witness->declaration(),
+      arena_->New<Bindings>(std::move(deduced_args), std::move(impls)));
 }
 
 auto TypeChecker::MakeConstraintWitness(
     const ConstraintType& constraint,
     std::vector<Nonnull<const Witness*>> impl_constraint_witnesses,
     SourceLocation source_loc) const -> Nonnull<const Witness*> {
-  // TODO: Create a TupleValue when possible.
-  std::vector<Nonnull<Expression*>> witness_literals;
-  witness_literals.reserve(impl_constraint_witnesses.size());
-  // TODO: A witness expression has no type.
-  auto* witness_type = arena_->New<TypeType>();
-  for (const Witness* witness : impl_constraint_witnesses) {
-    witness_literals.push_back(arena_->New<ValueLiteral>(
-        source_loc, witness, witness_type, ValueCategory::Let));
-  }
-  return arena_->New<SymbolicWitness>(
-      arena_->New<TupleLiteral>(source_loc, std::move(witness_literals)));
+  return arena_->New<ConstraintWitness>(std::move(impl_constraint_witnesses));
 }
 
 auto TypeChecker::MakeConstraintWitnessAccess(Nonnull<const Witness*> witness,
                                               size_t impl_offset) const
     -> Nonnull<const Witness*> {
-  SourceLocation no_source_loc("", 0);
-  return arena_->New<SymbolicWitness>(arena_->New<IndexExpression>(
-      no_source_loc,
-      const_cast<Expression*>(
-          &cast<SymbolicWitness>(witness)->impl_expression()),
-      arena_->New<IntLiteral>(no_source_loc, impl_offset)));
+  return ConstraintImplWitness::Make(arena_, witness, impl_offset);
 }
 
 auto TypeChecker::SatisfyImpls(
@@ -1501,7 +1500,6 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
     return Success();
   }
   switch (e->kind()) {
-    case ExpressionKind::InstantiateImpl:
     case ExpressionKind::ValueLiteral:
       CARBON_FATAL() << "attempting to type check node " << *e
                      << " generated during type checking";
@@ -2664,14 +2662,6 @@ void TypeChecker::BringImplsIntoScope(
   }
 }
 
-auto TypeChecker::CreateImplBindingWitness(
-    Nonnull<const ImplBinding*> impl_binding) -> Nonnull<const Witness*> {
-  auto impl_id =
-      arena_->New<IdentifierExpression>(impl_binding->source_loc(), "impl");
-  impl_id->set_value_node(impl_binding);
-  return arena_->New<SymbolicWitness>(impl_id);
-}
-
 void TypeChecker::BringImplIntoScope(Nonnull<const ImplBinding*> impl_binding,
                                      ImplScope& impl_scope) {
   CARBON_CHECK(impl_binding->type_var()->symbolic_identity().has_value() &&
@@ -2817,7 +2807,7 @@ auto TypeChecker::TypeCheckPattern(
         Nonnull<ImplBinding*> impl_binding =
             arena_->New<ImplBinding>(binding.source_loc(), &binding, type);
         impl_binding->set_symbolic_identity(
-            CreateImplBindingWitness(impl_binding));
+            arena_->New<BindingWitness>(impl_binding));
         binding.set_impl_binding(impl_binding);
         BringImplIntoScope(impl_binding, impl_scope);
       }
@@ -3637,21 +3627,24 @@ auto TypeChecker::DeclareInterfaceDeclaration(
     iface_decl->set_static_type(arena_->New<TypeOfInterfaceType>(iface_type));
   }
 
+  // Set the type of Self to be the instantiated interface.
+  Nonnull<SelfDeclaration*> self_type = iface_decl->self_type();
+  self_type->set_static_type(arena_->New<TypeType>());
+  SetConstantValue(self_type, 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());
 
   ScopeInfo iface_scope_info = ScopeInfo::ForNonClassScope(&iface_scope);
   for (Nonnull<Declaration*> m : iface_decl->members()) {
     CARBON_RETURN_IF_ERROR(DeclareDeclaration(m, iface_scope_info));
 
     if (auto* assoc = dyn_cast<AssociatedConstantDeclaration>(m)) {
-      // TODO: The witness should be optional in AssociatedConstant.
-      Nonnull<const Expression*> witness_expr =
-          arena_->New<DotSelfExpression>(iface_decl->source_loc());
       assoc->binding().set_symbolic_identity(arena_->New<AssociatedConstant>(
-          &iface_decl->self()->value(), iface_type, assoc,
-          arena_->New<SymbolicWitness>(witness_expr)));
+          &iface_decl->self()->value(), iface_type, assoc, self_witness));
     }
   }
   if (trace_stream_) {
@@ -4041,7 +4034,9 @@ static bool IsValidTypeForAliasTarget(Nonnull<const Value*> type) {
     case Value::Kind::AlternativeValue:
     case Value::Kind::TupleValue:
     case Value::Kind::ImplWitness:
-    case Value::Kind::SymbolicWitness:
+    case Value::Kind::BindingWitness:
+    case Value::Kind::ConstraintWitness:
+    case Value::Kind::ConstraintImplWitness:
     case Value::Kind::ParameterizedEntityName:
     case Value::Kind::MemberName:
     case Value::Kind::BindingPlaceholderValue:
diff --git a/explorer/interpreter/value.cpp b/explorer/interpreter/value.cpp
index a9adfe888f3d..725b1e68c5af 100644
--- a/explorer/interpreter/value.cpp
+++ b/explorer/interpreter/value.cpp
@@ -50,34 +50,27 @@ static auto GetMember(Nonnull<Arena*> arena, Nonnull<const Value*> v,
     }
 
     // Associated functions.
-    switch (witness->kind()) {
-      case Value::Kind::ImplWitness: {
-        auto* impl_witness = cast<ImplWitness>(witness);
-        if (std::optional<Nonnull<const Declaration*>> mem_decl =
-                FindMember(f, impl_witness->declaration().members());
-            mem_decl.has_value()) {
-          const auto& fun_decl = cast<FunctionDeclaration>(**mem_decl);
-          if (fun_decl.is_method()) {
-            return arena->New<BoundMethodValue>(&fun_decl, v,
-                                                &impl_witness->bindings());
-          } else {
-            // Class function.
-            auto* fun = cast<FunctionValue>(*fun_decl.constant_value());
-            return arena->New<FunctionValue>(&fun->declaration(),
-                                             &impl_witness->bindings());
-          }
+    if (auto* impl_witness = dyn_cast<ImplWitness>(witness)) {
+      if (std::optional<Nonnull<const Declaration*>> mem_decl =
+              FindMember(f, impl_witness->declaration().members());
+          mem_decl.has_value()) {
+        const auto& fun_decl = cast<FunctionDeclaration>(**mem_decl);
+        if (fun_decl.is_method()) {
+          return arena->New<BoundMethodValue>(&fun_decl, v,
+                                              &impl_witness->bindings());
         } else {
-          return CompilationError(source_loc)
-                 << "member " << f << " not in " << *witness;
+          // Class function.
+          auto* fun = cast<FunctionValue>(*fun_decl.constant_value());
+          return arena->New<FunctionValue>(&fun->declaration(),
+                                           &impl_witness->bindings());
         }
+      } else {
+        return CompilationError(source_loc)
+               << "member " << f << " not in " << *witness;
       }
-      case Value::Kind::SymbolicWitness: {
-        return RuntimeError(source_loc)
-               << "member lookup for " << f << " in symbolic " << *witness
-               << " not implemented yet";
-      }
-      default:
-        CARBON_FATAL() << "expected Witness, not " << *witness;
+    } else {
+      return RuntimeError(source_loc)
+             << "member lookup for " << f << " in symbolic " << *witness;
     }
   }
   switch (v->kind()) {
@@ -455,13 +448,29 @@ void Value::Print(llvm::raw_ostream& out) const {
     }
     case Value::Kind::ImplWitness: {
       const auto& witness = cast<ImplWitness>(*this);
-      out << "witness " << *witness.declaration().impl_type() << " as "
+      out << "witness for impl " << *witness.declaration().impl_type() << " as "
           << witness.declaration().interface();
       break;
     }
-    case Value::Kind::SymbolicWitness: {
-      const auto& witness = cast<SymbolicWitness>(*this);
-      out << "witness " << witness.impl_expression();
+    case Value::Kind::BindingWitness: {
+      const auto& witness = cast<BindingWitness>(*this);
+      out << "witness for " << *witness.binding()->type_var();
+      break;
+    }
+    case Value::Kind::ConstraintWitness: {
+      const auto& witness = cast<ConstraintWitness>(*this);
+      out << "(";
+      llvm::ListSeparator sep;
+      for (auto* elem : witness.witnesses()) {
+        out << sep << *elem;
+      }
+      out << ")";
+      break;
+    }
+    case Value::Kind::ConstraintImplWitness: {
+      const auto& witness = cast<ConstraintImplWitness>(*this);
+      out << "witness " << witness.index() << " of "
+          << *witness.constraint_witness();
       break;
     }
     case Value::Kind::ParameterizedEntityName:
@@ -767,7 +776,9 @@ auto TypeEqual(Nonnull<const Value*> t1, Nonnull<const Value*> t2,
                      << *t1 << "\n"
                      << *t2;
     case Value::Kind::ImplWitness:
-    case Value::Kind::SymbolicWitness:
+    case Value::Kind::BindingWitness:
+    case Value::Kind::ConstraintWitness:
+    case Value::Kind::ConstraintImplWitness:
       CARBON_FATAL() << "TypeEqual: unexpected Witness";
       break;
     case Value::Kind::AutoType:
@@ -868,7 +879,9 @@ auto ValueStructurallyEqual(
     case Value::Kind::InterfaceType:
     case Value::Kind::ConstraintType:
     case Value::Kind::ImplWitness:
-    case Value::Kind::SymbolicWitness:
+    case Value::Kind::BindingWitness:
+    case Value::Kind::ConstraintWitness:
+    case Value::Kind::ConstraintImplWitness:
     case Value::Kind::ChoiceType:
     case Value::Kind::ContinuationType:
     case Value::Kind::VariableType:
diff --git a/explorer/interpreter/value.h b/explorer/interpreter/value.h
index 8f830788bf2c..bb8800da8cab 100644
--- a/explorer/interpreter/value.h
+++ b/explorer/interpreter/value.h
@@ -50,7 +50,9 @@ class Value {
     TupleValue,
     UninitializedValue,
     ImplWitness,
-    SymbolicWitness,
+    BindingWitness,
+    ConstraintWitness,
+    ConstraintImplWitness,
     IntType,
     BoolType,
     TypeType,
@@ -831,7 +833,9 @@ class Witness : public Value {
  public:
   static auto classof(const Value* value) -> bool {
     return value->kind() == Kind::ImplWitness ||
-           value->kind() == Kind::SymbolicWitness;
+           value->kind() == Kind::BindingWitness ||
+           value->kind() == Kind::ConstraintWitness ||
+           value->kind() == Kind::ConstraintImplWitness;
   }
 };
 
@@ -869,23 +873,81 @@ class ImplWitness : public Witness {
   Nonnull<const Bindings*> bindings_ = Bindings::None();
 };
 
-// A witness table whose concrete value cannot be determined yet.
-//
-// These are used to represent symbolic witness values which can be computed at
-// runtime but whose values are not known statically.
-class SymbolicWitness : public Witness {
+// The symbolic witness corresponding to an unresolved impl binding.
+class BindingWitness : public Witness {
  public:
-  explicit SymbolicWitness(Nonnull<const Expression*> impl_expr)
-      : Witness(Kind::SymbolicWitness), impl_expr_(impl_expr) {}
+  // Construct a witness for an impl binding.
+  explicit BindingWitness(Nonnull<const ImplBinding*> binding)
+      : Witness(Kind::BindingWitness), binding_(binding) {}
 
   static auto classof(const Value* value) -> bool {
-    return value->kind() == Kind::SymbolicWitness;
+    return value->kind() == Kind::BindingWitness;
   }
 
-  auto impl_expression() const -> const Expression& { return *impl_expr_; }
+  auto binding() const -> Nonnull<const ImplBinding*> { return binding_; }
 
  private:
-  Nonnull<const Expression*> impl_expr_;
+  Nonnull<const ImplBinding*> binding_;
+};
+
+// A witness for a constraint type, expressed as a tuple of witnesses for the
+// individual impl constraints in the constraint type.
+class ConstraintWitness : public Witness {
+ public:
+  explicit ConstraintWitness(std::vector<Nonnull<const Witness*>> witnesses)
+      : Witness(Kind::ConstraintWitness), witnesses_(std::move(witnesses)) {}
+
+  static auto classof(const Value* value) -> bool {
+    return value->kind() == Kind::ConstraintWitness;
+  }
+
+  auto witnesses() const -> llvm::ArrayRef<Nonnull<const Witness*>> {
+    return witnesses_;
+  }
+
+ private:
+  std::vector<Nonnull<const Witness*>> witnesses_;
+};
+
+// A witness for an impl constraint in a constraint type, expressed in terms of
+// a symbolic witness for the constraint type.
+class ConstraintImplWitness : public Witness {
+ public:
+  // Make a witness for the given impl_constraint of the given `ConstraintType`
+  // witness. If we're indexing into a known tuple of witnesses, pull out the
+  // element.
+  static auto Make(Nonnull<Arena*> arena, Nonnull<const Witness*> witness,
+                   int index) -> Nonnull<const Witness*> {
+    if (auto* constraint_witness = llvm::dyn_cast<ConstraintWitness>(witness)) {
+      return constraint_witness->witnesses()[index];
+    }
+    return arena->New<ConstraintImplWitness>(witness, index);
+  }
+
+  explicit ConstraintImplWitness(Nonnull<const Witness*> constraint_witness,
+                                 int index)
+      : Witness(Kind::ConstraintImplWitness),
+        constraint_witness_(constraint_witness),
+        index_(index) {
+    CARBON_CHECK(!llvm::isa<ConstraintWitness>(constraint_witness))
+        << "should have resolved element from constraint witness";
+  }
+
+  static auto classof(const Value* value) -> bool {
+    return value->kind() == Kind::ConstraintImplWitness;
+  }
+
+  // Get the witness for the complete `ConstraintType`.
+  auto constraint_witness() const -> Nonnull<const Witness*> {
+    return constraint_witness_;
+  }
+
+  // Get the index of the impl constraint within the constraint type.
+  auto index() const -> int { return index_; }
+
+ private:
+  Nonnull<const Witness*> constraint_witness_;
+  int index_;
 };
 
 // A choice type.
diff --git a/explorer/syntax/parser.ypp b/explorer/syntax/parser.ypp
index 7821d5bb6a79..c2b675e1cc04 100644
--- a/explorer/syntax/parser.ypp
+++ b/explorer/syntax/parser.ypp
@@ -1172,13 +1172,7 @@ declaration:
     }
 | INTERFACE identifier type_params LEFT_CURLY_BRACE interface_body RIGHT_CURLY_BRACE
     {
-      // TODO: Type of `Self` should be the interface being declared, not
-      // `Type`.
-      auto ty_ty = arena -> New<TypeTypeLiteral>(context.source_loc());
-      // TODO: Should this be switched to use a `SelfDeclaration` instead?
-      auto self =
-          arena -> New<GenericBinding>(context.source_loc(), "Self", ty_ty);
-      $$ = arena->New<InterfaceDeclaration>(context.source_loc(), $2, $3, self,
+      $$ = arena->New<InterfaceDeclaration>(arena, context.source_loc(), $2, $3,
                                             $5);
     }
 | impl_kind IMPL impl_deduced_params impl_type AS type_or_where_expression LEFT_CURLY_BRACE impl_body RIGHT_CURLY_BRACE