diff --git a/explorer/ast/expression.cpp b/explorer/ast/expression.cpp
index 501055173b4b..0d5522aa1848 100644
--- a/explorer/ast/expression.cpp
+++ b/explorer/ast/expression.cpp
@@ -258,8 +258,9 @@ void Expression::Print(llvm::raw_ostream& out) const {
       break;
     }
     case ExpressionKind::InstantiateImpl: {
-      const auto& inst_impl = cast<InstantiateImpl>(*this);
-      out << "instantiate " << *inst_impl.generic_impl();
+      // TODO: For layering reasons, we can't print out the witness and
+      // argument values from here.
+      out << "instantiate impl";
       break;
     }
     case ExpressionKind::UnimplementedExpression: {
diff --git a/explorer/ast/expression.h b/explorer/ast/expression.h
index 67f923e29b04..72c80205fe00 100644
--- a/explorer/ast/expression.h
+++ b/explorer/ast/expression.h
@@ -26,6 +26,7 @@
 namespace Carbon {
 
 class Value;
+class Witness;
 class MemberName;
 class VariableType;
 class InterfaceType;
@@ -243,15 +244,13 @@ class SimpleMemberAccessExpression : public Expression {
   // Can only be called once, during typechecking.
   void set_is_field_addr_me_method() { is_field_addr_me_method_ = true; }
 
-  // If `object` has a generic type, returns the `ImplBinding` that
-  // identifies its witness table. Otherwise, returns `std::nullopt`. Should not
+  // If `object` has a generic type, returns the witness value, which might be
+  // either concrete or symbolic. Otherwise, returns `std::nullopt`. Should not
   // be called before typechecking.
-  auto impl() const -> std::optional<Nonnull<const Expression*>> {
-    return impl_;
-  }
+  auto impl() const -> std::optional<Nonnull<const Witness*>> { return impl_; }
 
   // Can only be called once, during typechecking.
-  void set_impl(Nonnull<const Expression*> impl) {
+  void set_impl(Nonnull<const Witness*> impl) {
     CARBON_CHECK(!impl_.has_value());
     impl_ = impl;
   }
@@ -275,7 +274,7 @@ class SimpleMemberAccessExpression : public Expression {
   std::string member_name_;
   std::optional<Member> member_;
   bool is_field_addr_me_method_ = false;
-  std::optional<Nonnull<const Expression*>> impl_;
+  std::optional<Nonnull<const Witness*>> impl_;
   std::optional<Nonnull<const InterfaceType*>> found_in_interface_;
 };
 
@@ -323,14 +322,12 @@ class CompoundMemberAccessExpression : public Expression {
     member_ = member;
   }
 
-  // Returns the expression to use to compute the witness table, if this
-  // expression names an interface member.
-  auto impl() const -> std::optional<Nonnull<const Expression*>> {
-    return impl_;
-  }
+  // If this expression names an interface member, returns the witness value,
+  // which might be symbolic.
+  auto impl() const -> std::optional<Nonnull<const Witness*>> { return impl_; }
 
   // Can only be called once, during typechecking.
-  void set_impl(Nonnull<const Expression*> impl) {
+  void set_impl(Nonnull<const Witness*> impl) {
     CARBON_CHECK(!impl_.has_value());
     impl_ = impl;
   }
@@ -342,7 +339,7 @@ class CompoundMemberAccessExpression : public Expression {
   Nonnull<Expression*> object_;
   Nonnull<Expression*> path_;
   std::optional<Nonnull<const MemberName*>> member_;
-  std::optional<Nonnull<const Expression*>> impl_;
+  std::optional<Nonnull<const Witness*>> impl_;
 };
 
 class IndexExpression : public Expression {
@@ -539,8 +536,6 @@ class OperatorExpression : public Expression {
   std::optional<Nonnull<const Expression*>> rewritten_form_;
 };
 
-using ImplExpMap = std::map<Nonnull<const ImplBinding*>, Nonnull<Expression*>>;
-
 class CallExpression : public Expression {
  public:
   explicit CallExpression(SourceLocation source_loc,
@@ -548,7 +543,8 @@ class CallExpression : public Expression {
                           Nonnull<Expression*> argument)
       : Expression(AstNodeKind::CallExpression, source_loc),
         function_(function),
-        argument_(argument) {}
+        argument_(argument),
+        bindings_({}, {}) {}
 
   static auto classof(const AstNode* node) -> bool {
     return InheritsFromCallExpression(node->kind());
@@ -559,23 +555,20 @@ class CallExpression : public Expression {
   auto argument() const -> const Expression& { return *argument_; }
   auto argument() -> Expression& { return *argument_; }
 
-  // Maps each of `function`'s impl bindings to an expression
-  // that constructs a witness table.
-  // Should not be called before typechecking, or if `function` is not
-  // a generic function.
-  auto impls() const -> const ImplExpMap& { return impls_; }
+  auto bindings() -> const Bindings& { return bindings_; }
 
   // Can only be called once, during typechecking.
-  void set_impls(const ImplExpMap& impls) {
-    CARBON_CHECK(impls_.empty());
-    impls_ = impls;
+  void set_bindings(Bindings bindings) {
+    CARBON_CHECK(bindings_.args().empty() && bindings_.witnesses().empty());
+    bindings_ = std::move(bindings);
   }
 
-  auto deduced_args() const -> const BindingMap& { return deduced_args_; }
+  auto deduced_args() const -> const BindingMap& { return bindings_.args(); }
 
-  void set_deduced_args(const BindingMap& deduced_args) {
-    deduced_args_ = deduced_args;
-  }
+  // Maps each of `function`'s impl bindings to a witness.
+  // Should not be called before typechecking, or if `function` is not
+  // a generic function.
+  auto impls() const -> const ImplWitnessMap& { return bindings_.witnesses(); }
 
   // Can only be called by type-checking, if a conversion was required.
   void set_argument(Nonnull<Expression*> argument) { argument_ = argument; }
@@ -583,8 +576,7 @@ class CallExpression : public Expression {
  private:
   Nonnull<Expression*> function_;
   Nonnull<Expression*> argument_;
-  ImplExpMap impls_;
-  BindingMap deduced_args_;
+  Bindings bindings_;
 };
 
 class FunctionTypeLiteral : public Expression {
@@ -867,27 +859,25 @@ class InstantiateImpl : public Expression {
   using ImplementsCarbonValueNode = void;
 
   explicit InstantiateImpl(SourceLocation source_loc,
-                           Nonnull<Expression*> generic_impl,
-                           const BindingMap& type_args, const ImplExpMap& impls)
+                           Nonnull<const Witness*> generic_impl,
+                           Bindings bindings)
       : Expression(AstNodeKind::InstantiateImpl, source_loc),
         generic_impl_(generic_impl),
-        type_args_(type_args),
-        impls_(impls) {}
+        bindings_(std::move(bindings)) {}
 
   static auto classof(const AstNode* node) -> bool {
     return InheritsFromInstantiateImpl(node->kind());
   }
-  auto generic_impl() const -> Nonnull<Expression*> { return generic_impl_; }
-  auto type_args() const -> const BindingMap& { return type_args_; }
+  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 ImplExpMap& { return impls_; }
+  auto impls() const -> const ImplWitnessMap& { return bindings_.witnesses(); }
 
  private:
-  Nonnull<Expression*> generic_impl_;
-  BindingMap type_args_;
-  ImplExpMap impls_;
+  Nonnull<const Witness*> generic_impl_;
+  Bindings bindings_;
 };
 
 // An expression whose semantics have not been implemented. This can be used
diff --git a/explorer/interpreter/action.cpp b/explorer/interpreter/action.cpp
index 62f496652874..3c21de3fc4f1 100644
--- a/explorer/interpreter/action.cpp
+++ b/explorer/interpreter/action.cpp
@@ -116,6 +116,9 @@ void Action::Print(llvm::raw_ostream& out) const {
     case Action::Kind::ExpressionAction:
       out << cast<ExpressionAction>(*this).expression() << " ";
       break;
+    case Action::Kind::WitnessAction:
+      out << *cast<WitnessAction>(*this).witness() << " ";
+      break;
     case Action::Kind::PatternAction:
       out << cast<PatternAction>(*this).pattern() << " ";
       break;
diff --git a/explorer/interpreter/action.h b/explorer/interpreter/action.h
index ee0a8dc6d69a..05912c55290f 100644
--- a/explorer/interpreter/action.h
+++ b/explorer/interpreter/action.h
@@ -113,6 +113,7 @@ class Action {
   enum class Kind {
     LValAction,
     ExpressionAction,
+    WitnessAction,
     PatternAction,
     StatementAction,
     DeclarationAction,
@@ -218,6 +219,24 @@ class ExpressionAction : public Action {
   Nonnull<const Expression*> expression_;
 };
 
+// An Action which implements evaluation of a Witness to resolve it in the
+// local context.
+class WitnessAction : public Action {
+ public:
+  explicit WitnessAction(Nonnull<const Witness*> witness)
+      : Action(Kind::WitnessAction), witness_(witness) {}
+
+  static auto classof(const Action* action) -> bool {
+    return action->kind() == Kind::WitnessAction;
+  }
+
+  // The Witness this Action resolves.
+  auto witness() const -> Nonnull<const Witness*> { return witness_; }
+
+ private:
+  Nonnull<const Witness*> witness_;
+};
+
 // An Action which implements evaluation of a Pattern. The result is expressed
 // as a Value.
 class PatternAction : public Action {
diff --git a/explorer/interpreter/action_stack.cpp b/explorer/interpreter/action_stack.cpp
index 4ce6fa3866ea..605121d7cdf0 100644
--- a/explorer/interpreter/action_stack.cpp
+++ b/explorer/interpreter/action_stack.cpp
@@ -126,23 +126,47 @@ void ActionStack::InitializeFragment(ContinuationValue::StackFragment& fragment,
   fragment.StoreReversed(std::move(reversed_todo));
 }
 
+namespace {
+// The way in which FinishAction should be called for a particular kind of
+// action.
+enum class FinishActionKind {
+  // FinishAction should not be passed a value.
+  NoValue,
+  // FinishAction should be passed a value.
+  Value,
+  // FinishAction should not be called. The Action needs custom handling.
+  NeverCalled,
+};
+}  // namespace
+
+static auto FinishActionKindFor(Action::Kind kind) -> FinishActionKind {
+  switch (kind) {
+    case Action::Kind::ExpressionAction:
+    case Action::Kind::WitnessAction:
+    case Action::Kind::LValAction:
+    case Action::Kind::PatternAction:
+      return FinishActionKind::Value;
+    case Action::Kind::StatementAction:
+    case Action::Kind::DeclarationAction:
+    case Action::Kind::RecursiveAction:
+      return FinishActionKind::NoValue;
+    case Action::Kind::ScopeAction:
+    case Action::Kind::CleanUpAction:
+      return FinishActionKind::NeverCalled;
+  }
+}
+
 auto ActionStack::FinishAction() -> ErrorOr<Success> {
   std::stack<std::unique_ptr<Action>> scopes_to_destroy;
   std::unique_ptr<Action> act = todo_.Pop();
-  switch (act->kind()) {
-    case Action::Kind::CleanUpAction:
-    case Action::Kind::ExpressionAction:
-    case Action::Kind::LValAction:
-    case Action::Kind::PatternAction:
+  switch (FinishActionKindFor(act->kind())) {
+    case FinishActionKind::Value:
       CARBON_FATAL() << "This kind of action must produce a result: " << *act;
-    case Action::Kind::ScopeAction:
-      CARBON_FATAL() << "ScopeAction at top of stack";
-    case Action::Kind::StatementAction:
-    case Action::Kind::DeclarationAction:
-    case Action::Kind::RecursiveAction: {
+    case FinishActionKind::NeverCalled:
+      CARBON_FATAL() << "Should not call FinishAction for: " << *act;
+    case FinishActionKind::NoValue:
       PopScopes(scopes_to_destroy);
       break;
-    }
   }
   PushCleanUpAction(std::move(act));
   PushCleanUpActions(std::move(scopes_to_destroy));
@@ -153,17 +177,12 @@ auto ActionStack::FinishAction(Nonnull<const Value*> result)
     -> ErrorOr<Success> {
   std::stack<std::unique_ptr<Action>> scopes_to_destroy;
   std::unique_ptr<Action> act = todo_.Pop();
-  switch (act->kind()) {
-    case Action::Kind::CleanUpAction:
-    case Action::Kind::StatementAction:
-    case Action::Kind::DeclarationAction:
-    case Action::Kind::RecursiveAction:
-      CARBON_FATAL() << "This kind of Action cannot produce results: " << *act;
-    case Action::Kind::ScopeAction:
-      CARBON_FATAL() << "ScopeAction at top of stack";
-    case Action::Kind::ExpressionAction:
-    case Action::Kind::LValAction:
-    case Action::Kind::PatternAction:
+  switch (FinishActionKindFor(act->kind())) {
+    case FinishActionKind::NoValue:
+      CARBON_FATAL() << "This kind of action cannot produce results: " << *act;
+    case FinishActionKind::NeverCalled:
+      CARBON_FATAL() << "Should not call FinishAction for: " << *act;
+    case FinishActionKind::Value:
       PopScopes(scopes_to_destroy);
       SetResult(result);
       break;
@@ -192,8 +211,9 @@ auto ActionStack::Spawn(std::unique_ptr<Action> child, RuntimeScope scope)
 auto ActionStack::ReplaceWith(std::unique_ptr<Action> replacement)
     -> ErrorOr<Success> {
   std::unique_ptr<Action> old = todo_.Pop();
-  CARBON_CHECK(replacement->kind() == old->kind())
-      << "ReplaceWith can't change action kind";
+  CARBON_CHECK(FinishActionKindFor(old->kind()) ==
+               FinishActionKindFor(replacement->kind()))
+      << "Can't replace action " << *old << " with " << *replacement;
   todo_.Push(std::move(replacement));
   return Success();
 }
diff --git a/explorer/interpreter/action_stack.h b/explorer/interpreter/action_stack.h
index 995cce42e699..fb13e59c3753 100644
--- a/explorer/interpreter/action_stack.h
+++ b/explorer/interpreter/action_stack.h
@@ -88,8 +88,8 @@ class ActionStack {
   auto Spawn(std::unique_ptr<Action> child) -> ErrorOr<Success>;
   auto Spawn(std::unique_ptr<Action> child, RuntimeScope scope)
       -> ErrorOr<Success>;
-  // Replace the current action with another action of the same kind and run it
-  // next.
+  // Replace the current action with another action that produces the same kind
+  // of result and run it next.
   auto ReplaceWith(std::unique_ptr<Action> child) -> ErrorOr<Success>;
 
   // Start a new recursive action.
diff --git a/explorer/interpreter/impl_scope.cpp b/explorer/interpreter/impl_scope.cpp
index 0d3b5dc73842..ae6ff6656399 100644
--- a/explorer/interpreter/impl_scope.cpp
+++ b/explorer/interpreter/impl_scope.cpp
@@ -15,16 +15,16 @@ using llvm::dyn_cast;
 namespace Carbon {
 
 void ImplScope::Add(Nonnull<const Value*> iface, Nonnull<const Value*> type,
-                    Nonnull<Expression*> impl,
+                    Nonnull<const Witness*> witness,
                     const TypeChecker& type_checker) {
-  Add(iface, {}, type, {}, impl, type_checker);
+  Add(iface, {}, type, {}, witness, type_checker);
 }
 
 void ImplScope::Add(Nonnull<const Value*> iface,
                     llvm::ArrayRef<Nonnull<const GenericBinding*>> deduced,
                     Nonnull<const Value*> type,
                     llvm::ArrayRef<Nonnull<const ImplBinding*>> impl_bindings,
-                    Nonnull<Expression*> impl_expr,
+                    Nonnull<const Witness*> witness,
                     const TypeChecker& type_checker) {
   if (auto* orig_constraint = dyn_cast<ConstraintType>(iface)) {
     BindingMap map;
@@ -34,7 +34,7 @@ void ImplScope::Add(Nonnull<const Value*> iface,
     for (size_t i = 0; i != constraint->impl_constraints().size(); ++i) {
       ConstraintType::ImplConstraint impl = constraint->impl_constraints()[i];
       Add(impl.interface, deduced, impl.type, impl_bindings,
-          type_checker.MakeConstraintWitnessAccess(impl_expr, i), type_checker);
+          type_checker.MakeConstraintWitnessAccess(witness, i), type_checker);
     }
     // A parameterized impl declaration doesn't contribute any equality
     // constraints to the scope. Instead, we'll resolve the equality
@@ -51,7 +51,7 @@ void ImplScope::Add(Nonnull<const Value*> iface,
                     .deduced = deduced,
                     .type = type,
                     .impl_bindings = impl_bindings,
-                    .impl = impl_expr});
+                    .witness = witness});
 }
 
 void ImplScope::AddParent(Nonnull<const ImplScope*> parent) {
@@ -62,17 +62,17 @@ auto ImplScope::Resolve(Nonnull<const Value*> constraint_type,
                         Nonnull<const Value*> impl_type,
                         SourceLocation source_loc,
                         const TypeChecker& type_checker) const
-    -> ErrorOr<Nonnull<Expression*>> {
+    -> ErrorOr<Nonnull<const Witness*>> {
   if (const auto* iface_type = dyn_cast<InterfaceType>(constraint_type)) {
     return ResolveInterface(iface_type, impl_type, source_loc, type_checker);
   }
   if (const auto* constraint = dyn_cast<ConstraintType>(constraint_type)) {
-    std::vector<Nonnull<Expression*>> witnesses;
+    std::vector<Nonnull<const Witness*>> witnesses;
     BindingMap map;
     map[constraint->self_binding()] = impl_type;
     for (auto impl : constraint->impl_constraints()) {
       CARBON_ASSIGN_OR_RETURN(
-          Nonnull<Expression*> result,
+          Nonnull<const Witness*> result,
           ResolveInterface(
               cast<InterfaceType>(type_checker.Substitute(map, impl.interface)),
               type_checker.Substitute(map, impl.type), source_loc,
@@ -106,9 +106,9 @@ auto ImplScope::ResolveInterface(Nonnull<const InterfaceType*> iface_type,
                                  Nonnull<const Value*> type,
                                  SourceLocation source_loc,
                                  const TypeChecker& type_checker) const
-    -> ErrorOr<Nonnull<Expression*>> {
+    -> ErrorOr<Nonnull<const Witness*>> {
   CARBON_ASSIGN_OR_RETURN(
-      std::optional<Nonnull<Expression*>> result,
+      std::optional<Nonnull<const Witness*>> result,
       TryResolve(iface_type, type, source_loc, *this, type_checker));
   if (!result.has_value()) {
     return CompilationError(source_loc) << "could not find implementation of "
@@ -122,14 +122,15 @@ auto ImplScope::TryResolve(Nonnull<const InterfaceType*> iface_type,
                            SourceLocation source_loc,
                            const ImplScope& original_scope,
                            const TypeChecker& type_checker) const
-    -> ErrorOr<std::optional<Nonnull<Expression*>>> {
+    -> ErrorOr<std::optional<Nonnull<const Witness*>>> {
   CARBON_ASSIGN_OR_RETURN(
-      std::optional<Nonnull<Expression*>> result,
+      std::optional<Nonnull<const Witness*>> result,
       ResolveHere(iface_type, type, source_loc, original_scope, type_checker));
   for (Nonnull<const ImplScope*> parent : parent_scopes_) {
-    CARBON_ASSIGN_OR_RETURN(std::optional<Nonnull<Expression*>> parent_result,
-                            parent->TryResolve(iface_type, type, source_loc,
-                                               original_scope, type_checker));
+    CARBON_ASSIGN_OR_RETURN(
+        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 CompilationError(source_loc) << "ambiguous implementations of "
@@ -147,10 +148,10 @@ auto ImplScope::ResolveHere(Nonnull<const InterfaceType*> iface_type,
                             SourceLocation source_loc,
                             const ImplScope& original_scope,
                             const TypeChecker& type_checker) const
-    -> ErrorOr<std::optional<Nonnull<Expression*>>> {
-  std::optional<Nonnull<Expression*>> result = std::nullopt;
+    -> ErrorOr<std::optional<Nonnull<const Witness*>>> {
+  std::optional<Nonnull<const Witness*>> result = std::nullopt;
   for (const Impl& impl : impls_) {
-    std::optional<Nonnull<Expression*>> m = type_checker.MatchImpl(
+    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()) {
diff --git a/explorer/interpreter/impl_scope.h b/explorer/interpreter/impl_scope.h
index 123b1eecdb87..cb80b6b7189b 100644
--- a/explorer/interpreter/impl_scope.h
+++ b/explorer/interpreter/impl_scope.h
@@ -44,14 +44,14 @@ class ImplScope {
  public:
   // Associates `iface` and `type` with the `impl` in this scope.
   void Add(Nonnull<const Value*> iface, Nonnull<const Value*> type,
-           Nonnull<Expression*> impl, const TypeChecker& type_checker);
+           Nonnull<const Witness*> witness, const TypeChecker& type_checker);
   // For a parameterized impl, associates `iface` and `type`
   // with the `impl` in this scope.
   void Add(Nonnull<const Value*> iface,
            llvm::ArrayRef<Nonnull<const GenericBinding*>> deduced,
            Nonnull<const Value*> type,
            llvm::ArrayRef<Nonnull<const ImplBinding*>> impl_bindings,
-           Nonnull<Expression*> impl, const TypeChecker& type_checker);
+           Nonnull<const Witness*> witness, const TypeChecker& type_checker);
 
   // Add a type equality constraint.
   void AddEqualityConstraint(Nonnull<const EqualityConstraint*> equal) {
@@ -67,7 +67,7 @@ class ImplScope {
   // at `source_loc` there isn't exactly one matching impl.
   auto Resolve(Nonnull<const Value*> constraint, Nonnull<const Value*> type,
                SourceLocation source_loc, const TypeChecker& type_checker) const
-      -> ErrorOr<Nonnull<Expression*>>;
+      -> ErrorOr<Nonnull<const Witness*>>;
 
   // Visits the values that are a single step away from `value` according to an
   // equality constraint that is in scope. That is, the values `v` such that we
@@ -94,7 +94,7 @@ class ImplScope {
     std::vector<Nonnull<const GenericBinding*>> deduced;
     Nonnull<const Value*> type;
     std::vector<Nonnull<const ImplBinding*>> impl_bindings;
-    Nonnull<Expression*> impl;
+    Nonnull<const Witness*> witness;
   };
 
  private:
@@ -104,7 +104,7 @@ class ImplScope {
   auto ResolveInterface(Nonnull<const InterfaceType*> iface,
                         Nonnull<const Value*> type, SourceLocation source_loc,
                         const TypeChecker& type_checker) const
-      -> ErrorOr<Nonnull<Expression*>>;
+      -> ErrorOr<Nonnull<const Witness*>>;
 
   // Returns the associated impl for the given `iface` and `type` in
   // the ancestor graph of this scope, returns std::nullopt if there
@@ -116,7 +116,7 @@ class ImplScope {
                   Nonnull<const Value*> type, SourceLocation source_loc,
                   const ImplScope& original_scope,
                   const TypeChecker& type_checker) const
-      -> ErrorOr<std::optional<Nonnull<Expression*>>>;
+      -> ErrorOr<std::optional<Nonnull<const Witness*>>>;
 
   // Returns the associated impl for the given `iface` and `type` in
   // this scope, returns std::nullopt if there is none, or reports
@@ -128,7 +128,7 @@ class ImplScope {
                    Nonnull<const Value*> impl_type, SourceLocation source_loc,
                    const ImplScope& original_scope,
                    const TypeChecker& type_checker) const
-      -> ErrorOr<std::optional<Nonnull<Expression*>>>;
+      -> ErrorOr<std::optional<Nonnull<const Witness*>>>;
 
   std::vector<Impl> impls_;
   std::vector<Nonnull<const EqualityConstraint*>> equalities_;
diff --git a/explorer/interpreter/interpreter.cpp b/explorer/interpreter/interpreter.cpp
index ed9cbeb769a8..471bf9efe6f2 100644
--- a/explorer/interpreter/interpreter.cpp
+++ b/explorer/interpreter/interpreter.cpp
@@ -79,6 +79,8 @@ class Interpreter {
   auto StepExp() -> ErrorOr<Success>;
   // State transitions for lvalues.
   auto StepLvalue() -> ErrorOr<Success>;
+  // State transitions for witnesses.
+  auto StepWitness() -> ErrorOr<Success>;
   // State transitions for patterns.
   auto StepPattern() -> ErrorOr<Success>;
   // State transition for statements.
@@ -897,7 +899,7 @@ auto Interpreter::StepExp() -> ErrorOr<Success> {
       const InstantiateImpl& inst_impl = cast<InstantiateImpl>(exp);
       if (act.pos() == 0) {
         return todo_.Spawn(
-            std::make_unique<ExpressionAction>(inst_impl.generic_impl()));
+            std::make_unique<WitnessAction>(inst_impl.generic_impl()));
       }
       if (act.pos() == 1 && isa<SymbolicWitness>(act.results()[0])) {
         return todo_.FinishAction(arena_->New<SymbolicWitness>(&exp));
@@ -905,7 +907,8 @@ auto Interpreter::StepExp() -> ErrorOr<Success> {
       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<ExpressionAction>(iter->second));
+        return todo_.Spawn(
+            std::make_unique<WitnessAction>(cast<Witness>(iter->second)));
       } else {
         Nonnull<const ImplWitness*> generic_witness =
             cast<ImplWitness>(act.results()[0]);
@@ -997,7 +1000,7 @@ auto Interpreter::StepExp() -> ErrorOr<Success> {
         // Next, if we're accessing an interface member, evaluate the `impl`
         // expression to find the corresponding witness.
         return todo_.Spawn(
-            std::make_unique<ExpressionAction>(access.impl().value()));
+            std::make_unique<WitnessAction>(access.impl().value()));
       } else {
         // Finally, produce the result.
         std::optional<Nonnull<const InterfaceType*>> found_in_interface =
@@ -1058,7 +1061,7 @@ auto Interpreter::StepExp() -> ErrorOr<Success> {
         // Next, if we're accessing an interface member, evaluate the `impl`
         // expression to find the corresponding witness.
         return todo_.Spawn(
-            std::make_unique<ExpressionAction>(access.impl().value()));
+            std::make_unique<WitnessAction>(access.impl().value()));
       } else {
         // Finally, produce the result.
         std::optional<Nonnull<const InterfaceType*>> found_in_interface =
@@ -1181,7 +1184,8 @@ auto Interpreter::StepExp() -> ErrorOr<Success> {
       } else if (num_impls > 0 && act.pos() < 2 + int(num_impls)) {
         auto iter = call.impls().begin();
         std::advance(iter, act.pos() - 2);
-        return todo_.Spawn(std::make_unique<ExpressionAction>(iter->second));
+        return todo_.Spawn(
+            std::make_unique<WitnessAction>(cast<Witness>(iter->second)));
       } else if (act.pos() == 2 + int(num_impls)) {
         //    { { v2 :: v1([]) :: C, E, F} :: S, H}
         // -> { {C',E',F'} :: {C, E, F} :: S, H}
@@ -1435,6 +1439,26 @@ auto Interpreter::StepExp() -> ErrorOr<Success> {
   }  // switch (exp->kind)
 }
 
+auto Interpreter::StepWitness() -> ErrorOr<Success> {
+  Action& act = todo_.CurrentAction();
+  const Witness* witness = cast<WitnessAction>(act).witness();
+  if (trace_stream_) {
+    **trace_stream_ << "--- step witness " << *witness << " ." << act.pos()
+                    << ". --->\n";
+  }
+  switch (witness->kind()) {
+    case Value::Kind::SymbolicWitness:
+      return todo_.ReplaceWith(std::make_unique<ExpressionAction>(
+          &cast<SymbolicWitness>(witness)->impl_expression()));
+
+    case Value::Kind::ImplWitness:
+      return todo_.FinishAction(witness);
+
+    default:
+      CARBON_FATAL() << "unexpected kind of witness " << *witness;
+  }
+}
+
 auto Interpreter::StepPattern() -> ErrorOr<Success> {
   Action& act = todo_.CurrentAction();
   const Pattern& pattern = cast<PatternAction>(act).pattern();
@@ -1940,6 +1964,9 @@ auto Interpreter::Step() -> ErrorOr<Success> {
     case Action::Kind::ExpressionAction:
       CARBON_RETURN_IF_ERROR(StepExp());
       break;
+    case Action::Kind::WitnessAction:
+      CARBON_RETURN_IF_ERROR(StepWitness());
+      break;
     case Action::Kind::PatternAction:
       CARBON_RETURN_IF_ERROR(StepPattern());
       break;
diff --git a/explorer/interpreter/type_checker.cpp b/explorer/interpreter/type_checker.cpp
index 057fe1560c8c..5fe920ef3de5 100644
--- a/explorer/interpreter/type_checker.cpp
+++ b/explorer/interpreter/type_checker.cpp
@@ -48,13 +48,10 @@ struct TypeChecker::SingleStepEqualityContext : public EqualityContext {
     }
 
     CARBON_ASSIGN_OR_RETURN(
-        Nonnull<const Expression*> witness_expr,
+        Nonnull<const Witness*> witness,
         impl_scope_->Resolve(&assoc->interface(), &assoc->base(), source_loc,
                              *type_checker_));
-    CARBON_ASSIGN_OR_RETURN(Nonnull<const Value*> witness_value,
-                            InterpExp(witness_expr, type_checker_->arena_,
-                                      type_checker_->trace_stream_));
-    impl_witness = dyn_cast<ImplWitness>(witness_value);
+    impl_witness = dyn_cast<ImplWitness>(witness);
     if (impl_witness) {
       return impl_witness;
     }
@@ -1088,6 +1085,7 @@ auto TypeChecker::Substitute(
         Nonnull<ImplBinding*> new_ib =
             arena_->New<ImplBinding>(ib->source_loc(), bind_map[ib->type_var()],
                                      Substitute(new_dict, ib->interface()));
+        // TODO: Should we set a symbolic identity on this impl binding?
         new_ib->set_original(ib->original());
         impl_bindings.push_back(new_ib);
       }
@@ -1207,7 +1205,7 @@ auto TypeChecker::MatchImpl(const InterfaceType& iface,
                             const ImplScope::Impl& impl,
                             const ImplScope& impl_scope,
                             SourceLocation source_loc) const
-    -> std::optional<Nonnull<Expression*>> {
+    -> std::optional<Nonnull<const Witness*>> {
   if (trace_stream_) {
     **trace_stream_ << "MatchImpl: looking for " << *impl_type << " as "
                     << iface << "\n";
@@ -1251,7 +1249,7 @@ auto TypeChecker::MatchImpl(const InterfaceType& iface,
 
   // Ensure the constraints on the `impl` are satisfied by the deduced
   // arguments.
-  ImplExpMap impls;
+  ImplWitnessMap impls;
   if (ErrorOr<Success> e = SatisfyImpls(impl.impl_bindings, impl_scope,
                                         source_loc, deduced_args, impls);
       !e.ok()) {
@@ -1265,31 +1263,45 @@ auto TypeChecker::MatchImpl(const InterfaceType& iface,
     **trace_stream_ << "matched with " << *impl.type << " as "
                     << *impl.interface << "\n\n";
   }
-  return deduced_args.empty() ? impl.impl
-                              : arena_->New<InstantiateImpl>(
-                                    source_loc, impl.impl, deduced_args, impls);
+  return deduced_args.empty()
+             ? impl.witness
+             : arena_->New<SymbolicWitness>(arena_->New<InstantiateImpl>(
+                   source_loc, impl.witness,
+                   Bindings(std::move(deduced_args), std::move(impls))));
 }
 
 auto TypeChecker::MakeConstraintWitness(
     const ConstraintType& constraint,
-    std::vector<Nonnull<Expression*>> impl_constraint_witnesses,
-    SourceLocation source_loc) const -> Nonnull<Expression*> {
-  return arena_->New<TupleLiteral>(source_loc,
-                                   std::move(impl_constraint_witnesses));
+    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)));
 }
 
-auto TypeChecker::MakeConstraintWitnessAccess(Nonnull<Expression*> witness,
+auto TypeChecker::MakeConstraintWitnessAccess(Nonnull<const Witness*> witness,
                                               size_t impl_offset) const
-    -> Nonnull<Expression*> {
-  return arena_->New<IndexExpression>(
-      witness->source_loc(), witness,
-      arena_->New<IntLiteral>(witness->source_loc(), impl_offset));
+    -> 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)));
 }
 
 auto TypeChecker::SatisfyImpls(
     llvm::ArrayRef<Nonnull<const ImplBinding*>> impl_bindings,
     const ImplScope& impl_scope, SourceLocation source_loc,
-    const BindingMap& deduced_type_args, ImplExpMap& impls) const
+    const BindingMap& deduced_type_args, ImplWitnessMap& impls) const
     -> ErrorOr<Success> {
   for (Nonnull<const ImplBinding*> impl_binding : impl_bindings) {
     Nonnull<const Value*> interface =
@@ -1297,11 +1309,11 @@ auto TypeChecker::SatisfyImpls(
     CARBON_CHECK(deduced_type_args.find(impl_binding->type_var()) !=
                  deduced_type_args.end());
     CARBON_ASSIGN_OR_RETURN(
-        Nonnull<Expression*> impl,
+        Nonnull<const Value*> impl,
         impl_scope.Resolve(interface,
                            deduced_type_args.at(impl_binding->type_var()),
                            source_loc, *this));
-    impls.emplace(impl_binding, impl);
+    impls.insert({impl_binding, impl});
   }
   return Success();
 }
@@ -1377,7 +1389,6 @@ auto TypeChecker::DeduceCallBindings(
   CARBON_CHECK(generic_params.empty())
       << "did not find all generic parameters in parameter list";
 
-  call.set_deduced_args(generic_bindings);
   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.
@@ -1391,15 +1402,16 @@ auto TypeChecker::DeduceCallBindings(
   }
 
   // Find impls for all the required impl bindings.
-  ImplExpMap impls;
+  ImplWitnessMap impls;
   CARBON_RETURN_IF_ERROR(SatisfyImpls(
       impl_bindings, impl_scope, call.source_loc(), generic_bindings, impls));
-  call.set_impls(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(generic_bindings, params_type);
+  Nonnull<const Value*> param_type =
+      Substitute(call.bindings().args(), params_type);
 
   // Convert the arguments to the deduced and substituted parameter type.
   CARBON_ASSIGN_OR_RETURN(
@@ -1661,7 +1673,7 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
           access.set_static_type(inst_member_type);
 
           CARBON_ASSIGN_OR_RETURN(
-              Nonnull<Expression*> impl,
+              Nonnull<const Witness*> impl,
               impl_scope.Resolve(result.interface, &object_type,
                                  e->source_loc(), *this));
           access.set_impl(impl);
@@ -1684,7 +1696,7 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
               ConstraintLookupResult result,
               LookupInConstraint(e->source_loc(), "member access", &object_type,
                                  access.member_name()));
-          CARBON_ASSIGN_OR_RETURN(Nonnull<Expression*> impl,
+          CARBON_ASSIGN_OR_RETURN(Nonnull<const Witness*> impl,
                                   impl_scope.Resolve(result.interface, type,
                                                      e->source_loc(), *this));
           access.set_member(Member(result.member));
@@ -1884,7 +1896,7 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
       if (std::optional<Nonnull<const Value*>> iface =
               member_name.interface()) {
         CARBON_ASSIGN_OR_RETURN(
-            Nonnull<Expression*> impl,
+            Nonnull<const Witness*> impl,
             impl_scope.Resolve(*iface, *base_type, e->source_loc(), *this));
         access.set_impl(impl);
       }
@@ -2652,20 +2664,21 @@ void TypeChecker::BringImplsIntoScope(
   }
 }
 
-auto TypeChecker::CreateImplReference(Nonnull<const ImplBinding*> impl_binding)
-    -> Nonnull<Expression*> {
+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 impl_id;
+  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());
+  CARBON_CHECK(impl_binding->type_var()->symbolic_identity().has_value() &&
+               impl_binding->symbolic_identity().has_value());
   impl_scope.Add(impl_binding->interface(),
                  *impl_binding->type_var()->symbolic_identity(),
-                 CreateImplReference(impl_binding), *this);
+                 cast<Witness>(*impl_binding->symbolic_identity()), *this);
 }
 
 auto TypeChecker::TypeCheckTypeExp(Nonnull<Expression*> type_expression,
@@ -2804,7 +2817,7 @@ auto TypeChecker::TypeCheckPattern(
         Nonnull<ImplBinding*> impl_binding =
             arena_->New<ImplBinding>(binding.source_loc(), &binding, type);
         impl_binding->set_symbolic_identity(
-            arena_->New<SymbolicWitness>(CreateImplReference(impl_binding)));
+            CreateImplBindingWitness(impl_binding));
         binding.set_impl_binding(impl_binding);
         BringImplIntoScope(impl_binding, impl_scope);
       }
@@ -3783,11 +3796,7 @@ auto TypeChecker::CheckAndAddImplBindings(
                           impl_decl->deduced_parameters().end());
 
   // An expression that evaluates to this impl's witness.
-  // TODO: Store witnesses as `Witness*` rather than `Expression*` everywhere
-  // so we don't need to create this.
-  auto* impl_expr = arena_->New<ValueLiteral>(
-      impl_decl->source_loc(), arena_->New<ImplWitness>(impl_decl),
-      arena_->New<TypeType>(), ValueCategory::Let);
+  auto* witness = arena_->New<ImplWitness>(impl_decl);
 
   // Form the resolved constraint type by substituting `Self` for `.Self`.
   Nonnull<const Value*> self = *impl_decl->self()->constant_value();
@@ -3818,7 +3827,7 @@ auto TypeChecker::CheckAndAddImplBindings(
 
       scope_info.innermost_non_class_scope->Add(
           iface_type, deduced_bindings, impl_type, impl_decl->impl_bindings(),
-          impl_expr, *this);
+          witness, *this);
     } else {
       // TODO: Add support for implementing `adapter`s.
       return CompilationError(impl_decl->source_loc())
diff --git a/explorer/interpreter/type_checker.h b/explorer/interpreter/type_checker.h
index 0088819c9aa1..adfc43c428aa 100644
--- a/explorer/interpreter/type_checker.h
+++ b/explorer/interpreter/type_checker.h
@@ -62,13 +62,13 @@ class TypeChecker {
                                  Nonnull<const Value*>>& dict,
                   Nonnull<const Value*> type) const -> Nonnull<const Value*>;
 
-  // If `impl` can be an implementation of interface `iface` for the
-  // given `type`, then return an expression that will produce the witness
-  // for this `impl` (at runtime). Otherwise return std::nullopt.
+  // If `impl` can be an implementation of interface `iface` for the given
+  // `type`, then return the witness for this `impl`. Otherwise return
+  // std::nullopt.
   auto MatchImpl(const InterfaceType& iface, Nonnull<const Value*> type,
                  const ImplScope::Impl& impl, const ImplScope& impl_scope,
                  SourceLocation source_loc) const
-      -> std::optional<Nonnull<Expression*>>;
+      -> std::optional<Nonnull<const Witness*>>;
 
   /*
   ** Finds the direct or indirect member of a class or mixin by its name and
@@ -88,14 +88,14 @@ class TypeChecker {
   // the constraint.
   auto MakeConstraintWitness(
       const ConstraintType& constraint,
-      std::vector<Nonnull<Expression*>> impl_constraint_witnesses,
-      SourceLocation source_loc) const -> Nonnull<Expression*>;
+      std::vector<Nonnull<const Witness*>> impl_constraint_witnesses,
+      SourceLocation source_loc) const -> Nonnull<const Witness*>;
 
   // Given the witnesses for the components of a constraint, form a witness for
   // the constraint.
-  auto MakeConstraintWitnessAccess(Nonnull<Expression*> witness,
+  auto MakeConstraintWitnessAccess(Nonnull<const Witness*> witness,
                                    size_t impl_offset) const
-      -> Nonnull<Expression*>;
+      -> Nonnull<const Witness*>;
 
  private:
   struct SingleStepEqualityContext;
@@ -252,9 +252,9 @@ class TypeChecker {
   void BringPatternImplsIntoScope(Nonnull<const Pattern*> p,
                                   ImplScope& impl_scope);
 
-  // Create a reference to the given `impl` binding.
-  auto CreateImplReference(Nonnull<const ImplBinding*> impl_binding)
-      -> Nonnull<Expression*>;
+  // Create a witness for the given `impl` binding.
+  auto CreateImplBindingWitness(Nonnull<const ImplBinding*> impl_binding)
+      -> Nonnull<const Witness*>;
 
   // Add the given ImplBinding to the given `impl_scope`.
   void BringImplIntoScope(Nonnull<const ImplBinding*> impl_binding,
@@ -418,7 +418,7 @@ class TypeChecker {
   auto SatisfyImpls(llvm::ArrayRef<Nonnull<const ImplBinding*>> impl_bindings,
                     const ImplScope& impl_scope, SourceLocation source_loc,
                     const BindingMap& deduced_type_args,
-                    ImplExpMap& impls) const -> ErrorOr<Success>;
+                    ImplWitnessMap& impls) const -> ErrorOr<Success>;
 
   // Given an interface type, form a corresponding constraint type.
   auto MakeConstraintForInterface(SourceLocation source_loc,