diff --git a/toolchain/base/value_store.h b/toolchain/base/value_store.h
index 3d69304033533..2e6851fff43fc 100644
--- a/toolchain/base/value_store.h
+++ b/toolchain/base/value_store.h
@@ -146,6 +146,9 @@ class CanonicalValueStore {
   // Returns the value for an ID.
   auto Get(IdT id) const -> ConstRefType { return values_.Get(id); }
 
+  // Returns the value for an ID. Changes should not affect hash or ==.
+  auto GetMutable(IdT id) -> RefType { return values_.Get(id); }
+
   // Looks up the canonical ID for a value, or returns `None` if not in the
   // store.
   auto Lookup(ValueType value) const -> IdT;
diff --git a/toolchain/check/BUILD b/toolchain/check/BUILD
index f07994f3e7c3d..9ff786751c9d2 100644
--- a/toolchain/check/BUILD
+++ b/toolchain/check/BUILD
@@ -22,6 +22,7 @@ cc_library(
         "decl_name_stack.cpp",
         "deduce.cpp",
         "eval.cpp",
+        "facet_type.cpp",
         "function.cpp",
         "generic.cpp",
         "global_init.cpp",
@@ -56,6 +57,7 @@ cc_library(
         "deduce.h",
         "diagnostic_helpers.h",
         "eval.h",
+        "facet_type.h",
         "function.h",
         "generic.h",
         "global_init.h",
diff --git a/toolchain/check/call.cpp b/toolchain/check/call.cpp
index 5916c4ddc5a2c..db1f7334c4c80 100644
--- a/toolchain/check/call.cpp
+++ b/toolchain/check/call.cpp
@@ -8,6 +8,7 @@
 #include "toolchain/check/context.h"
 #include "toolchain/check/convert.h"
 #include "toolchain/check/deduce.h"
+#include "toolchain/check/facet_type.h"
 #include "toolchain/check/function.h"
 #include "toolchain/check/type.h"
 #include "toolchain/diagnostics/format_providers.h"
diff --git a/toolchain/check/context.cpp b/toolchain/check/context.cpp
index 5f2150fdfce54..ffaaf026593d1 100644
--- a/toolchain/check/context.cpp
+++ b/toolchain/check/context.cpp
@@ -11,6 +11,7 @@
 #include "common/check.h"
 #include "common/vlog.h"
 #include "llvm/ADT/Sequence.h"
+#include "toolchain/check/convert.h"
 #include "toolchain/check/decl_name_stack.h"
 #include "toolchain/check/eval.h"
 #include "toolchain/check/generic.h"
@@ -18,6 +19,7 @@
 #include "toolchain/check/import.h"
 #include "toolchain/check/import_ref.h"
 #include "toolchain/check/inst_block_stack.h"
+#include "toolchain/check/interface.h"
 #include "toolchain/check/merge.h"
 #include "toolchain/check/type_completion.h"
 #include "toolchain/diagnostics/diagnostic_emitter.h"
diff --git a/toolchain/check/context.h b/toolchain/check/context.h
index c3d62edb337d1..28b4477eae30a 100644
--- a/toolchain/check/context.h
+++ b/toolchain/check/context.h
@@ -224,6 +224,9 @@ class Context {
   auto facet_types() -> CanonicalValueStore<SemIR::FacetTypeId>& {
     return sem_ir().facet_types();
   }
+  auto complete_facet_types() -> ValueStore<SemIR::CompleteFacetTypeId>& {
+    return sem_ir().complete_facet_types();
+  }
   auto impls() -> SemIR::ImplStore& { return sem_ir().impls(); }
   auto generics() -> SemIR::GenericStore& { return sem_ir().generics(); }
   auto specifics() -> SemIR::SpecificStore& { return sem_ir().specifics(); }
diff --git a/toolchain/check/dump.cpp b/toolchain/check/dump.cpp
index ff8678b89e053..e25fe98fe5416 100644
--- a/toolchain/check/dump.cpp
+++ b/toolchain/check/dump.cpp
@@ -132,6 +132,12 @@ LLVM_DUMP_METHOD static auto Dump(const Context& context,
   SemIR::Dump(context.sem_ir(), name_scope_id);
 }
 
+LLVM_DUMP_METHOD static auto Dump(
+    const Context& context, SemIR::CompleteFacetTypeId complete_facet_type_id)
+    -> void {
+  SemIR::Dump(context.sem_ir(), complete_facet_type_id);
+}
+
 LLVM_DUMP_METHOD static auto Dump(const Context& context,
                                   SemIR::SpecificId specific_id) -> void {
   SemIR::Dump(context.sem_ir(), specific_id);
diff --git a/toolchain/check/eval.cpp b/toolchain/check/eval.cpp
index 0d87c67e01ea5..367d9785a0600 100644
--- a/toolchain/check/eval.cpp
+++ b/toolchain/check/eval.cpp
@@ -6,6 +6,7 @@
 
 #include "toolchain/base/kind_switch.h"
 #include "toolchain/check/diagnostic_helpers.h"
+#include "toolchain/check/facet_type.h"
 #include "toolchain/check/generic.h"
 #include "toolchain/check/import_ref.h"
 #include "toolchain/check/type.h"
@@ -462,19 +463,27 @@ static auto GetConstantValue(EvalContext& eval_context,
 static auto GetConstantFacetTypeInfo(EvalContext& eval_context,
                                      SemIR::FacetTypeId facet_type_id,
                                      Phase* phase) -> SemIR::FacetTypeInfo {
-  SemIR::FacetTypeInfo info = eval_context.facet_types().Get(facet_type_id);
-  for (auto& interface : info.impls_constraints) {
-    interface.specific_id =
-        GetConstantValue(eval_context, interface.specific_id, phase);
-  }
-  for (auto& rewrite : info.rewrite_constraints) {
-    rewrite.lhs_const_id = eval_context.GetInContext(rewrite.lhs_const_id);
-    rewrite.rhs_const_id = eval_context.GetInContext(rewrite.rhs_const_id);
+  const auto& orig = eval_context.facet_types().Get(facet_type_id);
+  SemIR::FacetTypeInfo info;
+  info.impls_constraints.reserve(orig.impls_constraints.size());
+  for (const auto& interface : orig.impls_constraints) {
+    info.impls_constraints.push_back(
+        {.interface_id = interface.interface_id,
+         .specific_id =
+             GetConstantValue(eval_context, interface.specific_id, phase)});
+  }
+  info.rewrite_constraints.reserve(orig.rewrite_constraints.size());
+  for (const auto& rewrite : orig.rewrite_constraints) {
+    auto lhs_const_id = eval_context.GetInContext(rewrite.lhs_const_id);
+    auto rhs_const_id = eval_context.GetInContext(rewrite.rhs_const_id);
     // `where` requirements using `.Self` should not be considered symbolic
-    UpdatePhaseIgnorePeriodSelf(eval_context, rewrite.lhs_const_id, phase);
-    UpdatePhaseIgnorePeriodSelf(eval_context, rewrite.rhs_const_id, phase);
+    UpdatePhaseIgnorePeriodSelf(eval_context, lhs_const_id, phase);
+    UpdatePhaseIgnorePeriodSelf(eval_context, rhs_const_id, phase);
+    info.rewrite_constraints.push_back(
+        {.lhs_const_id = lhs_const_id, .rhs_const_id = rhs_const_id});
   }
   // TODO: Process other requirements.
+  info.other_requirements = orig.other_requirements;
   return info;
 }
 
diff --git a/toolchain/check/facet_type.cpp b/toolchain/check/facet_type.cpp
new file mode 100644
index 0000000000000..d50d58bac602c
--- /dev/null
+++ b/toolchain/check/facet_type.cpp
@@ -0,0 +1,188 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#include "toolchain/check/facet_type.h"
+
+#include "toolchain/check/convert.h"
+#include "toolchain/check/import_ref.h"
+#include "toolchain/check/inst.h"
+#include "toolchain/check/interface.h"
+#include "toolchain/check/type.h"
+
+namespace Carbon::Check {
+
+auto FacetTypeFromInterface(Context& context, SemIR::InterfaceId interface_id,
+                            SemIR::SpecificId specific_id) -> SemIR::FacetType {
+  SemIR::FacetTypeId facet_type_id = context.facet_types().Add(
+      SemIR::FacetTypeInfo{.impls_constraints = {{interface_id, specific_id}},
+                           .other_requirements = false});
+  return {.type_id = SemIR::TypeType::SingletonTypeId,
+          .facet_type_id = facet_type_id};
+}
+
+// Returns `true` if the `FacetAccessWitness` of `witness_id` matches
+// `interface`.
+static auto WitnessAccessMatchesInterface(
+    Context& context, SemIR::InstId witness_id,
+    const SemIR::SpecificInterface& interface) -> bool {
+  auto access = context.insts().GetAs<SemIR::FacetAccessWitness>(witness_id);
+  auto type_id = context.insts().Get(access.facet_value_inst_id).type_id();
+  auto facet_type = context.types().GetAs<SemIR::FacetType>(type_id);
+  const auto& facet_info = context.facet_types().Get(facet_type.facet_type_id);
+  if (auto impls = facet_info.TryAsSingleInterface()) {
+    return impls->interface_id == interface.interface_id &&
+           impls->specific_id == interface.specific_id;
+  }
+  return false;
+}
+
+auto ResolveFacetTypeImplWitness(
+    Context& context, SemIR::LocId witness_loc_id,
+    SemIR::InstId facet_type_inst_id, SemIR::InstId self_type_inst_id,
+    const SemIR::SpecificInterface& interface_to_witness,
+    SemIR::SpecificId self_specific_id) -> SemIR::InstId {
+  // TODO: Finish facet type resolution. This code currently only handles
+  // rewrite constraints that set associated constants to a concrete value.
+  // Need logic to topologically sort rewrites to respect dependencies, and
+  // afterwards reject duplicates that are not identical.
+
+  const auto& interface =
+      context.interfaces().Get(interface_to_witness.interface_id);
+  auto assoc_entities =
+      context.inst_blocks().Get(interface.associated_entities_id);
+  // TODO: When this function is used for things other than just impls, may want
+  // to only load the specific associated entities that are mentioned in rewrite
+  // rules.
+  for (auto decl_id : assoc_entities) {
+    LoadImportRef(context, decl_id);
+  }
+
+  SemIR::InstId witness_inst_id = SemIR::InstId::None;
+  llvm::MutableArrayRef<SemIR::InstId> table;
+  {
+    llvm::SmallVector<SemIR::InstId> empty_table(assoc_entities.size(),
+                                                 SemIR::InstId::None);
+    auto table_id = context.inst_blocks().Add(empty_table);
+    table = context.inst_blocks().GetMutable(table_id);
+    witness_inst_id = AddInst<SemIR::ImplWitness>(
+        context, witness_loc_id,
+        {.type_id =
+             GetSingletonType(context, SemIR::WitnessType::SingletonInstId),
+         .elements_id = table_id,
+         .specific_id = self_specific_id});
+  }
+
+  auto facet_type_id =
+      context.types().GetTypeIdForTypeInstId(facet_type_inst_id);
+  CARBON_CHECK(facet_type_id != SemIR::ErrorInst::SingletonTypeId);
+  auto facet_type = context.types().GetAs<SemIR::FacetType>(facet_type_id);
+  // TODO: This is currently a copy because I'm not sure whether anything could
+  // cause the facet type store to resize before we are done with it.
+  auto facet_type_info = context.facet_types().Get(facet_type.facet_type_id);
+
+  for (auto rewrite : facet_type_info.rewrite_constraints) {
+    auto inst_id = context.constant_values().GetInstId(rewrite.lhs_const_id);
+    auto access = context.insts().GetAs<SemIR::ImplWitnessAccess>(inst_id);
+    if (!WitnessAccessMatchesInterface(context, access.witness_id,
+                                       interface_to_witness)) {
+      continue;
+    }
+    auto& table_entry = table[access.index.index];
+    if (table_entry == SemIR::ErrorInst::SingletonInstId) {
+      // Don't overwrite an error value. This prioritizes not generating
+      // multiple errors for one associated constant over picking a value
+      // for it to use to attempt recovery.
+      continue;
+    }
+    auto rewrite_value = rewrite.rhs_const_id;
+
+    if (table_entry.has_value()) {
+      auto const_id = context.constant_values().Get(table_entry);
+      if (const_id != rewrite_value &&
+          rewrite_value != SemIR::ErrorInst::SingletonConstantId) {
+        table_entry = SemIR::ErrorInst::SingletonInstId;
+        // TODO: Figure out how to print the two different values
+        // `const_id` & `rewrite_value` in the diagnostic
+        // message.
+        CARBON_DIAGNOSTIC(AssociatedConstantWithDifferentValues, Error,
+                          "associated constant {0} given two different values",
+                          SemIR::NameId);
+        auto decl_id = assoc_entities[access.index.index];
+        SemIR::NameId name_id = SemIR::NameId::None;
+        if (auto decl = context.insts().TryGetAs<SemIR::AssociatedConstantDecl>(
+                decl_id)) {
+          auto& assoc_const =
+              context.associated_constants().Get(decl->assoc_const_id);
+          name_id = assoc_const.name_id;
+        } else {
+          auto import_ref = context.insts().GetAs<SemIR::AnyImportRef>(decl_id);
+          const auto& entity_name =
+              context.entity_names().Get(import_ref.entity_name_id);
+          name_id = entity_name.name_id;
+        }
+        context.emitter().Emit(facet_type_inst_id,
+                               AssociatedConstantWithDifferentValues, name_id);
+      }
+      continue;
+    }
+    auto decl_id = context.constant_values().GetConstantInstId(
+        assoc_entities[access.index.index]);
+    CARBON_CHECK(decl_id.has_value(), "Non-constant associated entity");
+    if (auto decl =
+            context.insts().TryGetAs<SemIR::AssociatedConstantDecl>(decl_id)) {
+      // If the associated constant has a symbolic type, convert the rewrite
+      // value to that type now we know the value of `Self`.
+      SemIR::TypeId assoc_const_type_id = decl->type_id;
+      if (context.types().GetConstantId(assoc_const_type_id).is_symbolic()) {
+        // Get the type of the associated constant in this interface with this
+        // value for `Self`.
+        assoc_const_type_id = GetTypeForSpecificAssociatedEntity(
+            context, facet_type_inst_id, interface_to_witness.specific_id,
+            decl_id, context.types().GetTypeIdForTypeInstId(self_type_inst_id),
+            witness_inst_id);
+        // Perform the conversion of the value to the type. We skipped this when
+        // forming the facet type because the type of the associated constant
+        // was symbolic.
+        auto converted_inst_id = ConvertToValueOfType(
+            context, context.insts().GetLocId(facet_type_inst_id),
+            context.constant_values().GetInstId(rewrite_value),
+            assoc_const_type_id);
+        rewrite_value = context.constant_values().Get(converted_inst_id);
+        // The result of conversion can be non-constant even if the original
+        // value was constant.
+        if (!rewrite_value.is_constant() &&
+            rewrite_value != SemIR::ErrorInst::SingletonConstantId) {
+          const auto& assoc_const =
+              context.associated_constants().Get(decl->assoc_const_id);
+          CARBON_DIAGNOSTIC(
+              AssociatedConstantNotConstantAfterConversion, Error,
+              "associated constant {0} given value that is not constant "
+              "after conversion to {1}",
+              SemIR::NameId, SemIR::TypeId);
+          context.emitter().Emit(facet_type_inst_id,
+                                 AssociatedConstantNotConstantAfterConversion,
+                                 assoc_const.name_id, assoc_const_type_id);
+          rewrite_value = SemIR::ErrorInst::SingletonConstantId;
+        }
+      }
+    } else {
+      if (decl_id != SemIR::ErrorInst::SingletonInstId) {
+        auto type_id = context.insts().Get(decl_id).type_id();
+        auto type_inst = context.types().GetAsInst(type_id);
+        auto fn_type = type_inst.As<SemIR::FunctionType>();
+        const auto& fn = context.functions().Get(fn_type.function_id);
+        CARBON_DIAGNOSTIC(RewriteForAssociatedFunction, Error,
+                          "rewrite specified for associated function {0}",
+                          SemIR::NameId);
+        context.emitter().Emit(facet_type_inst_id, RewriteForAssociatedFunction,
+                               fn.name_id);
+      }
+      continue;
+    }
+    table_entry = context.constant_values().GetInstId(rewrite_value);
+  }
+  return witness_inst_id;
+}
+
+}  // namespace Carbon::Check
diff --git a/toolchain/check/facet_type.h b/toolchain/check/facet_type.h
new file mode 100644
index 0000000000000..810983310cef4
--- /dev/null
+++ b/toolchain/check/facet_type.h
@@ -0,0 +1,45 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#ifndef CARBON_TOOLCHAIN_CHECK_FACET_TYPE_H_
+#define CARBON_TOOLCHAIN_CHECK_FACET_TYPE_H_
+
+#include "toolchain/check/context.h"
+#include "toolchain/sem_ir/ids.h"
+
+namespace Carbon::Check {
+
+// Create a FacetType typed instruction object consisting of a single
+// interface. The `specific_id` specifies arguments in the case the interface is
+// generic.
+auto FacetTypeFromInterface(Context& context, SemIR::InterfaceId interface_id,
+                            SemIR::SpecificId specific_id) -> SemIR::FacetType;
+
+// Adds and returns an `ImplWitness` instruction (created with location set to
+// `witness_loc_id`) that shows "`Self` type" of type "facet type" (the value of
+// the `facet_type_inst_id` instruction) implements interface
+// `interface_to_witness`, which must be an interface required by "facet type"
+// (as determined by `RequireCompleteFacetType`). This witness reflects the
+// values assigned to associated constant members of that interface by rewrite
+// constraints in the facet type. `self_specific_id` will be the `specific_id`
+// of the resulting witness.
+//
+// `self_type_inst_id` is an instruction that evaluates to the `Self` type of
+// the facet type. For example, in `T:! X where ...`, we will bind the `.Self`
+// of the `where` facet type to `T`, and in `(X where ...) where ...`, we will
+// bind the inner `.Self` to the outer `.Self`.
+//
+// If the facet type contains a rewrite, we may have deferred converting the
+// rewritten value to the type of the associated constant. That conversion
+// will also be performed as part of resolution, and may depend on the
+// `Self` type.
+auto ResolveFacetTypeImplWitness(
+    Context& context, SemIR::LocId witness_loc_id,
+    SemIR::InstId facet_type_inst_id, SemIR::InstId self_type_inst_id,
+    const SemIR::SpecificInterface& interface_to_witness,
+    SemIR::SpecificId self_specific_id) -> SemIR::InstId;
+
+}  // namespace Carbon::Check
+
+#endif  // CARBON_TOOLCHAIN_CHECK_FACET_TYPE_H_
diff --git a/toolchain/check/handle_impl.cpp b/toolchain/check/handle_impl.cpp
index 80856d073b3b9..013cd4b90f036 100644
--- a/toolchain/check/handle_impl.cpp
+++ b/toolchain/check/handle_impl.cpp
@@ -14,6 +14,7 @@
 #include "toolchain/check/name_lookup.h"
 #include "toolchain/check/pattern_match.h"
 #include "toolchain/check/type.h"
+#include "toolchain/check/type_completion.h"
 #include "toolchain/parse/typed_nodes.h"
 #include "toolchain/sem_ir/generic.h"
 #include "toolchain/sem_ir/ids.h"
@@ -299,6 +300,43 @@ static auto IsValidImplRedecl(Context& context, SemIR::Impl& new_impl,
   return true;
 }
 
+// Checks that the constraint specified for the impl is valid and complete.
+// Returns a pointer to the interface that the impl implements. On error,
+// issues a diagnostic and returns nullptr.
+static auto CheckConstraintIsInterface(Context& context,
+                                       const SemIR::Impl& impl)
+    -> const SemIR::CompleteFacetType::RequiredInterface* {
+  auto facet_type_id =
+      context.types().GetTypeIdForTypeInstId(impl.constraint_id);
+  if (facet_type_id == SemIR::ErrorInst::SingletonTypeId) {
+    return nullptr;
+  }
+  auto facet_type = context.types().TryGetAs<SemIR::FacetType>(facet_type_id);
+  if (!facet_type) {
+    CARBON_DIAGNOSTIC(ImplAsNonFacetType, Error, "impl as non-facet type {0}",
+                      InstIdAsType);
+    context.emitter().Emit(impl.latest_decl_id(), ImplAsNonFacetType,
+                           impl.constraint_id);
+    return nullptr;
+  }
+
+  auto complete_id = RequireCompleteFacetType(
+      context, facet_type_id, context.insts().GetLocId(impl.constraint_id),
+      *facet_type, FacetTypeImpl);
+  if (!complete_id.has_value()) {
+    return nullptr;
+  }
+  const auto& complete = context.complete_facet_types().Get(complete_id);
+  if (complete.num_to_impl != 1) {
+    CARBON_DIAGNOSTIC(ImplOfNotOneInterface, Error,
+                      "impl as {0} interfaces, expected 1", int);
+    context.emitter().Emit(impl.latest_decl_id(), ImplOfNotOneInterface,
+                           complete.num_to_impl);
+    return nullptr;
+  }
+  return &complete.required_interfaces.front();
+}
+
 // Build an ImplDecl describing the signature of an impl. This handles the
 // common logic shared by impl forward declarations and impl definitions.
 static auto BuildImplDecl(Context& context, Parse::AnyImplDeclId node_id,
@@ -314,15 +352,8 @@ static auto BuildImplDecl(Context& context, Parse::AnyImplDeclId node_id,
   auto decl_block_id = context.inst_block_stack().Pop();
 
   // Convert the constraint expression to a type.
-  // TODO: Check that its constant value is a constraint.
   auto [constraint_inst_id, constraint_type_id] =
       ExprAsType(context, constraint_node, constraint_id);
-  // TODO: Do facet type resolution here, and enforce that the constraint
-  // extends a single interface.
-  // TODO: Determine `interface_id` and `specific_id` once and save it in the
-  // resolved facet type, instead of in multiple functions called below.
-  // TODO: Skip work below if facet type resolution fails, so we don't have a
-  // valid/non-error `interface_id` at all.
 
   // Process modifiers.
   // TODO: Should we somehow permit access specifiers on `impl`s?
@@ -344,11 +375,18 @@ static auto BuildImplDecl(Context& context, Parse::AnyImplDeclId node_id,
   auto impl_decl_id =
       AddPlaceholderInst(context, SemIR::LocIdAndInst(node_id, impl_decl));
 
-  SemIR::Impl impl_info = {
-      name_context.MakeEntityWithParamsBase(name, impl_decl_id,
-                                            /*is_extern=*/false,
-                                            SemIR::LibraryNameId::None),
-      {.self_id = self_inst_id, .constraint_id = constraint_inst_id}};
+  SemIR::Impl impl_info = {name_context.MakeEntityWithParamsBase(
+                               name, impl_decl_id,
+                               /*is_extern=*/false, SemIR::LibraryNameId::None),
+                           {.self_id = self_inst_id,
+                            .constraint_id = constraint_inst_id,
+                            .interface = SemIR::SpecificInterface::None}};
+
+  const SemIR::CompleteFacetType::RequiredInterface* required_interface =
+      CheckConstraintIsInterface(context, impl_info);
+  if (required_interface) {
+    impl_info.interface = *required_interface;
+  }
 
   // Add the impl declaration.
   bool invalid_redeclaration = false;
@@ -371,9 +409,15 @@ static auto BuildImplDecl(Context& context, Parse::AnyImplDeclId node_id,
   // Create a new impl if this isn't a valid redeclaration.
   if (!impl_decl.impl_id.has_value()) {
     impl_info.generic_id = BuildGeneric(context, impl_decl_id);
-    impl_info.witness_id = ImplWitnessForDeclaration(context, impl_info);
-    AddConstantsToImplWitnessFromConstraint(context, impl_info,
-                                            impl_info.witness_id);
+    if (required_interface) {
+      impl_info.witness_id = ImplWitnessForDeclaration(context, impl_info);
+    } else {
+      impl_info.witness_id = SemIR::ErrorInst::SingletonInstId;
+      // TODO: We might also want to mark that the name scope for the impl has
+      // an error -- at least once we start making name lookups within the impl
+      // also look into the facet (eg, so you can name associated constants from
+      // within the impl).
+    }
     FinishGenericDecl(context, impl_decl_id, impl_info.generic_id);
     impl_decl.impl_id = context.impls().Add(impl_info);
     lookup_bucket_ref.push_back(impl_decl.impl_id);
diff --git a/toolchain/check/handle_interface.cpp b/toolchain/check/handle_interface.cpp
index 0823f6474defb..cefdd20f3cd7c 100644
--- a/toolchain/check/handle_interface.cpp
+++ b/toolchain/check/handle_interface.cpp
@@ -4,6 +4,7 @@
 
 #include "toolchain/check/context.h"
 #include "toolchain/check/eval.h"
+#include "toolchain/check/facet_type.h"
 #include "toolchain/check/generic.h"
 #include "toolchain/check/handle.h"
 #include "toolchain/check/inst.h"
diff --git a/toolchain/check/handle_where.cpp b/toolchain/check/handle_where.cpp
index 52a228102f3d2..ed07db95e2645 100644
--- a/toolchain/check/handle_where.cpp
+++ b/toolchain/check/handle_where.cpp
@@ -66,12 +66,10 @@ auto HandleParseNode(Context& context, Parse::RequirementEqualId node_id)
     // If the type of the associated constant is symbolic, we defer conversion
     // until the constraint is resolved, in case it depends on `Self` (which
     // will now be a reference to `.Self`).
-    // TODO: It would be simpler to always defer this conversion until the
-    // constraint is resolved.
     // For now we convert to a value expression eagerly because otherwise we'll
     // often be unable to constant-evaluate the enclosing `where` expression.
-    // TODO: Find another way to handle this that allows us to only convert the
-    // RHS once.
+    // TODO: Perform the conversion symbolically and add an implicit constraint
+    // that this conversion is valid and produces a constant.
     rhs_id = ConvertToValueExpr(context, rhs_id);
   } else {
     rhs_id = ConvertToValueOfType(context, rhs_node, rhs_id,
@@ -116,6 +114,8 @@ auto HandleParseNode(Context& context, Parse::RequirementImplsId node_id)
     rhs_as_type.inst_id = SemIR::ErrorInst::SingletonInstId;
   }
   // TODO: Require that at least one side uses a designator.
+  // TODO: For things like `HashSet(.T) as type`, add an implied constraint
+  // that `.T impls Hash`.
 
   // Build up the list of arguments for the `WhereExpr` inst.
   context.args_type_info_stack().AddInstId(
diff --git a/toolchain/check/impl.cpp b/toolchain/check/impl.cpp
index 7fd2346fdb852..5cd024570f325 100644
--- a/toolchain/check/impl.cpp
+++ b/toolchain/check/impl.cpp
@@ -6,8 +6,8 @@
 
 #include "toolchain/base/kind_switch.h"
 #include "toolchain/check/context.h"
-#include "toolchain/check/convert.h"
 #include "toolchain/check/eval.h"
+#include "toolchain/check/facet_type.h"
 #include "toolchain/check/function.h"
 #include "toolchain/check/generic.h"
 #include "toolchain/check/import_ref.h"
@@ -91,198 +91,11 @@ auto ImplWitnessForDeclaration(Context& context, const SemIR::Impl& impl)
     // When 'impl as' is invalid, the self type is an error.
     return SemIR::ErrorInst::SingletonInstId;
   }
-  auto facet_type_id =
-      context.types().GetTypeIdForTypeInstId(impl.constraint_id);
-  if (facet_type_id == SemIR::ErrorInst::SingletonTypeId) {
-    return SemIR::ErrorInst::SingletonInstId;
-  }
-  auto facet_type = context.types().TryGetAs<SemIR::FacetType>(facet_type_id);
-  if (!facet_type) {
-    CARBON_DIAGNOSTIC(ImplAsNonFacetType, Error, "impl as non-facet type {0}",
-                      InstIdAsType);
-    context.emitter().Emit(impl.latest_decl_id(), ImplAsNonFacetType,
-                           impl.constraint_id);
-    return SemIR::ErrorInst::SingletonInstId;
-  }
-  const SemIR::FacetTypeInfo& facet_type_info =
-      context.facet_types().Get(facet_type->facet_type_id);
-
-  auto interface_type = facet_type_info.TryAsSingleInterface();
-  if (!interface_type) {
-    context.TODO(impl.latest_decl_id(), "impl as not 1 interface");
-    return SemIR::ErrorInst::SingletonInstId;
-  }
-  const auto& interface =
-      context.interfaces().Get(interface_type->interface_id);
-
-  // TODO: This should be done as part of facet type resolution.
-  if (!RequireDefinedType(context, facet_type_id,
-                          context.insts().GetLocId(impl.latest_decl_id()), [&] {
-                            CARBON_DIAGNOSTIC(
-                                ImplOfUndefinedInterface, Error,
-                                "implementation of undefined interface {0}",
-                                SemIR::NameId);
-                            return context.emitter().Build(
-                                impl.latest_decl_id(), ImplOfUndefinedInterface,
-                                interface.name_id);
-                          })) {
-    return SemIR::ErrorInst::SingletonInstId;
-  }
-
-  auto assoc_entities =
-      context.inst_blocks().Get(interface.associated_entities_id);
-  for (auto decl_id : assoc_entities) {
-    LoadImportRef(context, decl_id);
-  }
 
-  llvm::SmallVector<SemIR::InstId> table(assoc_entities.size(),
-                                         SemIR::InstId::None);
-  auto table_id = context.inst_blocks().Add(table);
-  return AddInst<SemIR::ImplWitness>(
+  return ResolveFacetTypeImplWitness(
       context, context.insts().GetLocId(impl.latest_decl_id()),
-      {.type_id =
-           GetSingletonType(context, SemIR::WitnessType::SingletonInstId),
-       .elements_id = table_id,
-       .specific_id = context.generics().GetSelfSpecific(impl.generic_id)});
-}
-
-// Returns `true` if the `FacetAccessWitness` of `witness_id` matches
-// `interface`.
-static auto WitnessAccessMatchesInterface(
-    Context& context, SemIR::InstId witness_id,
-    SemIR::FacetTypeInfo::ImplsConstraint interface) -> bool {
-  auto access = context.insts().GetAs<SemIR::FacetAccessWitness>(witness_id);
-  auto type_id = context.insts().Get(access.facet_value_inst_id).type_id();
-  auto facet_type = context.types().GetAs<SemIR::FacetType>(type_id);
-  const auto& facet_info = context.facet_types().Get(facet_type.facet_type_id);
-  if (auto impls = facet_info.TryAsSingleInterface()) {
-    return *impls == interface;
-  }
-  return false;
-}
-
-// TODO: Merge this function into `ImplWitnessForDeclaration`.
-auto AddConstantsToImplWitnessFromConstraint(Context& context,
-                                             const SemIR::Impl& impl,
-                                             SemIR::InstId witness_id) -> void {
-  CARBON_CHECK(!impl.has_definition_started());
-  CARBON_CHECK(witness_id.has_value());
-  if (witness_id == SemIR::ErrorInst::SingletonInstId) {
-    return;
-  }
-  auto facet_type_id =
-      context.types().GetTypeIdForTypeInstId(impl.constraint_id);
-  CARBON_CHECK(facet_type_id != SemIR::ErrorInst::SingletonTypeId);
-  auto facet_type = context.types().GetAs<SemIR::FacetType>(facet_type_id);
-  const SemIR::FacetTypeInfo& facet_type_info =
-      context.facet_types().Get(facet_type.facet_type_id);
-
-  auto interface_type = facet_type_info.TryAsSingleInterface();
-  CARBON_CHECK(interface_type.has_value());
-  const auto& interface =
-      context.interfaces().Get(interface_type->interface_id);
-
-  auto witness = context.insts().GetAs<SemIR::ImplWitness>(witness_id);
-  auto witness_block = context.inst_blocks().GetMutable(witness.elements_id);
-  auto assoc_entities =
-      context.inst_blocks().Get(interface.associated_entities_id);
-  CARBON_CHECK(witness_block.size() == assoc_entities.size());
-
-  // Scan through rewrites, produce map from element index to constant value.
-  // TODO: Perhaps move this into facet type resolution?
-  llvm::SmallVector<SemIR::ConstantId> rewrite_values(assoc_entities.size(),
-                                                      SemIR::ConstantId::None);
-  for (auto rewrite : facet_type_info.rewrite_constraints) {
-    auto inst_id = context.constant_values().GetInstId(rewrite.lhs_const_id);
-    auto access = context.insts().GetAs<SemIR::ImplWitnessAccess>(inst_id);
-    if (!WitnessAccessMatchesInterface(context, access.witness_id,
-                                       *interface_type)) {
-      // Skip rewrite constraints that apply to associated constants of
-      // a different interface than the one being implemented.
-      continue;
-    }
-    CARBON_CHECK(access.index.index >= 0);
-    CARBON_CHECK(access.index.index <
-                 static_cast<int32_t>(rewrite_values.size()));
-    auto& rewrite_value = rewrite_values[access.index.index];
-    if (rewrite_value.has_value() &&
-        rewrite_value != SemIR::ErrorInst::SingletonConstantId) {
-      if (rewrite_value != rewrite.rhs_const_id &&
-          rewrite.rhs_const_id != SemIR::ErrorInst::SingletonConstantId) {
-        // TODO: Do at least this checking as part of facet type resolution
-        // instead.
-
-        // TODO: Figure out how to print the two different values
-        // `rewrite_value` & `rewrite.rhs_const_id` in the diagnostic message.
-        CARBON_DIAGNOSTIC(AssociatedConstantWithDifferentValues, Error,
-                          "associated constant {0} given two different values",
-                          SemIR::NameId);
-        auto decl_id = context.constant_values().GetConstantInstId(
-            assoc_entities[access.index.index]);
-        CARBON_CHECK(decl_id.has_value(), "Non-constant associated entity");
-        auto decl =
-            context.insts().GetAs<SemIR::AssociatedConstantDecl>(decl_id);
-        context.emitter().Emit(
-            impl.constraint_id, AssociatedConstantWithDifferentValues,
-            context.associated_constants().Get(decl.assoc_const_id).name_id);
-      }
-    } else {
-      rewrite_value = rewrite.rhs_const_id;
-    }
-  }
-
-  // For each non-function associated constant, set the witness entry.
-  for (auto index : llvm::seq(assoc_entities.size())) {
-    auto decl_id =
-        context.constant_values().GetConstantInstId(assoc_entities[index]);
-    CARBON_CHECK(decl_id.has_value(), "Non-constant associated entity");
-    if (auto decl =
-            context.insts().TryGetAs<SemIR::AssociatedConstantDecl>(decl_id)) {
-      auto rewrite_value = rewrite_values[index];
-
-      // If the associated constant has a symbolic type, convert the rewrite
-      // value to that type now we know the value of `Self`.
-      SemIR::TypeId assoc_const_type_id = decl->type_id;
-      if (context.types().GetConstantId(assoc_const_type_id).is_symbolic()) {
-        // Get the type of the associated constant in this interface with this
-        // value for `Self`.
-        assoc_const_type_id = GetTypeForSpecificAssociatedEntity(
-            context, impl.constraint_id, interface_type->specific_id, decl_id,
-            context.types().GetTypeIdForTypeInstId(impl.self_id), witness_id);
-
-        // Perform the conversion of the value to the type. We skipped this when
-        // forming the facet type because the type of the associated constant
-        // was symbolic.
-        auto converted_inst_id = ConvertToValueOfType(
-            context, context.insts().GetLocId(impl.constraint_id),
-            context.constant_values().GetInstId(rewrite_value),
-            assoc_const_type_id);
-        rewrite_value = context.constant_values().Get(converted_inst_id);
-
-        // The result of conversion can be non-constant even if the original
-        // value was constant.
-        if (!rewrite_value.is_constant() &&
-            rewrite_value != SemIR::ErrorInst::SingletonConstantId) {
-          const auto& assoc_const =
-              context.associated_constants().Get(decl->assoc_const_id);
-          CARBON_DIAGNOSTIC(
-              AssociatedConstantNotConstantAfterConversion, Error,
-              "associated constant {0} given value that is not constant "
-              "after conversion to {1}",
-              SemIR::NameId, SemIR::TypeId);
-          context.emitter().Emit(impl.constraint_id,
-                                 AssociatedConstantNotConstantAfterConversion,
-                                 assoc_const.name_id, assoc_const_type_id);
-          rewrite_value = SemIR::ErrorInst::SingletonConstantId;
-        }
-      }
-
-      if (rewrite_value.has_value()) {
-        witness_block[index] =
-            context.constant_values().GetInstId(rewrite_value);
-      }
-    }
-  }
+      impl.constraint_id, impl.self_id, impl.interface,
+      context.generics().GetSelfSpecific(impl.generic_id));
 }
 
 auto ImplWitnessStartDefinition(Context& context, SemIR::Impl& impl) -> void {
@@ -291,21 +104,9 @@ auto ImplWitnessStartDefinition(Context& context, SemIR::Impl& impl) -> void {
   if (impl.witness_id == SemIR::ErrorInst::SingletonInstId) {
     return;
   }
-
-  auto facet_type_id =
-      context.types().GetTypeIdForTypeInstId(impl.constraint_id);
-  CARBON_CHECK(facet_type_id != SemIR::ErrorInst::SingletonTypeId);
-  auto facet_type = context.types().GetAs<SemIR::FacetType>(facet_type_id);
-  const SemIR::FacetTypeInfo& facet_type_info =
-      context.facet_types().Get(facet_type.facet_type_id);
-
-  auto interface_type = facet_type_info.TryAsSingleInterface();
-  CARBON_CHECK(interface_type.has_value());
-  const auto& interface =
-      context.interfaces().Get(interface_type->interface_id);
-
   auto witness = context.insts().GetAs<SemIR::ImplWitness>(impl.witness_id);
   auto witness_block = context.inst_blocks().GetMutable(witness.elements_id);
+  const auto& interface = context.interfaces().Get(impl.interface.interface_id);
   auto assoc_entities =
       context.inst_blocks().Get(interface.associated_entities_id);
   CARBON_CHECK(witness_block.size() == assoc_entities.size());
@@ -349,23 +150,11 @@ auto FinishImplWitness(Context& context, SemIR::Impl& impl) -> void {
   if (impl.witness_id == SemIR::ErrorInst::SingletonInstId) {
     return;
   }
-
-  auto facet_type_id =
-      context.types().GetTypeIdForTypeInstId(impl.constraint_id);
-  CARBON_CHECK(facet_type_id != SemIR::ErrorInst::SingletonTypeId);
-  auto facet_type = context.types().GetAs<SemIR::FacetType>(facet_type_id);
-  const SemIR::FacetTypeInfo& facet_type_info =
-      context.facet_types().Get(facet_type.facet_type_id);
-
-  auto interface_type = facet_type_info.TryAsSingleInterface();
-  CARBON_CHECK(interface_type.has_value());
-  const auto& interface =
-      context.interfaces().Get(interface_type->interface_id);
-
   auto witness = context.insts().GetAs<SemIR::ImplWitness>(impl.witness_id);
   auto witness_block = context.inst_blocks().GetMutable(witness.elements_id);
   auto& impl_scope = context.name_scopes().Get(impl.scope_id);
   auto self_type_id = context.types().GetTypeIdForTypeInstId(impl.self_id);
+  const auto& interface = context.interfaces().Get(impl.interface.interface_id);
   auto assoc_entities =
       context.inst_blocks().Get(interface.associated_entities_id);
   llvm::SmallVector<SemIR::InstId> used_decl_ids;
@@ -374,7 +163,7 @@ auto FinishImplWitness(Context& context, SemIR::Impl& impl) -> void {
     auto decl_id = assoc_entities[index];
     decl_id =
         context.constant_values().GetInstId(SemIR::GetConstantValueInSpecific(
-            context.sem_ir(), interface_type->specific_id, decl_id));
+            context.sem_ir(), impl.interface.specific_id, decl_id));
     CARBON_CHECK(decl_id.has_value(), "Non-constant associated entity");
     auto decl = context.insts().Get(decl_id);
     CARBON_KIND_SWITCH(decl) {
diff --git a/toolchain/check/impl.h b/toolchain/check/impl.h
index 7a513bab4b9e3..e8445e8f54ac9 100644
--- a/toolchain/check/impl.h
+++ b/toolchain/check/impl.h
@@ -14,10 +14,6 @@ namespace Carbon::Check {
 auto ImplWitnessForDeclaration(Context& context, const SemIR::Impl& impl)
     -> SemIR::InstId;
 
-auto AddConstantsToImplWitnessFromConstraint(Context& context,
-                                             const SemIR::Impl& impl,
-                                             SemIR::InstId witness_id) -> void;
-
 // Update `impl`'s witness at the start of a definition.
 auto ImplWitnessStartDefinition(Context& context, SemIR::Impl& impl) -> void;
 
diff --git a/toolchain/check/import_ref.cpp b/toolchain/check/import_ref.cpp
index 2cae7ae71f196..a7b2931b883a3 100644
--- a/toolchain/check/import_ref.cpp
+++ b/toolchain/check/import_ref.cpp
@@ -2081,6 +2081,7 @@ static auto MakeImplDeclaration(ImportContext& context,
       {GetIncompleteLocalEntityBase(context, impl_decl_id, import_impl),
        {.self_id = SemIR::InstId::None,
         .constraint_id = SemIR::InstId::None,
+        .interface = SemIR::SpecificInterface::None,
         .witness_id = witness_id}});
 
   // Write the impl ID into the ImplDecl.
@@ -2120,6 +2121,49 @@ static auto AddImplDefinition(ImportContext& context,
   }
 }
 
+namespace {
+struct SpecificInterfaceData {
+  SemIR::ConstantId interface_const_id;
+  SpecificData specific_data;
+};
+}  // namespace
+
+static auto GetLocalSpecificInstanceData(
+    ImportRefResolver& resolver, SemIR::SpecificInterface import_interface)
+    -> SpecificInterfaceData {
+  return {.interface_const_id = GetLocalConstantId(
+              resolver, resolver.import_interfaces()
+                            .Get(import_interface.interface_id)
+                            .first_owning_decl_id),
+          .specific_data =
+              GetLocalSpecificData(resolver, import_interface.specific_id)};
+}
+
+static auto GetLocalSpecificInterface(ImportContext& context,
+                                      SemIR::SpecificId import_specific_id,
+                                      SpecificInterfaceData interface_data)
+    -> SemIR::SpecificInterface {
+  // Find the corresponding interface type. For a non-generic interface,
+  // this is the type of the interface declaration. For a generic interface,
+  // build a interface type referencing this specialization of the generic
+  // interface.
+  auto interface_const_inst =
+      context.local_insts().Get(context.local_constant_values().GetInstId(
+          interface_data.interface_const_id));
+  if (auto facet_type = interface_const_inst.TryAs<SemIR::FacetType>()) {
+    const SemIR::FacetTypeInfo& new_facet_type_info =
+        context.local_facet_types().Get(facet_type->facet_type_id);
+    return new_facet_type_info.impls_constraints.front();
+  } else {
+    auto generic_interface_type =
+        context.local_types().GetAs<SemIR::GenericInterfaceType>(
+            interface_const_inst.type_id());
+    auto specific_id = GetOrAddLocalSpecific(context, import_specific_id,
+                                             interface_data.specific_data);
+    return {generic_interface_type.interface_id, specific_id};
+  }
+}
+
 static auto TryResolveTypedInst(ImportRefResolver& resolver,
                                 SemIR::ImplDecl inst,
                                 SemIR::ConstantId impl_const_id)
@@ -2127,7 +2171,8 @@ static auto TryResolveTypedInst(ImportRefResolver& resolver,
   // TODO: This duplicates a lot of the handling of interfaces, classes, and
   // functions. Factor out the commonality.
   const auto& import_impl = resolver.import_impls().Get(inst.impl_id);
-
+  auto specific_interface_data =
+      GetLocalSpecificInstanceData(resolver, import_impl.interface);
   SemIR::ImplId impl_id = SemIR::ImplId::None;
   if (!impl_const_id.has_value()) {
     if (resolver.HasNewWork()) {
@@ -2179,7 +2224,8 @@ static auto TryResolveTypedInst(ImportRefResolver& resolver,
   new_impl.constraint_id =
       AddLoadedImportRef(resolver, SemIR::TypeType::SingletonTypeId,
                          import_impl.constraint_id, constraint_const_id);
-
+  new_impl.interface = GetLocalSpecificInterface(
+      resolver, import_impl.interface.specific_id, specific_interface_data);
   if (import_impl.is_defined()) {
     AddImplDefinition(resolver, import_impl, new_impl);
   }
@@ -2392,10 +2438,9 @@ static auto TryResolveTypedInst(ImportRefResolver& resolver,
   const SemIR::FacetTypeInfo& facet_type_info =
       resolver.import_facet_types().Get(inst.facet_type_id);
   for (auto interface : facet_type_info.impls_constraints) {
-    GetLocalConstantId(resolver, resolver.import_interfaces()
-                                     .Get(interface.interface_id)
-                                     .first_owning_decl_id);
-    GetLocalSpecificData(resolver, interface.specific_id);
+    // We discard this here and recompute it below instead of saving it to avoid
+    // allocations.
+    GetLocalSpecificInstanceData(resolver, interface);
   }
   for (auto rewrite : facet_type_info.rewrite_constraints) {
     GetLocalConstantId(resolver, rewrite.lhs_const_id);
@@ -2407,31 +2452,9 @@ static auto TryResolveTypedInst(ImportRefResolver& resolver,
 
   llvm::SmallVector<SemIR::FacetTypeInfo::ImplsConstraint> impls_constraints;
   for (auto interface : facet_type_info.impls_constraints) {
-    auto interface_const_id =
-        GetLocalConstantId(resolver, resolver.import_interfaces()
-                                         .Get(interface.interface_id)
-                                         .first_owning_decl_id);
-    auto specific_data = GetLocalSpecificData(resolver, interface.specific_id);
-
-    // Find the corresponding interface type. For a non-generic interface,
-    // this is the type of the interface declaration. For a generic interface,
-    // build a interface type referencing this specialization of the generic
-    // interface.
-    auto interface_const_inst = resolver.local_insts().Get(
-        resolver.local_constant_values().GetInstId(interface_const_id));
-    if (auto facet_type = interface_const_inst.TryAs<SemIR::FacetType>()) {
-      const SemIR::FacetTypeInfo& new_facet_type_info =
-          resolver.local_facet_types().Get(facet_type->facet_type_id);
-      impls_constraints.append(new_facet_type_info.impls_constraints);
-    } else {
-      auto generic_interface_type =
-          resolver.local_types().GetAs<SemIR::GenericInterfaceType>(
-              interface_const_inst.type_id());
-      auto specific_id =
-          GetOrAddLocalSpecific(resolver, interface.specific_id, specific_data);
-      impls_constraints.push_back(
-          {generic_interface_type.interface_id, specific_id});
-    }
+    auto data = GetLocalSpecificInstanceData(resolver, interface);
+    impls_constraints.push_back(
+        GetLocalSpecificInterface(resolver, interface.specific_id, data));
   }
   llvm::SmallVector<SemIR::FacetTypeInfo::RewriteConstraint>
       rewrite_constraints;
diff --git a/toolchain/check/name_lookup.cpp b/toolchain/check/name_lookup.cpp
index d2388e1ac4fbf..712e27baf19e9 100644
--- a/toolchain/check/name_lookup.cpp
+++ b/toolchain/check/name_lookup.cpp
@@ -241,7 +241,7 @@ auto AppendLookupScopesForConstant(Context& context, SemIR::LocId loc_id,
     return true;
   }
   if (auto base_as_class = base.TryAs<SemIR::ClassType>()) {
-    RequireDefinedType(
+    RequireCompleteType(
         context, context.types().GetTypeIdForTypeConstantId(base_const_id),
         loc_id, [&] {
           CARBON_DIAGNOSTIC(QualifiedExprInIncompleteClassScope, Error,
@@ -256,21 +256,21 @@ auto AppendLookupScopesForConstant(Context& context, SemIR::LocId loc_id,
     return true;
   }
   if (auto base_as_facet_type = base.TryAs<SemIR::FacetType>()) {
-    RequireDefinedType(
+    auto complete_id = RequireCompleteFacetType(
         context, context.types().GetTypeIdForTypeConstantId(base_const_id),
-        loc_id, [&] {
-          CARBON_DIAGNOSTIC(QualifiedExprInUndefinedInterfaceScope, Error,
-                            "member access into undefined interface {0}",
-                            InstIdAsType);
-          return context.emitter().Build(
-              loc_id, QualifiedExprInUndefinedInterfaceScope, base_id);
-        });
-    const auto& facet_type_info =
-        context.facet_types().Get(base_as_facet_type->facet_type_id);
-    for (auto interface : facet_type_info.impls_constraints) {
-      auto& interface_info = context.interfaces().Get(interface.interface_id);
-      scopes->push_back(LookupScope{.name_scope_id = interface_info.scope_id,
-                                    .specific_id = interface.specific_id});
+        loc_id, *base_as_facet_type, FacetTypeMemberAccess);
+    if (complete_id.has_value()) {
+      const auto& resolved = context.complete_facet_types().Get(complete_id);
+      for (const auto& interface : resolved.required_interfaces) {
+        auto& interface_info = context.interfaces().Get(interface.interface_id);
+        scopes->push_back({.name_scope_id = interface_info.scope_id,
+                           .specific_id = interface.specific_id});
+      }
+    } else {
+      // Lookup into this scope should fail without producing an error since
+      // `RequireCompleteFacetType` has already issued a diagnostic.
+      scopes->push_back(LookupScope{.name_scope_id = SemIR::NameScopeId::None,
+                                    .specific_id = SemIR::SpecificId::None});
     }
     return true;
   }
diff --git a/toolchain/check/subst.cpp b/toolchain/check/subst.cpp
index dc1ab8920f861..1c8a200c3419d 100644
--- a/toolchain/check/subst.cpp
+++ b/toolchain/check/subst.cpp
@@ -206,20 +206,30 @@ static auto PopOperand(Context& context, Worklist& worklist, SemIR::IdKind kind,
     case SemIR::IdKind::For<SemIR::FacetTypeId>: {
       const auto& old_facet_type_info =
           context.facet_types().Get(SemIR::FacetTypeId(arg));
-      SemIR::FacetTypeInfo new_facet_type_info = old_facet_type_info;
+      SemIR::FacetTypeInfo new_facet_type_info;
       // Since these were added to a stack, we get them back in reverse order.
+      new_facet_type_info.rewrite_constraints.resize(
+          old_facet_type_info.rewrite_constraints.size(),
+          SemIR::FacetTypeInfo::RewriteConstraint::None);
       for (auto i : llvm::reverse(
                llvm::seq(old_facet_type_info.rewrite_constraints.size()))) {
         auto rhs_id = context.constant_values().Get(worklist.Pop());
         auto lhs_id = context.constant_values().Get(worklist.Pop());
-        new_facet_type_info.rewrite_constraints[i].rhs_const_id = rhs_id;
-        new_facet_type_info.rewrite_constraints[i].lhs_const_id = lhs_id;
+        new_facet_type_info.rewrite_constraints[i] = {.lhs_const_id = lhs_id,
+                                                      .rhs_const_id = rhs_id};
       }
+      new_facet_type_info.impls_constraints.resize(
+          old_facet_type_info.impls_constraints.size(),
+          SemIR::SpecificInterface::None);
       for (auto i : llvm::reverse(
                llvm::seq(old_facet_type_info.impls_constraints.size()))) {
-        new_facet_type_info.impls_constraints[i].specific_id =
-            pop_specific(old_facet_type_info.impls_constraints[i].specific_id);
+        const auto& old = old_facet_type_info.impls_constraints[i];
+        new_facet_type_info.impls_constraints[i] = {
+            .interface_id = old.interface_id,
+            .specific_id = pop_specific(old.specific_id)};
       }
+      new_facet_type_info.other_requirements =
+          old_facet_type_info.other_requirements;
       new_facet_type_info.Canonicalize();
       return context.facet_types().Add(new_facet_type_info).index;
     }
diff --git a/toolchain/check/testdata/class/import.carbon b/toolchain/check/testdata/class/import.carbon
index 80d375403acbf..48033d6fc31f1 100644
--- a/toolchain/check/testdata/class/import.carbon
+++ b/toolchain/check/testdata/class/import.carbon
@@ -361,5 +361,5 @@ fn Run() {
 // CHECK:STDOUT:
 // CHECK:STDOUT: fn @F[%self.param_patt: %ForwardDeclared.7b34f2.1]() [from "a.carbon"];
 // CHECK:STDOUT:
-// CHECK:STDOUT: fn @G[addr <unexpected>.inst1129: %ptr.6cf]() [from "a.carbon"];
+// CHECK:STDOUT: fn @G[addr <unexpected>.inst1150: %ptr.6cf]() [from "a.carbon"];
 // CHECK:STDOUT:
diff --git a/toolchain/check/testdata/function/builtin/no_prelude/call_from_operator.carbon b/toolchain/check/testdata/function/builtin/no_prelude/call_from_operator.carbon
index 733f727156a73..168945f036aa5 100644
--- a/toolchain/check/testdata/function/builtin/no_prelude/call_from_operator.carbon
+++ b/toolchain/check/testdata/function/builtin/no_prelude/call_from_operator.carbon
@@ -675,20 +675,20 @@ var arr: [i32; (1 as i32) + (2 as i32)] = (3, 4, (3 as i32) + (4 as i32));
 // CHECK:STDOUT:   %Core.import_ref.f6b058.2: type = import_ref Core//default, loc11_14, loaded [symbolic = @As.%T (constants.%T)]
 // CHECK:STDOUT:   %Core.import_ref.996: @As.%As.type (%As.type.eed) = import_ref Core//default, inst85 [no loc], loaded [symbolic = @As.%Self (constants.%Self.65a)]
 // CHECK:STDOUT:   %Core.import_ref.708: @As.%Convert.type (%Convert.type.843) = import_ref Core//default, loc12_32, loaded [symbolic = @As.%Convert (constants.%Convert.95f)]
-// CHECK:STDOUT:   %Core.import_ref.595: <witness> = import_ref Core//default, loc19_17, loaded [concrete = constants.%impl_witness.bd0]
 // CHECK:STDOUT:   %Core.import_ref.07c = import_ref Core//default, inst39 [no loc], unloaded
 // CHECK:STDOUT:   %Core.import_ref.bdf: %Add.assoc_type = import_ref Core//default, loc8_41, loaded [concrete = constants.%assoc0.b3c]
 // CHECK:STDOUT:   %Core.Op = import_ref Core//default, Op, unloaded
+// CHECK:STDOUT:   %Core.import_ref.595: <witness> = import_ref Core//default, loc19_17, loaded [concrete = constants.%impl_witness.bd0]
 // CHECK:STDOUT:   %Core.import_ref.c8c7cd.1: type = import_ref Core//default, loc19_6, loaded [concrete = constants.%i32.builtin]
 // CHECK:STDOUT:   %Core.import_ref.bf0: type = import_ref Core//default, loc19_13, loaded [concrete = constants.%Add.type]
 // CHECK:STDOUT:   %Core.import_ref.8aa: <witness> = import_ref Core//default, loc23_30, loaded [concrete = constants.%impl_witness.d9b]
 // CHECK:STDOUT:   %Core.import_ref.8721d7.1: type = import_ref Core//default, loc23_17, loaded [concrete = Core.IntLiteral]
 // CHECK:STDOUT:   %Core.import_ref.1e5: type = import_ref Core//default, loc23_28, loaded [concrete = constants.%As.type.a6d]
-// CHECK:STDOUT:   %Core.import_ref.de9: <witness> = import_ref Core//default, loc27_38, loaded [concrete = constants.%impl_witness.39c]
 // CHECK:STDOUT:   %Core.import_ref.f6b058.3: type = import_ref Core//default, loc15_22, loaded [symbolic = @ImplicitAs.%T (constants.%T)]
 // CHECK:STDOUT:   %Core.import_ref.ff5 = import_ref Core//default, inst128 [no loc], unloaded
 // CHECK:STDOUT:   %Core.import_ref.630: @ImplicitAs.%ImplicitAs.assoc_type (%ImplicitAs.assoc_type.837) = import_ref Core//default, loc16_32, loaded [symbolic = @ImplicitAs.%assoc0 (constants.%assoc0.43db8b.2)]
 // CHECK:STDOUT:   %Core.Convert.e69 = import_ref Core//default, Convert, unloaded
+// CHECK:STDOUT:   %Core.import_ref.de9: <witness> = import_ref Core//default, loc27_38, loaded [concrete = constants.%impl_witness.39c]
 // CHECK:STDOUT:   %Core.import_ref.8721d7.2: type = import_ref Core//default, loc27_17, loaded [concrete = Core.IntLiteral]
 // CHECK:STDOUT:   %Core.import_ref.4d9: type = import_ref Core//default, loc27_36, loaded [concrete = constants.%ImplicitAs.type.61e]
 // CHECK:STDOUT:   %Core.import_ref.f6b058.4: type = import_ref Core//default, loc15_22, loaded [symbolic = @ImplicitAs.%T (constants.%T)]
diff --git a/toolchain/check/testdata/if_expr/fail_not_in_function.carbon b/toolchain/check/testdata/if_expr/fail_not_in_function.carbon
index eaa114f92874a..168249a779cca 100644
--- a/toolchain/check/testdata/if_expr/fail_not_in_function.carbon
+++ b/toolchain/check/testdata/if_expr/fail_not_in_function.carbon
@@ -94,7 +94,7 @@ class C {
 // CHECK:STDOUT:     %int_32: Core.IntLiteral = int_value 32 [concrete = constants.%int_32]
 // CHECK:STDOUT:     %i32: type = class_type @Int, @Int(constants.%int_32) [concrete = constants.%i32]
 // CHECK:STDOUT:   }
-// CHECK:STDOUT:   %x: %i32 = bind_name x, <unexpected>.inst1051.loc27_14
+// CHECK:STDOUT:   %x: %i32 = bind_name x, <unexpected>.inst1072.loc27_14
 // CHECK:STDOUT:   name_binding_decl {
 // CHECK:STDOUT:     %y.patt: %i32 = binding_pattern y
 // CHECK:STDOUT:     %.loc37: %i32 = var_pattern %y.patt
diff --git a/toolchain/check/testdata/impl/fail_extend_partially_defined_interface.carbon b/toolchain/check/testdata/impl/fail_extend_partially_defined_interface.carbon
index 4a57b51018ea5..e5beff3f8d1a3 100644
--- a/toolchain/check/testdata/impl/fail_extend_partially_defined_interface.carbon
+++ b/toolchain/check/testdata/impl/fail_extend_partially_defined_interface.carbon
@@ -10,9 +10,9 @@
 
 interface I {
   class C {
-    // CHECK:STDERR: fail_extend_partially_defined_interface.carbon:[[@LINE+11]]:5: error: implementation of undefined interface I [ImplOfUndefinedInterface]
+    // CHECK:STDERR: fail_extend_partially_defined_interface.carbon:[[@LINE+11]]:20: error: impl of undefined interface I [ResolveFacetTypeWithUndefinedInterface]
     // CHECK:STDERR:     extend impl as I;
-    // CHECK:STDERR:     ^~~~~~~~~~~~~~~~~
+    // CHECK:STDERR:                    ^
     // CHECK:STDERR: fail_extend_partially_defined_interface.carbon:[[@LINE-5]]:1: note: interface is currently being defined [InterfaceUndefinedWithinDefinition]
     // CHECK:STDERR: interface I {
     // CHECK:STDERR: ^~~~~~~~~~~~~
diff --git a/toolchain/check/testdata/impl/fail_extend_undefined_interface.carbon b/toolchain/check/testdata/impl/fail_extend_undefined_interface.carbon
index d489b94fb2b42..7e25502409aff 100644
--- a/toolchain/check/testdata/impl/fail_extend_undefined_interface.carbon
+++ b/toolchain/check/testdata/impl/fail_extend_undefined_interface.carbon
@@ -11,9 +11,9 @@
 interface I;
 
 class C {
-  // CHECK:STDERR: fail_extend_undefined_interface.carbon:[[@LINE+7]]:3: error: implementation of undefined interface I [ImplOfUndefinedInterface]
+  // CHECK:STDERR: fail_extend_undefined_interface.carbon:[[@LINE+7]]:18: error: impl of undefined interface I [ResolveFacetTypeWithUndefinedInterface]
   // CHECK:STDERR:   extend impl as I;
-  // CHECK:STDERR:   ^~~~~~~~~~~~~~~~~
+  // CHECK:STDERR:                  ^
   // CHECK:STDERR: fail_extend_undefined_interface.carbon:[[@LINE-6]]:1: note: interface was forward declared here [InterfaceForwardDeclaredHere]
   // CHECK:STDERR: interface I;
   // CHECK:STDERR: ^~~~~~~~~~~~
@@ -22,7 +22,7 @@ class C {
 }
 
 fn F(c: C) {
-  // CHECK:STDERR: fail_extend_undefined_interface.carbon:[[@LINE+10]]:3: error: member access into undefined interface `I` [QualifiedExprInUndefinedInterfaceScope]
+  // CHECK:STDERR: fail_extend_undefined_interface.carbon:[[@LINE+10]]:3: error: member access into undefined interface I [ResolveFacetTypeWithUndefinedInterface]
   // CHECK:STDERR:   C.F();
   // CHECK:STDERR:   ^~~
   // CHECK:STDERR: fail_extend_undefined_interface.carbon:[[@LINE-17]]:1: note: interface was forward declared here [InterfaceForwardDeclaredHere]
@@ -33,7 +33,7 @@ fn F(c: C) {
   // CHECK:STDERR:                  ^
   // CHECK:STDERR:
   C.F();
-  // CHECK:STDERR: fail_extend_undefined_interface.carbon:[[@LINE+14]]:3: error: member access into undefined interface `I` [QualifiedExprInUndefinedInterfaceScope]
+  // CHECK:STDERR: fail_extend_undefined_interface.carbon:[[@LINE+14]]:3: error: member access into undefined interface I [ResolveFacetTypeWithUndefinedInterface]
   // CHECK:STDERR:   c.F();
   // CHECK:STDERR:   ^~~
   // CHECK:STDERR: fail_extend_undefined_interface.carbon:[[@LINE-28]]:1: note: interface was forward declared here [InterfaceForwardDeclaredHere]
diff --git a/toolchain/check/testdata/impl/fail_impl_bad_interface.carbon b/toolchain/check/testdata/impl/fail_impl_bad_interface.carbon
index b6d7820cd39ca..968c4d90bea65 100644
--- a/toolchain/check/testdata/impl/fail_impl_bad_interface.carbon
+++ b/toolchain/check/testdata/impl/fail_impl_bad_interface.carbon
@@ -38,7 +38,7 @@ library "[[@TEST_NAME]]";
 // Note: This code is not expected to pass checking, even once the TODO is
 // addressed.
 
-// CHECK:STDERR: fail_impl_as_type_where.carbon:[[@LINE+4]]:1: error: semantics TODO: `impl as not 1 interface` [SemanticsTodo]
+// CHECK:STDERR: fail_impl_as_type_where.carbon:[[@LINE+4]]:1: error: impl as 0 interfaces, expected 1 [ImplOfNotOneInterface]
 // CHECK:STDERR: impl f64 as type where .Self impls type {}
 // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 // CHECK:STDERR:
diff --git a/toolchain/check/testdata/impl/lookup/no_prelude/import.carbon b/toolchain/check/testdata/impl/lookup/no_prelude/import.carbon
index 66eb6482e1792..637433eec4be8 100644
--- a/toolchain/check/testdata/impl/lookup/no_prelude/import.carbon
+++ b/toolchain/check/testdata/impl/lookup/no_prelude/import.carbon
@@ -568,10 +568,10 @@ fn Test(c: HasExtraInterfaces.C(type)) {
 // CHECK:STDOUT:   %PackageA.import_ref.2c4 = import_ref PackageA//default, inst25 [no loc], unloaded
 // CHECK:STDOUT:   %PackageA.import_ref.29a: type = import_ref PackageA//default, loc11_6, loaded [concrete = constants.%C]
 // CHECK:STDOUT:   %PackageA.import_ref.e8c: type = import_ref PackageA//default, loc11_11, loaded [concrete = constants.%HasF.type]
-// CHECK:STDOUT:   %PackageB.import_ref.fa0 = import_ref PackageB//default, loc13_25, unloaded
 // CHECK:STDOUT:   %PackageB.import_ref.5d8 = import_ref PackageB//default, inst17 [no loc], unloaded
 // CHECK:STDOUT:   %PackageB.import_ref.ed7 = import_ref PackageB//default, loc7_9, unloaded
 // CHECK:STDOUT:   %PackageB.G = import_ref PackageB//default, G, unloaded
+// CHECK:STDOUT:   %PackageB.import_ref.fa0 = import_ref PackageB//default, loc13_25, unloaded
 // CHECK:STDOUT:   %PackageB.import_ref.dfb: type = import_ref PackageB//default, loc13_14, loaded [concrete = constants.%C]
 // CHECK:STDOUT:   %PackageB.import_ref.cee586.1: type = import_ref PackageB//default, loc13_20, loaded [concrete = constants.%HasG.type]
 // CHECK:STDOUT:   %PackageB.import_ref.f2f: <witness> = import_ref PackageB//default, loc18_25, loaded [concrete = constants.%impl_witness]
@@ -710,10 +710,10 @@ fn Test(c: HasExtraInterfaces.C(type)) {
 // CHECK:STDOUT:   %PackageB.import_ref.5d8 = import_ref PackageB//default, inst17 [no loc], unloaded
 // CHECK:STDOUT:   %PackageB.import_ref.604: %HasG.assoc_type = import_ref PackageB//default, loc7_9, loaded [concrete = constants.%assoc0]
 // CHECK:STDOUT:   %PackageB.G = import_ref PackageB//default, G, unloaded
-// CHECK:STDOUT:   %PackageA.import_ref.0e8 = import_ref PackageA//default, loc11_16, unloaded
 // CHECK:STDOUT:   %PackageA.import_ref.28c = import_ref PackageA//default, inst15 [no loc], unloaded
 // CHECK:STDOUT:   %PackageA.import_ref.a2a = import_ref PackageA//default, loc5_9, unloaded
 // CHECK:STDOUT:   %PackageA.F = import_ref PackageA//default, F, unloaded
+// CHECK:STDOUT:   %PackageA.import_ref.0e8 = import_ref PackageA//default, loc11_16, unloaded
 // CHECK:STDOUT:   %PackageA.import_ref.29a: type = import_ref PackageA//default, loc11_6, loaded [concrete = constants.%C]
 // CHECK:STDOUT:   %PackageA.import_ref.e8c: type = import_ref PackageA//default, loc11_11, loaded [concrete = constants.%HasF.type]
 // CHECK:STDOUT:   %PackageB.import_ref.5d9: <witness> = import_ref PackageB//default, loc13_25, loaded [concrete = constants.%impl_witness]
@@ -859,10 +859,10 @@ fn Test(c: HasExtraInterfaces.C(type)) {
 // CHECK:STDOUT:   %PackageB.import_ref.6a9 = import_ref PackageB//default, inst36 [indirect], unloaded
 // CHECK:STDOUT:   %PackageB.import_ref.dfb: type = import_ref PackageB//default, loc13_14, loaded [concrete = constants.%C]
 // CHECK:STDOUT:   %PackageB.import_ref.cee586.1: type = import_ref PackageB//default, loc13_20, loaded [concrete = constants.%HasG.type]
-// CHECK:STDOUT:   %PackageB.import_ref.7db = import_ref PackageB//default, loc18_25, unloaded
 // CHECK:STDOUT:   %PackageB.import_ref.96f = import_ref PackageB//default, inst53 [indirect], unloaded
 // CHECK:STDOUT:   %PackageB.import_ref.b30 = import_ref PackageB//default, inst54 [indirect], unloaded
 // CHECK:STDOUT:   %PackageB.F = import_ref PackageB//default, F, unloaded
+// CHECK:STDOUT:   %PackageB.import_ref.7db = import_ref PackageB//default, loc18_25, unloaded
 // CHECK:STDOUT:   %PackageB.import_ref.aa9f8a.1: type = import_ref PackageB//default, loc18_6, loaded [concrete = constants.%D]
 // CHECK:STDOUT:   %PackageB.import_ref.831: type = import_ref PackageB//default, loc18_19, loaded [concrete = constants.%HasF.type]
 // CHECK:STDOUT:   %PackageB.import_ref.240: <witness> = import_ref PackageB//default, loc23_16, loaded [concrete = constants.%impl_witness]
diff --git a/toolchain/check/testdata/impl/no_prelude/fail_extend_impl_scope.carbon b/toolchain/check/testdata/impl/no_prelude/fail_extend_impl_scope.carbon
index 6e68bfdb787ec..5bb330ad0e9ad 100644
--- a/toolchain/check/testdata/impl/no_prelude/fail_extend_impl_scope.carbon
+++ b/toolchain/check/testdata/impl/no_prelude/fail_extend_impl_scope.carbon
@@ -38,10 +38,17 @@ library "[[@TEST_NAME]]";
 interface Z {
   fn Zero();
 
-  // CHECK:STDERR: fail_extend_impl_self_interface.carbon:[[@LINE+4]]:15: error: `impl as` can only be used in a class [ImplAsOutsideClass]
+  // CHECK:STDERR: fail_extend_impl_self_interface.carbon:[[@LINE+11]]:15: error: `impl as` can only be used in a class [ImplAsOutsideClass]
   // CHECK:STDERR:   extend impl as Z {
   // CHECK:STDERR:               ^~
   // CHECK:STDERR:
+  // CHECK:STDERR: fail_extend_impl_self_interface.carbon:[[@LINE+7]]:18: error: impl of undefined interface Z [ResolveFacetTypeWithUndefinedInterface]
+  // CHECK:STDERR:   extend impl as Z {
+  // CHECK:STDERR:                  ^
+  // CHECK:STDERR: fail_extend_impl_self_interface.carbon:[[@LINE-10]]:1: note: interface is currently being defined [InterfaceUndefinedWithinDefinition]
+  // CHECK:STDERR: interface Z {
+  // CHECK:STDERR: ^~~~~~~~~~~~~
+  // CHECK:STDERR:
   extend impl as Z {
     fn Zero() {}
   }
@@ -250,12 +257,12 @@ fn F() {
 // CHECK:STDOUT:
 // CHECK:STDOUT: fn @F() {
 // CHECK:STDOUT: !entry:
-// CHECK:STDOUT:   %.loc25_5.1: %empty_struct_type = struct_literal ()
+// CHECK:STDOUT:   %.loc32_5.1: %empty_struct_type = struct_literal ()
 // CHECK:STDOUT:   %Point.ref: type = name_ref Point, file.%Point.decl [concrete = constants.%Point]
-// CHECK:STDOUT:   %.loc25_5.2: ref %Point = temporary_storage
-// CHECK:STDOUT:   %.loc25_5.3: init %Point = class_init (), %.loc25_5.2 [concrete = constants.%Point.val]
-// CHECK:STDOUT:   %.loc25_5.4: ref %Point = temporary %.loc25_5.2, %.loc25_5.3
-// CHECK:STDOUT:   %.loc25_7: ref %Point = converted %.loc25_5.1, %.loc25_5.4
+// CHECK:STDOUT:   %.loc32_5.2: ref %Point = temporary_storage
+// CHECK:STDOUT:   %.loc32_5.3: init %Point = class_init (), %.loc32_5.2 [concrete = constants.%Point.val]
+// CHECK:STDOUT:   %.loc32_5.4: ref %Point = temporary %.loc32_5.2, %.loc32_5.3
+// CHECK:STDOUT:   %.loc32_7: ref %Point = converted %.loc32_5.1, %.loc32_5.4
 // CHECK:STDOUT:   %Zero.ref: %Z.assoc_type = name_ref Zero, @Z.%assoc0 [concrete = constants.%assoc0]
 // CHECK:STDOUT:   %impl.elem0: %.c37 = impl_witness_access constants.%impl_witness, element0 [concrete = constants.%Zero.dec]
 // CHECK:STDOUT:   %Zero.call: init %empty_tuple.type = call %impl.elem0()
diff --git a/toolchain/check/testdata/impl/no_prelude/fail_impl_as_scope.carbon b/toolchain/check/testdata/impl/no_prelude/fail_impl_as_scope.carbon
index 9fb43cf3d2ba6..aec43b4a0a4c9 100644
--- a/toolchain/check/testdata/impl/no_prelude/fail_impl_as_scope.carbon
+++ b/toolchain/check/testdata/impl/no_prelude/fail_impl_as_scope.carbon
@@ -45,10 +45,17 @@ library "[[@TEST_NAME]]";
 interface Z {
   fn Zero();
 
-   // CHECK:STDERR: fail_impl_as_self_interface.carbon:[[@LINE+4]]:9: error: `impl as` can only be used in a class [ImplAsOutsideClass]
+   // CHECK:STDERR: fail_impl_as_self_interface.carbon:[[@LINE+11]]:9: error: `impl as` can only be used in a class [ImplAsOutsideClass]
    // CHECK:STDERR:    impl as Z {
    // CHECK:STDERR:         ^~
    // CHECK:STDERR:
+   // CHECK:STDERR: fail_impl_as_self_interface.carbon:[[@LINE+7]]:12: error: impl of undefined interface Z [ResolveFacetTypeWithUndefinedInterface]
+   // CHECK:STDERR:    impl as Z {
+   // CHECK:STDERR:            ^
+   // CHECK:STDERR: fail_impl_as_self_interface.carbon:[[@LINE-10]]:1: note: interface is currently being defined [InterfaceUndefinedWithinDefinition]
+   // CHECK:STDERR: interface Z {
+   // CHECK:STDERR: ^~~~~~~~~~~~~
+   // CHECK:STDERR:
    impl as Z {
     fn Zero() {}
   }
@@ -304,12 +311,12 @@ class X {
 // CHECK:STDOUT:
 // CHECK:STDOUT: fn @F() {
 // CHECK:STDOUT: !entry:
-// CHECK:STDOUT:   %.loc25_5.1: %empty_struct_type = struct_literal ()
+// CHECK:STDOUT:   %.loc32_5.1: %empty_struct_type = struct_literal ()
 // CHECK:STDOUT:   %Point.ref: type = name_ref Point, file.%Point.decl [concrete = constants.%Point]
-// CHECK:STDOUT:   %.loc25_5.2: ref %Point = temporary_storage
-// CHECK:STDOUT:   %.loc25_5.3: init %Point = class_init (), %.loc25_5.2 [concrete = constants.%Point.val]
-// CHECK:STDOUT:   %.loc25_5.4: ref %Point = temporary %.loc25_5.2, %.loc25_5.3
-// CHECK:STDOUT:   %.loc25_7: ref %Point = converted %.loc25_5.1, %.loc25_5.4
+// CHECK:STDOUT:   %.loc32_5.2: ref %Point = temporary_storage
+// CHECK:STDOUT:   %.loc32_5.3: init %Point = class_init (), %.loc32_5.2 [concrete = constants.%Point.val]
+// CHECK:STDOUT:   %.loc32_5.4: ref %Point = temporary %.loc32_5.2, %.loc32_5.3
+// CHECK:STDOUT:   %.loc32_7: ref %Point = converted %.loc32_5.1, %.loc32_5.4
 // CHECK:STDOUT:   %Z.ref: type = name_ref Z, file.%Z.decl [concrete = constants.%Z.type]
 // CHECK:STDOUT:   %Zero.ref: %Z.assoc_type = name_ref Zero, @Z.%assoc0 [concrete = constants.%assoc0]
 // CHECK:STDOUT:   %impl.elem0: %.c37 = impl_witness_access constants.%impl_witness, element0 [concrete = constants.%Zero.dec]
diff --git a/toolchain/check/testdata/impl/no_prelude/fail_undefined_interface.carbon b/toolchain/check/testdata/impl/no_prelude/fail_undefined_interface.carbon
index 76baaf0b39bf4..584082f1832fa 100644
--- a/toolchain/check/testdata/impl/no_prelude/fail_undefined_interface.carbon
+++ b/toolchain/check/testdata/impl/no_prelude/fail_undefined_interface.carbon
@@ -13,9 +13,9 @@
 library "[[@TEST_NAME]]";
 
 interface I;
-// CHECK:STDERR: fail_empty_struct.carbon:[[@LINE+7]]:1: error: implementation of undefined interface I [ImplOfUndefinedInterface]
+// CHECK:STDERR: fail_empty_struct.carbon:[[@LINE+7]]:12: error: impl of undefined interface I [ResolveFacetTypeWithUndefinedInterface]
 // CHECK:STDERR: impl {} as I {}
-// CHECK:STDERR: ^~~~~~~~~~~~~~
+// CHECK:STDERR:            ^
 // CHECK:STDERR: fail_empty_struct.carbon:[[@LINE-4]]:1: note: interface was forward declared here [InterfaceForwardDeclaredHere]
 // CHECK:STDERR: interface I;
 // CHECK:STDERR: ^~~~~~~~~~~~
@@ -28,9 +28,9 @@ library "[[@TEST_NAME]]";
 
 interface J;
 class C {}
-// CHECK:STDERR: fail_class.carbon:[[@LINE+7]]:1: error: implementation of undefined interface J [ImplOfUndefinedInterface]
+// CHECK:STDERR: fail_class.carbon:[[@LINE+7]]:11: error: impl of undefined interface J [ResolveFacetTypeWithUndefinedInterface]
 // CHECK:STDERR: impl C as J {}
-// CHECK:STDERR: ^~~~~~~~~~~~~
+// CHECK:STDERR:           ^
 // CHECK:STDERR: fail_class.carbon:[[@LINE-5]]:1: note: interface was forward declared here [InterfaceForwardDeclaredHere]
 // CHECK:STDERR: interface J;
 // CHECK:STDERR: ^~~~~~~~~~~~
diff --git a/toolchain/check/testdata/impl/no_prelude/impl_assoc_const.carbon b/toolchain/check/testdata/impl/no_prelude/impl_assoc_const.carbon
index 0c84aecaf1426..f2234f3a41b92 100644
--- a/toolchain/check/testdata/impl/no_prelude/impl_assoc_const.carbon
+++ b/toolchain/check/testdata/impl/no_prelude/impl_assoc_const.carbon
@@ -163,6 +163,21 @@ interface N {
 
 impl () as N where .Y = {.a = {}} { }
 
+// --- fail_where_rewrite_function.carbon
+library "[[@TEST_NAME]]";
+
+interface IF { fn F(); }
+
+class CD { }
+
+// CHECK:STDERR: fail_where_rewrite_function.carbon:[[@LINE+4]]:12: error: rewrite specified for associated function F [RewriteForAssociatedFunction]
+// CHECK:STDERR: impl CD as IF where .F = 0 {
+// CHECK:STDERR:            ^~~~~~~~~~~~~~~
+// CHECK:STDERR:
+impl CD as IF where .F = 0 {
+  fn F() {}
+}
+
 // CHECK:STDOUT: --- success.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
@@ -727,7 +742,7 @@ impl () as N where .Y = {.a = {}} { }
 // CHECK:STDOUT:   %impl.elem0: type = impl_witness_access %.Self.as_wit, element0 [symbolic_self]
 // CHECK:STDOUT:   %empty_struct_type: type = struct_type {} [concrete]
 // CHECK:STDOUT:   %L_where.type: type = facet_type <@L where %impl.elem0 = %empty_tuple.type and %impl.elem0 = %empty_struct_type> [concrete]
-// CHECK:STDOUT:   %impl_witness: <witness> = impl_witness (%empty_tuple.type) [concrete]
+// CHECK:STDOUT:   %impl_witness: <witness> = impl_witness (<error>) [concrete]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
@@ -761,7 +776,7 @@ impl () as N where .Y = {.a = {}} { }
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc9_32, %.loc9_38.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
-// CHECK:STDOUT:   %impl_witness: <witness> = impl_witness (constants.%empty_tuple.type) [concrete = constants.%impl_witness]
+// CHECK:STDOUT:   %impl_witness: <witness> = impl_witness (<error>) [concrete = constants.%impl_witness]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: interface @L {
@@ -1161,3 +1176,94 @@ impl () as N where .Y = {.a = {}} { }
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @Y(constants.%N.facet) {}
 // CHECK:STDOUT:
+// CHECK:STDOUT: --- fail_where_rewrite_function.carbon
+// CHECK:STDOUT:
+// CHECK:STDOUT: constants {
+// CHECK:STDOUT:   %IF.type: type = facet_type <@IF> [concrete]
+// CHECK:STDOUT:   %Self: %IF.type = bind_symbolic_name Self, 0 [symbolic]
+// CHECK:STDOUT:   %F.type.496: type = fn_type @F.1 [concrete]
+// CHECK:STDOUT:   %F.1de: %F.type.496 = struct_value () [concrete]
+// CHECK:STDOUT:   %IF.assoc_type: type = assoc_entity_type %IF.type [concrete]
+// CHECK:STDOUT:   %assoc0: %IF.assoc_type = assoc_entity element0, @IF.%F.decl [concrete]
+// CHECK:STDOUT:   %CD: type = class_type @CD [concrete]
+// CHECK:STDOUT:   %empty_struct_type: type = struct_type {} [concrete]
+// CHECK:STDOUT:   %complete_type: <witness> = complete_type_witness %empty_struct_type [concrete]
+// CHECK:STDOUT:   %.Self: %IF.type = bind_symbolic_name .Self [symbolic_self]
+// CHECK:STDOUT:   %.Self.as_type: type = facet_access_type %.Self [symbolic_self]
+// CHECK:STDOUT:   %.Self.as_wit: <witness> = facet_access_witness %.Self [symbolic_self]
+// CHECK:STDOUT:   %IF.facet.3a2: %IF.type = facet_value %.Self.as_type, %.Self.as_wit [symbolic_self]
+// CHECK:STDOUT:   %.99d: type = fn_type_with_self_type %F.type.496, %IF.facet.3a2 [symbolic_self]
+// CHECK:STDOUT:   %impl.elem0: %.99d = impl_witness_access %.Self.as_wit, element0 [symbolic_self]
+// CHECK:STDOUT:   %int_0: Core.IntLiteral = int_value 0 [concrete]
+// CHECK:STDOUT:   %IF_where.type: type = facet_type <@IF where %impl.elem0 = %int_0> [concrete]
+// CHECK:STDOUT:   %impl_witness: <witness> = impl_witness (@impl.%F.decl) [concrete]
+// CHECK:STDOUT:   %F.type.064: type = fn_type @F.2 [concrete]
+// CHECK:STDOUT:   %F.822: %F.type.064 = struct_value () [concrete]
+// CHECK:STDOUT:   %IF.facet.b37: %IF.type = facet_value %CD, %impl_witness [concrete]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: file {
+// CHECK:STDOUT:   package: <namespace> = namespace [concrete] {
+// CHECK:STDOUT:     .IF = %IF.decl
+// CHECK:STDOUT:     .CD = %CD.decl
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %IF.decl: type = interface_decl @IF [concrete = constants.%IF.type] {} {}
+// CHECK:STDOUT:   %CD.decl: type = class_decl @CD [concrete = constants.%CD] {} {}
+// CHECK:STDOUT:   impl_decl @impl [concrete] {} {
+// CHECK:STDOUT:     %CD.ref: type = name_ref CD, file.%CD.decl [concrete = constants.%CD]
+// CHECK:STDOUT:     %IF.ref: type = name_ref IF, file.%IF.decl [concrete = constants.%IF.type]
+// CHECK:STDOUT:     %.Self: %IF.type = bind_symbolic_name .Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %.Self.ref: %IF.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %F.ref: %IF.assoc_type = name_ref F, @IF.%assoc0 [concrete = constants.%assoc0]
+// CHECK:STDOUT:     %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:     %.loc11_21: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:     %.Self.as_wit: <witness> = facet_access_witness %.Self.ref [symbolic_self = constants.%.Self.as_wit]
+// CHECK:STDOUT:     %impl.elem0: %.99d = impl_witness_access %.Self.as_wit, element0 [symbolic_self = constants.%impl.elem0]
+// CHECK:STDOUT:     %int_0: Core.IntLiteral = int_value 0 [concrete = constants.%int_0]
+// CHECK:STDOUT:     %.loc11_15: type = where_expr %.Self [concrete = constants.%IF_where.type] {
+// CHECK:STDOUT:       requirement_rewrite %impl.elem0, %int_0
+// CHECK:STDOUT:     }
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %impl_witness: <witness> = impl_witness (@impl.%F.decl) [concrete = constants.%impl_witness]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: interface @IF {
+// CHECK:STDOUT:   %Self: %IF.type = bind_symbolic_name Self, 0 [symbolic = constants.%Self]
+// CHECK:STDOUT:   %F.decl: %F.type.496 = fn_decl @F.1 [concrete = constants.%F.1de] {} {}
+// CHECK:STDOUT:   %assoc0: %IF.assoc_type = assoc_entity element0, %F.decl [concrete = constants.%assoc0]
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = %Self
+// CHECK:STDOUT:   .F = %assoc0
+// CHECK:STDOUT:   witness = (%F.decl)
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: impl @impl: %CD.ref as %.loc11_15 {
+// CHECK:STDOUT:   %F.decl: %F.type.064 = fn_decl @F.2 [concrete = constants.%F.822] {} {}
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .F = %F.decl
+// CHECK:STDOUT:   witness = file.%impl_witness
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: class @CD {
+// CHECK:STDOUT:   %complete_type: <witness> = complete_type_witness %empty_struct_type [concrete = constants.%complete_type]
+// CHECK:STDOUT:   complete_type_witness = %complete_type
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = constants.%CD
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: generic fn @F.1(@IF.%Self: %IF.type) {
+// CHECK:STDOUT:   fn();
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: fn @F.2() {
+// CHECK:STDOUT: !entry:
+// CHECK:STDOUT:   return
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @F.1(constants.%Self) {}
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @F.1(constants.%IF.facet.b37) {}
+// CHECK:STDOUT:
diff --git a/toolchain/check/testdata/impl/no_prelude/import_generic.carbon b/toolchain/check/testdata/impl/no_prelude/import_generic.carbon
index ebe1572d6aa67..499e8c8e7f1f4 100644
--- a/toolchain/check/testdata/impl/no_prelude/import_generic.carbon
+++ b/toolchain/check/testdata/impl/no_prelude/import_generic.carbon
@@ -296,9 +296,9 @@ impl forall [T:! type] D as J(T*) {}
 // CHECK:STDOUT: imports {
 // CHECK:STDOUT:   %Main.C: type = import_ref Main//import_generic, C, loaded [concrete = constants.%C]
 // CHECK:STDOUT:   %Main.I: %I.type.dac = import_ref Main//import_generic, I, loaded [concrete = constants.%I.generic]
-// CHECK:STDOUT:   %Main.import_ref.003 = import_ref Main//import_generic, loc8_33, unloaded
 // CHECK:STDOUT:   %Main.import_ref.f6b058.1: type = import_ref Main//import_generic, loc5_13, loaded [symbolic = @I.%T (constants.%T)]
 // CHECK:STDOUT:   %Main.import_ref.884 = import_ref Main//import_generic, inst31 [no loc], unloaded
+// CHECK:STDOUT:   %Main.import_ref.003 = import_ref Main//import_generic, loc8_33, unloaded
 // CHECK:STDOUT:   %Main.import_ref.8f2: <witness> = import_ref Main//import_generic, loc4_10, loaded [concrete = constants.%complete_type]
 // CHECK:STDOUT:   %Main.import_ref.2c4 = import_ref Main//import_generic, inst14 [no loc], unloaded
 // CHECK:STDOUT:   %Main.import_ref.f6b058.2: type = import_ref Main//import_generic, loc8_14, loaded [symbolic = @impl.1.%T (constants.%T)]
diff --git a/toolchain/check/testdata/impl/no_prelude/import_interface_assoc_const.carbon b/toolchain/check/testdata/impl/no_prelude/import_interface_assoc_const.carbon
index 726c23b8ec5d1..a6f4109b2daf5 100644
--- a/toolchain/check/testdata/impl/no_prelude/import_interface_assoc_const.carbon
+++ b/toolchain/check/testdata/impl/no_prelude/import_interface_assoc_const.carbon
@@ -184,6 +184,25 @@ class CC { }
 
 impl CC as NonType where .Y = {.a = {}} { }
 
+// --- interface_with_function.carbon
+library "[[@TEST_NAME]]";
+
+interface IF { fn F(); }
+
+// --- fail_where_rewrite_function.carbon
+library "[[@TEST_NAME]]";
+import library "interface_with_function";
+
+class CD { }
+
+// CHECK:STDERR: fail_where_rewrite_function.carbon:[[@LINE+4]]:12: error: rewrite specified for associated function F [RewriteForAssociatedFunction]
+// CHECK:STDERR: impl CD as IF where .F = 0 {
+// CHECK:STDERR:            ^~~~~~~~~~~~~~~
+// CHECK:STDERR:
+impl CD as IF where .F = 0 {
+  fn F() {}
+}
+
 // CHECK:STDOUT: --- interface.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
@@ -954,7 +973,7 @@ impl CC as NonType where .Y = {.a = {}} { }
 // CHECK:STDOUT:   %I.facet: %I.type = facet_value %.Self.as_type, %.Self.as_wit [symbolic_self]
 // CHECK:STDOUT:   %impl.elem0: type = impl_witness_access %.Self.as_wit, element0 [symbolic_self]
 // CHECK:STDOUT:   %I_where.type: type = facet_type <@I where %impl.elem0 = %empty_struct_type and %impl.elem0 = %empty_tuple.type> [concrete]
-// CHECK:STDOUT:   %impl_witness: <witness> = impl_witness (%empty_struct_type) [concrete]
+// CHECK:STDOUT:   %impl_witness: <witness> = impl_witness (<error>) [concrete]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: imports {
@@ -1001,7 +1020,7 @@ impl CC as NonType where .Y = {.a = {}} { }
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc10_32, %.loc10_38.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
-// CHECK:STDOUT:   %impl_witness: <witness> = impl_witness (constants.%empty_struct_type) [concrete = constants.%impl_witness]
+// CHECK:STDOUT:   %impl_witness: <witness> = impl_witness (<error>) [concrete = constants.%impl_witness]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: interface @I [from "interface.carbon"] {
@@ -1492,3 +1511,133 @@ impl CC as NonType where .Y = {.a = {}} { }
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @Y(constants.%NonType.facet) {}
 // CHECK:STDOUT:
+// CHECK:STDOUT: --- interface_with_function.carbon
+// CHECK:STDOUT:
+// CHECK:STDOUT: constants {
+// CHECK:STDOUT:   %IF.type: type = facet_type <@IF> [concrete]
+// CHECK:STDOUT:   %Self: %IF.type = bind_symbolic_name Self, 0 [symbolic]
+// CHECK:STDOUT:   %F.type: type = fn_type @F [concrete]
+// CHECK:STDOUT:   %F: %F.type = struct_value () [concrete]
+// CHECK:STDOUT:   %IF.assoc_type: type = assoc_entity_type %IF.type [concrete]
+// CHECK:STDOUT:   %assoc0: %IF.assoc_type = assoc_entity element0, @IF.%F.decl [concrete]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: file {
+// CHECK:STDOUT:   package: <namespace> = namespace [concrete] {
+// CHECK:STDOUT:     .IF = %IF.decl
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %IF.decl: type = interface_decl @IF [concrete = constants.%IF.type] {} {}
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: interface @IF {
+// CHECK:STDOUT:   %Self: %IF.type = bind_symbolic_name Self, 0 [symbolic = constants.%Self]
+// CHECK:STDOUT:   %F.decl: %F.type = fn_decl @F [concrete = constants.%F] {} {}
+// CHECK:STDOUT:   %assoc0: %IF.assoc_type = assoc_entity element0, %F.decl [concrete = constants.%assoc0]
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = %Self
+// CHECK:STDOUT:   .F = %assoc0
+// CHECK:STDOUT:   witness = (%F.decl)
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: generic fn @F(@IF.%Self: %IF.type) {
+// CHECK:STDOUT:   fn();
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @F(constants.%Self) {}
+// CHECK:STDOUT:
+// CHECK:STDOUT: --- fail_where_rewrite_function.carbon
+// CHECK:STDOUT:
+// CHECK:STDOUT: constants {
+// CHECK:STDOUT:   %CD: type = class_type @CD [concrete]
+// CHECK:STDOUT:   %empty_struct_type: type = struct_type {} [concrete]
+// CHECK:STDOUT:   %complete_type: <witness> = complete_type_witness %empty_struct_type [concrete]
+// CHECK:STDOUT:   %IF.type: type = facet_type <@IF> [concrete]
+// CHECK:STDOUT:   %Self: %IF.type = bind_symbolic_name Self, 0 [symbolic]
+// CHECK:STDOUT:   %.Self: %IF.type = bind_symbolic_name .Self [symbolic_self]
+// CHECK:STDOUT:   %IF.assoc_type: type = assoc_entity_type %IF.type [concrete]
+// CHECK:STDOUT:   %assoc0: %IF.assoc_type = assoc_entity element0, imports.%Main.import_ref.4b7 [concrete]
+// CHECK:STDOUT:   %.Self.as_type: type = facet_access_type %.Self [symbolic_self]
+// CHECK:STDOUT:   %.Self.as_wit: <witness> = facet_access_witness %.Self [symbolic_self]
+// CHECK:STDOUT:   %F.type.496: type = fn_type @F.1 [concrete]
+// CHECK:STDOUT:   %F.1de: %F.type.496 = struct_value () [concrete]
+// CHECK:STDOUT:   %IF.facet.3a2: %IF.type = facet_value %.Self.as_type, %.Self.as_wit [symbolic_self]
+// CHECK:STDOUT:   %.99d: type = fn_type_with_self_type %F.type.496, %IF.facet.3a2 [symbolic_self]
+// CHECK:STDOUT:   %impl.elem0: %.99d = impl_witness_access %.Self.as_wit, element0 [symbolic_self]
+// CHECK:STDOUT:   %int_0: Core.IntLiteral = int_value 0 [concrete]
+// CHECK:STDOUT:   %IF_where.type: type = facet_type <@IF where %impl.elem0 = %int_0> [concrete]
+// CHECK:STDOUT:   %impl_witness: <witness> = impl_witness (@impl.%F.decl) [concrete]
+// CHECK:STDOUT:   %F.type.064: type = fn_type @F.2 [concrete]
+// CHECK:STDOUT:   %F.822: %F.type.064 = struct_value () [concrete]
+// CHECK:STDOUT:   %IF.facet.b37: %IF.type = facet_value %CD, %impl_witness [concrete]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: imports {
+// CHECK:STDOUT:   %Main.IF: type = import_ref Main//interface_with_function, IF, loaded [concrete = constants.%IF.type]
+// CHECK:STDOUT:   %Main.import_ref.a2a = import_ref Main//interface_with_function, inst15 [no loc], unloaded
+// CHECK:STDOUT:   %Main.import_ref.f61: %IF.assoc_type = import_ref Main//interface_with_function, loc3_22, loaded [concrete = constants.%assoc0]
+// CHECK:STDOUT:   %Main.F: %F.type.496 = import_ref Main//interface_with_function, F, loaded [concrete = constants.%F.1de]
+// CHECK:STDOUT:   %Main.import_ref.f57: %IF.type = import_ref Main//interface_with_function, inst15 [no loc], loaded [symbolic = constants.%Self]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: file {
+// CHECK:STDOUT:   package: <namespace> = namespace [concrete] {
+// CHECK:STDOUT:     .IF = imports.%Main.IF
+// CHECK:STDOUT:     .CD = %CD.decl
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %default.import = import <none>
+// CHECK:STDOUT:   %CD.decl: type = class_decl @CD [concrete = constants.%CD] {} {}
+// CHECK:STDOUT:   impl_decl @impl [concrete] {} {
+// CHECK:STDOUT:     %CD.ref: type = name_ref CD, file.%CD.decl [concrete = constants.%CD]
+// CHECK:STDOUT:     %IF.ref: type = name_ref IF, imports.%Main.IF [concrete = constants.%IF.type]
+// CHECK:STDOUT:     %.Self: %IF.type = bind_symbolic_name .Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %.Self.ref: %IF.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %F.ref: %IF.assoc_type = name_ref F, imports.%Main.import_ref.f61 [concrete = constants.%assoc0]
+// CHECK:STDOUT:     %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:     %.loc10_21: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:     %.Self.as_wit: <witness> = facet_access_witness %.Self.ref [symbolic_self = constants.%.Self.as_wit]
+// CHECK:STDOUT:     %impl.elem0: %.99d = impl_witness_access %.Self.as_wit, element0 [symbolic_self = constants.%impl.elem0]
+// CHECK:STDOUT:     %int_0: Core.IntLiteral = int_value 0 [concrete = constants.%int_0]
+// CHECK:STDOUT:     %.loc10_15: type = where_expr %.Self [concrete = constants.%IF_where.type] {
+// CHECK:STDOUT:       requirement_rewrite %impl.elem0, %int_0
+// CHECK:STDOUT:     }
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %impl_witness: <witness> = impl_witness (@impl.%F.decl) [concrete = constants.%impl_witness]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: interface @IF [from "interface_with_function.carbon"] {
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = imports.%Main.import_ref.a2a
+// CHECK:STDOUT:   .F = imports.%Main.import_ref.f61
+// CHECK:STDOUT:   witness = (imports.%Main.F)
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: impl @impl: %CD.ref as %.loc10_15 {
+// CHECK:STDOUT:   %F.decl: %F.type.064 = fn_decl @F.2 [concrete = constants.%F.822] {} {}
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .F = %F.decl
+// CHECK:STDOUT:   witness = file.%impl_witness
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: class @CD {
+// CHECK:STDOUT:   %complete_type: <witness> = complete_type_witness %empty_struct_type [concrete = constants.%complete_type]
+// CHECK:STDOUT:   complete_type_witness = %complete_type
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = constants.%CD
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: generic fn @F.1(imports.%Main.import_ref.f57: %IF.type) [from "interface_with_function.carbon"] {
+// CHECK:STDOUT:   fn();
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: fn @F.2() {
+// CHECK:STDOUT: !entry:
+// CHECK:STDOUT:   return
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @F.1(constants.%Self) {}
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @F.1(constants.%IF.facet.b37) {}
+// CHECK:STDOUT:
diff --git a/toolchain/check/testdata/impl/no_prelude/interface_args.carbon b/toolchain/check/testdata/impl/no_prelude/interface_args.carbon
index a62d66fa05ee0..be3a3ab959638 100644
--- a/toolchain/check/testdata/impl/no_prelude/interface_args.carbon
+++ b/toolchain/check/testdata/impl/no_prelude/interface_args.carbon
@@ -288,13 +288,13 @@ fn MakeC(a: A) -> C {
 // CHECK:STDOUT:   %Main.B: type = import_ref Main//action, B, loaded [concrete = constants.%B]
 // CHECK:STDOUT:   %Main.C = import_ref Main//action, C, unloaded
 // CHECK:STDOUT:   %Main.F = import_ref Main//action, F, unloaded
-// CHECK:STDOUT:   %Main.import_ref.71c: <witness> = import_ref Main//action, loc12_21, loaded [concrete = constants.%impl_witness]
 // CHECK:STDOUT:   %Main.import_ref.8f24d3.1: <witness> = import_ref Main//action, loc9_10, loaded [concrete = constants.%complete_type]
 // CHECK:STDOUT:   %Main.import_ref.54a = import_ref Main//action, inst46 [no loc], unloaded
 // CHECK:STDOUT:   %Main.import_ref.f6b058.1: type = import_ref Main//action, loc4_18, loaded [symbolic = @Action.%T (constants.%T)]
 // CHECK:STDOUT:   %Main.import_ref.ddc = import_ref Main//action, inst26 [no loc], unloaded
 // CHECK:STDOUT:   %Main.import_ref.318: @Action.%Action.assoc_type (%Action.assoc_type.8f9) = import_ref Main//action, loc5_10, loaded [symbolic = @Action.%assoc0 (constants.%assoc0.905ab9.2)]
 // CHECK:STDOUT:   %Main.Op = import_ref Main//action, Op, unloaded
+// CHECK:STDOUT:   %Main.import_ref.71c: <witness> = import_ref Main//action, loc12_21, loaded [concrete = constants.%impl_witness]
 // CHECK:STDOUT:   %Main.import_ref.8f24d3.2: <witness> = import_ref Main//action, loc8_10, loaded [concrete = constants.%complete_type]
 // CHECK:STDOUT:   %Main.import_ref.da3 = import_ref Main//action, inst41 [no loc], unloaded
 // CHECK:STDOUT:   %Main.import_ref.984: type = import_ref Main//action, loc12_6, loaded [concrete = constants.%A]
@@ -446,13 +446,13 @@ fn MakeC(a: A) -> C {
 // CHECK:STDOUT:   %Main.B = import_ref Main//action, B, unloaded
 // CHECK:STDOUT:   %Main.C: type = import_ref Main//action, C, loaded [concrete = constants.%C]
 // CHECK:STDOUT:   %Main.F = import_ref Main//action, F, unloaded
-// CHECK:STDOUT:   %Main.import_ref.7a1 = import_ref Main//action, loc12_21, unloaded
 // CHECK:STDOUT:   %Main.import_ref.8f24d3.1: <witness> = import_ref Main//action, loc9_10, loaded [concrete = constants.%complete_type]
 // CHECK:STDOUT:   %Main.import_ref.54a = import_ref Main//action, inst46 [no loc], unloaded
 // CHECK:STDOUT:   %Main.import_ref.f6b058.1: type = import_ref Main//action, loc4_18, loaded [symbolic = @Action.%T (constants.%T)]
 // CHECK:STDOUT:   %Main.import_ref.ddc = import_ref Main//action, inst26 [no loc], unloaded
 // CHECK:STDOUT:   %Main.import_ref.318: @Action.%Action.assoc_type (%Action.assoc_type.8f9) = import_ref Main//action, loc5_10, loaded [symbolic = @Action.%assoc0 (constants.%assoc0.905ab9.2)]
 // CHECK:STDOUT:   %Main.Op = import_ref Main//action, Op, unloaded
+// CHECK:STDOUT:   %Main.import_ref.7a1 = import_ref Main//action, loc12_21, unloaded
 // CHECK:STDOUT:   %Main.import_ref.8f24d3.2: <witness> = import_ref Main//action, loc8_10, loaded [concrete = constants.%complete_type]
 // CHECK:STDOUT:   %Main.import_ref.da3 = import_ref Main//action, inst41 [no loc], unloaded
 // CHECK:STDOUT:   %Main.import_ref.984: type = import_ref Main//action, loc12_6, loaded [concrete = constants.%A]
@@ -771,13 +771,13 @@ fn MakeC(a: A) -> C {
 // CHECK:STDOUT:   %Main.Factory: %Factory.type.1a8 = import_ref Main//factory, Factory, loaded [concrete = constants.%Factory.generic]
 // CHECK:STDOUT:   %Main.A: type = import_ref Main//factory, A, loaded [concrete = constants.%A]
 // CHECK:STDOUT:   %Main.B: type = import_ref Main//factory, B, loaded [concrete = constants.%B]
-// CHECK:STDOUT:   %Main.import_ref.72b: <witness> = import_ref Main//factory, loc11_22, loaded [concrete = constants.%impl_witness]
 // CHECK:STDOUT:   %Main.import_ref.8f24d3.1: <witness> = import_ref Main//factory, loc9_10, loaded [concrete = constants.%complete_type]
 // CHECK:STDOUT:   %Main.import_ref.54a = import_ref Main//factory, inst52 [no loc], unloaded
 // CHECK:STDOUT:   %Main.import_ref.f6b058.1: type = import_ref Main//factory, loc4_19, loaded [symbolic = @Factory.%T (constants.%T)]
 // CHECK:STDOUT:   %Main.import_ref.fbb = import_ref Main//factory, inst26 [no loc], unloaded
 // CHECK:STDOUT:   %Main.import_ref.8d5: @Factory.%Factory.assoc_type (%Factory.assoc_type.ca7) = import_ref Main//factory, loc5_17, loaded [symbolic = @Factory.%assoc0 (constants.%assoc0.35472f.2)]
 // CHECK:STDOUT:   %Main.Make = import_ref Main//factory, Make, unloaded
+// CHECK:STDOUT:   %Main.import_ref.72b: <witness> = import_ref Main//factory, loc11_22, loaded [concrete = constants.%impl_witness]
 // CHECK:STDOUT:   %Main.import_ref.8f24d3.2: <witness> = import_ref Main//factory, loc8_10, loaded [concrete = constants.%complete_type]
 // CHECK:STDOUT:   %Main.import_ref.da3 = import_ref Main//factory, inst47 [no loc], unloaded
 // CHECK:STDOUT:   %Main.import_ref.984: type = import_ref Main//factory, loc11_6, loaded [concrete = constants.%A]
@@ -935,13 +935,13 @@ fn MakeC(a: A) -> C {
 // CHECK:STDOUT:   %Main.Factory: %Factory.type.1a8 = import_ref Main//factory, Factory, loaded [concrete = constants.%Factory.generic]
 // CHECK:STDOUT:   %Main.A: type = import_ref Main//factory, A, loaded [concrete = constants.%A]
 // CHECK:STDOUT:   %Main.B = import_ref Main//factory, B, unloaded
-// CHECK:STDOUT:   %Main.import_ref.3e9 = import_ref Main//factory, loc11_22, unloaded
 // CHECK:STDOUT:   %Main.import_ref.8f24d3.1: <witness> = import_ref Main//factory, loc9_10, loaded [concrete = constants.%complete_type]
 // CHECK:STDOUT:   %Main.import_ref.54a = import_ref Main//factory, inst52 [no loc], unloaded
 // CHECK:STDOUT:   %Main.import_ref.f6b058.1: type = import_ref Main//factory, loc4_19, loaded [symbolic = @Factory.%T (constants.%T)]
 // CHECK:STDOUT:   %Main.import_ref.fbb = import_ref Main//factory, inst26 [no loc], unloaded
 // CHECK:STDOUT:   %Main.import_ref.8d5: @Factory.%Factory.assoc_type (%Factory.assoc_type.ca7) = import_ref Main//factory, loc5_17, loaded [symbolic = @Factory.%assoc0 (constants.%assoc0.35472f.2)]
 // CHECK:STDOUT:   %Main.Make = import_ref Main//factory, Make, unloaded
+// CHECK:STDOUT:   %Main.import_ref.3e9 = import_ref Main//factory, loc11_22, unloaded
 // CHECK:STDOUT:   %Main.import_ref.8f24d3.2: <witness> = import_ref Main//factory, loc8_10, loaded [concrete = constants.%complete_type]
 // CHECK:STDOUT:   %Main.import_ref.da3 = import_ref Main//factory, inst47 [no loc], unloaded
 // CHECK:STDOUT:   %Main.import_ref.984: type = import_ref Main//factory, loc11_6, loaded [concrete = constants.%A]
diff --git a/toolchain/check/testdata/interface/no_prelude/fail_lookup_undefined.carbon b/toolchain/check/testdata/interface/no_prelude/fail_lookup_undefined.carbon
index 461f8c4dab94b..1869b426c7764 100644
--- a/toolchain/check/testdata/interface/no_prelude/fail_lookup_undefined.carbon
+++ b/toolchain/check/testdata/interface/no_prelude/fail_lookup_undefined.carbon
@@ -20,7 +20,7 @@ interface Undefined;
 fn Undefined.F();
 
 fn Test() {
-  // CHECK:STDERR: fail_lookup_undefined.carbon:[[@LINE+7]]:3: error: member access into undefined interface `Undefined` [QualifiedExprInUndefinedInterfaceScope]
+  // CHECK:STDERR: fail_lookup_undefined.carbon:[[@LINE+7]]:3: error: member access into undefined interface Undefined [ResolveFacetTypeWithUndefinedInterface]
   // CHECK:STDERR:   Undefined.G();
   // CHECK:STDERR:   ^~~~~~~~~~~
   // CHECK:STDERR: fail_lookup_undefined.carbon:[[@LINE-15]]:1: note: interface was forward declared here [InterfaceForwardDeclaredHere]
@@ -31,17 +31,13 @@ fn Test() {
 }
 
 interface BeingDefined {
-  // CHECK:STDERR: fail_lookup_undefined.carbon:[[@LINE+11]]:13: error: member access into undefined interface `BeingDefined` [QualifiedExprInUndefinedInterfaceScope]
+  // CHECK:STDERR: fail_lookup_undefined.carbon:[[@LINE+7]]:13: error: member access into undefined interface BeingDefined [ResolveFacetTypeWithUndefinedInterface]
   // CHECK:STDERR:   fn H() -> BeingDefined.T;
   // CHECK:STDERR:             ^~~~~~~~~~~~~~
   // CHECK:STDERR: fail_lookup_undefined.carbon:[[@LINE-4]]:1: note: interface is currently being defined [InterfaceUndefinedWithinDefinition]
   // CHECK:STDERR: interface BeingDefined {
   // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~
   // CHECK:STDERR:
-  // CHECK:STDERR: fail_lookup_undefined.carbon:[[@LINE+4]]:13: error: member name `T` not found in `BeingDefined` [MemberNameNotFoundInScope]
-  // CHECK:STDERR:   fn H() -> BeingDefined.T;
-  // CHECK:STDERR:             ^~~~~~~~~~~~~~
-  // CHECK:STDERR:
   fn H() -> BeingDefined.T;
   // CHECK:STDERR: fail_lookup_undefined.carbon:[[@LINE+4]]:6: error: name `BeingDefined` not found [NameNotFound]
   // CHECK:STDERR:   fn BeingDefined.I();
@@ -99,7 +95,6 @@ interface BeingDefined {
 // CHECK:STDOUT: !members:
 // CHECK:STDOUT:   .Self = %Self
 // CHECK:STDOUT:   .BeingDefined = <poisoned>
-// CHECK:STDOUT:   .T = <poisoned>
 // CHECK:STDOUT:   .H = %assoc0
 // CHECK:STDOUT:   witness = (%H.decl)
 // CHECK:STDOUT: }
diff --git a/toolchain/check/testdata/struct/import.carbon b/toolchain/check/testdata/struct/import.carbon
index f024d80b4a8d8..699f56f075dad 100644
--- a/toolchain/check/testdata/struct/import.carbon
+++ b/toolchain/check/testdata/struct/import.carbon
@@ -322,7 +322,7 @@ var c_bad: C({.a = 3, .b = 4}) = F();
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %Implicit.import_ref.a11: %struct_type.a.b.5ca = import_ref Implicit//default, loc8_9, loaded [symbolic = @C.%S (constants.%S)]
 // CHECK:STDOUT:   %Implicit.import_ref.8f2: <witness> = import_ref Implicit//default, loc8_34, loaded [concrete = constants.%complete_type.357]
-// CHECK:STDOUT:   %Implicit.import_ref.b8b = import_ref Implicit//default, inst1126 [no loc], unloaded
+// CHECK:STDOUT:   %Implicit.import_ref.b8b = import_ref Implicit//default, inst1147 [no loc], unloaded
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
@@ -497,7 +497,7 @@ var c_bad: C({.a = 3, .b = 4}) = F();
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %Implicit.import_ref.a11: %struct_type.a.b = import_ref Implicit//default, loc8_9, loaded [symbolic = @C.%S (constants.%S)]
 // CHECK:STDOUT:   %Implicit.import_ref.8f2: <witness> = import_ref Implicit//default, loc8_34, loaded [concrete = constants.%complete_type.357]
-// CHECK:STDOUT:   %Implicit.import_ref.b8b = import_ref Implicit//default, inst1126 [no loc], unloaded
+// CHECK:STDOUT:   %Implicit.import_ref.b8b = import_ref Implicit//default, inst1147 [no loc], unloaded
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
@@ -613,7 +613,7 @@ var c_bad: C({.a = 3, .b = 4}) = F();
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %Implicit.import_ref.a11: %struct_type.a.b.5ca = import_ref Implicit//default, loc8_9, loaded [symbolic = @C.%S (constants.%S)]
 // CHECK:STDOUT:   %Implicit.import_ref.8f2: <witness> = import_ref Implicit//default, loc8_34, loaded [concrete = constants.%complete_type.357]
-// CHECK:STDOUT:   %Implicit.import_ref.b8b = import_ref Implicit//default, inst1126 [no loc], unloaded
+// CHECK:STDOUT:   %Implicit.import_ref.b8b = import_ref Implicit//default, inst1147 [no loc], unloaded
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
diff --git a/toolchain/check/testdata/tuple/import.carbon b/toolchain/check/testdata/tuple/import.carbon
index 123bcc9d519c2..ff54fb4546770 100644
--- a/toolchain/check/testdata/tuple/import.carbon
+++ b/toolchain/check/testdata/tuple/import.carbon
@@ -351,7 +351,7 @@ var c_bad: C((3, 4)) = F();
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %Implicit.import_ref.554: %tuple.type.c2c = import_ref Implicit//default, loc7_9, loaded [symbolic = @C.%X (constants.%X)]
 // CHECK:STDOUT:   %Implicit.import_ref.8f2: <witness> = import_ref Implicit//default, loc7_26, loaded [concrete = constants.%complete_type.357]
-// CHECK:STDOUT:   %Implicit.import_ref.964 = import_ref Implicit//default, inst1161 [no loc], unloaded
+// CHECK:STDOUT:   %Implicit.import_ref.964 = import_ref Implicit//default, inst1182 [no loc], unloaded
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
@@ -542,7 +542,7 @@ var c_bad: C((3, 4)) = F();
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %Implicit.import_ref.554: %tuple.type.c2c = import_ref Implicit//default, loc7_9, loaded [symbolic = @C.%X (constants.%X)]
 // CHECK:STDOUT:   %Implicit.import_ref.8f2: <witness> = import_ref Implicit//default, loc7_26, loaded [concrete = constants.%complete_type.357]
-// CHECK:STDOUT:   %Implicit.import_ref.964 = import_ref Implicit//default, inst1161 [no loc], unloaded
+// CHECK:STDOUT:   %Implicit.import_ref.964 = import_ref Implicit//default, inst1182 [no loc], unloaded
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
@@ -659,7 +659,7 @@ var c_bad: C((3, 4)) = F();
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %Implicit.import_ref.554: %tuple.type.c2c = import_ref Implicit//default, loc7_9, loaded [symbolic = @C.%X (constants.%X)]
 // CHECK:STDOUT:   %Implicit.import_ref.8f2: <witness> = import_ref Implicit//default, loc7_26, loaded [concrete = constants.%complete_type.357]
-// CHECK:STDOUT:   %Implicit.import_ref.964 = import_ref Implicit//default, inst1161 [no loc], unloaded
+// CHECK:STDOUT:   %Implicit.import_ref.964 = import_ref Implicit//default, inst1182 [no loc], unloaded
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
diff --git a/toolchain/check/type.cpp b/toolchain/check/type.cpp
index 83beb66706cab..9e54c936a4b6b 100644
--- a/toolchain/check/type.cpp
+++ b/toolchain/check/type.cpp
@@ -5,6 +5,7 @@
 #include "toolchain/check/type.h"
 
 #include "toolchain/check/eval.h"
+#include "toolchain/check/facet_type.h"
 #include "toolchain/check/type_completion.h"
 
 namespace Carbon::Check {
@@ -19,15 +20,6 @@ static auto GetTypeImpl(Context& context, EachArgT... each_arg)
       TryEvalInst(context, SemIR::InstId::None, inst));
 }
 
-auto FacetTypeFromInterface(Context& context, SemIR::InterfaceId interface_id,
-                            SemIR::SpecificId specific_id) -> SemIR::FacetType {
-  SemIR::FacetTypeId facet_type_id = context.facet_types().Add(
-      SemIR::FacetTypeInfo{.impls_constraints = {{interface_id, specific_id}},
-                           .other_requirements = false});
-  return {.type_id = SemIR::TypeType::SingletonTypeId,
-          .facet_type_id = facet_type_id};
-}
-
 // Gets or forms a type_id for a type, given the instruction kind and arguments,
 // and completes the type. This should only be used when type completion cannot
 // fail.
diff --git a/toolchain/check/type.h b/toolchain/check/type.h
index 260dc853228e1..8d7f7ee77055b 100644
--- a/toolchain/check/type.h
+++ b/toolchain/check/type.h
@@ -11,11 +11,6 @@
 
 namespace Carbon::Check {
 
-// Create a FacetType typed instruction object consisting of a single
-// interface.
-auto FacetTypeFromInterface(Context& context, SemIR::InterfaceId interface_id,
-                            SemIR::SpecificId specific_id) -> SemIR::FacetType;
-
 // Gets the type to use for an unbound associated entity declared in this
 // interface. For example, this is the type of `I.T` after
 // `interface I { let T:! type; }`. The name of the interface is used for
diff --git a/toolchain/check/type_completion.cpp b/toolchain/check/type_completion.cpp
index 887a844bf432a..3892cac8131b8 100644
--- a/toolchain/check/type_completion.cpp
+++ b/toolchain/check/type_completion.cpp
@@ -9,6 +9,7 @@
 #include "toolchain/check/generic.h"
 #include "toolchain/check/inst.h"
 #include "toolchain/check/type.h"
+#include "toolchain/diagnostics/format_providers.h"
 
 namespace Carbon::Check {
 
@@ -25,6 +26,9 @@ namespace {
 // - A `BuildValueRepr` step computes the value representation for a
 //   type, once all of its nested types are complete, and marks the type as
 //   complete.
+//
+// TODO: Extend this to support computing other properties of types, like
+// being concrete.
 class TypeCompleter {
  public:
   TypeCompleter(Context& context, SemIRLoc loc,
@@ -519,12 +523,15 @@ auto RequireConcreteType(Context& context, SemIR::TypeId type_id,
                          Context::BuildDiagnosticFn diagnoser,
                          Context::BuildDiagnosticFn abstract_diagnoser)
     -> bool {
+  // TODO: For symbolic types, should add a RequireConcreteType instruction,
+  // like RequireCompleteType.
   CARBON_CHECK(abstract_diagnoser);
 
   if (!RequireCompleteType(context, type_id, loc_id, diagnoser)) {
     return false;
   }
 
+  // TODO: This doesn't properly handle tuples and structs.
   if (auto class_type = context.types().TryGetAs<SemIR::ClassType>(type_id)) {
     auto& class_info = context.classes().Get(class_type->class_id);
     if (class_info.inheritance_kind !=
@@ -544,46 +551,68 @@ auto RequireConcreteType(Context& context, SemIR::TypeId type_id,
   return true;
 }
 
-auto RequireDefinedType(Context& context, SemIR::TypeId type_id,
-                        SemIR::LocId loc_id,
-                        Context::BuildDiagnosticFn diagnoser) -> bool {
-  if (!RequireCompleteType(context, type_id, loc_id, diagnoser)) {
-    return false;
-  }
-
-  if (auto facet_type = context.types().TryGetAs<SemIR::FacetType>(type_id)) {
-    const auto& facet_type_info =
-        context.facet_types().Get(facet_type->facet_type_id);
-    for (auto interface : facet_type_info.impls_constraints) {
-      auto interface_id = interface.interface_id;
-      if (!context.interfaces().Get(interface_id).is_defined()) {
-        auto builder = diagnoser();
-        NoteUndefinedInterface(context, interface_id, builder);
-        builder.Emit();
-        return false;
-      }
+static auto AddCompleteFacetType(Context& context, SemIR::LocId loc_id,
+                                 const SemIR::FacetTypeInfo& facet_type_info,
+                                 FacetTypeContext context_for_diagnostics)
+    -> SemIR::CompleteFacetTypeId {
+  SemIR::CompleteFacetType result;
+  result.required_interfaces.reserve(facet_type_info.impls_constraints.size());
+  // Every mentioned interface needs to be defined.
+  for (auto impl_interface : facet_type_info.impls_constraints) {
+    // TODO: expand named constraints
+    auto interface_id = impl_interface.interface_id;
+    const auto& interface = context.interfaces().Get(interface_id);
+    if (!interface.is_defined()) {
+      CARBON_DIAGNOSTIC(
+          ResolveFacetTypeWithUndefinedInterface, Error,
+          "{0:=0:member access into|=1:impl of} undefined interface {1}",
+          IntAsSelect, SemIR::NameId);
+      auto builder = context.emitter().Build(
+          loc_id, ResolveFacetTypeWithUndefinedInterface,
+          static_cast<int>(context_for_diagnostics), interface.name_id);
+      NoteUndefinedInterface(context, interface_id, builder);
+      builder.Emit();
+      return SemIR::CompleteFacetTypeId::None;
+    }
 
-      if (interface.specific_id.has_value()) {
-        ResolveSpecificDefinition(context, loc_id, interface.specific_id);
-      }
+    if (impl_interface.specific_id.has_value()) {
+      ResolveSpecificDefinition(context, loc_id, impl_interface.specific_id);
     }
-    // TODO: Finish facet type resolution.
-    //
-    // Note that we will need Self to be passed into facet type resolution.
-    // The `.Self` of a facet type created by `where` will then be bound to the
-    // provided self type.
-    //
-    // For example, in `T:! X where ...`, we will bind the `.Self` of the
-    // `where` facet type to `T`, and in `(X where ...) where ...`, we will bind
-    // the inner `.Self` to the outer `.Self`.
-    //
-    // If the facet type contains a rewrite, we may have deferred converting the
-    // rewritten value to the type of the associated constant. That conversion
-    // should also be performed as part of resolution, and may depend on the
-    // Self type.
+    result.required_interfaces.push_back(
+        {.interface_id = interface_id,
+         .specific_id = impl_interface.specific_id});
+  }
+  // TODO: Sort and deduplicate result.required_interfaces. For now, we have at
+  // most one.
+  CARBON_CHECK(result.required_interfaces.size() <= 1);
+
+  // TODO: Distinguish interfaces that are required but would not be
+  // implemented, such as those from `where .Self impls I`.
+  result.num_to_impl = result.required_interfaces.size();
+  return context.complete_facet_types().Add(result);
+}
+
+// TODO: RequireCompleteType should do these checks, this should just return
+// additional information.
+auto RequireCompleteFacetType(Context& context, SemIR::TypeId type_id,
+                              SemIR::LocId loc_id,
+                              const SemIR::FacetType& facet_type,
+                              FacetTypeContext context_for_diagnostics)
+    -> SemIR::CompleteFacetTypeId {
+  if (!RequireCompleteType(
+          context, type_id, loc_id, [&]() -> Context::DiagnosticBuilder {
+            CARBON_FATAL("Unreachable, facet types are always complete.");
+          })) {
+    return SemIR::CompleteFacetTypeId::None;
   }
 
-  return true;
+  auto& facet_type_info =
+      context.facet_types().GetMutable(facet_type.facet_type_id);
+  if (!facet_type_info.complete_id.has_value()) {
+    facet_type_info.complete_id = AddCompleteFacetType(
+        context, loc_id, facet_type_info, context_for_diagnostics);
+  }
+  return facet_type_info.complete_id;
 }
 
 auto AsCompleteType(Context& context, SemIR::TypeId type_id,
diff --git a/toolchain/check/type_completion.h b/toolchain/check/type_completion.h
index 64e5d9bca09f0..923c99ffca231 100644
--- a/toolchain/check/type_completion.h
+++ b/toolchain/check/type_completion.h
@@ -48,15 +48,17 @@ auto RequireConcreteType(Context& context, SemIR::TypeId type_id,
                          Context::BuildDiagnosticFn diagnoser,
                          Context::BuildDiagnosticFn abstract_diagnoser) -> bool;
 
-// Like `RequireCompleteType`, but also require the type to be defined. A
-// defined type has known members. If the type is not defined, `diagnoser` is
-// used to diagnose the problem, and this function returns false.
-//
-// This is the same as `RequireCompleteType` except for facet types, which are
-// complete before they are fully defined.
-auto RequireDefinedType(Context& context, SemIR::TypeId type_id,
-                        SemIR::LocId loc_id,
-                        Context::BuildDiagnosticFn diagnoser) -> bool;
+// Like `RequireCompleteType`, but also require the facet type to be fully
+// defined with known members. If it uses some incomplete interface, diagnoses
+// the problem and returns None.
+// TODO: Get rid of this enum and use the `RequireCompleteType` diagnostic
+// mechanism instead.
+enum FacetTypeContext { FacetTypeMemberAccess, FacetTypeImpl };
+auto RequireCompleteFacetType(Context& context, SemIR::TypeId type_id,
+                              SemIR::LocId loc_id,
+                              const SemIR::FacetType& facet_type,
+                              FacetTypeContext context_for_diagnostics)
+    -> SemIR::CompleteFacetTypeId;
 
 // Returns the type `type_id` if it is a complete type, or produces an
 // incomplete type error and returns an error type. This is a convenience
diff --git a/toolchain/diagnostics/diagnostic_kind.def b/toolchain/diagnostics/diagnostic_kind.def
index 41de887da5000..33b198dcaa2b0 100644
--- a/toolchain/diagnostics/diagnostic_kind.def
+++ b/toolchain/diagnostics/diagnostic_kind.def
@@ -275,7 +275,6 @@ CARBON_DIAGNOSTIC_KIND(VarInInterfaceDecl)
 
 // Impl checking.
 CARBON_DIAGNOSTIC_KIND(AssociatedConstantHere)
-CARBON_DIAGNOSTIC_KIND(AssociatedConstantNotConstantAfterConversion)
 CARBON_DIAGNOSTIC_KIND(AssociatedFunctionHere)
 CARBON_DIAGNOSTIC_KIND(ExtendImplForall)
 CARBON_DIAGNOSTIC_KIND(ExtendImplOutsideClass)
@@ -286,12 +285,12 @@ CARBON_DIAGNOSTIC_KIND(ImplAsNonFacetType)
 CARBON_DIAGNOSTIC_KIND(ImplAsOutsideClass)
 CARBON_DIAGNOSTIC_KIND(ImplAssociatedConstantNeedsValue)
 CARBON_DIAGNOSTIC_KIND(ImplFunctionWithNonFunction)
+CARBON_DIAGNOSTIC_KIND(ImplLookupCycle)
 CARBON_DIAGNOSTIC_KIND(ImplMissingDefinition)
 CARBON_DIAGNOSTIC_KIND(ImplMissingFunction)
 CARBON_DIAGNOSTIC_KIND(ImplPreviousDefinition)
 CARBON_DIAGNOSTIC_KIND(ImplRedefinition)
-CARBON_DIAGNOSTIC_KIND(ImplOfUndefinedInterface)
-CARBON_DIAGNOSTIC_KIND(ImplLookupCycle)
+CARBON_DIAGNOSTIC_KIND(ImplOfNotOneInterface)
 
 // Impl lookup.
 CARBON_DIAGNOSTIC_KIND(MissingImplInMemberAccess)
@@ -409,7 +408,6 @@ CARBON_DIAGNOSTIC_KIND(UnexpectedDeclNameParams)
 CARBON_DIAGNOSTIC_KIND(QualifiedNameInNonScope)
 CARBON_DIAGNOSTIC_KIND(QualifiedNameNonScopeEntity)
 CARBON_DIAGNOSTIC_KIND(QualifiedExprInIncompleteClassScope)
-CARBON_DIAGNOSTIC_KIND(QualifiedExprInUndefinedInterfaceScope)
 CARBON_DIAGNOSTIC_KIND(QualifiedExprUnsupported)
 CARBON_DIAGNOSTIC_KIND(QualifiedExprNameNotFound)
 CARBON_DIAGNOSTIC_KIND(UseOfNonExprAsValue)
@@ -440,10 +438,15 @@ CARBON_DIAGNOSTIC_KIND(ClassInvalidMemberAccess)
 CARBON_DIAGNOSTIC_KIND(AliasRequiresNameRef)
 
 // Where operator and its requirements.
-CARBON_DIAGNOSTIC_KIND(AssociatedConstantWithDifferentValues)
 CARBON_DIAGNOSTIC_KIND(ImplsOnNonFacetType)
 CARBON_DIAGNOSTIC_KIND(WhereOnNonFacetType)
 
+// Facet type resolution
+CARBON_DIAGNOSTIC_KIND(AssociatedConstantNotConstantAfterConversion)
+CARBON_DIAGNOSTIC_KIND(AssociatedConstantWithDifferentValues)
+CARBON_DIAGNOSTIC_KIND(RewriteForAssociatedFunction)
+CARBON_DIAGNOSTIC_KIND(ResolveFacetTypeWithUndefinedInterface)
+
 // ============================================================================
 // Language server diagnostics
 // ============================================================================
diff --git a/toolchain/sem_ir/dump.cpp b/toolchain/sem_ir/dump.cpp
index b28e634810303..f43e19e13dea0 100644
--- a/toolchain/sem_ir/dump.cpp
+++ b/toolchain/sem_ir/dump.cpp
@@ -39,7 +39,7 @@ static auto DumpNoNewline(const File& file, InstId inst_id) -> void {
 static auto DumpNoNewline(const File& file, InterfaceId interface_id) -> void {
   llvm::errs() << interface_id;
   if (interface_id.has_value()) {
-    auto interface = file.interfaces().Get(interface_id);
+    const auto& interface = file.interfaces().Get(interface_id);
     llvm::errs() << ": " << interface;
     DumpNameIfValid(file, interface.name_id);
   }
@@ -55,7 +55,7 @@ static auto DumpNoNewline(const File& file, SpecificId specific_id) -> void {
 LLVM_DUMP_METHOD auto Dump(const File& file, ClassId class_id) -> void {
   llvm::errs() << class_id;
   if (class_id.has_value()) {
-    auto class_obj = file.classes().Get(class_id);
+    const auto& class_obj = file.classes().Get(class_id);
     llvm::errs() << ": " << class_obj;
     DumpNameIfValid(file, class_obj.name_id);
   }
@@ -82,30 +82,36 @@ LLVM_DUMP_METHOD auto Dump(const File& file, FacetTypeId facet_type_id)
     -> void {
   llvm::errs() << facet_type_id;
   if (facet_type_id.has_value()) {
-    auto facet_type = file.facet_types().Get(facet_type_id);
-    llvm::errs() << ": " << facet_type;
+    const auto& facet_type = file.facet_types().Get(facet_type_id);
+    llvm::errs() << ": " << facet_type << '\n';
     for (auto impls : facet_type.impls_constraints) {
-      llvm::errs() << "\n  - ";
+      llvm::errs() << "  - ";
       DumpNoNewline(file, impls.interface_id);
       if (impls.specific_id.has_value()) {
         llvm::errs() << "; ";
         DumpNoNewline(file, impls.specific_id);
       }
+      llvm::errs() << '\n';
     }
     for (auto rewrite : facet_type.rewrite_constraints) {
-      llvm::errs() << "\n  - ";
-      DumpNoNewline(file, rewrite.lhs_const_id);
-      llvm::errs() << "\n  - ";
-      DumpNoNewline(file, rewrite.rhs_const_id);
+      llvm::errs() << "  - ";
+      Dump(file, rewrite.lhs_const_id);
+      llvm::errs() << "  - ";
+      Dump(file, rewrite.rhs_const_id);
+    }
+    if (facet_type.complete_id.has_value()) {
+      llvm::errs() << "complete: ";
+      Dump(file, facet_type.complete_id);
     }
+  } else {
+    llvm::errs() << '\n';
   }
-  llvm::errs() << '\n';
 }
 
 LLVM_DUMP_METHOD auto Dump(const File& file, FunctionId function_id) -> void {
   llvm::errs() << function_id;
   if (function_id.has_value()) {
-    auto function = file.functions().Get(function_id);
+    const auto& function = file.functions().Get(function_id);
     llvm::errs() << ": " << function;
     DumpNameIfValid(file, function.name_id);
   }
@@ -179,7 +185,7 @@ LLVM_DUMP_METHOD auto Dump(const File& file, NameScopeId name_scope_id)
     -> void {
   llvm::errs() << name_scope_id;
   if (name_scope_id.has_value()) {
-    auto name_scope = file.name_scopes().Get(name_scope_id);
+    const auto& name_scope = file.name_scopes().Get(name_scope_id);
     llvm::errs() << ": " << name_scope;
     if (name_scope.inst_id().has_value()) {
       llvm::errs() << " " << file.insts().Get(name_scope.inst_id());
@@ -189,6 +195,28 @@ LLVM_DUMP_METHOD auto Dump(const File& file, NameScopeId name_scope_id)
   llvm::errs() << '\n';
 }
 
+LLVM_DUMP_METHOD auto Dump(const File& file,
+                           CompleteFacetTypeId complete_facet_type_id) -> void {
+  llvm::errs() << complete_facet_type_id << "\n";
+  if (complete_facet_type_id.has_value()) {
+    const auto& complete_facet_type =
+        file.complete_facet_types().Get(complete_facet_type_id);
+    for (auto [i, req_interface] :
+         llvm::enumerate(complete_facet_type.required_interfaces)) {
+      llvm::errs() << "  - ";
+      DumpNoNewline(file, req_interface.interface_id);
+      if (req_interface.specific_id.has_value()) {
+        llvm::errs() << "; ";
+        DumpNoNewline(file, req_interface.specific_id);
+      }
+      if (static_cast<int>(i) < complete_facet_type.num_to_impl) {
+        llvm::errs() << " (to impl)";
+      }
+      llvm::errs() << '\n';
+    }
+  }
+}
+
 LLVM_DUMP_METHOD auto Dump(const File& file, SpecificId specific_id) -> void {
   DumpNoNewline(file, specific_id);
   llvm::errs() << '\n';
@@ -273,6 +301,10 @@ LLVM_DUMP_METHOD static auto MakeNameId(int id) -> NameId { return NameId(id); }
 LLVM_DUMP_METHOD static auto MakeNameScopeId(int id) -> NameScopeId {
   return NameScopeId(id);
 }
+LLVM_DUMP_METHOD static auto MakeCompleteFacetTypeId(int id)
+    -> CompleteFacetTypeId {
+  return CompleteFacetTypeId(id);
+}
 LLVM_DUMP_METHOD static auto MakeSpecificId(int id) -> SpecificId {
   return SpecificId(id);
 }
diff --git a/toolchain/sem_ir/dump.h b/toolchain/sem_ir/dump.h
index 2606bce424710..c0a674ee0fa01 100644
--- a/toolchain/sem_ir/dump.h
+++ b/toolchain/sem_ir/dump.h
@@ -32,6 +32,7 @@ auto Dump(const File& file, InstId inst_id) -> void;
 auto Dump(const File& file, InterfaceId interface_id) -> void;
 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, StructTypeFieldsId struct_type_fields_id) -> void;
 auto Dump(const File& file, TypeBlockId type_block_id) -> void;
diff --git a/toolchain/sem_ir/facet_type_info.cpp b/toolchain/sem_ir/facet_type_info.cpp
index 21d73dadb35c7..7843c76caec54 100644
--- a/toolchain/sem_ir/facet_type_info.cpp
+++ b/toolchain/sem_ir/facet_type_info.cpp
@@ -6,15 +6,30 @@
 
 namespace Carbon::SemIR {
 
-template <typename VecT>
-static auto SortAndDeduplicate(VecT& vec) -> void {
-  llvm::sort(vec);
+template <typename VecT, typename CompareT>
+static auto SortAndDeduplicate(VecT& vec, CompareT compare) -> void {
+  llvm::sort(vec, compare);
   vec.erase(llvm::unique(vec), vec.end());
 }
 
+// Canonically ordered by the numerical ids.
+static auto ImplsLess(const FacetTypeInfo::ImplsConstraint& lhs,
+                      const FacetTypeInfo::ImplsConstraint& rhs) -> bool {
+  return std::tie(lhs.interface_id.index, lhs.specific_id.index) <
+         std::tie(rhs.interface_id.index, rhs.specific_id.index);
+}
+
+// Canonically ordered by the numerical ids.
+static auto RewriteLess(const FacetTypeInfo::RewriteConstraint& lhs,
+                        const FacetTypeInfo::RewriteConstraint& rhs) -> bool {
+  return std::tie(lhs.lhs_const_id.index, lhs.rhs_const_id.index) <
+         std::tie(rhs.lhs_const_id.index, rhs.rhs_const_id.index);
+}
+
 auto FacetTypeInfo::Canonicalize() -> void {
-  SortAndDeduplicate(impls_constraints);
-  SortAndDeduplicate(rewrite_constraints);
+  CARBON_CHECK(!complete_id.has_value());
+  SortAndDeduplicate(impls_constraints, ImplsLess);
+  SortAndDeduplicate(rewrite_constraints, RewriteLess);
 }
 
 auto FacetTypeInfo::Print(llvm::raw_ostream& out) const -> void {
@@ -43,6 +58,10 @@ auto FacetTypeInfo::Print(llvm::raw_ostream& out) const -> void {
   if (other_requirements) {
     out << outer_sep << "+ TODO requirements";
   }
+
+  if (complete_id.has_value()) {
+    out << outer_sep << "complete: " << complete_id;
+  }
   out << "}";
 }
 
diff --git a/toolchain/sem_ir/facet_type_info.h b/toolchain/sem_ir/facet_type_info.h
index da6cb06961bac..2ebc263db55ab 100644
--- a/toolchain/sem_ir/facet_type_info.h
+++ b/toolchain/sem_ir/facet_type_info.h
@@ -11,6 +11,19 @@
 
 namespace Carbon::SemIR {
 
+struct SpecificInterface {
+  InterfaceId interface_id;
+  SpecificId specific_id;
+
+  static const SpecificInterface None;
+
+  friend auto operator==(const SpecificInterface& lhs,
+                         const SpecificInterface& rhs) -> bool = default;
+};
+
+constexpr SpecificInterface SpecificInterface::None = {
+    .interface_id = InterfaceId::None, .specific_id = SpecificId::None};
+
 struct FacetTypeInfo : Printable<FacetTypeInfo> {
   // TODO: Need to switch to a processed, canonical form, that can support facet
   // type equality as defined by
@@ -20,27 +33,11 @@ struct FacetTypeInfo : Printable<FacetTypeInfo> {
   // `llvm::BumpPtrAllocator`.
 
   // `ImplsConstraint` holds the interfaces this facet type requires.
-  struct ImplsConstraint {
-    // TODO: extend this so it can represent named constraint requirements
-    // and requirements on members, not just `.Self`.
-    // TODO: Add whether this is a lookup context. Those that are should sort
-    // first for easy access. Right now, all are assumed to be lookup contexts.
-    InterfaceId interface_id;
-    SpecificId specific_id;
-
-    friend auto operator==(const ImplsConstraint& lhs,
-                           const ImplsConstraint& rhs) -> bool {
-      return lhs.interface_id == rhs.interface_id &&
-             lhs.specific_id == rhs.specific_id;
-    }
-    // Canonically ordered by the numerical ids.
-    friend auto operator<=>(const ImplsConstraint& lhs,
-                            const ImplsConstraint& rhs)
-        -> std::strong_ordering {
-      return std::tie(lhs.interface_id.index, lhs.specific_id.index) <=>
-             std::tie(rhs.interface_id.index, rhs.specific_id.index);
-    }
-  };
+  // TODO: extend this so it can represent named constraint requirements
+  // and requirements on members, not just `.Self`.
+  // TODO: Add whether this is a lookup context. Those that are should sort
+  // first for easy access. Right now, all are assumed to be lookup contexts.
+  using ImplsConstraint = SpecificInterface;
   llvm::SmallVector<ImplsConstraint> impls_constraints;
 
   // Rewrite constraints of the form `.T = U`
@@ -48,27 +45,25 @@ struct FacetTypeInfo : Printable<FacetTypeInfo> {
     ConstantId lhs_const_id;
     ConstantId rhs_const_id;
 
+    static const RewriteConstraint None;
+
     friend auto operator==(const RewriteConstraint& lhs,
-                           const RewriteConstraint& rhs) -> bool {
-      return lhs.lhs_const_id == rhs.lhs_const_id &&
-             lhs.rhs_const_id == rhs.rhs_const_id;
-    }
-    // Canonically ordered by the numerical ids.
-    friend auto operator<=>(const RewriteConstraint& lhs,
-                            const RewriteConstraint& rhs)
-        -> std::strong_ordering {
-      return std::tie(lhs.lhs_const_id.index, lhs.rhs_const_id.index) <=>
-             std::tie(rhs.lhs_const_id.index, rhs.rhs_const_id.index);
-    }
+                           const RewriteConstraint& rhs) -> bool = default;
   };
   llvm::SmallVector<RewriteConstraint> rewrite_constraints;
 
   // TODO: Add same-type constraints.
   // TODO: Remove once all requirements are supported.
   bool other_requirements;
-  // TODO: Add optional resolved facet type.
 
-  // Sorts and deduplicates constraints.
+  // This is should be `None` for new facet type values, and only set as a
+  // private implementation detail of `RequireCompleteFacetType`. It is stored
+  // here so that we only compute its value once per facet type. This is not
+  // part of the value of the facet type, excluded from `==` and its hash value.
+  CompleteFacetTypeId complete_id = CompleteFacetTypeId::None;
+
+  // Sorts and deduplicates constraints. Call after building the value, and then
+  // don't mutate this value afterwards.
   auto Canonicalize() -> void;
 
   auto Print(llvm::raw_ostream& out) const -> void;
@@ -92,6 +87,27 @@ struct FacetTypeInfo : Printable<FacetTypeInfo> {
   }
 };
 
+constexpr FacetTypeInfo::RewriteConstraint
+    FacetTypeInfo::RewriteConstraint::None = {.lhs_const_id = ConstantId::None,
+                                              .rhs_const_id = ConstantId::None};
+
+struct CompleteFacetType {
+  // TODO: Add additional fields, for example to support types other than
+  // `.Self` implementation requirements.
+  using RequiredInterface = SpecificInterface;
+
+  // Interfaces mentioned explicitly in the facet type expression, or
+  // transitively through a named constraint.
+  llvm::SmallVector<RequiredInterface> required_interfaces;
+
+  // Number of interfaces from `interfaces` to implement if this is the facet
+  // type to the right of an `impl`...`as`. Invalid to use in that position
+  // unless this value is 1.
+  int num_to_impl;
+
+  // TODO: Which interfaces to perform name lookup into.
+};
+
 // See common/hashing.h.
 inline auto CarbonHashValue(const FacetTypeInfo& value, uint64_t seed)
     -> HashCode {
@@ -99,6 +115,7 @@ inline auto CarbonHashValue(const FacetTypeInfo& value, uint64_t seed)
   hasher.HashSizedBytes(llvm::ArrayRef(value.impls_constraints));
   hasher.HashSizedBytes(llvm::ArrayRef(value.rewrite_constraints));
   hasher.HashRaw(value.other_requirements);
+  // `complete_id` is not part of the state to hash.
   return static_cast<HashCode>(hasher);
 }
 
diff --git a/toolchain/sem_ir/file.h b/toolchain/sem_ir/file.h
index dee93e92eae57..34ae53b72b285 100644
--- a/toolchain/sem_ir/file.h
+++ b/toolchain/sem_ir/file.h
@@ -156,6 +156,12 @@ class File : public Printable<File> {
   auto facet_types() const -> const CanonicalValueStore<FacetTypeId>& {
     return facet_types_;
   }
+  auto complete_facet_types() -> ValueStore<CompleteFacetTypeId>& {
+    return complete_facet_types_;
+  }
+  auto complete_facet_types() const -> const ValueStore<CompleteFacetTypeId>& {
+    return complete_facet_types_;
+  }
   auto impls() -> ImplStore& { return impls_; }
   auto impls() const -> const ImplStore& { return impls_; }
   auto generics() -> GenericStore& { return generics_; }
@@ -269,6 +275,9 @@ class File : public Printable<File> {
   // Storage for facet types.
   CanonicalValueStore<FacetTypeId> facet_types_;
 
+  // Storage for complete facet types.
+  ValueStore<CompleteFacetTypeId> complete_facet_types_;
+
   // Storage for impls.
   ImplStore impls_;
 
diff --git a/toolchain/sem_ir/ids.h b/toolchain/sem_ir/ids.h
index 79e4076f57dbc..fa285936c2e94 100644
--- a/toolchain/sem_ir/ids.h
+++ b/toolchain/sem_ir/ids.h
@@ -25,6 +25,7 @@ struct ExprRegion;
 struct FacetTypeInfo;
 struct Function;
 struct Generic;
+struct CompleteFacetType;
 struct Specific;
 struct ImportCpp;
 struct ImportIR;
@@ -265,7 +266,7 @@ struct AssociatedConstantId : public IdBase<AssociatedConstantId> {
   static constexpr llvm::StringLiteral Label = "assoc_const";
   using ValueType = AssociatedConstant;
 
-  // An explicitly invalid ID.
+  // An ID with no value.
   static const AssociatedConstantId None;
 
   using IdBase::IdBase;
@@ -287,6 +288,20 @@ struct FacetTypeId : public IdBase<FacetTypeId> {
 
 constexpr FacetTypeId FacetTypeId::None = FacetTypeId(NoneIndex);
 
+// The ID of an resolved faceet type value.
+struct CompleteFacetTypeId : public IdBase<CompleteFacetTypeId> {
+  static constexpr llvm::StringLiteral Label = "complete_facet_type";
+  using ValueType = CompleteFacetType;
+
+  // An ID with no value.
+  static const CompleteFacetTypeId None;
+
+  using IdBase::IdBase;
+};
+
+constexpr CompleteFacetTypeId CompleteFacetTypeId::None =
+    CompleteFacetTypeId(NoneIndex);
+
 // The ID of an impl.
 struct ImplId : public IdBase<ImplId> {
   static constexpr llvm::StringLiteral Label = "impl";
diff --git a/toolchain/sem_ir/impl.h b/toolchain/sem_ir/impl.h
index 1203f55fb3b1a..6c006190c0431 100644
--- a/toolchain/sem_ir/impl.h
+++ b/toolchain/sem_ir/impl.h
@@ -8,19 +8,29 @@
 #include "common/map.h"
 #include "toolchain/base/value_store.h"
 #include "toolchain/sem_ir/entity_with_params_base.h"
+#include "toolchain/sem_ir/facet_type_info.h"
 #include "toolchain/sem_ir/ids.h"
 
 namespace Carbon::SemIR {
 
 struct ImplFields {
-  // The following members always have values, and do not change throughout the
-  // lifetime of the interface.
+  // This following members always have values and do not change.
 
   // The type for which the impl is implementing a constraint.
   InstId self_id;
   // The constraint that the impl implements.
   InstId constraint_id;
 
+  // The single interface to implement from `constraint_id`.
+  // The members are `None` if `constraint_id` isn't complete or doesn't
+  // correspond to a single interface.
+  SemIR::SpecificInterface interface;
+
+  // The witness for the impl. This can be `BuiltinErrorInst` or an import
+  // reference. Note that the entries in the witness are updated at the end of
+  // the impl definition.
+  InstId witness_id = InstId::None;
+
   // The following members are set at the `{` of the impl definition.
 
   // The impl scope.
@@ -28,10 +38,6 @@ struct ImplFields {
   // The first block of the impl body.
   // TODO: Handle control flow in the impl body, such as if-expressions.
   InstBlockId body_block_id = InstBlockId::None;
-  // The witness for the impl. This can be `BuiltinErrorInst` or an import
-  // reference. Note that the entries in the witness are updated at the end of
-  // the impl definition.
-  InstId witness_id = InstId::None;
 
   // The following members are set at the `}` of the impl definition.
   bool defined = false;