Import contained RequireImpls when importing an Interface or NamedConstraint (#6344)

When importing an Interface or NamedConstraint, walk the block of
`RequireImplsId`s, and for each one:
- Import the RequireImplsDecl from it, which also imports the
`RequireImpls` structure and its id.
- Collect those decls and build a block of `RequireImplsId`s for the
local SemIR to reference from the Interface or NamedConstraint.

The import of RequireImplsDecl is done in a single phase instead of
three, unlike other decls. This is possible since require declarations
have no name, so they can't be referenced by instructions inside them,
thus there's no cycles to concern ourselves with.

toolchain/check/handle_require.cpp

@@ -253,7 +253,6 @@ auto HandleParseNode(Context& context, Parse::RequireDeclId node_id) -> bool {
        .facet_type_id = constraint_facet_type.facet_type_id,
        .decl_id = decl_id,
        .parent_scope_id = context.scope_stack().PeekNameScopeId(),
-       .body_block_id = decl_block_id,
        .generic_id = BuildGenericDecl(context, decl_id)});
 
   require_impls_decl.require_impls_id = require_impls_id;

toolchain/check/import_ref.cpp

@@ -32,6 +32,7 @@
 #include "toolchain/sem_ir/inst_kind.h"
 #include "toolchain/sem_ir/name_scope.h"
 #include "toolchain/sem_ir/specific_interface.h"
+#include "toolchain/sem_ir/specific_named_constraint.h"
 #include "toolchain/sem_ir/type_info.h"
 #include "toolchain/sem_ir/typed_insts.h"
 
@@ -212,6 +213,12 @@ class ImportContext {
   auto import_name_scopes() -> const SemIR::NameScopeStore& {
     return import_ir().name_scopes();
   }
+  auto import_require_impls() -> const SemIR::RequireImplsStore& {
+    return import_ir().require_impls();
+  }
+  auto import_require_impls_blocks() -> const SemIR::RequireImplsBlockStore& {
+    return import_ir().require_impls_blocks();
+  }
   auto import_specifics() -> const SemIR::SpecificStore& {
     return import_ir().specifics();
   }
@@ -288,6 +295,12 @@ class ImportContext {
   auto local_name_scopes() -> SemIR::NameScopeStore& {
     return local_ir().name_scopes();
   }
+  auto local_require_impls() -> SemIR::RequireImplsStore& {
+    return local_ir().require_impls();
+  }
+  auto local_require_impls_blocks() -> SemIR::RequireImplsBlockStore& {
+    return local_ir().require_impls_blocks();
+  }
   auto local_specifics() -> SemIR::SpecificStore& {
     return local_ir().specifics();
   }
@@ -663,9 +676,7 @@ static auto GetLocalInstBlockContents(ImportRefResolver& resolver,
   auto import_block = resolver.import_inst_blocks().Get(import_block_id);
   inst_ids.reserve(import_block.size());
   for (auto import_inst_id : import_block) {
-    auto const_id = GetLocalConstantId(resolver, import_inst_id);
-    inst_ids.push_back(
-        resolver.local_constant_values().GetInstIdIfValid(const_id));
+    inst_ids.push_back(GetLocalConstantInstId(resolver, import_inst_id));
   }
 
   return inst_ids;
@@ -684,6 +695,56 @@ static auto GetLocalCanonicalInstBlockId(ImportContext& context,
   return context.local_inst_blocks().AddCanonical(contents);
 }
 
+// Imports the RequireImplsDecl instructions for each RequireImplsId in the
+// block, and gets the local RequireImplsIds from them. The returned vector is
+// only complete if there is no more work to do in the resolver on return.
+static auto GetLocalRequireImplsBlockContents(
+    ImportRefResolver& resolver, SemIR::RequireImplsBlockId import_block_id)
+    -> llvm::SmallVector<SemIR::RequireImplsId> {
+  llvm::SmallVector<SemIR::RequireImplsId> require_decl_ids;
+  if (!import_block_id.has_value() ||
+      import_block_id == SemIR::RequireImplsBlockId::Empty) {
+    return require_decl_ids;
+  }
+
+  // Import the RequireImplsDecl for each RequireImpls in the block.
+  auto import_block =
+      resolver.import_require_impls_blocks().Get(import_block_id);
+  require_decl_ids.reserve(import_block.size());
+  for (auto import_require_impls_id : import_block) {
+    const auto& import_require =
+        resolver.import_require_impls().Get(import_require_impls_id);
+    auto local_decl_id =
+        GetLocalConstantInstId(resolver, import_require.decl_id);
+    // If `local_decl_id` is None, the resolver will have more work to do, and
+    // we will call this function to try get all the decl instructions again.
+    if (local_decl_id.has_value()) {
+      // Importing the RequireImplsDecl instruction in `local_decl_id` also
+      // imported the RequireImpls structure that it points to through the
+      // RequireImplsId.
+      require_decl_ids.push_back(
+          resolver.local_insts()
+              .GetAs<SemIR::RequireImplsDecl>(local_decl_id)
+              .require_impls_id);
+    }
+  }
+
+  return require_decl_ids;
+}
+
+// Gets the local block of RequireImplsIds from the imported block. Only valid
+// to call once there is no more work to do after the call to
+// GetLocalRequireImplsBlockContents().
+static auto GetLocalCanonicalRequireImplsBlockId(
+    ImportContext& context, SemIR::RequireImplsBlockId import_block_id,
+    llvm::ArrayRef<SemIR::RequireImplsId> contents)
+    -> SemIR::RequireImplsBlockId {
+  if (!import_block_id.has_value()) {
+    return SemIR::RequireImplsBlockId::None;
+  }
+  return context.local_require_impls_blocks().Add(contents);
+}
+
 // Gets a local instruction block containing ImportRefs referring to the
 // instructions in the specified imported instruction block.
 static auto GetLocalImportRefInstBlock(ImportContext& context,
@@ -892,7 +953,8 @@ static auto GetLocalSpecificInterface(
   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.TryAsSingleInterface();
+    return std::get<SemIR::SpecificInterface>(
+        *new_facet_type_info.TryAsSingleExtend());
   } else {
     auto generic_interface_type =
         context.local_types().GetAs<SemIR::GenericInterfaceType>(
@@ -923,13 +985,23 @@ static auto GetLocalNameScopeIdImpl(ImportRefResolver& resolver,
     case CARBON_KIND(SemIR::FacetType inst): {
       const SemIR::FacetTypeInfo& facet_type_info =
           resolver.local_facet_types().Get(inst.facet_type_id);
-      // This is specifically the facet type produced by an interface
-      // declaration, and so should consist of a single interface.
-      // TODO: Will also have to handle named constraints here, once those are
-      // implemented.
-      auto interface = facet_type_info.TryAsSingleInterface();
-      CARBON_CHECK(interface);
-      return resolver.local_interfaces().Get(interface->interface_id).scope_id;
+      if (auto single = facet_type_info.TryAsSingleExtend()) {
+        // This is the facet type produced by an interface or named constraint
+        // declaration.
+        CARBON_KIND_SWITCH(*single) {
+          case CARBON_KIND(SemIR::SpecificInterface interface): {
+            return resolver.local_interfaces()
+                .Get(interface.interface_id)
+                .scope_id;
+          }
+          case CARBON_KIND(SemIR::SpecificNamedConstraint constraint): {
+            return resolver.local_named_constraints()
+                .Get(constraint.named_constraint_id)
+                .scope_id;
+          }
+        }
+      }
+      break;
     }
     case CARBON_KIND(SemIR::ImplDecl inst): {
       return resolver.local_impls().Get(inst.impl_id).scope_id;
@@ -2292,6 +2364,64 @@ static auto TryResolveTypedInst(ImportRefResolver& resolver,
   return ResolveResult::Done(impl_const_id, new_impl.first_decl_id());
 }
 
+static auto TryResolveTypedInst(ImportRefResolver& resolver,
+                                SemIR::RequireImplsDecl inst) -> ResolveResult {
+  const auto& import_require =
+      resolver.import_require_impls().Get(inst.require_impls_id);
+
+  // Load dependent constants.
+  auto parent_scope_id =
+      GetLocalNameScopeId(resolver, import_require.parent_scope_id);
+  auto generic_data = GetLocalGenericData(resolver, import_require.generic_id);
+  auto self_const_id = GetLocalConstantId(resolver, import_require.self_id);
+  auto facet_type_const_id =
+      GetLocalConstantId(resolver, import_require.facet_type_inst_id);
+
+  if (resolver.HasNewWork()) {
+    return ResolveResult::Retry();
+  }
+
+  // Make the decl and structure with placeholder values to be filled in.
+  SemIR::RequireImplsDecl require_decl = {
+      .require_impls_id = SemIR::RequireImplsId::None,
+      .decl_block_id = SemIR::InstBlockId::Empty};
+  auto require_decl_id = AddPlaceholderImportedInst(
+      resolver, import_require.decl_id, require_decl);
+  auto require_impls_id = resolver.local_require_impls().Add(
+      {.self_id = SemIR::TypeInstId::None,
+       .facet_type_inst_id = SemIR::TypeInstId::None,
+       .facet_type_id = SemIR::FacetTypeId::None,
+       .decl_id = require_decl_id,
+       .parent_scope_id = SemIR::NameScopeId::None,
+       .generic_id = MakeIncompleteGeneric(resolver, require_decl_id,
+                                           import_require.generic_id)});
+
+  // Write the RequireImplsId into the RequireImplsDecl.
+  require_decl.require_impls_id = require_impls_id;
+  auto require_decl_const_id =
+      ReplacePlaceholderImportedInst(resolver, require_decl_id, require_decl);
+
+  // Fill in the RequireImpls structure.
+  auto& new_require = resolver.local_require_impls().Get(require_impls_id);
+  new_require.self_id = AddLoadedImportRefForType(
+      resolver, import_require.self_id, self_const_id);
+  new_require.facet_type_inst_id = AddLoadedImportRefForType(
+      resolver, import_require.facet_type_inst_id, facet_type_const_id);
+  auto new_canonical_facet_type_inst_id =
+      resolver.local_constant_values().GetConstantInstId(
+          new_require.facet_type_inst_id);
+  auto new_canonical_facet_type =
+      resolver.local_insts().GetAs<SemIR::FacetType>(
+          new_canonical_facet_type_inst_id);
+  new_require.facet_type_id = new_canonical_facet_type.facet_type_id;
+  new_require.parent_scope_id = parent_scope_id;
+
+  SetGenericData(resolver, import_require.generic_id, new_require.generic_id,
+                 generic_data);
+
+  return ResolveResult::Done(require_decl_const_id, require_decl_id);
+}
+
 static auto TryResolveTypedInst(ImportRefResolver& resolver,
                                 SemIR::ImportRefLoaded /*inst*/,
                                 SemIR::InstId inst_id) -> ResolveResult {
@@ -2403,9 +2533,9 @@ static auto TryResolveTypedInst(ImportRefResolver& resolver,
     if (auto facet_type = interface_const_inst.TryAs<SemIR::FacetType>()) {
       const SemIR::FacetTypeInfo& facet_type_info =
           resolver.local_facet_types().Get(facet_type->facet_type_id);
-      auto interface_type = facet_type_info.TryAsSingleInterface();
-      CARBON_CHECK(interface_type);
-      interface_id = interface_type->interface_id;
+      auto single = facet_type_info.TryAsSingleExtend();
+      CARBON_CHECK(single);
+      interface_id = std::get<SemIR::SpecificInterface>(*single).interface_id;
     } else {
       auto generic_interface_type =
           resolver.local_types().GetAs<SemIR::GenericInterfaceType>(
@@ -2422,6 +2552,8 @@ static auto TryResolveTypedInst(ImportRefResolver& resolver,
       GetLocalInstBlockContents(resolver, import_interface.param_patterns_id);
   auto generic_data =
       GetLocalGenericData(resolver, import_interface.generic_id);
+  auto require_impls = GetLocalRequireImplsBlockContents(
+      resolver, import_interface.require_impls_block_id);
 
   std::optional<SemIR::InstId> self_param_id;
   if (import_interface.is_complete()) {
@@ -2441,7 +2573,8 @@ static auto TryResolveTypedInst(ImportRefResolver& resolver,
       implicit_param_patterns);
   new_interface.param_patterns_id = GetLocalCanonicalInstBlockId(
       resolver, import_interface.param_patterns_id, param_patterns);
-  // TODO: Import require_impls_block_id.
+  new_interface.require_impls_block_id = GetLocalCanonicalRequireImplsBlockId(
+      resolver, import_interface.require_impls_block_id, require_impls);
   SetGenericData(resolver, import_interface.generic_id,
                  new_interface.generic_id, generic_data);
 
@@ -2555,12 +2688,10 @@ static auto TryResolveTypedInst(ImportRefResolver& resolver,
             named_constraint_const_inst.TryAs<SemIR::FacetType>()) {
       const SemIR::FacetTypeInfo& facet_type_info =
           resolver.local_facet_types().Get(facet_type->facet_type_id);
-      CARBON_CHECK(facet_type_info.extend_named_constraints.size() == 1);
-      CARBON_CHECK(facet_type_info.extend_constraints.empty());
-      CARBON_CHECK(facet_type_info.self_impls_constraints.empty());
-      CARBON_CHECK(facet_type_info.self_impls_named_constraints.empty());
+      auto single = facet_type_info.TryAsSingleExtend();
+      CARBON_CHECK(single);
       named_constraint_id =
-          facet_type_info.extend_named_constraints.front().named_constraint_id;
+          std::get<SemIR::SpecificNamedConstraint>(*single).named_constraint_id;
     } else {
       auto generic_named_constraint_type =
           resolver.local_types().GetAs<SemIR::GenericNamedConstraintType>(
@@ -2577,6 +2708,8 @@ static auto TryResolveTypedInst(ImportRefResolver& resolver,
       resolver, import_named_constraint.param_patterns_id);
   auto generic_data =
       GetLocalGenericData(resolver, import_named_constraint.generic_id);
+  auto require_impls = GetLocalRequireImplsBlockContents(
+      resolver, import_named_constraint.require_impls_block_id);
 
   std::optional<SemIR::InstId> self_param_id;
   if (import_named_constraint.is_complete()) {
@@ -2598,7 +2731,10 @@ static auto TryResolveTypedInst(ImportRefResolver& resolver,
           implicit_param_patterns);
   new_named_constraint.param_patterns_id = GetLocalCanonicalInstBlockId(
       resolver, import_named_constraint.param_patterns_id, param_patterns);
-  // TODO: Import require_impls_block_id.
+  new_named_constraint.require_impls_block_id =
+      GetLocalCanonicalRequireImplsBlockId(
+          resolver, import_named_constraint.require_impls_block_id,
+          require_impls);
   SetGenericData(resolver, import_named_constraint.generic_id,
                  import_named_constraint.generic_id, generic_data);
 
@@ -2644,6 +2780,7 @@ static auto TryResolveTypedInst(ImportRefResolver& resolver,
     GetLocalConstantInstId(resolver, rewrite.lhs_id);
     GetLocalConstantInstId(resolver, rewrite.rhs_id);
   }
+  // TODO: Import named constraints in the facet type.
   if (resolver.HasNewWork()) {
     return ResolveResult::Retry();
   }
@@ -3373,6 +3510,9 @@ static auto TryResolveInstCanonical(ImportRefResolver& resolver,
     case CARBON_KIND(SemIR::RequireCompleteType inst): {
       return TryResolveTypedInst(resolver, inst);
     }
+    case CARBON_KIND(SemIR::RequireImplsDecl inst): {
+      return TryResolveTypedInst(resolver, inst);
+    }
     case CARBON_KIND(SemIR::ReturnSlotPattern inst): {
       return TryResolveTypedInst(resolver, inst, constant_inst_id);
     }
@@ -3918,12 +4058,12 @@ auto ImportInterface(Context& context, SemIR::ImportIRId import_ir_id,
   // A non-generic interface will import as a facet type for that single
   // interface.
   if (auto facet_type = local_inst.TryAs<SemIR::FacetType>()) {
-    auto interface = context.facet_types()
-                         .Get(facet_type->facet_type_id)
-                         .TryAsSingleInterface();
-    CARBON_CHECK(interface,
+    auto single = context.facet_types()
+                      .Get(facet_type->facet_type_id)
+                      .TryAsSingleExtend();
+    CARBON_CHECK(single,
                  "Importing an interface didn't produce a single interface");
-    return interface->interface_id;
+    return std::get<SemIR::SpecificInterface>(*single).interface_id;
   }
 
   // A generic interface will import as a constant of generic interface type.

toolchain/check/testdata/facet/require_import.carbon

@@ -35,9 +35,13 @@ fn F(A:! X, B:! Y) {}
 // CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
 // CHECK:STDOUT:   %.Self: %type = symbolic_binding .Self [symbolic_self]
 // CHECK:STDOUT:   %X.type: type = facet_type <@X> [concrete]
+// CHECK:STDOUT:   %Self.861: %type = symbolic_binding Self, 0 [symbolic]
+// CHECK:STDOUT:   %Self.binding.as_type.1a1: type = symbolic_binding_type Self, 0, %Self.861 [symbolic]
 // CHECK:STDOUT:   %A: %X.type = symbolic_binding A, 0 [symbolic]
 // CHECK:STDOUT:   %pattern_type.e25: type = pattern_type %X.type [concrete]
 // CHECK:STDOUT:   %Y.type: type = facet_type <@Y> [concrete]
+// CHECK:STDOUT:   %Self.29b: %Y.type = symbolic_binding Self, 0 [symbolic]
+// CHECK:STDOUT:   %Self.binding.as_type.384: type = symbolic_binding_type Self, 0, %Self.29b [symbolic]
 // CHECK:STDOUT:   %B: %Y.type = symbolic_binding B, 1 [symbolic]
 // CHECK:STDOUT:   %pattern_type.6e5: type = pattern_type %Y.type [concrete]
 // CHECK:STDOUT:   %F.type: type = fn_type @F [concrete]
@@ -48,7 +52,12 @@ fn F(A:! X, B:! Y) {}
 // CHECK:STDOUT:   %Main.Z = import_ref Main//a, Z, unloaded
 // CHECK:STDOUT:   %Main.Y: type = import_ref Main//a, Y, loaded [concrete = constants.%Y.type]
 // CHECK:STDOUT:   %Main.X: type = import_ref Main//a, X, loaded [concrete = constants.%X.type]
+// CHECK:STDOUT:   %Main.import_ref.462 = import_ref Main//a, loc3_13, unloaded
+// CHECK:STDOUT:   %Main.import_ref.b7c: type = import_ref Main//a, loc10_18, loaded [symbolic = constants.%Self.binding.as_type.1a1]
+// CHECK:STDOUT:   %Main.import_ref.dec: %type = import_ref Main//a, loc9_14, loaded [symbolic = constants.%Self.861]
 // CHECK:STDOUT:   %Main.import_ref.cae = import_ref Main//a, loc9_14, unloaded
+// CHECK:STDOUT:   %Main.import_ref.3e6: type = import_ref Main//a, loc6_11, loaded [symbolic = constants.%Self.binding.as_type.384]
+// CHECK:STDOUT:   %Main.import_ref.35b: %Y.type = import_ref Main//a, loc5_13, loaded [symbolic = constants.%Self.29b]
 // CHECK:STDOUT:   %Main.import_ref.581 = import_ref Main//a, loc5_13, unloaded
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
@@ -78,12 +87,23 @@ fn F(A:! X, B:! Y) {}
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
+// CHECK:STDOUT: interface @Z [from "a.carbon"] {
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = imports.%Main.import_ref.462
+// CHECK:STDOUT:   witness = ()
+// CHECK:STDOUT:
+// CHECK:STDOUT: !requires:
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
 // CHECK:STDOUT: interface @Y [from "a.carbon"] {
 // CHECK:STDOUT: !members:
 // CHECK:STDOUT:   .Self = imports.%Main.import_ref.581
 // CHECK:STDOUT:   witness = ()
 // CHECK:STDOUT:
 // CHECK:STDOUT: !requires:
+// CHECK:STDOUT:   @Y.require1 {
+// CHECK:STDOUT:     require imports.%Main.import_ref.3e6 impls <@Z>
+// CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: constraint @X [from "a.carbon"] {
@@ -91,6 +111,19 @@ fn F(A:! X, B:! Y) {}
 // CHECK:STDOUT:   .Self = imports.%Main.import_ref.cae
 // CHECK:STDOUT:
 // CHECK:STDOUT: !requires:
+// CHECK:STDOUT:   @X.require0 {
+// CHECK:STDOUT:     require imports.%Main.import_ref.b7c impls <@Z>
+// CHECK:STDOUT:   }
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: generic require @X.require0(imports.%Main.import_ref.dec: %type) [from "a.carbon"] {
+// CHECK:STDOUT:   %Self: %type = symbolic_binding Self, 0 [symbolic = %Self (constants.%Self.861)]
+// CHECK:STDOUT:   %Self.binding.as_type: type = symbolic_binding_type Self, 0, %Self [symbolic = %Self.binding.as_type (constants.%Self.binding.as_type.1a1)]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: generic require @Y.require1(imports.%Main.import_ref.35b: %Y.type) [from "a.carbon"] {
+// CHECK:STDOUT:   %Self: %Y.type = symbolic_binding Self, 0 [symbolic = %Self (constants.%Self.29b)]
+// CHECK:STDOUT:   %Self.binding.as_type: type = symbolic_binding_type Self, 0, %Self [symbolic = %Self.binding.as_type (constants.%Self.binding.as_type.384)]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: generic fn @F(%A.loc4_6.2: %X.type, %B.loc4_13.2: %Y.type) {
@@ -105,6 +138,16 @@ fn F(A:! X, B:! Y) {}
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
+// CHECK:STDOUT: specific @X.require0(constants.%Self.861) {
+// CHECK:STDOUT:   %Self => constants.%Self.861
+// CHECK:STDOUT:   %Self.binding.as_type => constants.%Self.binding.as_type.1a1
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @Y.require1(constants.%Self.29b) {
+// CHECK:STDOUT:   %Self => constants.%Self.29b
+// CHECK:STDOUT:   %Self.binding.as_type => constants.%Self.binding.as_type.384
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
 // CHECK:STDOUT: specific @F(constants.%A, constants.%B) {
 // CHECK:STDOUT:   %A.loc4_6.1 => constants.%A
 // CHECK:STDOUT:   %B.loc4_13.1 => constants.%B

toolchain/check/testdata/interface/incomplete.carbon

@@ -176,7 +176,9 @@ interface B {
 // CHECK:STDOUT:   witness = ()
 // CHECK:STDOUT:
 // CHECK:STDOUT: !requires:
-// CHECK:STDOUT:   @B.require0
+// CHECK:STDOUT:   @B.require0 {
+// CHECK:STDOUT:     require @B.require0.%Self.as_type impls <@A>
+// CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: generic require @B.require0(@B.%Self: %B.type) {

toolchain/check/testdata/interface/require.carbon

@@ -301,7 +301,9 @@ interface Z(T:! type) {
 // CHECK:STDOUT:   witness = ()
 // CHECK:STDOUT:
 // CHECK:STDOUT: !requires:
-// CHECK:STDOUT:   @Z.require0
+// CHECK:STDOUT:   @Z.require0 {
+// CHECK:STDOUT:     require @Z.require0.%Self.as_type impls <@Y>
+// CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: generic require @Z.require0(@Z.%Self: %Z.type) {
@@ -345,7 +347,9 @@ interface Z(T:! type) {
 // CHECK:STDOUT:   witness = ()
 // CHECK:STDOUT:
 // CHECK:STDOUT: !requires:
-// CHECK:STDOUT:   @Z.require0
+// CHECK:STDOUT:   @Z.require0 {
+// CHECK:STDOUT:     require @Z.require0.%Self.as_type impls <@Y>
+// CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: generic require @Z.require0(@Z.%Self: %Z.type) {
@@ -391,7 +395,9 @@ interface Z(T:! type) {
 // CHECK:STDOUT:   witness = ()
 // CHECK:STDOUT:
 // CHECK:STDOUT: !requires:
-// CHECK:STDOUT:   @Z.require0
+// CHECK:STDOUT:   @Z.require0 {
+// CHECK:STDOUT:     require @Z.require0.%.loc9 impls <@Y>
+// CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: generic require @Z.require0(@Z.%Self: %Z.type) {
@@ -443,7 +449,9 @@ interface Z(T:! type) {
 // CHECK:STDOUT:   witness = ()
 // CHECK:STDOUT:
 // CHECK:STDOUT: !requires:
-// CHECK:STDOUT:   @Z.require0
+// CHECK:STDOUT:   @Z.require0 {
+// CHECK:STDOUT:     require @Z.require0.%C.loc9_17.1 impls <@Y>
+// CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: generic require @Z.require0(@Z.%Self: %Z.type) {
@@ -510,7 +518,9 @@ interface Z(T:! type) {
 // CHECK:STDOUT:   witness = ()
 // CHECK:STDOUT:
 // CHECK:STDOUT: !requires:
-// CHECK:STDOUT:   @Z.require0
+// CHECK:STDOUT:   @Z.require0 {
+// CHECK:STDOUT:     require @Z.require0.%Self.as_type impls <@Y where constants.%impl.elem0 = constants.%empty_tuple.type>
+// CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: generic require @Z.require0(@Z.%Self: %Z.type) {
@@ -576,7 +586,9 @@ interface Z(T:! type) {
 // CHECK:STDOUT:     witness = ()
 // CHECK:STDOUT:
 // CHECK:STDOUT:   !requires:
-// CHECK:STDOUT:     @Z.require0
+// CHECK:STDOUT:     @Z.require0 {
+// CHECK:STDOUT:       require @Z.require0.%T.ref impls <@Z, @Z(constants.%Self.binding.as_type)>
+// CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
@@ -655,7 +667,9 @@ interface Z(T:! type) {
 // CHECK:STDOUT:   witness = ()
 // CHECK:STDOUT:
 // CHECK:STDOUT: !requires:
-// CHECK:STDOUT:   @Z.require0
+// CHECK:STDOUT:   @Z.require0 {
+// CHECK:STDOUT:     require @Z.require0.%Self.as_type.loc10_11 impls <@Y where constants.%impl.elem0 = constants.%Self.binding.as_type>
+// CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: generic require @Z.require0(@Z.%Self: %Z.type) {
@@ -719,7 +733,9 @@ interface Z(T:! type) {
 // CHECK:STDOUT:     witness = ()
 // CHECK:STDOUT:
 // CHECK:STDOUT:   !requires:
-// CHECK:STDOUT:     @Z.require1
+// CHECK:STDOUT:     @Z.require1 {
+// CHECK:STDOUT:       require @Z.require1.%Self.as_type impls <@Z, @Z(constants.%T)>
+// CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:

toolchain/check/testdata/named_constraint/convert.carbon

@@ -137,8 +137,8 @@ fn G(T:! Z) {
 // CHECK:STDOUT:   %G.type: type = fn_type @G [concrete]
 // CHECK:STDOUT:   %G: %G.type = struct_value () [concrete]
 // CHECK:STDOUT:   %T.binding.as_type: type = symbolic_binding_type T, 0, %T.8619ef.2 [symbolic]
-// CHECK:STDOUT:   %facet_value: %E1.type = facet_value %T.binding.as_type, () [symbolic]
-// CHECK:STDOUT:   %F.specific_fn: <specific function> = specific_function %F, @F(%facet_value) [symbolic]
+// CHECK:STDOUT:   %E1.facet: %E1.type = facet_value %T.binding.as_type, () [symbolic]
+// CHECK:STDOUT:   %F.specific_fn: <specific function> = specific_function %F, @F(%E1.facet) [symbolic]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: imports {
@@ -161,17 +161,17 @@ fn G(T:! Z) {
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT:   %T.binding.as_type: type = symbolic_binding_type T, 0, %T.loc9_6.1 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
-// CHECK:STDOUT:   %facet_value.loc10_6.2: %E1.type = facet_value %T.binding.as_type, () [symbolic = %facet_value.loc10_6.2 (constants.%facet_value)]
-// CHECK:STDOUT:   %F.specific_fn.loc10_3.2: <specific function> = specific_function constants.%F, @F(%facet_value.loc10_6.2) [symbolic = %F.specific_fn.loc10_3.2 (constants.%F.specific_fn)]
+// CHECK:STDOUT:   %E1.facet.loc10_6.2: %E1.type = facet_value %T.binding.as_type, () [symbolic = %E1.facet.loc10_6.2 (constants.%E1.facet)]
+// CHECK:STDOUT:   %F.specific_fn.loc10_3.2: <specific function> = specific_function constants.%F, @F(%E1.facet.loc10_6.2) [symbolic = %F.specific_fn.loc10_3.2 (constants.%F.specific_fn)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   fn() {
 // CHECK:STDOUT:   !entry:
 // CHECK:STDOUT:     %F.ref: %F.type = name_ref F, file.%F.decl [concrete = constants.%F]
 // CHECK:STDOUT:     %T.ref: %E2.type = name_ref T, %T.loc9_6.2 [symbolic = %T.loc9_6.1 (constants.%T.8619ef.2)]
 // CHECK:STDOUT:     %T.as_type: type = facet_access_type %T.ref [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
-// CHECK:STDOUT:     %facet_value.loc10_6.1: %E1.type = facet_value %T.as_type, () [symbolic = %facet_value.loc10_6.2 (constants.%facet_value)]
-// CHECK:STDOUT:     %.loc10: %E1.type = converted %T.ref, %facet_value.loc10_6.1 [symbolic = %facet_value.loc10_6.2 (constants.%facet_value)]
-// CHECK:STDOUT:     %F.specific_fn.loc10_3.1: <specific function> = specific_function %F.ref, @F(constants.%facet_value) [symbolic = %F.specific_fn.loc10_3.2 (constants.%F.specific_fn)]
+// CHECK:STDOUT:     %E1.facet.loc10_6.1: %E1.type = facet_value %T.as_type, () [symbolic = %E1.facet.loc10_6.2 (constants.%E1.facet)]
+// CHECK:STDOUT:     %.loc10: %E1.type = converted %T.ref, %E1.facet.loc10_6.1 [symbolic = %E1.facet.loc10_6.2 (constants.%E1.facet)]
+// CHECK:STDOUT:     %F.specific_fn.loc10_3.1: <specific function> = specific_function %F.ref, @F(constants.%E1.facet) [symbolic = %F.specific_fn.loc10_3.2 (constants.%F.specific_fn)]
 // CHECK:STDOUT:     %F.call: init %empty_tuple.type = call %F.specific_fn.loc10_3.1()
 // CHECK:STDOUT:     return
 // CHECK:STDOUT:   }

toolchain/check/testdata/named_constraint/empty.carbon

@@ -50,15 +50,15 @@ fn G(T:! Z, U:! type, V:! Empty) {
 // CHECK:STDOUT:   %G: %G.type = struct_value () [concrete]
 // CHECK:STDOUT:   %empty_struct_type: type = struct_type {} [concrete]
 // CHECK:STDOUT:   %empty_struct: %empty_struct_type = struct_value () [concrete]
-// CHECK:STDOUT:   %facet_value.6fa: %Empty.type = facet_value %empty_struct_type, () [concrete]
-// CHECK:STDOUT:   %F.specific_fn.007: <specific function> = specific_function %F, @F(%facet_value.6fa) [concrete]
-// CHECK:STDOUT:   %facet_value.832: %Empty.type = facet_value type, () [concrete]
-// CHECK:STDOUT:   %F.specific_fn.7db: <specific function> = specific_function %F, @F(%facet_value.832) [concrete]
+// CHECK:STDOUT:   %Empty.facet.6fa: %Empty.type = facet_value %empty_struct_type, () [concrete]
+// CHECK:STDOUT:   %F.specific_fn.007: <specific function> = specific_function %F, @F(%Empty.facet.6fa) [concrete]
+// CHECK:STDOUT:   %Empty.facet.832: %Empty.type = facet_value type, () [concrete]
+// CHECK:STDOUT:   %F.specific_fn.7db: <specific function> = specific_function %F, @F(%Empty.facet.832) [concrete]
 // CHECK:STDOUT:   %T.binding.as_type: type = symbolic_binding_type T, 0, %T.3b3 [symbolic]
-// CHECK:STDOUT:   %facet_value.146: %Empty.type = facet_value %T.binding.as_type, () [symbolic]
-// CHECK:STDOUT:   %F.specific_fn.2bd: <specific function> = specific_function %F, @F(%facet_value.146) [symbolic]
-// CHECK:STDOUT:   %facet_value.a70: %Empty.type = facet_value %U, () [symbolic]
-// CHECK:STDOUT:   %F.specific_fn.1c5: <specific function> = specific_function %F, @F(%facet_value.a70) [symbolic]
+// CHECK:STDOUT:   %Empty.facet.146: %Empty.type = facet_value %T.binding.as_type, () [symbolic]
+// CHECK:STDOUT:   %F.specific_fn.2bd: <specific function> = specific_function %F, @F(%Empty.facet.146) [symbolic]
+// CHECK:STDOUT:   %Empty.facet.a70: %Empty.type = facet_value %U, () [symbolic]
+// CHECK:STDOUT:   %F.specific_fn.1c5: <specific function> = specific_function %F, @F(%Empty.facet.a70) [symbolic]
 // CHECK:STDOUT:   %F.specific_fn.f38: <specific function> = specific_function %F, @F(%V) [symbolic]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
@@ -110,37 +110,37 @@ fn G(T:! Z, U:! type, V:! Empty) {
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT:   %T.binding.as_type: type = symbolic_binding_type T, 0, %T.loc25_6.1 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
-// CHECK:STDOUT:   %facet_value.loc28_6.2: %Empty.type = facet_value %T.binding.as_type, () [symbolic = %facet_value.loc28_6.2 (constants.%facet_value.146)]
-// CHECK:STDOUT:   %F.specific_fn.loc28_3.2: <specific function> = specific_function constants.%F, @F(%facet_value.loc28_6.2) [symbolic = %F.specific_fn.loc28_3.2 (constants.%F.specific_fn.2bd)]
-// CHECK:STDOUT:   %facet_value.loc29_6.2: %Empty.type = facet_value %U.loc25_13.1, () [symbolic = %facet_value.loc29_6.2 (constants.%facet_value.a70)]
-// CHECK:STDOUT:   %F.specific_fn.loc29_3.2: <specific function> = specific_function constants.%F, @F(%facet_value.loc29_6.2) [symbolic = %F.specific_fn.loc29_3.2 (constants.%F.specific_fn.1c5)]
+// CHECK:STDOUT:   %Empty.facet.loc28_6.2: %Empty.type = facet_value %T.binding.as_type, () [symbolic = %Empty.facet.loc28_6.2 (constants.%Empty.facet.146)]
+// CHECK:STDOUT:   %F.specific_fn.loc28_3.2: <specific function> = specific_function constants.%F, @F(%Empty.facet.loc28_6.2) [symbolic = %F.specific_fn.loc28_3.2 (constants.%F.specific_fn.2bd)]
+// CHECK:STDOUT:   %Empty.facet.loc29_6.2: %Empty.type = facet_value %U.loc25_13.1, () [symbolic = %Empty.facet.loc29_6.2 (constants.%Empty.facet.a70)]
+// CHECK:STDOUT:   %F.specific_fn.loc29_3.2: <specific function> = specific_function constants.%F, @F(%Empty.facet.loc29_6.2) [symbolic = %F.specific_fn.loc29_3.2 (constants.%F.specific_fn.1c5)]
 // CHECK:STDOUT:   %F.specific_fn.loc30_3.2: <specific function> = specific_function constants.%F, @F(%V.loc25_23.1) [symbolic = %F.specific_fn.loc30_3.2 (constants.%F.specific_fn.f38)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   fn() {
 // CHECK:STDOUT:   !entry:
 // CHECK:STDOUT:     %F.ref.loc26: %F.type = name_ref F, file.%F.decl [concrete = constants.%F]
 // CHECK:STDOUT:     %.loc26_6: %empty_struct_type = struct_literal () [concrete = constants.%empty_struct]
-// CHECK:STDOUT:     %facet_value.loc26: %Empty.type = facet_value constants.%empty_struct_type, () [concrete = constants.%facet_value.6fa]
-// CHECK:STDOUT:     %.loc26_7: %Empty.type = converted %.loc26_6, %facet_value.loc26 [concrete = constants.%facet_value.6fa]
-// CHECK:STDOUT:     %F.specific_fn.loc26: <specific function> = specific_function %F.ref.loc26, @F(constants.%facet_value.6fa) [concrete = constants.%F.specific_fn.007]
+// CHECK:STDOUT:     %Empty.facet.loc26: %Empty.type = facet_value constants.%empty_struct_type, () [concrete = constants.%Empty.facet.6fa]
+// CHECK:STDOUT:     %.loc26_7: %Empty.type = converted %.loc26_6, %Empty.facet.loc26 [concrete = constants.%Empty.facet.6fa]
+// CHECK:STDOUT:     %F.specific_fn.loc26: <specific function> = specific_function %F.ref.loc26, @F(constants.%Empty.facet.6fa) [concrete = constants.%F.specific_fn.007]
 // CHECK:STDOUT:     %F.call.loc26: init %empty_tuple.type = call %F.specific_fn.loc26()
 // CHECK:STDOUT:     %F.ref.loc27: %F.type = name_ref F, file.%F.decl [concrete = constants.%F]
-// CHECK:STDOUT:     %facet_value.loc27: %Empty.type = facet_value type, () [concrete = constants.%facet_value.832]
-// CHECK:STDOUT:     %.loc27: %Empty.type = converted type, %facet_value.loc27 [concrete = constants.%facet_value.832]
-// CHECK:STDOUT:     %F.specific_fn.loc27: <specific function> = specific_function %F.ref.loc27, @F(constants.%facet_value.832) [concrete = constants.%F.specific_fn.7db]
+// CHECK:STDOUT:     %Empty.facet.loc27: %Empty.type = facet_value type, () [concrete = constants.%Empty.facet.832]
+// CHECK:STDOUT:     %.loc27: %Empty.type = converted type, %Empty.facet.loc27 [concrete = constants.%Empty.facet.832]
+// CHECK:STDOUT:     %F.specific_fn.loc27: <specific function> = specific_function %F.ref.loc27, @F(constants.%Empty.facet.832) [concrete = constants.%F.specific_fn.7db]
 // CHECK:STDOUT:     %F.call.loc27: init %empty_tuple.type = call %F.specific_fn.loc27()
 // CHECK:STDOUT:     %F.ref.loc28: %F.type = name_ref F, file.%F.decl [concrete = constants.%F]
 // CHECK:STDOUT:     %T.ref: %Z.type = name_ref T, %T.loc25_6.2 [symbolic = %T.loc25_6.1 (constants.%T.3b3)]
 // CHECK:STDOUT:     %T.as_type: type = facet_access_type %T.ref [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
-// CHECK:STDOUT:     %facet_value.loc28_6.1: %Empty.type = facet_value %T.as_type, () [symbolic = %facet_value.loc28_6.2 (constants.%facet_value.146)]
-// CHECK:STDOUT:     %.loc28: %Empty.type = converted %T.ref, %facet_value.loc28_6.1 [symbolic = %facet_value.loc28_6.2 (constants.%facet_value.146)]
-// CHECK:STDOUT:     %F.specific_fn.loc28_3.1: <specific function> = specific_function %F.ref.loc28, @F(constants.%facet_value.146) [symbolic = %F.specific_fn.loc28_3.2 (constants.%F.specific_fn.2bd)]
+// CHECK:STDOUT:     %Empty.facet.loc28_6.1: %Empty.type = facet_value %T.as_type, () [symbolic = %Empty.facet.loc28_6.2 (constants.%Empty.facet.146)]
+// CHECK:STDOUT:     %.loc28: %Empty.type = converted %T.ref, %Empty.facet.loc28_6.1 [symbolic = %Empty.facet.loc28_6.2 (constants.%Empty.facet.146)]
+// CHECK:STDOUT:     %F.specific_fn.loc28_3.1: <specific function> = specific_function %F.ref.loc28, @F(constants.%Empty.facet.146) [symbolic = %F.specific_fn.loc28_3.2 (constants.%F.specific_fn.2bd)]
 // CHECK:STDOUT:     %F.call.loc28: init %empty_tuple.type = call %F.specific_fn.loc28_3.1()
 // CHECK:STDOUT:     %F.ref.loc29: %F.type = name_ref F, file.%F.decl [concrete = constants.%F]
 // CHECK:STDOUT:     %U.ref: type = name_ref U, %U.loc25_13.2 [symbolic = %U.loc25_13.1 (constants.%U)]
-// CHECK:STDOUT:     %facet_value.loc29_6.1: %Empty.type = facet_value %U.ref, () [symbolic = %facet_value.loc29_6.2 (constants.%facet_value.a70)]
-// CHECK:STDOUT:     %.loc29: %Empty.type = converted %U.ref, %facet_value.loc29_6.1 [symbolic = %facet_value.loc29_6.2 (constants.%facet_value.a70)]
-// CHECK:STDOUT:     %F.specific_fn.loc29_3.1: <specific function> = specific_function %F.ref.loc29, @F(constants.%facet_value.a70) [symbolic = %F.specific_fn.loc29_3.2 (constants.%F.specific_fn.1c5)]
+// CHECK:STDOUT:     %Empty.facet.loc29_6.1: %Empty.type = facet_value %U.ref, () [symbolic = %Empty.facet.loc29_6.2 (constants.%Empty.facet.a70)]
+// CHECK:STDOUT:     %.loc29: %Empty.type = converted %U.ref, %Empty.facet.loc29_6.1 [symbolic = %Empty.facet.loc29_6.2 (constants.%Empty.facet.a70)]
+// CHECK:STDOUT:     %F.specific_fn.loc29_3.1: <specific function> = specific_function %F.ref.loc29, @F(constants.%Empty.facet.a70) [symbolic = %F.specific_fn.loc29_3.2 (constants.%F.specific_fn.1c5)]
 // CHECK:STDOUT:     %F.call.loc29: init %empty_tuple.type = call %F.specific_fn.loc29_3.1()
 // CHECK:STDOUT:     %F.ref.loc30: %F.type = name_ref F, file.%F.decl [concrete = constants.%F]
 // CHECK:STDOUT:     %V.ref: %Empty.type = name_ref V, %V.loc25_23.2 [symbolic = %V.loc25_23.1 (constants.%V)]
@@ -160,26 +160,26 @@ fn G(T:! Z, U:! type, V:! Empty) {
 // CHECK:STDOUT:   %V.loc25_23.1 => constants.%V
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @F(constants.%facet_value.6fa) {
-// CHECK:STDOUT:   %T.loc19_6.1 => constants.%facet_value.6fa
+// CHECK:STDOUT: specific @F(constants.%Empty.facet.6fa) {
+// CHECK:STDOUT:   %T.loc19_6.1 => constants.%Empty.facet.6fa
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @F(constants.%facet_value.832) {
-// CHECK:STDOUT:   %T.loc19_6.1 => constants.%facet_value.832
+// CHECK:STDOUT: specific @F(constants.%Empty.facet.832) {
+// CHECK:STDOUT:   %T.loc19_6.1 => constants.%Empty.facet.832
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @F(constants.%facet_value.146) {
-// CHECK:STDOUT:   %T.loc19_6.1 => constants.%facet_value.146
+// CHECK:STDOUT: specific @F(constants.%Empty.facet.146) {
+// CHECK:STDOUT:   %T.loc19_6.1 => constants.%Empty.facet.146
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @F(constants.%facet_value.a70) {
-// CHECK:STDOUT:   %T.loc19_6.1 => constants.%facet_value.a70
+// CHECK:STDOUT: specific @F(constants.%Empty.facet.a70) {
+// CHECK:STDOUT:   %T.loc19_6.1 => constants.%Empty.facet.a70
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT: }

toolchain/check/testdata/named_constraint/empty_generic.carbon

@@ -52,15 +52,15 @@ fn G(T:! Z, U:! Empty(T), V:! type) {
 // CHECK:STDOUT:   %G: %G.type = struct_value () [concrete]
 // CHECK:STDOUT:   %empty_struct_type: type = struct_type {} [concrete]
 // CHECK:STDOUT:   %empty_struct.a40: %empty_struct_type = struct_value () [concrete]
-// CHECK:STDOUT:   %facet_value.6fa: %Empty.type.b8d23b.2 = facet_value %empty_struct_type, () [symbolic]
-// CHECK:STDOUT:   %F.specific_fn.8ba: <specific function> = specific_function %F, @F(%T.binding.as_type, %facet_value.6fa) [symbolic]
-// CHECK:STDOUT:   %facet_value.832: %Empty.type.b8d23b.2 = facet_value type, () [symbolic]
-// CHECK:STDOUT:   %F.specific_fn.55c: <specific function> = specific_function %F, @F(%T.binding.as_type, %facet_value.832) [symbolic]
-// CHECK:STDOUT:   %facet_value.146: %Empty.type.b8d23b.2 = facet_value %T.binding.as_type, () [symbolic]
-// CHECK:STDOUT:   %F.specific_fn.d3f: <specific function> = specific_function %F, @F(%T.binding.as_type, %facet_value.146) [symbolic]
+// CHECK:STDOUT:   %Empty.facet.6fa: %Empty.type.b8d23b.2 = facet_value %empty_struct_type, () [symbolic]
+// CHECK:STDOUT:   %F.specific_fn.8ba: <specific function> = specific_function %F, @F(%T.binding.as_type, %Empty.facet.6fa) [symbolic]
+// CHECK:STDOUT:   %Empty.facet.832: %Empty.type.b8d23b.2 = facet_value type, () [symbolic]
+// CHECK:STDOUT:   %F.specific_fn.55c: <specific function> = specific_function %F, @F(%T.binding.as_type, %Empty.facet.832) [symbolic]
+// CHECK:STDOUT:   %Empty.facet.146: %Empty.type.b8d23b.2 = facet_value %T.binding.as_type, () [symbolic]
+// CHECK:STDOUT:   %F.specific_fn.d3f: <specific function> = specific_function %F, @F(%T.binding.as_type, %Empty.facet.146) [symbolic]
 // CHECK:STDOUT:   %F.specific_fn.4af: <specific function> = specific_function %F, @F(%T.binding.as_type, %U.aa1546.2) [symbolic]
-// CHECK:STDOUT:   %facet_value.920: %Empty.type.b8d23b.2 = facet_value %V, () [symbolic]
-// CHECK:STDOUT:   %F.specific_fn.905: <specific function> = specific_function %F, @F(%T.binding.as_type, %facet_value.920) [symbolic]
+// CHECK:STDOUT:   %Empty.facet.920: %Empty.type.b8d23b.2 = facet_value %V, () [symbolic]
+// CHECK:STDOUT:   %F.specific_fn.905: <specific function> = specific_function %F, @F(%T.binding.as_type, %Empty.facet.920) [symbolic]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
@@ -148,15 +148,15 @@ fn G(T:! Z, U:! Empty(T), V:! type) {
 // CHECK:STDOUT:   %V.loc20_27.1: type = symbolic_binding V, 2 [symbolic = %V.loc20_27.1 (constants.%V)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
-// CHECK:STDOUT:   %facet_value.loc21_18.2: @G.%Empty.type.loc20_24.1 (%Empty.type.b8d23b.2) = facet_value constants.%empty_struct_type, () [symbolic = %facet_value.loc21_18.2 (constants.%facet_value.6fa)]
-// CHECK:STDOUT:   %F.specific_fn.loc21_3.2: <specific function> = specific_function constants.%F, @F(%T.binding.as_type, %facet_value.loc21_18.2) [symbolic = %F.specific_fn.loc21_3.2 (constants.%F.specific_fn.8ba)]
-// CHECK:STDOUT:   %facet_value.loc22_12.2: @G.%Empty.type.loc20_24.1 (%Empty.type.b8d23b.2) = facet_value type, () [symbolic = %facet_value.loc22_12.2 (constants.%facet_value.832)]
-// CHECK:STDOUT:   %F.specific_fn.loc22_3.2: <specific function> = specific_function constants.%F, @F(%T.binding.as_type, %facet_value.loc22_12.2) [symbolic = %F.specific_fn.loc22_3.2 (constants.%F.specific_fn.55c)]
-// CHECK:STDOUT:   %facet_value.loc23_9.2: @G.%Empty.type.loc20_24.1 (%Empty.type.b8d23b.2) = facet_value %T.binding.as_type, () [symbolic = %facet_value.loc23_9.2 (constants.%facet_value.146)]
-// CHECK:STDOUT:   %F.specific_fn.loc23_3.2: <specific function> = specific_function constants.%F, @F(%T.binding.as_type, %facet_value.loc23_9.2) [symbolic = %F.specific_fn.loc23_3.2 (constants.%F.specific_fn.d3f)]
+// CHECK:STDOUT:   %Empty.facet.loc21_18.2: @G.%Empty.type.loc20_24.1 (%Empty.type.b8d23b.2) = facet_value constants.%empty_struct_type, () [symbolic = %Empty.facet.loc21_18.2 (constants.%Empty.facet.6fa)]
+// CHECK:STDOUT:   %F.specific_fn.loc21_3.2: <specific function> = specific_function constants.%F, @F(%T.binding.as_type, %Empty.facet.loc21_18.2) [symbolic = %F.specific_fn.loc21_3.2 (constants.%F.specific_fn.8ba)]
+// CHECK:STDOUT:   %Empty.facet.loc22_12.2: @G.%Empty.type.loc20_24.1 (%Empty.type.b8d23b.2) = facet_value type, () [symbolic = %Empty.facet.loc22_12.2 (constants.%Empty.facet.832)]
+// CHECK:STDOUT:   %F.specific_fn.loc22_3.2: <specific function> = specific_function constants.%F, @F(%T.binding.as_type, %Empty.facet.loc22_12.2) [symbolic = %F.specific_fn.loc22_3.2 (constants.%F.specific_fn.55c)]
+// CHECK:STDOUT:   %Empty.facet.loc23_9.2: @G.%Empty.type.loc20_24.1 (%Empty.type.b8d23b.2) = facet_value %T.binding.as_type, () [symbolic = %Empty.facet.loc23_9.2 (constants.%Empty.facet.146)]
+// CHECK:STDOUT:   %F.specific_fn.loc23_3.2: <specific function> = specific_function constants.%F, @F(%T.binding.as_type, %Empty.facet.loc23_9.2) [symbolic = %F.specific_fn.loc23_3.2 (constants.%F.specific_fn.d3f)]
 // CHECK:STDOUT:   %F.specific_fn.loc24_3.2: <specific function> = specific_function constants.%F, @F(%T.binding.as_type, %U.loc20_13.1) [symbolic = %F.specific_fn.loc24_3.2 (constants.%F.specific_fn.4af)]
-// CHECK:STDOUT:   %facet_value.loc25_9.2: @G.%Empty.type.loc20_24.1 (%Empty.type.b8d23b.2) = facet_value %V.loc20_27.1, () [symbolic = %facet_value.loc25_9.2 (constants.%facet_value.920)]
-// CHECK:STDOUT:   %F.specific_fn.loc25_3.2: <specific function> = specific_function constants.%F, @F(%T.binding.as_type, %facet_value.loc25_9.2) [symbolic = %F.specific_fn.loc25_3.2 (constants.%F.specific_fn.905)]
+// CHECK:STDOUT:   %Empty.facet.loc25_9.2: @G.%Empty.type.loc20_24.1 (%Empty.type.b8d23b.2) = facet_value %V.loc20_27.1, () [symbolic = %Empty.facet.loc25_9.2 (constants.%Empty.facet.920)]
+// CHECK:STDOUT:   %F.specific_fn.loc25_3.2: <specific function> = specific_function constants.%F, @F(%T.binding.as_type, %Empty.facet.loc25_9.2) [symbolic = %F.specific_fn.loc25_3.2 (constants.%F.specific_fn.905)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   fn() {
 // CHECK:STDOUT:   !entry:
@@ -166,17 +166,17 @@ fn G(T:! Z, U:! Empty(T), V:! type) {
 // CHECK:STDOUT:     %.loc21_11: type = converted %.loc21_9, constants.%empty_struct_type [concrete = constants.%empty_struct_type]
 // CHECK:STDOUT:     %T.as_type.loc21: type = facet_access_type %T.ref.loc21 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
 // CHECK:STDOUT:     %.loc21_18.1: type = converted %T.ref.loc21, %T.as_type.loc21 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
-// CHECK:STDOUT:     %facet_value.loc21_18.1: @G.%Empty.type.loc20_24.1 (%Empty.type.b8d23b.2) = facet_value constants.%empty_struct_type, () [symbolic = %facet_value.loc21_18.2 (constants.%facet_value.6fa)]
-// CHECK:STDOUT:     %.loc21_18.2: @G.%Empty.type.loc20_24.1 (%Empty.type.b8d23b.2) = converted constants.%empty_struct_type, %facet_value.loc21_18.1 [symbolic = %facet_value.loc21_18.2 (constants.%facet_value.6fa)]
-// CHECK:STDOUT:     %F.specific_fn.loc21_3.1: <specific function> = specific_function %F.ref.loc21, @F(constants.%T.binding.as_type, constants.%facet_value.6fa) [symbolic = %F.specific_fn.loc21_3.2 (constants.%F.specific_fn.8ba)]
+// CHECK:STDOUT:     %Empty.facet.loc21_18.1: @G.%Empty.type.loc20_24.1 (%Empty.type.b8d23b.2) = facet_value constants.%empty_struct_type, () [symbolic = %Empty.facet.loc21_18.2 (constants.%Empty.facet.6fa)]
+// CHECK:STDOUT:     %.loc21_18.2: @G.%Empty.type.loc20_24.1 (%Empty.type.b8d23b.2) = converted constants.%empty_struct_type, %Empty.facet.loc21_18.1 [symbolic = %Empty.facet.loc21_18.2 (constants.%Empty.facet.6fa)]
+// CHECK:STDOUT:     %F.specific_fn.loc21_3.1: <specific function> = specific_function %F.ref.loc21, @F(constants.%T.binding.as_type, constants.%Empty.facet.6fa) [symbolic = %F.specific_fn.loc21_3.2 (constants.%F.specific_fn.8ba)]
 // CHECK:STDOUT:     %F.call.loc21: init %empty_tuple.type = call %F.specific_fn.loc21_3.1()
 // CHECK:STDOUT:     %F.ref.loc22: %F.type = name_ref F, file.%F.decl [concrete = constants.%F]
 // CHECK:STDOUT:     %T.ref.loc22: %Z.type = name_ref T, %T.loc20_6.2 [symbolic = %T.loc20_6.1 (constants.%T.3b3)]
 // CHECK:STDOUT:     %T.as_type.loc22: type = facet_access_type %T.ref.loc22 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
 // CHECK:STDOUT:     %.loc22_12.1: type = converted %T.ref.loc22, %T.as_type.loc22 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
-// CHECK:STDOUT:     %facet_value.loc22_12.1: @G.%Empty.type.loc20_24.1 (%Empty.type.b8d23b.2) = facet_value type, () [symbolic = %facet_value.loc22_12.2 (constants.%facet_value.832)]
-// CHECK:STDOUT:     %.loc22_12.2: @G.%Empty.type.loc20_24.1 (%Empty.type.b8d23b.2) = converted type, %facet_value.loc22_12.1 [symbolic = %facet_value.loc22_12.2 (constants.%facet_value.832)]
-// CHECK:STDOUT:     %F.specific_fn.loc22_3.1: <specific function> = specific_function %F.ref.loc22, @F(constants.%T.binding.as_type, constants.%facet_value.832) [symbolic = %F.specific_fn.loc22_3.2 (constants.%F.specific_fn.55c)]
+// CHECK:STDOUT:     %Empty.facet.loc22_12.1: @G.%Empty.type.loc20_24.1 (%Empty.type.b8d23b.2) = facet_value type, () [symbolic = %Empty.facet.loc22_12.2 (constants.%Empty.facet.832)]
+// CHECK:STDOUT:     %.loc22_12.2: @G.%Empty.type.loc20_24.1 (%Empty.type.b8d23b.2) = converted type, %Empty.facet.loc22_12.1 [symbolic = %Empty.facet.loc22_12.2 (constants.%Empty.facet.832)]
+// CHECK:STDOUT:     %F.specific_fn.loc22_3.1: <specific function> = specific_function %F.ref.loc22, @F(constants.%T.binding.as_type, constants.%Empty.facet.832) [symbolic = %F.specific_fn.loc22_3.2 (constants.%F.specific_fn.55c)]
 // CHECK:STDOUT:     %F.call.loc22: init %empty_tuple.type = call %F.specific_fn.loc22_3.1()
 // CHECK:STDOUT:     %F.ref.loc23: %F.type = name_ref F, file.%F.decl [concrete = constants.%F]
 // CHECK:STDOUT:     %T.ref.loc23_5: %Z.type = name_ref T, %T.loc20_6.2 [symbolic = %T.loc20_6.1 (constants.%T.3b3)]
@@ -184,9 +184,9 @@ fn G(T:! Z, U:! Empty(T), V:! type) {
 // CHECK:STDOUT:     %T.as_type.loc23_9.1: type = facet_access_type %T.ref.loc23_5 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
 // CHECK:STDOUT:     %.loc23_9.1: type = converted %T.ref.loc23_5, %T.as_type.loc23_9.1 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
 // CHECK:STDOUT:     %T.as_type.loc23_9.2: type = facet_access_type constants.%T.3b3 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
-// CHECK:STDOUT:     %facet_value.loc23_9.1: @G.%Empty.type.loc20_24.1 (%Empty.type.b8d23b.2) = facet_value %T.as_type.loc23_9.2, () [symbolic = %facet_value.loc23_9.2 (constants.%facet_value.146)]
-// CHECK:STDOUT:     %.loc23_9.2: @G.%Empty.type.loc20_24.1 (%Empty.type.b8d23b.2) = converted constants.%T.3b3, %facet_value.loc23_9.1 [symbolic = %facet_value.loc23_9.2 (constants.%facet_value.146)]
-// CHECK:STDOUT:     %F.specific_fn.loc23_3.1: <specific function> = specific_function %F.ref.loc23, @F(constants.%T.binding.as_type, constants.%facet_value.146) [symbolic = %F.specific_fn.loc23_3.2 (constants.%F.specific_fn.d3f)]
+// CHECK:STDOUT:     %Empty.facet.loc23_9.1: @G.%Empty.type.loc20_24.1 (%Empty.type.b8d23b.2) = facet_value %T.as_type.loc23_9.2, () [symbolic = %Empty.facet.loc23_9.2 (constants.%Empty.facet.146)]
+// CHECK:STDOUT:     %.loc23_9.2: @G.%Empty.type.loc20_24.1 (%Empty.type.b8d23b.2) = converted constants.%T.3b3, %Empty.facet.loc23_9.1 [symbolic = %Empty.facet.loc23_9.2 (constants.%Empty.facet.146)]
+// CHECK:STDOUT:     %F.specific_fn.loc23_3.1: <specific function> = specific_function %F.ref.loc23, @F(constants.%T.binding.as_type, constants.%Empty.facet.146) [symbolic = %F.specific_fn.loc23_3.2 (constants.%F.specific_fn.d3f)]
 // CHECK:STDOUT:     %F.call.loc23: init %empty_tuple.type = call %F.specific_fn.loc23_3.1()
 // CHECK:STDOUT:     %F.ref.loc24: %F.type = name_ref F, file.%F.decl [concrete = constants.%F]
 // CHECK:STDOUT:     %T.ref.loc24: %Z.type = name_ref T, %T.loc20_6.2 [symbolic = %T.loc20_6.1 (constants.%T.3b3)]
@@ -200,9 +200,9 @@ fn G(T:! Z, U:! Empty(T), V:! type) {
 // CHECK:STDOUT:     %V.ref: type = name_ref V, %V.loc20_27.2 [symbolic = %V.loc20_27.1 (constants.%V)]
 // CHECK:STDOUT:     %T.as_type.loc25: type = facet_access_type %T.ref.loc25 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
 // CHECK:STDOUT:     %.loc25_9.1: type = converted %T.ref.loc25, %T.as_type.loc25 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
-// CHECK:STDOUT:     %facet_value.loc25_9.1: @G.%Empty.type.loc20_24.1 (%Empty.type.b8d23b.2) = facet_value constants.%V, () [symbolic = %facet_value.loc25_9.2 (constants.%facet_value.920)]
-// CHECK:STDOUT:     %.loc25_9.2: @G.%Empty.type.loc20_24.1 (%Empty.type.b8d23b.2) = converted constants.%V, %facet_value.loc25_9.1 [symbolic = %facet_value.loc25_9.2 (constants.%facet_value.920)]
-// CHECK:STDOUT:     %F.specific_fn.loc25_3.1: <specific function> = specific_function %F.ref.loc25, @F(constants.%T.binding.as_type, constants.%facet_value.920) [symbolic = %F.specific_fn.loc25_3.2 (constants.%F.specific_fn.905)]
+// CHECK:STDOUT:     %Empty.facet.loc25_9.1: @G.%Empty.type.loc20_24.1 (%Empty.type.b8d23b.2) = facet_value constants.%V, () [symbolic = %Empty.facet.loc25_9.2 (constants.%Empty.facet.920)]
+// CHECK:STDOUT:     %.loc25_9.2: @G.%Empty.type.loc20_24.1 (%Empty.type.b8d23b.2) = converted constants.%V, %Empty.facet.loc25_9.1 [symbolic = %Empty.facet.loc25_9.2 (constants.%Empty.facet.920)]
+// CHECK:STDOUT:     %F.specific_fn.loc25_3.1: <specific function> = specific_function %F.ref.loc25, @F(constants.%T.binding.as_type, constants.%Empty.facet.920) [symbolic = %F.specific_fn.loc25_3.2 (constants.%F.specific_fn.905)]
 // CHECK:STDOUT:     %F.call.loc25: init %empty_tuple.type = call %F.specific_fn.loc25_3.1()
 // CHECK:STDOUT:     return
 // CHECK:STDOUT:   }
@@ -232,28 +232,28 @@ fn G(T:! Z, U:! Empty(T), V:! type) {
 // CHECK:STDOUT:   %V.loc20_27.1 => constants.%V
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @F(constants.%T.binding.as_type, constants.%facet_value.6fa) {
+// CHECK:STDOUT: specific @F(constants.%T.binding.as_type, constants.%Empty.facet.6fa) {
 // CHECK:STDOUT:   %T.loc18_6.1 => constants.%T.binding.as_type
 // CHECK:STDOUT:   %Empty.type.loc18_27.1 => constants.%Empty.type.b8d23b.2
-// CHECK:STDOUT:   %U.loc18_16.1 => constants.%facet_value.6fa
+// CHECK:STDOUT:   %U.loc18_16.1 => constants.%Empty.facet.6fa
 // CHECK:STDOUT:   %pattern_type => constants.%pattern_type.e25e9f.2
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @F(constants.%T.binding.as_type, constants.%facet_value.832) {
+// CHECK:STDOUT: specific @F(constants.%T.binding.as_type, constants.%Empty.facet.832) {
 // CHECK:STDOUT:   %T.loc18_6.1 => constants.%T.binding.as_type
 // CHECK:STDOUT:   %Empty.type.loc18_27.1 => constants.%Empty.type.b8d23b.2
-// CHECK:STDOUT:   %U.loc18_16.1 => constants.%facet_value.832
+// CHECK:STDOUT:   %U.loc18_16.1 => constants.%Empty.facet.832
 // CHECK:STDOUT:   %pattern_type => constants.%pattern_type.e25e9f.2
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @F(constants.%T.binding.as_type, constants.%facet_value.146) {
+// CHECK:STDOUT: specific @F(constants.%T.binding.as_type, constants.%Empty.facet.146) {
 // CHECK:STDOUT:   %T.loc18_6.1 => constants.%T.binding.as_type
 // CHECK:STDOUT:   %Empty.type.loc18_27.1 => constants.%Empty.type.b8d23b.2
-// CHECK:STDOUT:   %U.loc18_16.1 => constants.%facet_value.146
+// CHECK:STDOUT:   %U.loc18_16.1 => constants.%Empty.facet.146
 // CHECK:STDOUT:   %pattern_type => constants.%pattern_type.e25e9f.2
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
@@ -268,10 +268,10 @@ fn G(T:! Z, U:! Empty(T), V:! type) {
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @F(constants.%T.binding.as_type, constants.%facet_value.920) {
+// CHECK:STDOUT: specific @F(constants.%T.binding.as_type, constants.%Empty.facet.920) {
 // CHECK:STDOUT:   %T.loc18_6.1 => constants.%T.binding.as_type
 // CHECK:STDOUT:   %Empty.type.loc18_27.1 => constants.%Empty.type.b8d23b.2
-// CHECK:STDOUT:   %U.loc18_16.1 => constants.%facet_value.920
+// CHECK:STDOUT:   %U.loc18_16.1 => constants.%Empty.facet.920
 // CHECK:STDOUT:   %pattern_type => constants.%pattern_type.e25e9f.2
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:

toolchain/check/testdata/named_constraint/import_constraint_decl.carbon

@@ -92,6 +92,8 @@ impl C as B {}
 // CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
 // CHECK:STDOUT:   %.Self: %type = symbolic_binding .Self [symbolic_self]
 // CHECK:STDOUT:   %B.type: type = facet_type <@B> [concrete]
+// CHECK:STDOUT:   %Self.861: %type = symbolic_binding Self, 0 [symbolic]
+// CHECK:STDOUT:   %Self.binding.as_type: type = symbolic_binding_type Self, 0, %Self.861 [symbolic]
 // CHECK:STDOUT:   %T: %B.type = symbolic_binding T, 0 [symbolic]
 // CHECK:STDOUT:   %pattern_type: type = pattern_type %B.type [concrete]
 // CHECK:STDOUT:   %F.type: type = fn_type @F [concrete]
@@ -101,7 +103,10 @@ impl C as B {}
 // CHECK:STDOUT: imports {
 // CHECK:STDOUT:   %Main.I = import_ref Main//b, I, unloaded
 // CHECK:STDOUT:   %Main.B: type = import_ref Main//b, B, loaded [concrete = constants.%B.type]
-// CHECK:STDOUT:   %Main.import_ref = import_ref Main//b, loc4_14, unloaded
+// CHECK:STDOUT:   %Main.import_ref.8df = import_ref Main//b, loc3_13, unloaded
+// CHECK:STDOUT:   %Main.import_ref.b7c: type = import_ref Main//b, loc5_18, loaded [symbolic = constants.%Self.binding.as_type]
+// CHECK:STDOUT:   %Main.import_ref.dec: %type = import_ref Main//b, loc4_14, loaded [symbolic = constants.%Self.861]
+// CHECK:STDOUT:   %Main.import_ref.cae = import_ref Main//b, loc4_14, unloaded
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
@@ -123,11 +128,27 @@ impl C as B {}
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
+// CHECK:STDOUT: interface @I [from "b.carbon"] {
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = imports.%Main.import_ref.8df
+// CHECK:STDOUT:   witness = ()
+// CHECK:STDOUT:
+// CHECK:STDOUT: !requires:
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
 // CHECK:STDOUT: constraint @B [from "b.carbon"] {
 // CHECK:STDOUT: !members:
-// CHECK:STDOUT:   .Self = imports.%Main.import_ref
+// CHECK:STDOUT:   .Self = imports.%Main.import_ref.cae
 // CHECK:STDOUT:
 // CHECK:STDOUT: !requires:
+// CHECK:STDOUT:   @B.require0 {
+// CHECK:STDOUT:     require imports.%Main.import_ref.b7c impls <@I>
+// CHECK:STDOUT:   }
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: generic require @B.require0(imports.%Main.import_ref.dec: %type) [from "b.carbon"] {
+// CHECK:STDOUT:   %Self: %type = symbolic_binding Self, 0 [symbolic = %Self (constants.%Self.861)]
+// CHECK:STDOUT:   %Self.binding.as_type: type = symbolic_binding_type Self, 0, %Self [symbolic = %Self.binding.as_type (constants.%Self.binding.as_type)]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: generic fn @F(%T.loc4_6.2: %B.type) {
@@ -141,6 +162,11 @@ impl C as B {}
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
+// CHECK:STDOUT: specific @B.require0(constants.%Self.861) {
+// CHECK:STDOUT:   %Self => constants.%Self.861
+// CHECK:STDOUT:   %Self.binding.as_type => constants.%Self.binding.as_type
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
 // CHECK:STDOUT: specific @F(constants.%T) {
 // CHECK:STDOUT:   %T.loc4_6.1 => constants.%T
 // CHECK:STDOUT: }

toolchain/check/testdata/named_constraint/require.carbon

@@ -327,7 +327,9 @@ constraint Z {
 // CHECK:STDOUT:   .Y = <poisoned>
 // CHECK:STDOUT:
 // CHECK:STDOUT: !requires:
-// CHECK:STDOUT:   @Z.require0
+// CHECK:STDOUT:   @Z.require0 {
+// CHECK:STDOUT:     require @Z.require0.%Self.as_type impls <@Y>
+// CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: generic require @Z.require0(@Z.%Self: %Z.type) {
@@ -370,7 +372,9 @@ constraint Z {
 // CHECK:STDOUT:   .Y = <poisoned>
 // CHECK:STDOUT:
 // CHECK:STDOUT: !requires:
-// CHECK:STDOUT:   @Z.require0
+// CHECK:STDOUT:   @Z.require0 {
+// CHECK:STDOUT:     require @Z.require0.%Self.as_type impls <@Y>
+// CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: generic require @Z.require0(@Z.%Self: %Z.type) {
@@ -415,7 +419,9 @@ constraint Z {
 // CHECK:STDOUT:   .Y = <poisoned>
 // CHECK:STDOUT:
 // CHECK:STDOUT: !requires:
-// CHECK:STDOUT:   @Z.require0
+// CHECK:STDOUT:   @Z.require0 {
+// CHECK:STDOUT:     require @Z.require0.%.loc9 impls <@Y>
+// CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: generic require @Z.require0(@Z.%Self: %Z.type) {
@@ -466,7 +472,9 @@ constraint Z {
 // CHECK:STDOUT:   .Y = <poisoned>
 // CHECK:STDOUT:
 // CHECK:STDOUT: !requires:
-// CHECK:STDOUT:   @Z.require0
+// CHECK:STDOUT:   @Z.require0 {
+// CHECK:STDOUT:     require @Z.require0.%C.loc9_17.1 impls <@Y>
+// CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: generic require @Z.require0(@Z.%Self: %Z.type) {
@@ -532,7 +540,9 @@ constraint Z {
 // CHECK:STDOUT:   .Y = <poisoned>
 // CHECK:STDOUT:
 // CHECK:STDOUT: !requires:
-// CHECK:STDOUT:   @Z.require0
+// CHECK:STDOUT:   @Z.require0 {
+// CHECK:STDOUT:     require @Z.require0.%Self.as_type impls <@Y where constants.%impl.elem0 = constants.%empty_tuple.type>
+// CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: generic require @Z.require0(@Z.%Self: %Z.type) {
@@ -740,7 +750,9 @@ constraint Z {
 // CHECK:STDOUT:   .Y = <poisoned>
 // CHECK:STDOUT:
 // CHECK:STDOUT: !requires:
-// CHECK:STDOUT:   @Z.require0
+// CHECK:STDOUT:   @Z.require0 {
+// CHECK:STDOUT:     require @Z.require0.%Self.as_type.loc10_11 impls <@Y where constants.%impl.elem0 = constants.%Self.binding.as_type>
+// CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: generic require @Z.require0(@Z.%Self: %Z.type) {

toolchain/sem_ir/facet_type_info.h

@@ -42,6 +42,11 @@ class BuiltinConstraintMask
 CARBON_BUILTIN_CONSTRAINT_MASK(CARBON_BUILTIN_CONSTRAINT_MASK_WITH_TYPE)
 #undef CARBON_BUILTIN_CONSTRAINT_MASK_WITH_TYPE
 
+// A representation of a facet type that extends a single interface or
+// named constraint.
+using SingleExtendFacetType =
+    std::variant<SpecificInterface, SpecificNamedConstraint>;
+
 struct FacetTypeInfo : Printable<FacetTypeInfo> {
   // Returns a FacetTypeInfo that combines `lhs` and `rhs`. It is not
   // canonicalized, so that it can be further modified by the caller if desired.
@@ -98,18 +103,24 @@ struct FacetTypeInfo : Printable<FacetTypeInfo> {
 
   auto Print(llvm::raw_ostream& out) const -> void;
 
-  // In some cases, a facet type is expected to represent a single interface.
-  // For example, an interface declaration or an associated constant are
-  // associated with a facet type that will always be a single interface with no
-  // other constraints. This returns the single interface that this facet type
-  // represents, or `std::nullopt` if it has any other constraints.
-  auto TryAsSingleInterface() const -> std::optional<ImplsConstraint> {
-    if (extend_constraints.size() == 1 && self_impls_constraints.empty() &&
-        extend_named_constraints.empty() &&
-        self_impls_named_constraints.empty() && rewrite_constraints.empty() &&
-        builtin_constraint_mask.empty() && !other_requirements) {
+  // In some cases, a facet type is expected to represent a single interface or
+  // named constraint. For example, an interface declaration, or an associated
+  // constant are associated with a facet type that will always be a single
+  // interface with no other requirements. This returns the single interface or
+  // named constraint that this facet type represents, or `std::nullopt` if it
+  // has any other requirements.
+  auto TryAsSingleExtend() const -> std::optional<SingleExtendFacetType> {
+    if (!self_impls_constraints.empty() ||
+        !self_impls_named_constraints.empty() || !rewrite_constraints.empty() ||
+        !builtin_constraint_mask.empty() || other_requirements) {
+      return std::nullopt;
+    }
+    if (extend_constraints.size() == 1 && extend_named_constraints.empty()) {
       return extend_constraints.front();
     }
+    if (extend_constraints.empty() && extend_named_constraints.size() == 1) {
+      return extend_named_constraints.front();
+    }
     return std::nullopt;
   }
 

toolchain/sem_ir/formatter.cpp

@@ -1185,22 +1185,9 @@ auto Formatter::FormatInstRhs(Inst inst) -> void {
 
     case CARBON_KIND(RequireImplsDecl decl): {
       FormatArgs(decl.require_impls_id);
-
-      const auto& require = sem_ir_->require_impls().Get(decl.require_impls_id);
-
       llvm::SaveAndRestore scope(
           scope_, inst_namer_.GetScopeFor(decl.require_impls_id));
-
-      out_ << ' ';
-      OpenBrace();
-      Indent();
-      out_ << "require ";
-      FormatArg(require.self_id);
-      out_ << " impls ";
-      FormatArg(require.facet_type_id);
-      out_ << "\n";
-      CloseBrace();
-
+      FormatRequireImpls(decl.require_impls_id);
       FormatTrailingBlock(decl.decl_block_id);
       return;
     }
@@ -1380,6 +1367,20 @@ auto Formatter::FormatImportRefRhs(AnyImportRef inst) -> void {
        << (inst.kind == InstKind::ImportRefLoaded ? "loaded" : "unloaded");
 }
 
+auto Formatter::FormatRequireImpls(RequireImplsId id) -> void {
+  out_ << ' ';
+
+  const auto& require = sem_ir_->require_impls().Get(id);
+  OpenBrace();
+  Indent();
+  out_ << "require ";
+  FormatArg(require.self_id);
+  out_ << " impls ";
+  FormatArg(require.facet_type_id);
+  out_ << "\n";
+  CloseBrace();
+}
+
 auto Formatter::FormatRequireImplsBlock(RequireImplsBlockId block_id) -> void {
   IndentLabel();
   out_ << "!requires:\n";
@@ -1389,6 +1390,7 @@ auto Formatter::FormatRequireImplsBlock(RequireImplsBlockId block_id) -> void {
   for (auto require_impls_id : sem_ir_->require_impls_blocks().Get(block_id)) {
     Indent();
     FormatArg(require_impls_id);
+    FormatRequireImpls(require_impls_id);
     out_ << "\n";
   }
 }

toolchain/sem_ir/formatter.h

@@ -225,6 +225,9 @@ class Formatter {
   // Prints the contents of a name scope, with an optional label.
   auto FormatNameScope(NameScopeId id, llvm::StringRef label = "") -> void;
 
+  // Prints the contents of a require impls as a block.
+  auto FormatRequireImpls(RequireImplsId id) -> void;
+
   // Prints a single instruction. This typically formats as:
   //   `FormatInstLhs()` `<ir_name>` `FormatInstRhs()` `<constant>`
   //

toolchain/sem_ir/impl.cpp

@@ -4,7 +4,10 @@
 
 #include "toolchain/sem_ir/impl.h"
 
+#include "toolchain/base/kind_switch.h"
 #include "toolchain/sem_ir/file.h"
+#include "toolchain/sem_ir/specific_interface.h"
+#include "toolchain/sem_ir/specific_named_constraint.h"
 
 namespace Carbon::SemIR {
 
@@ -20,9 +23,19 @@ auto ImplStore::GetOrAddLookupBucket(const Impl& impl) -> LookupBucketRef {
   if (auto facet_type = sem_ir_.types().TryGetAs<FacetType>(facet_type_id)) {
     const FacetTypeInfo& facet_type_info =
         sem_ir_.facet_types().Get(facet_type->facet_type_id);
-    if (auto interface_type = facet_type_info.TryAsSingleInterface()) {
-      interface_id = interface_type->interface_id;
-      specific_id = interface_type->specific_id;
+    if (auto single = facet_type_info.TryAsSingleExtend()) {
+      CARBON_KIND_SWITCH(*single) {
+        case CARBON_KIND(SemIR::SpecificInterface interface): {
+          interface_id = interface.interface_id;
+          specific_id = interface.specific_id;
+          break;
+        }
+        case CARBON_KIND(SemIR::SpecificNamedConstraint _): {
+          // TODO: Handle named constraints which resolve to a single interface
+          // in the IdentifiedFacetType.
+          break;
+        }
+      }
     }
   }
   return LookupBucketRef(

toolchain/sem_ir/inst_namer.cpp

@@ -25,6 +25,8 @@
 #include "toolchain/sem_ir/inst_kind.h"
 #include "toolchain/sem_ir/pattern.h"
 #include "toolchain/sem_ir/singleton_insts.h"
+#include "toolchain/sem_ir/specific_interface.h"
+#include "toolchain/sem_ir/specific_named_constraint.h"
 #include "toolchain/sem_ir/type_info.h"
 #include "toolchain/sem_ir/typed_insts.h"
 
@@ -618,7 +620,8 @@ auto InstNamer::PushEntity(RequireImplsId require_impls_id, ScopeId scope_id,
       llvm::formatv("{0}{1}require{2}", scope_prefix,
                     scope_prefix.empty() ? "" : ".", require_impls_id.index));
 
-  AddBlockLabel(scope_id, require.body_block_id, "require", require_loc);
+  auto decl = sem_ir_->insts().GetAs<SemIR::RequireImplsDecl>(require.decl_id);
+  AddBlockLabel(scope_id, decl.decl_block_id, "require", require_loc);
 
   // Push blocks in reverse order.
   PushGeneric(scope_id, require.generic_id);
@@ -960,8 +963,18 @@ auto InstNamer::NamingContext::NameInst() -> void {
               sem_ir().types().TryGetAs<FacetType>(inst.type_id)) {
         const auto& facet_type_info =
             sem_ir().facet_types().Get(facet_type->facet_type_id);
-        if (auto interface = facet_type_info.TryAsSingleInterface()) {
-          AddEntityNameAndMaybePush(interface->interface_id, ".facet");
+        if (auto single = facet_type_info.TryAsSingleExtend()) {
+          CARBON_KIND_SWITCH(*single) {
+            case CARBON_KIND(SemIR::SpecificInterface interface): {
+              AddEntityNameAndMaybePush(interface.interface_id, ".facet");
+              break;
+            }
+            case CARBON_KIND(SemIR::SpecificNamedConstraint constraint): {
+              AddEntityNameAndMaybePush(constraint.named_constraint_id,
+                                        ".facet");
+              break;
+            }
+          }
           return;
         }
       }

toolchain/sem_ir/require_impls.h

@@ -29,9 +29,6 @@ struct RequireImpls : Printable<RequireImpls> {
   InstId decl_id;
   // The interface or named constraint which contains the `require` declaration.
   NameScopeId parent_scope_id;
-  // The instructions that make up the `require` declaration. It will contain
-  // instructions that provide the `self_id` and `facet_type_inst_id`.
-  InstBlockId body_block_id;
   // A `require` declaration is always generic over `Self` since it's inside an
   // interface or named constraint definition.
   GenericId generic_id;