Poison impl lookup queries with concrete results (#5373)

Once a concrete result has been found, it's not legal to write an `impl`
that would change the concrete result afterward.

---------

Co-authored-by: Richard Smith <richard@metafoo.co.uk>

toolchain/check/check_unit.cpp

@@ -12,18 +12,22 @@
 #include "llvm/Support/VirtualFileSystem.h"
 #include "toolchain/base/kind_switch.h"
 #include "toolchain/base/pretty_stack_trace_function.h"
+#include "toolchain/check/diagnostic_helpers.h"
 #include "toolchain/check/generic.h"
 #include "toolchain/check/handle.h"
 #include "toolchain/check/impl.h"
+#include "toolchain/check/impl_lookup.h"
 #include "toolchain/check/import.h"
 #include "toolchain/check/import_cpp.h"
 #include "toolchain/check/import_ref.h"
 #include "toolchain/check/inst.h"
 #include "toolchain/check/node_id_traversal.h"
 #include "toolchain/check/type.h"
+#include "toolchain/diagnostics/diagnostic.h"
 #include "toolchain/sem_ir/function.h"
 #include "toolchain/sem_ir/ids.h"
 #include "toolchain/sem_ir/import_ir.h"
+#include "toolchain/sem_ir/typed_insts.h"
 
 namespace Carbon::Check {
 
@@ -511,9 +515,65 @@ auto CheckUnit::CheckRequiredDefinitions() -> void {
   }
 }
 
+auto CheckUnit::CheckPoisonedConcreteImplLookupQueries() -> void {
+  // Impl lookup can generate instructions (via deduce) which we don't use, as
+  // we're only generating diagnostics here, so we catch and discard them.
+  context_.inst_block_stack().Push();
+  auto poisoned_queries =
+      std::exchange(context_.poisoned_concrete_impl_lookup_queries(), {});
+  for (const auto& poison : poisoned_queries) {
+    auto witness_result =
+        EvalLookupSingleImplWitness(context_, poison.loc_id, poison.query,
+                                    poison.non_canonical_query_self_inst_id,
+                                    /*poison_concrete_results=*/false);
+    CARBON_CHECK(witness_result.has_concrete_value());
+    auto found_witness_id = witness_result.concrete_witness();
+    if (found_witness_id != poison.impl_witness) {
+      auto witness_to_impl_id = [&](SemIR::InstId witness_id) {
+        auto table_id = context_.insts()
+                            .GetAs<SemIR::ImplWitness>(witness_id)
+                            .witness_table_id;
+        return context_.insts()
+            .GetAs<SemIR::ImplWitnessTable>(table_id)
+            .impl_id;
+      };
+
+      // We can get the `Impl` from the resulting witness here, which is the
+      // `Impl` that conflicts with the previous poison query.
+      auto bad_impl_id = witness_to_impl_id(found_witness_id);
+      const auto& bad_impl = context_.impls().Get(bad_impl_id);
+
+      auto prev_impl_id = witness_to_impl_id(poison.impl_witness);
+      const auto& prev_impl = context_.impls().Get(prev_impl_id);
+
+      CARBON_DIAGNOSTIC(
+          PoisonedImplLookupConcreteResult, Error,
+          "found `impl` that would change the result of an earlier "
+          "use of `{0} as {1}`",
+          InstIdAsRawType, SpecificInterfaceIdAsRawType);
+      auto builder =
+          emitter_.Build(poison.loc_id, PoisonedImplLookupConcreteResult,
+                         poison.query.query_self_inst_id,
+                         poison.query.query_specific_interface_id);
+      CARBON_DIAGNOSTIC(
+          PoisonedImplLookupConcreteResultNoteBadImpl, Note,
+          "the use would select the `impl` here but it was not found yet");
+      builder.Note(bad_impl.first_decl_id(),
+                   PoisonedImplLookupConcreteResultNoteBadImpl);
+      CARBON_DIAGNOSTIC(PoisonedImplLookupConcreteResultNotePreviousImpl, Note,
+                        "the use had selected the `impl` here");
+      builder.Note(prev_impl.first_decl_id(),
+                   PoisonedImplLookupConcreteResultNotePreviousImpl);
+      builder.Emit();
+    }
+  }
+  context_.inst_block_stack().PopAndDiscard();
+}
+
 auto CheckUnit::FinishRun() -> void {
   CheckRequiredDeclarations();
   CheckRequiredDefinitions();
+  CheckPoisonedConcreteImplLookupQueries();
 
   // Pop information for the file-level scope.
   context_.sem_ir().set_top_inst_block_id(context_.inst_block_stack().Pop());

toolchain/check/check_unit.h

@@ -166,6 +166,10 @@ class CheckUnit {
   // context.definitions_required_by_use that doesn't have a definition.
   auto CheckRequiredDefinitions() -> void;
 
+  // Re-run every impl lookup with a concrete result and make sure they find the
+  // same witnesses.
+  auto CheckPoisonedConcreteImplLookupQueries() -> void;
+
   // Does work after processing the parse tree, such as finishing the IR and
   // checking for missing contents.
   auto FinishRun() -> void;

toolchain/check/context.h

@@ -204,6 +204,21 @@ class Context {
     return impl_lookup_stack_;
   }
 
+  // A concrete impl lookup query and its result.
+  struct PoisonedConcreteImplLookupQuery {
+    // The location the LookupImplWitness originated from.
+    SemIR::LocId loc_id;
+    // The query for a witness of an impl for an interface.
+    SemIR::LookupImplWitness query;
+    SemIR::InstId non_canonical_query_self_inst_id;
+    // The resulting ImplWitness.
+    SemIR::InstId impl_witness;
+  };
+  auto poisoned_concrete_impl_lookup_queries()
+      -> llvm::SmallVector<PoisonedConcreteImplLookupQuery>& {
+    return poisoned_concrete_impl_lookup_queries_;
+  }
+
   // --------------------------------------------------------------------------
   // Directly expose SemIR::File data accessors for brevity in calls.
   // --------------------------------------------------------------------------
@@ -386,6 +401,12 @@ class Context {
   // Tracks all ongoing impl lookups in order to ensure that lookup terminates
   // via the acyclic rule and the termination rule.
   llvm::SmallVector<ImplLookupStackEntry> impl_lookup_stack_;
+
+  // Tracks impl lookup queries that lead to concrete witness results, along
+  // with those results. Used to verify that the same queries produce the same
+  // results at the end of the file. Any difference is diagnosed.
+  llvm::SmallVector<PoisonedConcreteImplLookupQuery>
+      poisoned_concrete_impl_lookup_queries_;
 };
 
 }  // namespace Carbon::Check

toolchain/check/diagnostic_emitter.cpp

@@ -9,6 +9,7 @@
 #include <string>
 
 #include "common/raw_string_ostream.h"
+#include "toolchain/check/diagnostic_helpers.h"
 #include "toolchain/sem_ir/absolute_node_id.h"
 #include "toolchain/sem_ir/stringify.h"
 
@@ -164,6 +165,18 @@ auto DiagnosticEmitter::ConvertArg(llvm::Any arg) const -> llvm::Any {
     return llvm::APSInt(typed_int->value,
                         !sem_ir_->types().IsSignedInt(typed_int->type));
   }
+  if (auto* specific_interface_id =
+          llvm::any_cast<SemIR::SpecificInterfaceId>(&arg)) {
+    auto specific_interface =
+        sem_ir_->specific_interfaces().Get(*specific_interface_id);
+    return "`" + StringifySpecificInterface(*sem_ir_, specific_interface) + "`";
+  }
+  if (auto* specific_interface_raw =
+          llvm::any_cast<SpecificInterfaceIdAsRawType>(&arg)) {
+    auto specific_interface = sem_ir_->specific_interfaces().Get(
+        specific_interface_raw->specific_interface_id);
+    return StringifySpecificInterface(*sem_ir_, specific_interface);
+  }
   return DiagnosticEmitterBase::ConvertArg(arg);
 }
 

toolchain/check/diagnostic_helpers.h

@@ -127,6 +127,16 @@ struct TypedInt {
   llvm::APInt value;
 };
 
+struct SpecificInterfaceIdAsRawType {
+  using DiagnosticType = Diagnostics::TypeInfo<std::string>;
+
+  // NOLINTNEXTLINE(google-explicit-constructor)
+  SpecificInterfaceIdAsRawType(SemIR::SpecificInterfaceId specific_interface_id)
+      : specific_interface_id(specific_interface_id) {}
+
+  SemIR::SpecificInterfaceId specific_interface_id;
+};
+
 }  // namespace Carbon::Check
 
 #endif  // CARBON_TOOLCHAIN_CHECK_DIAGNOSTIC_HELPERS_H_

toolchain/check/eval_inst.cpp

@@ -207,7 +207,8 @@ auto EvalConstantInst(Context& context, SemIR::InstId inst_id,
       GetCanonicalizedFacetOrTypeValue(context, inst.query_self_inst_id);
 
   auto result = EvalLookupSingleImplWitness(
-      context, SemIR::LocId(inst_id), inst, non_canonical_query_self_inst_id);
+      context, SemIR::LocId(inst_id), inst, non_canonical_query_self_inst_id,
+      /*poison_concrete_results=*/true);
   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

toolchain/check/impl_lookup.cpp

@@ -286,7 +286,7 @@ static auto GetWitnessIdForImpl(Context& context, SemIR::LocId loc_id,
     ResolveSpecificDefinition(context, loc_id, specific_id);
   }
 
-  if (query_is_concrete || IsImplEffectivelyFinal(context, impl)) {
+  if (query_is_concrete || impl.is_final) {
     // TODO: These final results should be cached somehow. Positive (non-None)
     // results could be cached globally, as they can not change. But
     // negative results can change after a final impl is written, so
@@ -460,8 +460,6 @@ auto LookupImplWitness(Context& context, SemIR::LocId loc_id,
     }
   }
   stack.pop_back();
-  // TODO: Validate that the witness satisfies the other requirements in
-  // `interface_const_id`.
 
   // All interfaces in the query facet type must have been found to be available
   // through some impl, or directly on the value's facet type if
@@ -470,13 +468,16 @@ auto LookupImplWitness(Context& context, SemIR::LocId loc_id,
     return SemIR::InstBlockId::None;
   }
 
+  // TODO: Validate that the witness satisfies the other requirements in
+  // `interface_const_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)
+                            const SemIR::SpecificInterface& specific_interface)
     -> bool {
   if (!self_const_id.is_concrete()) {
     return false;
@@ -571,7 +572,8 @@ static auto CollectCandidateImplsForQuery(
 
 auto EvalLookupSingleImplWitness(Context& context, SemIR::LocId loc_id,
                                  SemIR::LookupImplWitness eval_query,
-                                 SemIR::InstId non_canonical_query_self_inst_id)
+                                 SemIR::InstId non_canonical_query_self_inst_id,
+                                 bool poison_concrete_results)
     -> EvalImplLookupResult {
   // NOTE: Do not retain this reference to the SpecificInterface obtained from a
   // value store by SpecificInterfaceId. Doing impl lookup does deduce which can
@@ -652,6 +654,22 @@ auto EvalLookupSingleImplWitness(Context& context, SemIR::LocId loc_id,
         context, loc_id, query_is_concrete, query_self_const_id,
         query_specific_interface, candidate.impl_id);
     if (result.has_value()) {
+      // Record the query which found a concrete impl witness. It's illegal to
+      // write a final impl afterward that would match the same query.
+      //
+      // If the impl was effectively final, then we don't need to poison here. A
+      // change of query result will already be diagnosed at the point where the
+      // new impl decl was written that changes the result.
+      if (poison_concrete_results && result.has_concrete_value() &&
+          !IsImplEffectivelyFinal(context,
+                                  context.impls().Get(candidate.impl_id))) {
+        context.poisoned_concrete_impl_lookup_queries().push_back(
+            {.loc_id = loc_id,
+             .query = eval_query,
+             .non_canonical_query_self_inst_id =
+                 non_canonical_query_self_inst_id,
+             .impl_witness = result.concrete_witness()});
+      }
       return result;
     }
   }

toolchain/check/impl_lookup.h

@@ -96,7 +96,8 @@ class [[nodiscard]] EvalImplLookupResult {
 // have found that and not caused us to defer lookup to here.
 auto EvalLookupSingleImplWitness(Context& context, SemIR::LocId loc_id,
                                  SemIR::LookupImplWitness eval_query,
-                                 SemIR::InstId non_canonical_query_self_inst_id)
+                                 SemIR::InstId non_canonical_query_self_inst_id,
+                                 bool poison_concrete_results)
     -> EvalImplLookupResult;
 
 }  // namespace Carbon::Check

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

@@ -11,7 +11,7 @@
 // TIP: To dump output, run:
 // TIP:   bazel run //toolchain/testing:file_test -- --dump_output --file_tests=toolchain/check/testdata/impl/lookup/min_prelude/specialization_poison.carbon
 
-// --- todo_fail_final_poisoned_concrete_query.carbon
+// --- fail_final_poisoned_concrete_query_in_specific.carbon
 library "[[@TEST_NAME]]";
 
 interface I {
@@ -23,6 +23,9 @@ impl forall [U:! type] U as I where .T = () {
   fn F[self: Self]() -> () { return (); }
 }
 
+// CHECK:STDERR: fail_final_poisoned_concrete_query_in_specific.carbon:[[@LINE+3]]:25: error: found `impl` that would change the result of an earlier use of `C* as I` [PoisonedImplLookupConcreteResult]
+// CHECK:STDERR: fn H[W:! type](v: W) -> W.(I.T) {
+// CHECK:STDERR:                         ^~~~~~~
 fn H[W:! type](v: W) -> W.(I.T) {
   return v.(I.F)();
 }
@@ -34,12 +37,46 @@ fn G(p: C*) -> () {
   return H(p);
 }
 
-// TODO: Diagnose this as a poisoned specialization.
+// CHECK:STDERR: fail_final_poisoned_concrete_query_in_specific.carbon:[[@LINE+7]]:1: note: the use would select the `impl` here but it was not found yet [PoisonedImplLookupConcreteResultNoteBadImpl]
+// CHECK:STDERR: impl C* as I where .T = C {
+// CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR: fail_final_poisoned_concrete_query_in_specific.carbon:[[@LINE-21]]:1: note: the use had selected the `impl` here [PoisonedImplLookupConcreteResultNotePreviousImpl]
+// CHECK:STDERR: impl forall [U:! type] U as I where .T = () {
+// CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR:
 impl C* as I where .T = C {
   fn F[self: Self]() -> C { return *self; }
 }
 
-// --- todo_fail_final_poisoned_concrete_query_nested_type_in_self.carbon
+// --- fail_final_poisoned_concrete_query_in_generic.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let T:! type;
+}
+
+impl forall [U:! type] U as I where .T = () {}
+
+class C {}
+
+fn H[W:! type](v: W) {
+  // This concrete impl lookup query poisons any further specializations.
+  // CHECK:STDERR: fail_final_poisoned_concrete_query_in_generic.carbon:[[@LINE+3]]:10: error: found `impl` that would change the result of an earlier use of `C as I` [PoisonedImplLookupConcreteResult]
+  // CHECK:STDERR:   let a: C.(I.T) = ();
+  // CHECK:STDERR:          ^~~~~~~
+  let a: C.(I.T) = ();
+}
+
+// CHECK:STDERR: fail_final_poisoned_concrete_query_in_generic.carbon:[[@LINE+7]]:1: note: the use would select the `impl` here but it was not found yet [PoisonedImplLookupConcreteResultNoteBadImpl]
+// CHECK:STDERR: impl C as I where .T = C {}
+// CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR: fail_final_poisoned_concrete_query_in_generic.carbon:[[@LINE-15]]:1: note: the use had selected the `impl` here [PoisonedImplLookupConcreteResultNotePreviousImpl]
+// CHECK:STDERR: impl forall [U:! type] U as I where .T = () {}
+// CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR:
+impl C as I where .T = C {}
+
+// --- fail_final_poisoned_concrete_query_nested_type_in_self.carbon
 library "[[@TEST_NAME]]";
 
 interface I {
@@ -55,15 +92,24 @@ impl forall [U:! type] C(U) as I where .T = () {
 
 fn G(c: C(())) -> () {
   // This concrete impl lookup query poisons any further specializations.
+  // CHECK:STDERR: fail_final_poisoned_concrete_query_nested_type_in_self.carbon:[[@LINE+3]]:10: error: found `impl` that would change the result of an earlier use of `C(()) as I` [PoisonedImplLookupConcreteResult]
+  // CHECK:STDERR:   return c.(I.F)();
+  // CHECK:STDERR:          ^~~~~~~
   return c.(I.F)();
 }
 
-// TODO: Diagnose this as a poisoned specialization.
+// CHECK:STDERR: fail_final_poisoned_concrete_query_nested_type_in_self.carbon:[[@LINE+7]]:1: note: the use would select the `impl` here but it was not found yet [PoisonedImplLookupConcreteResultNoteBadImpl]
+// CHECK:STDERR: impl C(()) as I where .T = {} {
+// CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR: fail_final_poisoned_concrete_query_nested_type_in_self.carbon:[[@LINE-15]]:1: note: the use had selected the `impl` here [PoisonedImplLookupConcreteResultNotePreviousImpl]
+// CHECK:STDERR: impl forall [U:! type] C(U) as I where .T = () {
+// CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR:
 impl C(()) as I where .T = {} {
   fn F[self: Self]() -> {} { return {}; }
 }
 
-// --- todo_fail_final_poisoned_concrete_query_nested_type_in_interface.carbon
+// --- fail_final_poisoned_concrete_query_nested_type_in_interface.carbon
 library "[[@TEST_NAME]]";
 
 interface I(U:! type) {
@@ -79,10 +125,19 @@ class C {}
 
 fn G(c: C) -> () {
   // This concrete impl lookup query poisons any further specializations.
+  // CHECK:STDERR: fail_final_poisoned_concrete_query_nested_type_in_interface.carbon:[[@LINE+3]]:10: error: found `impl` that would change the result of an earlier use of `C as I(C)` [PoisonedImplLookupConcreteResult]
+  // CHECK:STDERR:   return c.(I(C).F)();
+  // CHECK:STDERR:          ^~~~~~~~~~
   return c.(I(C).F)();
 }
 
-// TODO: Diagnose this as a poisoned specialization.
+// CHECK:STDERR: fail_final_poisoned_concrete_query_nested_type_in_interface.carbon:[[@LINE+7]]:1: note: the use would select the `impl` here but it was not found yet [PoisonedImplLookupConcreteResultNoteBadImpl]
+// CHECK:STDERR: impl C as I(C) where .T = {} {
+// CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR: fail_final_poisoned_concrete_query_nested_type_in_interface.carbon:[[@LINE-17]]:1: note: the use had selected the `impl` here [PoisonedImplLookupConcreteResultNotePreviousImpl]
+// CHECK:STDERR: impl forall [U:! type] U as I(U) where .T = () {
+// CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR:
 impl C as I(C) where .T = {} {
   fn F[self: Self]() -> {} { return {}; }
 }
@@ -114,3 +169,62 @@ fn G[X:! type](p: X*) -> (X*).(I.T) {
 final impl forall [V:! type] V* as I where .T = V {
   fn F[self: Self]() -> V { return *self; }
 }
+
+// --- todo_final_overlaps_earlier_non_final_impl.carbon
+library "[[@TEST_NAME]]";
+
+interface Z(T:! type) {}
+interface Y {}
+
+impl forall [T:! Y] T as Z(T) {}
+
+// TODO: Diagnose overlap with previous impl (query of this matches that).
+final impl forall [T:! type] T as Z(T) {}
+
+// --- todo_final_overlaps_later_non_final_impl.carbon
+library "[[@TEST_NAME]]";
+
+interface Z(T:! type) {}
+interface Y {}
+
+// TODO: Diagnose overlap with next impl (query of this matches that).
+final impl forall [T:! type] T as Z(T) {}
+
+impl forall [T:! Y] T as Z(T) {}
+
+// --- todo_final_overlaps_earlier_final_impl.carbon
+library "[[@TEST_NAME]]";
+
+interface Z(T:! type) {}
+interface Y {}
+
+final impl forall [T:! Y] T as Z(T) {}
+
+// TODO: Diagnose overlap with previous impl (query of this matches that).
+final impl forall [T:! type] T as Z(T) {}
+
+// --- todo_final_overlaps_later_final_impl.carbon
+library "[[@TEST_NAME]]";
+
+interface Z(T:! type) {}
+interface Y {}
+
+// TODO: Diagnose overlap with next impl (query of this matches that)
+final impl forall [T:! type] T as Z(T) {}
+
+final impl forall [T:! Y] T as Z(T) {}
+
+// --- todo_non_final_overlaps_non_final_impl.carbon
+library "[[@TEST_NAME]]";
+
+interface Z(T:! type) {}
+interface Y {}
+
+impl forall [T:! Y] T as Z(T) {}
+
+class C(T:! type) {}
+// No diagnosis here as the type structure is unique.
+impl forall [T:! type] T as Z(C(T)) {}
+
+// TODO: Diagnose overlap with first impl (same type structure).
+impl forall [T:! type] T as Z(T) {}

toolchain/diagnostics/diagnostic_kind.def

@@ -315,6 +315,9 @@ CARBON_DIAGNOSTIC_KIND(ImplUnusedBinding)
 // Impl lookup.
 CARBON_DIAGNOSTIC_KIND(MissingImplInMemberAccess)
 CARBON_DIAGNOSTIC_KIND(MissingImplInMemberAccessNote)
+CARBON_DIAGNOSTIC_KIND(PoisonedImplLookupConcreteResult)
+CARBON_DIAGNOSTIC_KIND(PoisonedImplLookupConcreteResultNoteBadImpl)
+CARBON_DIAGNOSTIC_KIND(PoisonedImplLookupConcreteResultNotePreviousImpl)
 
 // Let declaration checking.
 CARBON_DIAGNOSTIC_KIND(ExpectedInitializerAfterLet)

toolchain/sem_ir/ids.h

@@ -317,6 +317,8 @@ struct IdentifiedFacetTypeId : public IdBase<IdentifiedFacetTypeId> {
 
 // The ID of an impl.
 struct ImplId : public IdBase<ImplId> {
+  using DiagnosticType = Diagnostics::TypeInfo<std::string>;
+
   static constexpr llvm::StringLiteral Label = "impl";
   using ValueType = Impl;
 
@@ -344,6 +346,8 @@ struct SpecificId : public IdBase<SpecificId> {
 
 // The ID of a SpecificInterface, which is an interface and a specific pair.
 struct SpecificInterfaceId : public IdBase<SpecificInterfaceId> {
+  using DiagnosticType = Diagnostics::TypeInfo<std::string>;
+
   static constexpr llvm::StringLiteral Label = "specific_interface";
   using ValueType = SpecificInterface;
 
@@ -1006,6 +1010,8 @@ struct AnyRawId : public AnyIdBase {
 
 // A pair of an interface and a specific for that interface.
 struct SpecificInterface {
+  using DiagnosticType = Diagnostics::TypeInfo<std::string>;
+
   InterfaceId interface_id;
   SpecificId specific_id;
 

toolchain/sem_ir/stringify.cpp

@@ -723,4 +723,16 @@ auto StringifySpecific(const File& sem_ir, SpecificId specific_id)
   return Stringify(sem_ir, step_stack);
 }
 
+auto StringifySpecificInterface(const File& sem_ir,
+                                SpecificInterface specific_interface)
+    -> std::string {
+  if (specific_interface.specific_id.has_value()) {
+    return StringifySpecific(sem_ir, specific_interface.specific_id);
+  } else {
+    auto name_id =
+        sem_ir.interfaces().Get(specific_interface.interface_id).name_id;
+    return sem_ir.names().GetFormatted(name_id).str();
+  }
+}
+
 }  // namespace Carbon::SemIR

toolchain/sem_ir/stringify.h

@@ -25,6 +25,15 @@ auto StringifyConstantInst(const File& sem_ir, InstId outer_inst_id)
 auto StringifySpecific(const File& sem_ir, SpecificId specific_id)
     -> std::string;
 
+// Produces a string version of the name of a specific interface. If the
+// interface is not generic, this is just the name of the interface. Otheewise,
+// it is the interface name and its generic arguments.  Generally, this should
+// not be called directly. To format a string into a diagnostic, use a
+// diagnostic parameter of type `SpecificInterface`.
+auto StringifySpecificInterface(const File& sem_ir,
+                                SpecificInterface specific_interface)
+    -> std::string;
+
 }  // namespace Carbon::SemIR
 
 #endif  // CARBON_TOOLCHAIN_SEM_IR_STRINGIFY_H_