diff --git a/explorer/interpreter/action.cpp b/explorer/interpreter/action.cpp
index 5ad6534b2da8..e2adbda74c8d 100644
--- a/explorer/interpreter/action.cpp
+++ b/explorer/interpreter/action.cpp
@@ -116,6 +116,9 @@ void Action::Print(llvm::raw_ostream& out) const {
       break;
     case Action::Kind::ScopeAction:
       break;
+    case Action::Kind::RecursiveAction:
+      out << "recursive";
+      break;
   }
   out << "." << pos_ << ".";
   if (!results_.empty()) {
diff --git a/explorer/interpreter/action.h b/explorer/interpreter/action.h
index 88e6bb81d249..46ce4115a529 100644
--- a/explorer/interpreter/action.h
+++ b/explorer/interpreter/action.h
@@ -85,6 +85,7 @@ class Action {
     StatementAction,
     DeclarationAction,
     ScopeAction,
+    RecursiveAction,
   };
 
   Action(const Value&) = delete;
@@ -250,6 +251,23 @@ class ScopeAction : public Action {
   }
 };
 
+// Action which contains another action and does nothing further once that
+// action completes. This action therefore acts as a marker on the action stack
+// that indicates that the interpreter should stop when the inner action has
+// finished, and holds the result of that inner action. This is useful to allow
+// a sequence of steps for an action to be run immediately rather than as part
+// of the normal step queue.
+//
+// Should be avoided where possible.
+class RecursiveAction : public Action {
+ public:
+  explicit RecursiveAction() : Action(Kind::RecursiveAction) {}
+
+  static auto classof(const Action* action) -> bool {
+    return action->kind() == Kind::RecursiveAction;
+  }
+};
+
 }  // namespace Carbon
 
 #endif  // CARBON_EXPLORER_INTERPRETER_ACTION_H_
diff --git a/explorer/interpreter/action_stack.cpp b/explorer/interpreter/action_stack.cpp
index 1535e5a3ac77..4a51dfeac902 100644
--- a/explorer/interpreter/action_stack.cpp
+++ b/explorer/interpreter/action_stack.cpp
@@ -124,6 +124,7 @@ auto ActionStack::FinishAction() -> ErrorOr<Success> {
       CARBON_FATAL() << "ScopeAction at top of stack";
     case Action::Kind::StatementAction:
     case Action::Kind::DeclarationAction:
+    case Action::Kind::RecursiveAction:
       PopScopes();
   }
   return Success();
@@ -135,6 +136,7 @@ auto ActionStack::FinishAction(Nonnull<const Value*> result)
   switch (act->kind()) {
     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";
diff --git a/explorer/interpreter/action_stack.h b/explorer/interpreter/action_stack.h
index 49e5711b67f2..877434cc8404 100644
--- a/explorer/interpreter/action_stack.h
+++ b/explorer/interpreter/action_stack.h
@@ -88,6 +88,11 @@ class ActionStack {
   auto Spawn(std::unique_ptr<Action> child, RuntimeScope scope)
       -> ErrorOr<Success>;
 
+  // Start a new recursive action.
+  auto BeginRecursiveAction() {
+    todo_.Push(std::make_unique<RecursiveAction>());
+  }
+
   // Advances the current action one step.
   auto RunAgain() -> ErrorOr<Success>;
 
diff --git a/explorer/interpreter/interpreter.cpp b/explorer/interpreter/interpreter.cpp
index 08fb63bc29fd..baa918991c36 100644
--- a/explorer/interpreter/interpreter.cpp
+++ b/explorer/interpreter/interpreter.cpp
@@ -91,17 +91,13 @@ class Interpreter {
   // Returns the result of converting `value` to type `destination_type`.
   auto Convert(Nonnull<const Value*> value,
                Nonnull<const Value*> destination_type,
-               SourceLocation source_loc) const
-      -> ErrorOr<Nonnull<const Value*>>;
+               SourceLocation source_loc) -> ErrorOr<Nonnull<const Value*>>;
 
-  // Evaluate an impl expression to produce a witness, or signal an
-  // error.
+  // Evaluate an expression immediately, recursively.
   //
-  // An impl expression is either
-  // 1) an IdentifierExpression whose value_node is an impl declaration, or
-  // 2) an InstantiateImpl expression.
-  auto EvalImplExp(Nonnull<const Expression*> exp) const
-      -> ErrorOr<Nonnull<const Witness*>>;
+  // TODO: Stop using this.
+  auto EvalExpRecursively(Nonnull<const Expression*> exp)
+      -> ErrorOr<Nonnull<const Value*>>;
 
   // Instantiate a type by replacing all type variables that occur inside the
   // type by the current values of those variables.
@@ -110,8 +106,7 @@ class Interpreter {
   //     __Fn (Point(T)) -> Point(U)
   // becomes
   //     __Fn (Point(i32)) -> Point(Bool)
-  auto InstantiateType(Nonnull<const Value*> type,
-                       SourceLocation source_loc) const
+  auto InstantiateType(Nonnull<const Value*> type, SourceLocation source_loc)
       -> ErrorOr<Nonnull<const Value*>>;
 
   // Call the function `fun` with the given `arg` and the `witnesses`
@@ -421,39 +416,34 @@ auto Interpreter::StepLvalue() -> ErrorOr<Success> {
   }
 }
 
-auto Interpreter::EvalImplExp(Nonnull<const Expression*> exp) const
-    -> ErrorOr<Nonnull<const Witness*>> {
-  switch (exp->kind()) {
-    case ExpressionKind::InstantiateImpl: {
-      const InstantiateImpl& inst_impl = cast<InstantiateImpl>(*exp);
-      CARBON_ASSIGN_OR_RETURN(Nonnull<const Witness*> gen_impl,
-                              EvalImplExp(inst_impl.generic_impl()));
-      ImplWitnessMap witnesses;
-      for (auto& [bind, impl_exp] : inst_impl.impls()) {
-        CARBON_ASSIGN_OR_RETURN(witnesses[bind], EvalImplExp(impl_exp));
-      }
-      return arena_->New<Witness>(&gen_impl->declaration(),
-                                  inst_impl.type_args(), witnesses);
-    }
-    case ExpressionKind::IdentifierExpression: {
-      const auto& ident = cast<IdentifierExpression>(*exp);
-      CARBON_ASSIGN_OR_RETURN(
-          Nonnull<const Value*> value,
-          todo_.ValueOfNode(ident.value_node(), ident.source_loc()));
-      if (const auto* lvalue = dyn_cast<LValue>(value)) {
-        CARBON_ASSIGN_OR_RETURN(
-            value, heap_.Read(lvalue->address(), exp->source_loc()));
-      }
-      return cast<Witness>(value);
-    }
-    default: {
-      CARBON_FATAL() << "EvalImplExp, unexpected expression: " << *exp;
+auto Interpreter::EvalExpRecursively(Nonnull<const Expression*> exp)
+    -> ErrorOr<Nonnull<const Value*>> {
+  if (trace_stream_) {
+    **trace_stream_ << "--- recursive eval of " << *exp << "\n";
+    PrintState(**trace_stream_);
+  }
+  todo_.BeginRecursiveAction();
+  CARBON_RETURN_IF_ERROR(todo_.Spawn(std::make_unique<ExpressionAction>(exp)));
+  // 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.
+  while (!isa<RecursiveAction>(todo_.CurrentAction())) {
+    CARBON_RETURN_IF_ERROR(Step());
+    if (trace_stream_) {
+      PrintState(**trace_stream_);
     }
   }
+  if (trace_stream_) {
+    **trace_stream_ << "--- recursive eval done\n";
+  }
+  Nonnull<const Value*> result =
+      cast<RecursiveAction>(todo_.CurrentAction()).results()[0];
+  CARBON_RETURN_IF_ERROR(todo_.FinishAction());
+  return result;
 }
 
 auto Interpreter::InstantiateType(Nonnull<const Value*> type,
-                                  SourceLocation source_loc) const
+                                  SourceLocation source_loc)
     -> ErrorOr<Nonnull<const Value*>> {
   switch (type->kind()) {
     case Value::Kind::VariableType: {
@@ -473,9 +463,12 @@ auto Interpreter::InstantiateType(Nonnull<const Value*> type,
         CARBON_ASSIGN_OR_RETURN(inst_type_args[ty_var],
                                 InstantiateType(ty_arg, source_loc));
       }
-      ImplWitnessMap witnesses;
-      for (const auto& [bind, impl_exp] : class_type.impls()) {
-        CARBON_ASSIGN_OR_RETURN(witnesses[bind], EvalImplExp(impl_exp));
+      ImplWitnessMap witnesses = class_type.witnesses();
+      for (auto& [bind, witness] : witnesses) {
+        if (auto* sym = dyn_cast<SymbolicWitness>(witness)) {
+          CARBON_ASSIGN_OR_RETURN(witness,
+                                  EvalExpRecursively(&sym->impl_expression()));
+        }
       }
       return arena_->New<NominalClassType>(&class_type.declaration(),
                                            inst_type_args, witnesses);
@@ -487,7 +480,7 @@ auto Interpreter::InstantiateType(Nonnull<const Value*> type,
 
 auto Interpreter::Convert(Nonnull<const Value*> value,
                           Nonnull<const Value*> destination_type,
-                          SourceLocation source_loc) const
+                          SourceLocation source_loc)
     -> ErrorOr<Nonnull<const Value*>> {
   switch (value->kind()) {
     case Value::Kind::IntValue:
@@ -507,7 +500,8 @@ auto Interpreter::Convert(Nonnull<const Value*> value,
     case Value::Kind::NominalClassType:
     case Value::Kind::InterfaceType:
     case Value::Kind::ConstraintType:
-    case Value::Kind::Witness:
+    case Value::Kind::ImplWitness:
+    case Value::Kind::SymbolicWitness:
     case Value::Kind::ParameterizedEntityName:
     case Value::Kind::ChoiceType:
     case Value::Kind::ContinuationType:
@@ -696,27 +690,12 @@ auto Interpreter::CallFunction(const CallExpression& call,
                                 &params_scope, generic_args, trace_stream_,
                                 this->arena_));
       switch (decl.kind()) {
-        case DeclarationKind::ClassDeclaration: {
-          switch (phase()) {
-            case Phase::RunTime:
-              return todo_.FinishAction(arena_->New<NominalClassType>(
-                  &cast<ClassDeclaration>(decl), generic_args, witnesses));
-            case Phase::CompileTime:
-              return todo_.FinishAction(arena_->New<NominalClassType>(
-                  &cast<ClassDeclaration>(decl), generic_args, call.impls()));
-          }
-        }
-        case DeclarationKind::InterfaceDeclaration: {
-          switch (phase()) {
-            case Phase::RunTime:
-              return todo_.FinishAction(arena_->New<InterfaceType>(
-                  &cast<InterfaceDeclaration>(decl), generic_args, witnesses));
-            case Phase::CompileTime:
-              return todo_.FinishAction(
-                  arena_->New<InterfaceType>(&cast<InterfaceDeclaration>(decl),
-                                             generic_args, call.impls()));
-          }
-        }
+        case DeclarationKind::ClassDeclaration:
+          return todo_.FinishAction(arena_->New<NominalClassType>(
+              &cast<ClassDeclaration>(decl), generic_args, witnesses));
+        case DeclarationKind::InterfaceDeclaration:
+          return todo_.FinishAction(arena_->New<InterfaceType>(
+              &cast<InterfaceDeclaration>(decl), generic_args, witnesses));
         default:
           CARBON_FATAL() << "unknown kind of ParameterizedEntityName " << decl;
       }
@@ -740,20 +719,24 @@ auto Interpreter::StepExp() -> ErrorOr<Success> {
       if (act.pos() == 0) {
         return todo_.Spawn(
             std::make_unique<ExpressionAction>(inst_impl.generic_impl()));
-      } else if (act.pos() - 1 < int(inst_impl.impls().size())) {
+      }
+      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<ExpressionAction>(iter->second));
       } else {
-        Nonnull<const Witness*> generic_witness =
-            cast<Witness>(act.results()[0]);
+        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<Witness>(
+        return todo_.FinishAction(arena_->New<ImplWitness>(
             &generic_witness->declaration(), inst_impl.type_args(), witnesses));
       }
     }
@@ -764,6 +747,9 @@ 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 {
@@ -924,9 +910,16 @@ auto Interpreter::StepExp() -> ErrorOr<Success> {
       CARBON_CHECK(act.pos() == 0);
       const auto& ident = cast<IdentifierExpression>(exp);
       // { {x :: C, E, F} :: S, H} -> { {H(E(x)) :: C, E, F} :: S, H}
-      CARBON_ASSIGN_OR_RETURN(
-          Nonnull<const Value*> value,
-          todo_.ValueOfNode(ident.value_node(), ident.source_loc()));
+      auto value_or_error =
+          todo_.ValueOfNode(ident.value_node(), ident.source_loc());
+      if (!value_or_error.ok() && phase() == Phase::CompileTime &&
+          isa<ImplBinding>(ident.value_node().base())) {
+        // The `ImplBinding` might not be in scope. If so, just remember the
+        // expression from which it was derived.
+        return todo_.FinishAction(arena_->New<SymbolicWitness>(&exp));
+      }
+      CARBON_ASSIGN_OR_RETURN(Nonnull<const Value*> value,
+                              std::move(value_or_error));
       if (const auto* lvalue = dyn_cast<LValue>(value)) {
         CARBON_ASSIGN_OR_RETURN(
             value, heap_.Read(lvalue->address(), exp.source_loc()));
@@ -965,9 +958,7 @@ auto Interpreter::StepExp() -> ErrorOr<Success> {
     }
     case ExpressionKind::CallExpression: {
       const CallExpression& call = cast<CallExpression>(exp);
-      // Don't evaluate the impls at compile time?
-      unsigned int num_impls =
-          phase() == Phase::CompileTime ? 0 : call.impls().size();
+      unsigned int num_impls = call.impls().size();
       if (act.pos() == 0) {
         //    { {e1(e2) :: C, E, F} :: S, H}
         // -> { {e1 :: [](e2) :: C, E, F} :: S, H}
@@ -1468,6 +1459,8 @@ auto Interpreter::Step() -> ErrorOr<Success> {
       break;
     case Action::Kind::ScopeAction:
       CARBON_FATAL() << "ScopeAction escaped ActionStack";
+    case Action::Kind::RecursiveAction:
+      CARBON_FATAL() << "Tried to step a RecursiveAction";
   }  // switch
   return Success();
 }
diff --git a/explorer/interpreter/type_checker.cpp b/explorer/interpreter/type_checker.cpp
index 7c3a586dd9fe..08cf46106c1d 100644
--- a/explorer/interpreter/type_checker.cpp
+++ b/explorer/interpreter/type_checker.cpp
@@ -82,7 +82,8 @@ static auto IsTypeOfType(Nonnull<const Value*> value) -> bool {
     case Value::Kind::AlternativeConstructorValue:
     case Value::Kind::ContinuationValue:
     case Value::Kind::StringValue:
-    case Value::Kind::Witness:
+    case Value::Kind::ImplWitness:
+    case Value::Kind::SymbolicWitness:
     case Value::Kind::ParameterizedEntityName:
     case Value::Kind::MemberName:
     case Value::Kind::TypeOfParameterizedEntityName:
@@ -137,7 +138,8 @@ static auto IsType(Nonnull<const Value*> value, bool concrete = false) -> bool {
     case Value::Kind::AlternativeConstructorValue:
     case Value::Kind::ContinuationValue:
     case Value::Kind::StringValue:
-    case Value::Kind::Witness:
+    case Value::Kind::ImplWitness:
+    case Value::Kind::SymbolicWitness:
     case Value::Kind::ParameterizedEntityName:
     case Value::Kind::MemberName:
       return false;
@@ -704,7 +706,8 @@ auto TypeChecker::ArgumentDeduction(
     case Value::Kind::TypeOfParameterizedEntityName:
     case Value::Kind::TypeOfMemberName:
       return handle_non_deduced_type();
-    case Value::Kind::Witness:
+    case Value::Kind::ImplWitness:
+    case Value::Kind::SymbolicWitness:
     case Value::Kind::ParameterizedEntityName:
     case Value::Kind::MemberName:
     case Value::Kind::IntValue:
@@ -993,7 +996,8 @@ auto TypeChecker::Substitute(
       // TODO: We should substitute into the value and produce a new type of
       // type for it.
       return type;
-    case Value::Kind::Witness:
+    case Value::Kind::ImplWitness:
+    case Value::Kind::SymbolicWitness:
     case Value::Kind::ParameterizedEntityName:
     case Value::Kind::MemberName:
     case Value::Kind::IntValue:
@@ -1904,8 +1908,7 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
             case DeclarationKind::ClassDeclaration: {
               Nonnull<NominalClassType*> inst_class_type =
                   arena_->New<NominalClassType>(&cast<ClassDeclaration>(decl),
-                                                call.deduced_args(),
-                                                call.impls());
+                                                call.deduced_args());
               call.set_static_type(
                   arena_->New<TypeOfClassType>(inst_class_type));
               call.set_value_category(ValueCategory::Let);
@@ -1914,7 +1917,7 @@ auto TypeChecker::TypeCheckExp(Nonnull<Expression*> e,
             case DeclarationKind::InterfaceDeclaration: {
               Nonnull<InterfaceType*> inst_iface_type =
                   arena_->New<InterfaceType>(&cast<InterfaceDeclaration>(decl),
-                                             call.deduced_args(), call.impls());
+                                             call.deduced_args());
               call.set_static_type(
                   arena_->New<TypeOfInterfaceType>(inst_iface_type));
               call.set_value_category(ValueCategory::Let);
@@ -2991,7 +2994,7 @@ auto TypeChecker::DeclareImplDeclaration(Nonnull<ImplDeclaration*> impl_decl,
       }
     }
   }
-  impl_decl->set_constant_value(arena_->New<Witness>(impl_decl));
+  impl_decl->set_constant_value(arena_->New<ImplWitness>(impl_decl));
   if (trace_stream_) {
     **trace_stream_ << "** finished declaring impl " << *impl_decl->impl_type()
                     << " as " << impl_decl->interface() << "\n";
@@ -3053,7 +3056,8 @@ static bool IsValidTypeForAliasTarget(Nonnull<const Value*> type) {
     case Value::Kind::NominalClassValue:
     case Value::Kind::AlternativeValue:
     case Value::Kind::TupleValue:
-    case Value::Kind::Witness:
+    case Value::Kind::ImplWitness:
+    case Value::Kind::SymbolicWitness:
     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 bed3fe84d2e1..fd3c8b485479 100644
--- a/explorer/interpreter/value.cpp
+++ b/explorer/interpreter/value.cpp
@@ -36,28 +36,35 @@ static auto GetMember(Nonnull<Arena*> arena, Nonnull<const Value*> v,
   const std::string& f = field.name();
 
   if (field.witness().has_value()) {
-    Nonnull<const Witness*> witness = *field.witness();
+    Nonnull<const Witness*> witness = cast<Witness>(*field.witness());
     switch (witness->kind()) {
-      case Value::Kind::Witness: {
+      case Value::Kind::ImplWitness: {
+        auto* impl_witness = cast<ImplWitness>(witness);
         if (std::optional<Nonnull<const Declaration*>> mem_decl =
-                FindMember(f, witness->declaration().members());
+                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, witness->type_args(), witness->witnesses());
+            return arena->New<BoundMethodValue>(&fun_decl, v,
+                                                impl_witness->type_args(),
+                                                impl_witness->witnesses());
           } else {
             // Class function.
-            auto fun = cast<FunctionValue>(*fun_decl.constant_value());
+            auto* fun = cast<FunctionValue>(*fun_decl.constant_value());
             return arena->New<FunctionValue>(&fun->declaration(),
-                                             witness->type_args(),
-                                             witness->witnesses());
+                                             impl_witness->type_args(),
+                                             impl_witness->witnesses());
           }
         } 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;
     }
@@ -337,13 +344,6 @@ void Value::Print(llvm::raw_ostream& out) const {
       out << "class ";
       PrintNameWithBindings(out, &class_type.declaration(),
                             class_type.type_args());
-      if (!class_type.impls().empty()) {
-        out << " impls ";
-        llvm::ListSeparator sep;
-        for (const auto& [impl_bind, impl] : class_type.impls()) {
-          out << sep << *impl;
-        }
-      }
       if (!class_type.witnesses().empty()) {
         out << " witnesses ";
         llvm::ListSeparator sep;
@@ -385,12 +385,17 @@ void Value::Print(llvm::raw_ostream& out) const {
       }
       break;
     }
-    case Value::Kind::Witness: {
-      const auto& witness = cast<Witness>(*this);
+    case Value::Kind::ImplWitness: {
+      const auto& witness = cast<ImplWitness>(*this);
       out << "witness " << *witness.declaration().impl_type() << " as "
           << witness.declaration().interface();
       break;
     }
+    case Value::Kind::SymbolicWitness: {
+      const auto& witness = cast<SymbolicWitness>(*this);
+      out << "witness " << witness.impl_expression();
+      break;
+    }
     case Value::Kind::ParameterizedEntityName:
       out << *GetName(cast<ParameterizedEntityName>(*this).declaration());
       break;
@@ -660,7 +665,8 @@ auto TypeEqual(Nonnull<const Value*> t1, Nonnull<const Value*> t2) -> bool {
       CARBON_FATAL() << "TypeEqual used to compare non-type values\n"
                      << *t1 << "\n"
                      << *t2;
-    case Value::Kind::Witness:
+    case Value::Kind::ImplWitness:
+    case Value::Kind::SymbolicWitness:
       CARBON_FATAL() << "TypeEqual: unexpected Witness";
       break;
     case Value::Kind::AutoType:
@@ -748,7 +754,8 @@ auto ValueEqual(Nonnull<const Value*> v1, Nonnull<const Value*> v2) -> bool {
     case Value::Kind::NominalClassType:
     case Value::Kind::InterfaceType:
     case Value::Kind::ConstraintType:
-    case Value::Kind::Witness:
+    case Value::Kind::ImplWitness:
+    case Value::Kind::SymbolicWitness:
     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 05a07d78dda3..6cad900e1109 100644
--- a/explorer/interpreter/value.h
+++ b/explorer/interpreter/value.h
@@ -45,7 +45,8 @@ class Value {
     NominalClassValue,
     AlternativeValue,
     TupleValue,
-    Witness,
+    ImplWitness,
+    SymbolicWitness,
     IntType,
     BoolType,
     TypeType,
@@ -564,17 +565,6 @@ class NominalClassType : public Value {
         declaration_(declaration),
         type_args_(type_args) {}
 
-  // Construct a class type that represents the result of applying the
-  // given generic class to the `type_args` and that records the result of the
-  // compile-time search for any required impls.
-  explicit NominalClassType(Nonnull<const ClassDeclaration*> declaration,
-                            const BindingMap& type_args,
-                            const ImplExpMap& impls)
-      : Value(Kind::NominalClassType),
-        declaration_(declaration),
-        type_args_(type_args),
-        impls_(impls) {}
-
   // Construct a fully instantiated generic class type to represent the
   // run-time type of an object.
   explicit NominalClassType(Nonnull<const ClassDeclaration*> declaration,
@@ -592,13 +582,6 @@ class NominalClassType : public Value {
   auto declaration() const -> const ClassDeclaration& { return *declaration_; }
   auto type_args() const -> const BindingMap& { return type_args_; }
 
-  // Maps each of an instantiated generic class's impl bindings to an
-  // expression that constructs the witness table for the corresponding
-  // argument. Should not be called on 1) a non-generic class, 2) a
-  // generic-class that is not instantiated, or 3) a fully
-  // instantiated runtime type of a generic class.
-  auto impls() const -> const ImplExpMap& { return impls_; }
-
   // Maps each of the class's impl bindings to the witness table
   // for the corresponding argument. Should only be called on a fully
   // instantiated runtime type of a generic class.
@@ -618,7 +601,6 @@ class NominalClassType : public Value {
  private:
   Nonnull<const ClassDeclaration*> declaration_;
   BindingMap type_args_;
-  ImplExpMap impls_;
   ImplWitnessMap witnesses_;
 };
 
@@ -639,12 +621,6 @@ class InterfaceType : public Value {
   explicit InterfaceType(Nonnull<const InterfaceDeclaration*> declaration,
                          const BindingMap& args)
       : Value(Kind::InterfaceType), declaration_(declaration), args_(args) {}
-  explicit InterfaceType(Nonnull<const InterfaceDeclaration*> declaration,
-                         const BindingMap& args, const ImplExpMap& impls)
-      : Value(Kind::InterfaceType),
-        declaration_(declaration),
-        args_(args),
-        impls_(impls) {}
   explicit InterfaceType(Nonnull<const InterfaceDeclaration*> declaration,
                          const BindingMap& args, const ImplWitnessMap& wits)
       : Value(Kind::InterfaceType),
@@ -662,13 +638,11 @@ class InterfaceType : public Value {
   auto args() const -> const BindingMap& { return args_; }
 
   // TODO: These aren't used for anything yet.
-  auto impls() const -> const ImplExpMap& { return impls_; }
   auto witnesses() const -> const ImplWitnessMap& { return witnesses_; }
 
  private:
   Nonnull<const InterfaceDeclaration*> declaration_;
   BindingMap args_;
-  ImplExpMap impls_;
   ImplWitnessMap witnesses_;
 };
 
@@ -744,25 +718,37 @@ class ConstraintType : public Value {
   std::vector<LookupContext> lookup_contexts_;
 };
 
-// The witness table for an impl.
+// A witness table.
 class Witness : public Value {
+ protected:
+  explicit Witness(Value::Kind kind) : Value(kind) {}
+
+ public:
+  static auto classof(const Value* value) -> bool {
+    return value->kind() == Kind::ImplWitness ||
+           value->kind() == Kind::SymbolicWitness;
+  }
+};
+
+// The witness table for an impl.
+class ImplWitness : public Witness {
  public:
   // Construct a witness for
   // 1) a non-generic impl, or
   // 2) a generic impl that has not yet been applied to type arguments.
-  explicit Witness(Nonnull<const ImplDeclaration*> declaration)
-      : Value(Kind::Witness), declaration_(declaration) {}
+  explicit ImplWitness(Nonnull<const ImplDeclaration*> declaration)
+      : Witness(Kind::ImplWitness), declaration_(declaration) {}
 
   // Construct an instantiated generic impl.
-  explicit Witness(Nonnull<const ImplDeclaration*> declaration,
-                   const BindingMap& type_args, const ImplWitnessMap& wits)
-      : Value(Kind::Witness),
+  explicit ImplWitness(Nonnull<const ImplDeclaration*> declaration,
+                       const BindingMap& type_args, const ImplWitnessMap& wits)
+      : Witness(Kind::ImplWitness),
         declaration_(declaration),
         type_args_(type_args),
         witnesses_(wits) {}
 
   static auto classof(const Value* value) -> bool {
-    return value->kind() == Kind::Witness;
+    return value->kind() == Kind::ImplWitness;
   }
   auto declaration() const -> const ImplDeclaration& { return *declaration_; }
   auto type_args() const -> const BindingMap& { return type_args_; }
@@ -777,6 +763,25 @@ class Witness : public Value {
   ImplWitnessMap witnesses_;
 };
 
+// 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 {
+ public:
+  explicit SymbolicWitness(Nonnull<const Expression*> impl_expr)
+      : Witness(Kind::SymbolicWitness), impl_expr_(impl_expr) {}
+
+  static auto classof(const Value* value) -> bool {
+    return value->kind() == Kind::SymbolicWitness;
+  }
+
+  auto impl_expression() const -> const Expression& { return *impl_expr_; }
+
+ private:
+  Nonnull<const Expression*> impl_expr_;
+};
+
 // A choice type.
 class ChoiceType : public Value {
  public:
diff --git a/explorer/testdata/generic_class/use_at_compile_time.carbon b/explorer/testdata/generic_class/use_at_compile_time.carbon
new file mode 100644
index 000000000000..6c268dc50daa
--- /dev/null
+++ b/explorer/testdata/generic_class/use_at_compile_time.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 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK: result: 0
+
+package ExplorerTest api;
+
+interface Has(T:! Type) {
+  fn Get() -> T;
+}
+impl i32 as Has(Type) {
+  fn Get() -> Type { return Self; }
+}
+
+class WithType(T:! Has(Type)) {
+  fn Get() -> Type { return T.Get(); }
+}
+
+fn Main() -> i32 {
+  var v: WithType(i32).Get() = 0;
+  return v;
+}
diff --git a/explorer/testdata/generic_function/call_at_compile_time.carbon b/explorer/testdata/generic_function/call_at_compile_time.carbon
new file mode 100644
index 000000000000..0ace774c63a9
--- /dev/null
+++ b/explorer/testdata/generic_function/call_at_compile_time.carbon
@@ -0,0 +1,25 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK: result: 0
+
+package ExplorerTest api;
+
+interface X { fn F(); }
+impl i32 as X { fn F() {} }
+
+fn G[T:! X](v: T) -> Type {
+  v.F();
+  return i32;
+}
+
+fn Main() -> i32 {
+  var v: G(0) = 0;
+  return v;
+}