Przeglądaj źródła

Add `where T impls X` constraints into the FacetTypeInfo (#7038)

This makes them part of the identified facet type, and we can see the
constraints as part of stringify and format output.

But this does not do enough to make them useful yet: Any `T impls X`
constraint must contain a reference to `.Self` somewhere. And `.Self`
references do not get substituted, so neither `T(.Self) impls X` and `T
impls X(.Self)` will match against an incoming facet value derived from
an `impl T(U) as X` or `impl T as X(U)`, since `U` and `.Self` are never
the same thing until `.Self` can be substituted.

Now that impl lookup runs into facet values containing `.Self` (a
symbolic binding), such as in `C(.Self)`, we were crashing assuming the
type of `.Self` is a FacetType, but it can be `type` in the case of
`type where C(.Self) impls...`. Instead, use an empty facet type for the
type of `.Self` so it is always a facet. This assists with substituting
other facets into it, without having to insert an extra FacetAccessType.
`MakePeriodSelfFacetValue()` now enforces this requirement.

---------

Co-authored-by: Richard Smith <richard@metafoo.co.uk>
Dana Jansens 3 tygodni temu
rodzic
commit
cc5a42691e

+ 96 - 22
toolchain/check/eval.cpp

@@ -36,6 +36,7 @@
 #include "toolchain/sem_ir/impl.h"
 #include "toolchain/sem_ir/inst_categories.h"
 #include "toolchain/sem_ir/inst_kind.h"
+#include "toolchain/sem_ir/specific_named_constraint.h"
 #include "toolchain/sem_ir/typed_insts.h"
 
 namespace Carbon::Check {
@@ -2633,36 +2634,109 @@ static auto AddRequirementImpls(Context& context, SemIR::RequirementImpls impls,
     return;
   }
 
+  auto facet_type = context.insts().GetAs<SemIR::FacetType>(rhs_id);
+  const auto& rhs = context.facet_types().Get(facet_type.facet_type_id);
+
   if (IsSameFacetValue(context, context.constant_values().Get(lhs_id),
                        period_self_id)) {
-    auto facet_type = context.insts().GetAs<SemIR::FacetType>(rhs_id);
-    const auto& more_info = context.facet_types().Get(facet_type.facet_type_id);
-    // The way to prevent lookup into the interface requirements of a
-    // facet type is to put it to the right of a `.Self impls`, which we
-    // accomplish by putting them into `self_impls_constraints`.
-    llvm::append_range(info->self_impls_constraints,
-                       more_info.extend_constraints);
+    // A facet type with `.Self impls <RHS facet type>`. Whatever the RHS facet
+    // type constrains for `.Self` gets forwarded to the output facet type to
+    // also constrain `.Self`. Nothing on the RHS of `impls` can extend the
+    // resulting facet type.
+    llvm::append_range(info->self_impls_constraints, rhs.extend_constraints);
     llvm::append_range(info->self_impls_constraints,
-                       more_info.self_impls_constraints);
+                       rhs.self_impls_constraints);
     llvm::append_range(info->self_impls_named_constraints,
-                       more_info.extend_named_constraints);
+                       rhs.extend_named_constraints);
     llvm::append_range(info->self_impls_named_constraints,
-                       more_info.self_impls_named_constraints);
-    // If `.Self impls Z` and Z implies `C impls Y`, then the facet type
-    // of `.Self` also knows `C impls Y`.
-    llvm::append_range(info->type_impls_interfaces,
-                       more_info.type_impls_interfaces);
+                       rhs.self_impls_named_constraints);
+    llvm::append_range(info->type_impls_interfaces, rhs.type_impls_interfaces);
     llvm::append_range(info->type_impls_named_constraints,
-                       more_info.type_impls_named_constraints);
-    // Other requirements are copied in.
-    llvm::append_range(info->rewrite_constraints,
-                       more_info.rewrite_constraints);
-    info->other_requirements |= more_info.other_requirements;
-    return;
+                       rhs.type_impls_named_constraints);
+  } else {
+    // Consider `I where C(.Self) impls (J(.Self) where .Self impls K(.Self))`,
+    // when we are evaluating the `C(.Self) impls (<facet type>)` requirement.
+    // The <facet type> is our `rhs` here, and it will contain:
+    // * extend constraint: J(.Self)
+    // * self impls constraint: K(.Self)
+    //
+    // The value of `.Self` changes where we cross a `where` operator. This
+    // means extend constraints retain their original `.Self`, but self impls
+    // constraints should have their `.Self` replaced by the LHS of the impls
+    // requirement.
+    //
+    // However that is not quite enough. The view of the LHS of the impls
+    // requirement should be a facet with a facet type of the RHS extend
+    // constraints. In this case the LHS is C(.Self) and the RHS facet type is
+    // `J(.Self) where .Self impls K(.Self)`. The RHS facet type has impls
+    // constraints (which are on the RHS of a `where` operator), in which their
+    // `.Self` should be replaced by `C(.Self)` converted to the RHS facet
+    // type's extend constraints (which are on the LHS of a `where` operator),
+    // which is `C(.Self) as J(.Self)`. It should be enough to convert the LHS
+    // type to the type of the `.Self` that it is replacing, as that contains
+    // the extend constraints.
+    //
+    // So the final RHS facet type to be merged into `info` is:
+    //
+    // `J(.Self) where (C(.Self) as J(.Self)) impls K(C(.Self) as J(.Self))`.
+
+    auto lhs_facet_or_type = GetCanonicalFacetOrTypeValue(context, lhs_id);
+
+    auto impls_interface = [&](SemIR::SpecificInterface si)
+        -> SemIR::FacetTypeInfo::TypeImplsInterface {
+      return {lhs_facet_or_type, si};
+    };
+    auto impls_constraint = [&](SemIR::SpecificNamedConstraint sc)
+        -> SemIR::FacetTypeInfo::TypeImplsNamedConstraint {
+      return {lhs_facet_or_type, sc};
+    };
+
+    // Extend constraints are copied over without replacing anything, but are
+    // converted to type impls constraints so they apply to the LHS type.
+    llvm::append_range(
+        info->type_impls_interfaces,
+        llvm::map_range(rhs.extend_constraints, impls_interface));
+    llvm::append_range(
+        info->type_impls_named_constraints,
+        llvm::map_range(rhs.extend_named_constraints, impls_constraint));
+
+    // To replace the `.Self` in `.Self impls X` we convert from a self impls
+    // constraint to a type impls constraint where the type is the impls LHS
+    // type. We must also replace any `.Self` references in the constraint in
+    // the same way. The LHS type needs to be converted to a facet with its type
+    // containing the RHS facet type's extend constraints so that the extend
+    // constraints can be referenced in impls constraints.
+    //
+    // TODO: Convert the LHS used in the TypeImplsNamedConstraint to a facet
+    // with the RHS extend constraints (interfaces and named constraints).
+    //
+    // TODO: Replace `.Self` with the LHS type as a facet with the RHS extend
+    // constraints.
+    llvm::append_range(
+        info->type_impls_interfaces,
+        llvm::map_range(rhs.self_impls_constraints, impls_interface));
+    llvm::append_range(
+        info->type_impls_named_constraints,
+        llvm::map_range(rhs.self_impls_named_constraints, impls_constraint));
+
+    // Type impls constraints are copied in, but need to have their `.Self`
+    // references replaced by the impls LHS type. Like above, the LHS type
+    // should be converted to a facet type containing the RHS facet type's
+    // extend constraints.
+    //
+    // TODO: Convert the LHS used in the TypeImplsNamedConstraint to a facet
+    // with the RHS extend constraints (interfaces and named constraints).
+    //
+    // TODO: Replace `.Self` with the LHS type as a facet with the RHS extend
+    // constraints.
+    llvm::append_range(info->type_impls_interfaces, rhs.type_impls_interfaces);
+    llvm::append_range(info->type_impls_named_constraints,
+                       rhs.type_impls_named_constraints);
   }
 
-  // TODO: Handle `impls` constraints beyond `.Self impls`.
-  info->other_requirements = true;
+  // Other requirements are copied in.
+  llvm::append_range(info->rewrite_constraints, rhs.rewrite_constraints);
+  info->other_requirements |= rhs.other_requirements;
 }
 
 // Add the constraints from the WhereExpr instruction into a FacetTypeInfo in

+ 2 - 0
toolchain/check/facet_type.cpp

@@ -403,6 +403,8 @@ auto ResolveFacetTypeRewriteConstraints(
 
 auto MakePeriodSelfFacetValue(Context& context, SemIR::TypeId self_type_id)
     -> SemIR::InstId {
+  CARBON_CHECK(self_type_id == SemIR::ErrorInst::TypeId ||
+               context.types().Is<SemIR::FacetType>(self_type_id));
   auto entity_name_id = context.entity_names().AddCanonical({
       .name_id = SemIR::NameId::PeriodSelf,
       .parent_scope_id = context.scope_stack().PeekNameScopeId(),

+ 4 - 2
toolchain/check/facet_type.h

@@ -64,8 +64,10 @@ auto ResolveFacetTypeRewriteConstraints(
 // Introduce `.Self` as a symbolic binding into the current scope, and return
 // the `SymbolicBinding` instruction.
 //
-// The `self_type_id` is either a facet type (as `FacetType`) or `type` (as
-// `TypeType`).
+// The type of `.Self` must be a `FacetType`, so that it gets wrapped in
+// `FacetAccessType` when used in a type position, such as in `U:! I(.Self)`.
+// This allows substitution with other facet values without requiring an
+// additional `FacetAccessType` to be inserted.
 auto MakePeriodSelfFacetValue(Context& context, SemIR::TypeId self_type_id)
     -> SemIR::InstId;
 

+ 1 - 8
toolchain/check/handle_binding_pattern.cpp

@@ -404,14 +404,7 @@ auto HandleParseNode(Context& context,
   // compile time binding. This is popped when handling the
   // CompileTimeBindingPatternId.
   context.scope_stack().PushForSameRegion();
-
-  // The `.Self` must have a type of `FacetType`, so that it gets wrapped in
-  // `FacetAccessType` when used in a type position, such as in `U:! I(.Self)`.
-  // This allows substitution with other facet values without requiring an
-  // additional `FacetAccessType` to be inserted.
-  auto type_id = GetEmptyFacetType(context);
-
-  MakePeriodSelfFacetValue(context, type_id);
+  MakePeriodSelfFacetValue(context, GetEmptyFacetType(context));
   return true;
 }
 

+ 12 - 5
toolchain/check/handle_where.cpp

@@ -41,15 +41,22 @@ auto HandleParseNode(Context& context, Parse::WhereOperandId node_id) -> bool {
   // Any references to `.Self` in constraints for the current `WhereExpr` will
   // not see constraints in the `Self` facet type, but they will resolve to
   // values through the constraints explicitly when they are combined together.
-  auto self_without_constraints_type_id = self_with_constraints_type_id;
-  if (auto facet_type = context.types().TryGetAs<SemIR::FacetType>(
-          self_without_constraints_type_id)) {
+  auto period_self_type_id = self_with_constraints_type_id;
+  if (auto facet_type =
+          context.types().TryGetAs<SemIR::FacetType>(period_self_type_id)) {
     const auto& info = context.facet_types().Get(facet_type->facet_type_id);
     // TODO: Missing named constraints here.
     auto stripped_info =
         SemIR::FacetTypeInfo{.extend_constraints = info.extend_constraints};
     stripped_info.Canonicalize();
-    self_without_constraints_type_id = GetFacetType(context, stripped_info);
+    period_self_type_id = GetFacetType(context, stripped_info);
+  } else if (period_self_type_id == SemIR::TypeType::TypeId) {
+    // The self may be `TypeType` in `type where X impls Y`, so we use an empty
+    // facet type.
+    period_self_type_id = GetEmptyFacetType(context);
+  } else {
+    CARBON_CHECK(period_self_type_id == SemIR::ErrorInst::TypeId,
+                 "unexpected .Self type {0}", period_self_type_id);
   }
 
   // Introduce a name scope so that we can remove the `.Self` entry we are
@@ -58,7 +65,7 @@ auto HandleParseNode(Context& context, Parse::WhereOperandId node_id) -> bool {
   // Introduce `.Self` as a symbolic binding. Its type is the value of the
   // expression to the left of `where`, so `MyInterface` in the example above.
   auto period_self_inst_id =
-      MakePeriodSelfFacetValue(context, self_without_constraints_type_id);
+      MakePeriodSelfFacetValue(context, period_self_type_id);
 
   // Save the `.Self` symbolic binding on the node stack. It will become the
   // first argument to the `WhereExpr` instruction.

+ 46 - 44
toolchain/check/testdata/deduce/binding_pattern.carbon

@@ -257,7 +257,7 @@ fn F(unused U:! type, V:! type where {} impls Core.ImplicitAs(.Self)) {
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
 // CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
-// CHECK:STDOUT:   %.Self.c39: %type = symbolic_binding .Self [symbolic_self]
+// CHECK:STDOUT:   %.Self: %type = symbolic_binding .Self [symbolic_self]
 // CHECK:STDOUT:   %pattern_type.98f: type = pattern_type type [concrete]
 // CHECK:STDOUT:   %T: type = symbolic_binding T, 0 [symbolic]
 // CHECK:STDOUT:   %C.type: type = generic_class_type @C [concrete]
@@ -271,7 +271,6 @@ fn F(unused U:! type, V:! type where {} impls Core.ImplicitAs(.Self)) {
 // CHECK:STDOUT:   %complete_type: <witness> = complete_type_witness %empty_struct_type [concrete]
 // CHECK:STDOUT:   %require_complete.944: <witness> = require_complete_type %T [symbolic]
 // CHECK:STDOUT:   %U: type = symbolic_binding U, 0 [symbolic]
-// CHECK:STDOUT:   %.Self.16f: type = symbolic_binding .Self [symbolic_self]
 // CHECK:STDOUT:   %empty_struct: %empty_struct_type = struct_value () [concrete]
 // CHECK:STDOUT:   %ImplicitAs.type.cc7: type = generic_interface_type @ImplicitAs [concrete]
 // CHECK:STDOUT:   %ImplicitAs.generic: %ImplicitAs.type.cc7 = struct_value () [concrete]
@@ -281,24 +280,25 @@ fn F(unused U:! type, V:! type where {} impls Core.ImplicitAs(.Self)) {
 // CHECK:STDOUT:   %ImplicitAs.assoc_type.ff3: type = assoc_entity_type @ImplicitAs, @ImplicitAs(%Dest) [symbolic]
 // CHECK:STDOUT:   %ImplicitAs.WithSelf.Convert.type.b3a: type = fn_type @ImplicitAs.WithSelf.Convert, @ImplicitAs.WithSelf(%Dest, %Self.738) [symbolic]
 // CHECK:STDOUT:   %ImplicitAs.WithSelf.Convert.1de: %ImplicitAs.WithSelf.Convert.type.b3a = struct_value () [symbolic]
-// CHECK:STDOUT:   %ImplicitAs.type.f60: type = facet_type <@ImplicitAs, @ImplicitAs(%.Self.16f)> [symbolic_self]
-// CHECK:STDOUT:   %type_where: type = facet_type <type where TODO> [concrete]
-// CHECK:STDOUT:   %pattern_type.354: type = pattern_type %type_where [concrete]
+// CHECK:STDOUT:   %.Self.binding.as_type: type = symbolic_binding_type .Self, %.Self [symbolic_self]
+// CHECK:STDOUT:   %ImplicitAs.type.164: type = facet_type <@ImplicitAs, @ImplicitAs(%.Self.binding.as_type)> [symbolic_self]
+// CHECK:STDOUT:   %type_where: type = facet_type <type where %empty_struct_type impls @ImplicitAs, @ImplicitAs(%.Self.binding.as_type)> [symbolic_self]
+// CHECK:STDOUT:   %pattern_type.9a5: type = pattern_type %type_where [symbolic_self]
 // CHECK:STDOUT:   %V: %type_where = symbolic_binding V, 1 [symbolic]
 // CHECK:STDOUT:   %F.type: type = fn_type @F [concrete]
 // CHECK:STDOUT:   %F: %F.type = struct_value () [concrete]
 // CHECK:STDOUT:   %V.binding.as_type: type = symbolic_binding_type V, 1, %V [symbolic]
-// CHECK:STDOUT:   %C.bca: type = class_type @C, @C(%V.binding.as_type) [symbolic]
-// CHECK:STDOUT:   %C.Create.type.242: type = fn_type @C.Create, @C(%V.binding.as_type) [symbolic]
-// CHECK:STDOUT:   %C.Create.206: %C.Create.type.242 = struct_value () [symbolic]
-// CHECK:STDOUT:   %require_complete.232: <witness> = require_complete_type %C.bca [symbolic]
-// CHECK:STDOUT:   %pattern_type.20b: type = pattern_type %V.binding.as_type [symbolic]
-// CHECK:STDOUT:   %C.Create.specific_fn: <specific function> = specific_function %C.Create.206, @C.Create(%V.binding.as_type) [symbolic]
-// CHECK:STDOUT:   %require_complete.94b: <witness> = require_complete_type %V.binding.as_type [symbolic]
-// CHECK:STDOUT:   %ImplicitAs.type.ee4: type = facet_type <@ImplicitAs, @ImplicitAs(%V.binding.as_type)> [symbolic]
-// CHECK:STDOUT:   %ImplicitAs.assoc_type.f30: type = assoc_entity_type @ImplicitAs, @ImplicitAs(%V.binding.as_type) [symbolic]
-// CHECK:STDOUT:   %assoc0.a1c: %ImplicitAs.assoc_type.f30 = assoc_entity element0, imports.%Core.import_ref.201 [symbolic]
-// CHECK:STDOUT:   %require_complete.24c: <witness> = require_complete_type %ImplicitAs.type.ee4 [symbolic]
+// CHECK:STDOUT:   %C.635: type = class_type @C, @C(%V.binding.as_type) [symbolic]
+// CHECK:STDOUT:   %C.Create.type.069: type = fn_type @C.Create, @C(%V.binding.as_type) [symbolic]
+// CHECK:STDOUT:   %C.Create.63a: %C.Create.type.069 = struct_value () [symbolic]
+// CHECK:STDOUT:   %require_complete.829: <witness> = require_complete_type %C.635 [symbolic]
+// CHECK:STDOUT:   %pattern_type.29e: type = pattern_type %V.binding.as_type [symbolic]
+// CHECK:STDOUT:   %C.Create.specific_fn: <specific function> = specific_function %C.Create.63a, @C.Create(%V.binding.as_type) [symbolic]
+// CHECK:STDOUT:   %require_complete.3f7: <witness> = require_complete_type %V.binding.as_type [symbolic]
+// CHECK:STDOUT:   %ImplicitAs.type.3ee: type = facet_type <@ImplicitAs, @ImplicitAs(%V.binding.as_type)> [symbolic]
+// CHECK:STDOUT:   %ImplicitAs.assoc_type.efc: type = assoc_entity_type @ImplicitAs, @ImplicitAs(%V.binding.as_type) [symbolic]
+// CHECK:STDOUT:   %assoc0.57e: %ImplicitAs.assoc_type.efc = assoc_entity element0, imports.%Core.import_ref.201 [symbolic]
+// CHECK:STDOUT:   %require_complete.8dc: <witness> = require_complete_type %ImplicitAs.type.3ee [symbolic]
 // CHECK:STDOUT:   %assoc0.843: %ImplicitAs.assoc_type.ff3 = assoc_entity element0, imports.%Core.import_ref.cc1 [symbolic]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
@@ -325,31 +325,33 @@ fn F(unused U:! type, V:! type where {} impls Core.ImplicitAs(.Self)) {
 // CHECK:STDOUT:     %T.patt: %pattern_type.98f = symbolic_binding_pattern T, 0 [concrete]
 // CHECK:STDOUT:   } {
 // CHECK:STDOUT:     %.loc4_13.1: type = splice_block %.loc4_13.2 [concrete = type] {
-// CHECK:STDOUT:       %.Self: %type = symbolic_binding .Self [symbolic_self = constants.%.Self.c39]
+// CHECK:STDOUT:       %.Self: %type = symbolic_binding .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.loc4_13.2: type = type_literal type [concrete = type]
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %T.loc4_10.2: type = symbolic_binding T, 0 [symbolic = %T.loc4_10.1 (constants.%T)]
 // 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:     %V.patt: %pattern_type.354 = symbolic_binding_pattern V, 1 [concrete]
+// CHECK:STDOUT:     %V.patt: %pattern_type.9a5 = symbolic_binding_pattern V, 1 [concrete]
 // CHECK:STDOUT:   } {
 // CHECK:STDOUT:     %.loc9_17.1: type = splice_block %.loc9_17.2 [concrete = type] {
-// CHECK:STDOUT:       %.Self.3: %type = symbolic_binding .Self [symbolic_self = constants.%.Self.c39]
+// CHECK:STDOUT:       %.Self.3: %type = symbolic_binding .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.loc9_17.2: type = type_literal type [concrete = type]
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %U.loc9_14.2: type = symbolic_binding U, 0 [symbolic = %U.loc9_14.1 (constants.%U)]
-// CHECK:STDOUT:     %.loc9_32.1: type = splice_block %.loc9_32.2 [concrete = constants.%type_where] {
-// CHECK:STDOUT:       %.Self.1: %type = symbolic_binding .Self [symbolic_self = constants.%.Self.c39]
+// CHECK:STDOUT:     %.loc9_32.1: type = splice_block %.loc9_32.2 [symbolic_self = constants.%type_where] {
+// CHECK:STDOUT:       %.Self.1: %type = symbolic_binding .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.loc9_27: type = type_literal type [concrete = type]
-// CHECK:STDOUT:       %.Self.2: type = symbolic_binding .Self [symbolic_self = constants.%.Self.16f]
+// CHECK:STDOUT:       %.Self.2: %type = symbolic_binding .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.loc9_39.1: %empty_struct_type = struct_literal () [concrete = constants.%empty_struct]
 // CHECK:STDOUT:       %Core.ref: <namespace> = name_ref Core, imports.%Core [concrete = imports.%Core]
 // CHECK:STDOUT:       %ImplicitAs.ref: %ImplicitAs.type.cc7 = name_ref ImplicitAs, imports.%Core.ImplicitAs [concrete = constants.%ImplicitAs.generic]
-// CHECK:STDOUT:       %.Self.ref: type = name_ref .Self, %.Self.2 [symbolic_self = constants.%.Self.16f]
-// CHECK:STDOUT:       %ImplicitAs.type.loc9: type = facet_type <@ImplicitAs, @ImplicitAs(constants.%.Self.16f)> [symbolic_self = constants.%ImplicitAs.type.f60]
+// CHECK:STDOUT:       %.Self.ref: %type = name_ref .Self, %.Self.2 [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:       %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.binding.as_type]
+// CHECK:STDOUT:       %.loc9_68: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.binding.as_type]
+// CHECK:STDOUT:       %ImplicitAs.type.loc9: type = facet_type <@ImplicitAs, @ImplicitAs(constants.%.Self.binding.as_type)> [symbolic_self = constants.%ImplicitAs.type.164]
 // CHECK:STDOUT:       %.loc9_39.2: type = converted %.loc9_39.1, constants.%empty_struct_type [concrete = constants.%empty_struct_type]
-// CHECK:STDOUT:       %.loc9_32.2: type = where_expr %.Self.2 [concrete = constants.%type_where] {
+// CHECK:STDOUT:       %.loc9_32.2: type = where_expr %.Self.2 [symbolic_self = constants.%type_where] {
 // CHECK:STDOUT:         requirement_base_facet_type type
 // CHECK:STDOUT:         requirement_impls %.loc9_39.2, %ImplicitAs.type.loc9
 // CHECK:STDOUT:       }
@@ -403,16 +405,16 @@ fn F(unused U:! type, V:! type where {} impls Core.ImplicitAs(.Self)) {
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT:   %V.binding.as_type: type = symbolic_binding_type V, 1, %V.loc9_24.1 [symbolic = %V.binding.as_type (constants.%V.binding.as_type)]
-// CHECK:STDOUT:   %C.loc20_6.2: type = class_type @C, @C(%V.binding.as_type) [symbolic = %C.loc20_6.2 (constants.%C.bca)]
-// CHECK:STDOUT:   %require_complete.loc20_7: <witness> = require_complete_type %C.loc20_6.2 [symbolic = %require_complete.loc20_7 (constants.%require_complete.232)]
-// CHECK:STDOUT:   %C.Create.type: type = fn_type @C.Create, @C(%V.binding.as_type) [symbolic = %C.Create.type (constants.%C.Create.type.242)]
-// CHECK:STDOUT:   %C.Create: @F.%C.Create.type (%C.Create.type.242) = struct_value () [symbolic = %C.Create (constants.%C.Create.206)]
+// CHECK:STDOUT:   %C.loc20_6.2: type = class_type @C, @C(%V.binding.as_type) [symbolic = %C.loc20_6.2 (constants.%C.635)]
+// CHECK:STDOUT:   %require_complete.loc20_7: <witness> = require_complete_type %C.loc20_6.2 [symbolic = %require_complete.loc20_7 (constants.%require_complete.829)]
+// CHECK:STDOUT:   %C.Create.type: type = fn_type @C.Create, @C(%V.binding.as_type) [symbolic = %C.Create.type (constants.%C.Create.type.069)]
+// CHECK:STDOUT:   %C.Create: @F.%C.Create.type (%C.Create.type.069) = struct_value () [symbolic = %C.Create (constants.%C.Create.63a)]
 // CHECK:STDOUT:   %C.Create.specific_fn.loc20_7.2: <specific function> = specific_function %C.Create, @C.Create(%V.binding.as_type) [symbolic = %C.Create.specific_fn.loc20_7.2 (constants.%C.Create.specific_fn)]
-// CHECK:STDOUT:   %require_complete.loc20_16.1: <witness> = require_complete_type %V.binding.as_type [symbolic = %require_complete.loc20_16.1 (constants.%require_complete.94b)]
-// CHECK:STDOUT:   %ImplicitAs.type.loc20_16.2: type = facet_type <@ImplicitAs, @ImplicitAs(%V.binding.as_type)> [symbolic = %ImplicitAs.type.loc20_16.2 (constants.%ImplicitAs.type.ee4)]
-// CHECK:STDOUT:   %require_complete.loc20_16.2: <witness> = require_complete_type %ImplicitAs.type.loc20_16.2 [symbolic = %require_complete.loc20_16.2 (constants.%require_complete.24c)]
-// CHECK:STDOUT:   %ImplicitAs.assoc_type: type = assoc_entity_type @ImplicitAs, @ImplicitAs(%V.binding.as_type) [symbolic = %ImplicitAs.assoc_type (constants.%ImplicitAs.assoc_type.f30)]
-// CHECK:STDOUT:   %assoc0: @F.%ImplicitAs.assoc_type (%ImplicitAs.assoc_type.f30) = assoc_entity element0, imports.%Core.import_ref.201 [symbolic = %assoc0 (constants.%assoc0.a1c)]
+// CHECK:STDOUT:   %require_complete.loc20_16.1: <witness> = require_complete_type %V.binding.as_type [symbolic = %require_complete.loc20_16.1 (constants.%require_complete.3f7)]
+// CHECK:STDOUT:   %ImplicitAs.type.loc20_16.2: type = facet_type <@ImplicitAs, @ImplicitAs(%V.binding.as_type)> [symbolic = %ImplicitAs.type.loc20_16.2 (constants.%ImplicitAs.type.3ee)]
+// CHECK:STDOUT:   %require_complete.loc20_16.2: <witness> = require_complete_type %ImplicitAs.type.loc20_16.2 [symbolic = %require_complete.loc20_16.2 (constants.%require_complete.8dc)]
+// CHECK:STDOUT:   %ImplicitAs.assoc_type: type = assoc_entity_type @ImplicitAs, @ImplicitAs(%V.binding.as_type) [symbolic = %ImplicitAs.assoc_type (constants.%ImplicitAs.assoc_type.efc)]
+// CHECK:STDOUT:   %assoc0: @F.%ImplicitAs.assoc_type (%ImplicitAs.assoc_type.efc) = assoc_entity element0, imports.%Core.import_ref.201 [symbolic = %assoc0 (constants.%assoc0.57e)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   fn() {
 // CHECK:STDOUT:   !entry:
@@ -420,14 +422,14 @@ fn F(unused U:! type, V:! type where {} impls Core.ImplicitAs(.Self)) {
 // CHECK:STDOUT:     %V.ref: %type_where = name_ref V, %V.loc9_24.2 [symbolic = %V.loc9_24.1 (constants.%V)]
 // CHECK:STDOUT:     %V.as_type: type = facet_access_type %V.ref [symbolic = %V.binding.as_type (constants.%V.binding.as_type)]
 // CHECK:STDOUT:     %.loc20_6: type = converted %V.ref, %V.as_type [symbolic = %V.binding.as_type (constants.%V.binding.as_type)]
-// CHECK:STDOUT:     %C.loc20_6.1: type = class_type @C, @C(constants.%V.binding.as_type) [symbolic = %C.loc20_6.2 (constants.%C.bca)]
-// CHECK:STDOUT:     %.loc20_7: @F.%C.Create.type (%C.Create.type.242) = specific_constant @C.%C.Create.decl, @C(constants.%V.binding.as_type) [symbolic = %C.Create (constants.%C.Create.206)]
-// CHECK:STDOUT:     %Create.ref: @F.%C.Create.type (%C.Create.type.242) = name_ref Create, %.loc20_7 [symbolic = %C.Create (constants.%C.Create.206)]
+// CHECK:STDOUT:     %C.loc20_6.1: type = class_type @C, @C(constants.%V.binding.as_type) [symbolic = %C.loc20_6.2 (constants.%C.635)]
+// CHECK:STDOUT:     %.loc20_7: @F.%C.Create.type (%C.Create.type.069) = specific_constant @C.%C.Create.decl, @C(constants.%V.binding.as_type) [symbolic = %C.Create (constants.%C.Create.63a)]
+// CHECK:STDOUT:     %Create.ref: @F.%C.Create.type (%C.Create.type.069) = name_ref Create, %.loc20_7 [symbolic = %C.Create (constants.%C.Create.63a)]
 // CHECK:STDOUT:     %.loc20_16.1: %empty_struct_type = struct_literal () [concrete = constants.%empty_struct]
 // CHECK:STDOUT:     %C.Create.specific_fn.loc20_7.1: <specific function> = specific_function %Create.ref, @C.Create(constants.%V.binding.as_type) [symbolic = %C.Create.specific_fn.loc20_7.2 (constants.%C.Create.specific_fn)]
-// CHECK:STDOUT:     %ImplicitAs.type.loc20_16.1: type = facet_type <@ImplicitAs, @ImplicitAs(constants.%V.binding.as_type)> [symbolic = %ImplicitAs.type.loc20_16.2 (constants.%ImplicitAs.type.ee4)]
-// CHECK:STDOUT:     %.loc20_16.2: @F.%ImplicitAs.assoc_type (%ImplicitAs.assoc_type.f30) = specific_constant imports.%Core.import_ref.178, @ImplicitAs.WithSelf(constants.%V.binding.as_type, constants.%Self.738) [symbolic = %assoc0 (constants.%assoc0.a1c)]
-// CHECK:STDOUT:     %Convert.ref: @F.%ImplicitAs.assoc_type (%ImplicitAs.assoc_type.f30) = name_ref Convert, %.loc20_16.2 [symbolic = %assoc0 (constants.%assoc0.a1c)]
+// CHECK:STDOUT:     %ImplicitAs.type.loc20_16.1: type = facet_type <@ImplicitAs, @ImplicitAs(constants.%V.binding.as_type)> [symbolic = %ImplicitAs.type.loc20_16.2 (constants.%ImplicitAs.type.3ee)]
+// CHECK:STDOUT:     %.loc20_16.2: @F.%ImplicitAs.assoc_type (%ImplicitAs.assoc_type.efc) = specific_constant imports.%Core.import_ref.178, @ImplicitAs.WithSelf(constants.%V.binding.as_type, constants.%Self.738) [symbolic = %assoc0 (constants.%assoc0.57e)]
+// CHECK:STDOUT:     %Convert.ref: @F.%ImplicitAs.assoc_type (%ImplicitAs.assoc_type.efc) = name_ref Convert, %.loc20_16.2 [symbolic = %assoc0 (constants.%assoc0.57e)]
 // CHECK:STDOUT:     %.loc20_16.3: @F.%V.binding.as_type (%V.binding.as_type) = converted %.loc20_16.1, <error> [concrete = <error>]
 // CHECK:STDOUT:     %C.Create.call: init %empty_tuple.type = call %C.Create.specific_fn.loc20_7.1(<error>)
 // CHECK:STDOUT:     return
@@ -456,15 +458,15 @@ fn F(unused U:! type, V:! type where {} impls Core.ImplicitAs(.Self)) {
 // CHECK:STDOUT:   %T.loc4_10.1 => constants.%V.binding.as_type
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
-// CHECK:STDOUT:   %C.Create.type => constants.%C.Create.type.242
-// CHECK:STDOUT:   %C.Create => constants.%C.Create.206
+// CHECK:STDOUT:   %C.Create.type => constants.%C.Create.type.069
+// CHECK:STDOUT:   %C.Create => constants.%C.Create.63a
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @C.Create(constants.%V.binding.as_type) {
 // CHECK:STDOUT:   %T => constants.%V.binding.as_type
-// CHECK:STDOUT:   %pattern_type => constants.%pattern_type.20b
+// CHECK:STDOUT:   %pattern_type => constants.%pattern_type.29e
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
-// CHECK:STDOUT:   %require_complete => constants.%require_complete.94b
+// CHECK:STDOUT:   %require_complete => constants.%require_complete.3f7
 // CHECK:STDOUT: }
 // CHECK:STDOUT:

+ 32 - 24
toolchain/check/testdata/facet/convert_facet_value_to_narrowed_facet_type.carbon

@@ -959,7 +959,7 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
 // CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
-// CHECK:STDOUT:   %.Self.c39: %type = symbolic_binding .Self [symbolic_self]
+// CHECK:STDOUT:   %.Self: %type = symbolic_binding .Self [symbolic_self]
 // CHECK:STDOUT:   %pattern_type.98f: type = pattern_type type [concrete]
 // CHECK:STDOUT:   %T.67db0b.1: type = symbolic_binding T, 0 [symbolic]
 // CHECK:STDOUT:   %pattern_type.51d: type = pattern_type %T.67db0b.1 [symbolic]
@@ -967,7 +967,7 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:   %empty_tuple.type: type = tuple_type () [concrete]
 // CHECK:STDOUT:   %TakesTypeDeduced: %TakesTypeDeduced.type = struct_value () [concrete]
 // CHECK:STDOUT:   %require_complete.944: <witness> = require_complete_type %T.67db0b.1 [symbolic]
-// CHECK:STDOUT:   %.Self.16f: type = symbolic_binding .Self [symbolic_self]
+// CHECK:STDOUT:   %.Self.binding.as_type: type = symbolic_binding_type .Self, %.Self [symbolic_self]
 // CHECK:STDOUT:   %pattern_type.9a5: type = pattern_type %type [concrete]
 // CHECK:STDOUT:   %U: %type = symbolic_binding U, 0 [symbolic]
 // CHECK:STDOUT:   %U.binding.as_type: type = symbolic_binding_type U, 0, %U [symbolic]
@@ -1006,7 +1006,7 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:     %x.patt: @TakesTypeDeduced.%pattern_type (%pattern_type.51d) = at_binding_pattern x, %x.param_patt [concrete]
 // CHECK:STDOUT:   } {
 // CHECK:STDOUT:     %.loc3_25.1: type = splice_block %.loc3_25.2 [concrete = type] {
-// CHECK:STDOUT:       %.Self: %type = symbolic_binding .Self [symbolic_self = constants.%.Self.c39]
+// CHECK:STDOUT:       %.Self: %type = symbolic_binding .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.loc3_25.2: type = type_literal type [concrete = type]
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %T.loc3_22.2: type = symbolic_binding T, 0 [symbolic = %T.loc3_22.1 (constants.%T.67db0b.1)]
@@ -1020,14 +1020,16 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:     %y.patt: @CallsWithExtraWhere.%pattern_type (%pattern_type.349) = at_binding_pattern y, %y.param_patt [concrete]
 // CHECK:STDOUT:   } {
 // CHECK:STDOUT:     %.loc4_33.1: type = splice_block %.loc4_33.2 [concrete = constants.%type] {
-// CHECK:STDOUT:       %.Self.1: %type = symbolic_binding .Self [symbolic_self = constants.%.Self.c39]
+// CHECK:STDOUT:       %.Self.1: %type = symbolic_binding .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.loc4_28: type = type_literal type [concrete = type]
-// CHECK:STDOUT:       %.Self.2: type = symbolic_binding .Self [symbolic_self = constants.%.Self.16f]
-// CHECK:STDOUT:       %.Self.ref: type = name_ref .Self, %.Self.2 [symbolic_self = constants.%.Self.16f]
+// CHECK:STDOUT:       %.Self.2: %type = symbolic_binding .Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:       %.Self.ref: %type = name_ref .Self, %.Self.2 [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.loc4_51: type = type_literal type [concrete = type]
+// CHECK:STDOUT:       %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.binding.as_type]
+// CHECK:STDOUT:       %.loc4_39: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.binding.as_type]
 // CHECK:STDOUT:       %.loc4_33.2: type = where_expr %.Self.2 [concrete = constants.%type] {
 // CHECK:STDOUT:         requirement_base_facet_type type
-// CHECK:STDOUT:         requirement_impls %.Self.ref, %.loc4_51
+// CHECK:STDOUT:         requirement_impls %.loc4_39, %.loc4_51
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %U.loc4_25.2: %type = symbolic_binding U, 0 [symbolic = %U.loc4_25.1 (constants.%U)]
@@ -1043,7 +1045,7 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:     %T.patt: %pattern_type.98f = symbolic_binding_pattern T, 0 [concrete]
 // CHECK:STDOUT:   } {
 // CHECK:STDOUT:     %.loc8_33.1: type = splice_block %.loc8_33.2 [concrete = type] {
-// CHECK:STDOUT:       %.Self: %type = symbolic_binding .Self [symbolic_self = constants.%.Self.c39]
+// CHECK:STDOUT:       %.Self: %type = symbolic_binding .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.loc8_33.2: type = type_literal type [concrete = type]
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %T.loc8_30.3: type = symbolic_binding T, 0 [symbolic = %T.loc8_30.2 (constants.%T.67db0b.2)]
@@ -1052,14 +1054,16 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:     %U.patt: %pattern_type.9a5 = symbolic_binding_pattern U, 0 [concrete]
 // CHECK:STDOUT:   } {
 // CHECK:STDOUT:     %.loc9_41.1: type = splice_block %.loc9_41.2 [concrete = constants.%type] {
-// CHECK:STDOUT:       %.Self.1: %type = symbolic_binding .Self [symbolic_self = constants.%.Self.c39]
+// CHECK:STDOUT:       %.Self.1: %type = symbolic_binding .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.loc9_36: type = type_literal type [concrete = type]
-// CHECK:STDOUT:       %.Self.2: type = symbolic_binding .Self [symbolic_self = constants.%.Self.16f]
-// CHECK:STDOUT:       %.Self.ref: type = name_ref .Self, %.Self.2 [symbolic_self = constants.%.Self.16f]
+// CHECK:STDOUT:       %.Self.2: %type = symbolic_binding .Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:       %.Self.ref: %type = name_ref .Self, %.Self.2 [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.loc9_59: type = type_literal type [concrete = type]
+// CHECK:STDOUT:       %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.binding.as_type]
+// CHECK:STDOUT:       %.loc9_47: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.binding.as_type]
 // CHECK:STDOUT:       %.loc9_41.2: type = where_expr %.Self.2 [concrete = constants.%type] {
 // CHECK:STDOUT:         requirement_base_facet_type type
-// CHECK:STDOUT:         requirement_impls %.Self.ref, %.loc9_59
+// CHECK:STDOUT:         requirement_impls %.loc9_47, %.loc9_59
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %U.loc9_33.2: %type = symbolic_binding U, 0 [symbolic = %U.loc9_33.1 (constants.%U)]
@@ -1168,8 +1172,8 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
 // CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
-// CHECK:STDOUT:   %.Self.c39: %type = symbolic_binding .Self [symbolic_self]
-// CHECK:STDOUT:   %.Self.16f: type = symbolic_binding .Self [symbolic_self]
+// CHECK:STDOUT:   %.Self: %type = symbolic_binding .Self [symbolic_self]
+// CHECK:STDOUT:   %.Self.binding.as_type: type = symbolic_binding_type .Self, %.Self [symbolic_self]
 // CHECK:STDOUT:   %pattern_type.9a5: type = pattern_type %type [concrete]
 // CHECK:STDOUT:   %T.f45530.1: %type = symbolic_binding T, 0 [symbolic]
 // CHECK:STDOUT:   %T.binding.as_type: type = symbolic_binding_type T, 0, %T.f45530.1 [symbolic]
@@ -1216,14 +1220,16 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:     %x.patt: @TakesExtraWhereDeduced.%pattern_type (%pattern_type.349) = at_binding_pattern x, %x.param_patt [concrete]
 // CHECK:STDOUT:   } {
 // CHECK:STDOUT:     %.loc3_36.1: type = splice_block %.loc3_36.2 [concrete = constants.%type] {
-// CHECK:STDOUT:       %.Self.1: %type = symbolic_binding .Self [symbolic_self = constants.%.Self.c39]
+// CHECK:STDOUT:       %.Self.1: %type = symbolic_binding .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.loc3_31: type = type_literal type [concrete = type]
-// CHECK:STDOUT:       %.Self.2: type = symbolic_binding .Self [symbolic_self = constants.%.Self.16f]
-// CHECK:STDOUT:       %.Self.ref: type = name_ref .Self, %.Self.2 [symbolic_self = constants.%.Self.16f]
+// CHECK:STDOUT:       %.Self.2: %type = symbolic_binding .Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:       %.Self.ref: %type = name_ref .Self, %.Self.2 [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.loc3_54: type = type_literal type [concrete = type]
+// CHECK:STDOUT:       %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.binding.as_type]
+// CHECK:STDOUT:       %.loc3_42: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.binding.as_type]
 // CHECK:STDOUT:       %.loc3_36.2: type = where_expr %.Self.2 [concrete = constants.%type] {
 // CHECK:STDOUT:         requirement_base_facet_type type
-// CHECK:STDOUT:         requirement_impls %.Self.ref, %.loc3_54
+// CHECK:STDOUT:         requirement_impls %.loc3_42, %.loc3_54
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %T.loc3_28.2: %type = symbolic_binding T, 0 [symbolic = %T.loc3_28.1 (constants.%T.f45530.1)]
@@ -1241,7 +1247,7 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:     %y.patt: @CallsWithType.%pattern_type (%pattern_type.51d) = at_binding_pattern y, %y.param_patt [concrete]
 // CHECK:STDOUT:   } {
 // CHECK:STDOUT:     %.loc4_22.1: type = splice_block %.loc4_22.2 [concrete = type] {
-// CHECK:STDOUT:       %.Self: %type = symbolic_binding .Self [symbolic_self = constants.%.Self.c39]
+// CHECK:STDOUT:       %.Self: %type = symbolic_binding .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.loc4_22.2: type = type_literal type [concrete = type]
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %U.loc4_19.2: type = symbolic_binding U, 0 [symbolic = %U.loc4_19.1 (constants.%U)]
@@ -1253,14 +1259,16 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:     %T.patt: %pattern_type.9a5 = symbolic_binding_pattern T, 0 [concrete]
 // CHECK:STDOUT:   } {
 // CHECK:STDOUT:     %.loc8_44.1: type = splice_block %.loc8_44.2 [concrete = constants.%type] {
-// CHECK:STDOUT:       %.Self.1: %type = symbolic_binding .Self [symbolic_self = constants.%.Self.c39]
+// CHECK:STDOUT:       %.Self.1: %type = symbolic_binding .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.loc8_39: type = type_literal type [concrete = type]
-// CHECK:STDOUT:       %.Self.2: type = symbolic_binding .Self [symbolic_self = constants.%.Self.16f]
-// CHECK:STDOUT:       %.Self.ref: type = name_ref .Self, %.Self.2 [symbolic_self = constants.%.Self.16f]
+// CHECK:STDOUT:       %.Self.2: %type = symbolic_binding .Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:       %.Self.ref: %type = name_ref .Self, %.Self.2 [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.loc8_62: type = type_literal type [concrete = type]
+// CHECK:STDOUT:       %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.binding.as_type]
+// CHECK:STDOUT:       %.loc8_50: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.binding.as_type]
 // CHECK:STDOUT:       %.loc8_44.2: type = where_expr %.Self.2 [concrete = constants.%type] {
 // CHECK:STDOUT:         requirement_base_facet_type type
-// CHECK:STDOUT:         requirement_impls %.Self.ref, %.loc8_62
+// CHECK:STDOUT:         requirement_impls %.loc8_50, %.loc8_62
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %T.loc8_36.3: %type = symbolic_binding T, 0 [symbolic = %T.loc8_36.2 (constants.%T.f45530.2)]
@@ -1269,7 +1277,7 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:     %U.patt: %pattern_type.98f = symbolic_binding_pattern U, 0 [concrete]
 // CHECK:STDOUT:   } {
 // CHECK:STDOUT:     %.loc9_30.1: type = splice_block %.loc9_30.2 [concrete = type] {
-// CHECK:STDOUT:       %.Self: %type = symbolic_binding .Self [symbolic_self = constants.%.Self.c39]
+// CHECK:STDOUT:       %.Self: %type = symbolic_binding .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.loc9_30.2: type = type_literal type [concrete = type]
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %U.loc9_27.2: type = symbolic_binding U, 0 [symbolic = %U.loc9_27.1 (constants.%U)]

+ 73 - 6
toolchain/check/testdata/facet/validate_impl_constraints.carbon

@@ -55,12 +55,12 @@ impl forall [U:! L] C(U) as M where .M0 = {} {}
 fn F(unused U:! type where C(.Self) impls (M where .M0 = {})) {}
 
 fn G(T:! L) {
-  // CHECK:STDERR: fail_todo_where_impls_tests_associated_constant_of_generic_type.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `L` into type implementing `type where...` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR: fail_todo_where_impls_tests_associated_constant_of_generic_type.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `L` into type implementing `type where C(.Self) impls M and .(M.M0) = {}` [ConversionFailureFacetToFacet]
   // CHECK:STDERR:   F(T);
   // CHECK:STDERR:   ^~~~
-  // CHECK:STDERR: fail_todo_where_impls_tests_associated_constant_of_generic_type.carbon:[[@LINE-6]]:13: note: initializing generic parameter `U` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fail_todo_where_impls_tests_associated_constant_of_generic_type.carbon:[[@LINE-6]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
   // CHECK:STDERR: fn F(unused U:! type where C(.Self) impls (M where .M0 = {})) {}
-  // CHECK:STDERR:             ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   // CHECK:STDERR:
   F(T);
 }
@@ -81,12 +81,12 @@ impl forall [U:! L] C(U) as M where .M0 = () {}
 fn F(unused U:! type where C(.Self) impls (M where .M0 = {})) {}
 
 fn G(T:! L) {
-  // CHECK:STDERR: fail_where_impls_tests_associated_constant_of_generic_type_type_differs.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `L` into type implementing `type where...` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR: fail_where_impls_tests_associated_constant_of_generic_type_type_differs.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `L` into type implementing `type where C(.Self) impls M and .(M.M0) = {}` [ConversionFailureFacetToFacet]
   // CHECK:STDERR:   F(T);
   // CHECK:STDERR:   ^~~~
-  // CHECK:STDERR: fail_where_impls_tests_associated_constant_of_generic_type_type_differs.carbon:[[@LINE-6]]:13: note: initializing generic parameter `U` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fail_where_impls_tests_associated_constant_of_generic_type_type_differs.carbon:[[@LINE-6]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
   // CHECK:STDERR: fn F(unused U:! type where C(.Self) impls (M where .M0 = {})) {}
-  // CHECK:STDERR:             ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   // CHECK:STDERR:
   F(T);
 }
@@ -130,3 +130,70 @@ fn F(unused T:! I(.Self) where .Self impls Z) {}
 fn G(T:! Z & I(.Self)) {
   F(T);
 }
+
+// --- fail_todo_where_period_self_rhs_sees_lhs.carbon
+library "[[@TEST_NAME]]";
+
+interface Z {}
+interface Y {}
+interface X(T:! Z & Y) {}
+
+constraint N {
+  require impls Y;
+}
+
+// The RHS of `where` can see the extend constraints on the LHS of `where`.
+// CHECK:STDERR: fail_todo_where_period_self_rhs_sees_lhs.carbon:[[@LINE+7]]:34: error: cannot convert type `.Self` that implements `Z` into type implementing `Z & Y` [ConversionFailureFacetToFacet]
+// CHECK:STDERR: fn F(_:! Z & N where .Self impls X(.Self)) {}
+// CHECK:STDERR:                                  ^~~~~~~~
+// CHECK:STDERR: fail_todo_where_period_self_rhs_sees_lhs.carbon:[[@LINE-10]]:13: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+// CHECK:STDERR: interface X(T:! Z & Y) {}
+// CHECK:STDERR:             ^~~~~~~~~
+// CHECK:STDERR:
+fn F(_:! Z & N where .Self impls X(.Self)) {}
+
+fn G() {
+  class C;
+  impl C as Z {}
+  impl C as Y {}
+  impl C as X(C) {}
+  F(C);
+}
+
+// --- fail_todo_where_type_rhs_sees_lhs.carbon
+library "[[@TEST_NAME]]";
+
+interface Z {}
+interface Y {}
+interface X(T:! Z & Y) {}
+
+constraint N {
+  require impls Y;
+}
+
+class R(T:! Z & Y);
+
+// The RHS of `where` can see the extend constraints on the LHS of `where`.
+// CHECK:STDERR: fail_todo_where_type_rhs_sees_lhs.carbon:[[@LINE+14]]:22: error: cannot convert type `.Self` that implements `Z` into type implementing `Z & Y` [ConversionFailureFacetToFacet]
+// CHECK:STDERR: fn F(_:! Z & N where R(.Self) impls X(.Self)) {}
+// CHECK:STDERR:                      ^~~~~~~~
+// CHECK:STDERR: fail_todo_where_type_rhs_sees_lhs.carbon:[[@LINE-6]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+// CHECK:STDERR: class R(T:! Z & Y);
+// CHECK:STDERR:         ^~~~~~~~~
+// CHECK:STDERR:
+// CHECK:STDERR: fail_todo_where_type_rhs_sees_lhs.carbon:[[@LINE+7]]:37: error: cannot convert type `.Self` that implements `Z` into type implementing `Z & Y` [ConversionFailureFacetToFacet]
+// CHECK:STDERR: fn F(_:! Z & N where R(.Self) impls X(.Self)) {}
+// CHECK:STDERR:                                     ^~~~~~~~
+// CHECK:STDERR: fail_todo_where_type_rhs_sees_lhs.carbon:[[@LINE-19]]:13: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+// CHECK:STDERR: interface X(T:! Z & Y) {}
+// CHECK:STDERR:             ^~~~~~~~~
+// CHECK:STDERR:
+fn F(_:! Z & N where R(.Self) impls X(.Self)) {}
+
+fn G() {
+  class C;
+  impl C as Z {}
+  impl C as Y {}
+  impl R(C) as X(C) {}
+  F(C);
+}

+ 11 - 11
toolchain/check/testdata/impl/assoc_const_self.carbon

@@ -90,12 +90,12 @@ fn F(T:! I where {} impls Core.ImplicitAs(.Self) and .V = {});
 
 fn CallF() {
   // TODO: This call should eventually work.
-  // CHECK:STDERR: fail_todo_constrained_fn.carbon:[[@LINE+7]]:3: error: cannot convert type `{}` into type implementing `I where .(I.V) = {} and...` [ConversionFailureTypeToFacet]
+  // CHECK:STDERR: fail_todo_constrained_fn.carbon:[[@LINE+7]]:3: error: cannot convert type `{}` into type implementing `I where {} impls Core.ImplicitAs(.Self) and .(I.V) = {}` [ConversionFailureTypeToFacet]
   // CHECK:STDERR:   F({});
   // CHECK:STDERR:   ^~~~~
-  // CHECK:STDERR: fail_todo_constrained_fn.carbon:[[@LINE-7]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fail_todo_constrained_fn.carbon:[[@LINE-7]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
   // CHECK:STDERR: fn F(T:! I where {} impls Core.ImplicitAs(.Self) and .V = {});
-  // CHECK:STDERR:      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   // CHECK:STDERR:
   F({});
 }
@@ -742,10 +742,10 @@ fn CallF() {
 // CHECK:STDOUT:   %ImplicitAs.generic: %ImplicitAs.type.cc7 = struct_value () [concrete]
 // CHECK:STDOUT:   %.Self.binding.as_type: type = symbolic_binding_type .Self, %.Self.1dc [symbolic_self]
 // CHECK:STDOUT:   %ImplicitAs.type.d65: type = facet_type <@ImplicitAs, @ImplicitAs(%.Self.binding.as_type)> [symbolic_self]
-// CHECK:STDOUT:   %I.lookup_impl_witness: <witness> = lookup_impl_witness %.Self.1dc, @I [symbolic_self]
-// CHECK:STDOUT:   %impl.elem0: %.Self.binding.as_type = impl_witness_access %I.lookup_impl_witness, element0 [symbolic_self]
-// CHECK:STDOUT:   %I_where.type: type = facet_type <@I where %impl.elem0 = %empty_struct and TODO> [concrete]
-// CHECK:STDOUT:   %pattern_type.d53: type = pattern_type %I_where.type [concrete]
+// CHECK:STDOUT:   %I.lookup_impl_witness.c4b: <witness> = lookup_impl_witness %.Self.1dc, @I [symbolic_self]
+// CHECK:STDOUT:   %impl.elem0: %.Self.binding.as_type = impl_witness_access %I.lookup_impl_witness.c4b, element0 [symbolic_self]
+// CHECK:STDOUT:   %I_where.type: type = facet_type <@I where %empty_struct_type impls @ImplicitAs, @ImplicitAs(%.Self.binding.as_type) and %impl.elem0 = %empty_struct> [symbolic_self]
+// CHECK:STDOUT:   %pattern_type.81c: type = pattern_type %I_where.type [symbolic_self]
 // CHECK:STDOUT:   %T: %I_where.type = symbolic_binding T, 0 [symbolic]
 // CHECK:STDOUT:   %F.type: type = fn_type @F [concrete]
 // CHECK:STDOUT:   %F: %F.type = struct_value () [concrete]
@@ -772,9 +772,9 @@ fn CallF() {
 // CHECK:STDOUT:   %Core.import = import Core
 // CHECK:STDOUT:   %I.decl: type = interface_decl @I [concrete = constants.%I.type] {} {}
 // CHECK:STDOUT:   %F.decl: %F.type = fn_decl @F [concrete = constants.%F] {
-// CHECK:STDOUT:     %T.patt: %pattern_type.d53 = symbolic_binding_pattern T, 0 [concrete]
+// CHECK:STDOUT:     %T.patt: %pattern_type.81c = symbolic_binding_pattern T, 0 [concrete]
 // CHECK:STDOUT:   } {
-// CHECK:STDOUT:     %.loc8_12.1: type = splice_block %.loc8_12.2 [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:     %.loc8_12.1: type = splice_block %.loc8_12.2 [symbolic_self = constants.%I_where.type] {
 // CHECK:STDOUT:       %.Self.1: %type = symbolic_binding .Self [symbolic_self = constants.%.Self.c39]
 // CHECK:STDOUT:       %I.ref: type = name_ref I, file.%I.decl [concrete = constants.%I.type]
 // CHECK:STDOUT:       %.Self.2: %I.type = symbolic_binding .Self [symbolic_self = constants.%.Self.1dc]
@@ -790,11 +790,11 @@ fn CallF() {
 // CHECK:STDOUT:       %.Self.as_type.loc8_54: type = facet_access_type %.Self.ref.loc8_54 [symbolic_self = constants.%.Self.binding.as_type]
 // CHECK:STDOUT:       %.loc8_54: type = converted %.Self.ref.loc8_54, %.Self.as_type.loc8_54 [symbolic_self = constants.%.Self.binding.as_type]
 // CHECK:STDOUT:       %V.ref: %I.assoc_type = name_ref V, @V.%assoc0 [concrete = constants.%assoc0.490]
-// CHECK:STDOUT:       %impl.elem0: %.Self.binding.as_type = impl_witness_access constants.%I.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
+// CHECK:STDOUT:       %impl.elem0: %.Self.binding.as_type = impl_witness_access constants.%I.lookup_impl_witness.c4b, element0 [symbolic_self = constants.%impl.elem0]
 // CHECK:STDOUT:       %.loc8_60.1: %empty_struct_type = struct_literal () [concrete = constants.%empty_struct]
 // CHECK:STDOUT:       %empty_struct: %empty_struct_type = struct_value () [concrete = constants.%empty_struct]
 // CHECK:STDOUT:       %.loc8_60.2: %empty_struct_type = converted %.loc8_60.1, %empty_struct [concrete = constants.%empty_struct]
-// CHECK:STDOUT:       %.loc8_12.2: type = where_expr %.Self.2 [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       %.loc8_12.2: type = where_expr %.Self.2 [symbolic_self = constants.%I_where.type] {
 // CHECK:STDOUT:         requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:         requirement_impls %.loc8_19.2, %ImplicitAs.type
 // CHECK:STDOUT:         requirement_rewrite %impl.elem0, %.loc8_60.2

+ 15 - 8
toolchain/check/testdata/impl/fail_impl_bad_interface.carbon

@@ -136,8 +136,9 @@ impl {.a: bool} as type where .Self impls I {}
 // CHECK:STDOUT:   %Float.type: type = generic_class_type @Float [concrete]
 // CHECK:STDOUT:   %Float.generic: %Float.type = struct_value () [concrete]
 // CHECK:STDOUT:   %f64: type = class_type @Float, @Float(%int_64) [concrete]
-// CHECK:STDOUT:   %.Self: type = symbolic_binding .Self [symbolic_self]
 // CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
+// CHECK:STDOUT:   %.Self: %type = symbolic_binding .Self [symbolic_self]
+// CHECK:STDOUT:   %.Self.binding.as_type: type = symbolic_binding_type .Self, %.Self [symbolic_self]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: imports {
@@ -157,12 +158,14 @@ impl {.a: bool} as type where .Self impls I {}
 // CHECK:STDOUT:   impl_decl @f64.as.<error>.impl [concrete] {} {
 // CHECK:STDOUT:     %f64: type = type_literal constants.%f64 [concrete = constants.%f64]
 // CHECK:STDOUT:     %.loc8_13: type = type_literal type [concrete = type]
-// CHECK:STDOUT:     %.Self: type = symbolic_binding .Self [symbolic_self = constants.%.Self]
-// CHECK:STDOUT:     %.Self.ref: type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %.Self: %type = symbolic_binding .Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %.Self.ref: %type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:     %.loc8_36: type = type_literal type [concrete = type]
+// CHECK:STDOUT:     %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.binding.as_type]
+// CHECK:STDOUT:     %.loc8_24: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.binding.as_type]
 // CHECK:STDOUT:     %.loc8_18: type = where_expr %.Self [concrete = constants.%type] {
 // CHECK:STDOUT:       requirement_base_facet_type type
-// CHECK:STDOUT:       requirement_impls %.Self.ref, %.loc8_36
+// CHECK:STDOUT:       requirement_impls %.loc8_24, %.loc8_36
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
@@ -180,7 +183,9 @@ impl {.a: bool} as type where .Self impls I {}
 // CHECK:STDOUT:   %Bool.type: type = fn_type @Bool [concrete]
 // CHECK:STDOUT:   %Bool: %Bool.type = struct_value () [concrete]
 // CHECK:STDOUT:   %struct_type.a: type = struct_type {.a: bool} [concrete]
-// CHECK:STDOUT:   %.Self: type = symbolic_binding .Self [symbolic_self]
+// CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
+// CHECK:STDOUT:   %.Self: %type = symbolic_binding .Self [symbolic_self]
+// CHECK:STDOUT:   %.Self.binding.as_type: type = symbolic_binding_type .Self, %.Self [symbolic_self]
 // CHECK:STDOUT:   %type_where: type = facet_type <type where .Self impls @I> [concrete]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
@@ -204,12 +209,14 @@ impl {.a: bool} as type where .Self impls I {}
 // CHECK:STDOUT:     %.loc10_11: type = type_literal bool [concrete = bool]
 // CHECK:STDOUT:     %struct_type.a: type = struct_type {.a: bool} [concrete = constants.%struct_type.a]
 // CHECK:STDOUT:     %.loc10_20: type = type_literal type [concrete = type]
-// CHECK:STDOUT:     %.Self: type = symbolic_binding .Self [symbolic_self = constants.%.Self]
-// CHECK:STDOUT:     %.Self.ref: type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %.Self: %type = symbolic_binding .Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %.Self.ref: %type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:     %I.ref: type = name_ref I, file.%I.decl [concrete = constants.%I.type]
+// CHECK:STDOUT:     %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.binding.as_type]
+// CHECK:STDOUT:     %.loc10_31: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.binding.as_type]
 // CHECK:STDOUT:     %.loc10_25: type = where_expr %.Self [concrete = constants.%type_where] {
 // CHECK:STDOUT:       requirement_base_facet_type type
-// CHECK:STDOUT:       requirement_impls %.Self.ref, %I.ref
+// CHECK:STDOUT:       requirement_impls %.loc10_31, %I.ref
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }

+ 7 - 4
toolchain/check/testdata/interface/fail_lookup_in_type_type.carbon

@@ -59,8 +59,9 @@ let U: (type where .Self impls type).missing = {};
 // CHECK:STDOUT: --- fail_lookup_type_where.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
-// CHECK:STDOUT:   %.Self: type = symbolic_binding .Self [symbolic_self]
 // CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
+// CHECK:STDOUT:   %.Self: %type = symbolic_binding .Self [symbolic_self]
+// CHECK:STDOUT:   %.Self.binding.as_type: type = symbolic_binding_type .Self, %.Self [symbolic_self]
 // CHECK:STDOUT:   %empty_struct_type: type = struct_type {} [concrete]
 // CHECK:STDOUT:   %empty_struct: %empty_struct_type = struct_value () [concrete]
 // CHECK:STDOUT: }
@@ -74,12 +75,14 @@ let U: (type where .Self impls type).missing = {};
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %.1: <error> = splice_block <error> [concrete = <error>] {
 // CHECK:STDOUT:     %.loc8_9: type = type_literal type [concrete = type]
-// CHECK:STDOUT:     %.Self: type = symbolic_binding .Self [symbolic_self = constants.%.Self]
-// CHECK:STDOUT:     %.Self.ref: type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %.Self: %type = symbolic_binding .Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %.Self.ref: %type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:     %.loc8_32: type = type_literal type [concrete = type]
+// CHECK:STDOUT:     %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.binding.as_type]
+// CHECK:STDOUT:     %.loc8_20: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.binding.as_type]
 // CHECK:STDOUT:     %.loc8_14: type = where_expr %.Self [concrete = constants.%type] {
 // CHECK:STDOUT:       requirement_base_facet_type type
-// CHECK:STDOUT:       requirement_impls %.Self.ref, %.loc8_32
+// CHECK:STDOUT:       requirement_impls %.loc8_20, %.loc8_32
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %missing.ref: <error> = name_ref missing, <error> [concrete = <error>]
 // CHECK:STDOUT:   }

+ 7 - 3
toolchain/check/testdata/named_constraint/extend_name_lookup.carbon

@@ -192,7 +192,9 @@ fn F(T:! type where .Self impls W) {
 // CHECK:STDOUT:   %Y.assoc_type: type = assoc_entity_type @Y [concrete]
 // CHECK:STDOUT:   %assoc0.2e5: %Y.assoc_type = assoc_entity element0, @Y.WithSelf.%Y.WithSelf.YF.decl [concrete]
 // CHECK:STDOUT:   %W.type: type = facet_type <@W> [concrete]
-// CHECK:STDOUT:   %.Self.16f: type = symbolic_binding .Self [symbolic_self]
+// CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
+// CHECK:STDOUT:   %.Self: %type = symbolic_binding .Self [symbolic_self]
+// CHECK:STDOUT:   %.Self.binding.as_type: type = symbolic_binding_type .Self, %.Self [symbolic_self]
 // CHECK:STDOUT:   %type_where: type = facet_type <type> [concrete]
 // CHECK:STDOUT:   %pattern_type: type = pattern_type %type_where [concrete]
 // CHECK:STDOUT:   %T: %type_where = symbolic_binding T, 0 [symbolic]
@@ -221,11 +223,13 @@ fn F(T:! type where .Self impls W) {
 // CHECK:STDOUT:       <elided>
 // CHECK:STDOUT:       %.loc12_10: type = type_literal type [concrete = type]
 // CHECK:STDOUT:       <elided>
-// CHECK:STDOUT:       %.Self.ref: type = name_ref .Self, %.Self.2 [symbolic_self = constants.%.Self.16f]
+// CHECK:STDOUT:       %.Self.ref: %type = name_ref .Self, %.Self.2 [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %W.ref: type = name_ref W, file.%W.decl [concrete = constants.%W.type]
+// CHECK:STDOUT:       %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.binding.as_type]
+// CHECK:STDOUT:       %.loc12_21: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.binding.as_type]
 // CHECK:STDOUT:       %.loc12_15.2: type = where_expr %.Self.2 [concrete = constants.%type_where] {
 // CHECK:STDOUT:         requirement_base_facet_type type
-// CHECK:STDOUT:         requirement_impls %.Self.ref, %W.ref
+// CHECK:STDOUT:         requirement_impls %.loc12_21, %W.ref
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %T.loc12_7.2: %type_where = symbolic_binding T, 0 [symbolic = %T.loc12_7.1 (constants.%T)]

+ 1 - 3
toolchain/check/testdata/named_constraint/require.carbon

@@ -226,9 +226,7 @@ library "[[@TEST_NAME]]";
 
 class C(T:! type);
 constraint Z {
-  // TODO: This should be a RequireImplsReferenceCycle error since `Z` is being
-  // used inside `Z`.
-  // CHECK:STDERR: fail_require_impls_incomplete_self_in_class_impls.carbon:[[@LINE+4]]:17: error: semantics TODO: `facet type has constraints that we don't handle yet` [SemanticsTodo]
+  // CHECK:STDERR: fail_require_impls_incomplete_self_in_class_impls.carbon:[[@LINE+4]]:17: error: facet type in `require` declaration refers to the named constraint `Z` from within its definition [RequireImplsReferenceCycle]
   // CHECK:STDERR:   require impls type where C(.Self) impls Z;
   // CHECK:STDERR:                 ^~~~~~~~~~~~~~~~~~~~~~~~~~~
   // CHECK:STDERR:

+ 11 - 7
toolchain/check/testdata/where_expr/constraints.carbon

@@ -431,8 +431,8 @@ fn F() {
 // CHECK:STDOUT:   %K.lookup_impl_witness: <witness> = lookup_impl_witness %.Self.2ca, @K [symbolic_self]
 // CHECK:STDOUT:   %impl.elem0: %L.type = impl_witness_access %K.lookup_impl_witness, element0 [symbolic_self]
 // CHECK:STDOUT:   %as_type: type = facet_access_type %impl.elem0 [symbolic_self]
-// CHECK:STDOUT:   %K_where.type: type = facet_type <@K where TODO> [concrete]
-// CHECK:STDOUT:   %pattern_type: type = pattern_type %K_where.type [concrete]
+// CHECK:STDOUT:   %K_where.type: type = facet_type <@K where %impl.elem0 impls @M> [symbolic_self]
+// CHECK:STDOUT:   %pattern_type: type = pattern_type %K_where.type [symbolic_self]
 // CHECK:STDOUT:   %W: %K_where.type = symbolic_binding W, 0 [symbolic]
 // CHECK:STDOUT:   %AssociatedTypeImpls.type: type = fn_type @AssociatedTypeImpls [concrete]
 // CHECK:STDOUT:   %AssociatedTypeImpls: %AssociatedTypeImpls.type = struct_value () [concrete]
@@ -442,7 +442,7 @@ fn F() {
 // CHECK:STDOUT:   %AssociatedTypeImpls.decl: %AssociatedTypeImpls.type = fn_decl @AssociatedTypeImpls [concrete = constants.%AssociatedTypeImpls] {
 // CHECK:STDOUT:     %W.patt: %pattern_type = symbolic_binding_pattern W, 0 [concrete]
 // CHECK:STDOUT:   } {
-// CHECK:STDOUT:     %.loc12_30.1: type = splice_block %.loc12_30.2 [concrete = constants.%K_where.type] {
+// CHECK:STDOUT:     %.loc12_30.1: type = splice_block %.loc12_30.2 [symbolic_self = constants.%K_where.type] {
 // CHECK:STDOUT:       <elided>
 // CHECK:STDOUT:       %K.ref: type = name_ref K, file.%K.decl [concrete = constants.%K.type]
 // CHECK:STDOUT:       <elided>
@@ -454,7 +454,7 @@ fn F() {
 // CHECK:STDOUT:       %M.ref: type = name_ref M, file.%M.decl [concrete = constants.%M.type]
 // CHECK:STDOUT:       %as_type: type = facet_access_type %impl.elem0 [symbolic_self = constants.%as_type]
 // CHECK:STDOUT:       %.loc12_36.2: type = converted %impl.elem0, %as_type [symbolic_self = constants.%as_type]
-// CHECK:STDOUT:       %.loc12_30.2: type = where_expr %.Self.2 [concrete = constants.%K_where.type] {
+// CHECK:STDOUT:       %.loc12_30.2: type = where_expr %.Self.2 [symbolic_self = constants.%K_where.type] {
 // CHECK:STDOUT:         requirement_base_facet_type constants.%K.type
 // CHECK:STDOUT:         requirement_impls %.loc12_36.2, %M.ref
 // CHECK:STDOUT:       }
@@ -476,7 +476,9 @@ fn F() {
 // CHECK:STDOUT: --- fail_error_in_constraint.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
-// CHECK:STDOUT:   %.Self.16f: type = symbolic_binding .Self [symbolic_self]
+// CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
+// CHECK:STDOUT:   %.Self: %type = symbolic_binding .Self [symbolic_self]
+// CHECK:STDOUT:   %.Self.binding.as_type: type = symbolic_binding_type .Self, %.Self [symbolic_self]
 // CHECK:STDOUT:   %WithError.type: type = fn_type @WithError [concrete]
 // CHECK:STDOUT:   %WithError: %WithError.type = struct_value () [concrete]
 // CHECK:STDOUT: }
@@ -489,11 +491,13 @@ fn F() {
 // CHECK:STDOUT:       <elided>
 // CHECK:STDOUT:       %.loc9_18: type = type_literal type [concrete = type]
 // CHECK:STDOUT:       <elided>
-// CHECK:STDOUT:       %.Self.ref: type = name_ref .Self, %.Self.2 [symbolic_self = constants.%.Self.16f]
+// CHECK:STDOUT:       %.Self.ref: %type = name_ref .Self, %.Self.2 [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %I.ref: <error> = name_ref I, <error> [concrete = <error>]
+// CHECK:STDOUT:       %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.binding.as_type]
+// CHECK:STDOUT:       %.loc9_29: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.binding.as_type]
 // CHECK:STDOUT:       %.loc9_23.2: type = where_expr %.Self.2 [concrete = <error>] {
 // CHECK:STDOUT:         requirement_base_facet_type type
-// CHECK:STDOUT:         requirement_impls %.Self.ref, <error>
+// CHECK:STDOUT:         requirement_impls %.loc9_29, <error>
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %U: <error> = symbolic_binding U, 0 [concrete = <error>]

+ 10 - 6
toolchain/check/testdata/where_expr/designator.carbon

@@ -145,6 +145,8 @@ fn G(unused T:! type where C(()) impls I(.Self)) {}
 // CHECK:STDOUT:   %I.type: type = facet_type <@I> [concrete]
 // CHECK:STDOUT:   %I.assoc_type: type = assoc_entity_type @I [concrete]
 // CHECK:STDOUT:   %assoc0: %I.assoc_type = assoc_entity element0, @I.WithSelf.%Member [concrete]
+// CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
+// CHECK:STDOUT:   %.Self.c39: %type = symbolic_binding .Self [symbolic_self]
 // CHECK:STDOUT:   %.Self.1dc: %I.type = symbolic_binding .Self [symbolic_self]
 // CHECK:STDOUT:   %empty_tuple.type: type = tuple_type () [concrete]
 // CHECK:STDOUT:   %empty_tuple: %empty_tuple.type = tuple_value () [concrete]
@@ -153,13 +155,13 @@ fn G(unused T:! type where C(()) impls I(.Self)) {}
 // CHECK:STDOUT:   %T: %I_where.type = symbolic_binding T, 0 [symbolic]
 // CHECK:STDOUT:   %PeriodSelf.type: type = fn_type @PeriodSelf [concrete]
 // CHECK:STDOUT:   %PeriodSelf: %PeriodSelf.type = struct_value () [concrete]
-// CHECK:STDOUT:   %.Self.binding.as_type: type = symbolic_binding_type .Self, %.Self.1dc [symbolic_self]
+// CHECK:STDOUT:   %.Self.binding.as_type.15d: type = symbolic_binding_type .Self, %.Self.1dc [symbolic_self]
 // CHECK:STDOUT:   %I.lookup_impl_witness: <witness> = lookup_impl_witness %.Self.1dc, @I [symbolic_self]
 // CHECK:STDOUT:   %impl.elem0: type = impl_witness_access %I.lookup_impl_witness, element0 [symbolic_self]
 // CHECK:STDOUT:   %U: %I_where.type = symbolic_binding U, 0 [symbolic]
 // CHECK:STDOUT:   %PeriodMember.type: type = fn_type @PeriodMember [concrete]
 // CHECK:STDOUT:   %PeriodMember: %PeriodMember.type = struct_value () [concrete]
-// CHECK:STDOUT:   %.Self.16f: type = symbolic_binding .Self [symbolic_self]
+// CHECK:STDOUT:   %.Self.binding.as_type.8db: type = symbolic_binding_type .Self, %.Self.c39 [symbolic_self]
 // CHECK:STDOUT:   %type_where: type = facet_type <type where .Self impls @I> [concrete]
 // CHECK:STDOUT:   %pattern_type.17f: type = pattern_type %type_where [concrete]
 // CHECK:STDOUT:   %V: %type_where = symbolic_binding V, 0 [symbolic]
@@ -192,8 +194,8 @@ fn G(unused T:! type where C(()) impls I(.Self)) {}
 // CHECK:STDOUT:       %I.ref: type = name_ref I, file.%I.decl [concrete = constants.%I.type]
 // CHECK:STDOUT:       <elided>
 // CHECK:STDOUT:       %.Self.ref: %I.type = name_ref .Self, %.Self.2 [symbolic_self = constants.%.Self.1dc]
-// CHECK:STDOUT:       %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.binding.as_type]
-// CHECK:STDOUT:       %.loc11_29: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.binding.as_type]
+// CHECK:STDOUT:       %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.binding.as_type.15d]
+// CHECK:STDOUT:       %.loc11_29: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.binding.as_type.15d]
 // CHECK:STDOUT:       %Member.ref: %I.assoc_type = name_ref Member, @Member.%assoc0 [concrete = constants.%assoc0]
 // CHECK:STDOUT:       %impl.elem0: type = impl_witness_access constants.%I.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
 // CHECK:STDOUT:       %.loc11_41: %empty_tuple.type = tuple_literal () [concrete = constants.%empty_tuple]
@@ -211,11 +213,13 @@ fn G(unused T:! type where C(()) impls I(.Self)) {}
 // CHECK:STDOUT:       <elided>
 // CHECK:STDOUT:       %.loc13_22: type = type_literal type [concrete = type]
 // CHECK:STDOUT:       <elided>
-// CHECK:STDOUT:       %.Self.ref: type = name_ref .Self, %.Self.2 [symbolic_self = constants.%.Self.16f]
+// CHECK:STDOUT:       %.Self.ref: %type = name_ref .Self, %.Self.2 [symbolic_self = constants.%.Self.c39]
 // CHECK:STDOUT:       %I.ref: type = name_ref I, file.%I.decl [concrete = constants.%I.type]
+// CHECK:STDOUT:       %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.binding.as_type.8db]
+// CHECK:STDOUT:       %.loc13_33: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.binding.as_type.8db]
 // CHECK:STDOUT:       %.loc13_27.2: type = where_expr %.Self.2 [concrete = constants.%type_where] {
 // CHECK:STDOUT:         requirement_base_facet_type type
-// CHECK:STDOUT:         requirement_impls %.Self.ref, %I.ref
+// CHECK:STDOUT:         requirement_impls %.loc13_33, %I.ref
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %V.loc13_19.2: %type_where = symbolic_binding V, 0 [symbolic = %V.loc13_19.1 (constants.%V)]

+ 2 - 2
toolchain/sem_ir/stringify.cpp

@@ -749,7 +749,7 @@ class Stringifier {
       if (some_where) {
         step_stack_->PushString(" and");
       }
-      step_stack_->Push(type_impls.self_type, " impls ",
+      step_stack_->Push(" ", type_impls.self_type, " impls ",
                         type_impls.specific_interface);
       some_where = true;
     }
@@ -758,7 +758,7 @@ class Stringifier {
       if (some_where) {
         step_stack_->PushString(" and");
       }
-      step_stack_->Push(type_impls.self_type, " impls ",
+      step_stack_->Push(" ", type_impls.self_type, " impls ",
                         type_impls.specific_named_constraint);
       some_where = true;
     }