Explorar el Código

Make named constraint eval to a FacetType with itself in it (#6308)

This requires declared FacetTypes to hold NamedConstraintIds (along with
a specific) that are named in an extend or impls requirement. We add
support to stringify and formatter to display the named constraints in
the facet type, and special case when a facet type contains a single
extend named constraint, like we did for a single extend interface.

This means that `RequireIndentifiedFacetType` can now fail, if the facet
type contains a forward-declared named constraint. Add the appropriate
diagnostics for each call to this function, and note the ones that
should change to `RequireCompleteFacetType` in the future with TODOs.

We also add tests for using facet types that can or can't be identified,
or completed, with named constraints in them.
Dana Jansens hace 6 meses
padre
commit
ca3f95faa6

+ 23 - 6
toolchain/check/eval.cpp

@@ -623,19 +623,36 @@ static auto GetConstantFacetTypeInfo(EvalContext& eval_context,
       .other_requirements = orig.other_requirements};
 
   info.extend_constraints.reserve(orig.extend_constraints.size());
-  for (const auto& interface : orig.extend_constraints) {
+  for (const auto& extend : orig.extend_constraints) {
     info.extend_constraints.push_back(
-        {.interface_id = interface.interface_id,
+        {.interface_id = extend.interface_id,
          .specific_id =
-             GetConstantValue(eval_context, interface.specific_id, phase)});
+             GetConstantValue(eval_context, extend.specific_id, phase)});
   }
 
   info.self_impls_constraints.reserve(orig.self_impls_constraints.size());
-  for (const auto& interface : orig.self_impls_constraints) {
+  for (const auto& self_impls : orig.self_impls_constraints) {
     info.self_impls_constraints.push_back(
-        {.interface_id = interface.interface_id,
+        {.interface_id = self_impls.interface_id,
          .specific_id =
-             GetConstantValue(eval_context, interface.specific_id, phase)});
+             GetConstantValue(eval_context, self_impls.specific_id, phase)});
+  }
+
+  info.extend_named_constraints.reserve(orig.extend_named_constraints.size());
+  for (const auto& extend : orig.extend_named_constraints) {
+    info.extend_named_constraints.push_back(
+        {.named_constraint_id = extend.named_constraint_id,
+         .specific_id =
+             GetConstantValue(eval_context, extend.specific_id, phase)});
+  }
+
+  info.self_impls_named_constraints.reserve(
+      orig.self_impls_named_constraints.size());
+  for (const auto& self_impls : orig.self_impls_named_constraints) {
+    info.self_impls_named_constraints.push_back(
+        {.named_constraint_id = self_impls.named_constraint_id,
+         .specific_id =
+             GetConstantValue(eval_context, self_impls.specific_id, phase)});
   }
 
   // Rewrite constraints are resolved first before replacing them with their

+ 4 - 2
toolchain/check/eval_inst.cpp

@@ -448,7 +448,8 @@ auto EvalConstantInst(Context& context, SemIR::InterfaceDecl inst)
         .type_id = inst.type_id, .elements_id = SemIR::InstBlockId::Empty});
   }
 
-  // A non-parameterized interface declaration evaluates to a facet type.
+  // A non-parameterized interface declaration evaluates to a declared facet
+  // type containing just the interface.
   return ConstantEvalResult::NewAnyPhase(FacetTypeFromInterface(
       context, inst.interface_id,
       context.generics().GetSelfSpecific(interface_info.generic_id)));
@@ -467,7 +468,8 @@ auto EvalConstantInst(Context& context, SemIR::NamedConstraintDecl inst)
         .type_id = inst.type_id, .elements_id = SemIR::InstBlockId::Empty});
   }
 
-  // A non-parameterized named constraint declaration evaluates to a facet type.
+  // A non-parameterized named constraint declaration evaluates to a declared
+  // facet type containing just the named constraint.
   return ConstantEvalResult::NewAnyPhase(FacetTypeFromNamedConstraint(
       context, inst.named_constraint_id,
       context.generics().GetSelfSpecific(named_constraint_info.generic_id)));

+ 5 - 9
toolchain/check/facet_type.cpp

@@ -26,22 +26,18 @@ namespace Carbon::Check {
 auto FacetTypeFromInterface(Context& context, SemIR::InterfaceId interface_id,
                             SemIR::SpecificId specific_id) -> SemIR::FacetType {
   auto info = SemIR::FacetTypeInfo{};
-
   info.extend_constraints.push_back({interface_id, specific_id});
-  // TODO: Add `require impls` to the set of constraints.
-
   info.Canonicalize();
   SemIR::FacetTypeId facet_type_id = context.facet_types().Add(info);
   return {.type_id = SemIR::TypeType::TypeId, .facet_type_id = facet_type_id};
 }
 
-auto FacetTypeFromNamedConstraint(
-    Context& context, SemIR::NamedConstraintId /*named_constraint_id*/,
-    SemIR::SpecificId /*specific_id*/) -> SemIR::FacetType {
+auto FacetTypeFromNamedConstraint(Context& context,
+                                  SemIR::NamedConstraintId named_constraint_id,
+                                  SemIR::SpecificId specific_id)
+    -> SemIR::FacetType {
   auto info = SemIR::FacetTypeInfo{};
-
-  // TODO: Add `require impls` to the set of constraints.
-
+  info.extend_named_constraints.push_back({named_constraint_id, specific_id});
   info.Canonicalize();
   SemIR::FacetTypeId facet_type_id = context.facet_types().Add(info);
   return {.type_id = SemIR::TypeType::TypeId, .facet_type_id = facet_type_id};

+ 13 - 1
toolchain/check/handle_require.cpp

@@ -167,7 +167,19 @@ auto HandleParseNode(Context& context, Parse::RequireDeclId node_id) -> bool {
   }
 
   auto identified_facet_type_id =
-      RequireIdentifiedFacetType(context, *constraint_facet_type);
+      RequireIdentifiedFacetType(context, *constraint_facet_type, [&] {
+        CARBON_DIAGNOSTIC(
+            RequireImplsUnidentifiedFacetType, Error,
+            "facet type {0} cannot be identified in `require` declaration",
+            InstIdAsType);
+        return context.emitter().Build(constraint_node_id,
+                                       RequireImplsUnidentifiedFacetType,
+                                       constraint_inst_id);
+      });
+  if (!identified_facet_type_id.has_value()) {
+    // The constraint can't be used.
+    return true;
+  }
   const auto& identified =
       context.identified_facet_types().Get(identified_facet_type_id);
 

+ 10 - 1
toolchain/check/impl.cpp

@@ -296,7 +296,16 @@ auto CheckConstraintIsInterface(Context& context, SemIR::InstId impl_decl_id,
     return SemIR::SpecificInterface::None;
   }
 
-  auto identified_id = RequireIdentifiedFacetType(context, *facet_type);
+  auto identified_id = RequireIdentifiedFacetType(context, *facet_type, [&] {
+    CARBON_DIAGNOSTIC(ImplOfUnidentifiedFacetType, Error,
+                      "facet type {0} cannot be identified in `impl as`",
+                      InstIdAsType);
+    return context.emitter().Build(impl_decl_id, ImplOfUnidentifiedFacetType,
+                                   constraint_id);
+  });
+  if (!identified_id.has_value()) {
+    return SemIR::SpecificInterface::None;
+  }
   const auto& identified = context.identified_facet_types().Get(identified_id);
   if (!identified.is_valid_impl_as_target()) {
     CARBON_DIAGNOSTIC(ImplOfNotOneInterface, Error,

+ 38 - 15
toolchain/check/impl_lookup.cpp

@@ -184,7 +184,7 @@ static auto FindAndDiagnoseImplLookupCycle(
 }
 
 struct InterfacesFromConstantId {
-  llvm::SmallVector<SemIR::SpecificInterface> interfaces;
+  llvm::ArrayRef<SemIR::SpecificInterface> interfaces;
   SemIR::BuiltinConstraintMask builtin_constraint_mask;
   bool other_requirements;
 };
@@ -192,23 +192,31 @@ struct InterfacesFromConstantId {
 // Gets the set of `SpecificInterface`s that are required by a facet type
 // (as a constant value), and any special requirements.
 static auto GetInterfacesFromConstantId(
-    Context& context, SemIR::ConstantId query_facet_type_const_id)
-    -> InterfacesFromConstantId {
+    Context& context, SemIR::LocId loc_id,
+    SemIR::ConstantId query_facet_type_const_id)
+    -> std::optional<InterfacesFromConstantId> {
   auto facet_type_inst_id =
       context.constant_values().GetInstId(query_facet_type_const_id);
   auto facet_type_inst =
       context.insts().GetAs<SemIR::FacetType>(facet_type_inst_id);
   const auto& facet_type_info =
       context.facet_types().Get(facet_type_inst.facet_type_id);
-  auto identified_id = RequireIdentifiedFacetType(context, facet_type_inst);
-  auto interfaces_array_ref =
-      context.identified_facet_types().Get(identified_id).required_interfaces();
-  // Returns a copy to avoid use-after-free when the identified_facet_types
-  // store resizes.
-  return {
-      .interfaces = {interfaces_array_ref.begin(), interfaces_array_ref.end()},
-      .builtin_constraint_mask = facet_type_info.builtin_constraint_mask,
-      .other_requirements = facet_type_info.other_requirements};
+  // TODO: Get the complete facet type here.
+  auto identified_id =
+      RequireIdentifiedFacetType(context, facet_type_inst, [&] {
+        CARBON_DIAGNOSTIC(ImplLookupInIncompleteFacetType, Error,
+                          "facet type {0} is incomplete", InstIdAsType);
+        return context.emitter().Build(loc_id, ImplLookupInIncompleteFacetType,
+                                       facet_type_inst_id);
+      });
+  if (!identified_id.has_value()) {
+    return std::nullopt;
+  }
+  return {{.interfaces = context.identified_facet_types()
+                             .Get(identified_id)
+                             .required_interfaces(),
+           .builtin_constraint_mask = facet_type_info.builtin_constraint_mask,
+           .other_requirements = facet_type_info.other_requirements}};
 }
 
 static auto GetWitnessIdForImpl(Context& context, SemIR::LocId loc_id,
@@ -313,8 +321,18 @@ static auto LookupImplWitnessInSelfFacetValue(
   }
 
   // The position of the interface in `required_interfaces()` is also the
-  // position of the witness for that interface in `FacetValue`.
-  auto identified_id = RequireIdentifiedFacetType(context, *facet_type);
+  // position of the witness for that interface in `FacetValue`. The
+  // `FacetValue` witnesses are the output of an impl lookup, which finds and
+  // returns witnesses in the same order.
+  //
+  // TODO: Get the complete facet type here.
+  auto identified_id =
+      RequireIdentifiedFacetType(context, *facet_type, nullptr);
+  // This should not be possible as FacetValue is constructed by a conversion
+  // to a facet type, which performs impl lookup for that facet type, and
+  // lookup only succeeds for complete facet types.
+  CARBON_CHECK(identified_id.has_value(),
+               "FacetValue was constructed with an incomplete facet type");
   auto facet_type_required_interfaces =
       llvm::enumerate(context.identified_facet_types()
                           .Get(identified_id)
@@ -589,8 +607,13 @@ auto LookupImplWitness(Context& context, SemIR::LocId loc_id,
         context.constant_values().GetInstId(query_facet_type_const_id)));
   }
 
+  auto interfaces_from_constant_id =
+      GetInterfacesFromConstantId(context, loc_id, query_facet_type_const_id);
+  if (!interfaces_from_constant_id) {
+    return SemIR::InstBlockIdOrError::MakeError();
+  }
   auto [interfaces, builtin_constraint_mask, other_requirements] =
-      GetInterfacesFromConstantId(context, query_facet_type_const_id);
+      *interfaces_from_constant_id;
   if (other_requirements) {
     // TODO: Remove this when other requirements go away.
     return SemIR::InstBlockId::None;

+ 69 - 12
toolchain/check/testdata/facet/fail_incomplete.carbon

@@ -10,6 +10,9 @@
 // TIP: To dump output, run:
 // TIP:   bazel run //toolchain/testing:file_test -- --dump_output --file_tests=toolchain/check/testdata/facet/fail_incomplete.carbon
 
+// --- fail_incomplete_interface.carbon
+library "[[@TEST_NAME]]";
+
 interface A;
 interface B {}
 class C {}
@@ -18,31 +21,85 @@ fn G[T:! A](t: T) {}
 fn H[T:! A & B](t: T) {}
 
 fn F() {
-  // CHECK:STDERR: fail_incomplete.carbon:[[@LINE+4]]:17: error: cannot convert type `C` into type implementing `A` [ConversionFailureTypeToFacet]
-  // CHECK:STDERR:   ({} as C) as (C as A);
-  // CHECK:STDERR:                 ^~~~~~
+  // CHECK:STDERR: fail_incomplete_interface.carbon:[[@LINE+4]]:3: error: cannot convert type `C` into type implementing `A` [ConversionFailureTypeToFacet]
+  // CHECK:STDERR:   C as A;
+  // CHECK:STDERR:   ^~~~~~
+  // CHECK:STDERR:
+  C as A;
+
+  // CHECK:STDERR: fail_incomplete_interface.carbon:[[@LINE+4]]:3: error: cannot convert type `C` into type implementing `A & B` [ConversionFailureTypeToFacet]
+  // CHECK:STDERR:   C as (A & B);
+  // CHECK:STDERR:   ^~~~~~~~~~~~
+  // CHECK:STDERR:
+  C as (A & B);
+
+  // CHECK:STDERR: fail_incomplete_interface.carbon:[[@LINE+7]]:3: error: cannot convert type `C` into type implementing `A` [ConversionFailureTypeToFacet]
+  // CHECK:STDERR:   G({} as C);
+  // CHECK:STDERR:   ^~~~~~~~~~
+  // CHECK:STDERR: fail_incomplete_interface.carbon:[[@LINE-19]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
+  // CHECK:STDERR: fn G[T:! A](t: T) {}
+  // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR:
+  G({} as C);
+
+  // CHECK:STDERR: fail_incomplete_interface.carbon:[[@LINE+7]]:3: error: cannot convert type `C` into type implementing `A & B` [ConversionFailureTypeToFacet]
+  // CHECK:STDERR:   H({} as C);
+  // CHECK:STDERR:   ^~~~~~~~~~
+  // CHECK:STDERR: fail_incomplete_interface.carbon:[[@LINE-27]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
+  // CHECK:STDERR: fn H[T:! A & B](t: T) {}
+  // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR:
+  H({} as C);
+}
+
+// --- fail_incomplete_constraint.carbon
+library "[[@TEST_NAME]]";
+
+constraint A;
+interface B {}
+class C {}
+
+fn G[T:! A](t: T) {}
+fn H[T:! A & B](t: T) {}
+
+fn F() {
+  // CHECK:STDERR: fail_incomplete_constraint.carbon:[[@LINE+7]]:3: error: facet type `A` is incomplete [ImplLookupInIncompleteFacetType]
+  // CHECK:STDERR:   C as A;
+  // CHECK:STDERR:   ^~~~~~
+  // CHECK:STDERR: fail_incomplete_constraint.carbon:[[@LINE-11]]:1: note: constraint was forward declared here [NamedConstraintForwardDeclaredHere]
+  // CHECK:STDERR: constraint A;
+  // CHECK:STDERR: ^~~~~~~~~~~~~
   // CHECK:STDERR:
-  ({} as C) as (C as A);
+  C as A;
 
-  // CHECK:STDERR: fail_incomplete.carbon:[[@LINE+4]]:17: error: cannot convert type `C` into type implementing `A & B` [ConversionFailureTypeToFacet]
-  // CHECK:STDERR:   ({} as C) as (C as (A & B));
-  // CHECK:STDERR:                 ^~~~~~~~~~~~
+  // CHECK:STDERR: fail_incomplete_constraint.carbon:[[@LINE+7]]:3: error: facet type `B & A` is incomplete [ImplLookupInIncompleteFacetType]
+  // CHECK:STDERR:   C as (A & B);
+  // CHECK:STDERR:   ^~~~~~~~~~~~
+  // CHECK:STDERR: fail_incomplete_constraint.carbon:[[@LINE-20]]:1: note: constraint was forward declared here [NamedConstraintForwardDeclaredHere]
+  // CHECK:STDERR: constraint A;
+  // CHECK:STDERR: ^~~~~~~~~~~~~
   // CHECK:STDERR:
-  ({} as C) as (C as (A & B));
+  C as (A & B);
 
-  // CHECK:STDERR: fail_incomplete.carbon:[[@LINE+7]]:3: error: cannot convert type `C` into type implementing `A` [ConversionFailureTypeToFacet]
+  // CHECK:STDERR: fail_incomplete_constraint.carbon:[[@LINE+10]]:3: error: facet type `A` is incomplete [ImplLookupInIncompleteFacetType]
   // CHECK:STDERR:   G({} as C);
   // CHECK:STDERR:   ^~~~~~~~~~
-  // CHECK:STDERR: fail_incomplete.carbon:[[@LINE-19]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
+  // CHECK:STDERR: fail_incomplete_constraint.carbon:[[@LINE-29]]:1: note: constraint was forward declared here [NamedConstraintForwardDeclaredHere]
+  // CHECK:STDERR: constraint A;
+  // CHECK:STDERR: ^~~~~~~~~~~~~
+  // CHECK:STDERR: fail_incomplete_constraint.carbon:[[@LINE-28]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
   // CHECK:STDERR: fn G[T:! A](t: T) {}
   // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~
   // CHECK:STDERR:
   G({} as C);
 
-  // CHECK:STDERR: fail_incomplete.carbon:[[@LINE+7]]:3: error: cannot convert type `C` into type implementing `A & B` [ConversionFailureTypeToFacet]
+  // CHECK:STDERR: fail_incomplete_constraint.carbon:[[@LINE+10]]:3: error: facet type `B & A` is incomplete [ImplLookupInIncompleteFacetType]
   // CHECK:STDERR:   H({} as C);
   // CHECK:STDERR:   ^~~~~~~~~~
-  // CHECK:STDERR: fail_incomplete.carbon:[[@LINE-27]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
+  // CHECK:STDERR: fail_incomplete_constraint.carbon:[[@LINE-41]]:1: note: constraint was forward declared here [NamedConstraintForwardDeclaredHere]
+  // CHECK:STDERR: constraint A;
+  // CHECK:STDERR: ^~~~~~~~~~~~~
+  // CHECK:STDERR: fail_incomplete_constraint.carbon:[[@LINE-39]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
   // CHECK:STDERR: fn H[T:! A & B](t: T) {}
   // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~
   // CHECK:STDERR:

+ 94 - 0
toolchain/check/testdata/impl/impl_as_named_constraint.carbon

@@ -0,0 +1,94 @@
+// 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-FILE: toolchain/testing/testdata/min_prelude/convert.carbon
+//
+// AUTOUPDATE
+// TIP: To test this file alone, run:
+// TIP:   bazel test //toolchain/testing:file_test --test_arg=--file_tests=toolchain/check/testdata/impl/impl_as_named_constraint.carbon
+// TIP: To dump output, run:
+// TIP:   bazel run //toolchain/testing:file_test -- --dump_output --file_tests=toolchain/check/testdata/impl/impl_as_named_constraint.carbon
+
+// --- fail_incomplete_constraint.carbon
+library "[[@TEST_NAME]]";
+
+constraint A;
+
+class C {}
+
+// CHECK:STDERR: fail_incomplete_constraint.carbon:[[@LINE+7]]:1: error: facet type `A` cannot be identified in `impl as` [ImplOfUnidentifiedFacetType]
+// CHECK:STDERR: impl C as A {}
+// CHECK:STDERR: ^~~~~~~~~~~~~
+// CHECK:STDERR: fail_incomplete_constraint.carbon:[[@LINE-7]]:1: note: constraint was forward declared here [NamedConstraintForwardDeclaredHere]
+// CHECK:STDERR: constraint A;
+// CHECK:STDERR: ^~~~~~~~~~~~~
+// CHECK:STDERR:
+impl C as A {}
+
+// --- fail_empty_constraint.carbon
+library "[[@TEST_NAME]]";
+
+constraint A {}
+
+class C {}
+
+// CHECK:STDERR: fail_empty_constraint.carbon:[[@LINE+4]]:1: error: impl as 0 interfaces, expected 1 [ImplOfNotOneInterface]
+// CHECK:STDERR: impl C as A {}
+// CHECK:STDERR: ^~~~~~~~~~~~~
+// CHECK:STDERR:
+impl C as A {}
+
+// --- fail_too_many_interfaces_in_constraint.carbon
+library "[[@TEST_NAME]]";
+
+interface A1;
+interface A2;
+constraint B {
+  require impls A1;
+  require impls A2;
+}
+
+class C {}
+
+// TODO: This should fail since B does not name a single interface, it names
+// more than one.
+// CHECK:STDERR: fail_too_many_interfaces_in_constraint.carbon:[[@LINE+4]]:1: error: impl as 0 interfaces, expected 1 [ImplOfNotOneInterface]
+// CHECK:STDERR: impl C as B {}
+// CHECK:STDERR: ^~~~~~~~~~~~~
+// CHECK:STDERR:
+impl C as B {}
+
+// --- fail_todo_one_declared_interface_in_constraint.carbon
+library "[[@TEST_NAME]]";
+
+// TODO: This should work since B can be identified to have one interface.
+
+interface A;
+constraint B {
+  require impls A;
+}
+
+class C {}
+// CHECK:STDERR: fail_todo_one_declared_interface_in_constraint.carbon:[[@LINE+4]]:1: error: impl as 0 interfaces, expected 1 [ImplOfNotOneInterface]
+// CHECK:STDERR: impl C as B {}
+// CHECK:STDERR: ^~~~~~~~~~~~~
+// CHECK:STDERR:
+impl C as B {}
+
+// --- fail_todo_one_defined_interface_in_constraint.carbon
+library "[[@TEST_NAME]]";
+
+// TODO: This should work since B can be identified to have one interface.
+
+interface A {}
+constraint B {
+  require impls A;
+}
+
+class C {}
+// CHECK:STDERR: fail_todo_one_defined_interface_in_constraint.carbon:[[@LINE+4]]:1: error: impl as 0 interfaces, expected 1 [ImplOfNotOneInterface]
+// CHECK:STDERR: impl C as B {}
+// CHECK:STDERR: ^~~~~~~~~~~~~
+// CHECK:STDERR:
+impl C as B {}

+ 0 - 67
toolchain/check/testdata/interface/fail_incomplete_type.carbon

@@ -1,67 +0,0 @@
-// 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-FILE: toolchain/testing/testdata/min_prelude/none.carbon
-// TODO: Add ranges and switch to "--dump-sem-ir-ranges=only".
-// EXTRA-ARGS: --dump-sem-ir-ranges=if-present
-//
-// AUTOUPDATE
-// TIP: To test this file alone, run:
-// TIP:   bazel test //toolchain/testing:file_test --test_arg=--file_tests=toolchain/check/testdata/interface/fail_incomplete_type.carbon
-// TIP: To dump output, run:
-// TIP:   bazel run //toolchain/testing:file_test -- --dump_output --file_tests=toolchain/check/testdata/interface/fail_incomplete_type.carbon
-
-class C;
-
-interface I {
-  // CHECK:STDERR: fail_incomplete_type.carbon:[[@LINE+7]]:11: error: associated constant has incomplete type `C` [IncompleteTypeInAssociatedConstantDecl]
-  // CHECK:STDERR:   let T:! C;
-  // CHECK:STDERR:           ^
-  // CHECK:STDERR: fail_incomplete_type.carbon:[[@LINE-6]]:1: note: class was forward declared here [ClassForwardDeclaredHere]
-  // CHECK:STDERR: class C;
-  // CHECK:STDERR: ^~~~~~~~
-  // CHECK:STDERR:
-  let T:! C;
-}
-
-// CHECK:STDOUT: --- fail_incomplete_type.carbon
-// CHECK:STDOUT:
-// CHECK:STDOUT: constants {
-// CHECK:STDOUT:   %C: type = class_type @C [concrete]
-// CHECK:STDOUT:   %I.type: type = facet_type <@I> [concrete]
-// CHECK:STDOUT:   %Self: %I.type = symbolic_binding Self, 0 [symbolic]
-// CHECK:STDOUT:   %I.assoc_type: type = assoc_entity_type @I [concrete]
-// CHECK:STDOUT:   %assoc0: %I.assoc_type = assoc_entity element0, @I.%T [concrete]
-// CHECK:STDOUT: }
-// CHECK:STDOUT:
-// CHECK:STDOUT: file {
-// CHECK:STDOUT:   package: <namespace> = namespace [concrete] {
-// CHECK:STDOUT:     .C = %C.decl
-// CHECK:STDOUT:     .I = %I.decl
-// CHECK:STDOUT:   }
-// CHECK:STDOUT:   %C.decl: type = class_decl @C [concrete = constants.%C] {} {}
-// CHECK:STDOUT:   %I.decl: type = interface_decl @I [concrete = constants.%I.type] {} {}
-// CHECK:STDOUT: }
-// CHECK:STDOUT:
-// CHECK:STDOUT: interface @I {
-// CHECK:STDOUT:   %Self: %I.type = symbolic_binding Self, 0 [symbolic = constants.%Self]
-// CHECK:STDOUT:   %T: <error> = assoc_const_decl @T [concrete] {
-// CHECK:STDOUT:     %assoc0: %I.assoc_type = assoc_entity element0, @I.%T [concrete = constants.%assoc0]
-// CHECK:STDOUT:   }
-// CHECK:STDOUT:
-// CHECK:STDOUT: !members:
-// CHECK:STDOUT:   .Self = %Self
-// CHECK:STDOUT:   .C = <poisoned>
-// CHECK:STDOUT:   .T = @T.%assoc0
-// CHECK:STDOUT:   witness = (%T)
-// CHECK:STDOUT: }
-// CHECK:STDOUT:
-// CHECK:STDOUT: generic assoc_const @T(@I.%Self: %I.type) {
-// CHECK:STDOUT:   assoc_const T:! <error>;
-// CHECK:STDOUT: }
-// CHECK:STDOUT:
-// CHECK:STDOUT: class @C;
-// CHECK:STDOUT:
-// CHECK:STDOUT: specific @T(constants.%Self) {}
-// CHECK:STDOUT:

+ 195 - 0
toolchain/check/testdata/interface/incomplete.carbon

@@ -0,0 +1,195 @@
+// 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-FILE: toolchain/testing/testdata/min_prelude/none.carbon
+// TODO: Add ranges and switch to "--dump-sem-ir-ranges=only".
+// EXTRA-ARGS: --dump-sem-ir-ranges=if-present
+//
+// AUTOUPDATE
+// TIP: To test this file alone, run:
+// TIP:   bazel test //toolchain/testing:file_test --test_arg=--file_tests=toolchain/check/testdata/interface/incomplete.carbon
+// TIP: To dump output, run:
+// TIP:   bazel run //toolchain/testing:file_test -- --dump_output --file_tests=toolchain/check/testdata/interface/incomplete.carbon
+
+// --- fail_incomplete_type.carbon
+library "[[@TEST_NAME]]";
+
+class C;
+
+interface I {
+  // CHECK:STDERR: fail_incomplete_type.carbon:[[@LINE+7]]:11: error: associated constant has incomplete type `C` [IncompleteTypeInAssociatedConstantDecl]
+  // CHECK:STDERR:   let T:! C;
+  // CHECK:STDERR:           ^
+  // CHECK:STDERR: fail_incomplete_type.carbon:[[@LINE-6]]:1: note: class was forward declared here [ClassForwardDeclaredHere]
+  // CHECK:STDERR: class C;
+  // CHECK:STDERR: ^~~~~~~~
+  // CHECK:STDERR:
+  let T:! C;
+}
+
+// --- fail_incomplete_constraint.carbon
+library "[[@TEST_NAME]]";
+
+constraint A;
+
+interface B {
+  // CHECK:STDERR: fail_incomplete_constraint.carbon:[[@LINE+7]]:17: error: facet type `A` cannot be identified in `require` declaration [RequireImplsUnidentifiedFacetType]
+  // CHECK:STDERR:   require impls A;
+  // CHECK:STDERR:                 ^
+  // CHECK:STDERR: fail_incomplete_constraint.carbon:[[@LINE-6]]:1: note: constraint was forward declared here [NamedConstraintForwardDeclaredHere]
+  // CHECK:STDERR: constraint A;
+  // CHECK:STDERR: ^~~~~~~~~~~~~
+  // CHECK:STDERR:
+  require impls A;
+}
+
+// --- incomplete_interface.carbon
+library "[[@TEST_NAME]]";
+
+interface A;
+
+interface B {
+  require impls A;
+}
+
+// --- fail_incomplete_interface_in_where.carbon
+library "[[@TEST_NAME]]";
+
+interface A;
+
+interface B {
+  // CHECK:STDERR: fail_incomplete_interface_in_where.carbon:[[@LINE+7]]:25: error: member access into object of incomplete type `A` [IncompleteTypeInMemberAccess]
+  // CHECK:STDERR:   require impls A where .X = {};
+  // CHECK:STDERR:                         ^~
+  // CHECK:STDERR: fail_incomplete_interface_in_where.carbon:[[@LINE-6]]:1: note: interface was forward declared here [InterfaceForwardDeclaredHere]
+  // CHECK:STDERR: interface A;
+  // CHECK:STDERR: ^~~~~~~~~~~~
+  // CHECK:STDERR:
+  require impls A where .X = {};
+}
+
+// CHECK:STDOUT: --- fail_incomplete_type.carbon
+// CHECK:STDOUT:
+// CHECK:STDOUT: constants {
+// CHECK:STDOUT:   %C: type = class_type @C [concrete]
+// CHECK:STDOUT:   %I.type: type = facet_type <@I> [concrete]
+// CHECK:STDOUT:   %Self: %I.type = symbolic_binding Self, 0 [symbolic]
+// CHECK:STDOUT:   %I.assoc_type: type = assoc_entity_type @I [concrete]
+// CHECK:STDOUT:   %assoc0: %I.assoc_type = assoc_entity element0, @I.%T [concrete]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: file {
+// CHECK:STDOUT:   package: <namespace> = namespace [concrete] {
+// CHECK:STDOUT:     .C = %C.decl
+// CHECK:STDOUT:     .I = %I.decl
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %C.decl: type = class_decl @C [concrete = constants.%C] {} {}
+// CHECK:STDOUT:   %I.decl: type = interface_decl @I [concrete = constants.%I.type] {} {}
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: interface @I {
+// CHECK:STDOUT:   %Self: %I.type = symbolic_binding Self, 0 [symbolic = constants.%Self]
+// CHECK:STDOUT:   %T: <error> = assoc_const_decl @T [concrete] {
+// CHECK:STDOUT:     %assoc0: %I.assoc_type = assoc_entity element0, @I.%T [concrete = constants.%assoc0]
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = %Self
+// CHECK:STDOUT:   .C = <poisoned>
+// CHECK:STDOUT:   .T = @T.%assoc0
+// CHECK:STDOUT:   witness = (%T)
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: generic assoc_const @T(@I.%Self: %I.type) {
+// CHECK:STDOUT:   assoc_const T:! <error>;
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: class @C;
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @T(constants.%Self) {}
+// CHECK:STDOUT:
+// CHECK:STDOUT: --- fail_incomplete_constraint.carbon
+// CHECK:STDOUT:
+// CHECK:STDOUT: constants {
+// CHECK:STDOUT:   %A.type: type = facet_type <@A> [concrete]
+// CHECK:STDOUT:   %B.type: type = facet_type <@B> [concrete]
+// CHECK:STDOUT:   %Self: %B.type = symbolic_binding Self, 0 [symbolic]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: file {
+// CHECK:STDOUT:   package: <namespace> = namespace [concrete] {
+// CHECK:STDOUT:     .A = %A.decl
+// CHECK:STDOUT:     .B = %B.decl
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %A.decl: type = constraint_decl @A [concrete = constants.%A.type] {} {}
+// CHECK:STDOUT:   %B.decl: type = interface_decl @B [concrete = constants.%B.type] {} {}
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: interface @B {
+// CHECK:STDOUT:   %Self: %B.type = symbolic_binding Self, 0 [symbolic = constants.%Self]
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = %Self
+// CHECK:STDOUT:   .A = <poisoned>
+// CHECK:STDOUT:   witness = ()
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: constraint @A;
+// CHECK:STDOUT:
+// CHECK:STDOUT: --- incomplete_interface.carbon
+// CHECK:STDOUT:
+// CHECK:STDOUT: constants {
+// CHECK:STDOUT:   %A.type: type = facet_type <@A> [concrete]
+// CHECK:STDOUT:   %B.type: type = facet_type <@B> [concrete]
+// CHECK:STDOUT:   %Self: %B.type = symbolic_binding Self, 0 [symbolic]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: file {
+// CHECK:STDOUT:   package: <namespace> = namespace [concrete] {
+// CHECK:STDOUT:     .A = %A.decl
+// CHECK:STDOUT:     .B = %B.decl
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %A.decl: type = interface_decl @A [concrete = constants.%A.type] {} {}
+// CHECK:STDOUT:   %B.decl: type = interface_decl @B [concrete = constants.%B.type] {} {}
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: interface @A;
+// CHECK:STDOUT:
+// CHECK:STDOUT: interface @B {
+// CHECK:STDOUT:   %Self: %B.type = symbolic_binding Self, 0 [symbolic = constants.%Self]
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = %Self
+// CHECK:STDOUT:   .A = <poisoned>
+// CHECK:STDOUT:   witness = ()
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: --- fail_incomplete_interface_in_where.carbon
+// CHECK:STDOUT:
+// CHECK:STDOUT: constants {
+// CHECK:STDOUT:   %A.type: type = facet_type <@A> [concrete]
+// CHECK:STDOUT:   %B.type: type = facet_type <@B> [concrete]
+// CHECK:STDOUT:   %Self: %B.type = symbolic_binding Self, 0 [symbolic]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: file {
+// CHECK:STDOUT:   package: <namespace> = namespace [concrete] {
+// CHECK:STDOUT:     .A = %A.decl
+// CHECK:STDOUT:     .B = %B.decl
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %A.decl: type = interface_decl @A [concrete = constants.%A.type] {} {}
+// CHECK:STDOUT:   %B.decl: type = interface_decl @B [concrete = constants.%B.type] {} {}
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: interface @A;
+// CHECK:STDOUT:
+// CHECK:STDOUT: interface @B {
+// CHECK:STDOUT:   %Self: %B.type = symbolic_binding Self, 0 [symbolic = constants.%Self]
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = %Self
+// CHECK:STDOUT:   .A = <poisoned>
+// CHECK:STDOUT:   witness = ()
+// CHECK:STDOUT: }
+// CHECK:STDOUT:

+ 9 - 9
toolchain/check/testdata/named_constraint/basic.carbon

@@ -55,19 +55,19 @@ constraint Declared {}
 // CHECK:STDOUT: --- definition.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
-// CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
-// CHECK:STDOUT:   %Self: %type = symbolic_binding Self, 0 [symbolic]
+// CHECK:STDOUT:   %Declared.type: type = facet_type <@Declared> [concrete]
+// CHECK:STDOUT:   %Self: %Declared.type = symbolic_binding Self, 0 [symbolic]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
 // CHECK:STDOUT:   package: <namespace> = namespace [concrete] {
 // CHECK:STDOUT:     .Declared = %Declared.decl
 // CHECK:STDOUT:   }
-// CHECK:STDOUT:   %Declared.decl: type = constraint_decl @Declared [concrete = constants.%type] {} {}
+// CHECK:STDOUT:   %Declared.decl: type = constraint_decl @Declared [concrete = constants.%Declared.type] {} {}
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: constraint @Declared {
-// CHECK:STDOUT:   %Self: %type = symbolic_binding Self, 0 [symbolic = constants.%Self]
+// CHECK:STDOUT:   %Self: %Declared.type = symbolic_binding Self, 0 [symbolic = constants.%Self]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !members:
 // CHECK:STDOUT:   .Self = %Self
@@ -76,20 +76,20 @@ constraint Declared {}
 // CHECK:STDOUT: --- forward_declaration.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
-// CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
-// CHECK:STDOUT:   %Self: %type = symbolic_binding Self, 0 [symbolic]
+// CHECK:STDOUT:   %ForwardDeclared.type: type = facet_type <@ForwardDeclared> [concrete]
+// CHECK:STDOUT:   %Self: %ForwardDeclared.type = symbolic_binding Self, 0 [symbolic]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
 // CHECK:STDOUT:   package: <namespace> = namespace [concrete] {
 // CHECK:STDOUT:     .ForwardDeclared = %ForwardDeclared.decl.loc4
 // CHECK:STDOUT:   }
-// CHECK:STDOUT:   %ForwardDeclared.decl.loc4: type = constraint_decl @ForwardDeclared [concrete = constants.%type] {} {}
-// CHECK:STDOUT:   %ForwardDeclared.decl.loc6: type = constraint_decl @ForwardDeclared [concrete = constants.%type] {} {}
+// CHECK:STDOUT:   %ForwardDeclared.decl.loc4: type = constraint_decl @ForwardDeclared [concrete = constants.%ForwardDeclared.type] {} {}
+// CHECK:STDOUT:   %ForwardDeclared.decl.loc6: type = constraint_decl @ForwardDeclared [concrete = constants.%ForwardDeclared.type] {} {}
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: constraint @ForwardDeclared {
-// CHECK:STDOUT:   %Self: %type = symbolic_binding Self, 0 [symbolic = constants.%Self]
+// CHECK:STDOUT:   %Self: %ForwardDeclared.type = symbolic_binding Self, 0 [symbolic = constants.%Self]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !members:
 // CHECK:STDOUT:   .Self = %Self

+ 37 - 29
toolchain/check/testdata/named_constraint/convert.carbon

@@ -62,9 +62,9 @@ fn G(T:! Z) {
 // CHECK:STDOUT: --- type_and_with_named_constraint_self.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
-// CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
-// CHECK:STDOUT:   %T: %type = symbolic_binding T, 0 [symbolic]
-// CHECK:STDOUT:   %pattern_type.e25: type = pattern_type %type [concrete]
+// CHECK:STDOUT:   %E.type: type = facet_type <@E> [concrete]
+// CHECK:STDOUT:   %T: %E.type = symbolic_binding T, 0 [symbolic]
+// CHECK:STDOUT:   %pattern_type.e25: type = pattern_type %E.type [concrete]
 // CHECK:STDOUT:   %F.type: type = fn_type @F [concrete]
 // CHECK:STDOUT:   %empty_tuple.type: type = tuple_type () [concrete]
 // CHECK:STDOUT:   %F: %F.type = struct_value () [concrete]
@@ -75,7 +75,7 @@ fn G(T:! Z) {
 // CHECK:STDOUT:   %.fa7: type = fn_type_with_self_type %BitAndWith.Op.type.9a3, %BitAndWith.facet [concrete]
 // CHECK:STDOUT:   %type.as.BitAndWith.impl.Op.type: type = fn_type @type.as.BitAndWith.impl.Op [concrete]
 // CHECK:STDOUT:   %type.as.BitAndWith.impl.Op: %type.as.BitAndWith.impl.Op.type = struct_value () [concrete]
-// CHECK:STDOUT:   %type.as.BitAndWith.impl.Op.bound: <bound method> = bound_method %type, %type.as.BitAndWith.impl.Op [concrete]
+// CHECK:STDOUT:   %type.as.BitAndWith.impl.Op.bound: <bound method> = bound_method %E.type, %type.as.BitAndWith.impl.Op [concrete]
 // CHECK:STDOUT:   %G.type: type = fn_type @G [concrete]
 // CHECK:STDOUT:   %G: %G.type = struct_value () [concrete]
 // CHECK:STDOUT:   %F.specific_fn: <specific function> = specific_function %F, @F(%T) [symbolic]
@@ -90,22 +90,22 @@ fn G(T:! Z) {
 // CHECK:STDOUT:   %G.decl: %G.type = fn_decl @G [concrete = constants.%G] {
 // CHECK:STDOUT:     %T.patt: %pattern_type.e25 = symbolic_binding_pattern T, 0 [concrete]
 // CHECK:STDOUT:   } {
-// CHECK:STDOUT:     %.loc8_12.1: type = splice_block %.loc8_12.3 [concrete = constants.%type] {
+// CHECK:STDOUT:     %.loc8_12.1: type = splice_block %.loc8_12.3 [concrete = constants.%E.type] {
 // CHECK:STDOUT:       <elided>
-// CHECK:STDOUT:       %E.ref.loc8_10: type = name_ref E, file.%E.decl [concrete = constants.%type]
-// CHECK:STDOUT:       %E.ref.loc8_14: type = name_ref E, file.%E.decl [concrete = constants.%type]
+// CHECK:STDOUT:       %E.ref.loc8_10: type = name_ref E, file.%E.decl [concrete = constants.%E.type]
+// CHECK:STDOUT:       %E.ref.loc8_14: type = name_ref E, file.%E.decl [concrete = constants.%E.type]
 // CHECK:STDOUT:       %impl.elem0: %.fa7 = impl_witness_access constants.%BitAndWith.impl_witness, element0 [concrete = constants.%type.as.BitAndWith.impl.Op]
 // CHECK:STDOUT:       %bound_method: <bound method> = bound_method %E.ref.loc8_10, %impl.elem0 [concrete = constants.%type.as.BitAndWith.impl.Op.bound]
-// CHECK:STDOUT:       %type.as.BitAndWith.impl.Op.call: init type = call %bound_method(%E.ref.loc8_10, %E.ref.loc8_14) [concrete = constants.%type]
-// CHECK:STDOUT:       %.loc8_12.2: type = value_of_initializer %type.as.BitAndWith.impl.Op.call [concrete = constants.%type]
-// CHECK:STDOUT:       %.loc8_12.3: type = converted %type.as.BitAndWith.impl.Op.call, %.loc8_12.2 [concrete = constants.%type]
+// CHECK:STDOUT:       %type.as.BitAndWith.impl.Op.call: init type = call %bound_method(%E.ref.loc8_10, %E.ref.loc8_14) [concrete = constants.%E.type]
+// CHECK:STDOUT:       %.loc8_12.2: type = value_of_initializer %type.as.BitAndWith.impl.Op.call [concrete = constants.%E.type]
+// CHECK:STDOUT:       %.loc8_12.3: type = converted %type.as.BitAndWith.impl.Op.call, %.loc8_12.2 [concrete = constants.%E.type]
 // CHECK:STDOUT:     }
-// CHECK:STDOUT:     %T.loc8_6.2: %type = symbolic_binding T, 0 [symbolic = %T.loc8_6.1 (constants.%T)]
+// CHECK:STDOUT:     %T.loc8_6.2: %E.type = symbolic_binding T, 0 [symbolic = %T.loc8_6.1 (constants.%T)]
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: generic fn @G(%T.loc8_6.2: %type) {
-// CHECK:STDOUT:   %T.loc8_6.1: %type = symbolic_binding T, 0 [symbolic = %T.loc8_6.1 (constants.%T)]
+// CHECK:STDOUT: generic fn @G(%T.loc8_6.2: %E.type) {
+// CHECK:STDOUT:   %T.loc8_6.1: %E.type = symbolic_binding T, 0 [symbolic = %T.loc8_6.1 (constants.%T)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT:   %F.specific_fn.loc9_3.2: <specific function> = specific_function constants.%F, @F(%T.loc8_6.1) [symbolic = %F.specific_fn.loc9_3.2 (constants.%F.specific_fn)]
@@ -113,7 +113,7 @@ fn G(T:! Z) {
 // 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: %type = name_ref T, %T.loc8_6.2 [symbolic = %T.loc8_6.1 (constants.%T)]
+// CHECK:STDOUT:     %T.ref: %E.type = name_ref T, %T.loc8_6.2 [symbolic = %T.loc8_6.1 (constants.%T)]
 // CHECK:STDOUT:     %F.specific_fn.loc9_3.1: <specific function> = specific_function %F.ref, @F(constants.%T) [symbolic = %F.specific_fn.loc9_3.2 (constants.%F.specific_fn)]
 // CHECK:STDOUT:     %F.call: init %empty_tuple.type = call %F.specific_fn.loc9_3.1()
 // CHECK:STDOUT:     return
@@ -127,15 +127,18 @@ fn G(T:! Z) {
 // CHECK:STDOUT: --- compatible_constraints.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
-// CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
-// CHECK:STDOUT:   %T: %type = symbolic_binding T, 0 [symbolic]
-// CHECK:STDOUT:   %pattern_type: type = pattern_type %type [concrete]
+// CHECK:STDOUT:   %E1.type: type = facet_type <@E1> [concrete]
+// CHECK:STDOUT:   %E2.type: type = facet_type <@E2> [concrete]
 // CHECK:STDOUT:   %F.type: type = fn_type @F [concrete]
 // CHECK:STDOUT:   %empty_tuple.type: type = tuple_type () [concrete]
 // CHECK:STDOUT:   %F: %F.type = struct_value () [concrete]
+// CHECK:STDOUT:   %T.8619ef.2: %E2.type = symbolic_binding T, 0 [symbolic]
+// CHECK:STDOUT:   %pattern_type.e25e9f.2: type = pattern_type %E2.type [concrete]
 // CHECK:STDOUT:   %G.type: type = fn_type @G [concrete]
 // CHECK:STDOUT:   %G: %G.type = struct_value () [concrete]
-// CHECK:STDOUT:   %F.specific_fn: <specific function> = specific_function %F, @F(%T) [symbolic]
+// 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: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: imports {
@@ -143,33 +146,38 @@ fn G(T:! Z) {
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
 // CHECK:STDOUT:   %G.decl: %G.type = fn_decl @G [concrete = constants.%G] {
-// CHECK:STDOUT:     %T.patt: %pattern_type = symbolic_binding_pattern T, 0 [concrete]
+// CHECK:STDOUT:     %T.patt: %pattern_type.e25e9f.2 = symbolic_binding_pattern T, 0 [concrete]
 // CHECK:STDOUT:   } {
-// CHECK:STDOUT:     %.loc9: type = splice_block %E2.ref [concrete = constants.%type] {
+// CHECK:STDOUT:     %.loc9: type = splice_block %E2.ref [concrete = constants.%E2.type] {
 // CHECK:STDOUT:       <elided>
-// CHECK:STDOUT:       %E2.ref: type = name_ref E2, file.%E2.decl [concrete = constants.%type]
+// CHECK:STDOUT:       %E2.ref: type = name_ref E2, file.%E2.decl [concrete = constants.%E2.type]
 // CHECK:STDOUT:     }
-// CHECK:STDOUT:     %T.loc9_6.2: %type = symbolic_binding T, 0 [symbolic = %T.loc9_6.1 (constants.%T)]
+// CHECK:STDOUT:     %T.loc9_6.2: %E2.type = symbolic_binding T, 0 [symbolic = %T.loc9_6.1 (constants.%T.8619ef.2)]
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: generic fn @G(%T.loc9_6.2: %type) {
-// CHECK:STDOUT:   %T.loc9_6.1: %type = symbolic_binding T, 0 [symbolic = %T.loc9_6.1 (constants.%T)]
+// CHECK:STDOUT: generic fn @G(%T.loc9_6.2: %E2.type) {
+// CHECK:STDOUT:   %T.loc9_6.1: %E2.type = symbolic_binding T, 0 [symbolic = %T.loc9_6.1 (constants.%T.8619ef.2)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
-// CHECK:STDOUT:   %F.specific_fn.loc10_3.2: <specific function> = specific_function constants.%F, @F(%T.loc9_6.1) [symbolic = %F.specific_fn.loc10_3.2 (constants.%F.specific_fn)]
+// 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:
 // 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: %type = name_ref T, %T.loc9_6.2 [symbolic = %T.loc9_6.1 (constants.%T)]
-// CHECK:STDOUT:     %F.specific_fn.loc10_3.1: <specific function> = specific_function %F.ref, @F(constants.%T) [symbolic = %F.specific_fn.loc10_3.2 (constants.%F.specific_fn)]
+// 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:     %F.call: init %empty_tuple.type = call %F.specific_fn.loc10_3.1()
 // CHECK:STDOUT:     return
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @G(constants.%T) {
-// CHECK:STDOUT:   %T.loc9_6.1 => constants.%T
+// CHECK:STDOUT: specific @G(constants.%T.8619ef.2) {
+// CHECK:STDOUT:   %T.loc9_6.1 => constants.%T.8619ef.2
 // CHECK:STDOUT: }
 // CHECK:STDOUT:

+ 29 - 29
toolchain/check/testdata/named_constraint/empty.carbon

@@ -34,9 +34,9 @@ fn G(T:! Z, U:! type, V:! Empty) {
 // CHECK:STDOUT: --- empty.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
-// CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
-// CHECK:STDOUT:   %T.861: %type = symbolic_binding T, 0 [symbolic]
-// CHECK:STDOUT:   %pattern_type.e25: type = pattern_type %type [concrete]
+// CHECK:STDOUT:   %Empty.type: type = facet_type <@Empty> [concrete]
+// CHECK:STDOUT:   %T.861: %Empty.type = symbolic_binding T, 0 [symbolic]
+// CHECK:STDOUT:   %pattern_type.e25: type = pattern_type %Empty.type [concrete]
 // CHECK:STDOUT:   %F.type: type = fn_type @F [concrete]
 // CHECK:STDOUT:   %empty_tuple.type: type = tuple_type () [concrete]
 // CHECK:STDOUT:   %F: %F.type = struct_value () [concrete]
@@ -45,18 +45,18 @@ fn G(T:! Z, U:! type, V:! Empty) {
 // CHECK:STDOUT:   %pattern_type.4a0: type = pattern_type %Z.type [concrete]
 // CHECK:STDOUT:   %U: type = symbolic_binding U, 1 [symbolic]
 // CHECK:STDOUT:   %pattern_type.98f: type = pattern_type type [concrete]
-// CHECK:STDOUT:   %V: %type = symbolic_binding V, 2 [symbolic]
+// CHECK:STDOUT:   %V: %Empty.type = symbolic_binding V, 2 [symbolic]
 // CHECK:STDOUT:   %G.type: type = fn_type @G [concrete]
 // CHECK:STDOUT:   %G: %G.type = struct_value () [concrete]
 // CHECK:STDOUT:   %empty_struct_type: type = struct_type {} [concrete]
-// CHECK:STDOUT:   %facet_value.6fa: %type = facet_value %empty_struct_type, () [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: %type = facet_value type, () [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:   %T.binding.as_type: type = symbolic_binding_type T, 0, %T.3b3 [symbolic]
-// CHECK:STDOUT:   %facet_value.146: %type = facet_value %T.binding.as_type, () [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: %type = facet_value %U, () [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:   %F.specific_fn.f38: <specific function> = specific_function %F, @F(%V) [symbolic]
 // CHECK:STDOUT: }
@@ -65,11 +65,11 @@ fn G(T:! Z, U:! type, V:! Empty) {
 // CHECK:STDOUT:   %F.decl: %F.type = fn_decl @F [concrete = constants.%F] {
 // CHECK:STDOUT:     %T.patt: %pattern_type.e25 = symbolic_binding_pattern T, 0 [concrete]
 // CHECK:STDOUT:   } {
-// CHECK:STDOUT:     %.loc19: type = splice_block %Empty.ref [concrete = constants.%type] {
+// CHECK:STDOUT:     %.loc19: type = splice_block %Empty.ref [concrete = constants.%Empty.type] {
 // CHECK:STDOUT:       <elided>
-// CHECK:STDOUT:       %Empty.ref: type = name_ref Empty, file.%Empty.decl [concrete = constants.%type]
+// CHECK:STDOUT:       %Empty.ref: type = name_ref Empty, file.%Empty.decl [concrete = constants.%Empty.type]
 // CHECK:STDOUT:     }
-// CHECK:STDOUT:     %T.loc19_6.2: %type = symbolic_binding T, 0 [symbolic = %T.loc19_6.1 (constants.%T.861)]
+// CHECK:STDOUT:     %T.loc19_6.2: %Empty.type = symbolic_binding T, 0 [symbolic = %T.loc19_6.1 (constants.%T.861)]
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %G.decl: %G.type = fn_decl @G [concrete = constants.%G] {
 // CHECK:STDOUT:     %T.patt: %pattern_type.4a0 = symbolic_binding_pattern T, 0 [concrete]
@@ -83,16 +83,16 @@ fn G(T:! Z, U:! type, V:! Empty) {
 // CHECK:STDOUT:     %T.loc25_6.2: %Z.type = symbolic_binding T, 0 [symbolic = %T.loc25_6.1 (constants.%T.3b3)]
 // CHECK:STDOUT:     <elided>
 // CHECK:STDOUT:     %U.loc25_13.2: type = symbolic_binding U, 1 [symbolic = %U.loc25_13.1 (constants.%U)]
-// CHECK:STDOUT:     %.loc25_27: type = splice_block %Empty.ref [concrete = constants.%type] {
+// CHECK:STDOUT:     %.loc25_27: type = splice_block %Empty.ref [concrete = constants.%Empty.type] {
 // CHECK:STDOUT:       <elided>
-// CHECK:STDOUT:       %Empty.ref: type = name_ref Empty, file.%Empty.decl [concrete = constants.%type]
+// CHECK:STDOUT:       %Empty.ref: type = name_ref Empty, file.%Empty.decl [concrete = constants.%Empty.type]
 // CHECK:STDOUT:     }
-// CHECK:STDOUT:     %V.loc25_23.2: %type = symbolic_binding V, 2 [symbolic = %V.loc25_23.1 (constants.%V)]
+// CHECK:STDOUT:     %V.loc25_23.2: %Empty.type = symbolic_binding V, 2 [symbolic = %V.loc25_23.1 (constants.%V)]
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: generic fn @F(%T.loc19_6.2: %type) {
-// CHECK:STDOUT:   %T.loc19_6.1: %type = symbolic_binding T, 0 [symbolic = %T.loc19_6.1 (constants.%T.861)]
+// CHECK:STDOUT: generic fn @F(%T.loc19_6.2: %Empty.type) {
+// CHECK:STDOUT:   %T.loc19_6.1: %Empty.type = symbolic_binding T, 0 [symbolic = %T.loc19_6.1 (constants.%T.861)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT:
@@ -102,16 +102,16 @@ fn G(T:! Z, U:! type, V:! Empty) {
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: generic fn @G(%T.loc25_6.2: %Z.type, %U.loc25_13.2: type, %V.loc25_23.2: %type) {
+// CHECK:STDOUT: generic fn @G(%T.loc25_6.2: %Z.type, %U.loc25_13.2: type, %V.loc25_23.2: %Empty.type) {
 // CHECK:STDOUT:   %T.loc25_6.1: %Z.type = symbolic_binding T, 0 [symbolic = %T.loc25_6.1 (constants.%T.3b3)]
 // CHECK:STDOUT:   %U.loc25_13.1: type = symbolic_binding U, 1 [symbolic = %U.loc25_13.1 (constants.%U)]
-// CHECK:STDOUT:   %V.loc25_23.1: %type = symbolic_binding V, 2 [symbolic = %V.loc25_23.1 (constants.%V)]
+// CHECK:STDOUT:   %V.loc25_23.1: %Empty.type = symbolic_binding V, 2 [symbolic = %V.loc25_23.1 (constants.%V)]
 // 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: %type = facet_value %T.binding.as_type, () [symbolic = %facet_value.loc28_6.2 (constants.%facet_value.146)]
+// 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: %type = facet_value %U.loc25_13.1, () [symbolic = %facet_value.loc29_6.2 (constants.%facet_value.a70)]
+// 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:   %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:
@@ -119,30 +119,30 @@ fn G(T:! Z, U:! type, V:! Empty) {
 // 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 ()
-// CHECK:STDOUT:     %facet_value.loc26: %type = facet_value constants.%empty_struct_type, () [concrete = constants.%facet_value.6fa]
-// CHECK:STDOUT:     %.loc26_7: %type = converted %.loc26_6, %facet_value.loc26 [concrete = constants.%facet_value.6fa]
+// 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:     %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: %type = facet_value type, () [concrete = constants.%facet_value.832]
-// CHECK:STDOUT:     %.loc27: %type = converted type, %facet_value.loc27 [concrete = constants.%facet_value.832]
+// 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:     %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: %type = facet_value %T.as_type, () [symbolic = %facet_value.loc28_6.2 (constants.%facet_value.146)]
-// CHECK:STDOUT:     %.loc28: %type = converted %T.ref, %facet_value.loc28_6.1 [symbolic = %facet_value.loc28_6.2 (constants.%facet_value.146)]
+// 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:     %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: %type = facet_value %U.ref, () [symbolic = %facet_value.loc29_6.2 (constants.%facet_value.a70)]
-// CHECK:STDOUT:     %.loc29: %type = converted %U.ref, %facet_value.loc29_6.1 [symbolic = %facet_value.loc29_6.2 (constants.%facet_value.a70)]
+// 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:     %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: %type = name_ref V, %V.loc25_23.2 [symbolic = %V.loc25_23.1 (constants.%V)]
+// CHECK:STDOUT:     %V.ref: %Empty.type = name_ref V, %V.loc25_23.2 [symbolic = %V.loc25_23.1 (constants.%V)]
 // CHECK:STDOUT:     %F.specific_fn.loc30_3.1: <specific function> = specific_function %F.ref.loc30, @F(constants.%V) [symbolic = %F.specific_fn.loc30_3.2 (constants.%F.specific_fn.f38)]
 // CHECK:STDOUT:     %F.call.loc30: init %empty_tuple.type = call %F.specific_fn.loc30_3.1()
 // CHECK:STDOUT:     return

+ 105 - 80
toolchain/check/testdata/named_constraint/empty_generic.carbon

@@ -15,16 +15,15 @@ interface Z {}
 //@dump-sem-ir-begin
 constraint Empty(T:! type) {}
 
-fn F(U:! type, T:! Empty(U)) {}
+fn F(T:! type, U:! Empty(T)) {}
 
-fn G(T:! Z, U:! type, V:! Empty(T)) {
-  F(T, {});
+fn G(T:! Z, U:! Empty(T), V:! type) {
+  F(T, {} as type);
   F(T, type);
   F(T, T);
   F(T, U);
   F(T, V);
 }
-
 //@dump-sem-ir-end
 
 // CHECK:STDOUT: --- empty_generic.carbon
@@ -34,20 +33,23 @@ fn G(T:! Z, U:! type, V:! Empty(T)) {
 // CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
 // CHECK:STDOUT:   %T.d9f: type = symbolic_binding T, 0 [symbolic]
 // CHECK:STDOUT:   %pattern_type.98f: type = pattern_type type [concrete]
-// CHECK:STDOUT:   %Empty.type: type = generic_named_constaint_type @Empty [concrete]
+// CHECK:STDOUT:   %Empty.type.a8a: type = generic_named_constaint_type @Empty [concrete]
 // CHECK:STDOUT:   %empty_tuple.type: type = tuple_type () [concrete]
-// CHECK:STDOUT:   %empty_struct: %Empty.type = struct_value () [concrete]
-// CHECK:STDOUT:   %Self.aa1: %type = symbolic_binding Self, 1 [symbolic]
-// CHECK:STDOUT:   %U.d9f: type = symbolic_binding U, 0 [symbolic]
-// CHECK:STDOUT:   %T.aa1: %type = symbolic_binding T, 1 [symbolic]
-// CHECK:STDOUT:   %pattern_type.e25: type = pattern_type %type [concrete]
+// CHECK:STDOUT:   %empty_struct: %Empty.type.a8a = struct_value () [concrete]
+// CHECK:STDOUT:   %Empty.type.b8d23b.1: type = facet_type <@Empty, @Empty(%T.d9f)> [symbolic]
+// CHECK:STDOUT:   %Self.aa1: %Empty.type.b8d23b.1 = symbolic_binding Self, 1 [symbolic]
+// CHECK:STDOUT:   %U.aa1546.1: %Empty.type.b8d23b.1 = symbolic_binding U, 1 [symbolic]
+// CHECK:STDOUT:   %pattern_type.e25e9f.1: type = pattern_type %Empty.type.b8d23b.1 [symbolic]
+// CHECK:STDOUT:   %pattern_type.e25e9f.2: type = pattern_type %type [concrete]
 // CHECK:STDOUT:   %F.type: type = fn_type @F [concrete]
 // CHECK:STDOUT:   %F: %F.type = struct_value () [concrete]
 // CHECK:STDOUT:   %T.3b3: %Z.type = symbolic_binding T, 0 [symbolic]
 // CHECK:STDOUT:   %pattern_type.4a0: type = pattern_type %Z.type [concrete]
-// CHECK:STDOUT:   %U.b88: type = symbolic_binding U, 1 [symbolic]
 // CHECK:STDOUT:   %T.binding.as_type: type = symbolic_binding_type T, 0, %T.3b3 [symbolic]
-// CHECK:STDOUT:   %V: %type = symbolic_binding V, 2 [symbolic]
+// CHECK:STDOUT:   %Empty.type.b8d23b.2: type = facet_type <@Empty, @Empty(%T.binding.as_type)> [symbolic]
+// CHECK:STDOUT:   %U.aa1546.2: %Empty.type.b8d23b.2 = symbolic_binding U, 1 [symbolic]
+// CHECK:STDOUT:   %pattern_type.e25e9f.3: type = pattern_type %Empty.type.b8d23b.2 [symbolic]
+// CHECK:STDOUT:   %V: type = symbolic_binding V, 2 [symbolic]
 // CHECK:STDOUT:   %G.type: type = fn_type @G [concrete]
 // CHECK:STDOUT:   %G: %G.type = struct_value () [concrete]
 // CHECK:STDOUT:   %empty_struct_type: type = struct_type {} [concrete]
@@ -57,53 +59,55 @@ fn G(T:! Z, U:! type, V:! Empty(T)) {
 // 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: %type = 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:   %facet_value.a70: %type = facet_value %U.b88, () [symbolic]
-// CHECK:STDOUT:   %F.specific_fn.794: <specific function> = specific_function %F, @F(%T.binding.as_type, %facet_value.a70) [symbolic]
-// CHECK:STDOUT:   %F.specific_fn.e3f: <specific function> = specific_function %F, @F(%T.binding.as_type, %V) [symbolic]
+// CHECK:STDOUT:   %U.binding.as_type: type = symbolic_binding_type U, 1, %U.aa1546.2 [symbolic]
+// CHECK:STDOUT:   %facet_value.356: %type = facet_value %U.binding.as_type, () [symbolic]
+// CHECK:STDOUT:   %F.specific_fn.df4: <specific function> = specific_function %F, @F(%T.binding.as_type, %facet_value.356) [symbolic]
+// CHECK:STDOUT:   %facet_value.920: %type = 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: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
-// CHECK:STDOUT:   %Empty.decl: %Empty.type = constraint_decl @Empty [concrete = constants.%empty_struct] {
+// CHECK:STDOUT:   %Empty.decl: %Empty.type.a8a = constraint_decl @Empty [concrete = constants.%empty_struct] {
 // CHECK:STDOUT:     %T.patt: %pattern_type.98f = symbolic_binding_pattern T, 0 [concrete]
 // CHECK:STDOUT:   } {
 // CHECK:STDOUT:     <elided>
 // CHECK:STDOUT:     %T.loc16_18.2: type = symbolic_binding T, 0 [symbolic = %T.loc16_18.1 (constants.%T.d9f)]
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %F.decl: %F.type = fn_decl @F [concrete = constants.%F] {
-// CHECK:STDOUT:     %U.patt: %pattern_type.98f = symbolic_binding_pattern U, 0 [concrete]
-// CHECK:STDOUT:     %T.patt: %pattern_type.e25 = symbolic_binding_pattern T, 1 [concrete]
+// CHECK:STDOUT:     %T.patt: %pattern_type.98f = symbolic_binding_pattern T, 0 [concrete]
+// CHECK:STDOUT:     %U.patt: @F.%pattern_type (%pattern_type.e25e9f.1) = symbolic_binding_pattern U, 1 [concrete]
 // CHECK:STDOUT:   } {
 // CHECK:STDOUT:     <elided>
-// CHECK:STDOUT:     %U.loc18_6.2: type = symbolic_binding U, 0 [symbolic = %U.loc18_6.1 (constants.%U.d9f)]
-// CHECK:STDOUT:     %.loc18: type = splice_block %type [concrete = constants.%type] {
+// CHECK:STDOUT:     %T.loc18_6.2: type = symbolic_binding T, 0 [symbolic = %T.loc18_6.1 (constants.%T.d9f)]
+// CHECK:STDOUT:     %.loc18: type = splice_block %Empty.type [symbolic = %type (constants.%Empty.type.b8d23b.1)] {
 // CHECK:STDOUT:       <elided>
-// CHECK:STDOUT:       %Empty.ref: %Empty.type = name_ref Empty, file.%Empty.decl [concrete = constants.%empty_struct]
-// CHECK:STDOUT:       %U.ref: type = name_ref U, %U.loc18_6.2 [symbolic = %U.loc18_6.1 (constants.%U.d9f)]
-// CHECK:STDOUT:       %type: type = facet_type <type> [concrete = constants.%type]
+// CHECK:STDOUT:       %Empty.ref: %Empty.type.a8a = name_ref Empty, file.%Empty.decl [concrete = constants.%empty_struct]
+// CHECK:STDOUT:       %T.ref: type = name_ref T, %T.loc18_6.2 [symbolic = %T.loc18_6.1 (constants.%T.d9f)]
+// CHECK:STDOUT:       %Empty.type: type = facet_type <@Empty, @Empty(constants.%T.d9f)> [symbolic = %type (constants.%Empty.type.b8d23b.1)]
 // CHECK:STDOUT:     }
-// CHECK:STDOUT:     %T.loc18_16.2: %type = symbolic_binding T, 1 [symbolic = %T.loc18_16.1 (constants.%T.aa1)]
+// CHECK:STDOUT:     %U.loc18_16.2: @F.%type (%Empty.type.b8d23b.1) = symbolic_binding U, 1 [symbolic = %U.loc18_16.1 (constants.%U.aa1546.1)]
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %G.decl: %G.type = fn_decl @G [concrete = constants.%G] {
 // CHECK:STDOUT:     %T.patt: %pattern_type.4a0 = symbolic_binding_pattern T, 0 [concrete]
-// CHECK:STDOUT:     %U.patt: %pattern_type.98f = symbolic_binding_pattern U, 1 [concrete]
-// CHECK:STDOUT:     %V.patt: %pattern_type.e25 = symbolic_binding_pattern V, 2 [concrete]
+// CHECK:STDOUT:     %U.patt: @G.%pattern_type (%pattern_type.e25e9f.3) = symbolic_binding_pattern U, 1 [concrete]
+// CHECK:STDOUT:     %V.patt: %pattern_type.98f = symbolic_binding_pattern V, 2 [concrete]
 // CHECK:STDOUT:   } {
 // CHECK:STDOUT:     %.loc20_10: type = splice_block %Z.ref [concrete = constants.%Z.type] {
 // CHECK:STDOUT:       <elided>
 // CHECK:STDOUT:       %Z.ref: type = name_ref Z, file.%Z.decl [concrete = constants.%Z.type]
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %T.loc20_6.2: %Z.type = symbolic_binding T, 0 [symbolic = %T.loc20_6.1 (constants.%T.3b3)]
-// CHECK:STDOUT:     <elided>
-// CHECK:STDOUT:     %U.loc20_13.2: type = symbolic_binding U, 1 [symbolic = %U.loc20_13.1 (constants.%U.b88)]
-// CHECK:STDOUT:     %.loc20_34.1: type = splice_block %type [concrete = constants.%type] {
+// CHECK:STDOUT:     %.loc20_24.1: type = splice_block %Empty.type [symbolic = %type (constants.%Empty.type.b8d23b.2)] {
 // CHECK:STDOUT:       <elided>
-// CHECK:STDOUT:       %Empty.ref: %Empty.type = name_ref Empty, file.%Empty.decl [concrete = constants.%empty_struct]
+// CHECK:STDOUT:       %Empty.ref: %Empty.type.a8a = name_ref Empty, file.%Empty.decl [concrete = constants.%empty_struct]
 // CHECK:STDOUT:       %T.ref.loc20: %Z.type = name_ref T, %T.loc20_6.2 [symbolic = %T.loc20_6.1 (constants.%T.3b3)]
 // CHECK:STDOUT:       %T.as_type.loc20: type = facet_access_type %T.ref.loc20 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
-// CHECK:STDOUT:       %.loc20_34.2: type = converted %T.ref.loc20, %T.as_type.loc20 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
-// CHECK:STDOUT:       %type: type = facet_type <type> [concrete = constants.%type]
+// CHECK:STDOUT:       %.loc20_24.2: type = converted %T.ref.loc20, %T.as_type.loc20 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
+// CHECK:STDOUT:       %Empty.type: type = facet_type <@Empty, @Empty(constants.%T.binding.as_type)> [symbolic = %type (constants.%Empty.type.b8d23b.2)]
 // CHECK:STDOUT:     }
-// CHECK:STDOUT:     %V.loc20_23.2: %type = symbolic_binding V, 2 [symbolic = %V.loc20_23.1 (constants.%V)]
+// CHECK:STDOUT:     %U.loc20_13.2: @G.%type (%Empty.type.b8d23b.2) = symbolic_binding U, 1 [symbolic = %U.loc20_13.1 (constants.%U.aa1546.2)]
+// CHECK:STDOUT:     <elided>
+// CHECK:STDOUT:     %V.loc20_27.2: type = symbolic_binding V, 2 [symbolic = %V.loc20_27.1 (constants.%V)]
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
@@ -111,19 +115,22 @@ fn G(T:! Z, U:! type, V:! Empty(T)) {
 // CHECK:STDOUT:   %T.loc16_18.1: type = symbolic_binding T, 0 [symbolic = %T.loc16_18.1 (constants.%T.d9f)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
-// CHECK:STDOUT:   %Self.loc16_28.2: %type = symbolic_binding Self, 1 [symbolic = %Self.loc16_28.2 (constants.%Self.aa1)]
+// CHECK:STDOUT:   %type: type = facet_type <type> [symbolic = %type (constants.%Empty.type.b8d23b.1)]
+// CHECK:STDOUT:   %Self.loc16_28.2: @Empty.%type (%Empty.type.b8d23b.1) = symbolic_binding Self, 1 [symbolic = %Self.loc16_28.2 (constants.%Self.aa1)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   constraint {
-// CHECK:STDOUT:     %Self.loc16_28.1: %type = symbolic_binding Self, 1 [symbolic = %Self.loc16_28.2 (constants.%Self.aa1)]
+// CHECK:STDOUT:     %Self.loc16_28.1: @Empty.%type (%Empty.type.b8d23b.1) = symbolic_binding Self, 1 [symbolic = %Self.loc16_28.2 (constants.%Self.aa1)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   !members:
 // CHECK:STDOUT:     .Self = %Self.loc16_28.1
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: generic fn @F(%U.loc18_6.2: type, %T.loc18_16.2: %type) {
-// CHECK:STDOUT:   %U.loc18_6.1: type = symbolic_binding U, 0 [symbolic = %U.loc18_6.1 (constants.%U.d9f)]
-// CHECK:STDOUT:   %T.loc18_16.1: %type = symbolic_binding T, 1 [symbolic = %T.loc18_16.1 (constants.%T.aa1)]
+// CHECK:STDOUT: generic fn @F(%T.loc18_6.2: type, %U.loc18_16.2: @F.%type (%Empty.type.b8d23b.1)) {
+// CHECK:STDOUT:   %T.loc18_6.1: type = symbolic_binding T, 0 [symbolic = %T.loc18_6.1 (constants.%T.d9f)]
+// CHECK:STDOUT:   %type: type = facet_type <type> [symbolic = %type (constants.%Empty.type.b8d23b.1)]
+// CHECK:STDOUT:   %U.loc18_16.1: @F.%type (%Empty.type.b8d23b.1) = symbolic_binding U, 1 [symbolic = %U.loc18_16.1 (constants.%U.aa1546.1)]
+// CHECK:STDOUT:   %pattern_type: type = pattern_type %type [symbolic = %pattern_type (constants.%pattern_type.e25e9f.1)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT:
@@ -133,30 +140,35 @@ fn G(T:! Z, U:! type, V:! Empty(T)) {
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: generic fn @G(%T.loc20_6.2: %Z.type, %U.loc20_13.2: type, %V.loc20_23.2: %type) {
+// CHECK:STDOUT: generic fn @G(%T.loc20_6.2: %Z.type, %U.loc20_13.2: @G.%type (%Empty.type.b8d23b.2), %V.loc20_27.2: type) {
 // CHECK:STDOUT:   %T.loc20_6.1: %Z.type = symbolic_binding T, 0 [symbolic = %T.loc20_6.1 (constants.%T.3b3)]
-// CHECK:STDOUT:   %U.loc20_13.1: type = symbolic_binding U, 1 [symbolic = %U.loc20_13.1 (constants.%U.b88)]
 // CHECK:STDOUT:   %T.binding.as_type: type = symbolic_binding_type T, 0, %T.loc20_6.1 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
-// CHECK:STDOUT:   %V.loc20_23.1: %type = symbolic_binding V, 2 [symbolic = %V.loc20_23.1 (constants.%V)]
+// CHECK:STDOUT:   %type: type = facet_type <type> [symbolic = %type (constants.%Empty.type.b8d23b.2)]
+// CHECK:STDOUT:   %U.loc20_13.1: @G.%type (%Empty.type.b8d23b.2) = symbolic_binding U, 1 [symbolic = %U.loc20_13.1 (constants.%U.aa1546.2)]
+// CHECK:STDOUT:   %pattern_type: type = pattern_type %type [symbolic = %pattern_type (constants.%pattern_type.e25e9f.3)]
+// 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:   %F.specific_fn.loc21_3.2: <specific function> = specific_function constants.%F, @F(%T.binding.as_type, constants.%facet_value.6fa) [symbolic = %F.specific_fn.loc21_3.2 (constants.%F.specific_fn.8ba)]
 // CHECK:STDOUT:   %F.specific_fn.loc22_3.2: <specific function> = specific_function constants.%F, @F(%T.binding.as_type, constants.%facet_value.832) [symbolic = %F.specific_fn.loc22_3.2 (constants.%F.specific_fn.55c)]
 // CHECK:STDOUT:   %facet_value.loc23_9.2: %type = 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:   %facet_value.loc24_9.2: %type = facet_value %U.loc20_13.1, () [symbolic = %facet_value.loc24_9.2 (constants.%facet_value.a70)]
-// CHECK:STDOUT:   %F.specific_fn.loc24_3.2: <specific function> = specific_function constants.%F, @F(%T.binding.as_type, %facet_value.loc24_9.2) [symbolic = %F.specific_fn.loc24_3.2 (constants.%F.specific_fn.794)]
-// CHECK:STDOUT:   %F.specific_fn.loc25_3.2: <specific function> = specific_function constants.%F, @F(%T.binding.as_type, %V.loc20_23.1) [symbolic = %F.specific_fn.loc25_3.2 (constants.%F.specific_fn.e3f)]
+// CHECK:STDOUT:   %U.binding.as_type: type = symbolic_binding_type U, 1, %U.loc20_13.1 [symbolic = %U.binding.as_type (constants.%U.binding.as_type)]
+// CHECK:STDOUT:   %facet_value.loc24_9.2: %type = facet_value %U.binding.as_type, () [symbolic = %facet_value.loc24_9.2 (constants.%facet_value.356)]
+// CHECK:STDOUT:   %F.specific_fn.loc24_3.2: <specific function> = specific_function constants.%F, @F(%T.binding.as_type, %facet_value.loc24_9.2) [symbolic = %F.specific_fn.loc24_3.2 (constants.%F.specific_fn.df4)]
+// CHECK:STDOUT:   %facet_value.loc25_9.2: %type = 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:
 // CHECK:STDOUT:   fn() {
 // CHECK:STDOUT:   !entry:
 // CHECK:STDOUT:     %F.ref.loc21: %F.type = name_ref F, file.%F.decl [concrete = constants.%F]
 // CHECK:STDOUT:     %T.ref.loc21: %Z.type = name_ref T, %T.loc20_6.2 [symbolic = %T.loc20_6.1 (constants.%T.3b3)]
 // CHECK:STDOUT:     %.loc21_9: %empty_struct_type = struct_literal ()
+// 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_10.1: type = converted %T.ref.loc21, %T.as_type.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: %type = facet_value constants.%empty_struct_type, () [concrete = constants.%facet_value.6fa]
-// CHECK:STDOUT:     %.loc21_10.2: %type = converted %.loc21_9, %facet_value.loc21 [concrete = constants.%facet_value.6fa]
+// CHECK:STDOUT:     %.loc21_18.2: %type = converted constants.%empty_struct_type, %facet_value.loc21 [concrete = 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:     %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]
@@ -170,28 +182,31 @@ fn G(T:! Z, U:! type, V:! Empty(T)) {
 // 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)]
 // CHECK:STDOUT:     %T.ref.loc23_8: %Z.type = name_ref T, %T.loc20_6.2 [symbolic = %T.loc20_6.1 (constants.%T.3b3)]
-// 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 %T.ref.loc23_8 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
-// CHECK:STDOUT:     %facet_value.loc23_9.1: %type = facet_value %T.as_type.loc23_9.2, () [symbolic = %facet_value.loc23_9.2 (constants.%facet_value.146)]
-// CHECK:STDOUT:     %.loc23_9.2: %type = converted %T.ref.loc23_8, %facet_value.loc23_9.1 [symbolic = %facet_value.loc23_9.2 (constants.%facet_value.146)]
+// CHECK:STDOUT:     %T.as_type.loc23: 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 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
+// CHECK:STDOUT:     %as_type.loc23: type = facet_access_type constants.%T.3b3 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
+// CHECK:STDOUT:     %facet_value.loc23_9.1: %type = facet_value %as_type.loc23, () [symbolic = %facet_value.loc23_9.2 (constants.%facet_value.146)]
+// CHECK:STDOUT:     %.loc23_9.2: %type = 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:     %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)]
-// CHECK:STDOUT:     %U.ref: type = name_ref U, %U.loc20_13.2 [symbolic = %U.loc20_13.1 (constants.%U.b88)]
+// CHECK:STDOUT:     %U.ref: @G.%type (%Empty.type.b8d23b.2) = name_ref U, %U.loc20_13.2 [symbolic = %U.loc20_13.1 (constants.%U.aa1546.2)]
 // CHECK:STDOUT:     %T.as_type.loc24: type = facet_access_type %T.ref.loc24 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
 // CHECK:STDOUT:     %.loc24_9.1: type = converted %T.ref.loc24, %T.as_type.loc24 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
-// CHECK:STDOUT:     %facet_value.loc24_9.1: %type = facet_value %U.ref, () [symbolic = %facet_value.loc24_9.2 (constants.%facet_value.a70)]
-// CHECK:STDOUT:     %.loc24_9.2: %type = converted %U.ref, %facet_value.loc24_9.1 [symbolic = %facet_value.loc24_9.2 (constants.%facet_value.a70)]
-// CHECK:STDOUT:     %F.specific_fn.loc24_3.1: <specific function> = specific_function %F.ref.loc24, @F(constants.%T.binding.as_type, constants.%facet_value.a70) [symbolic = %F.specific_fn.loc24_3.2 (constants.%F.specific_fn.794)]
+// CHECK:STDOUT:     %as_type.loc24: type = facet_access_type constants.%U.aa1546.2 [symbolic = %U.binding.as_type (constants.%U.binding.as_type)]
+// CHECK:STDOUT:     %facet_value.loc24_9.1: %type = facet_value %as_type.loc24, () [symbolic = %facet_value.loc24_9.2 (constants.%facet_value.356)]
+// CHECK:STDOUT:     %.loc24_9.2: %type = converted constants.%U.aa1546.2, %facet_value.loc24_9.1 [symbolic = %facet_value.loc24_9.2 (constants.%facet_value.356)]
+// CHECK:STDOUT:     %F.specific_fn.loc24_3.1: <specific function> = specific_function %F.ref.loc24, @F(constants.%T.binding.as_type, constants.%facet_value.356) [symbolic = %F.specific_fn.loc24_3.2 (constants.%F.specific_fn.df4)]
 // CHECK:STDOUT:     %F.call.loc24: init %empty_tuple.type = call %F.specific_fn.loc24_3.1()
 // CHECK:STDOUT:     %F.ref.loc25: %F.type = name_ref F, file.%F.decl [concrete = constants.%F]
 // CHECK:STDOUT:     %T.ref.loc25: %Z.type = name_ref T, %T.loc20_6.2 [symbolic = %T.loc20_6.1 (constants.%T.3b3)]
-// CHECK:STDOUT:     %V.ref: %type = name_ref V, %V.loc20_23.2 [symbolic = %V.loc20_23.1 (constants.%V)]
+// 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: type = converted %T.ref.loc25, %T.as_type.loc25 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
-// CHECK:STDOUT:     %F.specific_fn.loc25_3.1: <specific function> = specific_function %F.ref.loc25, @F(constants.%T.binding.as_type, constants.%V) [symbolic = %F.specific_fn.loc25_3.2 (constants.%F.specific_fn.e3f)]
+// 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: %type = facet_value constants.%V, () [symbolic = %facet_value.loc25_9.2 (constants.%facet_value.920)]
+// CHECK:STDOUT:     %.loc25_9.2: %type = 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:     %F.call.loc25: init %empty_tuple.type = call %F.specific_fn.loc25_3.1()
 // CHECK:STDOUT:     return
 // CHECK:STDOUT:   }
@@ -201,57 +216,67 @@ fn G(T:! Z, U:! type, V:! Empty(T)) {
 // CHECK:STDOUT:   %T.loc16_18.1 => constants.%T.d9f
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @Empty(constants.%U.d9f) {
-// CHECK:STDOUT:   %T.loc16_18.1 => constants.%U.d9f
-// CHECK:STDOUT: }
-// CHECK:STDOUT:
-// CHECK:STDOUT: specific @F(constants.%U.d9f, constants.%T.aa1) {
-// CHECK:STDOUT:   %U.loc18_6.1 => constants.%U.d9f
-// CHECK:STDOUT:   %T.loc18_16.1 => constants.%T.aa1
+// CHECK:STDOUT: specific @F(constants.%T.d9f, constants.%U.aa1546.1) {
+// CHECK:STDOUT:   %T.loc18_6.1 => constants.%T.d9f
+// CHECK:STDOUT:   %type => constants.%type
+// CHECK:STDOUT:   %U.loc18_16.1 => constants.%U.aa1546.1
+// CHECK:STDOUT:   %pattern_type => constants.%pattern_type.e25e9f.2
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @Empty(constants.%T.binding.as_type) {
 // CHECK:STDOUT:   %T.loc16_18.1 => constants.%T.binding.as_type
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @G(constants.%T.3b3, constants.%U.b88, constants.%V) {
+// CHECK:STDOUT: specific @G(constants.%T.3b3, constants.%U.aa1546.2, constants.%V) {
 // CHECK:STDOUT:   %T.loc20_6.1 => constants.%T.3b3
-// CHECK:STDOUT:   %U.loc20_13.1 => constants.%U.b88
 // CHECK:STDOUT:   %T.binding.as_type => constants.%T.binding.as_type
-// CHECK:STDOUT:   %V.loc20_23.1 => constants.%V
+// CHECK:STDOUT:   %type => constants.%type
+// CHECK:STDOUT:   %U.loc20_13.1 => constants.%U.aa1546.2
+// CHECK:STDOUT:   %pattern_type => constants.%pattern_type.e25e9f.2
+// 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:   %U.loc18_6.1 => constants.%T.binding.as_type
-// CHECK:STDOUT:   %T.loc18_16.1 => constants.%facet_value.6fa
+// CHECK:STDOUT:   %T.loc18_6.1 => constants.%T.binding.as_type
+// CHECK:STDOUT:   %type => constants.%type
+// CHECK:STDOUT:   %U.loc18_16.1 => constants.%facet_value.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:   %U.loc18_6.1 => constants.%T.binding.as_type
-// CHECK:STDOUT:   %T.loc18_16.1 => constants.%facet_value.832
+// CHECK:STDOUT:   %T.loc18_6.1 => constants.%T.binding.as_type
+// CHECK:STDOUT:   %type => constants.%type
+// CHECK:STDOUT:   %U.loc18_16.1 => constants.%facet_value.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:   %U.loc18_6.1 => constants.%T.binding.as_type
-// CHECK:STDOUT:   %T.loc18_16.1 => constants.%facet_value.146
+// CHECK:STDOUT:   %T.loc18_6.1 => constants.%T.binding.as_type
+// CHECK:STDOUT:   %type => constants.%type
+// CHECK:STDOUT:   %U.loc18_16.1 => constants.%facet_value.146
+// 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.a70) {
-// CHECK:STDOUT:   %U.loc18_6.1 => constants.%T.binding.as_type
-// CHECK:STDOUT:   %T.loc18_16.1 => constants.%facet_value.a70
+// CHECK:STDOUT: specific @F(constants.%T.binding.as_type, constants.%facet_value.356) {
+// CHECK:STDOUT:   %T.loc18_6.1 => constants.%T.binding.as_type
+// CHECK:STDOUT:   %type => constants.%type
+// CHECK:STDOUT:   %U.loc18_16.1 => constants.%facet_value.356
+// 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.%V) {
-// CHECK:STDOUT:   %U.loc18_6.1 => constants.%T.binding.as_type
-// CHECK:STDOUT:   %T.loc18_16.1 => constants.%V
+// CHECK:STDOUT: specific @F(constants.%T.binding.as_type, constants.%facet_value.920) {
+// CHECK:STDOUT:   %T.loc18_6.1 => constants.%T.binding.as_type
+// CHECK:STDOUT:   %type => constants.%type
+// CHECK:STDOUT:   %U.loc18_16.1 => constants.%facet_value.920
+// CHECK:STDOUT:   %pattern_type => constants.%pattern_type.e25e9f.2
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT: }

+ 25 - 19
toolchain/check/testdata/named_constraint/generic.carbon

@@ -82,19 +82,22 @@ fn F(T:! Generic((), ())) {}
 // CHECK:STDOUT:   %.Self: %type = symbolic_binding .Self [symbolic_self]
 // CHECK:STDOUT:   %T: type = symbolic_binding T, 0 [symbolic]
 // CHECK:STDOUT:   %pattern_type.98f: type = pattern_type type [concrete]
-// CHECK:STDOUT:   %GenericType.type: type = generic_named_constaint_type @GenericType [concrete]
-// CHECK:STDOUT:   %empty_struct.bd5: %GenericType.type = struct_value () [concrete]
-// CHECK:STDOUT:   %Self.aa1546.1: %type = symbolic_binding Self, 1 [symbolic]
+// CHECK:STDOUT:   %GenericType.type.ace: type = generic_named_constaint_type @GenericType [concrete]
+// CHECK:STDOUT:   %empty_struct.bd5: %GenericType.type.ace = struct_value () [concrete]
+// CHECK:STDOUT:   %GenericType.type.b8d: type = facet_type <@GenericType, @GenericType(%T)> [symbolic]
+// CHECK:STDOUT:   %Self.aa1546.1: %GenericType.type.b8d = symbolic_binding Self, 1 [symbolic]
 // CHECK:STDOUT:   %Z.type: type = facet_type <@Z> [concrete]
 // CHECK:STDOUT:   %Self.3b3: %Z.type = symbolic_binding Self, 0 [symbolic]
 // CHECK:STDOUT:   %U: %Z.type = symbolic_binding U, 0 [symbolic]
 // CHECK:STDOUT:   %pattern_type.4a0: type = pattern_type %Z.type [concrete]
-// CHECK:STDOUT:   %GenericZ.type: type = generic_named_constaint_type @GenericZ [concrete]
-// CHECK:STDOUT:   %empty_struct.05e: %GenericZ.type = struct_value () [concrete]
-// CHECK:STDOUT:   %Self.aa1546.2: %type = symbolic_binding Self, 1 [symbolic]
-// CHECK:STDOUT:   %ForwardDeclaredGeneric.type: type = generic_named_constaint_type @ForwardDeclaredGeneric [concrete]
-// CHECK:STDOUT:   %empty_struct.1a7: %ForwardDeclaredGeneric.type = struct_value () [concrete]
-// CHECK:STDOUT:   %Self.aa1546.3: %type = symbolic_binding Self, 1 [symbolic]
+// CHECK:STDOUT:   %GenericZ.type.e48: type = generic_named_constaint_type @GenericZ [concrete]
+// CHECK:STDOUT:   %empty_struct.05e: %GenericZ.type.e48 = struct_value () [concrete]
+// CHECK:STDOUT:   %GenericZ.type.b8d: type = facet_type <@GenericZ, @GenericZ(%U)> [symbolic]
+// CHECK:STDOUT:   %Self.aa1546.2: %GenericZ.type.b8d = symbolic_binding Self, 1 [symbolic]
+// CHECK:STDOUT:   %ForwardDeclaredGeneric.type.341: type = generic_named_constaint_type @ForwardDeclaredGeneric [concrete]
+// CHECK:STDOUT:   %empty_struct.1a7: %ForwardDeclaredGeneric.type.341 = struct_value () [concrete]
+// CHECK:STDOUT:   %ForwardDeclaredGeneric.type.b8d: type = facet_type <@ForwardDeclaredGeneric, @ForwardDeclaredGeneric(%T)> [symbolic]
+// CHECK:STDOUT:   %Self.aa1546.3: %ForwardDeclaredGeneric.type.b8d = symbolic_binding Self, 1 [symbolic]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
@@ -104,14 +107,14 @@ fn F(T:! Generic((), ())) {}
 // CHECK:STDOUT:     .GenericZ = %GenericZ.decl
 // CHECK:STDOUT:     .ForwardDeclaredGeneric = %ForwardDeclaredGeneric.decl.loc9
 // CHECK:STDOUT:   }
-// CHECK:STDOUT:   %GenericType.decl: %GenericType.type = constraint_decl @GenericType [concrete = constants.%empty_struct.bd5] {
+// CHECK:STDOUT:   %GenericType.decl: %GenericType.type.ace = constraint_decl @GenericType [concrete = constants.%empty_struct.bd5] {
 // CHECK:STDOUT:     %T.patt: %pattern_type.98f = symbolic_binding_pattern T, 0 [concrete]
 // CHECK:STDOUT:   } {
 // CHECK:STDOUT:     %.Self: %type = symbolic_binding .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:     %T.loc4_24.2: type = symbolic_binding T, 0 [symbolic = %T.loc4_24.1 (constants.%T)]
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %Z.decl: type = interface_decl @Z [concrete = constants.%Z.type] {} {}
-// CHECK:STDOUT:   %GenericZ.decl: %GenericZ.type = constraint_decl @GenericZ [concrete = constants.%empty_struct.05e] {
+// CHECK:STDOUT:   %GenericZ.decl: %GenericZ.type.e48 = constraint_decl @GenericZ [concrete = constants.%empty_struct.05e] {
 // CHECK:STDOUT:     %U.patt: %pattern_type.4a0 = symbolic_binding_pattern U, 0 [concrete]
 // CHECK:STDOUT:   } {
 // CHECK:STDOUT:     %.loc7: type = splice_block %Z.ref [concrete = constants.%Z.type] {
@@ -120,13 +123,13 @@ fn F(T:! Generic((), ())) {}
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %U.loc7_21.2: %Z.type = symbolic_binding U, 0 [symbolic = %U.loc7_21.1 (constants.%U)]
 // CHECK:STDOUT:   }
-// CHECK:STDOUT:   %ForwardDeclaredGeneric.decl.loc9: %ForwardDeclaredGeneric.type = constraint_decl @ForwardDeclaredGeneric [concrete = constants.%empty_struct.1a7] {
+// CHECK:STDOUT:   %ForwardDeclaredGeneric.decl.loc9: %ForwardDeclaredGeneric.type.341 = constraint_decl @ForwardDeclaredGeneric [concrete = constants.%empty_struct.1a7] {
 // CHECK:STDOUT:     %T.patt: %pattern_type.98f = symbolic_binding_pattern T, 0 [concrete]
 // CHECK:STDOUT:   } {
 // CHECK:STDOUT:     %.Self.2: %type = symbolic_binding .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:     %T.loc9_35.2: type = symbolic_binding T, 0 [symbolic = %T.loc9_35.1 (constants.%T)]
 // CHECK:STDOUT:   }
-// CHECK:STDOUT:   %ForwardDeclaredGeneric.decl.loc10: %ForwardDeclaredGeneric.type = constraint_decl @ForwardDeclaredGeneric [concrete = constants.%empty_struct.1a7] {
+// CHECK:STDOUT:   %ForwardDeclaredGeneric.decl.loc10: %ForwardDeclaredGeneric.type.341 = constraint_decl @ForwardDeclaredGeneric [concrete = constants.%empty_struct.1a7] {
 // CHECK:STDOUT:     %T.patt: %pattern_type.98f = symbolic_binding_pattern T, 0 [concrete]
 // CHECK:STDOUT:   } {
 // CHECK:STDOUT:     %.Self.1: %type = symbolic_binding .Self [symbolic_self = constants.%.Self]
@@ -146,10 +149,11 @@ fn F(T:! Generic((), ())) {}
 // CHECK:STDOUT:   %T.loc4_24.1: type = symbolic_binding T, 0 [symbolic = %T.loc4_24.1 (constants.%T)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
-// CHECK:STDOUT:   %Self.loc4_34.2: %type = symbolic_binding Self, 1 [symbolic = %Self.loc4_34.2 (constants.%Self.aa1546.1)]
+// CHECK:STDOUT:   %type: type = facet_type <type> [symbolic = %type (constants.%GenericType.type.b8d)]
+// CHECK:STDOUT:   %Self.loc4_34.2: @GenericType.%type (%GenericType.type.b8d) = symbolic_binding Self, 1 [symbolic = %Self.loc4_34.2 (constants.%Self.aa1546.1)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   constraint {
-// CHECK:STDOUT:     %Self.loc4_34.1: %type = symbolic_binding Self, 1 [symbolic = %Self.loc4_34.2 (constants.%Self.aa1546.1)]
+// CHECK:STDOUT:     %Self.loc4_34.1: @GenericType.%type (%GenericType.type.b8d) = symbolic_binding Self, 1 [symbolic = %Self.loc4_34.2 (constants.%Self.aa1546.1)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   !members:
 // CHECK:STDOUT:     .Self = %Self.loc4_34.1
@@ -160,10 +164,11 @@ fn F(T:! Generic((), ())) {}
 // CHECK:STDOUT:   %U.loc7_21.1: %Z.type = symbolic_binding U, 0 [symbolic = %U.loc7_21.1 (constants.%U)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
-// CHECK:STDOUT:   %Self.loc7_28.2: %type = symbolic_binding Self, 1 [symbolic = %Self.loc7_28.2 (constants.%Self.aa1546.2)]
+// CHECK:STDOUT:   %type: type = facet_type <type> [symbolic = %type (constants.%GenericZ.type.b8d)]
+// CHECK:STDOUT:   %Self.loc7_28.2: @GenericZ.%type (%GenericZ.type.b8d) = symbolic_binding Self, 1 [symbolic = %Self.loc7_28.2 (constants.%Self.aa1546.2)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   constraint {
-// CHECK:STDOUT:     %Self.loc7_28.1: %type = symbolic_binding Self, 1 [symbolic = %Self.loc7_28.2 (constants.%Self.aa1546.2)]
+// CHECK:STDOUT:     %Self.loc7_28.1: @GenericZ.%type (%GenericZ.type.b8d) = symbolic_binding Self, 1 [symbolic = %Self.loc7_28.2 (constants.%Self.aa1546.2)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   !members:
 // CHECK:STDOUT:     .Self = %Self.loc7_28.1
@@ -174,10 +179,11 @@ fn F(T:! Generic((), ())) {}
 // CHECK:STDOUT:   %T.loc9_35.1: type = symbolic_binding T, 0 [symbolic = %T.loc9_35.1 (constants.%T)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
-// CHECK:STDOUT:   %Self.loc10_45.2: %type = symbolic_binding Self, 1 [symbolic = %Self.loc10_45.2 (constants.%Self.aa1546.3)]
+// CHECK:STDOUT:   %type: type = facet_type <type> [symbolic = %type (constants.%ForwardDeclaredGeneric.type.b8d)]
+// CHECK:STDOUT:   %Self.loc10_45.2: @ForwardDeclaredGeneric.%type (%ForwardDeclaredGeneric.type.b8d) = symbolic_binding Self, 1 [symbolic = %Self.loc10_45.2 (constants.%Self.aa1546.3)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   constraint {
-// CHECK:STDOUT:     %Self.loc10_45.1: %type = symbolic_binding Self, 1 [symbolic = %Self.loc10_45.2 (constants.%Self.aa1546.3)]
+// CHECK:STDOUT:     %Self.loc10_45.1: @ForwardDeclaredGeneric.%type (%ForwardDeclaredGeneric.type.b8d) = symbolic_binding Self, 1 [symbolic = %Self.loc10_45.2 (constants.%Self.aa1546.3)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   !members:
 // CHECK:STDOUT:     .Self = %Self.loc10_45.1

+ 76 - 58
toolchain/check/testdata/named_constraint/require.carbon

@@ -29,7 +29,7 @@ fn F(T:! Z) {
   // CHECK:STDERR:   ^~~~
   // CHECK:STDERR:
   T.YY();
-  // CHECK:STDERR: fail_todo_extend.carbon:[[@LINE+4]]:3: error: cannot convert type `T` that implements `type` into type implementing `Y` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR: fail_todo_extend.carbon:[[@LINE+4]]:3: error: cannot convert type `T` that implements `Z` into type implementing `Y` [ConversionFailureFacetToFacet]
   // CHECK:STDERR:   T.(Y.YY)();
   // CHECK:STDERR:   ^~~~~~~~
   // CHECK:STDERR:
@@ -50,7 +50,7 @@ constraint Z {
 //@dump-sem-ir-end
 
 fn F(T:! Z) {
-  // CHECK:STDERR: fail_todo_implicit_self_impls.carbon:[[@LINE+4]]:3: error: cannot convert type `T` that implements `type` into type implementing `Y` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR: fail_todo_implicit_self_impls.carbon:[[@LINE+4]]:3: error: cannot convert type `T` that implements `Z` into type implementing `Y` [ConversionFailureFacetToFacet]
   // CHECK:STDERR:   T.(Y.YY)();
   // CHECK:STDERR:   ^~~~~~~~
   // CHECK:STDERR:
@@ -71,7 +71,7 @@ constraint Z {
 //@dump-sem-ir-end
 
 fn F(T:! Z) {
-  // CHECK:STDERR: fail_todo_explicit_self_impls.carbon:[[@LINE+4]]:3: error: cannot convert type `T` that implements `type` into type implementing `Y` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR: fail_todo_explicit_self_impls.carbon:[[@LINE+4]]:3: error: cannot convert type `T` that implements `Z` into type implementing `Y` [ConversionFailureFacetToFacet]
   // CHECK:STDERR:   T.(Y.YY)();
   // CHECK:STDERR:   ^~~~~~~~
   // CHECK:STDERR:
@@ -144,24 +144,36 @@ constraint Z {
 }
 //@dump-sem-ir-end
 
-// --- todo_fail_require_impls_incomplete_constraint.carbon
+// --- fail_require_impls_incomplete_constraint.carbon
 library "[[@TEST_NAME]]";
 
 constraint Y;
 
 //@dump-sem-ir-begin
 constraint Z {
-  // TODO: This should fail since `Y` cannot be identified.
+  // CHECK:STDERR: fail_require_impls_incomplete_constraint.carbon:[[@LINE+7]]:17: error: facet type `Y` cannot be identified in `require` declaration [RequireImplsUnidentifiedFacetType]
+  // CHECK:STDERR:   require impls Y;
+  // CHECK:STDERR:                 ^
+  // CHECK:STDERR: fail_require_impls_incomplete_constraint.carbon:[[@LINE-7]]:1: note: constraint was forward declared here [NamedConstraintForwardDeclaredHere]
+  // CHECK:STDERR: constraint Y;
+  // CHECK:STDERR: ^~~~~~~~~~~~~
+  // CHECK:STDERR:
   require impls Y;
 }
 //@dump-sem-ir-end
 
-// --- todo_fail_require_impls_incomplete_self.carbon
+// --- fail_require_impls_incomplete_self.carbon
 library "[[@TEST_NAME]]";
 
 //@dump-sem-ir-begin
 constraint Z {
-  // TODO: This should fail since `Z` cannot be identified.
+  // CHECK:STDERR: fail_require_impls_incomplete_self.carbon:[[@LINE+7]]:17: error: facet type `Z` cannot be identified in `require` declaration [RequireImplsUnidentifiedFacetType]
+  // CHECK:STDERR:   require impls Z;
+  // CHECK:STDERR:                 ^
+  // CHECK:STDERR: fail_require_impls_incomplete_self.carbon:[[@LINE-4]]:1: note: constraint is currently being defined [NamedConstraintIncompleteWithinDefinition]
+  // CHECK:STDERR: constraint Z {
+  // CHECK:STDERR: ^~~~~~~~~~~~~~
+  // CHECK:STDERR:
   require impls Z;
 }
 //@dump-sem-ir-end
@@ -171,10 +183,12 @@ library "[[@TEST_NAME]]";
 
 //@dump-sem-ir-begin
 constraint Z(T:! type) {
-  // TODO: This should fail since `Z` cannot be identified.
-  // CHECK:STDERR: fail_require_impls_incomplete_self_specific.carbon:[[@LINE+4]]:3: error: no `Self` reference found in `require` declaration; `Self` must appear in the self-type or as a generic parameter for each `interface` or `constraint` [RequireImplsMissingSelf]
+  // CHECK:STDERR: fail_require_impls_incomplete_self_specific.carbon:[[@LINE+7]]:19: error: facet type `Z(Self)` cannot be identified in `require` declaration [RequireImplsUnidentifiedFacetType]
   // CHECK:STDERR:   require T impls Z(Self);
-  // CHECK:STDERR:   ^~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR:                   ^~~~~~~
+  // CHECK:STDERR: fail_require_impls_incomplete_self_specific.carbon:[[@LINE-4]]:1: note: constraint is currently being defined [NamedConstraintIncompleteWithinDefinition]
+  // CHECK:STDERR: constraint Z(T:! type) {
+  // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~
   // CHECK:STDERR:
   require T impls Z(Self);
 }
@@ -286,19 +300,19 @@ constraint Z {
 // CHECK:STDOUT: --- fail_todo_extend.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
-// CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
-// CHECK:STDOUT:   %Self.861: %type = symbolic_binding Self, 0 [symbolic]
+// CHECK:STDOUT:   %Z.type: type = facet_type <@Z> [concrete]
+// CHECK:STDOUT:   %Self.861: %Z.type = symbolic_binding Self, 0 [symbolic]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: imports {
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
-// CHECK:STDOUT:   %Z.decl: type = constraint_decl @Z [concrete = constants.%type] {} {}
+// CHECK:STDOUT:   %Z.decl: type = constraint_decl @Z [concrete = constants.%Z.type] {} {}
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: constraint @Z {
-// CHECK:STDOUT:   %Self: %type = symbolic_binding Self, 0 [symbolic = constants.%Self.861]
+// CHECK:STDOUT:   %Self: %Z.type = symbolic_binding Self, 0 [symbolic = constants.%Self.861]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !members:
 // CHECK:STDOUT:   .Self = %Self
@@ -308,19 +322,19 @@ constraint Z {
 // CHECK:STDOUT: --- fail_todo_implicit_self_impls.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
-// CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
-// CHECK:STDOUT:   %Self.861: %type = symbolic_binding Self, 0 [symbolic]
+// CHECK:STDOUT:   %Z.type: type = facet_type <@Z> [concrete]
+// CHECK:STDOUT:   %Self.861: %Z.type = symbolic_binding Self, 0 [symbolic]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: imports {
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
-// CHECK:STDOUT:   %Z.decl: type = constraint_decl @Z [concrete = constants.%type] {} {}
+// CHECK:STDOUT:   %Z.decl: type = constraint_decl @Z [concrete = constants.%Z.type] {} {}
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: constraint @Z {
-// CHECK:STDOUT:   %Self: %type = symbolic_binding Self, 0 [symbolic = constants.%Self.861]
+// CHECK:STDOUT:   %Self: %Z.type = symbolic_binding Self, 0 [symbolic = constants.%Self.861]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !members:
 // CHECK:STDOUT:   .Self = %Self
@@ -330,19 +344,19 @@ constraint Z {
 // CHECK:STDOUT: --- fail_todo_explicit_self_impls.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
-// CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
-// CHECK:STDOUT:   %Self.861: %type = symbolic_binding Self, 0 [symbolic]
+// CHECK:STDOUT:   %Z.type: type = facet_type <@Z> [concrete]
+// CHECK:STDOUT:   %Self.861: %Z.type = symbolic_binding Self, 0 [symbolic]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: imports {
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
-// CHECK:STDOUT:   %Z.decl: type = constraint_decl @Z [concrete = constants.%type] {} {}
+// CHECK:STDOUT:   %Z.decl: type = constraint_decl @Z [concrete = constants.%Z.type] {} {}
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: constraint @Z {
-// CHECK:STDOUT:   %Self: %type = symbolic_binding Self, 0 [symbolic = constants.%Self.861]
+// CHECK:STDOUT:   %Self: %Z.type = symbolic_binding Self, 0 [symbolic = constants.%Self.861]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !members:
 // CHECK:STDOUT:   .Self = %Self
@@ -352,19 +366,19 @@ constraint Z {
 // CHECK:STDOUT: --- explicit_self_specific_impls.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
-// CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
-// CHECK:STDOUT:   %Self.861: %type = symbolic_binding Self, 0 [symbolic]
+// CHECK:STDOUT:   %Z.type: type = facet_type <@Z> [concrete]
+// CHECK:STDOUT:   %Self.861: %Z.type = symbolic_binding Self, 0 [symbolic]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: imports {
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
-// CHECK:STDOUT:   %Z.decl: type = constraint_decl @Z [concrete = constants.%type] {} {}
+// CHECK:STDOUT:   %Z.decl: type = constraint_decl @Z [concrete = constants.%Z.type] {} {}
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: constraint @Z {
-// CHECK:STDOUT:   %Self: %type = symbolic_binding Self, 0 [symbolic = constants.%Self.861]
+// CHECK:STDOUT:   %Self: %Z.type = symbolic_binding Self, 0 [symbolic = constants.%Self.861]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !members:
 // CHECK:STDOUT:   .Self = %Self
@@ -375,63 +389,63 @@ constraint Z {
 // CHECK:STDOUT: --- require_impls_where.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
-// CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
-// CHECK:STDOUT:   %Self.861: %type = symbolic_binding Self, 0 [symbolic]
+// CHECK:STDOUT:   %Z.type: type = facet_type <@Z> [concrete]
+// CHECK:STDOUT:   %Self.861: %Z.type = symbolic_binding Self, 0 [symbolic]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: imports {
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
-// CHECK:STDOUT:   %Z.decl: type = constraint_decl @Z [concrete = constants.%type] {} {}
+// CHECK:STDOUT:   %Z.decl: type = constraint_decl @Z [concrete = constants.%Z.type] {} {}
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: constraint @Z {
-// CHECK:STDOUT:   %Self: %type = symbolic_binding Self, 0 [symbolic = constants.%Self.861]
+// CHECK:STDOUT:   %Self: %Z.type = symbolic_binding Self, 0 [symbolic = constants.%Self.861]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !members:
 // CHECK:STDOUT:   .Self = %Self
 // CHECK:STDOUT:   .Y = <poisoned>
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: --- todo_fail_require_impls_incomplete_constraint.carbon
+// CHECK:STDOUT: --- fail_require_impls_incomplete_constraint.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
-// CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
-// CHECK:STDOUT:   %Self: %type = symbolic_binding Self, 0 [symbolic]
+// CHECK:STDOUT:   %Z.type: type = facet_type <@Z> [concrete]
+// CHECK:STDOUT:   %Self: %Z.type = symbolic_binding Self, 0 [symbolic]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: imports {
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
-// CHECK:STDOUT:   %Z.decl: type = constraint_decl @Z [concrete = constants.%type] {} {}
+// CHECK:STDOUT:   %Z.decl: type = constraint_decl @Z [concrete = constants.%Z.type] {} {}
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: constraint @Z {
-// CHECK:STDOUT:   %Self: %type = symbolic_binding Self, 0 [symbolic = constants.%Self]
+// CHECK:STDOUT:   %Self: %Z.type = symbolic_binding Self, 0 [symbolic = constants.%Self]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !members:
 // CHECK:STDOUT:   .Self = %Self
 // CHECK:STDOUT:   .Y = <poisoned>
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: --- todo_fail_require_impls_incomplete_self.carbon
+// CHECK:STDOUT: --- fail_require_impls_incomplete_self.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
-// CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
-// CHECK:STDOUT:   %Self: %type = symbolic_binding Self, 0 [symbolic]
+// CHECK:STDOUT:   %Z.type: type = facet_type <@Z> [concrete]
+// CHECK:STDOUT:   %Self: %Z.type = symbolic_binding Self, 0 [symbolic]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: imports {
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
-// CHECK:STDOUT:   %Z.decl: type = constraint_decl @Z [concrete = constants.%type] {} {}
+// CHECK:STDOUT:   %Z.decl: type = constraint_decl @Z [concrete = constants.%Z.type] {} {}
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: constraint @Z {
-// CHECK:STDOUT:   %Self: %type = symbolic_binding Self, 0 [symbolic = constants.%Self]
+// CHECK:STDOUT:   %Self: %Z.type = symbolic_binding Self, 0 [symbolic = constants.%Self]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !members:
 // CHECK:STDOUT:   .Self = %Self
@@ -441,20 +455,21 @@ constraint Z {
 // CHECK:STDOUT: --- fail_require_impls_incomplete_self_specific.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
-// CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
 // CHECK:STDOUT:   %T: type = symbolic_binding T, 0 [symbolic]
 // CHECK:STDOUT:   %pattern_type: type = pattern_type type [concrete]
-// CHECK:STDOUT:   %Z.type: type = generic_named_constaint_type @Z [concrete]
-// CHECK:STDOUT:   %empty_struct: %Z.type = struct_value () [concrete]
-// CHECK:STDOUT:   %Self: %type = symbolic_binding Self, 1 [symbolic]
+// CHECK:STDOUT:   %Z.type.82a: type = generic_named_constaint_type @Z [concrete]
+// CHECK:STDOUT:   %empty_struct: %Z.type.82a = struct_value () [concrete]
+// CHECK:STDOUT:   %Z.type.b8d23b.1: type = facet_type <@Z, @Z(%T)> [symbolic]
+// CHECK:STDOUT:   %Self: %Z.type.b8d23b.1 = symbolic_binding Self, 1 [symbolic]
 // CHECK:STDOUT:   %Self.binding.as_type: type = symbolic_binding_type Self, 1, %Self [symbolic]
+// CHECK:STDOUT:   %Z.type.b8d23b.2: type = facet_type <@Z, @Z(%Self.binding.as_type)> [symbolic]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: imports {
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
-// CHECK:STDOUT:   %Z.decl: %Z.type = constraint_decl @Z [concrete = constants.%empty_struct] {
+// CHECK:STDOUT:   %Z.decl: %Z.type.82a = constraint_decl @Z [concrete = constants.%empty_struct] {
 // CHECK:STDOUT:     %T.patt: %pattern_type = symbolic_binding_pattern T, 0 [concrete]
 // CHECK:STDOUT:   } {
 // CHECK:STDOUT:     <elided>
@@ -466,11 +481,13 @@ constraint Z {
 // CHECK:STDOUT:   %T.loc4_14.1: type = symbolic_binding T, 0 [symbolic = %T.loc4_14.1 (constants.%T)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
-// CHECK:STDOUT:   %Self.loc4_24.2: %type = symbolic_binding Self, 1 [symbolic = %Self.loc4_24.2 (constants.%Self)]
+// CHECK:STDOUT:   %type.loc4: type = facet_type <type> [symbolic = %type.loc4 (constants.%Z.type.b8d23b.1)]
+// CHECK:STDOUT:   %Self.loc4_24.2: @Z.%type.loc4 (%Z.type.b8d23b.1) = symbolic_binding Self, 1 [symbolic = %Self.loc4_24.2 (constants.%Self)]
 // CHECK:STDOUT:   %Self.binding.as_type: type = symbolic_binding_type Self, 1, %Self.loc4_24.2 [symbolic = %Self.binding.as_type (constants.%Self.binding.as_type)]
+// CHECK:STDOUT:   %type.loc12: type = facet_type <type> [symbolic = %type.loc12 (constants.%Z.type.b8d23b.2)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   constraint {
-// CHECK:STDOUT:     %Self.loc4_24.1: %type = symbolic_binding Self, 1 [symbolic = %Self.loc4_24.2 (constants.%Self)]
+// CHECK:STDOUT:     %Self.loc4_24.1: @Z.%type.loc4 (%Z.type.b8d23b.1) = symbolic_binding Self, 1 [symbolic = %Self.loc4_24.2 (constants.%Self)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   !members:
 // CHECK:STDOUT:     .Self = %Self.loc4_24.1
@@ -491,12 +508,12 @@ constraint Z {
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
 // CHECK:STDOUT:   %Y.type: type = facet_type <@Y> [concrete]
-// CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
 // CHECK:STDOUT:   %T: type = symbolic_binding T, 0 [symbolic]
 // CHECK:STDOUT:   %pattern_type: type = pattern_type type [concrete]
-// CHECK:STDOUT:   %Z.type: type = generic_named_constaint_type @Z [concrete]
-// CHECK:STDOUT:   %empty_struct: %Z.type = struct_value () [concrete]
-// CHECK:STDOUT:   %Self.aa1: %type = symbolic_binding Self, 1 [symbolic]
+// CHECK:STDOUT:   %Z.type.82a: type = generic_named_constaint_type @Z [concrete]
+// CHECK:STDOUT:   %empty_struct: %Z.type.82a = struct_value () [concrete]
+// CHECK:STDOUT:   %Z.type.b8d: type = facet_type <@Z, @Z(%T)> [symbolic]
+// CHECK:STDOUT:   %Self.aa1: %Z.type.b8d = symbolic_binding Self, 1 [symbolic]
 // CHECK:STDOUT:   %.Self.a96: %Y.type = symbolic_binding .Self [symbolic_self]
 // CHECK:STDOUT:   %Y.lookup_impl_witness: <witness> = lookup_impl_witness %.Self.a96, @Y [symbolic_self]
 // CHECK:STDOUT:   %impl.elem0: type = impl_witness_access %Y.lookup_impl_witness, element0 [symbolic_self]
@@ -508,7 +525,7 @@ constraint Z {
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
-// CHECK:STDOUT:   %Z.decl: %Z.type = constraint_decl @Z [concrete = constants.%empty_struct] {
+// CHECK:STDOUT:   %Z.decl: %Z.type.82a = constraint_decl @Z [concrete = constants.%empty_struct] {
 // CHECK:STDOUT:     %T.patt: %pattern_type = symbolic_binding_pattern T, 0 [concrete]
 // CHECK:STDOUT:   } {
 // CHECK:STDOUT:     <elided>
@@ -520,12 +537,13 @@ constraint Z {
 // CHECK:STDOUT:   %T.loc8_14.1: type = symbolic_binding T, 0 [symbolic = %T.loc8_14.1 (constants.%T)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
-// CHECK:STDOUT:   %Self.loc8_24.2: %type = symbolic_binding Self, 1 [symbolic = %Self.loc8_24.2 (constants.%Self.aa1)]
+// CHECK:STDOUT:   %type: type = facet_type <type> [symbolic = %type (constants.%Z.type.b8d)]
+// CHECK:STDOUT:   %Self.loc8_24.2: @Z.%type (%Z.type.b8d) = symbolic_binding Self, 1 [symbolic = %Self.loc8_24.2 (constants.%Self.aa1)]
 // CHECK:STDOUT:   %Self.binding.as_type: type = symbolic_binding_type Self, 1, %Self.loc8_24.2 [symbolic = %Self.binding.as_type (constants.%Self.binding.as_type)]
 // CHECK:STDOUT:   %Y_where.type: type = facet_type <@Y where constants.%impl.elem0 = %Self.binding.as_type> [symbolic = %Y_where.type (constants.%Y_where.type)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   constraint {
-// CHECK:STDOUT:     %Self.loc8_24.1: %type = symbolic_binding Self, 1 [symbolic = %Self.loc8_24.2 (constants.%Self.aa1)]
+// CHECK:STDOUT:     %Self.loc8_24.1: @Z.%type (%Z.type.b8d) = symbolic_binding Self, 1 [symbolic = %Self.loc8_24.2 (constants.%Self.aa1)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   !members:
 // CHECK:STDOUT:     .Self = %Self.loc8_24.1
@@ -541,19 +559,19 @@ constraint Z {
 // CHECK:STDOUT: --- require_self_in_requirement.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
-// CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
-// CHECK:STDOUT:   %Self.861: %type = symbolic_binding Self, 0 [symbolic]
+// CHECK:STDOUT:   %Z.type: type = facet_type <@Z> [concrete]
+// CHECK:STDOUT:   %Self.861: %Z.type = symbolic_binding Self, 0 [symbolic]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: imports {
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
-// CHECK:STDOUT:   %Z.decl: type = constraint_decl @Z [concrete = constants.%type] {} {}
+// CHECK:STDOUT:   %Z.decl: type = constraint_decl @Z [concrete = constants.%Z.type] {} {}
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: constraint @Z {
-// CHECK:STDOUT:   %Self: %type = symbolic_binding Self, 0 [symbolic = constants.%Self.861]
+// CHECK:STDOUT:   %Self: %Z.type = symbolic_binding Self, 0 [symbolic = constants.%Self.861]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !members:
 // CHECK:STDOUT:   .Self = %Self

+ 76 - 33
toolchain/check/type_completion.cpp

@@ -12,10 +12,60 @@
 #include "toolchain/check/type.h"
 #include "toolchain/diagnostics/format_providers.h"
 #include "toolchain/sem_ir/ids.h"
+#include "toolchain/sem_ir/specific_named_constraint.h"
 #include "toolchain/sem_ir/typed_insts.h"
 
 namespace Carbon::Check {
 
+auto NoteIncompleteClass(Context& context, SemIR::ClassId class_id,
+                         DiagnosticBuilder& builder) -> void {
+  const auto& class_info = context.classes().Get(class_id);
+  CARBON_CHECK(!class_info.is_complete(), "Class is not incomplete");
+  if (class_info.has_definition_started()) {
+    CARBON_DIAGNOSTIC(ClassIncompleteWithinDefinition, Note,
+                      "class is incomplete within its definition");
+    builder.Note(class_info.definition_id, ClassIncompleteWithinDefinition);
+  } else {
+    CARBON_DIAGNOSTIC(ClassForwardDeclaredHere, Note,
+                      "class was forward declared here");
+    builder.Note(class_info.latest_decl_id(), ClassForwardDeclaredHere);
+  }
+}
+
+auto NoteIncompleteInterface(Context& context, SemIR::InterfaceId interface_id,
+                             DiagnosticBuilder& builder) -> void {
+  const auto& interface_info = context.interfaces().Get(interface_id);
+  CARBON_CHECK(!interface_info.is_complete(), "Interface is not incomplete");
+  if (interface_info.is_being_defined()) {
+    CARBON_DIAGNOSTIC(InterfaceIncompleteWithinDefinition, Note,
+                      "interface is currently being defined");
+    builder.Note(interface_info.definition_id,
+                 InterfaceIncompleteWithinDefinition);
+  } else {
+    CARBON_DIAGNOSTIC(InterfaceForwardDeclaredHere, Note,
+                      "interface was forward declared here");
+    builder.Note(interface_info.latest_decl_id(), InterfaceForwardDeclaredHere);
+  }
+}
+
+static auto NoteIncompleteNamedConstraint(
+    Context& context, SemIR::NamedConstraintId named_constraint_id,
+    DiagnosticBuilder& builder) -> void {
+  const auto& constraint = context.named_constraints().Get(named_constraint_id);
+  CARBON_CHECK(!constraint.is_complete(), "Named constraint is not incomplete");
+  if (constraint.is_being_defined()) {
+    CARBON_DIAGNOSTIC(NamedConstraintIncompleteWithinDefinition, Note,
+                      "constraint is currently being defined");
+    builder.Note(constraint.definition_id,
+                 NamedConstraintIncompleteWithinDefinition);
+  } else {
+    CARBON_DIAGNOSTIC(NamedConstraintForwardDeclaredHere, Note,
+                      "constraint was forward declared here");
+    builder.Note(constraint.latest_decl_id(),
+                 NamedConstraintForwardDeclaredHere);
+  }
+}
+
 namespace {
 // Worklist-based type completion mechanism.
 //
@@ -337,7 +387,12 @@ auto TypeCompleter::AddNestedIncompleteTypes(SemIR::Inst type_inst) -> bool {
       break;
     }
     case CARBON_KIND(SemIR::FacetType inst): {
-      auto identified_id = RequireIdentifiedFacetType(*context_, inst);
+      // TODO: Get the complete facet type here.
+      auto identified_id =
+          RequireIdentifiedFacetType(*context_, inst, diagnoser_);
+      if (!identified_id.has_value()) {
+        return false;
+      }
       const auto& identified =
           context_->identified_facet_types().Get(identified_id);
       // Every mentioned interface needs to be complete.
@@ -690,7 +745,8 @@ auto RequireConcreteType(Context& context, SemIR::TypeId type_id,
 }
 
 auto RequireIdentifiedFacetType(Context& context,
-                                const SemIR::FacetType& facet_type)
+                                const SemIR::FacetType& facet_type,
+                                MakeDiagnosticBuilderFn diagnoser)
     -> SemIR::IdentifiedFacetTypeId {
   if (auto identified_id =
           context.identified_facet_types().TryGetId(facet_type.facet_type_id);
@@ -700,6 +756,24 @@ auto RequireIdentifiedFacetType(Context& context,
   const auto& facet_type_info =
       context.facet_types().Get(facet_type.facet_type_id);
 
+  auto named_constraint_ids = llvm::map_range(
+      llvm::concat<const SemIR::SpecificNamedConstraint>(
+          facet_type_info.extend_named_constraints,
+          facet_type_info.self_impls_named_constraints),
+      [](SemIR::SpecificNamedConstraint s) { return s.named_constraint_id; });
+  for (auto named_constraint_id : named_constraint_ids) {
+    const auto& constraint =
+        context.named_constraints().Get(named_constraint_id);
+    if (!constraint.is_complete()) {
+      if (diagnoser) {
+        auto builder = diagnoser();
+        NoteIncompleteNamedConstraint(context, named_constraint_id, builder);
+        builder.Emit();
+      }
+      return SemIR::IdentifiedFacetTypeId::None;
+    }
+  }
+
   // TODO: expand named constraints
   // TODO: Process other kinds of requirements.
   return context.identified_facet_types().Add(
@@ -728,35 +802,4 @@ auto AsConcreteType(Context& context, SemIR::TypeId type_id,
              : SemIR::ErrorInst::TypeId;
 }
 
-auto NoteIncompleteClass(Context& context, SemIR::ClassId class_id,
-                         DiagnosticBuilder& builder) -> void {
-  const auto& class_info = context.classes().Get(class_id);
-  CARBON_CHECK(!class_info.is_complete(), "Class is not incomplete");
-  if (class_info.has_definition_started()) {
-    CARBON_DIAGNOSTIC(ClassIncompleteWithinDefinition, Note,
-                      "class is incomplete within its definition");
-    builder.Note(class_info.definition_id, ClassIncompleteWithinDefinition);
-  } else {
-    CARBON_DIAGNOSTIC(ClassForwardDeclaredHere, Note,
-                      "class was forward declared here");
-    builder.Note(class_info.latest_decl_id(), ClassForwardDeclaredHere);
-  }
-}
-
-auto NoteIncompleteInterface(Context& context, SemIR::InterfaceId interface_id,
-                             DiagnosticBuilder& builder) -> void {
-  const auto& interface_info = context.interfaces().Get(interface_id);
-  CARBON_CHECK(!interface_info.is_complete(), "Interface is not incomplete");
-  if (interface_info.is_being_defined()) {
-    CARBON_DIAGNOSTIC(InterfaceIncompleteWithinDefinition, Note,
-                      "interface is currently being defined");
-    builder.Note(interface_info.definition_id,
-                 InterfaceIncompleteWithinDefinition);
-  } else {
-    CARBON_DIAGNOSTIC(InterfaceForwardDeclaredHere, Note,
-                      "interface was forward declared here");
-    builder.Note(interface_info.latest_decl_id(), InterfaceForwardDeclaredHere);
-  }
-}
-
 }  // namespace Carbon::Check

+ 4 - 6
toolchain/check/type_completion.h

@@ -70,13 +70,11 @@ auto AsConcreteType(Context& context, SemIR::TypeId type_id,
     -> SemIR::TypeId;
 
 // Requires the named constraints in the facet type to be complete, so that the
-// set of interfaces the facet type requires is known. Since named constraints
-// are not yet supported, this currently never fails. Eventually this function
-// will be passed a diagnoser for facet types that use some incomplete named
-// constraint, and return `None` in that case. If not `None`, the result will be
-// present in context.identified_facet_type()`.
+// set of interfaces the facet type requires is known. Diagnoses an error and
+// returns None if any named constraint is not complete.
 auto RequireIdentifiedFacetType(Context& context,
-                                const SemIR::FacetType& facet_type)
+                                const SemIR::FacetType& facet_type,
+                                MakeDiagnosticBuilderFn diagnoser)
     -> SemIR::IdentifiedFacetTypeId;
 
 // Adds a note to a diagnostic explaining that a class is incomplete.

+ 9 - 2
toolchain/diagnostics/diagnostic_kind.def

@@ -312,6 +312,10 @@ CARBON_DIAGNOSTIC_KIND(ExportPrevious)
 CARBON_DIAGNOSTIC_KIND(InterfaceForwardDeclaredHere)
 CARBON_DIAGNOSTIC_KIND(InterfaceIncompleteWithinDefinition)
 
+// Named constraint checking.
+CARBON_DIAGNOSTIC_KIND(NamedConstraintForwardDeclaredHere)
+CARBON_DIAGNOSTIC_KIND(NamedConstraintIncompleteWithinDefinition)
+
 // Impl checking.
 CARBON_DIAGNOSTIC_KIND(AssociatedConstantHere)
 CARBON_DIAGNOSTIC_KIND(AssociatedFunctionHere)
@@ -327,12 +331,11 @@ CARBON_DIAGNOSTIC_KIND(ImplAsNonFacetType)
 CARBON_DIAGNOSTIC_KIND(ImplAsOutsideClass)
 CARBON_DIAGNOSTIC_KIND(ImplAssociatedConstantNeedsValue)
 CARBON_DIAGNOSTIC_KIND(ImplFunctionWithNonFunction)
-CARBON_DIAGNOSTIC_KIND(ImplLookupCycle)
-CARBON_DIAGNOSTIC_KIND(ImplLookupCycleNote)
 CARBON_DIAGNOSTIC_KIND(ImplMissingDefinition)
 CARBON_DIAGNOSTIC_KIND(ImplMissingFunction)
 CARBON_DIAGNOSTIC_KIND(ImplPreviousDefinition)
 CARBON_DIAGNOSTIC_KIND(ImplRedefinition)
+CARBON_DIAGNOSTIC_KIND(ImplOfUnidentifiedFacetType)
 CARBON_DIAGNOSTIC_KIND(ImplOfNotOneInterface)
 CARBON_DIAGNOSTIC_KIND(ImplUnusedBinding)
 CARBON_DIAGNOSTIC_KIND(PoisonedImplLookupConcreteResult)
@@ -351,11 +354,15 @@ CARBON_DIAGNOSTIC_KIND(FinalImplOverlapsDifferentFileNote)
 // Impl lookup.
 CARBON_DIAGNOSTIC_KIND(MissingImplInMemberAccess)
 CARBON_DIAGNOSTIC_KIND(MissingImplInMemberAccessNote)
+CARBON_DIAGNOSTIC_KIND(ImplLookupCycle)
+CARBON_DIAGNOSTIC_KIND(ImplLookupCycleNote)
+CARBON_DIAGNOSTIC_KIND(ImplLookupInIncompleteFacetType)
 
 // Require checking.
 CARBON_DIAGNOSTIC_KIND(RequireImplsMissingFacetType)
 CARBON_DIAGNOSTIC_KIND(RequireImplsMissingSelf)
 CARBON_DIAGNOSTIC_KIND(RequireInWrongScope)
+CARBON_DIAGNOSTIC_KIND(RequireImplsUnidentifiedFacetType)
 
 // Let declaration checking.
 CARBON_DIAGNOSTIC_KIND(ExpectedInitializerAfterLet)

+ 1 - 0
toolchain/sem_ir/BUILD

@@ -19,6 +19,7 @@ cc_library(
         "inst_kind.h",
         "singleton_insts.h",
         "specific_interface.h",
+        "specific_named_constraint.h",
         "typed_insts.h",
     ],
     textual_hdrs = ["inst_kind.def"],

+ 71 - 25
toolchain/sem_ir/facet_type_info.cpp

@@ -6,14 +6,21 @@
 
 #include <tuple>
 
+#include "toolchain/sem_ir/ids.h"
+
 namespace Carbon::SemIR {
 
 CARBON_DEFINE_ENUM_MASK_NAMES(BuiltinConstraintMask) {
   CARBON_BUILTIN_CONSTRAINT_MASK(CARBON_ENUM_MASK_NAME_STRING)
 };
 
-template <typename VecT, typename CompareT>
-static auto SortAndDeduplicate(VecT& vec, CompareT compare) -> void {
+template <typename T>
+using LessThanFn = llvm::function_ref<auto(const T&, const T&)->bool>;
+
+template <typename VecT>
+static auto SortAndDeduplicate(VecT& vec,
+                               LessThanFn<typename VecT::value_type> compare)
+    -> void {
   llvm::sort(vec, compare);
   vec.erase(llvm::unique(vec), vec.end());
 }
@@ -32,6 +39,13 @@ static auto RewriteLess(const FacetTypeInfo::RewriteConstraint& lhs,
          std::tie(rhs.lhs_id.index, rhs.rhs_id.index);
 }
 
+// Canonically ordered by the numerical ids.
+static auto NamedConstraintsLess(const SpecificNamedConstraint& lhs,
+                                 const SpecificNamedConstraint& rhs) -> bool {
+  return std::tie(lhs.named_constraint_id.index, lhs.specific_id.index) <
+         std::tie(rhs.named_constraint_id.index, rhs.specific_id.index);
+}
+
 // Canonically ordered by the numerical ids.
 static auto RequiredLess(const IdentifiedFacetType::RequiredInterface& lhs,
                          const IdentifiedFacetType::RequiredInterface& rhs)
@@ -42,21 +56,21 @@ static auto RequiredLess(const IdentifiedFacetType::RequiredInterface& lhs,
 
 // Assuming both `a` and `b` are sorted and deduplicated, replaces `a` with `a -
 // b` as sets. Assumes there are few elements between them.
-static auto SubtractSorted(
-    llvm::SmallVector<FacetTypeInfo::ImplsConstraint>& a,
-    const llvm::SmallVector<FacetTypeInfo::ImplsConstraint>& b) -> void {
-  using Iter = llvm::SmallVector<FacetTypeInfo::ImplsConstraint>::iterator;
+template <typename VecT>
+static auto SubtractSorted(VecT& a, const VecT& b,
+                           LessThanFn<typename VecT::value_type> compare)
+    -> void {
+  using Iter = VecT::iterator;
   Iter a_iter = a.begin();
   Iter a_end = a.end();
-  using ConstIter =
-      llvm::SmallVector<FacetTypeInfo::ImplsConstraint>::const_iterator;
+  using ConstIter = VecT::const_iterator;
   ConstIter b_iter = b.begin();
   ConstIter b_end = b.end();
   // Advance the iterator pointing to the smaller element until we find a match.
   while (a_iter != a_end && b_iter != b_end) {
-    if (ImplsLess(*a_iter, *b_iter)) {
+    if (compare(*a_iter, *b_iter)) {
       ++a_iter;
-    } else if (ImplsLess(*b_iter, *a_iter)) {
+    } else if (compare(*b_iter, *a_iter)) {
       ++b_iter;
     } else {
       break;
@@ -74,11 +88,11 @@ static auto SubtractSorted(
   ++a_iter;
   ++b_iter;
   while (a_iter != a_end && b_iter != b_end) {
-    if (ImplsLess(*a_iter, *b_iter)) {
+    if (compare(*a_iter, *b_iter)) {
       *a_new_end = *a_iter;
       ++a_new_end;
       ++a_iter;
-    } else if (ImplsLess(*b_iter, *a_iter)) {
+    } else if (compare(*b_iter, *a_iter)) {
       ++b_iter;
     } else {
       CARBON_DCHECK(*a_iter == *b_iter);
@@ -96,21 +110,27 @@ static auto SubtractSorted(
   a.erase(a_new_end, a_end);
 }
 
+template <typename VecT>
+static auto CombineVectors(VecT& vec, const VecT& lhs, const VecT& rhs) {
+  vec.reserve(lhs.size() + rhs.size());
+  llvm::append_range(vec,
+                     llvm::concat<const typename VecT::value_type>(lhs, rhs));
+}
+
 auto FacetTypeInfo::Combine(const FacetTypeInfo& lhs, const FacetTypeInfo& rhs)
     -> FacetTypeInfo {
   FacetTypeInfo info;
-  info.extend_constraints.reserve(lhs.extend_constraints.size() +
-                                  rhs.extend_constraints.size());
-  llvm::append_range(info.extend_constraints, lhs.extend_constraints);
-  llvm::append_range(info.extend_constraints, rhs.extend_constraints);
-  info.self_impls_constraints.reserve(lhs.self_impls_constraints.size() +
-                                      rhs.self_impls_constraints.size());
-  llvm::append_range(info.self_impls_constraints, lhs.self_impls_constraints);
-  llvm::append_range(info.self_impls_constraints, rhs.self_impls_constraints);
-  info.rewrite_constraints.reserve(lhs.rewrite_constraints.size() +
-                                   rhs.rewrite_constraints.size());
-  llvm::append_range(info.rewrite_constraints, lhs.rewrite_constraints);
-  llvm::append_range(info.rewrite_constraints, rhs.rewrite_constraints);
+  CombineVectors(info.extend_constraints, lhs.extend_constraints,
+                 rhs.extend_constraints);
+  CombineVectors(info.self_impls_constraints, lhs.self_impls_constraints,
+                 rhs.self_impls_constraints);
+  CombineVectors(info.extend_named_constraints, lhs.extend_named_constraints,
+                 rhs.extend_named_constraints);
+  CombineVectors(info.self_impls_named_constraints,
+                 lhs.self_impls_named_constraints,
+                 rhs.self_impls_named_constraints);
+  CombineVectors(info.rewrite_constraints, lhs.rewrite_constraints,
+                 rhs.rewrite_constraints);
   info.builtin_constraint_mask =
       lhs.builtin_constraint_mask | rhs.builtin_constraint_mask;
   info.other_requirements = lhs.other_requirements || rhs.other_requirements;
@@ -120,7 +140,11 @@ auto FacetTypeInfo::Combine(const FacetTypeInfo& lhs, const FacetTypeInfo& rhs)
 auto FacetTypeInfo::Canonicalize() -> void {
   SortAndDeduplicate(extend_constraints, ImplsLess);
   SortAndDeduplicate(self_impls_constraints, ImplsLess);
-  SubtractSorted(self_impls_constraints, extend_constraints);
+  SubtractSorted(self_impls_constraints, extend_constraints, ImplsLess);
+  SortAndDeduplicate(extend_named_constraints, NamedConstraintsLess);
+  SortAndDeduplicate(self_impls_named_constraints, NamedConstraintsLess);
+  SubtractSorted(self_impls_named_constraints, extend_named_constraints,
+                 NamedConstraintsLess);
   SortAndDeduplicate(rewrite_constraints, RewriteLess);
 }
 
@@ -158,6 +182,28 @@ auto FacetTypeInfo::Print(llvm::raw_ostream& out) const -> void {
     }
   }
 
+  if (!extend_named_constraints.empty()) {
+    out << outer_sep << "extends named constraint: ";
+    llvm::ListSeparator sep;
+    for (auto extend : extend_named_constraints) {
+      out << sep << extend.named_constraint_id;
+      if (extend.specific_id.has_value()) {
+        out << "(" << extend.specific_id << ")";
+      }
+    }
+  }
+
+  if (!self_impls_constraints.empty()) {
+    out << outer_sep << "self impls named constraint: ";
+    llvm::ListSeparator sep;
+    for (auto self_impls : self_impls_named_constraints) {
+      out << sep << self_impls.named_constraint_id;
+      if (self_impls.specific_id.has_value()) {
+        out << "(" << self_impls.specific_id << ")";
+      }
+    }
+  }
+
   if (!builtin_constraint_mask.empty()) {
     out << outer_sep << "builtin_constraint_mask: " << builtin_constraint_mask;
   }

+ 21 - 5
toolchain/sem_ir/facet_type_info.h

@@ -11,6 +11,7 @@
 #include "toolchain/base/canonical_value_store.h"
 #include "toolchain/sem_ir/ids.h"
 #include "toolchain/sem_ir/specific_interface.h"
+#include "toolchain/sem_ir/specific_named_constraint.h"
 
 namespace Carbon::SemIR {
 
@@ -63,6 +64,12 @@ struct FacetTypeInfo : Printable<FacetTypeInfo> {
   // These are the required interfaces that are not lookup contexts.
   llvm::SmallVector<ImplsConstraint> self_impls_constraints;
 
+  // These name constraints add interfaces as lookup contexts, if they are
+  // extended in the named constraint.
+  llvm::SmallVector<SpecificNamedConstraint> extend_named_constraints;
+  // These name constraints don't add interfaces as lookup contexts.
+  llvm::SmallVector<SpecificNamedConstraint> self_impls_named_constraints;
+
   // Rewrite constraints of the form `.T = U`.
   //
   // The InstIds here must be canonical instructions (which come from the
@@ -98,8 +105,9 @@ struct FacetTypeInfo : Printable<FacetTypeInfo> {
   // 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() &&
-        rewrite_constraints.empty() && builtin_constraint_mask.empty() &&
-        !other_requirements) {
+        extend_named_constraints.empty() &&
+        self_impls_named_constraints.empty() && rewrite_constraints.empty() &&
+        builtin_constraint_mask.empty() && !other_requirements) {
       return extend_constraints.front();
     }
     return std::nullopt;
@@ -109,6 +117,9 @@ struct FacetTypeInfo : Printable<FacetTypeInfo> {
       -> bool {
     return lhs.extend_constraints == rhs.extend_constraints &&
            lhs.self_impls_constraints == rhs.self_impls_constraints &&
+           lhs.extend_named_constraints == rhs.extend_named_constraints &&
+           lhs.self_impls_named_constraints ==
+               rhs.self_impls_named_constraints &&
            lhs.rewrite_constraints == rhs.rewrite_constraints &&
            lhs.builtin_constraint_mask == rhs.builtin_constraint_mask &&
            lhs.other_requirements == rhs.other_requirements;
@@ -179,14 +190,19 @@ struct IdentifiedFacetType {
 inline auto CarbonHashValue(const FacetTypeInfo& value, uint64_t seed)
     -> HashCode {
   Hasher hasher(seed);
-  hasher.HashSizedBytes(llvm::ArrayRef(value.extend_constraints));
-  hasher.HashSizedBytes(llvm::ArrayRef(value.self_impls_constraints));
-  hasher.HashSizedBytes(llvm::ArrayRef(value.rewrite_constraints));
+  hasher.HashArray(llvm::ArrayRef(value.extend_constraints));
+  hasher.HashArray(llvm::ArrayRef(value.self_impls_constraints));
+  hasher.HashArray(llvm::ArrayRef(value.extend_named_constraints));
+  hasher.HashArray(llvm::ArrayRef(value.self_impls_named_constraints));
+  hasher.HashArray(llvm::ArrayRef(value.rewrite_constraints));
   hasher.HashRaw(value.builtin_constraint_mask);
   hasher.HashRaw(value.other_requirements);
   return static_cast<HashCode>(hasher);
 }
 
+// Declared:
+// (Carbon::HashCode)  (value_ = 12557349131240970624)
+
 }  // namespace Carbon::SemIR
 
 #endif  // CARBON_TOOLCHAIN_SEM_IR_FACET_TYPE_INFO_H_

+ 28 - 10
toolchain/sem_ir/formatter.cpp

@@ -1340,15 +1340,24 @@ auto Formatter::FormatArg(FacetTypeId id) -> void {
   out_ << "<";
 
   llvm::ListSeparator sep(" & ");
-  if (info.extend_constraints.empty()) {
+  if (info.extend_constraints.empty() &&
+      info.extend_named_constraints.empty()) {
     out_ << "type";
   } else {
-    for (auto interface : info.extend_constraints) {
+    for (auto extend : info.extend_constraints) {
       out_ << sep;
-      FormatName(interface.interface_id);
-      if (interface.specific_id.has_value()) {
+      FormatName(extend.interface_id);
+      if (extend.specific_id.has_value()) {
         out_ << ", ";
-        FormatName(interface.specific_id);
+        FormatName(extend.specific_id);
+      }
+    }
+    for (auto extend : info.extend_named_constraints) {
+      out_ << sep;
+      FormatName(extend.named_constraint_id);
+      if (extend.specific_id.has_value()) {
+        out_ << ", ";
+        FormatName(extend.specific_id);
       }
     }
   }
@@ -1358,15 +1367,24 @@ auto Formatter::FormatArg(FacetTypeId id) -> void {
       !info.rewrite_constraints.empty()) {
     out_ << " where ";
     llvm::ListSeparator and_sep(" and ");
-    if (!info.self_impls_constraints.empty()) {
+    if (!info.self_impls_constraints.empty() ||
+        !info.self_impls_named_constraints.empty()) {
       out_ << and_sep << ".Self impls ";
       llvm::ListSeparator amp_sep(" & ");
-      for (auto interface : info.self_impls_constraints) {
+      for (auto self_impls : info.self_impls_constraints) {
+        out_ << amp_sep;
+        FormatName(self_impls.interface_id);
+        if (self_impls.specific_id.has_value()) {
+          out_ << ", ";
+          FormatName(self_impls.specific_id);
+        }
+      }
+      for (auto self_impls : info.self_impls_named_constraints) {
         out_ << amp_sep;
-        FormatName(interface.interface_id);
-        if (interface.specific_id.has_value()) {
+        FormatName(self_impls.named_constraint_id);
+        if (self_impls.specific_id.has_value()) {
           out_ << ", ";
-          FormatName(interface.specific_id);
+          FormatName(self_impls.specific_id);
         }
       }
     }

+ 11 - 2
toolchain/sem_ir/inst_namer.cpp

@@ -893,12 +893,21 @@ auto InstNamer::NamingContext::NameInst() -> void {
       bool has_where = facet_type_info.other_requirements ||
                        !facet_type_info.builtin_constraint_mask.empty() ||
                        !facet_type_info.self_impls_constraints.empty() ||
+                       !facet_type_info.self_impls_named_constraints.empty() ||
                        !facet_type_info.rewrite_constraints.empty();
-      if (facet_type_info.extend_constraints.size() == 1) {
+      if (facet_type_info.extend_constraints.size() == 1 &&
+          facet_type_info.extend_named_constraints.empty()) {
         AddEntityNameAndMaybePush(
             facet_type_info.extend_constraints.front().interface_id,
             has_where ? "_where.type" : ".type");
-      } else if (facet_type_info.extend_constraints.empty()) {
+      } else if (facet_type_info.extend_named_constraints.size() == 1 &&
+                 facet_type_info.extend_constraints.empty()) {
+        AddEntityNameAndMaybePush(
+            facet_type_info.extend_named_constraints.front()
+                .named_constraint_id,
+            has_where ? "_where.type" : ".type");
+      } else if (facet_type_info.extend_constraints.empty() &&
+                 facet_type_info.extend_named_constraints.empty()) {
         AddInstName(has_where ? "type_where" : "type");
       } else {
         AddInstName("facet_type");

+ 2 - 2
toolchain/sem_ir/specific_interface.h

@@ -14,11 +14,11 @@ namespace Carbon::SemIR {
 struct SpecificInterface {
   using DiagnosticType = Diagnostics::TypeInfo<std::string>;
 
+  static const SpecificInterface None;
+
   InterfaceId interface_id;
   SpecificId specific_id;
 
-  static const SpecificInterface None;
-
   friend auto operator==(const SpecificInterface& lhs,
                          const SpecificInterface& rhs) -> bool = default;
 };

+ 24 - 0
toolchain/sem_ir/specific_named_constraint.h

@@ -0,0 +1,24 @@
+// 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_SEM_IR_SPECIFIC_NAMED_CONSTRAINT_H_
+#define CARBON_TOOLCHAIN_SEM_IR_SPECIFIC_NAMED_CONSTRAINT_H_
+
+#include "toolchain/base/canonical_value_store.h"
+#include "toolchain/sem_ir/ids.h"
+
+namespace Carbon::SemIR {
+
+// A pair of a named constraint and a specific for that named constraint.
+struct SpecificNamedConstraint {
+  NamedConstraintId named_constraint_id;
+  SpecificId specific_id;
+
+  friend auto operator==(const SpecificNamedConstraint& lhs,
+                         const SpecificNamedConstraint& rhs) -> bool = default;
+};
+
+}  // namespace Carbon::SemIR
+
+#endif  // CARBON_TOOLCHAIN_SEM_IR_SPECIFIC_NAMED_CONSTRAINT_H_

+ 32 - 10
toolchain/sem_ir/stringify.cpp

@@ -58,10 +58,10 @@ class StepStack {
 
   // The full set of things which can be pushed, including all members of
   // `Step`.
-  using PushItem =
-      std::variant<InstId, llvm::StringRef, NameId, ElementIndex,
-                   QualifiedNameItem, EntityNameItem, EntityNameId, TypeId,
-                   SpecificInterface, llvm::ListSeparator*>;
+  using PushItem = std::variant<InstId, llvm::StringRef, NameId, ElementIndex,
+                                QualifiedNameItem, EntityNameItem, EntityNameId,
+                                SpecificNamedConstraint, SpecificInterface,
+                                TypeId, llvm::ListSeparator*>;
 
   // Starts a new stack, which always contains the first instruction to
   // stringify.
@@ -109,12 +109,20 @@ class StepStack {
     PushInstId(sem_ir_->types().GetInstId(type_id));
   }
 
-  // Pushes a specific interface.
+  // Pushes a specific interface by the interface's entity name.
   auto PushSpecificInterface(SpecificInterface specific_interface) -> void {
     PushEntityName(sem_ir_->interfaces().Get(specific_interface.interface_id),
                    specific_interface.specific_id);
   }
 
+  // Pushes a specific named constraint by the constraint's entity name.
+  auto PushSpecificNamedConstraint(
+      SpecificNamedConstraint specific_named_constraint) -> void {
+    PushEntityName(sem_ir_->named_constraints().Get(
+                       specific_named_constraint.named_constraint_id),
+                   specific_named_constraint.specific_id);
+  }
+
   // Pushes a sequence of items onto the stack. This handles reversal, such that
   // the caller can pass items in print order instead of stack order.
   //
@@ -160,6 +168,10 @@ class StepStack {
           PushSpecificInterface(specific_interface);
           break;
         }
+        case CARBON_KIND(SpecificNamedConstraint specific_named_constraint): {
+          PushSpecificNamedConstraint(specific_named_constraint);
+          break;
+        }
         case CARBON_KIND(llvm::ListSeparator * sep): {
           PushString(*sep);
           break;
@@ -345,11 +357,16 @@ class Stringifier {
       step_stack_->Push(" ", rewrite.lhs_id, " = ", rewrite.rhs_id);
       some_where = true;
     }
-    if (!facet_type_info.self_impls_constraints.empty()) {
+    if (!facet_type_info.self_impls_constraints.empty() ||
+        !facet_type_info.self_impls_named_constraints.empty()) {
       if (some_where) {
         step_stack_->PushString(" and");
       }
       llvm::ListSeparator sep(" & ");
+      for (auto impls :
+           llvm::reverse(facet_type_info.self_impls_named_constraints)) {
+        step_stack_->Push(impls, &sep);
+      }
       for (auto impls : llvm::reverse(facet_type_info.self_impls_constraints)) {
         step_stack_->Push(impls, &sep);
       }
@@ -361,14 +378,19 @@ class Stringifier {
       step_stack_->PushString(" where");
     }
 
-    // Output extend interface requirements.
-    if (facet_type_info.extend_constraints.empty()) {
+    // Output extend interface and named constraint requirements.
+    if (facet_type_info.extend_constraints.empty() &&
+        facet_type_info.extend_named_constraints.empty()) {
       step_stack_->PushString("type");
       return;
     }
     llvm::ListSeparator sep(" & ");
-    for (auto impls : llvm::reverse(facet_type_info.extend_constraints)) {
-      step_stack_->Push(impls, &sep);
+    for (auto extend :
+         llvm::reverse(facet_type_info.extend_named_constraints)) {
+      step_stack_->Push(extend, &sep);
+    }
+    for (auto extend : llvm::reverse(facet_type_info.extend_constraints)) {
+      step_stack_->Push(extend, &sep);
     }
   }