Support specialization in impl lookup with a symbolic query/impl. (#5169)

Add a new instruction called ImplSymbolicWitness which represents a
search for an impl declaration given a self type and an interface to
find implemented for the self type. The self type is stored as a
constant instruction id, rather than as a ConstantId, as instructions
don't currently support holding ConstantId. The interface is stored as a
SpecificInterface but we can't fit all of it directly into the
instruction. So we add a new id to refer to the SpecificInterface as
follows.

Add a new SpecificInterfaceId which indexes into a canonical value store
on SemIR::File. This tracks all `SpecificInterface`s stored in an
instruction - specifically the ImplSymbolicWitness instruction.

The SpecificInterface on Impl is still stored there as a value, not as
an id, and no id is eagerly constructed for it. We wait until an id is
needed to make one. Since they are canonical, a new id is only create
when a new SpecificInterface value is seen.

When doing impl lookup, and the query is not concrete, and the impl is
not effectively final, the query needs to consider future impls that may
specialize either the self type or the constaint to make a more precise
match and replace the found impl declaration. Instead of returning the
ImplWitness instruction from the found impl, we generate a
ImplSymbolicWitness instruction, storing the query so that it can be
replayed later. This instruction is added to the generic eval block and
thus will be re-evaluated later with a SpecificId that may make the
query more concrete. When evaluating the instruction and replaying the
query, the lookup has the same conditions and if it does not decide to
use the found impl concretely, then the same instruction is returned
from eval, leaving it as symbolic.

--- Impl lookup changes ---

Impl lookup gets a little more interesting now. It continues to look in
the facet value for a witness if the self type is a facet value. Then
falls back to looking for an impl declaration. This step is no longer
done directly. Instead, we construct a ImplSymbolicWitness instruction
and evaluate it immediately for each interface that are in the query
facet type.

The ImplSymbolicWitness instruction, when evaluated, calls back to the
impl lookup code, with a query specific interface. There we resume back
into the same code path as from before, finding a witness in an impl
declaration. But we may return "found a non-final impl" instead of a
concrete witness. If eval receives this back, it evaluates to the
current ImplSymbolicWitness instruction as the resulting constant value.

To pass lookup failures back through eval, a result of InstId::None from
the second step of impl lookup will result in a non-constant value,
which is used as a signal back up the stack to the original impl lookup
function that the lookup failed. Using a non-constant value here would
break evaluation of the generic eval block if impl lookup could fail
there, however we know it will not since we only leave behind an
ImplSymbolicWitness instruction in the eval block if we found at least
one matching impl already, and we just want to look for a better match
with a more specific query.

We must take care to not store a reference into any value store across
computation in impl lookup, since impl lookup can recurse into itself
invalidate those stores. That includes the SpecificInterface obtained
from a SpecificInterfaceId, which impl lookup also inserts into the
store.

--- The long tail ---

Adding a new instruction and a new id type requires a myriad of changes
to support them:

We add Dump() support for SpecificInterfaceId. And fix a crash in Dump
for SpecificId::None. We also add MakeSpecificInterfaceId() for dumping
arbitrary ids.

The type of ImplSymbolicWitness is a new singleton builtin type
instruction called WitnessSymbolicType (like WitnessType is the type for
an ImplWitness).

Both ImplSymbolicWitness and WitnessSymbolicType are given `Value` as
their expression category as they are builtin constant values. And
BuildInfo() in TypeCompleter is taught about them both, returning a
`ValueRepr::Copy`.

WitnessSymbolicType is added to the set of SingletonInstKinds, so that
it can have a singleton instrution id as a static member.

Lower's BuildTypeForInst() is taught to make an empty struct for
WitnessSymbolicType, similar to WitnessType.

Instruction formatter (FormatterImpl) grows support for printing a
SpecificInterfaceId so that it can print both arguments of
ImplSymbolicWitness on the RHS when printing the SemIR instruction. To
print a SpecificInterfaceId, it prints both the interface id and the
specific id (if there is one). For example, for a query on a generic
interface `Z` with one parameter, the RHS includes the query, interface,
and specific:
```
%Z.impl_symbolic_witness: <symbolic witness> = impl_symbolic_witness %U, @Z, @Z(%U.as_type) [symbolic]
```

IdKind is extended to include SpecificInterfaceId.

InstFingerprinter is taught to look through SpecificInterfaceId and use
the interface and specific ids in the fingerprint.

InstNamer is taught about SpecificInterfaceId, counting the interfaces
when building an index. It is also tought about ImplSymbolicWitness,
using the name of the interface within and the `.impl_symbolic_witness`
suffix. For example, here the LHS is named after the interface in the
query:
```
%Z.impl_symbolic_witness: <symbolic witness> = impl_symbolic_witness %U, @Z, @Z(%U.as_type) [symbolic]
```

StringifyTypeExpr is taught about WitnessSymbolicType, which uses its IR
name since it's a singleton. And about ImplSymbolicWitness which uses
its constant value. The handling of ImplWitnessAccess also needed to be
adjusted, since it assumed that ImplWitnessAccess::witness_id would
always be a FacetAccessWitness, but it can now also be an
ImplSymbolicWitness. (It seems that the witness_id is also assigned
ImplWitness instructions, but those ImplWitnessAccess instructions don't
ever seem to get stringified in a diagnostic at this time.) At the
moment the ImplWitnessAccess with a symbolic witness is just stringified
as "<symbolic>", such as in:
```
x.carbon:1:2: error: cannot implicitly convert value of type `()` to `<symbolic>` [ConversionFailure]
  let a: C(D).(Z.X) = ();
                      ^~
```

There is a TODO left behind to include more information there.

The TypeStructure builder is made to handle WitnessSymbolicType and
WitnessType. These come up now in deduce where a generic impl will have
a ImplSymbolicWitness in a FacetValue for a generic self type. The query
may have a concrete ImplWitness in the same position. Since deduce tries
to deduce through the FacetValue, it tries to convert ImplWitness to
ImplSymbolicWitness, tries to do an impl lookup for `impl ImplWitness as
ImplicitAs(ImplSymbolicWitness)` and causes us to build type structures
with each of these.

Subst is updated to handle pushing and popping SpecificInterfaceId.
Without this, when finishing a generic's eval block, we would walk into
the ImplSymbolicWitness instruction, and its arguments, and fail to
recurse down into the SpecificInterfaceId. Then any specifics inside
would be left as "orphaned" without any generic id attached to them, and
we would never update the instructions in the SpecificInterface's
instructions (inside its own SpecificId) with new constant values when
evaluating the generic eval block against a specific. To do this we push
the specific_id inside the SpecificInterface, and when popping we pop
the specific_id then construct a new canonical SpecificInterface with it
and return that id.

We add support for importing ImplSymbolicWitness by importing its self
constant instruction and specific interface id. However we also had to
add import support for SpecificImplFunction, which can now appear in the
generic eval block for a generic impl declaration, and thus must be
imported with the declaration. This is done very similarly to
SpecificFunction, except the `type_id` is a singleton value.

---------

Co-authored-by: Jon Ross-Perkins <jperkins@google.com>

toolchain/check/BUILD

@@ -103,6 +103,7 @@ cc_library(
         "//common:vlog",
         "//toolchain/base:index_base",
         "//toolchain/base:kind_switch",
+        "//toolchain/base:value_store",
         "//toolchain/check:generic_region_stack",
         "//toolchain/check:scope_stack",
         "//toolchain/diagnostics:diagnostic_emitter",

toolchain/check/context.h

@@ -10,6 +10,7 @@
 #include "common/map.h"
 #include "common/ostream.h"
 #include "llvm/ADT/SmallVector.h"
+#include "toolchain/base/value_store.h"
 #include "toolchain/check/decl_introducer_state.h"
 #include "toolchain/check/decl_name_stack.h"
 #include "toolchain/check/full_pattern_stack.h"
@@ -232,6 +233,10 @@ class Context {
     return sem_ir().complete_facet_types();
   }
   auto impls() -> SemIR::ImplStore& { return sem_ir().impls(); }
+  auto specific_interfaces()
+      -> CanonicalValueStore<SemIR::SpecificInterfaceId>& {
+    return sem_ir().specific_interfaces();
+  }
   auto generics() -> SemIR::GenericStore& { return sem_ir().generics(); }
   auto specifics() -> SemIR::SpecificStore& { return sem_ir().specifics(); }
   auto import_irs() -> ValueStore<SemIR::ImportIRId>& {

toolchain/check/diagnostic_helpers.h

@@ -34,6 +34,8 @@ class SemIRLoc {
  private:
   // Only allow member access for diagnostics.
   friend class SemIRLocDiagnosticEmitter;
+  // And also for eval to unwrap a LocId for calling into the rest of Check.
+  friend class UnwrapSemIRLoc;
 
   union {
     SemIR::InstId inst_id_;

toolchain/check/dump.cpp

@@ -147,6 +147,12 @@ LLVM_DUMP_METHOD static auto Dump(const Context& context,
   SemIR::Dump(context.sem_ir(), specific_id);
 }
 
+LLVM_DUMP_METHOD static auto Dump(
+    const Context& context, SemIR::SpecificInterfaceId specific_interface_id)
+    -> void {
+  SemIR::Dump(context.sem_ir(), specific_interface_id);
+}
+
 LLVM_DUMP_METHOD static auto Dump(
     const Context& context, SemIR::StructTypeFieldsId struct_type_fields_id)
     -> void {

toolchain/check/eval.cpp

@@ -153,6 +153,10 @@ class EvalContext {
   auto interfaces() -> const ValueStore<SemIR::InterfaceId>& {
     return sem_ir().interfaces();
   }
+  auto specific_interfaces()
+      -> CanonicalValueStore<SemIR::SpecificInterfaceId>& {
+    return sem_ir().specific_interfaces();
+  }
   auto facet_types() -> CanonicalValueStore<SemIR::FacetTypeId>& {
     return sem_ir().facet_types();
   }
@@ -553,6 +557,20 @@ static auto GetConstantValue(EvalContext& eval_context,
                       specific.generic_id, args_id);
 }
 
+static auto GetConstantValue(EvalContext& eval_context,
+                             SemIR::SpecificInterfaceId specific_interface_id,
+                             Phase* phase) -> SemIR::SpecificInterfaceId {
+  const auto& interface =
+      eval_context.specific_interfaces().Get(specific_interface_id);
+  if (!interface.specific_id.has_value()) {
+    return specific_interface_id;
+  }
+  return eval_context.specific_interfaces().Add(
+      {.interface_id = interface.interface_id,
+       .specific_id =
+           GetConstantValue(eval_context, interface.specific_id, phase)});
+}
+
 // Like `GetConstantValue` but does a `FacetTypeId` -> `FacetTypeInfo`
 // conversion. Does not perform canonicalization.
 static auto GetConstantFacetTypeInfo(EvalContext& eval_context,
@@ -1841,6 +1859,12 @@ static auto TryEvalInstInContext(EvalContext& eval_context,
                                                               inst_id, inst);
 }
 
+auto TryEvalInst(Context& context, SemIR::LocId loc_id, SemIR::InstId inst_id,
+                 SemIR::Inst inst) -> SemIR::ConstantId {
+  EvalContext eval_context(context, loc_id);
+  return TryEvalInstInContext(eval_context, inst_id, inst);
+}
+
 auto TryEvalInst(Context& context, SemIR::InstId inst_id, SemIR::Inst inst)
     -> SemIR::ConstantId {
   EvalContext eval_context(context, inst_id);

toolchain/check/eval.h

@@ -16,6 +16,10 @@ namespace Carbon::Check {
 // `SemIR::ConstantId::NotConstant`.
 auto TryEvalInst(Context& context, SemIR::InstId inst_id, SemIR::Inst inst)
     -> SemIR::ConstantId;
+// Like the above but specific a LocId instead of deriving it from the
+// `inst_id`. This is most useful when passing `None` as the `inst_id`.
+auto TryEvalInst(Context& context, SemIR::LocId loc_id, SemIR::InstId inst_id,
+                 SemIR::Inst inst) -> SemIR::ConstantId;
 
 // Evaluates the eval block for a region of a specific. Produces a block
 // containing the evaluated constant values of the instructions in the eval

toolchain/check/eval_inst.cpp

@@ -4,16 +4,41 @@
 
 #include "toolchain/check/eval_inst.h"
 
+#include <variant>
+
 #include "toolchain/check/action.h"
 #include "toolchain/check/facet_type.h"
 #include "toolchain/check/generic.h"
+#include "toolchain/check/impl_lookup.h"
 #include "toolchain/check/import_ref.h"
 #include "toolchain/check/type.h"
 #include "toolchain/check/type_completion.h"
+#include "toolchain/sem_ir/ids.h"
 #include "toolchain/sem_ir/typed_insts.h"
 
 namespace Carbon::Check {
 
+// When calling from eval to various Check functions, we need the actual LocId.
+// This allows us to unwrap the SemIRLoc to do so.
+//
+// TODO: Decide whether to refactor calls everywhere to accept `SemIRLoc`, or
+// fold `SemIRLoc` into `LocId`. Either way, we would like eval to call other
+// code without unwrapping `SemIRLoc`.
+class UnwrapSemIRLoc {
+ public:
+  auto operator()(Context& context, SemIRLoc loc) -> SemIR::LocId {
+    if (loc.is_inst_id_) {
+      if (loc.inst_id_.has_value()) {
+        return context.insts().GetLocId(loc.inst_id_);
+      } else {
+        return SemIR::LocId::None;
+      }
+    } else {
+      return loc.loc_id_;
+    }
+  }
+};
+
 // Performs an access into an aggregate, retrieving the specified element.
 static auto PerformAggregateAccess(Context& context, SemIR::Inst inst)
     -> ConstantEvalResult {
@@ -197,6 +222,24 @@ auto EvalConstantInst(Context& /*context*/, SemIRLoc /*loc*/,
       .type_id = inst.type_id, .elements_id = SemIR::InstBlockId::Empty});
 }
 
+auto EvalConstantInst(Context& context, SemIRLoc loc,
+                      SemIR::ImplSymbolicWitness inst) -> ConstantEvalResult {
+  auto result = EvalLookupSingleImplWitness(
+      context, UnwrapSemIRLoc()(context, loc), inst);
+  if (!result.has_value()) {
+    // We use NotConstant to communicate back to impl lookup that the lookup
+    // failed. This can not happen for a deferred symbolic lookup in a generic
+    // eval block, since we only add the deferred lookup instruction (being
+    // evaluated here) to the SemIR if the lookup succeeds.
+    return ConstantEvalResult::NotConstant;
+  }
+  if (!result.has_concrete_value()) {
+    return ConstantEvalResult::NewSamePhase(inst);
+  }
+  return ConstantEvalResult::Existing(
+      context.constant_values().Get(result.concrete_witness()));
+}
+
 auto EvalConstantInst(Context& context, SemIRLoc loc,
                       SemIR::ImplWitnessAccess inst) -> ConstantEvalResult {
   // This is PerformAggregateAccess followed by GetConstantInSpecific.

toolchain/check/impl_lookup.cpp

@@ -5,16 +5,19 @@
 #include "toolchain/check/impl_lookup.h"
 
 #include <algorithm>
+#include <variant>
 
 #include "toolchain/base/kind_switch.h"
 #include "toolchain/check/deduce.h"
 #include "toolchain/check/diagnostic_helpers.h"
+#include "toolchain/check/eval.h"
 #include "toolchain/check/generic.h"
 #include "toolchain/check/import_ref.h"
 #include "toolchain/check/inst.h"
 #include "toolchain/check/type.h"
 #include "toolchain/check/type_completion.h"
 #include "toolchain/check/type_structure.h"
+#include "toolchain/sem_ir/facet_type_info.h"
 #include "toolchain/sem_ir/ids.h"
 #include "toolchain/sem_ir/impl.h"
 #include "toolchain/sem_ir/inst.h"
@@ -44,8 +47,10 @@ static auto FindAssociatedImportIRs(Context& context,
 
   llvm::SmallVector<SemIR::InstId> worklist;
   worklist.push_back(context.constant_values().GetInstId(query_self_const_id));
-  worklist.push_back(
-      context.constant_values().GetInstId(query_facet_type_const_id));
+  if (query_facet_type_const_id.has_value()) {
+    worklist.push_back(
+        context.constant_values().GetInstId(query_facet_type_const_id));
+  }
 
   // Push the contents of an instruction block onto our worklist.
   auto push_block = [&](SemIR::InstBlockId block_id) {
@@ -183,9 +188,10 @@ static auto GetInterfacesFromConstantId(
 }
 
 static auto GetWitnessIdForImpl(Context& context, SemIR::LocId loc_id,
+                                bool query_is_concrete,
                                 SemIR::ConstantId query_self_const_id,
                                 const SemIR::SpecificInterface& interface,
-                                SemIR::ImplId impl_id) -> SemIR::InstId {
+                                SemIR::ImplId impl_id) -> EvalImplLookupResult {
   // The impl may have generic arguments, in which case we need to deduce them
   // to find what they are given the specific type and interface query. We use
   // that specific to map values in the impl to the deduced values.
@@ -202,7 +208,7 @@ static auto GetWitnessIdForImpl(Context& context, SemIR::LocId loc_id,
                                .specific_id = impl.interface.specific_id},
                               query_self_const_id, interface.specific_id);
       if (!specific_id.has_value()) {
-        return SemIR::InstId::None;
+        return EvalImplLookupResult::MakeNone();
       }
     }
   }
@@ -224,7 +230,7 @@ static auto GetWitnessIdForImpl(Context& context, SemIR::LocId loc_id,
         context.constant_values().Get(access->facet_value_inst_id);
   }
   if (query_self_const_id != deduced_self_const_id) {
-    return SemIR::InstId::None;
+    return EvalImplLookupResult::MakeNone();
   }
 
   // The impl's constraint is a facet type which it is implementing for the self
@@ -235,7 +241,7 @@ static auto GetWitnessIdForImpl(Context& context, SemIR::LocId loc_id,
       context.constant_values().GetInstId(SemIR::GetConstantValueInSpecific(
           context.sem_ir(), specific_id, impl.constraint_id));
   if (deduced_constraint_id == SemIR::ErrorInst::SingletonInstId) {
-    return SemIR::InstId::None;
+    return EvalImplLookupResult::MakeNone();
   }
 
   auto deduced_constraint_facet_type_id =
@@ -249,7 +255,7 @@ static auto GetWitnessIdForImpl(Context& context, SemIR::LocId loc_id,
 
   if (deduced_constraint_facet_type_info.other_requirements) {
     // TODO: Remove this when other requirements goes away.
-    return SemIR::InstId::None;
+    return EvalImplLookupResult::MakeNone();
   }
 
   // The specifics in the queried interface must match the deduced specifics in
@@ -258,7 +264,7 @@ static auto GetWitnessIdForImpl(Context& context, SemIR::LocId loc_id,
       deduced_constraint_facet_type_info.impls_constraints[0].specific_id;
   auto query_interface_specific_id = interface.specific_id;
   if (impl_interface_specific_id != query_interface_specific_id) {
-    return SemIR::InstId::None;
+    return EvalImplLookupResult::MakeNone();
   }
 
   LoadImportRef(context, impl.witness_id);
@@ -267,8 +273,18 @@ static auto GetWitnessIdForImpl(Context& context, SemIR::LocId loc_id,
     // witness.
     ResolveSpecificDefinition(context, loc_id, specific_id);
   }
-  return context.constant_values().GetInstId(SemIR::GetConstantValueInSpecific(
-      context.sem_ir(), specific_id, impl.witness_id));
+
+  bool impl_is_effectively_final =
+      // TODO: impl.is_final ||
+      (context.constant_values().Get(impl.self_id).is_concrete() &&
+       context.constant_values().Get(impl.constraint_id).is_concrete());
+  if (query_is_concrete || impl_is_effectively_final) {
+    return EvalImplLookupResult::MakeFinal(
+        context.constant_values().GetInstId(SemIR::GetConstantValueInSpecific(
+            context.sem_ir(), specific_id, impl.witness_id)));
+  } else {
+    return EvalImplLookupResult::MakeNonFinal();
+  }
 }
 
 // In the case where `facet_const_id` is a facet, see if its facet type requires
@@ -291,104 +307,46 @@ static auto FindWitnessInFacet(
     for (auto [index, interface] :
          llvm::enumerate(facet_type_info.impls_constraints)) {
       if (interface == specific_interface) {
-        return GetOrAddInst(
-            context, loc_id,
-            SemIR::FacetAccessWitness{
-                .type_id = GetSingletonType(
-                    context, SemIR::WitnessType::SingletonInstId),
-                .facet_value_inst_id = facet_inst_id,
-                .index = SemIR::ElementIndex(index)});
+        auto witness_id =
+            GetOrAddInst(context, loc_id,
+                         SemIR::FacetAccessWitness{
+                             .type_id = GetSingletonType(
+                                 context, SemIR::WitnessType::SingletonInstId),
+                             .facet_value_inst_id = facet_inst_id,
+                             .index = SemIR::ElementIndex(index)});
+        return witness_id;
       }
     }
   }
   return SemIR::InstId::None;
 }
 
-// Finds the best impl among all available impls that provides the
-// `specific_interface` for the type in `type_const_id`, and returns a witness
-// for that impl. Returns `None` if no match was found.
-static auto FindWitnessInImpls(
-    Context& context, SemIR::LocId loc_id,
-    SemIR::ConstantId query_self_const_id,
-    const SemIR::SpecificInterface& specific_interface) -> SemIR::InstId {
-  auto& stack = context.impl_lookup_stack();
-
-  struct CandidateImpl {
-    SemIR::ImplId impl_id;
-    SemIR::InstId loc_inst_id;
-    TypeStructure type_structure;
-  };
-
-  auto query_type_structure = BuildTypeStructure(
-      context, context.constant_values().GetInstId(query_self_const_id),
-      specific_interface);
-
-  llvm::SmallVector<CandidateImpl> candidate_impl_ids;
-  for (auto [id, impl] : context.impls().enumerate()) {
-    // If the impl's interface_id differs from the query, then this impl can not
-    // possibly provide the queried interface.
-    if (impl.interface.interface_id != specific_interface.interface_id) {
-      continue;
-    }
-
-    // When the impl's interface_id matches, but the interface is generic, the
-    // impl may or may not match based on restrictions in the generic parameters
-    // of the impl.
-    //
-    // As a shortcut, if the impl's constraint is not symbolic (does not depend
-    // on any generic parameters), then we can determine that we match if the
-    // specific ids match exactly.
-    auto impl_interface_const_id =
-        context.constant_values().Get(impl.constraint_id);
-    if (!impl_interface_const_id.is_symbolic()) {
-      if (impl.interface.specific_id != specific_interface.specific_id) {
-        continue;
-      }
-    }
-
-    // This check comes first to avoid deduction with an invalid impl. We use an
-    // error value to indicate an error during creation of the impl, such as a
-    // recursive impl which will cause deduction to recurse infinitely.
-    if (impl.witness_id == SemIR::ErrorInst::SingletonInstId) {
-      continue;
-    }
-    CARBON_CHECK(impl.witness_id.has_value());
-
-    auto type_structure =
-        BuildTypeStructure(context, impl.self_id, impl.interface);
-    if (!query_type_structure.IsCompatibleWith(type_structure)) {
-      continue;
-    }
-
-    candidate_impl_ids.push_back(
-        {id, impl.definition_id, std::move(type_structure)});
-  }
-
-  auto compare = [](auto& lhs, auto& rhs) -> bool {
-    // TODO: Allow Carbon code to provide a priority ordering explicitly. For
-    // now they have all the same priority, so the priority is the order in
-    // which they are found in code.
-
-    // Sort by their type structures. Higher value in type structure comes
-    // first, so we use `>` comparison.
-    return lhs.type_structure > rhs.type_structure;
-  };
-  // Stable sort is used so that impls that are seen first are preferred when
-  // they have an equal priority ordering.
-  std::ranges::stable_sort(candidate_impl_ids, compare);
-
-  for (const auto& candidate : candidate_impl_ids) {
-    stack.back().impl_loc = candidate.loc_inst_id;
-    // NOTE: GetWitnessIdForImpl() does deduction, which can cause new impls to
-    // be imported, invalidating any pointer into `context.impls()`.
-    auto witness_id =
-        GetWitnessIdForImpl(context, loc_id, query_self_const_id,
-                            specific_interface, candidate.impl_id);
-    if (witness_id.has_value()) {
-      return witness_id;
-    }
+// Begin a search for an impl declaration matching the query. We do this by
+// creating an ImplSymbolicWitness instruction and evaluating. If it's able to
+// find a final concrete impl, then it will evaluate to that `ImplWitness` but
+// if not, it will evaluate to itself as a symbolic witness to be further
+// evaluated with a more specific query when building a specific for the generic
+// context the query came from.
+static auto FindWitnessInImpls(Context& context, SemIR::LocId loc_id,
+                               SemIR::ConstantId query_self_const_id,
+                               SemIR::SpecificInterface interface)
+    -> SemIR::InstId {
+  auto witness_const_id = TryEvalInst(
+      context, loc_id, SemIR::InstId::None,
+      SemIR::ImplSymbolicWitness{
+          .type_id =
+              GetSingletonType(context, SemIR::WitnessType::SingletonInstId),
+          .query_self_inst_id =
+              context.constant_values().GetInstId(query_self_const_id),
+          .query_specific_interface_id =
+              context.specific_interfaces().Add(interface),
+      });
+  // We use a NotConstant result from eval to communicate back an impl
+  // lookup failure. See `EvalConstantInst()` for `ImplSymbolicWitness`.
+  if (!witness_const_id.is_constant()) {
+    return SemIR::InstId::None;
   }
-  return SemIR::InstId::None;
+  return context.constant_values().GetInstId(witness_const_id);
 }
 
 auto LookupImplWitness(Context& context, SemIR::LocId loc_id,
@@ -413,16 +371,6 @@ auto LookupImplWitness(Context& context, SemIR::LocId loc_id,
         context.constant_values().GetInstId(query_facet_type_const_id)));
   }
 
-  // If the self type is a FacetAccessType, work with the facet value directly,
-  // which gives us the potential witnesses to avoid looking for impl
-  // declarations. We will do the same for the impl declarations we try to match
-  // so that we can compare the self constant values.
-  if (auto access = context.insts().TryGetAs<SemIR::FacetAccessType>(
-          context.constant_values().GetInstId(query_self_const_id))) {
-    query_self_const_id =
-        context.constant_values().Get(access->facet_value_inst_id);
-  }
-
   auto import_irs = FindAssociatedImportIRs(context, query_self_const_id,
                                             query_facet_type_const_id);
   for (auto import_ir : import_irs) {
@@ -436,6 +384,16 @@ auto LookupImplWitness(Context& context, SemIR::LocId loc_id,
     }
   }
 
+  // If the self type is a FacetAccessType, work with the facet value directly,
+  // which gives us the potential witnesses to avoid looking for impl
+  // declarations. We will do the same for the impl declarations we try to match
+  // so that we can compare the self constant values.
+  if (auto access = context.insts().TryGetAs<SemIR::FacetAccessType>(
+          context.constant_values().GetInstId(query_self_const_id))) {
+    query_self_const_id =
+        context.constant_values().Get(access->facet_value_inst_id);
+  }
+
   if (FindAndDiagnoseImplLookupCycle(context, context.impl_lookup_stack(),
                                      loc_id, query_self_const_id,
                                      query_facet_type_const_id)) {
@@ -453,42 +411,20 @@ auto LookupImplWitness(Context& context, SemIR::LocId loc_id,
     return SemIR::InstBlockId::Empty;
   }
 
-  llvm::SmallVector<SemIR::InstId> result_witness_ids;
-
   auto& stack = context.impl_lookup_stack();
   stack.push_back({
       .query_self_const_id = query_self_const_id,
       .query_facet_type_const_id = query_facet_type_const_id,
   });
-
-  // We look for a witness in two different places if the query self type is a
-  // facet value. First we try to find a witness on the facet value itself. This
-  // avoids the need to do impl lookups which are more expensive. If that fails,
-  // then we go look for an impl declaration as we would for other self types.
-  auto facet_value_self_const_id = query_self_const_id;
-
-  // When the query is a concrete FacetValue, we want to look through it at the
-  // underlying type to find all interfaces it implements. This supports
-  // conversion from a FacetValue to any other possible FacetValue, since
-  // conversion depends on impl lookup to verify it is a valid type change. See
-  // https://github.com/carbon-language/carbon-lang/issues/5137. We can't do
-  // this step earlier than inside impl lookup since we want the converted facet
-  // value in `facet_value_self_const_id` to avoid looking for impl
-  // declarations.
-  if (auto facet_value = context.insts().TryGetAs<SemIR::FacetValue>(
-          context.constant_values().GetInstId(query_self_const_id))) {
-    query_self_const_id =
-        context.constant_values().Get(facet_value->type_inst_id);
-  }
-
   // We need to find a witness for each interface in `interfaces`. Every
   // consumer of a facet type needs to agree on the order of interfaces used for
   // its witnesses.
+  llvm::SmallVector<SemIR::InstId> result_witness_ids;
   for (const auto& interface : interfaces) {
     // TODO: Since both `interfaces` and `query_self_const_id` are sorted lists,
     // do an O(N+M) merge instead of O(N*M) nested loops.
-    auto result_witness_id = FindWitnessInFacet(
-        context, loc_id, facet_value_self_const_id, interface);
+    auto result_witness_id =
+        FindWitnessInFacet(context, loc_id, query_self_const_id, interface);
     if (!result_witness_id.has_value()) {
       result_witness_id =
           FindWitnessInImpls(context, loc_id, query_self_const_id, interface);
@@ -515,4 +451,163 @@ auto LookupImplWitness(Context& context, SemIR::LocId loc_id,
   return context.inst_blocks().AddCanonical(result_witness_ids);
 }
 
+// Returns whether the query is concrete, it is false if the self type or
+// interface specifics have a symbolic dependency.
+static auto QueryIsConcrete(Context& context, SemIR::ConstantId self_const_id,
+                            SemIR::SpecificInterface& specific_interface)
+    -> bool {
+  if (!self_const_id.is_concrete()) {
+    return false;
+  }
+  if (!specific_interface.specific_id.has_value()) {
+    return true;
+  }
+  auto args_id =
+      context.specifics().Get(specific_interface.specific_id).args_id;
+  for (auto inst_id : context.inst_blocks().Get(args_id)) {
+    if (!context.constant_values().Get(inst_id).is_concrete()) {
+      return false;
+    }
+  }
+  return true;
+}
+
+struct CandidateImpl {
+  SemIR::ImplId impl_id;
+  SemIR::InstId loc_inst_id;
+
+  // Used for sorting the candidates to find the most-specialized match.
+  TypeStructure type_structure;
+};
+
+// Returns the list of candidates impls for lookup to select from.
+static auto CollectCandidateImplsForQuery(
+    Context& context, const TypeStructure& query_type_structure,
+    SemIR::SpecificInterface& query_specific_interface)
+    -> llvm::SmallVector<CandidateImpl> {
+  llvm::SmallVector<CandidateImpl> candidate_impls;
+  for (auto [id, impl] : context.impls().enumerate()) {
+    // If the impl's interface_id differs from the query, then this impl can
+    // not possibly provide the queried interface.
+    if (impl.interface.interface_id != query_specific_interface.interface_id) {
+      continue;
+    }
+
+    // When the impl's interface_id matches, but the interface is generic, the
+    // impl may or may not match based on restrictions in the generic
+    // parameters of the impl.
+    //
+    // As a shortcut, if the impl's constraint is not symbolic (does not
+    // depend on any generic parameters), then we can determine whether we match
+    // by looking if the specific ids match exactly.
+    auto impl_interface_const_id =
+        context.constant_values().Get(impl.constraint_id);
+    if (!impl_interface_const_id.is_symbolic() &&
+        impl.interface.specific_id != query_specific_interface.specific_id) {
+      continue;
+    }
+
+    // This check comes first to avoid deduction with an invalid impl. We use
+    // an error value to indicate an error during creation of the impl, such
+    // as a recursive impl which will cause deduction to recurse infinitely.
+    if (impl.witness_id == SemIR::ErrorInst::SingletonInstId) {
+      continue;
+    }
+    CARBON_CHECK(impl.witness_id.has_value());
+
+    // Build the type structure used for choosing the best the candidate.
+    auto type_structure =
+        BuildTypeStructure(context, impl.self_id, impl.interface);
+    // TODO: We can skip the comparison here if the `impl_interface_const_id` is
+    // not symbolic, since when the interface and specific ids match, and they
+    // aren't symbolic, the structure will be identical.
+    if (!query_type_structure.IsCompatibleWith(type_structure)) {
+      continue;
+    }
+
+    candidate_impls.push_back(
+        {id, impl.definition_id, std::move(type_structure)});
+  }
+
+  auto compare = [](auto& lhs, auto& rhs) -> bool {
+    // TODO: Allow Carbon code to provide a priority ordering explicitly. For
+    // now they have all the same priority, so the priority is the order in
+    // which they are found in code.
+
+    // Sort by their type structures. Higher value in type structure comes
+    // first, so we use `>` comparison.
+    return lhs.type_structure > rhs.type_structure;
+  };
+  // Stable sort is used so that impls that are seen first are preferred when
+  // they have an equal priority ordering.
+  llvm::stable_sort(candidate_impls, compare);
+
+  return candidate_impls;
+}
+
+auto EvalLookupSingleImplWitness(Context& context, SemIR::LocId loc_id,
+                                 SemIR::ImplSymbolicWitness eval_query)
+    -> EvalImplLookupResult {
+  SemIR::ConstantId query_self_const_id =
+      context.constant_values().Get(eval_query.query_self_inst_id);
+  SemIR::SpecificInterfaceId query_specific_interface_id =
+      eval_query.query_specific_interface_id;
+
+  // NOTE: Do not retain this reference to the SpecificInterface obtained from a
+  // value store by SpecificInterfaceId. Doing impl lookup does deduce which can
+  // do more impl lookups, and impl lookup can add a new SpecificInterface to
+  // the store which can reallocate and invalidate any references held here into
+  // the store.
+  auto query_specific_interface =
+      context.specific_interfaces().Get(query_specific_interface_id);
+
+  // When the query is a concrete FacetValue, we want to look through it at the
+  // underlying type to find all interfaces it implements. This supports
+  // conversion from a FacetValue to any other possible FacetValue, since
+  // conversion depends on impl lookup to verify it is a valid type change. See
+  // https://github.com/carbon-language/carbon-lang/issues/5137. We can't do
+  // this step earlier than inside impl lookup since:
+  // - We want the converted facet value to be preserved in
+  //   `FindWitnessInFacet()` to avoid looking for impl declarations.
+  // - The constant self value may be modified during constant evaluation as a
+  //   more specific value is found.
+  if (auto facet_value = context.insts().TryGetAs<SemIR::FacetValue>(
+          context.constant_values().GetInstId(query_self_const_id))) {
+    query_self_const_id =
+        context.constant_values().Get(facet_value->type_inst_id);
+  }
+
+  auto query_type_structure = BuildTypeStructure(
+      context, context.constant_values().GetInstId(query_self_const_id),
+      query_specific_interface);
+  bool query_is_concrete =
+      QueryIsConcrete(context, query_self_const_id, query_specific_interface);
+
+  auto candidate_impls = CollectCandidateImplsForQuery(
+      context, query_type_structure, query_specific_interface);
+
+  for (const auto& candidate : candidate_impls) {
+    // In deferred lookup for a symbolic impl witness, while building a
+    // specific, there may be no stack yet as this may be the first lookup. If
+    // further lookups are started as a result in deduce, they will build the
+    // stack.
+    //
+    // NOTE: Don't retain a reference into the stack, it may be invalidated if
+    // we do further impl lookups when GetWitnessIdForImpl() does deduction.
+    if (!context.impl_lookup_stack().empty()) {
+      context.impl_lookup_stack().back().impl_loc = candidate.loc_inst_id;
+    }
+
+    // NOTE: GetWitnessIdForImpl() does deduction, which can cause new impls
+    // to be imported, invalidating any pointer into `context.impls()`.
+    auto result = GetWitnessIdForImpl(
+        context, loc_id, query_is_concrete, query_self_const_id,
+        query_specific_interface, candidate.impl_id);
+    if (result.has_value()) {
+      return result;
+    }
+  }
+  return EvalImplLookupResult::MakeNone();
+}
+
 }  // namespace Carbon::Check

toolchain/check/impl_lookup.h

@@ -5,8 +5,12 @@
 #ifndef CARBON_TOOLCHAIN_CHECK_IMPL_LOOKUP_H_
 #define CARBON_TOOLCHAIN_CHECK_IMPL_LOOKUP_H_
 
+#include <variant>
+
 #include "toolchain/check/context.h"
 #include "toolchain/sem_ir/ids.h"
+#include "toolchain/sem_ir/inst.h"
+#include "toolchain/sem_ir/typed_insts.h"
 
 namespace Carbon::Check {
 
@@ -35,6 +39,64 @@ auto LookupImplWitness(Context& context, SemIR::LocId loc_id,
                        SemIR::ConstantId query_facet_type_const_id)
     -> SemIR::InstBlockIdOrError;
 
+// The result of EvalLookupSingleImplWitness(). It can be one of:
+// - No value. Lookup failed to find an impl declaration.
+// - A concrete value. Lookup found a concrete impl declaration that can be
+//   used definitively.
+// - A symbolic value. Lookup found an impl but it is not returned since lookup
+//   will need to be done again with a more specific query to look for
+//   specializations.
+class EvalImplLookupResult {
+ public:
+  static auto MakeNone() -> EvalImplLookupResult {
+    return EvalImplLookupResult(SemIR::InstId::None);
+  }
+  static auto MakeFinal(SemIR::InstId inst_id) -> EvalImplLookupResult {
+    return EvalImplLookupResult(inst_id);
+  }
+  static auto MakeNonFinal() -> EvalImplLookupResult {
+    return EvalImplLookupResult(FoundNonFinalImpl());
+  }
+
+  // True if a concrete impl witness was found or a non-final impl. In the
+  // latter case the InstId of the impl's witness is not returned, only the fact
+  // that it exists.
+  auto has_value() const -> bool {
+    return std::holds_alternative<FoundNonFinalImpl>(result_) ||
+           std::get<SemIR::InstId>(result_).has_value();
+  }
+
+  // True if there is a concrete witness in the result. If false, and
+  // `has_value()` is true, it means a non-final impl was found and a further
+  // more specific query will need to be done.
+  auto has_concrete_value() const -> bool {
+    return std::holds_alternative<SemIR::InstId>(result_);
+  }
+
+  // Only valid if `has_concrete_value()` is true. Returns the witness id for
+  // the found impl declaration, or None if `has_value()` is false.
+  auto concrete_witness() const -> SemIR::InstId {
+    return std::get<SemIR::InstId>(result_);
+  }
+
+ private:
+  struct FoundNonFinalImpl {};
+
+  explicit EvalImplLookupResult(SemIR::InstId inst_id) : result_(inst_id) {}
+  explicit EvalImplLookupResult(FoundNonFinalImpl f) : result_(f) {}
+
+  std::variant<SemIR::InstId, FoundNonFinalImpl> result_;
+};
+
+// Looks for a witness instruction of an impl declaration for a query consisting
+// of a type value or facet value, and a single interface. This is for eval to
+// execute lookup via the ImplSymbolicWitness instruction. It does not consider
+// the self facet value for finding a witness, since LookupImplWitness() would
+// have found that and not caused us to defer lookup to here.
+auto EvalLookupSingleImplWitness(Context& context, SemIR::LocId loc_id,
+                                 SemIR::ImplSymbolicWitness eval_query)
+    -> EvalImplLookupResult;
+
 }  // namespace Carbon::Check
 
 #endif  // CARBON_TOOLCHAIN_CHECK_IMPL_LOOKUP_H_

toolchain/check/import_ref.cpp

@@ -278,6 +278,9 @@ class ImportContext {
     return import_ir().name_scopes();
   }
   auto import_specifics() -> decltype(auto) { return import_ir().specifics(); }
+  auto import_specific_interfaes() -> decltype(auto) {
+    return import_ir().specific_interfaces();
+  }
   auto import_string_literal_values() -> decltype(auto) {
     return import_ir().string_literal_values();
   }
@@ -338,6 +341,9 @@ class ImportContext {
     return local_ir().name_scopes();
   }
   auto local_specifics() -> decltype(auto) { return local_ir().specifics(); }
+  auto local_specific_interfaces() -> decltype(auto) {
+    return local_ir().specific_interfaces();
+  }
   auto local_string_literal_values() -> decltype(auto) {
     return local_ir().string_literal_values();
   }
@@ -2504,6 +2510,33 @@ static auto TryResolveTypedInst(ImportRefResolver& resolver,
            resolver, inst.witnesses_block_id, witnesses)});
 }
 
+static auto TryResolveTypedInst(ImportRefResolver& resolver,
+                                SemIR::ImplSymbolicWitness inst)
+    -> ResolveResult {
+  auto query_self_inst_id =
+      GetLocalConstantInstId(resolver, inst.query_self_inst_id);
+
+  const auto& import_specific_interface =
+      resolver.import_specific_interfaes().Get(
+          inst.query_specific_interface_id);
+  auto data = GetLocalSpecificInstanceData(resolver, import_specific_interface);
+
+  if (resolver.HasNewWork()) {
+    return ResolveResult::Retry();
+  }
+
+  auto specific_interface = GetLocalSpecificInterface(
+      resolver, import_specific_interface.specific_id, data);
+  auto query_specific_interface_id =
+      resolver.local_specific_interfaces().Add(specific_interface);
+  return ResolveAs<SemIR::ImplSymbolicWitness>(
+      resolver,
+      {.type_id = GetSingletonType(resolver.local_context(),
+                                   SemIR::WitnessType::SingletonInstId),
+       .query_self_inst_id = query_self_inst_id,
+       .query_specific_interface_id = query_specific_interface_id});
+}
+
 static auto TryResolveTypedInst(ImportRefResolver& resolver,
                                 SemIR::ImplWitness inst) -> ResolveResult {
   auto specific_data = GetLocalSpecificData(resolver, inst.specific_id);
@@ -2671,6 +2704,24 @@ static auto TryResolveTypedInst(ImportRefResolver& resolver,
       {.type_id = type_id, .callee_id = callee_id, .specific_id = specific_id});
 }
 
+static auto TryResolveTypedInst(ImportRefResolver& resolver,
+                                SemIR::SpecificImplFunction inst)
+    -> ResolveResult {
+  auto callee_id = GetLocalConstantInstId(resolver, inst.callee_id);
+  auto specific_data = GetLocalSpecificData(resolver, inst.specific_id);
+  if (resolver.HasNewWork()) {
+    return ResolveResult::Retry();
+  }
+
+  auto type_id = GetSingletonType(resolver.local_context(),
+                                  SemIR::SpecificFunctionType::SingletonInstId);
+  auto specific_id =
+      GetOrAddLocalSpecific(resolver, inst.specific_id, specific_data);
+  return ResolveAs<SemIR::SpecificImplFunction>(
+      resolver,
+      {.type_id = type_id, .callee_id = callee_id, .specific_id = specific_id});
+}
+
 static auto TryResolveTypedInst(ImportRefResolver& resolver,
                                 SemIR::StructType inst) -> ResolveResult {
   CARBON_CHECK(inst.type_id == SemIR::TypeType::SingletonTypeId);
@@ -2884,6 +2935,9 @@ static auto TryResolveInstCanonical(ImportRefResolver& resolver,
     case CARBON_KIND(SemIR::ImplDecl inst): {
       return TryResolveTypedInst(resolver, inst, const_id);
     }
+    case CARBON_KIND(SemIR::ImplSymbolicWitness inst): {
+      return TryResolveTypedInst(resolver, inst);
+    }
     case CARBON_KIND(SemIR::ImplWitness inst): {
       return TryResolveTypedInst(resolver, inst);
     }
@@ -2914,6 +2968,9 @@ static auto TryResolveInstCanonical(ImportRefResolver& resolver,
     case CARBON_KIND(SemIR::SpecificFunction inst): {
       return TryResolveTypedInst(resolver, inst);
     }
+    case CARBON_KIND(SemIR::SpecificImplFunction inst): {
+      return TryResolveTypedInst(resolver, inst);
+    }
     case CARBON_KIND(SemIR::SymbolicBindingPattern inst): {
       return TryResolveTypedInst(resolver, inst);
     }

toolchain/check/subst.cpp

@@ -104,6 +104,12 @@ static auto PushOperand(Context& context, Worklist& worklist,
     case SemIR::IdKind::For<SemIR::SpecificId>:
       push_specific(SemIR::SpecificId(arg));
       break;
+    case SemIR::IdKind::For<SemIR::SpecificInterfaceId>: {
+      auto interface =
+          context.specific_interfaces().Get(SemIR::SpecificInterfaceId(arg));
+      push_specific(interface.specific_id);
+      break;
+    }
     case SemIR::IdKind::For<SemIR::FacetTypeId>: {
       const auto& facet_type_info =
           context.facet_types().Get(SemIR::FacetTypeId(arg));
@@ -205,6 +211,17 @@ static auto PopOperand(Context& context, Worklist& worklist, SemIR::IdKind kind,
     case SemIR::IdKind::For<SemIR::SpecificId>: {
       return pop_specific(SemIR::SpecificId(arg)).index;
     }
+    case SemIR::IdKind::For<SemIR::SpecificInterfaceId>: {
+      auto interface =
+          context.specific_interfaces().Get(SemIR::SpecificInterfaceId(arg));
+      auto specific_id = pop_specific(interface.specific_id);
+      return context.specific_interfaces()
+          .Add({
+              .interface_id = interface.interface_id,
+              .specific_id = specific_id,
+          })
+          .index;
+    }
     case SemIR::IdKind::For<SemIR::FacetTypeId>: {
       const auto& old_facet_type_info =
           context.facet_types().Get(SemIR::FacetTypeId(arg));

toolchain/check/testdata/facet/min_prelude/convert_facet_value_to_narrowed_facet_type.carbon

@@ -743,8 +743,9 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:   %W.as_wit.iface0: <witness> = facet_access_witness %W, element0 [symbolic]
 // CHECK:STDOUT:   %Animal.facet: %Animal.type = facet_value %W.as_type, (%W.as_wit.iface0) [symbolic]
 // CHECK:STDOUT:   %impl_witness.1d8: <witness> = impl_witness (), @impl.e7b(%Animal.facet) [symbolic]
+// CHECK:STDOUT:   %Eats.impl_symbolic_witness: <witness> = impl_symbolic_witness %W, @Eats [symbolic]
 // CHECK:STDOUT:   %W.as_wit.iface1: <witness> = facet_access_witness %W, element1 [symbolic]
-// CHECK:STDOUT:   %facet_value: %facet_type.6ff = facet_value %W.as_type, (%impl_witness.1d8, %W.as_wit.iface1) [symbolic]
+// CHECK:STDOUT:   %facet_value: %facet_type.6ff = facet_value %W.as_type, (%Eats.impl_symbolic_witness, %W.as_wit.iface1) [symbolic]
 // CHECK:STDOUT:   %FeedTame2.specific_fn: <specific function> = specific_function %FeedTame2, @FeedTame2(%facet_value) [symbolic]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
@@ -941,8 +942,8 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:   %W.as_wit.iface0.loc12_14.3: <witness> = facet_access_witness %W.loc11_22.2, element0 [symbolic = %W.as_wit.iface0.loc12_14.3 (constants.%W.as_wit.iface0)]
 // CHECK:STDOUT:   %Animal.facet.loc12_14.3: %Animal.type = facet_value %W.as_type.loc11_44.2, (%W.as_wit.iface0.loc12_14.3) [symbolic = %Animal.facet.loc12_14.3 (constants.%Animal.facet)]
 // CHECK:STDOUT:   %W.as_wit.iface1.loc12_14.3: <witness> = facet_access_witness %W.loc11_22.2, element1 [symbolic = %W.as_wit.iface1.loc12_14.3 (constants.%W.as_wit.iface1)]
-// CHECK:STDOUT:   %impl_witness: <witness> = impl_witness (), @impl.e7b(%Animal.facet.loc12_14.3) [symbolic = %impl_witness (constants.%impl_witness.1d8)]
-// CHECK:STDOUT:   %facet_value.loc12_14.3: %facet_type.6ff = facet_value %W.as_type.loc11_44.2, (%impl_witness, %W.as_wit.iface1.loc12_14.3) [symbolic = %facet_value.loc12_14.3 (constants.%facet_value)]
+// CHECK:STDOUT:   %Eats.impl_symbolic_witness: <witness> = impl_symbolic_witness %W.loc11_22.2, @Eats [symbolic = %Eats.impl_symbolic_witness (constants.%Eats.impl_symbolic_witness)]
+// CHECK:STDOUT:   %facet_value.loc12_14.3: %facet_type.6ff = facet_value %W.as_type.loc11_44.2, (%Eats.impl_symbolic_witness, %W.as_wit.iface1.loc12_14.3) [symbolic = %facet_value.loc12_14.3 (constants.%facet_value)]
 // CHECK:STDOUT:   %FeedTame2.specific_fn.loc12_3.2: <specific function> = specific_function constants.%FeedTame2, @FeedTame2(%facet_value.loc12_14.3) [symbolic = %FeedTame2.specific_fn.loc12_3.2 (constants.%FeedTame2.specific_fn)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   fn[%W.patt.loc11_22.1: %facet_type.65c](%w.param_patt: @HandleTameAnimal2.%W.as_type.loc11_44.2 (%W.as_type)) {
@@ -955,7 +956,7 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:     %Animal.facet.loc12_14.1: %Animal.type = facet_value constants.%W.as_type, (%W.as_wit.iface0.loc12_14.1) [symbolic = %Animal.facet.loc12_14.3 (constants.%Animal.facet)]
 // CHECK:STDOUT:     %.loc12_14.2: %Animal.type = converted %.loc12_14.1, %Animal.facet.loc12_14.1 [symbolic = %Animal.facet.loc12_14.3 (constants.%Animal.facet)]
 // CHECK:STDOUT:     %W.as_wit.iface1.loc12_14.1: <witness> = facet_access_witness constants.%W, element1 [symbolic = %W.as_wit.iface1.loc12_14.3 (constants.%W.as_wit.iface1)]
-// CHECK:STDOUT:     %facet_value.loc12_14.1: %facet_type.6ff = facet_value constants.%W.as_type, (constants.%impl_witness.1d8, %W.as_wit.iface1.loc12_14.1) [symbolic = %facet_value.loc12_14.3 (constants.%facet_value)]
+// CHECK:STDOUT:     %facet_value.loc12_14.1: %facet_type.6ff = facet_value constants.%W.as_type, (constants.%Eats.impl_symbolic_witness, %W.as_wit.iface1.loc12_14.1) [symbolic = %facet_value.loc12_14.3 (constants.%facet_value)]
 // CHECK:STDOUT:     %.loc12_14.3: %facet_type.6ff = converted constants.%W.as_type, %facet_value.loc12_14.1 [symbolic = %facet_value.loc12_14.3 (constants.%facet_value)]
 // CHECK:STDOUT:     %W.as_type.loc12_14.2: type = facet_access_type constants.%W [symbolic = %W.as_type.loc11_44.2 (constants.%W.as_type)]
 // CHECK:STDOUT:     %.loc12_14.4: type = converted constants.%W, %W.as_type.loc12_14.2 [symbolic = %W.as_type.loc11_44.2 (constants.%W.as_type)]
@@ -963,7 +964,7 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:     %Animal.facet.loc12_14.2: %Animal.type = facet_value constants.%W.as_type, (%W.as_wit.iface0.loc12_14.2) [symbolic = %Animal.facet.loc12_14.3 (constants.%Animal.facet)]
 // CHECK:STDOUT:     %.loc12_14.5: %Animal.type = converted %.loc12_14.4, %Animal.facet.loc12_14.2 [symbolic = %Animal.facet.loc12_14.3 (constants.%Animal.facet)]
 // CHECK:STDOUT:     %W.as_wit.iface1.loc12_14.2: <witness> = facet_access_witness constants.%W, element1 [symbolic = %W.as_wit.iface1.loc12_14.3 (constants.%W.as_wit.iface1)]
-// CHECK:STDOUT:     %facet_value.loc12_14.2: %facet_type.6ff = facet_value constants.%W.as_type, (constants.%impl_witness.1d8, %W.as_wit.iface1.loc12_14.2) [symbolic = %facet_value.loc12_14.3 (constants.%facet_value)]
+// CHECK:STDOUT:     %facet_value.loc12_14.2: %facet_type.6ff = facet_value constants.%W.as_type, (constants.%Eats.impl_symbolic_witness, %W.as_wit.iface1.loc12_14.2) [symbolic = %facet_value.loc12_14.3 (constants.%facet_value)]
 // CHECK:STDOUT:     %.loc12_14.6: %facet_type.6ff = converted constants.%W.as_type, %facet_value.loc12_14.2 [symbolic = %facet_value.loc12_14.3 (constants.%facet_value)]
 // CHECK:STDOUT:     %FeedTame2.specific_fn.loc12_3.1: <specific function> = specific_function %FeedTame2.ref, @FeedTame2(constants.%facet_value) [symbolic = %FeedTame2.specific_fn.loc12_3.2 (constants.%FeedTame2.specific_fn)]
 // CHECK:STDOUT:     %FeedTame2.call: init %empty_tuple.type = call %FeedTame2.specific_fn.loc12_3.1(%w.ref)
@@ -1044,8 +1045,6 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:   %require_complete => constants.%require_complete.ba9
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @impl.e7b(@HandleTameAnimal2.%Animal.facet.loc12_14.3) {}
-// CHECK:STDOUT:
 // CHECK:STDOUT: specific @FeedTame2(@HandleTameAnimal2.%facet_value.loc12_14.3) {}
 // CHECK:STDOUT:
 // CHECK:STDOUT: --- equivalent.carbon

toolchain/check/testdata/facet/min_prelude/convert_facet_value_value_to_blanket_impl.carbon

@@ -45,7 +45,8 @@ fn HandleAnimal[T:! Animal](a: T) { Feed(a); }
 // CHECK:STDOUT:   %HandleAnimal: %HandleAnimal.type = struct_value () [concrete]
 // CHECK:STDOUT:   %require_complete.234: <witness> = require_complete_type %T.as_type.2ad [symbolic]
 // CHECK:STDOUT:   %impl_witness.11010a.2: <witness> = impl_witness (), @impl(%T.fd4) [symbolic]
-// CHECK:STDOUT:   %Eats.facet: %Eats.type = facet_value %T.as_type.2ad, (%impl_witness.11010a.2) [symbolic]
+// CHECK:STDOUT:   %Eats.impl_symbolic_witness: <witness> = impl_symbolic_witness %T.fd4, @Eats [symbolic]
+// CHECK:STDOUT:   %Eats.facet: %Eats.type = facet_value %T.as_type.2ad, (%Eats.impl_symbolic_witness) [symbolic]
 // CHECK:STDOUT:   %Feed.specific_fn: <specific function> = specific_function %Feed, @Feed(%Eats.facet) [symbolic]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
@@ -160,8 +161,8 @@ fn HandleAnimal[T:! Animal](a: T) { Feed(a); }
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT:   %require_complete: <witness> = require_complete_type @HandleAnimal.%T.as_type.loc21_32.2 (%T.as_type.2ad) [symbolic = %require_complete (constants.%require_complete.234)]
-// CHECK:STDOUT:   %impl_witness: <witness> = impl_witness (), @impl(%T.loc21_17.2) [symbolic = %impl_witness (constants.%impl_witness.11010a.2)]
-// CHECK:STDOUT:   %Eats.facet.loc21_43.3: %Eats.type = facet_value %T.as_type.loc21_32.2, (%impl_witness) [symbolic = %Eats.facet.loc21_43.3 (constants.%Eats.facet)]
+// CHECK:STDOUT:   %Eats.impl_symbolic_witness: <witness> = impl_symbolic_witness %T.loc21_17.2, @Eats [symbolic = %Eats.impl_symbolic_witness (constants.%Eats.impl_symbolic_witness)]
+// CHECK:STDOUT:   %Eats.facet.loc21_43.3: %Eats.type = facet_value %T.as_type.loc21_32.2, (%Eats.impl_symbolic_witness) [symbolic = %Eats.facet.loc21_43.3 (constants.%Eats.facet)]
 // CHECK:STDOUT:   %Feed.specific_fn.loc21_37.2: <specific function> = specific_function constants.%Feed, @Feed(%Eats.facet.loc21_43.3) [symbolic = %Feed.specific_fn.loc21_37.2 (constants.%Feed.specific_fn)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   fn[%T.patt.loc21_17.1: %Animal.type](%a.param_patt: @HandleAnimal.%T.as_type.loc21_32.2 (%T.as_type.2ad)) {
@@ -171,12 +172,12 @@ fn HandleAnimal[T:! Animal](a: T) { Feed(a); }
 // CHECK:STDOUT:     %T.as_type.loc21_43.1: type = facet_access_type constants.%T.fd4 [symbolic = %T.as_type.loc21_32.2 (constants.%T.as_type.2ad)]
 // CHECK:STDOUT:     %.loc21_43.1: type = converted constants.%T.fd4, %T.as_type.loc21_43.1 [symbolic = %T.as_type.loc21_32.2 (constants.%T.as_type.2ad)]
 // CHECK:STDOUT:     %.loc21_43.2: %Animal.type = converted %.loc21_43.1, constants.%T.fd4 [symbolic = %T.loc21_17.2 (constants.%T.fd4)]
-// CHECK:STDOUT:     %Eats.facet.loc21_43.1: %Eats.type = facet_value constants.%T.as_type.2ad, (constants.%impl_witness.11010a.2) [symbolic = %Eats.facet.loc21_43.3 (constants.%Eats.facet)]
+// CHECK:STDOUT:     %Eats.facet.loc21_43.1: %Eats.type = facet_value constants.%T.as_type.2ad, (constants.%Eats.impl_symbolic_witness) [symbolic = %Eats.facet.loc21_43.3 (constants.%Eats.facet)]
 // CHECK:STDOUT:     %.loc21_43.3: %Eats.type = converted constants.%T.as_type.2ad, %Eats.facet.loc21_43.1 [symbolic = %Eats.facet.loc21_43.3 (constants.%Eats.facet)]
 // CHECK:STDOUT:     %T.as_type.loc21_43.2: type = facet_access_type constants.%T.fd4 [symbolic = %T.as_type.loc21_32.2 (constants.%T.as_type.2ad)]
 // CHECK:STDOUT:     %.loc21_43.4: type = converted constants.%T.fd4, %T.as_type.loc21_43.2 [symbolic = %T.as_type.loc21_32.2 (constants.%T.as_type.2ad)]
 // CHECK:STDOUT:     %.loc21_43.5: %Animal.type = converted %.loc21_43.4, constants.%T.fd4 [symbolic = %T.loc21_17.2 (constants.%T.fd4)]
-// CHECK:STDOUT:     %Eats.facet.loc21_43.2: %Eats.type = facet_value constants.%T.as_type.2ad, (constants.%impl_witness.11010a.2) [symbolic = %Eats.facet.loc21_43.3 (constants.%Eats.facet)]
+// CHECK:STDOUT:     %Eats.facet.loc21_43.2: %Eats.type = facet_value constants.%T.as_type.2ad, (constants.%Eats.impl_symbolic_witness) [symbolic = %Eats.facet.loc21_43.3 (constants.%Eats.facet)]
 // CHECK:STDOUT:     %.loc21_43.6: %Eats.type = converted constants.%T.as_type.2ad, %Eats.facet.loc21_43.2 [symbolic = %Eats.facet.loc21_43.3 (constants.%Eats.facet)]
 // CHECK:STDOUT:     %Feed.specific_fn.loc21_37.1: <specific function> = specific_function %Feed.ref, @Feed(constants.%Eats.facet) [symbolic = %Feed.specific_fn.loc21_37.2 (constants.%Feed.specific_fn)]
 // CHECK:STDOUT:     %Feed.call: init %empty_tuple.type = call %Feed.specific_fn.loc21_37.1(%a.ref)
@@ -223,8 +224,6 @@ fn HandleAnimal[T:! Animal](a: T) { Feed(a); }
 // CHECK:STDOUT:   %require_complete => constants.%require_complete.234
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @impl(@HandleAnimal.%T.loc21_17.2) {}
-// CHECK:STDOUT:
 // CHECK:STDOUT: specific @Feed(@HandleAnimal.%Eats.facet.loc21_43.3) {}
 // CHECK:STDOUT:
 // CHECK:STDOUT: --- include_files/convert.carbon

toolchain/check/testdata/facet/min_prelude/convert_facet_value_value_to_generic_facet_value_value.carbon

@@ -84,8 +84,9 @@ fn F() {
 // CHECK:STDOUT:   %Eats.type.f54c3d.2: type = facet_type <@Eats, @Eats(%Food.as_type.fae)> [symbolic]
 // CHECK:STDOUT:   %require_complete.42532a.2: <witness> = require_complete_type %Eats.type.f54c3d.2 [symbolic]
 // CHECK:STDOUT:   %impl_witness.c7c36b.2: <witness> = impl_witness (), @impl.009(%T.fd4, %Food.5fe) [symbolic]
-// CHECK:STDOUT:   %Eats.facet.97e: %Eats.type.f54c3d.2 = facet_value %T.as_type.2ad, (%impl_witness.c7c36b.2) [symbolic]
-// CHECK:STDOUT:   %Feed.specific_fn.387: <specific function> = specific_function %Feed, @Feed(%Food.5fe, %Eats.facet.97e) [symbolic]
+// CHECK:STDOUT:   %Eats.impl_symbolic_witness: <witness> = impl_symbolic_witness %T.fd4, @Eats, @Eats(%Food.as_type.fae) [symbolic]
+// CHECK:STDOUT:   %Eats.facet.eea: %Eats.type.f54c3d.2 = facet_value %T.as_type.2ad, (%Eats.impl_symbolic_witness) [symbolic]
+// CHECK:STDOUT:   %Feed.specific_fn.824: <specific function> = specific_function %Feed, @Feed(%Food.5fe, %Eats.facet.eea) [symbolic]
 // CHECK:STDOUT:   %F.type: type = fn_type @F [concrete]
 // CHECK:STDOUT:   %F: %F.type = struct_value () [concrete]
 // CHECK:STDOUT:   %Goat.val: %Goat = struct_value () [concrete]
@@ -218,6 +219,10 @@ fn F() {
 // CHECK:STDOUT:     %food: @HandleAnimal.%Food.as_type.loc31_56.2 (%Food.as_type.fae) = bind_name food, %food.param
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %F.decl: %F.type = fn_decl @F [concrete = constants.%F] {} {}
+// CHECK:STDOUT:   %Edible.facet: %Edible.type = facet_value constants.%Grass, (constants.%impl_witness.1bc) [concrete = constants.%Edible.facet]
+// CHECK:STDOUT:   %.loc31_76.1: %Edible.type = converted constants.%Grass, %Edible.facet [concrete = constants.%Edible.facet]
+// CHECK:STDOUT:   %Animal.facet: %Animal.type = facet_value constants.%Goat, (constants.%impl_witness.1bc) [concrete = constants.%Animal.facet]
+// CHECK:STDOUT:   %.loc31_76.2: %Animal.type = converted constants.%Goat, %Animal.facet [concrete = constants.%Animal.facet]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: interface @Edible {
@@ -329,9 +334,9 @@ fn F() {
 // CHECK:STDOUT:   %require_complete.loc31_45: <witness> = require_complete_type @HandleAnimal.%T.as_type.loc31_47.2 (%T.as_type.2ad) [symbolic = %require_complete.loc31_45 (constants.%require_complete.234)]
 // CHECK:STDOUT:   %require_complete.loc31_54: <witness> = require_complete_type @HandleAnimal.%Food.as_type.loc31_56.2 (%Food.as_type.fae) [symbolic = %require_complete.loc31_54 (constants.%require_complete.444)]
 // CHECK:STDOUT:   %Eats.type: type = facet_type <@Eats, @Eats(%Food.as_type.loc31_56.2)> [symbolic = %Eats.type (constants.%Eats.type.f54c3d.2)]
-// CHECK:STDOUT:   %impl_witness: <witness> = impl_witness (), @impl.009(%T.loc31_17.2, %Food.loc31_29.2) [symbolic = %impl_witness (constants.%impl_witness.c7c36b.2)]
-// CHECK:STDOUT:   %Eats.facet.loc31_76.2: @HandleAnimal.%Eats.type (%Eats.type.f54c3d.2) = facet_value %T.as_type.loc31_47.2, (%impl_witness) [symbolic = %Eats.facet.loc31_76.2 (constants.%Eats.facet.97e)]
-// CHECK:STDOUT:   %Feed.specific_fn.loc31_64.2: <specific function> = specific_function constants.%Feed, @Feed(%Food.loc31_29.2, %Eats.facet.loc31_76.2) [symbolic = %Feed.specific_fn.loc31_64.2 (constants.%Feed.specific_fn.387)]
+// CHECK:STDOUT:   %Eats.impl_symbolic_witness: <witness> = impl_symbolic_witness %T.loc31_17.2, @Eats, @Eats(%Food.as_type.loc31_56.2) [symbolic = %Eats.impl_symbolic_witness (constants.%Eats.impl_symbolic_witness)]
+// CHECK:STDOUT:   %Eats.facet.loc31_76.2: @HandleAnimal.%Eats.type (%Eats.type.f54c3d.2) = facet_value %T.as_type.loc31_47.2, (%Eats.impl_symbolic_witness) [symbolic = %Eats.facet.loc31_76.2 (constants.%Eats.facet.eea)]
+// CHECK:STDOUT:   %Feed.specific_fn.loc31_64.2: <specific function> = specific_function constants.%Feed, @Feed(%Food.loc31_29.2, %Eats.facet.loc31_76.2) [symbolic = %Feed.specific_fn.loc31_64.2 (constants.%Feed.specific_fn.824)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   fn[%T.patt.loc31_17.1: %Animal.type, %Food.patt.loc31_29.1: %Edible.type](%a.param_patt: @HandleAnimal.%T.as_type.loc31_47.2 (%T.as_type.2ad), %food.param_patt: @HandleAnimal.%Food.as_type.loc31_56.2 (%Food.as_type.fae)) {
 // CHECK:STDOUT:   !entry:
@@ -344,9 +349,9 @@ fn F() {
 // CHECK:STDOUT:     %T.as_type.loc31_76: type = facet_access_type constants.%T.fd4 [symbolic = %T.as_type.loc31_47.2 (constants.%T.as_type.2ad)]
 // CHECK:STDOUT:     %.loc31_76.4: type = converted constants.%T.fd4, %T.as_type.loc31_76 [symbolic = %T.as_type.loc31_47.2 (constants.%T.as_type.2ad)]
 // CHECK:STDOUT:     %.loc31_76.5: %Animal.type = converted %.loc31_76.4, constants.%T.fd4 [symbolic = %T.loc31_17.2 (constants.%T.fd4)]
-// CHECK:STDOUT:     %Eats.facet.loc31_76.1: @HandleAnimal.%Eats.type (%Eats.type.f54c3d.2) = facet_value constants.%T.as_type.2ad, (constants.%impl_witness.c7c36b.2) [symbolic = %Eats.facet.loc31_76.2 (constants.%Eats.facet.97e)]
-// CHECK:STDOUT:     %.loc31_76.6: @HandleAnimal.%Eats.type (%Eats.type.f54c3d.2) = converted constants.%T.as_type.2ad, %Eats.facet.loc31_76.1 [symbolic = %Eats.facet.loc31_76.2 (constants.%Eats.facet.97e)]
-// CHECK:STDOUT:     %Feed.specific_fn.loc31_64.1: <specific function> = specific_function %Feed.ref, @Feed(constants.%Food.5fe, constants.%Eats.facet.97e) [symbolic = %Feed.specific_fn.loc31_64.2 (constants.%Feed.specific_fn.387)]
+// CHECK:STDOUT:     %Eats.facet.loc31_76.1: @HandleAnimal.%Eats.type (%Eats.type.f54c3d.2) = facet_value constants.%T.as_type.2ad, (constants.%Eats.impl_symbolic_witness) [symbolic = %Eats.facet.loc31_76.2 (constants.%Eats.facet.eea)]
+// CHECK:STDOUT:     %.loc31_76.6: @HandleAnimal.%Eats.type (%Eats.type.f54c3d.2) = converted constants.%T.as_type.2ad, %Eats.facet.loc31_76.1 [symbolic = %Eats.facet.loc31_76.2 (constants.%Eats.facet.eea)]
+// CHECK:STDOUT:     %Feed.specific_fn.loc31_64.1: <specific function> = specific_function %Feed.ref, @Feed(constants.%Food.5fe, constants.%Eats.facet.eea) [symbolic = %Feed.specific_fn.loc31_64.2 (constants.%Feed.specific_fn.824)]
 // CHECK:STDOUT:     %Feed.call: init %empty_tuple.type = call %Feed.specific_fn.loc31_64.1(%a.ref, %food.ref)
 // CHECK:STDOUT:     return
 // CHECK:STDOUT:   }
@@ -459,13 +464,13 @@ fn F() {
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @Feed(constants.%Food.5fe, constants.%Eats.facet.97e) {
+// CHECK:STDOUT: specific @Feed(constants.%Food.5fe, constants.%Eats.facet.eea) {
 // CHECK:STDOUT:   %Food.loc30_9.2 => constants.%Food.5fe
 // CHECK:STDOUT:   %Food.patt.loc30_9.2 => constants.%Food.5fe
 // CHECK:STDOUT:   %Food.as_type.loc30_37.2 => constants.%Food.as_type.fae
 // CHECK:STDOUT:   %Eats.type.loc30_37.2 => constants.%Eats.type.f54c3d.2
-// CHECK:STDOUT:   %T.loc30_24.2 => constants.%Eats.facet.97e
-// CHECK:STDOUT:   %T.patt.loc30_24.2 => constants.%Eats.facet.97e
+// CHECK:STDOUT:   %T.loc30_24.2 => constants.%Eats.facet.eea
+// CHECK:STDOUT:   %T.patt.loc30_24.2 => constants.%Eats.facet.eea
 // CHECK:STDOUT:   %T.as_type.loc30_43.2 => constants.%T.as_type.2ad
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
@@ -475,8 +480,6 @@ fn F() {
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @Eats(@HandleAnimal.%Food.as_type.loc31_56.2) {}
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @impl.009(@HandleAnimal.%T.loc31_17.2, @HandleAnimal.%Food.loc31_29.2) {}
-// CHECK:STDOUT:
 // CHECK:STDOUT: specific @Feed(@HandleAnimal.%Food.loc31_29.2, @HandleAnimal.%Eats.facet.loc31_76.2) {}
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @HandleAnimal(constants.%Animal.facet, constants.%Edible.facet) {
@@ -491,7 +494,7 @@ fn F() {
 // CHECK:STDOUT:   %require_complete.loc31_45 => constants.%complete_type.357
 // CHECK:STDOUT:   %require_complete.loc31_54 => constants.%complete_type.357
 // CHECK:STDOUT:   %Eats.type => constants.%Eats.type.1ae
-// CHECK:STDOUT:   %impl_witness => constants.%impl_witness.4f1
+// CHECK:STDOUT:   %Eats.impl_symbolic_witness => constants.%impl_witness.4f1
 // CHECK:STDOUT:   %Eats.facet.loc31_76.2 => constants.%Eats.facet.fa6
 // CHECK:STDOUT:   %Feed.specific_fn.loc31_64.2 => constants.%Feed.specific_fn.d82
 // CHECK:STDOUT: }
@@ -515,6 +518,8 @@ fn F() {
 // CHECK:STDOUT:   %Eats.type.loc25_49.2 => constants.%Eats.type.1ae
 // CHECK:STDOUT:   %require_complete => constants.%complete_type.004
 // CHECK:STDOUT:   %impl_witness => constants.%impl_witness.4f1
+// CHECK:STDOUT:
+// CHECK:STDOUT: !definition:
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @Feed(constants.%Edible.facet, constants.%Eats.facet.fa6) {

toolchain/check/testdata/function/generic/deduce.carbon

@@ -1519,17 +1519,18 @@ fn F() {
 // CHECK:STDOUT:   %CC.type: type = generic_class_type @CC [concrete]
 // CHECK:STDOUT:   %CC.generic: %CC.type = struct_value () [concrete]
 // CHECK:STDOUT:   %CC.a2f: type = class_type @CC, @CC(%D) [symbolic]
-// CHECK:STDOUT:   %Z.facet.42e: %Z.type = facet_value %DD.296, (%impl_witness.d1b) [symbolic]
-// CHECK:STDOUT:   %CC.379: type = class_type @CC, @CC(%Z.facet.42e) [symbolic]
-// CHECK:STDOUT:   %impl_witness.b93: <witness> = impl_witness (), @impl.c35(%E) [symbolic]
+// CHECK:STDOUT:   %Z.impl_symbolic_witness: <witness> = impl_symbolic_witness %DD.296, @Z [symbolic]
+// CHECK:STDOUT:   %Z.facet.f61: %Z.type = facet_value %DD.296, (%Z.impl_symbolic_witness) [symbolic]
+// CHECK:STDOUT:   %CC.43f: type = class_type @CC, @CC(%Z.facet.f61) [symbolic]
+// CHECK:STDOUT:   %impl_witness.dd1: <witness> = impl_witness (), @impl.5bc(%E) [symbolic]
 // CHECK:STDOUT:   %F.type: type = fn_type @F [concrete]
 // CHECK:STDOUT:   %F: %F.type = struct_value () [concrete]
 // CHECK:STDOUT:   %DD.689: type = class_type @DD, @DD(%EE) [concrete]
 // CHECK:STDOUT:   %impl_witness.f62: <witness> = impl_witness (), @impl.266(%EE) [concrete]
 // CHECK:STDOUT:   %Z.facet.85b: %Z.type = facet_value %DD.689, (%impl_witness.f62) [concrete]
 // CHECK:STDOUT:   %CC.4de: type = class_type @CC, @CC(%Z.facet.85b) [concrete]
-// CHECK:STDOUT:   %impl_witness.baa: <witness> = impl_witness (), @impl.c35(%EE) [concrete]
-// CHECK:STDOUT:   %Z.facet.fb6: %Z.type = facet_value %CC.4de, (%impl_witness.baa) [concrete]
+// CHECK:STDOUT:   %impl_witness.6b1: <witness> = impl_witness (), @impl.5bc(%EE) [concrete]
+// CHECK:STDOUT:   %Z.facet.a6a: %Z.type = facet_value %CC.4de, (%impl_witness.6b1) [concrete]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: imports {
@@ -1577,20 +1578,20 @@ fn F() {
 // CHECK:STDOUT:     %Z.ref: type = name_ref Z, file.%Z.decl [concrete = constants.%Z.type]
 // CHECK:STDOUT:     %D.loc11_10.1: %Z.type = bind_symbolic_name D, 0 [symbolic = %D.loc11_10.2 (constants.%D)]
 // CHECK:STDOUT:   }
-// CHECK:STDOUT:   impl_decl @impl.c35 [concrete] {
+// CHECK:STDOUT:   impl_decl @impl.5bc [concrete] {
 // CHECK:STDOUT:     %E.patt.loc12_14.1: type = symbolic_binding_pattern E, 0 [symbolic = %E.patt.loc12_14.2 (constants.%E.patt)]
 // CHECK:STDOUT:   } {
 // CHECK:STDOUT:     %CC.ref: %CC.type = name_ref CC, file.%CC.decl [concrete = constants.%CC.generic]
 // CHECK:STDOUT:     %DD.ref: %DD.type = name_ref DD, file.%DD.decl [concrete = constants.%DD.generic]
 // CHECK:STDOUT:     %E.ref: type = name_ref E, %E.loc12_14.1 [symbolic = %E.loc12_14.2 (constants.%E)]
 // CHECK:STDOUT:     %DD.loc12_31.1: type = class_type @DD, @DD(constants.%E) [symbolic = %DD.loc12_31.2 (constants.%DD.296)]
-// CHECK:STDOUT:     %Z.facet.loc12_32.1: %Z.type = facet_value constants.%DD.296, (constants.%impl_witness.d1b) [symbolic = %Z.facet.loc12_32.2 (constants.%Z.facet.42e)]
-// CHECK:STDOUT:     %.loc12: %Z.type = converted %DD.loc12_31.1, %Z.facet.loc12_32.1 [symbolic = %Z.facet.loc12_32.2 (constants.%Z.facet.42e)]
-// CHECK:STDOUT:     %CC.loc12_32.1: type = class_type @CC, @CC(constants.%Z.facet.42e) [symbolic = %CC.loc12_32.2 (constants.%CC.379)]
+// CHECK:STDOUT:     %Z.facet.loc12_32.1: %Z.type = facet_value constants.%DD.296, (constants.%Z.impl_symbolic_witness) [symbolic = %Z.facet.loc12_32.2 (constants.%Z.facet.f61)]
+// CHECK:STDOUT:     %.loc12: %Z.type = converted %DD.loc12_31.1, %Z.facet.loc12_32.1 [symbolic = %Z.facet.loc12_32.2 (constants.%Z.facet.f61)]
+// CHECK:STDOUT:     %CC.loc12_32.1: type = class_type @CC, @CC(constants.%Z.facet.f61) [symbolic = %CC.loc12_32.2 (constants.%CC.43f)]
 // CHECK:STDOUT:     %Z.ref: type = name_ref Z, file.%Z.decl [concrete = constants.%Z.type]
 // CHECK:STDOUT:     %E.loc12_14.1: type = bind_symbolic_name E, 0 [symbolic = %E.loc12_14.2 (constants.%E)]
 // CHECK:STDOUT:   }
-// CHECK:STDOUT:   %impl_witness.loc12: <witness> = impl_witness (), @impl.c35(constants.%E) [symbolic = @impl.c35.%impl_witness.loc12_39 (constants.%impl_witness.b93)]
+// CHECK:STDOUT:   %impl_witness.loc12: <witness> = impl_witness (), @impl.5bc(constants.%E) [symbolic = @impl.5bc.%impl_witness (constants.%impl_witness.dd1)]
 // CHECK:STDOUT:   %F.decl: %F.type = fn_decl @F [concrete = constants.%F] {} {}
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
@@ -1621,14 +1622,14 @@ fn F() {
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: generic impl @impl.c35(%E.loc12_14.1: type) {
+// CHECK:STDOUT: generic impl @impl.5bc(%E.loc12_14.1: type) {
 // CHECK:STDOUT:   %E.loc12_14.2: type = bind_symbolic_name E, 0 [symbolic = %E.loc12_14.2 (constants.%E)]
 // CHECK:STDOUT:   %E.patt.loc12_14.2: type = symbolic_binding_pattern E, 0 [symbolic = %E.patt.loc12_14.2 (constants.%E.patt)]
 // CHECK:STDOUT:   %DD.loc12_31.2: type = class_type @DD, @DD(%E.loc12_14.2) [symbolic = %DD.loc12_31.2 (constants.%DD.296)]
-// CHECK:STDOUT:   %impl_witness.loc12_32: <witness> = impl_witness (), @impl.266(%E.loc12_14.2) [symbolic = %impl_witness.loc12_32 (constants.%impl_witness.d1b)]
-// CHECK:STDOUT:   %Z.facet.loc12_32.2: %Z.type = facet_value %DD.loc12_31.2, (%impl_witness.loc12_32) [symbolic = %Z.facet.loc12_32.2 (constants.%Z.facet.42e)]
-// CHECK:STDOUT:   %CC.loc12_32.2: type = class_type @CC, @CC(%Z.facet.loc12_32.2) [symbolic = %CC.loc12_32.2 (constants.%CC.379)]
-// CHECK:STDOUT:   %impl_witness.loc12_39: <witness> = impl_witness (), @impl.c35(%E.loc12_14.2) [symbolic = %impl_witness.loc12_39 (constants.%impl_witness.b93)]
+// CHECK:STDOUT:   %Z.impl_symbolic_witness: <witness> = impl_symbolic_witness %DD.loc12_31.2, @Z [symbolic = %Z.impl_symbolic_witness (constants.%Z.impl_symbolic_witness)]
+// CHECK:STDOUT:   %Z.facet.loc12_32.2: %Z.type = facet_value %DD.loc12_31.2, (%Z.impl_symbolic_witness) [symbolic = %Z.facet.loc12_32.2 (constants.%Z.facet.f61)]
+// CHECK:STDOUT:   %CC.loc12_32.2: type = class_type @CC, @CC(%Z.facet.loc12_32.2) [symbolic = %CC.loc12_32.2 (constants.%CC.43f)]
+// CHECK:STDOUT:   %impl_witness: <witness> = impl_witness (), @impl.5bc(%E.loc12_14.2) [symbolic = %impl_witness (constants.%impl_witness.dd1)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT:
@@ -1686,8 +1687,8 @@ fn F() {
 // CHECK:STDOUT:   %.loc15_12: %Z.type = converted %DD, %Z.facet.loc15_12 [concrete = constants.%Z.facet.85b]
 // CHECK:STDOUT:   %CC: type = class_type @CC, @CC(constants.%Z.facet.85b) [concrete = constants.%CC.4de]
 // CHECK:STDOUT:   %Z.ref: type = name_ref Z, file.%Z.decl [concrete = constants.%Z.type]
-// CHECK:STDOUT:   %Z.facet.loc15_14: %Z.type = facet_value constants.%CC.4de, (constants.%impl_witness.baa) [concrete = constants.%Z.facet.fb6]
-// CHECK:STDOUT:   %.loc15_14: %Z.type = converted %CC, %Z.facet.loc15_14 [concrete = constants.%Z.facet.fb6]
+// CHECK:STDOUT:   %Z.facet.loc15_14: %Z.type = facet_value constants.%CC.4de, (constants.%impl_witness.6b1) [concrete = constants.%Z.facet.a6a]
+// CHECK:STDOUT:   %.loc15_14: %Z.type = converted %CC, %Z.facet.loc15_14 [concrete = constants.%Z.facet.a6a]
 // CHECK:STDOUT:   return
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
@@ -1714,28 +1715,26 @@ fn F() {
 // CHECK:STDOUT:   %D.patt.loc11_10.2 => constants.%D
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @CC(constants.%Z.facet.42e) {
-// CHECK:STDOUT:   %D.loc11_10.2 => constants.%Z.facet.42e
-// CHECK:STDOUT:   %D.patt.loc11_10.2 => constants.%Z.facet.42e
+// CHECK:STDOUT: specific @CC(constants.%Z.facet.f61) {
+// CHECK:STDOUT:   %D.loc11_10.2 => constants.%Z.facet.f61
+// CHECK:STDOUT:   %D.patt.loc11_10.2 => constants.%Z.facet.f61
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @impl.c35(constants.%E) {
+// CHECK:STDOUT: specific @impl.5bc(constants.%E) {
 // CHECK:STDOUT:   %E.loc12_14.2 => constants.%E
 // CHECK:STDOUT:   %E.patt.loc12_14.2 => constants.%E
 // CHECK:STDOUT:   %DD.loc12_31.2 => constants.%DD.296
-// CHECK:STDOUT:   %impl_witness.loc12_32 => constants.%impl_witness.d1b
-// CHECK:STDOUT:   %Z.facet.loc12_32.2 => constants.%Z.facet.42e
-// CHECK:STDOUT:   %CC.loc12_32.2 => constants.%CC.379
-// CHECK:STDOUT:   %impl_witness.loc12_39 => constants.%impl_witness.b93
+// CHECK:STDOUT:   %Z.impl_symbolic_witness => constants.%Z.impl_symbolic_witness
+// CHECK:STDOUT:   %Z.facet.loc12_32.2 => constants.%Z.facet.f61
+// CHECK:STDOUT:   %CC.loc12_32.2 => constants.%CC.43f
+// CHECK:STDOUT:   %impl_witness => constants.%impl_witness.dd1
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @DD(@impl.c35.%E.loc12_14.2) {}
+// CHECK:STDOUT: specific @DD(@impl.5bc.%E.loc12_14.2) {}
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @impl.266(@impl.c35.%E.loc12_14.2) {}
+// CHECK:STDOUT: specific @CC(@impl.5bc.%Z.facet.loc12_32.2) {}
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @CC(@impl.c35.%Z.facet.loc12_32.2) {}
-// CHECK:STDOUT:
-// CHECK:STDOUT: specific @impl.c35(%E.loc12_14.2) {}
+// CHECK:STDOUT: specific @impl.5bc(%E.loc12_14.2) {}
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @DD(constants.%EE) {
 // CHECK:STDOUT:   %E.loc8_10.2 => constants.%EE
@@ -1756,14 +1755,14 @@ fn F() {
 // CHECK:STDOUT:   %D.patt.loc11_10.2 => constants.%Z.facet.85b
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @impl.c35(constants.%EE) {
+// CHECK:STDOUT: specific @impl.5bc(constants.%EE) {
 // CHECK:STDOUT:   %E.loc12_14.2 => constants.%EE
 // CHECK:STDOUT:   %E.patt.loc12_14.2 => constants.%EE
 // CHECK:STDOUT:   %DD.loc12_31.2 => constants.%DD.689
-// CHECK:STDOUT:   %impl_witness.loc12_32 => constants.%impl_witness.f62
+// CHECK:STDOUT:   %Z.impl_symbolic_witness => constants.%impl_witness.f62
 // CHECK:STDOUT:   %Z.facet.loc12_32.2 => constants.%Z.facet.85b
 // CHECK:STDOUT:   %CC.loc12_32.2 => constants.%CC.4de
-// CHECK:STDOUT:   %impl_witness.loc12_39 => constants.%impl_witness.baa
+// CHECK:STDOUT:   %impl_witness => constants.%impl_witness.6b1
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT: }

toolchain/check/testdata/impl/lookup/min_prelude/specialization.carbon

@@ -217,7 +217,7 @@ fn F() {
   let a: C(D(E), D(E)).(Z.X) = {} as C(E, E);
 }
 
-// --- specialized_class_with_symbolic_facet_value_param.carbon
+// --- fail_specialized_class_with_symbolic_facet_value_param.carbon
 
 interface Z {
   let X:! type;
@@ -239,10 +239,13 @@ fn F[D:! Y](d: D) {
   // The FacetValue deduced for the param of `C` will be a symbolic FacetValue
   // because we are in a generic where `D` is an unknown type, which will cause
   // the query and impl self type to be C(FacetValue) for a symbolic FacetValue.
-  //
-  // TODO: The type of `.X` should actually be symbolic here, unless the impl is
-  // effectively final (since the lookup query uses a symbolic `D` in its
-  // input). But we don't have support for either of those yet.
+  // CHECK:STDERR: fail_specialized_class_with_symbolic_facet_value_param.carbon:[[@LINE+7]]:23: error: cannot implicitly convert value of type `()` to `<symbolic>` [ConversionFailure]
+  // CHECK:STDERR:   let a: C(D).(Z.X) = ();
+  // CHECK:STDERR:                       ^~
+  // CHECK:STDERR: fail_specialized_class_with_symbolic_facet_value_param.carbon:[[@LINE+4]]:23: note: type `()` does not implement interface `Core.ImplicitAs(<symbolic>)` [MissingImplInMemberAccessNote]
+  // CHECK:STDERR:   let a: C(D).(Z.X) = ();
+  // CHECK:STDERR:                       ^~
+  // CHECK:STDERR:
   let a: C(D).(Z.X) = ();
 }
 
@@ -379,21 +382,25 @@ fn F[U:! type](T:! Z(C)) {
 // TODO: Make this `final`.
 impl forall [T:! type] T as Z(C) where .X = C {}
 
-// --- fail_specialization_written_after_generic_use.carbon
+// --- specialization_written_after_generic_use.carbon
 library "[[@TEST_NAME]]";
 
 interface Z {
   let V:! type;
-  fn F() -> V;
+  fn ZZ() -> V;
 }
 
 interface Y {}
 impl forall [T:! Y] T as Z where .V = () {
-  fn F() -> () { return (); }
+  fn ZZ() -> () { return (); }
+}
+
+fn H(W:! Z, X: W.(Z.V)) -> W.(Z.V) {
+  return X;
 }
 
 fn G(U:! Y) -> U.(Z.V) {
-  return U.(Z.F)();
+  return H(U, U.(Z.ZZ)());
 }
 
 class C {
@@ -401,16 +408,42 @@ class C {
 }
 
 impl C as Z where .V = {} {
-  fn F() -> {} { return {}; }
+  fn ZZ() -> {} { return {}; }
 }
 
-fn H() {
-  // CHECK:STDERR: fail_specialization_written_after_generic_use.carbon:[[@LINE+7]]:15: error: cannot implicitly convert value of type `()` to `{}` [ConversionFailure]
-  // CHECK:STDERR:   let x: {} = G(C);
-  // CHECK:STDERR:               ^~~~
-  // CHECK:STDERR: fail_specialization_written_after_generic_use.carbon:[[@LINE+4]]:15: note: type `()` does not implement interface `Core.ImplicitAs({})` [MissingImplInMemberAccessNote]
-  // CHECK:STDERR:   let x: {} = G(C);
-  // CHECK:STDERR:               ^~~~
-  // CHECK:STDERR:
+fn F() {
+  let x: {} = G(C);
+}
+
+// --- specialization_written_after_generic_use_with_generic_interface.carbon
+library "[[@TEST_NAME]]";
+
+interface Z(T:! type) {
+  let V:! type;
+  fn ZZ() -> V;
+}
+
+interface Y {}
+impl forall [T:! Y] T as Z(T) where .V = () {
+  fn ZZ() -> () { return (); }
+}
+
+fn H(U:! Y, W:! Y & Z(U), X: W.(Z(U).V)) -> W.(Z(U).V) {
+  return X;
+}
+
+fn G(U:! Y) -> U.(Z(U).V) {
+  return H(U, U, U.(Z(U).ZZ)());
+}
+
+class C {
+  impl as Y {}
+}
+
+impl C as Z(C) where .V = {} {
+  fn ZZ() -> {} { return {}; }
+}
+
+fn F() {
   let x: {} = G(C);
 }

toolchain/check/testdata/impl/lookup/no_prelude/impl_forall.carbon

@@ -69,7 +69,7 @@ fn TestSpecific(a: A({})) -> {} {
 // CHECK:STDOUT:   %impl_witness.ab3b51.1: <witness> = impl_witness (@impl.%F.decl), @impl(%V) [symbolic]
 // CHECK:STDOUT:   %F.type.0fea45.1: type = fn_type @F.2, @impl(%V) [symbolic]
 // CHECK:STDOUT:   %F.d6ae34.1: %F.type.0fea45.1 = struct_value () [symbolic]
-// CHECK:STDOUT:   %I.facet.1299b2.1: %I.type.325e65.2 = facet_value %A.13025a.2, (%impl_witness.ab3b51.1) [symbolic]
+// CHECK:STDOUT:   %I.facet.129: %I.type.325e65.2 = facet_value %A.13025a.2, (%impl_witness.ab3b51.1) [symbolic]
 // CHECK:STDOUT:   %require_complete.4aeca8.2: <witness> = require_complete_type %V [symbolic]
 // CHECK:STDOUT:   %A.elem.1ceb36.2: type = unbound_element_type %A.13025a.2, %V [symbolic]
 // CHECK:STDOUT:   %struct_type.n.848971.2: type = struct_type {.n: %V} [symbolic]
@@ -95,9 +95,11 @@ fn TestSpecific(a: A({})) -> {} {
 // CHECK:STDOUT:   %impl_witness.ab3b51.2: <witness> = impl_witness (@impl.%F.decl), @impl(%W) [symbolic]
 // CHECK:STDOUT:   %F.type.0fea45.2: type = fn_type @F.2, @impl(%W) [symbolic]
 // CHECK:STDOUT:   %F.d6ae34.2: %F.type.0fea45.2 = struct_value () [symbolic]
-// CHECK:STDOUT:   %I.facet.1299b2.2: %I.type.325e65.3 = facet_value %A.13025a.3, (%impl_witness.ab3b51.2) [symbolic]
-// CHECK:STDOUT:   %.814: type = fn_type_with_self_type %F.type.2aef59.3, %I.facet.1299b2.2 [symbolic]
-// CHECK:STDOUT:   %F.specific_fn.e98: <specific function> = specific_function %F.d6ae34.2, @F.2(%W) [symbolic]
+// CHECK:STDOUT:   %I.impl_symbolic_witness: <witness> = impl_symbolic_witness %A.13025a.3, @I, @I(%W) [symbolic]
+// CHECK:STDOUT:   %I.facet.5fd: %I.type.325e65.3 = facet_value %A.13025a.3, (%I.impl_symbolic_witness) [symbolic]
+// CHECK:STDOUT:   %.ea0: type = fn_type_with_self_type %F.type.2aef59.3, %I.facet.5fd [symbolic]
+// CHECK:STDOUT:   %impl.elem0: %.ea0 = impl_witness_access %I.impl_symbolic_witness, element0 [symbolic]
+// CHECK:STDOUT:   %specific_impl_fn: <specific function> = specific_impl_function %impl.elem0, @F.1(%W, %I.facet.5fd) [symbolic]
 // CHECK:STDOUT:   %empty_struct_type: type = struct_type {} [concrete]
 // CHECK:STDOUT:   %A.235: type = class_type @A, @A(%empty_struct_type) [concrete]
 // CHECK:STDOUT:   %TestSpecific.type: type = fn_type @TestSpecific [concrete]
@@ -118,7 +120,7 @@ fn TestSpecific(a: A({})) -> {} {
 // CHECK:STDOUT:   %F.158: %F.type.875 = struct_value () [concrete]
 // CHECK:STDOUT:   %I.facet.b64: %I.type.885 = facet_value %A.235, (%impl_witness.f35) [concrete]
 // CHECK:STDOUT:   %.f80: type = fn_type_with_self_type %F.type.684, %I.facet.b64 [concrete]
-// CHECK:STDOUT:   %F.specific_fn.72f: <specific function> = specific_function %F.158, @F.2(%empty_struct_type) [concrete]
+// CHECK:STDOUT:   %F.specific_fn: <specific function> = specific_function %F.158, @F.2(%empty_struct_type) [concrete]
 // CHECK:STDOUT:   %empty_struct: %empty_struct_type = struct_value () [concrete]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
@@ -334,13 +336,12 @@ fn TestSpecific(a: A({})) -> {} {
 // CHECK:STDOUT:   %require_complete.loc18: <witness> = require_complete_type @TestGeneric.%I.type.loc18_16.2 (%I.type.325e65.3) [symbolic = %require_complete.loc18 (constants.%require_complete.cfebb2.2)]
 // CHECK:STDOUT:   %I.assoc_type: type = assoc_entity_type @TestGeneric.%I.type.loc18_16.2 (%I.type.325e65.3) [symbolic = %I.assoc_type (constants.%I.assoc_type.955255.3)]
 // CHECK:STDOUT:   %assoc0: @TestGeneric.%I.assoc_type (%I.assoc_type.955255.3) = assoc_entity element0, @I.%F.decl [symbolic = %assoc0 (constants.%assoc0.fef501.3)]
-// CHECK:STDOUT:   %F.type.loc18_11.1: type = fn_type @F.1, @I(%W.loc17_16.2) [symbolic = %F.type.loc18_11.1 (constants.%F.type.2aef59.3)]
-// CHECK:STDOUT:   %impl_witness: <witness> = impl_witness (@impl.%F.decl), @impl(%W.loc17_16.2) [symbolic = %impl_witness (constants.%impl_witness.ab3b51.2)]
-// CHECK:STDOUT:   %I.facet: @TestGeneric.%I.type.loc18_16.2 (%I.type.325e65.3) = facet_value %A.loc17_32.2, (%impl_witness) [symbolic = %I.facet (constants.%I.facet.1299b2.2)]
-// CHECK:STDOUT:   %.loc18_11: type = fn_type_with_self_type %F.type.loc18_11.1, %I.facet [symbolic = %.loc18_11 (constants.%.814)]
-// CHECK:STDOUT:   %F.type.loc18_11.2: type = fn_type @F.2, @impl(%W.loc17_16.2) [symbolic = %F.type.loc18_11.2 (constants.%F.type.0fea45.2)]
-// CHECK:STDOUT:   %F: @TestGeneric.%F.type.loc18_11.2 (%F.type.0fea45.2) = struct_value () [symbolic = %F (constants.%F.d6ae34.2)]
-// CHECK:STDOUT:   %F.specific_fn: <specific function> = specific_function %F, @F.2(%W.loc17_16.2) [symbolic = %F.specific_fn (constants.%F.specific_fn.e98)]
+// CHECK:STDOUT:   %F.type: type = fn_type @F.1, @I(%W.loc17_16.2) [symbolic = %F.type (constants.%F.type.2aef59.3)]
+// CHECK:STDOUT:   %I.impl_symbolic_witness: <witness> = impl_symbolic_witness %A.loc17_32.2, @I, @I(%W.loc17_16.2) [symbolic = %I.impl_symbolic_witness (constants.%I.impl_symbolic_witness)]
+// CHECK:STDOUT:   %I.facet: @TestGeneric.%I.type.loc18_16.2 (%I.type.325e65.3) = facet_value %A.loc17_32.2, (%I.impl_symbolic_witness) [symbolic = %I.facet (constants.%I.facet.5fd)]
+// CHECK:STDOUT:   %.loc18_11: type = fn_type_with_self_type %F.type, %I.facet [symbolic = %.loc18_11 (constants.%.ea0)]
+// CHECK:STDOUT:   %impl.elem0.loc18_11.2: @TestGeneric.%.loc18_11 (%.ea0) = impl_witness_access %I.impl_symbolic_witness, element0 [symbolic = %impl.elem0.loc18_11.2 (constants.%impl.elem0)]
+// CHECK:STDOUT:   %specific_impl_fn.loc18_11.2: <specific function> = specific_impl_function %impl.elem0.loc18_11.2, @F.1(%W.loc17_16.2, %I.facet) [symbolic = %specific_impl_fn.loc18_11.2 (constants.%specific_impl_fn)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   fn[%W.patt.loc17_16.1: type](%a.param_patt: @TestGeneric.%A.loc17_32.2 (%A.13025a.3)) -> @TestGeneric.%W.loc17_16.2 (%W) {
 // CHECK:STDOUT:   !entry:
@@ -350,13 +351,13 @@ fn TestSpecific(a: A({})) -> {} {
 // CHECK:STDOUT:     %I.type.loc18_16.1: type = facet_type <@I, @I(constants.%W)> [symbolic = %I.type.loc18_16.2 (constants.%I.type.325e65.3)]
 // CHECK:STDOUT:     %.loc18_17: @TestGeneric.%I.assoc_type (%I.assoc_type.955255.3) = specific_constant @I.%assoc0.loc8_26.1, @I(constants.%W) [symbolic = %assoc0 (constants.%assoc0.fef501.3)]
 // CHECK:STDOUT:     %F.ref: @TestGeneric.%I.assoc_type (%I.assoc_type.955255.3) = name_ref F, %.loc18_17 [symbolic = %assoc0 (constants.%assoc0.fef501.3)]
-// CHECK:STDOUT:     %impl.elem0: @TestGeneric.%.loc18_11 (%.814) = impl_witness_access constants.%impl_witness.ab3b51.2, element0 [symbolic = %F (constants.%F.d6ae34.2)]
-// CHECK:STDOUT:     %bound_method.loc18_11: <bound method> = bound_method %a.ref, %impl.elem0
-// CHECK:STDOUT:     %specific_fn: <specific function> = specific_function %impl.elem0, @F.2(constants.%W) [symbolic = %F.specific_fn (constants.%F.specific_fn.e98)]
-// CHECK:STDOUT:     %bound_method.loc18_21: <bound method> = bound_method %a.ref, %specific_fn
-// CHECK:STDOUT:     %F.call: init @TestGeneric.%W.loc17_16.2 (%W) = call %bound_method.loc18_21(%a.ref)
-// CHECK:STDOUT:     %.loc18_22.1: @TestGeneric.%W.loc17_16.2 (%W) = value_of_initializer %F.call
-// CHECK:STDOUT:     %.loc18_22.2: @TestGeneric.%W.loc17_16.2 (%W) = converted %F.call, %.loc18_22.1
+// CHECK:STDOUT:     %impl.elem0.loc18_11.1: @TestGeneric.%.loc18_11 (%.ea0) = impl_witness_access constants.%I.impl_symbolic_witness, element0 [symbolic = %impl.elem0.loc18_11.2 (constants.%impl.elem0)]
+// CHECK:STDOUT:     %bound_method.loc18_11: <bound method> = bound_method %a.ref, %impl.elem0.loc18_11.1
+// CHECK:STDOUT:     %specific_impl_fn.loc18_11.1: <specific function> = specific_impl_function %impl.elem0.loc18_11.1, @F.1(constants.%W, constants.%I.facet.5fd) [symbolic = %specific_impl_fn.loc18_11.2 (constants.%specific_impl_fn)]
+// CHECK:STDOUT:     %bound_method.loc18_21: <bound method> = bound_method %a.ref, %specific_impl_fn.loc18_11.1
+// CHECK:STDOUT:     %.loc18_21: init @TestGeneric.%W.loc17_16.2 (%W) = call %bound_method.loc18_21(%a.ref)
+// CHECK:STDOUT:     %.loc18_22.1: @TestGeneric.%W.loc17_16.2 (%W) = value_of_initializer %.loc18_21
+// CHECK:STDOUT:     %.loc18_22.2: @TestGeneric.%W.loc17_16.2 (%W) = converted %.loc18_21, %.loc18_22.1
 // CHECK:STDOUT:     return %.loc18_22.2
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
@@ -372,7 +373,7 @@ fn TestSpecific(a: A({})) -> {} {
 // CHECK:STDOUT:   %F.ref: %I.assoc_type.67f = name_ref F, %.loc22_18 [concrete = constants.%assoc0.639]
 // CHECK:STDOUT:   %impl.elem0: %.f80 = impl_witness_access constants.%impl_witness.f35, element0 [concrete = constants.%F.158]
 // CHECK:STDOUT:   %bound_method.loc22_11: <bound method> = bound_method %a.ref, %impl.elem0
-// CHECK:STDOUT:   %specific_fn: <specific function> = specific_function %impl.elem0, @F.2(constants.%empty_struct_type) [concrete = constants.%F.specific_fn.72f]
+// CHECK:STDOUT:   %specific_fn: <specific function> = specific_function %impl.elem0, @F.2(constants.%empty_struct_type) [concrete = constants.%F.specific_fn]
 // CHECK:STDOUT:   %bound_method.loc22_22: <bound method> = bound_method %a.ref, %specific_fn
 // CHECK:STDOUT:   %F.call: init %empty_struct_type = call %bound_method.loc22_22(%a.ref)
 // CHECK:STDOUT:   %.loc22_22.1: ref %empty_struct_type = temporary_storage
@@ -456,10 +457,10 @@ fn TestSpecific(a: A({})) -> {} {
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @A(@F.2.%V) {}
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @F.1(constants.%V, constants.%I.facet.1299b2.1) {
+// CHECK:STDOUT: specific @F.1(constants.%V, constants.%I.facet.129) {
 // CHECK:STDOUT:   %U => constants.%V
 // CHECK:STDOUT:   %I.type => constants.%I.type.325e65.2
-// CHECK:STDOUT:   %Self => constants.%I.facet.1299b2.1
+// CHECK:STDOUT:   %Self => constants.%I.facet.129
 // CHECK:STDOUT:   %Self.as_type.loc8_14.1 => constants.%A.13025a.2
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
@@ -509,21 +510,16 @@ fn TestSpecific(a: A({})) -> {} {
 // CHECK:STDOUT:   %F => constants.%F.d6ae34.2
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @F.2(constants.%W) {
-// CHECK:STDOUT:   %V => constants.%W
-// CHECK:STDOUT:   %A => constants.%A.13025a.3
-// CHECK:STDOUT:
-// CHECK:STDOUT: !definition:
-// CHECK:STDOUT:   %require_complete.loc12_22 => constants.%require_complete.4aeca8.3
-// CHECK:STDOUT:   %require_complete.loc12_12 => constants.%require_complete.5b8aee.2
-// CHECK:STDOUT:   %A.elem => constants.%A.elem.1ceb36.3
+// CHECK:STDOUT: specific @F.1(constants.%W, constants.%I.facet.5fd) {
+// CHECK:STDOUT:   %U => constants.%W
+// CHECK:STDOUT:   %I.type => constants.%I.type.325e65.3
+// CHECK:STDOUT:   %Self => constants.%I.facet.5fd
+// CHECK:STDOUT:   %Self.as_type.loc8_14.1 => constants.%A.13025a.3
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @I(@TestGeneric.%W.loc17_16.2) {}
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @impl(@TestGeneric.%W.loc17_16.2) {}
-// CHECK:STDOUT:
-// CHECK:STDOUT: specific @F.2(@TestGeneric.%W.loc17_16.2) {}
+// CHECK:STDOUT: specific @F.1(@TestGeneric.%W.loc17_16.2, @TestGeneric.%I.facet) {}
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @A(constants.%empty_struct_type) {
 // CHECK:STDOUT:   %T.loc3_9.2 => constants.%empty_struct_type

toolchain/check/testdata/impl/no_prelude/import_builtin_call.carbon

@@ -102,11 +102,14 @@ var n: Int(64) = MakeFromClass(FromLiteral(64) as OtherInt);
 // CHECK:STDOUT:   %Op.type.883: type = fn_type @Op.2, @impl(%N) [symbolic]
 // CHECK:STDOUT:   %Op.8bc: %Op.type.883 = struct_value () [symbolic]
 // CHECK:STDOUT:   %require_complete.fc7: <witness> = require_complete_type %MyInt [symbolic]
-// CHECK:STDOUT:   %Add.facet: %Add.type = facet_value %MyInt, (%impl_witness) [symbolic]
+// CHECK:STDOUT:   %Add.facet.c2b: %Add.type = facet_value %MyInt, (%impl_witness) [symbolic]
 // CHECK:STDOUT:   %Double.type: type = fn_type @Double [concrete]
 // CHECK:STDOUT:   %Double: %Double.type = struct_value () [concrete]
-// CHECK:STDOUT:   %.9b8: type = fn_type_with_self_type %Op.type.31b, %Add.facet [symbolic]
-// CHECK:STDOUT:   %Op.specific_fn: <specific function> = specific_function %Op.8bc, @Op.2(%N) [symbolic]
+// CHECK:STDOUT:   %Add.impl_symbolic_witness: <witness> = impl_symbolic_witness %MyInt, @Add [symbolic]
+// CHECK:STDOUT:   %Add.facet.f76: %Add.type = facet_value %MyInt, (%Add.impl_symbolic_witness) [symbolic]
+// CHECK:STDOUT:   %.dfa: type = fn_type_with_self_type %Op.type.31b, %Add.facet.f76 [symbolic]
+// CHECK:STDOUT:   %impl.elem0: %.dfa = impl_witness_access %Add.impl_symbolic_witness, element0 [symbolic]
+// CHECK:STDOUT:   %specific_impl_fn: <specific function> = specific_impl_function %impl.elem0, @Op.1(%Add.facet.f76) [symbolic]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
@@ -326,26 +329,29 @@ var n: Int(64) = MakeFromClass(FromLiteral(64) as OtherInt);
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT:   %require_complete: <witness> = require_complete_type @Double.%MyInt.loc19_39.2 (%MyInt) [symbolic = %require_complete (constants.%require_complete.fc7)]
-// CHECK:STDOUT:   %impl_witness: <witness> = impl_witness (@impl.%Op.decl), @impl(%N.loc19_11.2) [symbolic = %impl_witness (constants.%impl_witness)]
-// CHECK:STDOUT:   %Add.facet: %Add.type = facet_value %MyInt.loc19_39.2, (%impl_witness) [symbolic = %Add.facet (constants.%Add.facet)]
-// CHECK:STDOUT:   %.loc20_11: type = fn_type_with_self_type constants.%Op.type.31b, %Add.facet [symbolic = %.loc20_11 (constants.%.9b8)]
-// CHECK:STDOUT:   %Op.type: type = fn_type @Op.2, @impl(%N.loc19_11.2) [symbolic = %Op.type (constants.%Op.type.883)]
-// CHECK:STDOUT:   %Op: @Double.%Op.type (%Op.type.883) = struct_value () [symbolic = %Op (constants.%Op.8bc)]
-// CHECK:STDOUT:   %Op.specific_fn: <specific function> = specific_function %Op, @Op.2(%N.loc19_11.2) [symbolic = %Op.specific_fn (constants.%Op.specific_fn)]
+// CHECK:STDOUT:   %Add.impl_symbolic_witness: <witness> = impl_symbolic_witness %MyInt.loc19_39.2, @Add [symbolic = %Add.impl_symbolic_witness (constants.%Add.impl_symbolic_witness)]
+// CHECK:STDOUT:   %Add.facet.loc20_11: %Add.type = facet_value %MyInt.loc19_39.2, (%Add.impl_symbolic_witness) [symbolic = %Add.facet.loc20_11 (constants.%Add.facet.f76)]
+// CHECK:STDOUT:   %.loc20_11: type = fn_type_with_self_type constants.%Op.type.31b, %Add.facet.loc20_11 [symbolic = %.loc20_11 (constants.%.dfa)]
+// CHECK:STDOUT:   %impl.elem0.loc20_11.2: @Double.%.loc20_11 (%.dfa) = impl_witness_access %Add.impl_symbolic_witness, element0 [symbolic = %impl.elem0.loc20_11.2 (constants.%impl.elem0)]
+// CHECK:STDOUT:   %specific_impl_fn.loc20_11.2: <specific function> = specific_impl_function %impl.elem0.loc20_11.2, @Op.1(%Add.facet.loc20_11) [symbolic = %specific_impl_fn.loc20_11.2 (constants.%specific_impl_fn)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   fn[%N.patt.loc19_11.1: Core.IntLiteral](%x.param_patt: @Double.%MyInt.loc19_39.2 (%MyInt)) -> @Double.%MyInt.loc19_39.2 (%MyInt) {
 // CHECK:STDOUT:   !entry:
 // CHECK:STDOUT:     %x.ref.loc20_10: @Double.%MyInt.loc19_39.2 (%MyInt) = name_ref x, %x
 // CHECK:STDOUT:     %Add.ref: type = name_ref Add, file.%Add.decl [concrete = constants.%Add.type]
 // CHECK:STDOUT:     %Op.ref: %Add.assoc_type = name_ref Op, @Add.%assoc0 [concrete = constants.%assoc0]
-// CHECK:STDOUT:     %impl.elem0: @Double.%.loc20_11 (%.9b8) = impl_witness_access constants.%impl_witness, element0 [symbolic = %Op (constants.%Op.8bc)]
-// CHECK:STDOUT:     %bound_method.loc20_11: <bound method> = bound_method %x.ref.loc20_10, %impl.elem0
+// CHECK:STDOUT:     %impl.elem0.loc20_11.1: @Double.%.loc20_11 (%.dfa) = impl_witness_access constants.%Add.impl_symbolic_witness, element0 [symbolic = %impl.elem0.loc20_11.2 (constants.%impl.elem0)]
+// CHECK:STDOUT:     %bound_method.loc20_11: <bound method> = bound_method %x.ref.loc20_10, %impl.elem0.loc20_11.1
 // CHECK:STDOUT:     %x.ref.loc20_21: @Double.%MyInt.loc19_39.2 (%MyInt) = name_ref x, %x
-// CHECK:STDOUT:     %specific_fn: <specific function> = specific_function %impl.elem0, @Op.2(constants.%N) [symbolic = %Op.specific_fn (constants.%Op.specific_fn)]
-// CHECK:STDOUT:     %bound_method.loc20_22: <bound method> = bound_method %x.ref.loc20_10, %specific_fn
-// CHECK:STDOUT:     %int.sadd: init @Double.%MyInt.loc19_39.2 (%MyInt) = call %bound_method.loc20_22(%x.ref.loc20_10, %x.ref.loc20_21)
-// CHECK:STDOUT:     %.loc20_23.1: @Double.%MyInt.loc19_39.2 (%MyInt) = value_of_initializer %int.sadd
-// CHECK:STDOUT:     %.loc20_23.2: @Double.%MyInt.loc19_39.2 (%MyInt) = converted %int.sadd, %.loc20_23.1
+// CHECK:STDOUT:     %Add.facet.loc20_22.1: %Add.type = facet_value constants.%MyInt, (constants.%Add.impl_symbolic_witness) [symbolic = %Add.facet.loc20_11 (constants.%Add.facet.f76)]
+// CHECK:STDOUT:     %.loc20_22.1: %Add.type = converted constants.%MyInt, %Add.facet.loc20_22.1 [symbolic = %Add.facet.loc20_11 (constants.%Add.facet.f76)]
+// CHECK:STDOUT:     %Add.facet.loc20_22.2: %Add.type = facet_value constants.%MyInt, (constants.%Add.impl_symbolic_witness) [symbolic = %Add.facet.loc20_11 (constants.%Add.facet.f76)]
+// CHECK:STDOUT:     %.loc20_22.2: %Add.type = converted constants.%MyInt, %Add.facet.loc20_22.2 [symbolic = %Add.facet.loc20_11 (constants.%Add.facet.f76)]
+// CHECK:STDOUT:     %specific_impl_fn.loc20_11.1: <specific function> = specific_impl_function %impl.elem0.loc20_11.1, @Op.1(constants.%Add.facet.f76) [symbolic = %specific_impl_fn.loc20_11.2 (constants.%specific_impl_fn)]
+// CHECK:STDOUT:     %bound_method.loc20_22: <bound method> = bound_method %x.ref.loc20_10, %specific_impl_fn.loc20_11.1
+// CHECK:STDOUT:     %.loc20_22.3: init @Double.%MyInt.loc19_39.2 (%MyInt) = call %bound_method.loc20_22(%x.ref.loc20_10, %x.ref.loc20_21)
+// CHECK:STDOUT:     %.loc20_23.1: @Double.%MyInt.loc19_39.2 (%MyInt) = value_of_initializer %.loc20_22.3
+// CHECK:STDOUT:     %.loc20_23.2: @Double.%MyInt.loc19_39.2 (%MyInt) = converted %.loc20_22.3, %.loc20_23.1
 // CHECK:STDOUT:     return %.loc20_23.2
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
@@ -384,14 +390,12 @@ var n: Int(64) = MakeFromClass(FromLiteral(64) as OtherInt);
 // CHECK:STDOUT: specific @Op.2(constants.%N) {
 // CHECK:STDOUT:   %N => constants.%N
 // CHECK:STDOUT:   %MyInt => constants.%MyInt
-// CHECK:STDOUT:
-// CHECK:STDOUT: !definition:
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @MyInt(@Op.2.%N) {}
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @Op.1(constants.%Add.facet) {
-// CHECK:STDOUT:   %Self => constants.%Add.facet
+// CHECK:STDOUT: specific @Op.1(constants.%Add.facet.c2b) {
+// CHECK:STDOUT:   %Self => constants.%Add.facet.c2b
 // CHECK:STDOUT:   %Self.as_type.loc5_15.1 => constants.%MyInt
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
@@ -403,9 +407,12 @@ var n: Int(64) = MakeFromClass(FromLiteral(64) as OtherInt);
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @MyInt(@Double.%N.loc19_11.2) {}
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @impl(@Double.%N.loc19_11.2) {}
+// CHECK:STDOUT: specific @Op.1(constants.%Add.facet.f76) {
+// CHECK:STDOUT:   %Self => constants.%Add.facet.f76
+// CHECK:STDOUT:   %Self.as_type.loc5_15.1 => constants.%MyInt
+// CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @Op.2(@Double.%N.loc19_11.2) {}
+// CHECK:STDOUT: specific @Op.1(@Double.%Add.facet.loc20_11) {}
 // CHECK:STDOUT:
 // CHECK:STDOUT: --- use_generic_impl.carbon
 // CHECK:STDOUT:
@@ -435,24 +442,22 @@ var n: Int(64) = MakeFromClass(FromLiteral(64) as OtherInt);
 // CHECK:STDOUT:   %Op.8bc: %Op.type.883 = struct_value () [symbolic]
 // CHECK:STDOUT:   %require_complete.fc7: <witness> = require_complete_type %MyInt.09f [symbolic]
 // CHECK:STDOUT:   %impl_witness.8d6: <witness> = impl_witness (imports.%Main.import_ref.19b), @impl(%int_64) [concrete]
-// CHECK:STDOUT:   %impl_witness.7e5be3.1: <witness> = impl_witness (imports.%Main.import_ref.464c51.1), @impl(%N) [symbolic]
+// CHECK:STDOUT:   %impl_witness.7e5: <witness> = impl_witness (imports.%Main.import_ref.464), @impl(%N) [symbolic]
 // CHECK:STDOUT:   %Op.type.5a6: type = fn_type @Op.2, @impl(%int_64) [concrete]
 // CHECK:STDOUT:   %Op.cf9: %Op.type.5a6 = struct_value () [concrete]
 // CHECK:STDOUT:   %Add.facet.8db: %Add.type = facet_value %MyInt.f30, (%impl_witness.8d6) [concrete]
 // CHECK:STDOUT:   %.1ca: type = fn_type_with_self_type %Op.type.31b, %Add.facet.8db [concrete]
-// CHECK:STDOUT:   %Op.specific_fn.16a: <specific function> = specific_function %Op.cf9, @Op.2(%int_64) [concrete]
+// CHECK:STDOUT:   %Op.specific_fn: <specific function> = specific_function %Op.cf9, @Op.2(%int_64) [concrete]
 // CHECK:STDOUT:   %CallImportedDouble.type: type = fn_type @CallImportedDouble [concrete]
 // CHECK:STDOUT:   %CallImportedDouble: %CallImportedDouble.type = struct_value () [concrete]
 // CHECK:STDOUT:   %Double.type: type = fn_type @Double [concrete]
 // CHECK:STDOUT:   %Double: %Double.type = struct_value () [concrete]
-// CHECK:STDOUT:   %impl_witness.7e5be3.2: <witness> = impl_witness (imports.%Main.import_ref.464c51.2), @impl(%N) [symbolic]
-// CHECK:STDOUT:   %Add.facet.afa: %Add.type = facet_value %MyInt.09f, (%impl_witness.7e5be3.2) [symbolic]
-// CHECK:STDOUT:   %.207: type = fn_type_with_self_type %Op.type.31b, %Add.facet.afa [symbolic]
-// CHECK:STDOUT:   %Op.specific_fn.6c0: <specific function> = specific_function %Op.8bc, @Op.2(%N) [symbolic]
+// CHECK:STDOUT:   %Add.impl_symbolic_witness: <witness> = impl_symbolic_witness %MyInt.09f, @Add [symbolic]
+// CHECK:STDOUT:   %Add.facet.f76: %Add.type = facet_value %MyInt.09f, (%Add.impl_symbolic_witness) [symbolic]
+// CHECK:STDOUT:   %.dfa: type = fn_type_with_self_type %Op.type.31b, %Add.facet.f76 [symbolic]
+// CHECK:STDOUT:   %impl.elem0: %.dfa = impl_witness_access %Add.impl_symbolic_witness, element0 [symbolic]
+// CHECK:STDOUT:   %specific_impl_fn: <specific function> = specific_impl_function %impl.elem0, @Op.1(%Add.facet.f76) [symbolic]
 // CHECK:STDOUT:   %Double.specific_fn: <specific function> = specific_function %Double, @Double(%int_64) [concrete]
-// CHECK:STDOUT:   %impl_witness.bb3: <witness> = impl_witness (imports.%Main.import_ref.464c51.2), @impl(%int_64) [concrete]
-// CHECK:STDOUT:   %Add.facet.287: %Add.type = facet_value %MyInt.f30, (%impl_witness.bb3) [concrete]
-// CHECK:STDOUT:   %.fc5: type = fn_type_with_self_type %Op.type.31b, %Add.facet.287 [concrete]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: imports {
@@ -468,14 +473,13 @@ var n: Int(64) = MakeFromClass(FromLiteral(64) as OtherInt);
 // CHECK:STDOUT:   %Main.import_ref.db7: %Add.assoc_type = import_ref Main//generic_impl, loc5_41, loaded [concrete = constants.%assoc0]
 // CHECK:STDOUT:   %Main.Op = import_ref Main//generic_impl, Op, unloaded
 // CHECK:STDOUT:   %Main.import_ref.e5e: %Add.type = import_ref Main//generic_impl, inst16 [no loc], loaded [symbolic = constants.%Self]
-// CHECK:STDOUT:   %Main.import_ref.33b: <witness> = import_ref Main//generic_impl, loc15_48, loaded [symbolic = @impl.%impl_witness (constants.%impl_witness.7e5be3.1)]
+// CHECK:STDOUT:   %Main.import_ref.33b: <witness> = import_ref Main//generic_impl, loc15_48, loaded [symbolic = @impl.%impl_witness (constants.%impl_witness.7e5)]
 // CHECK:STDOUT:   %Main.import_ref.f1e294.2: Core.IntLiteral = import_ref Main//generic_impl, loc15_14, loaded [symbolic = @impl.%N (constants.%N)]
 // CHECK:STDOUT:   %Main.import_ref.719: type = import_ref Main//generic_impl, loc15_39, loaded [symbolic = @impl.%MyInt (constants.%MyInt.09f)]
 // CHECK:STDOUT:   %Main.import_ref.bf0: type = import_ref Main//generic_impl, loc15_44, loaded [concrete = constants.%Add.type]
 // CHECK:STDOUT:   %Main.import_ref.19b: @impl.%Op.type (%Op.type.883) = import_ref Main//generic_impl, loc16_42, loaded [symbolic = @impl.%Op (constants.%Op.8bc)]
 // CHECK:STDOUT:   %Main.import_ref.f1e294.3: Core.IntLiteral = import_ref Main//generic_impl, loc15_14, loaded [symbolic = @impl.%N (constants.%N)]
 // CHECK:STDOUT:   %Main.import_ref.f1e294.4: Core.IntLiteral = import_ref Main//generic_impl, loc19_11, loaded [symbolic = @Double.%N (constants.%N)]
-// CHECK:STDOUT:   %Main.import_ref.464c51.2 = import_ref Main//generic_impl, loc16_42, unloaded
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
@@ -578,7 +582,7 @@ var n: Int(64) = MakeFromClass(FromLiteral(64) as OtherInt);
 // CHECK:STDOUT:   %impl.elem0: %.1ca = impl_witness_access constants.%impl_witness.8d6, element0 [concrete = constants.%Op.cf9]
 // CHECK:STDOUT:   %bound_method.loc9_11: <bound method> = bound_method %x.ref.loc9_10, %impl.elem0
 // CHECK:STDOUT:   %x.ref.loc9_21: %MyInt.f30 = name_ref x, %x
-// CHECK:STDOUT:   %specific_fn: <specific function> = specific_function %impl.elem0, @Op.2(constants.%int_64) [concrete = constants.%Op.specific_fn.16a]
+// CHECK:STDOUT:   %specific_fn: <specific function> = specific_function %impl.elem0, @Op.2(constants.%int_64) [concrete = constants.%Op.specific_fn]
 // CHECK:STDOUT:   %bound_method.loc9_22: <bound method> = bound_method %x.ref.loc9_10, %specific_fn
 // CHECK:STDOUT:   %int.sadd: init %MyInt.f30 = call %bound_method.loc9_22(%x.ref.loc9_10, %x.ref.loc9_21)
 // CHECK:STDOUT:   %.loc9_23.1: %MyInt.f30 = value_of_initializer %int.sadd
@@ -620,12 +624,11 @@ var n: Int(64) = MakeFromClass(FromLiteral(64) as OtherInt);
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT:   %require_complete: <witness> = require_complete_type @Double.%MyInt (%MyInt.09f) [symbolic = %require_complete (constants.%require_complete.fc7)]
-// CHECK:STDOUT:   %impl_witness: <witness> = impl_witness (imports.%Main.import_ref.464c51.2), @impl(%N) [symbolic = %impl_witness (constants.%impl_witness.7e5be3.2)]
-// CHECK:STDOUT:   %Add.facet: %Add.type = facet_value %MyInt, (%impl_witness) [symbolic = %Add.facet (constants.%Add.facet.afa)]
-// CHECK:STDOUT:   %.1: type = fn_type_with_self_type constants.%Op.type.31b, %Add.facet [symbolic = %.1 (constants.%.207)]
-// CHECK:STDOUT:   %Op.type: type = fn_type @Op.2, @impl(%N) [symbolic = %Op.type (constants.%Op.type.883)]
-// CHECK:STDOUT:   %Op: @Double.%Op.type (%Op.type.883) = struct_value () [symbolic = %Op (constants.%Op.8bc)]
-// CHECK:STDOUT:   %Op.specific_fn: <specific function> = specific_function %Op, @Op.2(%N) [symbolic = %Op.specific_fn (constants.%Op.specific_fn.6c0)]
+// CHECK:STDOUT:   %Add.impl_symbolic_witness: <witness> = impl_symbolic_witness %MyInt, @Add [symbolic = %Add.impl_symbolic_witness (constants.%Add.impl_symbolic_witness)]
+// CHECK:STDOUT:   %Add.facet: %Add.type = facet_value %MyInt, (%Add.impl_symbolic_witness) [symbolic = %Add.facet (constants.%Add.facet.f76)]
+// CHECK:STDOUT:   %.1: type = fn_type_with_self_type constants.%Op.type.31b, %Add.facet [symbolic = %.1 (constants.%.dfa)]
+// CHECK:STDOUT:   %impl.elem0: @Double.%.1 (%.dfa) = impl_witness_access %Add.impl_symbolic_witness, element0 [symbolic = %impl.elem0 (constants.%impl.elem0)]
+// CHECK:STDOUT:   %specific_impl_fn: <specific function> = specific_impl_function %impl.elem0, @Op.1(%Add.facet) [symbolic = %specific_impl_fn (constants.%specific_impl_fn)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   fn[%N.patt.1: Core.IntLiteral](%x.param_patt: @Double.%MyInt (%MyInt.09f)) -> @Double.%MyInt (%MyInt.09f);
 // CHECK:STDOUT: }
@@ -676,8 +679,6 @@ var n: Int(64) = MakeFromClass(FromLiteral(64) as OtherInt);
 // CHECK:STDOUT: specific @Op.2(constants.%N) {
 // CHECK:STDOUT:   %N => constants.%N
 // CHECK:STDOUT:   %MyInt => constants.%MyInt.09f
-// CHECK:STDOUT:
-// CHECK:STDOUT: !definition:
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @impl(constants.%int_64) {
@@ -707,9 +708,12 @@ var n: Int(64) = MakeFromClass(FromLiteral(64) as OtherInt);
 // CHECK:STDOUT:   %MyInt => constants.%MyInt.09f
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @impl(@Double.%N) {}
+// CHECK:STDOUT: specific @Op.1(constants.%Add.facet.f76) {
+// CHECK:STDOUT:   %Self => constants.%Add.facet.f76
+// CHECK:STDOUT:   %Self.as_type => constants.%MyInt.09f
+// CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @Op.2(@Double.%N) {}
+// CHECK:STDOUT: specific @Op.1(@Double.%Add.facet) {}
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @Double(constants.%int_64) {
 // CHECK:STDOUT:   %N => constants.%int_64
@@ -718,12 +722,16 @@ var n: Int(64) = MakeFromClass(FromLiteral(64) as OtherInt);
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT:   %require_complete => constants.%complete_type.4a1
-// CHECK:STDOUT:   %impl_witness => constants.%impl_witness.bb3
-// CHECK:STDOUT:   %Add.facet => constants.%Add.facet.287
-// CHECK:STDOUT:   %.1 => constants.%.fc5
-// CHECK:STDOUT:   %Op.type => constants.%Op.type.5a6
-// CHECK:STDOUT:   %Op => constants.%Op.cf9
-// CHECK:STDOUT:   %Op.specific_fn => constants.%Op.specific_fn.16a
+// CHECK:STDOUT:   %Add.impl_symbolic_witness => constants.%impl_witness.8d6
+// CHECK:STDOUT:   %Add.facet => constants.%Add.facet.8db
+// CHECK:STDOUT:   %.1 => constants.%.1ca
+// CHECK:STDOUT:   %impl.elem0 => constants.%Op.cf9
+// CHECK:STDOUT:   %specific_impl_fn => constants.%Op.specific_fn
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @Op.1(constants.%Add.facet.8db) {
+// CHECK:STDOUT:   %Self => constants.%Add.facet.8db
+// CHECK:STDOUT:   %Self.as_type => constants.%MyInt.f30
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: --- convert_symbolic.carbon

toolchain/check/testdata/interface/no_prelude/fail_assoc_const_alias.carbon

@@ -360,13 +360,15 @@ interface C {
 // CHECK:STDOUT:   %.Self.as_type: type = facet_access_type %.Self [symbolic_self]
 // CHECK:STDOUT:   %.Self.as_wit.iface0: <witness> = facet_access_witness %.Self, element0 [symbolic_self]
 // CHECK:STDOUT:   %I2.facet.b82: %I2.type = facet_value %.Self.as_type, (%.Self.as_wit.iface0) [symbolic_self]
-// CHECK:STDOUT:   %impl.elem0: type = impl_witness_access %.Self.as_wit.iface0, element0 [symbolic_self]
-// CHECK:STDOUT:   %I2_where.type: type = facet_type <@I2 where %impl.elem0 = %empty_tuple.type> [concrete]
+// CHECK:STDOUT:   %impl.elem0.71d: type = impl_witness_access %.Self.as_wit.iface0, element0 [symbolic_self]
+// CHECK:STDOUT:   %I2_where.type: type = facet_type <@I2 where %impl.elem0.71d = %empty_tuple.type> [concrete]
 // CHECK:STDOUT:   %impl_witness.ec95d0.1: <witness> = impl_witness (%empty_tuple.type), @impl(%V) [symbolic]
 // CHECK:STDOUT:   %Self.541: %J2.type = bind_symbolic_name Self, 0 [symbolic]
 // CHECK:STDOUT:   %Self.as_type: type = facet_access_type %Self.541 [symbolic]
 // CHECK:STDOUT:   %impl_witness.ec95d0.2: <witness> = impl_witness (%empty_tuple.type), @impl(%Self.541) [symbolic]
-// CHECK:STDOUT:   %I2.facet.746: %I2.type = facet_value %Self.as_type, (%impl_witness.ec95d0.2) [symbolic]
+// CHECK:STDOUT:   %I2.impl_symbolic_witness: <witness> = impl_symbolic_witness %Self.541, @I2 [symbolic]
+// CHECK:STDOUT:   %I2.facet.fc4: %I2.type = facet_value %Self.as_type, (%I2.impl_symbolic_witness) [symbolic]
+// CHECK:STDOUT:   %impl.elem0.e6b: type = impl_witness_access %I2.impl_symbolic_witness, element0 [symbolic]
 // CHECK:STDOUT:   %F2.type: type = fn_type @F2 [concrete]
 // CHECK:STDOUT:   %F2: %F2.type = struct_value () [concrete]
 // CHECK:STDOUT:   %J2.assoc_type: type = assoc_entity_type %J2.type [concrete]
@@ -401,7 +403,7 @@ interface C {
 // CHECK:STDOUT:     %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:     %.loc11_36: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:     %.Self.as_wit.iface0: <witness> = facet_access_witness %.Self.ref, element0 [symbolic_self = constants.%.Self.as_wit.iface0]
-// CHECK:STDOUT:     %impl.elem0: type = impl_witness_access %.Self.as_wit.iface0, element0 [symbolic_self = constants.%impl.elem0]
+// CHECK:STDOUT:     %impl.elem0: type = impl_witness_access %.Self.as_wit.iface0, element0 [symbolic_self = constants.%impl.elem0.71d]
 // CHECK:STDOUT:     %.loc11_43.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:     %.loc11_43.2: type = converted %.loc11_43.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:     %.loc11_30: type = where_expr %.Self [concrete = constants.%I2_where.type] {
@@ -432,21 +434,24 @@ interface C {
 // CHECK:STDOUT:   %T2.ref: %I2.assoc_type = name_ref T2, @T2.%assoc0 [concrete = constants.%assoc0.166]
 // CHECK:STDOUT:   %U2: %I2.assoc_type = bind_alias U2, @T2.%assoc0 [concrete = constants.%assoc0.166]
 // CHECK:STDOUT:   %F2.decl: %F2.type = fn_decl @F2 [concrete = constants.%F2] {
-// CHECK:STDOUT:     %return.patt: %empty_tuple.type = return_slot_pattern
-// CHECK:STDOUT:     %return.param_patt: %empty_tuple.type = out_param_pattern %return.patt, call_param0
+// CHECK:STDOUT:     %return.patt: @F2.%impl.elem0.loc15_14.1 (%impl.elem0.e6b) = return_slot_pattern
+// CHECK:STDOUT:     %return.param_patt: @F2.%impl.elem0.loc15_14.1 (%impl.elem0.e6b) = out_param_pattern %return.patt, call_param0
 // CHECK:STDOUT:   } {
 // CHECK:STDOUT:     %Self.as_type.loc15_14.2: type = facet_access_type constants.%Self.541 [symbolic = %Self.as_type.loc15_14.1 (constants.%Self.as_type)]
 // CHECK:STDOUT:     %.loc15_14.1: type = converted constants.%Self.541, %Self.as_type.loc15_14.2 [symbolic = %Self.as_type.loc15_14.1 (constants.%Self.as_type)]
 // CHECK:STDOUT:     %.loc15_14.2: %J2.type = converted %.loc15_14.1, constants.%Self.541 [symbolic = %Self (constants.%Self.541)]
 // CHECK:STDOUT:     %Self.as_type.loc15_14.3: type = facet_access_type constants.%Self.541 [symbolic = %Self.as_type.loc15_14.1 (constants.%Self.as_type)]
-// CHECK:STDOUT:     %I2.facet.loc15_14.2: %I2.type = facet_value %Self.as_type.loc15_14.3, (constants.%impl_witness.ec95d0.2) [symbolic = %I2.facet.loc15_14.1 (constants.%I2.facet.746)]
-// CHECK:STDOUT:     %.loc15_14.3: %I2.type = converted @J2.%Self, %I2.facet.loc15_14.2 [symbolic = %I2.facet.loc15_14.1 (constants.%I2.facet.746)]
-// CHECK:STDOUT:     %as_wit.iface0: <witness> = facet_access_witness %.loc15_14.3, element0 [symbolic = %impl_witness (constants.%impl_witness.ec95d0.2)]
-// CHECK:STDOUT:     %impl.elem0: type = impl_witness_access %as_wit.iface0, element0 [concrete = constants.%empty_tuple.type]
-// CHECK:STDOUT:     %U2.ref: type = name_ref U2, %impl.elem0 [concrete = constants.%empty_tuple.type]
-// CHECK:STDOUT:     %return.param: ref %empty_tuple.type = out_param call_param0
-// CHECK:STDOUT:     %return: ref %empty_tuple.type = return_slot %return.param
+// CHECK:STDOUT:     %I2.facet.loc15_14.2: %I2.type = facet_value %Self.as_type.loc15_14.3, (constants.%I2.impl_symbolic_witness) [symbolic = %I2.facet.loc15_14.1 (constants.%I2.facet.fc4)]
+// CHECK:STDOUT:     %.loc15_14.3: %I2.type = converted @J2.%Self, %I2.facet.loc15_14.2 [symbolic = %I2.facet.loc15_14.1 (constants.%I2.facet.fc4)]
+// CHECK:STDOUT:     %as_wit.iface0: <witness> = facet_access_witness %.loc15_14.3, element0 [symbolic = %I2.impl_symbolic_witness (constants.%I2.impl_symbolic_witness)]
+// CHECK:STDOUT:     %impl.elem0.loc15_14.2: type = impl_witness_access %as_wit.iface0, element0 [symbolic = %impl.elem0.loc15_14.1 (constants.%impl.elem0.e6b)]
+// CHECK:STDOUT:     %U2.ref: type = name_ref U2, %impl.elem0.loc15_14.2 [symbolic = %impl.elem0.loc15_14.1 (constants.%impl.elem0.e6b)]
+// CHECK:STDOUT:     %return.param: ref @F2.%impl.elem0.loc15_14.1 (%impl.elem0.e6b) = out_param call_param0
+// CHECK:STDOUT:     %return: ref @F2.%impl.elem0.loc15_14.1 (%impl.elem0.e6b) = return_slot %return.param
 // CHECK:STDOUT:   }
+// CHECK:STDOUT:   %Self.as_type: type = facet_access_type constants.%Self.541 [symbolic = constants.%Self.as_type]
+// CHECK:STDOUT:   %.loc15_14.1: type = converted constants.%Self.541, %Self.as_type [symbolic = constants.%Self.as_type]
+// CHECK:STDOUT:   %.loc15_14.2: %J2.type = converted %.loc15_14.1, constants.%Self.541 [symbolic = constants.%Self.541]
 // CHECK:STDOUT:   %assoc0: %J2.assoc_type = assoc_entity element0, %F2.decl [concrete = constants.%assoc0.5b2]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !members:
@@ -478,10 +483,11 @@ interface C {
 // CHECK:STDOUT: generic fn @F2(@J2.%Self: %J2.type) {
 // CHECK:STDOUT:   %Self: %J2.type = bind_symbolic_name Self, 0 [symbolic = %Self (constants.%Self.541)]
 // CHECK:STDOUT:   %Self.as_type.loc15_14.1: type = facet_access_type %Self [symbolic = %Self.as_type.loc15_14.1 (constants.%Self.as_type)]
-// CHECK:STDOUT:   %impl_witness: <witness> = impl_witness (constants.%empty_tuple.type), @impl(%Self) [symbolic = %impl_witness (constants.%impl_witness.ec95d0.2)]
-// CHECK:STDOUT:   %I2.facet.loc15_14.1: %I2.type = facet_value %Self.as_type.loc15_14.1, (%impl_witness) [symbolic = %I2.facet.loc15_14.1 (constants.%I2.facet.746)]
+// CHECK:STDOUT:   %I2.impl_symbolic_witness: <witness> = impl_symbolic_witness %Self, @I2 [symbolic = %I2.impl_symbolic_witness (constants.%I2.impl_symbolic_witness)]
+// CHECK:STDOUT:   %I2.facet.loc15_14.1: %I2.type = facet_value %Self.as_type.loc15_14.1, (%I2.impl_symbolic_witness) [symbolic = %I2.facet.loc15_14.1 (constants.%I2.facet.fc4)]
+// CHECK:STDOUT:   %impl.elem0.loc15_14.1: type = impl_witness_access %I2.impl_symbolic_witness, element0 [symbolic = %impl.elem0.loc15_14.1 (constants.%impl.elem0.e6b)]
 // CHECK:STDOUT:
-// CHECK:STDOUT:   fn() -> %empty_tuple.type;
+// CHECK:STDOUT:   fn() -> @F2.%impl.elem0.loc15_14.1 (%impl.elem0.e6b);
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @T2(constants.%Self.c7b) {}
@@ -506,17 +512,16 @@ interface C {
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @T2(constants.%I2.facet.746) {}
+// CHECK:STDOUT: specific @T2(constants.%I2.facet.fc4) {}
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @F2(constants.%Self.541) {
 // CHECK:STDOUT:   %Self => constants.%Self.541
 // CHECK:STDOUT:   %Self.as_type.loc15_14.1 => constants.%Self.as_type
-// CHECK:STDOUT:   %impl_witness => constants.%impl_witness.ec95d0.2
-// CHECK:STDOUT:   %I2.facet.loc15_14.1 => constants.%I2.facet.746
+// CHECK:STDOUT:   %I2.impl_symbolic_witness => constants.%I2.impl_symbolic_witness
+// CHECK:STDOUT:   %I2.facet.loc15_14.1 => constants.%I2.facet.fc4
+// CHECK:STDOUT:   %impl.elem0.loc15_14.1 => constants.%impl.elem0.e6b
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @impl(@F2.%Self) {}
-// CHECK:STDOUT:
 // CHECK:STDOUT: --- fail_call_method_alias.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {

toolchain/check/type_completion.cpp

@@ -11,6 +11,7 @@
 #include "toolchain/check/type.h"
 #include "toolchain/diagnostics/format_providers.h"
 #include "toolchain/sem_ir/ids.h"
+#include "toolchain/sem_ir/typed_insts.h"
 
 namespace Carbon::Check {
 

toolchain/check/type_structure.cpp

@@ -206,7 +206,8 @@ class TypeStructureBuilder {
         case SemIR::IntLiteralType::Kind:
         case SemIR::LegacyFloatType::Kind:
         case SemIR::StringType::Kind:
-        case SemIR::TypeType::Kind: {
+        case SemIR::TypeType::Kind:
+        case SemIR::WitnessType::Kind: {
           AppendStructural(TypeStructure::Structural::Concrete);
           break;
         }

toolchain/sem_ir/dump.cpp

@@ -247,7 +247,20 @@ LLVM_DUMP_METHOD auto Dump(const File& file,
 LLVM_DUMP_METHOD auto Dump(const File& file, SpecificId specific_id) -> void {
   DumpNoNewline(file, specific_id);
   llvm::errs() << '\n';
-  Dump(file, file.specifics().Get(specific_id).args_id);
+  if (specific_id.has_value()) {
+    Dump(file, file.specifics().Get(specific_id).args_id);
+  }
+}
+
+LLVM_DUMP_METHOD auto Dump(const File& file,
+                           SpecificInterfaceId specific_interface_id) -> void {
+  const auto& interface = file.specific_interfaces().Get(specific_interface_id);
+  llvm::errs() << specific_interface_id << '\n';
+  llvm::errs() << "  - interface: ";
+  DumpNoNewline(file, interface.interface_id);
+  llvm::errs() << '\n';
+  llvm::errs() << "  - specific_id: ";
+  Dump(file, interface.specific_id);
 }
 
 LLVM_DUMP_METHOD auto Dump(const File& file,
@@ -336,6 +349,10 @@ LLVM_DUMP_METHOD static auto MakeCompleteFacetTypeId(int id)
 LLVM_DUMP_METHOD static auto MakeSpecificId(int id) -> SpecificId {
   return SpecificId(id);
 }
+LLVM_DUMP_METHOD static auto MakeSpecificInterfaceId(int id)
+    -> SpecificInterfaceId {
+  return SpecificInterfaceId(id);
+}
 LLVM_DUMP_METHOD static auto MakeStructTypeFieldsId(int id)
     -> StructTypeFieldsId {
   return StructTypeFieldsId(id);

toolchain/sem_ir/dump.h

@@ -34,6 +34,7 @@ auto Dump(const File& file, NameId name_id) -> void;
 auto Dump(const File& file, NameScopeId name_scope_id) -> void;
 auto Dump(const File& file, CompleteFacetTypeId complete_facet_type_id) -> void;
 auto Dump(const File& file, SpecificId specific_id) -> void;
+auto Dump(const File& file, SpecificInterfaceId specific_interface_id) -> void;
 auto Dump(const File& file, StructTypeFieldsId struct_type_fields_id) -> void;
 auto Dump(const File& file, TypeBlockId type_block_id) -> void;
 auto Dump(const File& file, TypeId type_id) -> void;

toolchain/sem_ir/file.cpp

@@ -270,6 +270,7 @@ auto GetExprCategory(const File& file, InstId inst_id) -> ExprCategory {
       case FunctionTypeWithSelfType::Kind:
       case GenericClassType::Kind:
       case GenericInterfaceType::Kind:
+      case ImplSymbolicWitness::Kind:
       case ImplWitness::Kind:
       case ImplWitnessAccess::Kind:
       case ImportCppDecl::Kind:

toolchain/sem_ir/file.h

@@ -169,6 +169,13 @@ class File : public Printable<File> {
   }
   auto impls() -> ImplStore& { return impls_; }
   auto impls() const -> const ImplStore& { return impls_; }
+  auto specific_interfaces() -> CanonicalValueStore<SpecificInterfaceId>& {
+    return specific_interfaces_;
+  }
+  auto specific_interfaces() const
+      -> const CanonicalValueStore<SpecificInterfaceId>& {
+    return specific_interfaces_;
+  }
   auto generics() -> GenericStore& { return generics_; }
   auto generics() const -> const GenericStore& { return generics_; }
   auto specifics() -> SpecificStore& { return specifics_; }
@@ -291,6 +298,10 @@ class File : public Printable<File> {
   // Storage for impls.
   ImplStore impls_;
 
+  // Storage for specific interfaces, which are an individual unit of impl
+  // lookup for a single interface.
+  CanonicalValueStore<SpecificInterfaceId> specific_interfaces_;
+
   // Storage for generics.
   GenericStore generics_;
 

toolchain/sem_ir/formatter.cpp

@@ -1388,6 +1388,15 @@ class FormatterImpl {
     FormatArg(specific.args_id);
   }
 
+  auto FormatName(SpecificInterfaceId id) -> void {
+    const auto& interface = sem_ir_->specific_interfaces().Get(id);
+    FormatName(interface.interface_id);
+    if (interface.specific_id.has_value()) {
+      out_ << ", ";
+      FormatArg(interface.specific_id);
+    }
+  }
+
   auto FormatLabel(InstBlockId id) -> void {
     out_ << inst_namer_->GetLabelFor(scope_, id);
   }

toolchain/sem_ir/id_kind.h

@@ -135,17 +135,52 @@ class TypeEnum : public Printable<TypeEnum<Types...>> {
 // instructions (`toolchain/sem_ir/typed_insts.h`) and must implement the
 // `FromRaw` and `ToRaw` protocol in `SemIR::Inst`. In most cases this is done
 // by inheriting from `IdBase` or `IndexBase`.
+//
+// clang-format off: We want one per line.
 using IdKind = TypeEnum<
     // From base/value_store.h.
-    IntId, RealId, FloatId, StringLiteralValueId,
+    FloatId,
+    IntId,
+    RealId,
+    StringLiteralValueId,
     // From sem_ir/ids.h.
-    InstId, AbsoluteInstId, DestInstId, MetaInstId, AnyRawId, ConstantId,
-    EntityNameId, CompileTimeBindIndex, CallParamIndex, FacetTypeId, FunctionId,
-    ClassId, InterfaceId, AssociatedConstantId, ImplId, GenericId, SpecificId,
-    ImportIRId, ImportIRInstId, LocId, BoolValue, IntKind, NameId, NameScopeId,
-    InstBlockId, AbsoluteInstBlockId, DeclInstBlockId, LabelId, ExprRegionId,
-    StructTypeFieldsId, TypeId, TypeBlockId, ElementIndex, LibraryNameId,
-    FloatKind>;
+    AbsoluteInstBlockId,
+    AbsoluteInstId,
+    AnyRawId,
+    AssociatedConstantId,
+    BoolValue,
+    CallParamIndex,
+    ClassId,
+    CompileTimeBindIndex,
+    ConstantId,
+    DeclInstBlockId,
+    DestInstId,
+    ElementIndex,
+    EntityNameId,
+    ExprRegionId,
+    FacetTypeId,
+    FloatKind,
+    FunctionId,
+    GenericId,
+    ImplId,
+    ImportIRId,
+    ImportIRInstId,
+    InstBlockId,
+    InstId,
+    InterfaceId,
+    IntKind,
+    LabelId,
+    LibraryNameId,
+    LocId,
+    MetaInstId,
+    NameId,
+    NameScopeId,
+    SpecificId,
+    SpecificInterfaceId,
+    StructTypeFieldsId,
+    TypeBlockId,
+    TypeId>;
+// clang-format on
 
 }  // namespace Carbon::SemIR
 

toolchain/sem_ir/ids.h

@@ -27,6 +27,7 @@ struct Function;
 struct Generic;
 struct CompleteFacetType;
 struct Specific;
+struct SpecificInterface;
 struct ImportCpp;
 struct ImportIR;
 struct ImportIRInst;
@@ -306,6 +307,14 @@ struct SpecificId : public IdBase<SpecificId> {
   using IdBase::IdBase;
 };
 
+// The ID of a SpecificInterface, which is an interface and a specific pair.
+struct SpecificInterfaceId : public IdBase<SpecificInterfaceId> {
+  static constexpr llvm::StringLiteral Label = "specific_interface";
+  using ValueType = SpecificInterface;
+
+  using IdBase::IdBase;
+};
+
 // The index of an instruction that depends on generic parameters within a
 // region of a generic. A corresponding specific version of the instruction can
 // be found in each specific corresponding to that generic. This is a pair of a

toolchain/sem_ir/inst_fingerprinter.cpp

@@ -240,6 +240,17 @@ struct Worklist {
     Add(specific.args_id);
   }
 
+  auto Add(SpecificInterfaceId specific_interface_id) -> void {
+    if (!specific_interface_id.has_value()) {
+      AddInvalid();
+      return;
+    }
+    const auto& interface =
+        sem_ir->specific_interfaces().Get(specific_interface_id);
+    Add(interface.interface_id);
+    Add(interface.specific_id);
+  }
+
   auto Add(const llvm::APInt& value) -> void {
     contents.push_back(value.getBitWidth());
     for (auto word : llvm::seq((value.getBitWidth() + 63) / 64)) {

toolchain/sem_ir/inst_kind.def

@@ -70,6 +70,7 @@ CARBON_SEM_IR_INST_KIND(FunctionTypeWithSelfType)
 CARBON_SEM_IR_INST_KIND(GenericClassType)
 CARBON_SEM_IR_INST_KIND(GenericInterfaceType)
 CARBON_SEM_IR_INST_KIND(ImplDecl)
+CARBON_SEM_IR_INST_KIND(ImplSymbolicWitness)
 CARBON_SEM_IR_INST_KIND(ImplWitness)
 CARBON_SEM_IR_INST_KIND(ImplWitnessAccess)
 CARBON_SEM_IR_INST_KIND(ImportCppDecl)

toolchain/sem_ir/inst_namer.cpp

@@ -696,6 +696,14 @@ auto InstNamer::CollectNamesInBlock(ScopeId top_scope_id,
         queue_block_id(impl_scope_id, inst.decl_block_id);
         break;
       }
+      case CARBON_KIND(ImplSymbolicWitness inst): {
+        const auto& interface = sem_ir_->specific_interfaces().Get(
+            inst.query_specific_interface_id);
+        add_inst_name_id(
+            sem_ir_->interfaces().Get(interface.interface_id).name_id,
+            ".impl_symbolic_witness");
+        continue;
+      }
       case ImplWitness::Kind: {
         // TODO: Include name of interface (is this available from the
         // specific?).

toolchain/sem_ir/inst_namer.h

@@ -50,8 +50,11 @@ class InstNamer {
             index += sem_ir_->associated_constants().size();
             if constexpr (!std::same_as<ImplId, IdT>) {
               index += sem_ir_->impls().size();
-              static_assert(std::same_as<NumberOfScopesTag, IdT>,
-                            "Unknown ID kind for scope");
+              if constexpr (!std::same_as<SpecificInterfaceId, IdT>) {
+                index += sem_ir_->specific_interfaces().size();
+                static_assert(std::same_as<NumberOfScopesTag, IdT>,
+                              "Unknown ID kind for scope");
+              }
             }
           }
         }

toolchain/sem_ir/stringify_type.cpp

@@ -375,6 +375,11 @@ class Stringifier {
       -> void {
     auto witness_inst_id =
         sem_ir_->constant_values().GetConstantInstId(inst.witness_id);
+    if (sem_ir_->insts().Is<SemIR::ImplSymbolicWitness>(witness_inst_id)) {
+      // TODO: Include the query in the diagnostic output?
+      step_stack_->PushString("<symbolic>");
+      return;
+    }
     auto witness = sem_ir_->insts().GetAs<FacetAccessWitness>(witness_inst_id);
     auto witness_type_id =
         sem_ir_->insts().Get(witness.facet_value_inst_id).type_id();

toolchain/sem_ir/typed_insts.h

@@ -868,6 +868,24 @@ struct ImplDecl {
   DeclInstBlockId decl_block_id;
 };
 
+// A symbolic witness that a type implements an interface. It represents a
+// promise that an impl lookup query can be satisfied without providing which
+// impl declaration satisfies it. When evaluated, it does lookup again to form a
+// concrete ImplWitness from a more specific query.
+struct ImplSymbolicWitness {
+  static constexpr auto Kind =
+      InstKind::ImplSymbolicWitness.Define<Parse::NodeId>(
+          {.ir_name = "impl_symbolic_witness",
+           .constant_kind = InstConstantKind::SymbolicOnly,
+           .is_lowered = false});
+
+  // Always the type of the builtin `WitnessType` singleton instruction.
+  TypeId type_id;
+  // The self type (or facet value) and interface of the impl lookup query.
+  InstId query_self_inst_id;
+  SpecificInterfaceId query_specific_interface_id;
+};
+
 // A witness that a type implements an interface.
 struct ImplWitness {
   static constexpr auto Kind = InstKind::ImplWitness.Define<Parse::NodeId>(
@@ -1780,7 +1798,9 @@ struct WhereExpr {
   InstBlockId requirements_id;
 };
 
-// The type of `ImplWitness` instructions.
+// The type of `ImplWitness` and `ImplSymbolicType` instructions. The latter
+// will evaluate at some point during specific computation into the former, and
+// their types should not change in the process.
 struct WitnessType {
   static constexpr auto Kind = InstKind::WitnessType.Define<Parse::NoneNodeId>(
       {.ir_name = "<witness>",