Extended name lookup replaces inner Self (#6632)

When doing name lookup into an extended scope of an interface or named
constraint, the containing scope has an inner `Self` facet which can
appear in the specific of the extended scope. For instance a constraint
`N` which requires an interface `Z(Self)`:

```js
constraint N {
  extend require impls Z(Self);
}
```

When doing member lookup into a facet constrained by `N`, we need to
find the specific interface `Z(...)` where the `Self` is replaced by the
self-type the member lookup is happening on in order for impl lookup to
find a witness later.

Inside that specific interface we repeat the name lookup to find an
associated entity. Then to produce a witness we perform impl lookup
against the specific interface that name lookup returned with the
self-type of the member access. So if we do member access into `A:! N`
for a member `F`, like `A.F`, we would be doing impl lookup with a query
self of `A` and looking for the interface `Z(...)` returned from name
lookup.

When impl lookup has a facet as the query self, which we do here as `A`,
it takes its type (a facet type) and identifies it to find all the
required interfaces, and it substitutes the query self into those
specific interfaces for `Self`. If the `Z(...)` we acquired from name
lookup is `Z(Self)` it will fail the lookup for `A as Z(Self)`, since in
the facet type of `A` it finds a witness for `Z(A)` instead.

Thus, we replace the inner `Self` in extended scopes, such as `N`, with
the self-type of the member access, which produces the extended scope
`Z(A)` for this example. This allows the impl lookup for `A as Z(A)` to
find a witness from the facet type of `A`.

In order to do this, we include an instruction for the inner self when
registering the extended scope. Then, when we find the extended scope in
name lookup, we can use its CompileTimeBindIndex to replace any instance
of that `Self` facet with a new facet. If the self-type of member access
is a type, we construct a FacetValue with an empty facet type that
refers to the type.

toolchain/check/handle_class.cpp

@@ -403,7 +403,7 @@ auto HandleParseNode(Context& context, Parse::AdaptDeclId node_id) -> bool {
   // Extend the class scope with the adapted type's scope if requested.
   if (introducer.modifier_set.HasAnyOf(KeywordModifierSet::Extend)) {
     auto& class_scope = context.name_scopes().Get(class_info.scope_id);
-    class_scope.AddExtendedScope(adapted_type_inst_id);
+    class_scope.AddExtendedScope({adapted_type_inst_id});
   }
   return true;
 }
@@ -553,7 +553,7 @@ auto HandleParseNode(Context& context, Parse::BaseDeclId node_id) -> bool {
   if (introducer.modifier_set.HasAnyOf(KeywordModifierSet::Extend)) {
     auto& class_scope = context.name_scopes().Get(class_info.scope_id);
     if (base_info.scope_id.has_value()) {
-      class_scope.AddExtendedScope(base_info.inst_id);
+      class_scope.AddExtendedScope({base_info.inst_id});
     } else {
       class_scope.set_has_error();
     }

toolchain/check/handle_require.cpp

@@ -314,6 +314,16 @@ auto HandleParseNode(Context& context, Parse::RequireDeclId node_id) -> bool {
       return true;
     }
 
+    // The generic of a require declaration is always inside an interface or
+    // constraint, which makes its last generic binding the inner `Self` facet
+    // of the interface/constraint definition. Thus the last argument of its
+    // `self_specific` is that inner `Self`.
+    auto self_specific_id = context.generics().GetSelfSpecific(
+        context.require_impls().Get(require_impls_id).generic_id);
+    const auto& self_specific = context.specifics().Get(self_specific_id);
+    auto self_specific_args = context.inst_blocks().Get(self_specific.args_id);
+    auto inner_self_inst_id = self_specific_args.back();
+
     // The extended scope instruction must be part of the enclosing scope (and
     // generic). A specific for the enclosing scope will be applied to it when
     // using the instruction later. To do so, we wrap the constraint facet type
@@ -323,11 +333,11 @@ auto HandleParseNode(Context& context, Parse::RequireDeclId node_id) -> bool {
         context, node_id,
         {.type_id = SemIR::TypeType::TypeId,
          .inst_id = constraint_inst_id,
-         .specific_id = context.generics().GetSelfSpecific(
-             context.require_impls().Get(require_impls_id).generic_id)});
+         .specific_id = self_specific_id});
     auto enclosing_scope_id = context.scope_stack().PeekNameScopeId();
     auto& enclosing_scope = context.name_scopes().Get(enclosing_scope_id);
-    enclosing_scope.AddExtendedScope(constraint_id_in_self_specific);
+    enclosing_scope.AddExtendedScope(
+        {constraint_id_in_self_specific, inner_self_inst_id});
   }
 
   context.require_impls_stack().AppendToTop(require_impls_id);

toolchain/check/impl.cpp

@@ -236,7 +236,7 @@ static auto ApplyExtendImplAs(Context& context, SemIR::LocId loc_id,
   }
 
   if (!impl.generic_id.has_value()) {
-    parent_scope.AddExtendedScope(impl.constraint_id);
+    parent_scope.AddExtendedScope({impl.constraint_id});
   } else {
     // The extended scope instruction must be part of the enclosing scope (and
     // generic). A specific for the enclosing scope will be applied to it when
@@ -248,7 +248,7 @@ static auto ApplyExtendImplAs(Context& context, SemIR::LocId loc_id,
         {.type_id = SemIR::TypeType::TypeId,
          .inst_id = impl.constraint_id,
          .specific_id = context.generics().GetSelfSpecific(impl.generic_id)});
-    parent_scope.AddExtendedScope(constraint_id_in_self_specific);
+    parent_scope.AddExtendedScope({constraint_id_in_self_specific});
   }
   return true;
 }

toolchain/check/import_ref.cpp

@@ -475,6 +475,9 @@ class ImportRefResolver : public ImportContext {
 static auto AddImportRef(ImportContext& context, SemIR::InstId inst_id,
                          SemIR::EntityNameId entity_name_id =
                              SemIR::EntityNameId::None) -> SemIR::InstId {
+  if (!inst_id.has_value()) {
+    return SemIR::InstId::None;
+  }
   return AddImportRef(context.local_context(),
                       SemIR::ImportIRInst(context.import_ir_id(), inst_id),
                       entity_name_id);
@@ -1323,8 +1326,9 @@ static auto AddNameScopeImportRefs(ImportContext& context,
                            .result = SemIR::ScopeLookupResult::MakeFound(
                                ref_id, result.access_kind())});
   }
-  for (auto scope_inst_id : import_scope.extended_scopes()) {
-    new_scope.AddExtendedScope(AddImportRef(context, scope_inst_id));
+  for (auto [scope_inst_id, inner_self_id] : import_scope.extended_scopes()) {
+    new_scope.AddExtendedScope({AddImportRef(context, scope_inst_id),
+                                AddImportRef(context, inner_self_id)});
   }
 }
 

toolchain/check/member_access.cpp

@@ -480,58 +480,64 @@ static auto PerformActionHelper(Context& context, SemIR::LocId loc_id,
       base_const_id.is_constant()) {
     llvm::SmallVector<LookupScope> lookup_scopes;
     if (AppendLookupScopesForConstant(context, loc_id, base_const_id,
-                                      &lookup_scopes)) {
+                                      base_const_id, &lookup_scopes)) {
       return LookupMemberNameInScope(
           context, loc_id, base_id, name_id, base_const_id, lookup_scopes,
           /*lookup_in_type_of_base=*/false, required);
     }
-  }
-
-  auto base_type_id = context.insts().Get(base_id).type_id();
 
-  // If the base is a facet (a symbolic name scope), perform lookup into its
-  // facet type. This is like the class case, as there is no instance to bind.
-  //
-  // TODO: According to the design, this should just lookup directly in the
-  // `base_id` (part the class case above), as the `base_id` facet should have
-  // member names that directly name members of the `impl`.
-  if (context.types().Is<SemIR::FacetType>(base_type_id)) {
-    // Name lookup into a facet requires the facet type to be complete, so that
-    // any names available through the facet type are known for the facet.
+    // If the base is a facet (a symbolic name scope), perform lookup into its
+    // facet type.
     //
-    // TODO: This should be part of AppendLookupScopesForConstant when we do
-    // lookup on the facet directly instead of the facet type. For now it's here
-    // to provide a better diagnostic than what we get when looking for scopes
-    // directly on the facet type.
-    if (!RequireCompleteType(context, base_type_id, SemIR::LocId(base_id), [&] {
-          CARBON_DIAGNOSTIC(IncompleteTypeInMemberAccessOfFacet, Error,
-                            "member access into facet of incomplete type {0}",
-                            SemIR::TypeId);
-          return context.emitter().Build(
-              base_id, IncompleteTypeInMemberAccessOfFacet, base_type_id);
-        })) {
-      // If the scope is invalid in AppendLookupScopesForConstant we still
-      // return true and proceed with lookup, just ignoring that scope. Match
-      // behaviour here for when this moves into AppendLookupScopesForConstant.
-      base_type_id = SemIR::ErrorInst::TypeId;
-    }
+    // TODO: According to the design, this should just lookup directly in the
+    // `base_id` (as part the class case above), as the `base_id` facet should
+    // have member names that directly name members of the `impl`.
+    auto base_type_id = context.insts().Get(base_id).type_id();
+    if (context.types().Is<SemIR::FacetType>(base_type_id)) {
+      // Name lookup into a facet requires the facet type to be complete, so
+      // that any names available through the facet type are known for the
+      // facet.
+      //
+      // TODO: This should be part of AppendLookupScopesForConstant when we do
+      // lookup on the facet directly instead of the facet type. For now it's
+      // here to provide a better diagnostic than what we get when looking for
+      // scopes directly on the facet type.
+      if (!RequireCompleteType(
+              context, base_type_id, SemIR::LocId(base_id), [&] {
+                CARBON_DIAGNOSTIC(
+                    IncompleteTypeInMemberAccessOfFacet, Error,
+                    "member access into facet of incomplete type {0}",
+                    SemIR::TypeId);
+                return context.emitter().Build(
+                    base_id, IncompleteTypeInMemberAccessOfFacet, base_type_id);
+              })) {
+        // If the scope is invalid in AppendLookupScopesForConstant we still
+        // return true and proceed with lookup, just ignoring that scope. Match
+        // behaviour here for when this moves into
+        // AppendLookupScopesForConstant.
+        base_type_id = SemIR::ErrorInst::TypeId;
+      }
 
-    auto base_type_const_id = context.types().GetConstantId(base_type_id);
-    llvm::SmallVector<LookupScope> lookup_scopes;
-    if (AppendLookupScopesForConstant(context, loc_id, base_type_const_id,
-                                      &lookup_scopes)) {
-      // The name scope constant needs to be a type, but is currently a
-      // FacetType, so perform `as type` to get a FacetAccessType.
-      auto base_as_type = ExprAsType(context, loc_id, base_id);
-      base_type_const_id = context.types().GetConstantId(base_as_type.type_id);
-      return LookupMemberNameInScope(
-          context, loc_id, base_id, name_id, base_type_const_id, lookup_scopes,
-          /*lookup_in_type_of_base=*/false, required);
+      auto base_type_const_id = context.types().GetConstantId(base_type_id);
+      llvm::SmallVector<LookupScope> lookup_scopes;
+      if (AppendLookupScopesForConstant(context, loc_id, base_type_const_id,
+                                        base_const_id, &lookup_scopes)) {
+        // The name scope constant needs to be a type, but is currently a
+        // FacetType, so perform `as type` to get a FacetAccessType.
+        auto base_as_type = ExprAsType(context, loc_id, base_id);
+        base_type_const_id =
+            context.types().GetConstantId(base_as_type.type_id);
+        return LookupMemberNameInScope(context, loc_id, base_id, name_id,
+                                       base_type_const_id, lookup_scopes,
+                                       /*lookup_in_type_of_base=*/false,
+                                       required);
+      }
     }
   }
 
   // Otherwise, handle `x.F` by performing lookup into the type of `x` (where
   // `x` is `base_id`).
+  auto base_type_id = context.insts().Get(base_id).type_id();
 
   // Require a complete type explicitly. Materializing a temporary will too, but
   // we can produce a better diagnostic here with context about what operation
@@ -569,8 +575,14 @@ static auto PerformActionHelper(Context& context, SemIR::LocId loc_id,
 
   // Perform lookup into the base type.
   llvm::SmallVector<LookupScope> lookup_scopes;
-  if (AppendLookupScopesForConstant(context, loc_id, lookup_const_id,
-                                    &lookup_scopes)) {
+  if (AppendLookupScopesForConstant(
+          context, loc_id, lookup_const_id,
+          // The `self_type_const_id` should be the type of `base_id` even if
+          // it's a facet.
+          //
+          // TODO: This can be replaced with `lookup_const_id` once we stop
+          // having to look through the facet at its type for the scope.
+          context.types().GetConstantId(base_type_id), &lookup_scopes)) {
     auto member_id = LookupMemberNameInScope(
         context, loc_id, base_id, name_id, lookup_const_id, lookup_scopes,
         /*lookup_in_type_of_base=*/true, required);

toolchain/check/name_lookup.cpp

@@ -8,10 +8,13 @@
 
 #include "common/raw_string_ostream.h"
 #include "toolchain/check/cpp/import.h"
+#include "toolchain/check/facet_type.h"
 #include "toolchain/check/generic.h"
 #include "toolchain/check/import.h"
 #include "toolchain/check/import_ref.h"
+#include "toolchain/check/inst.h"
 #include "toolchain/check/member_access.h"
+#include "toolchain/check/subst.h"
 #include "toolchain/check/type.h"
 #include "toolchain/check/type_completion.h"
 #include "toolchain/diagnostics/format_providers.h"
@@ -103,11 +106,12 @@ auto LookupUnqualifiedName(Context& context, SemIR::LocId loc_id,
   // Walk the non-lexical scopes and perform lookups into each of them.
   for (auto [index, lookup_scope_id, specific_id] :
        llvm::reverse(non_lexical_scopes)) {
-    if (auto non_lexical_result =
-            LookupQualifiedName(context, loc_id, name_id,
-                                LookupScope{.name_scope_id = lookup_scope_id,
-                                            .specific_id = specific_id},
-                                /*required=*/false);
+    if (auto non_lexical_result = LookupQualifiedName(
+            context, loc_id, name_id,
+            LookupScope{.name_scope_id = lookup_scope_id,
+                        .specific_id = specific_id,
+                        .self_const_id = SemIR::ConstantId::None},
+            /*required=*/false);
         non_lexical_result.scope_result.is_found()) {
       // In an interface definition, replace associated entity `M` with
       // `Self.M` (where the `Self` is the `Self` of the interface).
@@ -284,6 +288,7 @@ struct ProhibitedAccessInfo {
 
 auto AppendLookupScopesForConstant(Context& context, SemIR::LocId loc_id,
                                    SemIR::ConstantId lookup_const_id,
+                                   SemIR::ConstantId self_type_const_id,
                                    llvm::SmallVector<LookupScope>* scopes)
     -> bool {
   auto lookup_inst_id = context.constant_values().GetInstId(lookup_const_id);
@@ -291,7 +296,8 @@ auto AppendLookupScopesForConstant(Context& context, SemIR::LocId loc_id,
 
   if (auto ns = lookup.TryAs<SemIR::Namespace>()) {
     scopes->push_back(LookupScope{.name_scope_id = ns->name_scope_id,
-                                  .specific_id = SemIR::SpecificId::None});
+                                  .specific_id = SemIR::SpecificId::None,
+                                  .self_const_id = SemIR::ConstantId::None});
     return true;
   }
   if (auto class_ty = lookup.TryAs<SemIR::ClassType>()) {
@@ -308,7 +314,8 @@ auto AppendLookupScopesForConstant(Context& context, SemIR::LocId loc_id,
         });
     auto& class_info = context.classes().Get(class_ty->class_id);
     scopes->push_back(LookupScope{.name_scope_id = class_info.scope_id,
-                                  .specific_id = class_ty->specific_id});
+                                  .specific_id = class_ty->specific_id,
+                                  .self_const_id = self_type_const_id});
     return true;
   }
   if (auto facet_type = lookup.TryAs<SemIR::FacetType>()) {
@@ -331,26 +338,30 @@ auto AppendLookupScopesForConstant(Context& context, SemIR::LocId loc_id,
       for (const auto& extend : facet_type_info.extend_constraints) {
         auto& interface = context.interfaces().Get(extend.interface_id);
         scopes->push_back({.name_scope_id = interface.scope_id,
-                           .specific_id = extend.specific_id});
+                           .specific_id = extend.specific_id,
+                           .self_const_id = self_type_const_id});
       }
       for (const auto& extend : facet_type_info.extend_named_constraints) {
         auto& constraint =
             context.named_constraints().Get(extend.named_constraint_id);
         scopes->push_back({.name_scope_id = constraint.scope_id,
-                           .specific_id = extend.specific_id});
+                           .specific_id = extend.specific_id,
+                           .self_const_id = self_type_const_id});
       }
     } else {
       // Lookup into this scope should fail without producing an error since
       // `RequireCompleteFacetType` has already issued a diagnostic.
       scopes->push_back(LookupScope{.name_scope_id = SemIR::NameScopeId::None,
-                                    .specific_id = SemIR::SpecificId::None});
+                                    .specific_id = SemIR::SpecificId::None,
+                                    .self_const_id = SemIR::ConstantId::None});
     }
     return true;
   }
   if (lookup_const_id == SemIR::ErrorInst::ConstantId) {
     // Lookup into this scope should fail without producing an error.
     scopes->push_back(LookupScope{.name_scope_id = SemIR::NameScopeId::None,
-                                  .specific_id = SemIR::SpecificId::None});
+                                  .specific_id = SemIR::SpecificId::None,
+                                  .self_const_id = SemIR::ConstantId::None});
     return true;
   }
   // TODO: Per the design, if `base_id` is any kind of type, then lookup should
@@ -410,7 +421,7 @@ auto LookupQualifiedName(Context& context, SemIR::LocId loc_id,
 
   // Walk this scope and, if nothing is found here, the scopes it extends.
   while (!scopes.empty()) {
-    auto [scope_id, specific_id] = scopes.pop_back_val();
+    auto [scope_id, specific_id, self_const_id] = scopes.pop_back_val();
     if (!scope_id.has_value()) {
       has_error = true;
       continue;
@@ -447,7 +458,7 @@ auto LookupQualifiedName(Context& context, SemIR::LocId loc_id,
       // access, look in its extended scopes.
       const auto& extended = name_scope.extended_scopes();
       scopes.reserve(scopes.size() + extended.size());
-      for (auto extended_id : llvm::reverse(extended)) {
+      for (auto [extended_id, inner_self_id] : llvm::reverse(extended)) {
         // Substitute into the constant describing the extended scope to
         // determine its corresponding specific.
         CARBON_CHECK(extended_id.has_value());
@@ -455,8 +466,45 @@ auto LookupQualifiedName(Context& context, SemIR::LocId loc_id,
         SemIR::ConstantId const_id = GetConstantValueInSpecific(
             context.sem_ir(), specific_id, extended_id);
 
+        // Apply self_const_id to the extended_id, replacing inner_self_id
+        // inside.
+        //
+        // TODO: We do this by substituting a `Self` value that the extended
+        // scope provides us with the self type/facet of the name lookup. But
+        // we'd like to avoid using substitution, and do this through the
+        // generic system with a specific and/or eval. Ideally it's somehow done
+        // as part of the `GetConstantValueInSpecific` call above, but with
+        // providing the additional information of the self type/facet of the
+        // name lookup. Further thoughts here:
+        // https://discord.com/channels/655572317891461132/941071822756143115/1463277684082737214
+        if (inner_self_id.has_value() && self_const_id.has_value()) {
+          LoadImportRef(context, inner_self_id);
+
+          auto inner_self_binding =
+              context.insts().GetAs<SemIR::SymbolicBinding>(
+                  context.constant_values().GetConstantInstId(inner_self_id));
+          auto entity_id = inner_self_binding.entity_name_id;
+          auto bind_index = context.entity_names().Get(entity_id).bind_index();
+          auto facet_value = SemIR::ConstantId::None;
+          if (auto self_type_id =
+                  context.types().TryGetTypeIdForTypeConstantId(self_const_id);
+              self_type_id.has_value()) {
+            // The self for member lookup is a type, we need a facet value to
+            // replace `Self`.
+            facet_value = GetConstantFacetValueForType(
+                context, context.types().GetInstId(self_type_id));
+          } else {
+            // The self for member lookup is a facet value, use it as is to
+            // replace `Self`.
+            facet_value = self_const_id;
+          }
+          llvm::SmallVector<Substitution> substitutions = {
+              {.bind_id = bind_index, .replacement_id = facet_value}};
+          const_id = SubstConstant(context, loc_id, const_id, substitutions);
+        }
+
         if (!AppendLookupScopesForConstant(context, loc_id, const_id,
-                                           &scopes)) {
+                                           self_const_id, &scopes)) {
           // TODO: Handle case where we have a symbolic type and instead should
           // look in its type.
         }

toolchain/check/name_lookup.h

@@ -20,6 +20,9 @@ struct LookupScope {
   // The specific for the name scope, or `None` if the name scope is not
   // defined by a generic or we should perform lookup into the generic itself.
   SemIR::SpecificId specific_id;
+  // The self-type where lookup is happening when the lookup is for a member
+  // access.
+  SemIR::ConstantId self_const_id;
 };
 
 // A result produced by name lookup.
@@ -79,10 +82,18 @@ auto LookupNameInExactScope(Context& context, SemIR::LocId loc_id,
     -> SemIR::ScopeLookupResult;
 
 // Appends the lookup scopes corresponding to `lookup_const_id` to `*scopes`.
+//
+// The `self_type_const_id` is the self-type that we are looking for a name in,
+// and which is passed through to extended scopes. It may be a facet or a value
+// of type `type`. Some extended scopes have a symbolic `Self` internally which
+// needs to know the self-type in order to produce a correct specific scope in
+// the result.
+//
 // Returns `false` if not a scope. On invalid scopes, prints a diagnostic, but
 // still updates `*scopes` and returns `true`.
 auto AppendLookupScopesForConstant(Context& context, SemIR::LocId loc_id,
                                    SemIR::ConstantId lookup_const_id,
+                                   SemIR::ConstantId self_type_const_id,
                                    llvm::SmallVector<LookupScope>* scopes)
     -> bool;
 

toolchain/check/testdata/facet/require_import.carbon

@@ -13,21 +13,42 @@
 // --- a.carbon
 library "[[@TEST_NAME]]";
 
-interface Z {}
+interface Z(T:! type) {
+  fn F();
+}
 
 interface Y {
-  require impls Z;
+  extend require impls Z(Self);
 }
 
 constraint X {
-  extend require impls Z;
+  extend require impls Z(Self);
 }
 
 // --- a.impl.carbon
 //@include-in-dumps
 impl library "[[@TEST_NAME]]";
 
-fn F(A:! X, B:! Y) {}
+fn F(A:! X, B:! Y) {
+  A.F();
+}
+
+// --- fail_todo_symbolic_facet_interface_requires_interface.carbon
+library "[[@TEST_NAME]]";
+
+import library "a";
+
+fn F(B:! Y) {
+  // TODO: We find the name F, but then fail to do impl lookup for `F` in `B:!
+  // Y` since the identified facet type doesn't include Z. We need to be able to
+  // find a symbolic facet from the require decl in Y during impl lookup.
+  //
+  // CHECK:STDERR: fail_todo_symbolic_facet_interface_requires_interface.carbon:[[@LINE+4]]:3: error: cannot access member of interface `Z(B)` in type `B` that does not implement that interface [MissingImplInMemberAccess]
+  // CHECK:STDERR:   B.F();
+  // CHECK:STDERR:   ^~~
+  // CHECK:STDERR:
+  B.F();
+}
 
 // CHECK:STDOUT: --- a.impl.carbon
 // CHECK:STDOUT:
@@ -36,33 +57,76 @@ fn F(A:! X, B:! Y) {}
 // CHECK:STDOUT:   %.Self: %type = symbolic_binding .Self [symbolic_self]
 // CHECK:STDOUT:   %X.type: type = facet_type <@X> [concrete]
 // CHECK:STDOUT:   %Self.f45: %X.type = symbolic_binding Self, 0 [symbolic]
-// CHECK:STDOUT:   %Z.type: type = facet_type <@Z> [concrete]
 // CHECK:STDOUT:   %Self.binding.as_type.f60: type = symbolic_binding_type Self, 0, %Self.f45 [symbolic]
+// CHECK:STDOUT:   %empty_tuple.type: type = tuple_type () [concrete]
+// CHECK:STDOUT:   %T: type = symbolic_binding T, 0 [symbolic]
+// CHECK:STDOUT:   %Z.type.0ed: type = facet_type <@Z, @Z(%T)> [symbolic]
+// CHECK:STDOUT:   %Self.984: %Z.type.0ed = symbolic_binding Self, 1 [symbolic]
+// CHECK:STDOUT:   %Z.assoc_type.0bf: type = assoc_entity_type @Z, @Z(%T) [symbolic]
+// CHECK:STDOUT:   %assoc0.f88: %Z.assoc_type.0bf = assoc_entity element0, imports.%Main.import_ref.f14 [symbolic]
+// CHECK:STDOUT:   %Z.F.type.6cb: type = fn_type @Z.F, @Z(%T) [symbolic]
+// CHECK:STDOUT:   %Z.F.6cc: %Z.F.type.6cb = struct_value () [symbolic]
+// CHECK:STDOUT:   %Z.type.9f3244.1: type = facet_type <@Z, @Z(%Self.binding.as_type.f60)> [symbolic]
+// CHECK:STDOUT:   %Z.assoc_type.449133.1: type = assoc_entity_type @Z, @Z(%Self.binding.as_type.f60) [symbolic]
+// CHECK:STDOUT:   %assoc0.179: %Z.assoc_type.449133.1 = assoc_entity element0, imports.%Main.import_ref.5847cb.1 [symbolic]
+// CHECK:STDOUT:   %Z.F.type.0ab8e8.1: type = fn_type @Z.F, @Z(%Self.binding.as_type.f60) [symbolic]
+// CHECK:STDOUT:   %Z.F.d97fe5.1: %Z.F.type.0ab8e8.1 = struct_value () [symbolic]
+// CHECK:STDOUT:   %Self.fcd60c.1: %Z.type.9f3244.1 = symbolic_binding Self, 1 [symbolic]
 // CHECK:STDOUT:   %A: %X.type = symbolic_binding A, 0 [symbolic]
 // CHECK:STDOUT:   %pattern_type.9a5: type = pattern_type %X.type [concrete]
 // CHECK:STDOUT:   %Y.type: type = facet_type <@Y> [concrete]
 // CHECK:STDOUT:   %Self.d4d: %Y.type = symbolic_binding Self, 0 [symbolic]
 // CHECK:STDOUT:   %Self.binding.as_type.63e: type = symbolic_binding_type Self, 0, %Self.d4d [symbolic]
+// CHECK:STDOUT:   %Z.type.d16: type = facet_type <@Z, @Z(%Self.binding.as_type.63e)> [symbolic]
+// CHECK:STDOUT:   %Z.assoc_type.df3: type = assoc_entity_type @Z, @Z(%Self.binding.as_type.63e) [symbolic]
+// CHECK:STDOUT:   %assoc0.e61: %Z.assoc_type.df3 = assoc_entity element0, imports.%Main.import_ref.5847cb.2 [symbolic]
+// CHECK:STDOUT:   %Z.F.type.388: type = fn_type @Z.F, @Z(%Self.binding.as_type.63e) [symbolic]
+// CHECK:STDOUT:   %Z.F.791: %Z.F.type.388 = struct_value () [symbolic]
+// CHECK:STDOUT:   %Self.890: %Z.type.d16 = symbolic_binding Self, 1 [symbolic]
 // CHECK:STDOUT:   %B: %Y.type = symbolic_binding B, 1 [symbolic]
 // CHECK:STDOUT:   %pattern_type.95b: type = pattern_type %Y.type [concrete]
 // CHECK:STDOUT:   %F.type: type = fn_type @F [concrete]
 // CHECK:STDOUT:   %F: %F.type = struct_value () [concrete]
+// CHECK:STDOUT:   %A.binding.as_type: type = symbolic_binding_type A, 0, %A [symbolic]
+// CHECK:STDOUT:   %Z.type.9f3244.2: type = facet_type <@Z, @Z(%A.binding.as_type)> [symbolic]
+// CHECK:STDOUT:   %Self.fcd60c.2: %Z.type.9f3244.2 = symbolic_binding Self, 1 [symbolic]
+// CHECK:STDOUT:   %Z.F.type.0ab8e8.2: type = fn_type @Z.F, @Z(%A.binding.as_type) [symbolic]
+// CHECK:STDOUT:   %Z.F.d97fe5.2: %Z.F.type.0ab8e8.2 = struct_value () [symbolic]
+// CHECK:STDOUT:   %Z.assoc_type.449133.2: type = assoc_entity_type @Z, @Z(%A.binding.as_type) [symbolic]
+// CHECK:STDOUT:   %assoc0.f48: %Z.assoc_type.449133.2 = assoc_entity element0, imports.%Main.import_ref.f14 [symbolic]
+// CHECK:STDOUT:   %require_complete: <witness> = require_complete_type %Z.type.9f3244.2 [symbolic]
+// CHECK:STDOUT:   %assoc0.d5a: %Z.assoc_type.0bf = assoc_entity element0, imports.%Main.import_ref.5847cb.3 [symbolic]
+// CHECK:STDOUT:   %Z.lookup_impl_witness: <witness> = lookup_impl_witness %A, @Z, @Z(%A.binding.as_type) [symbolic]
+// CHECK:STDOUT:   %Z.facet: %Z.type.9f3244.2 = facet_value %A.binding.as_type, (%Z.lookup_impl_witness) [symbolic]
+// CHECK:STDOUT:   %.168: type = fn_type_with_self_type %Z.F.type.0ab8e8.2, %Z.facet [symbolic]
+// CHECK:STDOUT:   %impl.elem0: %.168 = impl_witness_access %Z.lookup_impl_witness, element0 [symbolic]
+// CHECK:STDOUT:   %specific_impl_fn: <specific function> = specific_impl_function %impl.elem0, @Z.F(%A.binding.as_type, %Z.facet) [symbolic]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: imports {
 // CHECK:STDOUT:   %Main.Z = import_ref Main//a, Z, unloaded
 // CHECK:STDOUT:   %Main.Y: type = import_ref Main//a, Y, loaded [concrete = constants.%Y.type]
 // CHECK:STDOUT:   %Main.X: type = import_ref Main//a, X, loaded [concrete = constants.%X.type]
-// CHECK:STDOUT:   %Main.import_ref.69e = import_ref Main//a, loc3_13, unloaded
-// CHECK:STDOUT:   %Main.import_ref.67f: type = import_ref Main//a, loc10_18, loaded [symbolic = @X.Self.binding.as_type.impls.Z.type.require.%Self.binding.as_type (constants.%Self.binding.as_type.f60)]
-// CHECK:STDOUT:   %Main.import_ref.926bc7.1: type = import_ref Main//a, loc10_24, loaded [concrete = constants.%Z.type]
-// CHECK:STDOUT:   %Main.import_ref.e33: %X.type = import_ref Main//a, loc9_14, loaded [symbolic = constants.%Self.f45]
-// CHECK:STDOUT:   %Main.import_ref.65b = import_ref Main//a, loc9_14, unloaded
-// CHECK:STDOUT:   %Main.import_ref.1c5 = import_ref Main//a, loc10_25, unloaded
-// CHECK:STDOUT:   %Main.import_ref.7bb: type = import_ref Main//a, loc6_11, loaded [symbolic = @Y.Self.binding.as_type.impls.Z.type.require.%Self.binding.as_type (constants.%Self.binding.as_type.63e)]
-// CHECK:STDOUT:   %Main.import_ref.926bc7.2: type = import_ref Main//a, loc6_17, loaded [concrete = constants.%Z.type]
-// CHECK:STDOUT:   %Main.import_ref.8c7: %Y.type = import_ref Main//a, loc5_13, loaded [symbolic = constants.%Self.d4d]
-// CHECK:STDOUT:   %Main.import_ref.3e2 = import_ref Main//a, loc5_13, unloaded
+// CHECK:STDOUT:   %Main.import_ref.145 = import_ref Main//a, loc3_23, unloaded
+// CHECK:STDOUT:   %Main.import_ref.f4a: @Z.%Z.assoc_type (%Z.assoc_type.0bf) = import_ref Main//a, loc4_9, loaded [symbolic = @Z.%assoc0 (constants.%assoc0.d5a)]
+// CHECK:STDOUT:   %Main.F = import_ref Main//a, F, unloaded
+// CHECK:STDOUT:   %Main.import_ref.b3bc94.1: type = import_ref Main//a, loc3_13, loaded [symbolic = @Z.%T (constants.%T)]
+// CHECK:STDOUT:   %Main.import_ref.f14: @Z.%Z.F.type (%Z.F.type.6cb) = import_ref Main//a, loc4_9, loaded [symbolic = @Z.%Z.F (constants.%Z.F.6cc)]
+// CHECK:STDOUT:   %Main.import_ref.b3bc94.2: type = import_ref Main//a, loc3_13, loaded [symbolic = @Z.%T (constants.%T)]
+// CHECK:STDOUT:   %Main.import_ref.1dc: @Z.%Z.type (%Z.type.0ed) = import_ref Main//a, loc3_23, loaded [symbolic = @Z.%Self (constants.%Self.984)]
+// CHECK:STDOUT:   %Main.import_ref.5847cb.1 = import_ref Main//a, loc4_9, unloaded
+// CHECK:STDOUT:   %Main.import_ref.67f: type = import_ref Main//a, loc12_18, loaded [symbolic = @X.Self.binding.as_type.impls.Z.type.require.%Self.binding.as_type (constants.%Self.binding.as_type.f60)]
+// CHECK:STDOUT:   %Main.import_ref.8d6: type = import_ref Main//a, loc12_30, loaded [symbolic = @X.Self.binding.as_type.impls.Z.type.require.%Z.type (constants.%Z.type.9f3244.1)]
+// CHECK:STDOUT:   %Main.import_ref.e33cd1.1: %X.type = import_ref Main//a, loc11_14, loaded [symbolic = constants.%Self.f45]
+// CHECK:STDOUT:   %Main.import_ref.65b = import_ref Main//a, loc11_14, unloaded
+// CHECK:STDOUT:   %Main.import_ref.f88: type = import_ref Main//a, loc12_31, loaded [symbolic = constants.%Z.type.9f3244.1]
+// CHECK:STDOUT:   %Main.import_ref.5847cb.2 = import_ref Main//a, loc4_9, unloaded
+// CHECK:STDOUT:   %Main.import_ref.7bb: type = import_ref Main//a, loc8_18, loaded [symbolic = @Y.Self.binding.as_type.impls.Z.type.require.%Self.binding.as_type (constants.%Self.binding.as_type.63e)]
+// CHECK:STDOUT:   %Main.import_ref.5ab: type = import_ref Main//a, loc8_30, loaded [symbolic = @Y.Self.binding.as_type.impls.Z.type.require.%Z.type (constants.%Z.type.d16)]
+// CHECK:STDOUT:   %Main.import_ref.8c7: %Y.type = import_ref Main//a, loc7_13, loaded [symbolic = constants.%Self.d4d]
+// CHECK:STDOUT:   %Main.import_ref.3e2c97.1 = import_ref Main//a, loc7_13, unloaded
+// CHECK:STDOUT:   %Main.import_ref.80a = import_ref Main//a, loc8_31, unloaded
+// CHECK:STDOUT:   %Main.import_ref.5847cb.3 = import_ref Main//a, loc4_9, unloaded
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
@@ -91,44 +155,65 @@ fn F(A:! X, B:! Y) {}
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: interface @Z [from "a.carbon"] {
-// CHECK:STDOUT: !members:
-// CHECK:STDOUT:   .Self = imports.%Main.import_ref.69e
-// CHECK:STDOUT:   witness = ()
+// CHECK:STDOUT: generic interface @Z(imports.%Main.import_ref.b3bc94.1: type) [from "a.carbon"] {
+// CHECK:STDOUT:   %T: type = symbolic_binding T, 0 [symbolic = %T (constants.%T)]
 // CHECK:STDOUT:
-// CHECK:STDOUT: !requires:
+// CHECK:STDOUT: !definition:
+// CHECK:STDOUT:   %Z.type: type = facet_type <@Z, @Z(%T)> [symbolic = %Z.type (constants.%Z.type.0ed)]
+// CHECK:STDOUT:   %Self: @Z.%Z.type (%Z.type.0ed) = symbolic_binding Self, 1 [symbolic = %Self (constants.%Self.984)]
+// CHECK:STDOUT:   %Z.F.type: type = fn_type @Z.F, @Z(%T) [symbolic = %Z.F.type (constants.%Z.F.type.6cb)]
+// CHECK:STDOUT:   %Z.F: @Z.%Z.F.type (%Z.F.type.6cb) = struct_value () [symbolic = %Z.F (constants.%Z.F.6cc)]
+// CHECK:STDOUT:   %Z.assoc_type: type = assoc_entity_type @Z, @Z(%T) [symbolic = %Z.assoc_type (constants.%Z.assoc_type.0bf)]
+// CHECK:STDOUT:   %assoc0: @Z.%Z.assoc_type (%Z.assoc_type.0bf) = assoc_entity element0, imports.%Main.import_ref.f14 [symbolic = %assoc0 (constants.%assoc0.f88)]
+// CHECK:STDOUT:
+// CHECK:STDOUT:   interface {
+// CHECK:STDOUT:   !members:
+// CHECK:STDOUT:     .Self = imports.%Main.import_ref.145
+// CHECK:STDOUT:     .F = imports.%Main.import_ref.f4a
+// CHECK:STDOUT:     witness = (imports.%Main.F)
+// CHECK:STDOUT:
+// CHECK:STDOUT:   !requires:
+// CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: interface @Y [from "a.carbon"] {
 // CHECK:STDOUT: !members:
-// CHECK:STDOUT:   .Self = imports.%Main.import_ref.3e2
+// CHECK:STDOUT:   .Self = imports.%Main.import_ref.3e2c97.1
+// CHECK:STDOUT:   extend imports.%Main.import_ref.80a
 // CHECK:STDOUT:   witness = ()
 // CHECK:STDOUT:
 // CHECK:STDOUT: !requires:
 // CHECK:STDOUT:   @Y.Self.binding.as_type.impls.Z.type.require {
-// CHECK:STDOUT:     require imports.%Main.import_ref.7bb impls imports.%Main.import_ref.926bc7.2
+// CHECK:STDOUT:     require imports.%Main.import_ref.7bb impls imports.%Main.import_ref.5ab
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: constraint @X [from "a.carbon"] {
 // CHECK:STDOUT: !members:
 // CHECK:STDOUT:   .Self = imports.%Main.import_ref.65b
-// CHECK:STDOUT:   extend imports.%Main.import_ref.1c5
+// CHECK:STDOUT:   .F = <poisoned>
+// CHECK:STDOUT:   extend imports.%Main.import_ref.f88
 // CHECK:STDOUT:
 // CHECK:STDOUT: !requires:
 // CHECK:STDOUT:   @X.Self.binding.as_type.impls.Z.type.require {
-// CHECK:STDOUT:     require imports.%Main.import_ref.67f impls imports.%Main.import_ref.926bc7.1
+// CHECK:STDOUT:     require imports.%Main.import_ref.67f impls imports.%Main.import_ref.8d6
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: generic require @X.Self.binding.as_type.impls.Z.type.require(imports.%Main.import_ref.e33: %X.type) [from "a.carbon"] {
+// CHECK:STDOUT: generic require @X.Self.binding.as_type.impls.Z.type.require(imports.%Main.import_ref.e33cd1.1: %X.type) [from "a.carbon"] {
 // CHECK:STDOUT:   %Self: %X.type = symbolic_binding Self, 0 [symbolic = %Self (constants.%Self.f45)]
 // CHECK:STDOUT:   %Self.binding.as_type: type = symbolic_binding_type Self, 0, %Self [symbolic = %Self.binding.as_type (constants.%Self.binding.as_type.f60)]
+// CHECK:STDOUT:   %Z.type: type = facet_type <@Z, @Z(%Self.binding.as_type)> [symbolic = %Z.type (constants.%Z.type.9f3244.1)]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: generic require @Y.Self.binding.as_type.impls.Z.type.require(imports.%Main.import_ref.8c7: %Y.type) [from "a.carbon"] {
 // CHECK:STDOUT:   %Self: %Y.type = symbolic_binding Self, 0 [symbolic = %Self (constants.%Self.d4d)]
 // CHECK:STDOUT:   %Self.binding.as_type: type = symbolic_binding_type Self, 0, %Self [symbolic = %Self.binding.as_type (constants.%Self.binding.as_type.63e)]
+// CHECK:STDOUT:   %Z.type: type = facet_type <@Z, @Z(%Self.binding.as_type)> [symbolic = %Z.type (constants.%Z.type.d16)]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: generic fn @Z.F(imports.%Main.import_ref.b3bc94.2: type, imports.%Main.import_ref.1dc: @Z.%Z.type (%Z.type.0ed)) [from "a.carbon"] {
+// CHECK:STDOUT:   fn;
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: generic fn @F(%A.loc4_6.2: %X.type, %B.loc4_13.2: %Y.type) {
@@ -136,21 +221,72 @@ fn F(A:! X, B:! Y) {}
 // CHECK:STDOUT:   %B.loc4_13.1: %Y.type = symbolic_binding B, 1 [symbolic = %B.loc4_13.1 (constants.%B)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
+// CHECK:STDOUT:   %A.binding.as_type: type = symbolic_binding_type A, 0, %A.loc4_6.1 [symbolic = %A.binding.as_type (constants.%A.binding.as_type)]
+// CHECK:STDOUT:   %Z.type: type = facet_type <@Z, @Z(%A.binding.as_type)> [symbolic = %Z.type (constants.%Z.type.9f3244.2)]
+// CHECK:STDOUT:   %require_complete: <witness> = require_complete_type %Z.type [symbolic = %require_complete (constants.%require_complete)]
+// CHECK:STDOUT:   %Z.assoc_type: type = assoc_entity_type @Z, @Z(%A.binding.as_type) [symbolic = %Z.assoc_type (constants.%Z.assoc_type.449133.2)]
+// CHECK:STDOUT:   %assoc0: @F.%Z.assoc_type (%Z.assoc_type.449133.2) = assoc_entity element0, imports.%Main.import_ref.f14 [symbolic = %assoc0 (constants.%assoc0.f48)]
+// CHECK:STDOUT:   %Z.lookup_impl_witness: <witness> = lookup_impl_witness %A.loc4_6.1, @Z, @Z(%A.binding.as_type) [symbolic = %Z.lookup_impl_witness (constants.%Z.lookup_impl_witness)]
+// CHECK:STDOUT:   %Z.F.type: type = fn_type @Z.F, @Z(%A.binding.as_type) [symbolic = %Z.F.type (constants.%Z.F.type.0ab8e8.2)]
+// CHECK:STDOUT:   %Z.facet: @F.%Z.type (%Z.type.9f3244.2) = facet_value %A.binding.as_type, (%Z.lookup_impl_witness) [symbolic = %Z.facet (constants.%Z.facet)]
+// CHECK:STDOUT:   %.loc5_4.3: type = fn_type_with_self_type %Z.F.type, %Z.facet [symbolic = %.loc5_4.3 (constants.%.168)]
+// CHECK:STDOUT:   %impl.elem0.loc5_4.2: @F.%.loc5_4.3 (%.168) = impl_witness_access %Z.lookup_impl_witness, element0 [symbolic = %impl.elem0.loc5_4.2 (constants.%impl.elem0)]
+// CHECK:STDOUT:   %specific_impl_fn.loc5_4.2: <specific function> = specific_impl_function %impl.elem0.loc5_4.2, @Z.F(%A.binding.as_type, %Z.facet) [symbolic = %specific_impl_fn.loc5_4.2 (constants.%specific_impl_fn)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   fn() {
 // CHECK:STDOUT:   !entry:
+// CHECK:STDOUT:     %A.ref: %X.type = name_ref A, %A.loc4_6.2 [symbolic = %A.loc4_6.1 (constants.%A)]
+// CHECK:STDOUT:     %A.as_type: type = facet_access_type %A.ref [symbolic = %A.binding.as_type (constants.%A.binding.as_type)]
+// CHECK:STDOUT:     %.loc5_4.1: type = converted %A.ref, %A.as_type [symbolic = %A.binding.as_type (constants.%A.binding.as_type)]
+// CHECK:STDOUT:     %.loc5_4.2: @F.%Z.assoc_type (%Z.assoc_type.449133.2) = specific_constant imports.%Main.import_ref.f4a, @Z(constants.%A.binding.as_type) [symbolic = %assoc0 (constants.%assoc0.f48)]
+// CHECK:STDOUT:     %F.ref: @F.%Z.assoc_type (%Z.assoc_type.449133.2) = name_ref F, %.loc5_4.2 [symbolic = %assoc0 (constants.%assoc0.f48)]
+// CHECK:STDOUT:     %impl.elem0.loc5_4.1: @F.%.loc5_4.3 (%.168) = impl_witness_access constants.%Z.lookup_impl_witness, element0 [symbolic = %impl.elem0.loc5_4.2 (constants.%impl.elem0)]
+// CHECK:STDOUT:     %specific_impl_fn.loc5_4.1: <specific function> = specific_impl_function %impl.elem0.loc5_4.1, @Z.F(constants.%A.binding.as_type, constants.%Z.facet) [symbolic = %specific_impl_fn.loc5_4.2 (constants.%specific_impl_fn)]
+// CHECK:STDOUT:     %Z.F.call: init %empty_tuple.type = call %specific_impl_fn.loc5_4.1()
 // CHECK:STDOUT:     return
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
+// CHECK:STDOUT: specific @Z(constants.%T) {
+// CHECK:STDOUT:   %T => constants.%T
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @Z.F(constants.%T, constants.%Self.984) {}
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @Z(constants.%Self.binding.as_type.f60) {
+// CHECK:STDOUT:   %T => constants.%Self.binding.as_type.f60
+// CHECK:STDOUT:
+// CHECK:STDOUT: !definition:
+// CHECK:STDOUT:   %Z.type => constants.%Z.type.9f3244.1
+// CHECK:STDOUT:   %Self => constants.%Self.fcd60c.1
+// CHECK:STDOUT:   %Z.F.type => constants.%Z.F.type.0ab8e8.1
+// CHECK:STDOUT:   %Z.F => constants.%Z.F.d97fe5.1
+// CHECK:STDOUT:   %Z.assoc_type => constants.%Z.assoc_type.449133.1
+// CHECK:STDOUT:   %assoc0 => constants.%assoc0.179
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
 // CHECK:STDOUT: specific @X.Self.binding.as_type.impls.Z.type.require(constants.%Self.f45) {
 // CHECK:STDOUT:   %Self => constants.%Self.f45
 // CHECK:STDOUT:   %Self.binding.as_type => constants.%Self.binding.as_type.f60
+// CHECK:STDOUT:   %Z.type => constants.%Z.type.9f3244.1
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @Z(constants.%Self.binding.as_type.63e) {
+// CHECK:STDOUT:   %T => constants.%Self.binding.as_type.63e
+// CHECK:STDOUT:
+// CHECK:STDOUT: !definition:
+// CHECK:STDOUT:   %Z.type => constants.%Z.type.d16
+// CHECK:STDOUT:   %Self => constants.%Self.890
+// CHECK:STDOUT:   %Z.F.type => constants.%Z.F.type.388
+// CHECK:STDOUT:   %Z.F => constants.%Z.F.791
+// CHECK:STDOUT:   %Z.assoc_type => constants.%Z.assoc_type.df3
+// CHECK:STDOUT:   %assoc0 => constants.%assoc0.e61
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @Y.Self.binding.as_type.impls.Z.type.require(constants.%Self.d4d) {
 // CHECK:STDOUT:   %Self => constants.%Self.d4d
 // CHECK:STDOUT:   %Self.binding.as_type => constants.%Self.binding.as_type.63e
+// CHECK:STDOUT:   %Z.type => constants.%Z.type.d16
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @F(constants.%A, constants.%B) {
@@ -158,3 +294,23 @@ fn F(A:! X, B:! Y) {}
 // CHECK:STDOUT:   %B.loc4_13.1 => constants.%B
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
+// CHECK:STDOUT: specific @Z(constants.%A.binding.as_type) {
+// CHECK:STDOUT:   %T => constants.%A.binding.as_type
+// CHECK:STDOUT:
+// CHECK:STDOUT: !definition:
+// CHECK:STDOUT:   %Z.type => constants.%Z.type.9f3244.2
+// CHECK:STDOUT:   %Self => constants.%Self.fcd60c.2
+// CHECK:STDOUT:   %Z.F.type => constants.%Z.F.type.0ab8e8.2
+// CHECK:STDOUT:   %Z.F => constants.%Z.F.d97fe5.2
+// CHECK:STDOUT:   %Z.assoc_type => constants.%Z.assoc_type.449133.2
+// CHECK:STDOUT:   %assoc0 => constants.%assoc0.f48
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @X.Self.binding.as_type.impls.Z.type.require(constants.%A) {
+// CHECK:STDOUT:   %Self => constants.%A
+// CHECK:STDOUT:   %Self.binding.as_type => constants.%A.binding.as_type
+// CHECK:STDOUT:   %Z.type => constants.%Z.type.9f3244.2
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @Z.F(constants.%A.binding.as_type, constants.%Z.facet) {}
+// CHECK:STDOUT:

toolchain/check/testdata/facet/runtime_value.carbon

@@ -72,7 +72,11 @@ interface Z {
   let X:! type;
 }
 
-// CHECK:STDERR: fail_member_lookup_in_runtime_facet_without_value.carbon:[[@LINE+4]]:15: error: cannot evaluate type expression [TypeExprEvaluationFailure]
+// TODO: Improve this diagnostic. The problem is that T is a runtime facet
+// _and_ its facet type doesn't specific a value for `.X`. Or make this work
+// by producing an ImplWitnessAccess that functions against a runtime facet.
+//
+// CHECK:STDERR: fail_member_lookup_in_runtime_facet_without_value.carbon:[[@LINE+4]]:15: error: cannot access member of interface `Z` in type `Z` that does not implement that interface [MissingImplInMemberAccess]
 // CHECK:STDERR: fn F(T: Z, v: T.X);
 // CHECK:STDERR:               ^~~
 // CHECK:STDERR:
@@ -104,7 +108,7 @@ interface Z {
 // TODO: We should be able to get the value of `.X` from the `FacetType` of
 // `T`.
 //
-// CHECK:STDERR: fail_todo_member_lookup_in_runtime_facet_with_value.carbon:[[@LINE+4]]:29: error: cannot evaluate type expression [TypeExprEvaluationFailure]
+// CHECK:STDERR: fail_todo_member_lookup_in_runtime_facet_with_value.carbon:[[@LINE+4]]:29: error: cannot access member of interface `Z` in type `Z where .(Z.X) = ()` that does not implement that interface [MissingImplInMemberAccess]
 // CHECK:STDERR: fn F(T: Z where .X = (), v: T.X);
 // CHECK:STDERR:                             ^~~
 // CHECK:STDERR:
@@ -118,7 +122,7 @@ interface Z {
 }
 
 fn F(T: Z) {
-  // CHECK:STDERR: fail_todo_member_lookup_in_type_of_runtime_facet_with_value.carbon:[[@LINE+4]]:3: error: cannot evaluate type expression [TypeExprEvaluationFailure]
+  // CHECK:STDERR: fail_todo_member_lookup_in_type_of_runtime_facet_with_value.carbon:[[@LINE+4]]:3: error: cannot access member of interface `Z` in type `Z` that does not implement that interface [MissingImplInMemberAccess]
   // CHECK:STDERR:   T.G();
   // CHECK:STDERR:   ^~~
   // CHECK:STDERR:

toolchain/check/testdata/impl/import_generic.carbon

@@ -342,7 +342,7 @@ impl forall [T:! type] D as N(T*) {}
 // CHECK:STDOUT:   %Main.import_ref.358: type = import_ref Main//basic_import_generic_interface, loc5_27, loaded [symbolic = @J.Self.binding.as_type.impls.I.type.require.%I.type (constants.%I.type.1ab)]
 // CHECK:STDOUT:   %Main.import_ref.b3bc94.2: type = import_ref Main//basic_import_generic_interface, loc4_13, loaded [symbolic = @J.%T (constants.%T)]
 // CHECK:STDOUT:   %Main.import_ref.99f: @J.%J.type (%J.type.04e) = import_ref Main//basic_import_generic_interface, loc4_23, loaded [symbolic = @J.%Self (constants.%Self.c25)]
-// CHECK:STDOUT:   %Main.import_ref.e9b = import_ref Main//basic_import_generic_interface, loc4_23, unloaded
+// CHECK:STDOUT:   %Main.import_ref.e9be38.1 = import_ref Main//basic_import_generic_interface, loc4_23, unloaded
 // CHECK:STDOUT:   %Main.import_ref.b55 = import_ref Main//basic_import_generic_interface, loc5_28, unloaded
 // CHECK:STDOUT:   %Main.import_ref.b3bc94.3: type = import_ref Main//basic_import_generic_interface, loc4_13, loaded [symbolic = @J.%T (constants.%T)]
 // CHECK:STDOUT: }
@@ -399,7 +399,7 @@ impl forall [T:! type] D as N(T*) {}
 // CHECK:STDOUT:
 // CHECK:STDOUT:   interface {
 // CHECK:STDOUT:   !members:
-// CHECK:STDOUT:     .Self = imports.%Main.import_ref.e9b
+// CHECK:STDOUT:     .Self = imports.%Main.import_ref.e9be38.1
 // CHECK:STDOUT:     extend imports.%Main.import_ref.b55
 // CHECK:STDOUT:     witness = ()
 // CHECK:STDOUT:
@@ -641,7 +641,7 @@ impl forall [T:! type] D as N(T*) {}
 // CHECK:STDOUT:   %Main.import_ref.358: type = import_ref Main//basic_import_generic_constraint, loc5_27, loaded [symbolic = @J.Self.binding.as_type.impls.I.type.require.%I.type (constants.%I.type.1ab)]
 // CHECK:STDOUT:   %Main.import_ref.b3bc94.2: type = import_ref Main//basic_import_generic_constraint, loc4_14, loaded [symbolic = @J.%T (constants.%T)]
 // CHECK:STDOUT:   %Main.import_ref.2fc: @J.%J.type (%J.type.d682d6.1) = import_ref Main//basic_import_generic_constraint, loc4_24, loaded [symbolic = @J.%Self (constants.%Self.e1f642.1)]
-// CHECK:STDOUT:   %Main.import_ref.830 = import_ref Main//basic_import_generic_constraint, loc4_24, unloaded
+// CHECK:STDOUT:   %Main.import_ref.830896.1 = import_ref Main//basic_import_generic_constraint, loc4_24, unloaded
 // CHECK:STDOUT:   %Main.import_ref.b41 = import_ref Main//basic_import_generic_constraint, loc5_28, unloaded
 // CHECK:STDOUT:   %Main.import_ref.b3bc94.3: type = import_ref Main//basic_import_generic_constraint, loc4_14, loaded [symbolic = @J.%T (constants.%T)]
 // CHECK:STDOUT: }
@@ -691,7 +691,7 @@ impl forall [T:! type] D as N(T*) {}
 // CHECK:STDOUT:
 // CHECK:STDOUT:   constraint {
 // CHECK:STDOUT:   !members:
-// CHECK:STDOUT:     .Self = imports.%Main.import_ref.830
+// CHECK:STDOUT:     .Self = imports.%Main.import_ref.830896.1
 // CHECK:STDOUT:     extend imports.%Main.import_ref.b41
 // CHECK:STDOUT:
 // CHECK:STDOUT:   !requires:
@@ -1047,7 +1047,7 @@ impl forall [T:! type] D as N(T*) {}
 // CHECK:STDOUT:   %Main.import_ref.3582b1.2: type = import_ref Main//import_generic, loc15_27, loaded [symbolic = @N.Self.binding.as_type.impls.I.type.require.%I.type (constants.%I.type.1ab)]
 // CHECK:STDOUT:   %Main.import_ref.b3bc94.4: type = import_ref Main//import_generic, loc14_14, loaded [symbolic = @N.%T (constants.%T)]
 // CHECK:STDOUT:   %Main.import_ref.2fc: @N.%N.type (%N.type.d682d6.1) = import_ref Main//import_generic, loc14_24, loaded [symbolic = @N.%Self (constants.%Self.e1f)]
-// CHECK:STDOUT:   %Main.import_ref.830 = import_ref Main//import_generic, loc14_24, unloaded
+// CHECK:STDOUT:   %Main.import_ref.830896.1 = import_ref Main//import_generic, loc14_24, unloaded
 // CHECK:STDOUT:   %Main.import_ref.b41 = import_ref Main//import_generic, loc15_28, unloaded
 // CHECK:STDOUT:   %Main.import_ref.b3bc94.5: type = import_ref Main//import_generic, loc14_14, loaded [symbolic = @N.%T (constants.%T)]
 // CHECK:STDOUT: }
@@ -1152,7 +1152,7 @@ impl forall [T:! type] D as N(T*) {}
 // CHECK:STDOUT:
 // CHECK:STDOUT:   constraint {
 // CHECK:STDOUT:   !members:
-// CHECK:STDOUT:     .Self = imports.%Main.import_ref.830
+// CHECK:STDOUT:     .Self = imports.%Main.import_ref.830896.1
 // CHECK:STDOUT:     extend imports.%Main.import_ref.b41
 // CHECK:STDOUT:
 // CHECK:STDOUT:   !requires:
@@ -1573,7 +1573,7 @@ impl forall [T:! type] D as N(T*) {}
 // CHECK:STDOUT:   %Main.import_ref.3582b1.2: type = import_ref Main//import_generic_with_different_specific, loc10_27, loaded [symbolic = @N.Self.binding.as_type.impls.I.type.require.%I.type (constants.%I.type.1ab)]
 // CHECK:STDOUT:   %Main.import_ref.b3bc94.3: type = import_ref Main//import_generic_with_different_specific, loc9_14, loaded [symbolic = @N.%T (constants.%T)]
 // CHECK:STDOUT:   %Main.import_ref.2fc: @N.%N.type (%N.type.d682d6.1) = import_ref Main//import_generic_with_different_specific, loc9_24, loaded [symbolic = @N.%Self (constants.%Self.e1f642.1)]
-// CHECK:STDOUT:   %Main.import_ref.830 = import_ref Main//import_generic_with_different_specific, loc9_24, unloaded
+// CHECK:STDOUT:   %Main.import_ref.830896.1 = import_ref Main//import_generic_with_different_specific, loc9_24, unloaded
 // CHECK:STDOUT:   %Main.import_ref.b41 = import_ref Main//import_generic_with_different_specific, loc10_28, unloaded
 // CHECK:STDOUT:   %Main.import_ref.b3bc94.4: type = import_ref Main//import_generic_with_different_specific, loc9_14, loaded [symbolic = @N.%T (constants.%T)]
 // CHECK:STDOUT: }
@@ -1638,7 +1638,7 @@ impl forall [T:! type] D as N(T*) {}
 // CHECK:STDOUT:
 // CHECK:STDOUT:   constraint {
 // CHECK:STDOUT:   !members:
-// CHECK:STDOUT:     .Self = imports.%Main.import_ref.830
+// CHECK:STDOUT:     .Self = imports.%Main.import_ref.830896.1
 // CHECK:STDOUT:     extend imports.%Main.import_ref.b41
 // CHECK:STDOUT:
 // CHECK:STDOUT:   !requires:
@@ -2023,7 +2023,7 @@ impl forall [T:! type] D as N(T*) {}
 // CHECK:STDOUT:   %Main.import_ref.f2a55c.2: type = import_ref Main//import_generic_decl, loc8_27, loaded [symbolic = @N.Self.binding.as_type.impls.J.type.require.%J.type (constants.%J.type.04e)]
 // CHECK:STDOUT:   %Main.import_ref.b3bc94.4: type = import_ref Main//import_generic_decl, loc7_14, loaded [symbolic = @N.%T (constants.%T)]
 // CHECK:STDOUT:   %Main.import_ref.2fc: @N.%N.type (%N.type.d682d6.1) = import_ref Main//import_generic_decl, loc7_24, loaded [symbolic = @N.%Self (constants.%Self.e1f)]
-// CHECK:STDOUT:   %Main.import_ref.830 = import_ref Main//import_generic_decl, loc7_24, unloaded
+// CHECK:STDOUT:   %Main.import_ref.830896.1 = import_ref Main//import_generic_decl, loc7_24, unloaded
 // CHECK:STDOUT:   %Main.import_ref.105 = import_ref Main//import_generic_decl, loc8_28, unloaded
 // CHECK:STDOUT:   %Main.import_ref.b3bc94.5: type = import_ref Main//import_generic_decl, loc7_14, loaded [symbolic = @N.%T (constants.%T)]
 // CHECK:STDOUT: }
@@ -2128,7 +2128,7 @@ impl forall [T:! type] D as N(T*) {}
 // CHECK:STDOUT:
 // CHECK:STDOUT:   constraint {
 // CHECK:STDOUT:   !members:
-// CHECK:STDOUT:     .Self = imports.%Main.import_ref.830
+// CHECK:STDOUT:     .Self = imports.%Main.import_ref.830896.1
 // CHECK:STDOUT:     extend imports.%Main.import_ref.105
 // CHECK:STDOUT:
 // CHECK:STDOUT:   !requires:

toolchain/check/testdata/interface/require.carbon

@@ -46,6 +46,36 @@ fn F(T:! Z, t:! T) {
   t.YY();
 }
 
+// --- fail_todo_extend_with_self.carbon
+library "[[@TEST_NAME]]";
+
+interface Y(T:! type) {
+  fn YY();
+}
+
+//@dump-sem-ir-begin
+interface Z {
+  extend require impls Y(Self);
+}
+//@dump-sem-ir-end
+
+fn F(T:! Z) {
+  // TODO: We find the name `YY`, but then fail to do impl lookup for `Y` in
+  // `T:! Z` since the identified facet type doesn't include `Y`. The
+  // identified facet type needs to include extends inside interfaces?
+  //
+  // CHECK:STDERR: fail_todo_extend_with_self.carbon:[[@LINE+4]]:3: error: cannot access member of interface `Y(T)` in type `T` that does not implement that interface [MissingImplInMemberAccess]
+  // CHECK:STDERR:   T.YY();
+  // CHECK:STDERR:   ^~~~
+  // CHECK:STDERR:
+  T.YY();
+  // CHECK:STDERR: fail_todo_extend_with_self.carbon:[[@LINE+4]]:3: error: cannot convert type `T` that implements `Z` into type implementing `Y(T)` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   T.(Y(T).YY)();
+  // CHECK:STDERR:   ^~~~~~~~~~~
+  // CHECK:STDERR:
+  T.(Y(T).YY)();
+}
+
 // --- fail_todo_implicit_self_impls.carbon
 library "[[@TEST_NAME]]";
 
@@ -347,6 +377,63 @@ interface Z(T:! type) {
 // CHECK:STDOUT:   %Self.binding.as_type => constants.%Self.binding.as_type
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
+// CHECK:STDOUT: --- fail_todo_extend_with_self.carbon
+// CHECK:STDOUT:
+// CHECK:STDOUT: constants {
+// CHECK:STDOUT:   %Y.type.82b: type = generic_interface_type @Y [concrete]
+// CHECK:STDOUT:   %Y.generic: %Y.type.82b = struct_value () [concrete]
+// CHECK:STDOUT:   %Z.type: type = facet_type <@Z> [concrete]
+// CHECK:STDOUT:   %Self.c59: %Z.type = symbolic_binding Self, 0 [symbolic]
+// CHECK:STDOUT:   %Self.binding.as_type: type = symbolic_binding_type Self, 0, %Self.c59 [symbolic]
+// CHECK:STDOUT:   %Y.type.432: type = facet_type <@Y, @Y(%Self.binding.as_type)> [symbolic]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: imports {
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: file {
+// CHECK:STDOUT:   %Z.decl: type = interface_decl @Z [concrete = constants.%Z.type] {} {}
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: interface @Z {
+// CHECK:STDOUT:   %Self: %Z.type = symbolic_binding Self, 0 [symbolic = constants.%Self.c59]
+// CHECK:STDOUT:   %Z.Self.binding.as_type.impls.Y.type.require.decl = require_decl @Z.Self.binding.as_type.impls.Y.type.require [concrete] {
+// CHECK:STDOUT:     require %Self.as_type.loc9_18 impls %Y.type.loc9_30.1
+// CHECK:STDOUT:   } {
+// CHECK:STDOUT:     %Self.as_type.loc9_18: type = facet_access_type @Z.%Self [symbolic = %Self.binding.as_type (constants.%Self.binding.as_type)]
+// CHECK:STDOUT:     %Y.ref: %Y.type.82b = name_ref Y, file.%Y.decl [concrete = constants.%Y.generic]
+// CHECK:STDOUT:     %Self.ref: %Z.type = name_ref Self, @Z.%Self [symbolic = %Self (constants.%Self.c59)]
+// CHECK:STDOUT:     %Self.as_type.loc9_30: type = facet_access_type %Self.ref [symbolic = %Self.binding.as_type (constants.%Self.binding.as_type)]
+// CHECK:STDOUT:     %.loc9: type = converted %Self.ref, %Self.as_type.loc9_30 [symbolic = %Self.binding.as_type (constants.%Self.binding.as_type)]
+// CHECK:STDOUT:     %Y.type.loc9_30.1: type = facet_type <@Y, @Y(constants.%Self.binding.as_type)> [symbolic = %Y.type.loc9_30.2 (constants.%Y.type.432)]
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %.loc9: type = specific_constant @Z.Self.binding.as_type.impls.Y.type.require.%Y.type.loc9_30.1, @Z.Self.binding.as_type.impls.Y.type.require(constants.%Self.c59) [symbolic = constants.%Y.type.432]
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = %Self
+// CHECK:STDOUT:   .Y = <poisoned>
+// CHECK:STDOUT:   .YY = <poisoned>
+// CHECK:STDOUT:   extend %.loc9
+// CHECK:STDOUT:   witness = ()
+// CHECK:STDOUT:
+// CHECK:STDOUT: !requires:
+// CHECK:STDOUT:   @Z.Self.binding.as_type.impls.Y.type.require {
+// CHECK:STDOUT:     require @Z.Self.binding.as_type.impls.Y.type.require.%Self.as_type.loc9_18 impls @Z.Self.binding.as_type.impls.Y.type.require.%Y.type.loc9_30.1
+// CHECK:STDOUT:   }
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: generic require @Z.Self.binding.as_type.impls.Y.type.require(@Z.%Self: %Z.type) {
+// CHECK:STDOUT:   %Self: %Z.type = symbolic_binding Self, 0 [symbolic = %Self (constants.%Self.c59)]
+// CHECK:STDOUT:   %Self.binding.as_type: type = symbolic_binding_type Self, 0, %Self [symbolic = %Self.binding.as_type (constants.%Self.binding.as_type)]
+// CHECK:STDOUT:   %Y.type.loc9_30.2: type = facet_type <@Y, @Y(%Self.binding.as_type)> [symbolic = %Y.type.loc9_30.2 (constants.%Y.type.432)]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @Z.Self.binding.as_type.impls.Y.type.require(constants.%Self.c59) {
+// CHECK:STDOUT:   %Self => constants.%Self.c59
+// CHECK:STDOUT:   %Self.binding.as_type => constants.%Self.binding.as_type
+// CHECK:STDOUT:   %Y.type.loc9_30.2 => constants.%Y.type.432
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
 // CHECK:STDOUT: --- fail_todo_implicit_self_impls.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {

toolchain/check/testdata/named_constraint/import_constraint_decl.carbon

@@ -98,7 +98,7 @@ impl C as B {}
 // CHECK:STDOUT:   %Main.import_ref.67f: type = import_ref Main//b, loc5_18, loaded [symbolic = @B.Self.binding.as_type.impls.I.type.require.%Self.binding.as_type (constants.%Self.binding.as_type)]
 // CHECK:STDOUT:   %Main.import_ref.72a: type = import_ref Main//b, loc5_24, loaded [concrete = constants.%I.type]
 // CHECK:STDOUT:   %Main.import_ref.e33: %B.type = import_ref Main//b, loc4_14, loaded [symbolic = constants.%Self.f45]
-// CHECK:STDOUT:   %Main.import_ref.65b = import_ref Main//b, loc4_14, unloaded
+// CHECK:STDOUT:   %Main.import_ref.65b437.1 = import_ref Main//b, loc4_14, unloaded
 // CHECK:STDOUT:   %Main.import_ref.121 = import_ref Main//b, loc5_25, unloaded
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
@@ -131,7 +131,7 @@ impl C as B {}
 // CHECK:STDOUT:
 // CHECK:STDOUT: constraint @B [from "b.carbon"] {
 // CHECK:STDOUT: !members:
-// CHECK:STDOUT:   .Self = imports.%Main.import_ref.65b
+// CHECK:STDOUT:   .Self = imports.%Main.import_ref.65b437.1
 // CHECK:STDOUT:   extend imports.%Main.import_ref.121
 // CHECK:STDOUT:
 // CHECK:STDOUT: !requires:

toolchain/check/testdata/named_constraint/require.carbon

@@ -32,6 +32,28 @@ fn F(T:! Z, t: T) {
   //@dump-sem-ir-end
 }
 
+// --- extend_with_self.carbon
+library "[[@TEST_NAME]]";
+
+interface Y(T:! type) {
+  fn YY();
+}
+
+//@dump-sem-ir-begin
+constraint Z {
+  extend require impls Y(Self);
+}
+//@dump-sem-ir-end
+
+fn F(T:! Z, t: T) {
+  //@dump-sem-ir-begin
+  T.YY();
+  T.(Y(T).YY)();
+
+  t.YY();
+  //@dump-sem-ir-end
+}
+
 // --- implicit_self_impls.carbon
 library "[[@TEST_NAME]]";
 
@@ -602,6 +624,138 @@ fn F() {
 // CHECK:STDOUT:   %Self.binding.as_type => constants.%T.binding.as_type
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
+// CHECK:STDOUT: --- extend_with_self.carbon
+// CHECK:STDOUT:
+// CHECK:STDOUT: constants {
+// CHECK:STDOUT:   %Y.type.82b: type = generic_interface_type @Y [concrete]
+// CHECK:STDOUT:   %empty_tuple.type: type = tuple_type () [concrete]
+// CHECK:STDOUT:   %Y.generic: %Y.type.82b = struct_value () [concrete]
+// CHECK:STDOUT:   %Z.type: type = facet_type <@Z> [concrete]
+// CHECK:STDOUT:   %Self.550: %Z.type = symbolic_binding Self, 0 [symbolic]
+// CHECK:STDOUT:   %Self.binding.as_type: type = symbolic_binding_type Self, 0, %Self.550 [symbolic]
+// CHECK:STDOUT:   %Y.type.83d: type = facet_type <@Y, @Y(%Self.binding.as_type)> [symbolic]
+// CHECK:STDOUT:   %T.f45: %Z.type = symbolic_binding T, 0 [symbolic]
+// CHECK:STDOUT:   %T.binding.as_type: type = symbolic_binding_type T, 0, %T.f45 [symbolic]
+// CHECK:STDOUT:   %pattern_type.349: type = pattern_type %T.binding.as_type [symbolic]
+// CHECK:STDOUT:   %Y.type.55c: type = facet_type <@Y, @Y(%T.binding.as_type)> [symbolic]
+// CHECK:STDOUT:   %Y.YY.type.fde: type = fn_type @Y.YY, @Y(%T.binding.as_type) [symbolic]
+// CHECK:STDOUT:   %Y.assoc_type.eee: type = assoc_entity_type @Y, @Y(%T.binding.as_type) [symbolic]
+// CHECK:STDOUT:   %assoc0.950: %Y.assoc_type.eee = assoc_entity element0, @Y.%Y.YY.decl [symbolic]
+// CHECK:STDOUT:   %require_complete.ec2: <witness> = require_complete_type %Y.type.55c [symbolic]
+// CHECK:STDOUT:   %Y.lookup_impl_witness: <witness> = lookup_impl_witness %T.f45, @Y, @Y(%T.binding.as_type) [symbolic]
+// CHECK:STDOUT:   %Y.facet: %Y.type.55c = facet_value %T.binding.as_type, (%Y.lookup_impl_witness) [symbolic]
+// CHECK:STDOUT:   %.c0b: type = fn_type_with_self_type %Y.YY.type.fde, %Y.facet [symbolic]
+// CHECK:STDOUT:   %impl.elem0: %.c0b = impl_witness_access %Y.lookup_impl_witness, element0 [symbolic]
+// CHECK:STDOUT:   %specific_impl_fn: <specific function> = specific_impl_function %impl.elem0, @Y.YY(%T.binding.as_type, %Y.facet) [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.%Z.type] {} {}
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: constraint @Z {
+// CHECK:STDOUT:   %Self: %Z.type = symbolic_binding Self, 0 [symbolic = constants.%Self.550]
+// CHECK:STDOUT:   %Z.Self.binding.as_type.impls.Y.type.require.decl = require_decl @Z.Self.binding.as_type.impls.Y.type.require [concrete] {
+// CHECK:STDOUT:     require %Self.as_type.loc9_18 impls %Y.type.loc9_30.1
+// CHECK:STDOUT:   } {
+// CHECK:STDOUT:     %Self.as_type.loc9_18: type = facet_access_type @Z.%Self [symbolic = %Self.binding.as_type (constants.%Self.binding.as_type)]
+// CHECK:STDOUT:     %Y.ref: %Y.type.82b = name_ref Y, file.%Y.decl [concrete = constants.%Y.generic]
+// CHECK:STDOUT:     %Self.ref: %Z.type = name_ref Self, @Z.%Self [symbolic = %Self (constants.%Self.550)]
+// CHECK:STDOUT:     %Self.as_type.loc9_30: type = facet_access_type %Self.ref [symbolic = %Self.binding.as_type (constants.%Self.binding.as_type)]
+// CHECK:STDOUT:     %.loc9: type = converted %Self.ref, %Self.as_type.loc9_30 [symbolic = %Self.binding.as_type (constants.%Self.binding.as_type)]
+// CHECK:STDOUT:     %Y.type.loc9_30.1: type = facet_type <@Y, @Y(constants.%Self.binding.as_type)> [symbolic = %Y.type.loc9_30.2 (constants.%Y.type.83d)]
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %.loc9: type = specific_constant @Z.Self.binding.as_type.impls.Y.type.require.%Y.type.loc9_30.1, @Z.Self.binding.as_type.impls.Y.type.require(constants.%Self.550) [symbolic = constants.%Y.type.83d]
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = %Self
+// CHECK:STDOUT:   .Y = <poisoned>
+// CHECK:STDOUT:   .YY = <poisoned>
+// CHECK:STDOUT:   extend %.loc9
+// CHECK:STDOUT:
+// CHECK:STDOUT: !requires:
+// CHECK:STDOUT:   @Z.Self.binding.as_type.impls.Y.type.require {
+// CHECK:STDOUT:     require @Z.Self.binding.as_type.impls.Y.type.require.%Self.as_type.loc9_18 impls @Z.Self.binding.as_type.impls.Y.type.require.%Y.type.loc9_30.1
+// CHECK:STDOUT:   }
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: generic require @Z.Self.binding.as_type.impls.Y.type.require(@Z.%Self: %Z.type) {
+// CHECK:STDOUT:   %Self: %Z.type = symbolic_binding Self, 0 [symbolic = %Self (constants.%Self.550)]
+// CHECK:STDOUT:   %Self.binding.as_type: type = symbolic_binding_type Self, 0, %Self [symbolic = %Self.binding.as_type (constants.%Self.binding.as_type)]
+// CHECK:STDOUT:   %Y.type.loc9_30.2: type = facet_type <@Y, @Y(%Self.binding.as_type)> [symbolic = %Y.type.loc9_30.2 (constants.%Y.type.83d)]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: generic fn @F(%T.loc13_6.2: %Z.type) {
+// CHECK:STDOUT:   <elided>
+// CHECK:STDOUT:
+// CHECK:STDOUT: !definition:
+// CHECK:STDOUT:   <elided>
+// CHECK:STDOUT:   %Y.type.loc15: type = facet_type <@Y, @Y(%T.binding.as_type)> [symbolic = %Y.type.loc15 (constants.%Y.type.55c)]
+// CHECK:STDOUT:   %require_complete.loc15: <witness> = require_complete_type %Y.type.loc15 [symbolic = %require_complete.loc15 (constants.%require_complete.ec2)]
+// CHECK:STDOUT:   %Y.assoc_type: type = assoc_entity_type @Y, @Y(%T.binding.as_type) [symbolic = %Y.assoc_type (constants.%Y.assoc_type.eee)]
+// CHECK:STDOUT:   %assoc0: @F.%Y.assoc_type (%Y.assoc_type.eee) = assoc_entity element0, @Y.%Y.YY.decl [symbolic = %assoc0 (constants.%assoc0.950)]
+// CHECK:STDOUT:   %Y.lookup_impl_witness: <witness> = lookup_impl_witness %T.loc13_6.1, @Y, @Y(%T.binding.as_type) [symbolic = %Y.lookup_impl_witness (constants.%Y.lookup_impl_witness)]
+// CHECK:STDOUT:   %Y.YY.type: type = fn_type @Y.YY, @Y(%T.binding.as_type) [symbolic = %Y.YY.type (constants.%Y.YY.type.fde)]
+// CHECK:STDOUT:   %Y.facet.loc15: @F.%Y.type.loc15 (%Y.type.55c) = facet_value %T.binding.as_type, (%Y.lookup_impl_witness) [symbolic = %Y.facet.loc15 (constants.%Y.facet)]
+// CHECK:STDOUT:   %.loc15_4.3: type = fn_type_with_self_type %Y.YY.type, %Y.facet.loc15 [symbolic = %.loc15_4.3 (constants.%.c0b)]
+// CHECK:STDOUT:   %impl.elem0.loc15_4.2: @F.%.loc15_4.3 (%.c0b) = impl_witness_access %Y.lookup_impl_witness, element0 [symbolic = %impl.elem0.loc15_4.2 (constants.%impl.elem0)]
+// CHECK:STDOUT:   %specific_impl_fn.loc15_4.2: <specific function> = specific_impl_function %impl.elem0.loc15_4.2, @Y.YY(%T.binding.as_type, %Y.facet.loc15) [symbolic = %specific_impl_fn.loc15_4.2 (constants.%specific_impl_fn)]
+// CHECK:STDOUT:
+// CHECK:STDOUT:   fn(%t.param: @F.%T.binding.as_type (%T.binding.as_type)) {
+// CHECK:STDOUT:   !entry:
+// CHECK:STDOUT:     %T.ref.loc15: %Z.type = name_ref T, %T.loc13_6.2 [symbolic = %T.loc13_6.1 (constants.%T.f45)]
+// CHECK:STDOUT:     %T.as_type.loc15: type = facet_access_type %T.ref.loc15 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
+// CHECK:STDOUT:     %.loc15_4.1: type = converted %T.ref.loc15, %T.as_type.loc15 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
+// CHECK:STDOUT:     %.loc15_4.2: @F.%Y.assoc_type (%Y.assoc_type.eee) = specific_constant @Y.%assoc0.loc4_10.1, @Y(constants.%T.binding.as_type) [symbolic = %assoc0 (constants.%assoc0.950)]
+// CHECK:STDOUT:     %YY.ref.loc15: @F.%Y.assoc_type (%Y.assoc_type.eee) = name_ref YY, %.loc15_4.2 [symbolic = %assoc0 (constants.%assoc0.950)]
+// CHECK:STDOUT:     %impl.elem0.loc15_4.1: @F.%.loc15_4.3 (%.c0b) = impl_witness_access constants.%Y.lookup_impl_witness, element0 [symbolic = %impl.elem0.loc15_4.2 (constants.%impl.elem0)]
+// CHECK:STDOUT:     %specific_impl_fn.loc15_4.1: <specific function> = specific_impl_function %impl.elem0.loc15_4.1, @Y.YY(constants.%T.binding.as_type, constants.%Y.facet) [symbolic = %specific_impl_fn.loc15_4.2 (constants.%specific_impl_fn)]
+// CHECK:STDOUT:     %Y.YY.call.loc15: init %empty_tuple.type = call %specific_impl_fn.loc15_4.1()
+// CHECK:STDOUT:     %T.ref.loc16_3: %Z.type = name_ref T, %T.loc13_6.2 [symbolic = %T.loc13_6.1 (constants.%T.f45)]
+// CHECK:STDOUT:     %Y.ref: %Y.type.82b = name_ref Y, file.%Y.decl [concrete = constants.%Y.generic]
+// CHECK:STDOUT:     %T.ref.loc16_8: %Z.type = name_ref T, %T.loc13_6.2 [symbolic = %T.loc13_6.1 (constants.%T.f45)]
+// CHECK:STDOUT:     %T.as_type.loc16_9: type = facet_access_type %T.ref.loc16_8 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
+// CHECK:STDOUT:     %.loc16_9: type = converted %T.ref.loc16_8, %T.as_type.loc16_9 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
+// CHECK:STDOUT:     %Y.type.loc16: type = facet_type <@Y, @Y(constants.%T.binding.as_type)> [symbolic = %Y.type.loc15 (constants.%Y.type.55c)]
+// CHECK:STDOUT:     %.loc16_10: @F.%Y.assoc_type (%Y.assoc_type.eee) = specific_constant @Y.%assoc0.loc4_10.1, @Y(constants.%T.binding.as_type) [symbolic = %assoc0 (constants.%assoc0.950)]
+// CHECK:STDOUT:     %YY.ref.loc16: @F.%Y.assoc_type (%Y.assoc_type.eee) = name_ref YY, %.loc16_10 [symbolic = %assoc0 (constants.%assoc0.950)]
+// CHECK:STDOUT:     %T.as_type.loc16_4: type = facet_access_type %T.ref.loc16_3 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
+// CHECK:STDOUT:     %Y.facet.loc16: @F.%Y.type.loc15 (%Y.type.55c) = facet_value %T.as_type.loc16_4, (constants.%Y.lookup_impl_witness) [symbolic = %Y.facet.loc15 (constants.%Y.facet)]
+// CHECK:STDOUT:     %.loc16_4: @F.%Y.type.loc15 (%Y.type.55c) = converted %T.ref.loc16_3, %Y.facet.loc16 [symbolic = %Y.facet.loc15 (constants.%Y.facet)]
+// CHECK:STDOUT:     %impl.elem0.loc16: @F.%.loc15_4.3 (%.c0b) = impl_witness_access constants.%Y.lookup_impl_witness, element0 [symbolic = %impl.elem0.loc15_4.2 (constants.%impl.elem0)]
+// CHECK:STDOUT:     %specific_impl_fn.loc16: <specific function> = specific_impl_function %impl.elem0.loc16, @Y.YY(constants.%T.binding.as_type, constants.%Y.facet) [symbolic = %specific_impl_fn.loc15_4.2 (constants.%specific_impl_fn)]
+// CHECK:STDOUT:     %Y.YY.call.loc16: init %empty_tuple.type = call %specific_impl_fn.loc16()
+// CHECK:STDOUT:     %t.ref: @F.%T.binding.as_type (%T.binding.as_type) = name_ref t, %t
+// CHECK:STDOUT:     %.loc18: @F.%Y.assoc_type (%Y.assoc_type.eee) = specific_constant @Y.%assoc0.loc4_10.1, @Y(constants.%T.binding.as_type) [symbolic = %assoc0 (constants.%assoc0.950)]
+// CHECK:STDOUT:     %YY.ref.loc18: @F.%Y.assoc_type (%Y.assoc_type.eee) = name_ref YY, %.loc18 [symbolic = %assoc0 (constants.%assoc0.950)]
+// CHECK:STDOUT:     %impl.elem0.loc18: @F.%.loc15_4.3 (%.c0b) = impl_witness_access constants.%Y.lookup_impl_witness, element0 [symbolic = %impl.elem0.loc15_4.2 (constants.%impl.elem0)]
+// CHECK:STDOUT:     %specific_impl_fn.loc18: <specific function> = specific_impl_function %impl.elem0.loc18, @Y.YY(constants.%T.binding.as_type, constants.%Y.facet) [symbolic = %specific_impl_fn.loc15_4.2 (constants.%specific_impl_fn)]
+// CHECK:STDOUT:     %Y.YY.call.loc18: init %empty_tuple.type = call %specific_impl_fn.loc18()
+// CHECK:STDOUT:     <elided>
+// CHECK:STDOUT:   }
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @Z.Self.binding.as_type.impls.Y.type.require(constants.%Self.550) {
+// CHECK:STDOUT:   %Self => constants.%Self.550
+// CHECK:STDOUT:   %Self.binding.as_type => constants.%Self.binding.as_type
+// CHECK:STDOUT:   %Y.type.loc9_30.2 => constants.%Y.type.83d
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @F(constants.%T.f45) {
+// CHECK:STDOUT:   %T.loc13_6.1 => constants.%T.f45
+// CHECK:STDOUT:   %T.binding.as_type => constants.%T.binding.as_type
+// CHECK:STDOUT:   %pattern_type => constants.%pattern_type.349
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @Z.Self.binding.as_type.impls.Y.type.require(constants.%T.f45) {
+// CHECK:STDOUT:   %Self => constants.%T.f45
+// CHECK:STDOUT:   %Self.binding.as_type => constants.%T.binding.as_type
+// CHECK:STDOUT:   %Y.type.loc9_30.2 => constants.%Y.type.55c
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
 // CHECK:STDOUT: --- implicit_self_impls.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {

toolchain/sem_ir/formatter.cpp

@@ -848,7 +848,7 @@ auto Formatter::FormatNameScope(NameScopeId id, llvm::StringRef label) -> void {
     out_ << "\n";
   }
 
-  for (auto extended_scope_id : scope.extended_scopes()) {
+  for (auto [extended_scope_id, _] : scope.extended_scopes()) {
     Indent();
     out_ << "extend ";
     FormatName(extended_scope_id);

toolchain/sem_ir/name_scope.cpp

@@ -22,8 +22,12 @@ auto NameScope::Print(llvm::raw_ostream& out) const -> void {
 
   out << ", extended_scopes: [";
   llvm::ListSeparator scope_sep;
-  for (auto id : extended_scopes_) {
-    out << scope_sep << id;
+  for (auto [id, inner_self_id] : extended_scopes_) {
+    if (inner_self_id.has_value()) {
+      out << scope_sep << "(" << id << ", inner self: " << inner_self_id << ")";
+    } else {
+      out << scope_sep << id;
+    }
   }
   out << "]";
 

toolchain/sem_ir/name_scope.h

@@ -185,11 +185,21 @@ class NameScope : public Printable<NameScope> {
   // identifiers will not be poisoned.
   auto LookupOrPoison(LocId loc_id, NameId name_id) -> std::optional<EntryId>;
 
-  auto extended_scopes() const -> llvm::ArrayRef<InstId> {
+  struct ExtendedScope {
+    SemIR::InstId extended_id;
+    // The inner `Self` of a scope which is part of generics inside the scope
+    // that it extends. These `Self` values need to be replaced with the self
+    // target of member lookup in order to find the right extended scope.
+    SemIR::InstId inner_self_id = SemIR::InstId::None;
+
+    friend auto operator==(NameScope::ExtendedScope lhs,
+                           NameScope::ExtendedScope rhs) -> bool = default;
+  };
+  auto extended_scopes() const -> llvm::ArrayRef<ExtendedScope> {
     return extended_scopes_;
   }
 
-  auto AddExtendedScope(InstId extended_scope) -> void {
+  auto AddExtendedScope(ExtendedScope extended_scope) -> void {
     extended_scopes_.push_back(extended_scope);
   }
 
@@ -275,7 +285,7 @@ class NameScope : public Printable<NameScope> {
   // than a single extended scope.
   // TODO: Revisit this once we have more kinds of extended scope and data.
   // TODO: Consider using something like `TinyPtrVector` for this.
-  llvm::SmallVector<InstId, 1> extended_scopes_;
+  llvm::SmallVector<ExtendedScope, 1> extended_scopes_;
 
   // The instruction which owns the scope.
   InstId inst_id_;

toolchain/sem_ir/name_scope_test.cpp

@@ -401,13 +401,19 @@ TEST(NameScope, ExtendedScopes) {
   EXPECT_THAT(name_scope.extended_scopes(), ElementsAre());
 
   InstId extended_scope1(++id);
-  name_scope.AddExtendedScope(extended_scope1);
-  EXPECT_THAT(name_scope.extended_scopes(), ElementsAre(extended_scope1));
+  InstId innert_self1(++id);
+  name_scope.AddExtendedScope({extended_scope1, innert_self1});
+  EXPECT_THAT(
+      name_scope.extended_scopes(),
+      ElementsAre(NameScope::ExtendedScope{extended_scope1, innert_self1}));
 
   InstId extended_scope2(++id);
-  name_scope.AddExtendedScope(extended_scope2);
-  EXPECT_THAT(name_scope.extended_scopes(),
-              ElementsAre(extended_scope1, extended_scope2));
+  InstId innert_self2(++id);
+  name_scope.AddExtendedScope({extended_scope2, innert_self2});
+  EXPECT_THAT(
+      name_scope.extended_scopes(),
+      ElementsAre(NameScope::ExtendedScope{extended_scope1, innert_self1},
+                  NameScope::ExtendedScope{extended_scope2, innert_self2}));
 }
 
 TEST(NameScope, HasError) {

toolchain/sem_ir/type.cpp

@@ -32,6 +32,20 @@ auto TypeStore::GetTypeIdForTypeConstantId(ConstantId constant_id) const
   return TypeId::ForTypeConstant(constant_id);
 }
 
+auto TypeStore::TryGetTypeIdForTypeConstantId(ConstantId constant_id) const
+    -> TypeId {
+  if (constant_id == SemIR::ErrorInst::ConstantId) {
+    return TypeId::None;
+  }
+  auto type_id = file_->insts()
+                     .Get(file_->constant_values().GetInstId(constant_id))
+                     .type_id();
+  if (type_id != SemIR::TypeType::TypeId) {
+    return TypeId::None;
+  }
+  return TypeId::ForTypeConstant(constant_id);
+}
+
 auto TypeStore::GetTypeIdForTypeInstId(InstId inst_id) const -> TypeId {
   auto constant_id = file_->constant_values().Get(inst_id);
   CheckTypeOfConstantIsTypeType(*file_, constant_id);

toolchain/sem_ir/type.h

@@ -62,6 +62,10 @@ class TypeStore : public Yaml::Printable<TypeStore> {
   // through an `as type` conversion, that is, to a value of type `TypeType`.
   auto GetTypeIdForTypeConstantId(ConstantId constant_id) const -> TypeId;
 
+  // Like GetTypeIdForTypeConstantId() but returns None if the constant is not a
+  // value of type `TypeType`.
+  auto TryGetTypeIdForTypeConstantId(ConstantId constant_id) const -> TypeId;
+
   // Returns the type ID for an instruction whose constant value is a type
   // value, i.e. it is a value of type `TypeType`.
   //