Replace .Self in facet types (#7097)

This allows `T impls X` constraints to function, since they must contain
some reference to `.Self` in order to be valid. This should be
sufficient to support the interfaces we need for for loops over C++
range-for-compatible types.

We replace `.Self` in the following places:
- In a require decl, as we have a specific self facet to replace it with
from the declaration, either a user-specified facet or the symbolic
`Self`.
- When identifying a facet type, as we have a specific self that we are
identifying the facet type with. That self gets used for all `.Self`
references.
- Implicit `.Self` references on the RHS of an `impls` constraint when
building a facet type. The `.Self` references there no longer refer to
the top level self facet, so replace them with the facet that we now
know they refer to, which is found on the LHS of the `where` before the
`impls`.
- Rewrite constraints in impl lookup when validating them and comparing
them with constants from witnesses, which come from identifying a facet
type.
- Rewrite constraints in ImplWitnessAccess eval when comparing them with
constants from witnesses, which come from identifying a facet type.

Substitution is done through `SubstPeriodSelf`. It handles replacing
`.Self` and `.Self as type`, for a replacement facet that is either of
type FacetType or TypeType.

Eval currently diagnoses some ambiguous `.Self` references when doing
substitution of `.Self` but this is the incorrect place to do it, so
there are TODOs about moving this to name lookup. To support these
diagnostics there's some additional complexity in `SubstPeriodSelf` that
can go away once the TODOs are addressed, such as asking the caller if
they want to replace each `.Self`, in order for it to report a
diagnostic.

There are a number of follow-up work items here:
- Some TODO tests.
- Remove `SymbolicBindingType` since its intention was to support
`.Self` but we don't need it with this approach.
- Replace `.Self` in rewrite constraints of require decls.
- Replace `.Self` in rewrite constraints of impl as when constructing
the witness table.
- Reject explicit `.Self` in name lookup when it would be ambiguous.
- Officially disallow `.Self.A = B` in rewrite constraints in the design
docs, so that we don't have the case where `.A` is allowed but `.Self.A`
is not due to ambiguity.

toolchain/check/eval.cpp

@@ -20,6 +20,7 @@
 #include "toolchain/check/facet_type.h"
 #include "toolchain/check/generic.h"
 #include "toolchain/check/import_ref.h"
+#include "toolchain/check/inst.h"
 #include "toolchain/check/name_lookup.h"
 #include "toolchain/check/type.h"
 #include "toolchain/check/type_completion.h"
@@ -2621,7 +2622,8 @@ static auto AddRequirementRewrite(Context& context,
       {.lhs_id = rewrite.lhs_id, .rhs_id = rewrite.rhs_id});
 }
 
-static auto AddRequirementImpls(Context& context, SemIR::RequirementImpls impls,
+static auto AddRequirementImpls(Context& context, SemIR::LocId loc_id,
+                                SemIR::RequirementImpls impls,
                                 SemIR::InstId period_self_id,
                                 SemIR::FacetTypeInfo* info, Phase* phase)
     -> void {
@@ -2657,40 +2659,15 @@ static auto AddRequirementImpls(Context& context, SemIR::RequirementImpls impls,
     llvm::append_range(info->type_impls_interfaces, rhs.type_impls_interfaces);
     llvm::append_range(info->type_impls_named_constraints,
                        rhs.type_impls_named_constraints);
+    llvm::append_range(info->rewrite_constraints, rhs.rewrite_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)
+    auto extends_interface = [=](SemIR::SpecificInterface si)
         -> SemIR::FacetTypeInfo::TypeImplsInterface {
       return {lhs_facet_or_type, si};
     };
-    auto impls_constraint = [&](SemIR::SpecificNamedConstraint sc)
+    auto extends_constraint = [=](SemIR::SpecificNamedConstraint sc)
         -> SemIR::FacetTypeInfo::TypeImplsNamedConstraint {
       return {lhs_facet_or_type, sc};
     };
@@ -2699,47 +2676,145 @@ static auto AddRequirementImpls(Context& context, SemIR::RequirementImpls impls,
     // 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::map_range(rhs.extend_constraints, extends_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.
+        llvm::map_range(rhs.extend_named_constraints, extends_constraint));
+
+    // Impls constraints are written as `T impls X` where `T` is a facet and `X`
+    // is a facet type. The `T` can be `.Self`.
     //
-    // TODO: Convert the LHS used in the TypeImplsNamedConstraint to a facet
-    // with the RHS extend constraints (interfaces and named constraints).
+    // What's important here is that since `X` is a facet type, it can contain a
+    // `where` expression, and the value of `.Self` changes across a `where`
+    // expression. This can create ambiguous `.Self` references where on the RHS
+    // they refer to a different facet (`T`) than on the LHS, which is diagnosed
+    // as an error.
     //
-    // TODO: Replace `.Self` with the LHS type as a facet with the RHS extend
-    // constraints.
+    // TODO: For now we do this diagnosis here, but we should diagnose this
+    // during name lookup of `.Self` instead, in order to properly allow only
+    // implicit `.Self` references when it would be ambiguous. Then use
+    // `should_replace_implicit_only` in all cases.
+    //
+    // Implicit `.Self` references can't be avoided when referencing members of
+    // the facet's type such as with `.Member`. As such, we replace implicit
+    // `.Self` references on the RHS of a nested `where` with the inner-most
+    // facet that it could possibly refer to, the `T as X` from the `impls`
+    // constraint, which eliminates any ambiguity in the resulting facet type.
+
+    class SubstPeriodSelfDiagnoseExplicitCallbacks
+        : public SubstPeriodSelfCallbacks {
+     public:
+      explicit SubstPeriodSelfDiagnoseExplicitCallbacks(
+          Context* context, SemIR::LocId loc_id,
+          SemIR::ConstantId period_self_replacement_id, Phase* phase)
+          : SubstPeriodSelfCallbacks(context, loc_id,
+                                     period_self_replacement_id),
+            phase_(phase) {}
+
+      auto ShouldReplace(bool implicit) -> bool override {
+        if (!implicit && *phase_ != Phase::UnknownDueToError) {
+          CARBON_DIAGNOSTIC(
+              AmbiguousPeriodSelf, Error,
+              "`.Self` is ambiguous after nested `where` in `<type> "
+              "impls ...` clause.");
+          context().emitter().Emit(loc_id(), AmbiguousPeriodSelf);
+          *phase_ = Phase::UnknownDueToError;
+        }
+        return implicit;
+      }
+
+      Phase* phase_;
+    };
+    SubstPeriodSelfDiagnoseExplicitCallbacks
+        callbacks_should_replace_explicit_is_error(
+            &context, loc_id, context.constant_values().Get(lhs_facet_or_type),
+            phase);
+
+    class SubstPeriodSelfImplicitOnlyCallbacks
+        : public SubstPeriodSelfCallbacks {
+     public:
+      explicit SubstPeriodSelfImplicitOnlyCallbacks(
+          Context* context, SemIR::LocId loc_id,
+          SemIR::ConstantId period_self_replacement_id)
+          : SubstPeriodSelfCallbacks(context, loc_id,
+                                     period_self_replacement_id) {}
+
+      // TODO: Replace this callback with a SubstPeriodSelf parameter saying
+      // what to replace (as a bool or an enum). Then this subclass can go away.
+      auto ShouldReplace(bool implicit) -> bool override { return implicit; }
+    };
+    SubstPeriodSelfImplicitOnlyCallbacks callbacks_should_replace_implicit_only(
+        &context, loc_id, context.constant_values().Get(lhs_facet_or_type));
+
+    auto self_impls_interface = [&](SemIR::SpecificInterface si) {
+      return SubstPeriodSelf(context,
+                             callbacks_should_replace_explicit_is_error, si);
+    };
+    auto self_impls_constraint = [&](SemIR::SpecificNamedConstraint sc) {
+      return SubstPeriodSelf(context,
+                             callbacks_should_replace_explicit_is_error, sc);
+    };
+    auto type_impls_interface =
+        [&](SemIR::FacetTypeInfo::TypeImplsInterface impls)
+        -> SemIR::FacetTypeInfo::TypeImplsInterface {
+      auto self =
+          SubstPeriodSelf(context, callbacks_should_replace_explicit_is_error,
+                          context.constant_values().Get(impls.self_type));
+      auto interface =
+          SubstPeriodSelf(context, callbacks_should_replace_explicit_is_error,
+                          impls.specific_interface);
+      return {context.constant_values().GetInstId(self), interface};
+    };
+    auto type_impls_constraint =
+        [&](SemIR::FacetTypeInfo::TypeImplsNamedConstraint impls)
+        -> SemIR::FacetTypeInfo::TypeImplsNamedConstraint {
+      auto self =
+          SubstPeriodSelf(context, callbacks_should_replace_explicit_is_error,
+                          context.constant_values().Get(impls.self_type));
+      auto constraint =
+          SubstPeriodSelf(context, callbacks_should_replace_explicit_is_error,
+                          impls.specific_named_constraint);
+      return {context.constant_values().GetInstId(self), constraint};
+    };
+
     llvm::append_range(
-        info->type_impls_interfaces,
-        llvm::map_range(rhs.self_impls_constraints, impls_interface));
+        info->self_impls_constraints,
+        llvm::map_range(rhs.self_impls_constraints, self_impls_interface));
+    llvm::append_range(info->self_impls_named_constraints,
+                       llvm::map_range(rhs.self_impls_named_constraints,
+                                       self_impls_constraint));
     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);
+        info->type_impls_interfaces,
+        llvm::map_range(rhs.type_impls_interfaces, type_impls_interface));
     llvm::append_range(info->type_impls_named_constraints,
-                       rhs.type_impls_named_constraints);
+                       llvm::map_range(rhs.type_impls_named_constraints,
+                                       type_impls_constraint));
+
+    // TODO: We have to pass explicit `.Self` along unchanged in rewrites. A
+    // rewrite of the form `M(.Self) where .M0 = {}` is an access into `.Self as
+    // M(.Self)`. The first `.Self` is implicit and should be replaced. The
+    // second is explicit but refers to the outer-most facet and should not be
+    // replaced. In the future when we diagnose ambiguous `.Self` in name
+    // lookup, we will replace all implicit `.Self` and leave all explicit
+    // `.Self` alone since they won't be ambiguous.
+    auto rewrite_constraint =
+        [&](SemIR::FacetTypeInfo::RewriteConstraint rewrite)
+        -> SemIR::FacetTypeInfo::RewriteConstraint {
+      auto lhs_id =
+          SubstPeriodSelf(context, callbacks_should_replace_implicit_only,
+                          context.constant_values().Get(rewrite.lhs_id));
+      auto rhs_id =
+          SubstPeriodSelf(context, callbacks_should_replace_implicit_only,
+                          context.constant_values().Get(rewrite.rhs_id));
+      return {context.constant_values().GetInstId(lhs_id),
+              context.constant_values().GetInstId(rhs_id)};
+    };
+
+    llvm::append_range(
+        info->rewrite_constraints,
+        llvm::map_range(rhs.rewrite_constraints, rewrite_constraint));
   }
 
-  // Other requirements are copied in.
-  llvm::append_range(info->rewrite_constraints, rhs.rewrite_constraints);
   info->other_requirements |= rhs.other_requirements;
 }
 
@@ -2782,8 +2857,8 @@ auto TryEvalTypedInst<SemIR::WhereExpr>(EvalContext& eval_context,
         break;
       }
       case CARBON_KIND(SemIR::RequirementImpls impls): {
-        AddRequirementImpls(eval_context.context(), impls,
-                            typed_inst.period_self_id, &info, &phase);
+        AddRequirementImpls(eval_context.context(), SemIR::LocId(inst_id),
+                            impls, typed_inst.period_self_id, &info, &phase);
         break;
       }
       case CARBON_KIND(SemIR::RequirementEquivalent _): {

toolchain/check/eval_inst.cpp

@@ -284,24 +284,13 @@ auto EvalConstantInst(Context& /*context*/, SemIR::FunctionDecl inst)
 
 auto EvalConstantInst(Context& context, SemIR::InstId inst_id,
                       SemIR::LookupImplWitness inst) -> ConstantEvalResult {
-  // If the monomorphized query self is a FacetValue, we may get a witness from
-  // it under limited circumstances. If no final witness is found though, we
-  // don't need to preserve it for future evaluations, so we strip it from the
-  // LookupImplWitness instruction to reduce the number of distinct constant
-  // values.
+  // Canonicalize the query self to reduce the number of unique witness
+  // instructions and enable constant value comparisons.
   auto self_facet_value_inst_id = SemIR::InstId::None;
-  if (auto facet_value = context.insts().TryGetAs<SemIR::FacetValue>(
-          inst.query_self_inst_id)) {
-    self_facet_value_inst_id =
-        std::exchange(inst.query_self_inst_id, facet_value->type_inst_id);
-  }
-
-  // The self value is canonicalized in order to produce a canonical
-  // LookupImplWitness instruction, avoiding multiple constant values for
-  // `<facet value>` and `<facet value>` as type, which always have the same
-  // lookup result.
-  inst.query_self_inst_id =
-      GetCanonicalFacetOrTypeValue(context, inst.query_self_inst_id);
+  inst.query_self_inst_id = context.constant_values().GetInstId(
+      GetCanonicalQuerySelfForLookupImplWitness(
+          context, context.constant_values().Get(inst.query_self_inst_id),
+          &self_facet_value_inst_id));
 
   auto witness_id = EvalLookupSingleFinalWitness(context, SemIR::LocId(inst_id),
                                                  inst, self_facet_value_inst_id,
@@ -361,22 +350,27 @@ auto EvalConstantInst(Context& context, SemIR::InstId inst_id,
     }
     case CARBON_KIND(SemIR::LookupImplWitness witness): {
       // If the witness is symbolic but has a self type that is a FacetType, it
-      // can pull rewrite values from the self type. If the access is for one of
-      // those rewrites, evaluate to the RHS of the rewrite.
+      // can pull rewrite values from the self's facet type. If the access is
+      // for one of those rewrites, evaluate to the RHS of the rewrite.
 
-      auto witness_self_type_id =
+      // The type of the query self type (a FacetType or TypeType).
+      auto access_self_type_id =
           context.insts().Get(witness.query_self_inst_id).type_id();
-      if (!context.types().Is<SemIR::FacetType>(witness_self_type_id)) {
+      if (context.types().Is<SemIR::TypeType>(access_self_type_id)) {
+        // A self facet of type `type` has no rewrite constraints to look in.
         return ConstantEvalResult::NewSamePhase(inst);
       }
 
       // The `ImplWitnessAccess` is accessing a value, by index, for this
-      // interface.
-      auto access_interface_id = witness.query_specific_interface_id;
+      // `self impls interface` combination.
+      auto access_self =
+          context.constant_values().Get(witness.query_self_inst_id);
+      auto access_interface = context.specific_interfaces().Get(
+          witness.query_specific_interface_id);
 
-      auto witness_self_facet_type_id =
+      auto access_self_facet_type_id =
           context.types()
-              .GetAs<SemIR::FacetType>(witness_self_type_id)
+              .GetAs<SemIR::FacetType>(access_self_type_id)
               .facet_type_id;
       // TODO: We could consider something better than linear search here, such
       // as a map. However that would probably require heap allocations which
@@ -385,35 +379,67 @@ auto EvalConstantInst(Context& context, SemIR::InstId inst_id,
       // associated constants are grouped together, as in
       // ResolveFacetTypeRewriteConstraints(), and limited to just the
       // `ImplWitnessAccess` entries, then a binary search may work here.
-      for (auto witness_rewrite : context.facet_types()
-                                      .Get(witness_self_facet_type_id)
-                                      .rewrite_constraints) {
-        // Look at each rewrite constraint in the self facet value's type. If
-        // the LHS is an `ImplWitnessAccess` into the same interface that `inst`
-        // is indexing into, then we can use its RHS as the value.
-        auto witness_rewrite_lhs_access =
-            context.insts().TryGetAs<SemIR::ImplWitnessAccess>(
-                witness_rewrite.lhs_id);
-        if (!witness_rewrite_lhs_access) {
+      for (const auto& rewrite : context.facet_types()
+                                     .Get(access_self_facet_type_id)
+                                     .rewrite_constraints) {
+        // Look at each rewrite constraint in the self facet's type. If the LHS
+        // is an `ImplWitnessAccess` into the same interface that `inst` is
+        // indexing into, then we can use its RHS as the value.
+        auto rewrite_lhs_access =
+            context.insts().TryGetAs<SemIR::ImplWitnessAccess>(rewrite.lhs_id);
+        if (!rewrite_lhs_access) {
+          continue;
+        }
+        if (rewrite_lhs_access->index != inst.index) {
           continue;
         }
-        if (witness_rewrite_lhs_access->index != inst.index) {
+
+        // Witnesses come from impl lookup, and the operands are from
+        // IdentifiedFacetTypes, so `.Self` is replaced. However rewrite
+        // constraints are not part of an IdentifiedFacetType, so they are not
+        // replaced. We have to do the same replacement in the rewrite's LHS
+        // witness in order to compare it with the access witness.
+        //
+        // However we don't substitute the witness directly as that would
+        // re-evaluate it and cause us to do an impl lookup. Instead we
+        // substitute and compare its operands.
+        auto rewrite_lhs_witness =
+            context.insts().GetAs<SemIR::LookupImplWitness>(
+                rewrite_lhs_access->witness_id);
+
+        SubstPeriodSelfCallbacks callbacks(&context, SemIR::LocId(inst_id),
+                                           access_self);
+
+        auto rewrite_lhs_self = context.constant_values().Get(
+            rewrite_lhs_witness.query_self_inst_id);
+        rewrite_lhs_self =
+            SubstPeriodSelf(context, callbacks, rewrite_lhs_self);
+        // Witnesses have a canonicalized self value. Perform the same
+        // canonicalization here so that we can compare them.
+        rewrite_lhs_self = GetCanonicalQuerySelfForLookupImplWitness(
+            context, rewrite_lhs_self);
+
+        if (rewrite_lhs_self != access_self) {
+          // This rewrite is into a different self type than the access query.
           continue;
         }
 
-        auto witness_rewrite_lhs_interface_id =
-            context.insts()
-                .GetAs<SemIR::LookupImplWitness>(
-                    witness_rewrite_lhs_access->witness_id)
-                .query_specific_interface_id;
-        if (witness_rewrite_lhs_interface_id != access_interface_id) {
+        auto rewrite_lhs_interface = SubstPeriodSelf(
+            context, callbacks,
+            context.specific_interfaces().Get(
+                rewrite_lhs_witness.query_specific_interface_id));
+
+        if (rewrite_lhs_interface != access_interface) {
+          // This rewrite is into a different interface than the access query.
           continue;
         }
 
         // The `ImplWitnessAccess` evaluates to the RHS from the witness self
-        // facet value's type.
-        return ConstantEvalResult::Existing(
-            context.constant_values().Get(witness_rewrite.rhs_id));
+        // facet value's type. Any `.Self` references in the RHS are also
+        // replaced with the self type of the access.
+        auto rewrite_rhs = SubstPeriodSelf(
+            context, callbacks, context.constant_values().Get(rewrite.rhs_id));
+        return ConstantEvalResult::Existing(rewrite_rhs);
       }
       break;
     }

toolchain/check/facet_type.cpp

@@ -7,6 +7,7 @@
 #include "toolchain/base/kind_switch.h"
 #include "toolchain/check/context.h"
 #include "toolchain/check/control_flow.h"
+#include "toolchain/check/convert.h"
 #include "toolchain/check/generic.h"
 #include "toolchain/check/import_ref.h"
 #include "toolchain/check/inst.h"
@@ -467,4 +468,258 @@ auto GetConstantFacetValueForTypeAndInterface(
   return self_value_const_id;
 }
 
+SubstPeriodSelfCallbacks::SubstPeriodSelfCallbacks(
+    Context* context, SemIR::LocId loc_id,
+    SemIR::ConstantId period_self_replacement_id)
+    : SubstInstCallbacks(context),
+      loc_id_(loc_id),
+      period_self_replacement_id_(period_self_replacement_id) {}
+
+auto SubstPeriodSelfCallbacks::Subst(SemIR::InstId& inst_id) -> SubstResult {
+  // FacetTypes are concrete even if they have `.Self` inside them, but we
+  // don't recurse into FacetTypes, so we can use this as a base case. This
+  // avoids infinite recursion on TypeType and ErrorInst.
+  if (context().constant_values().Get(inst_id).is_concrete()) {
+    return FullySubstituted;
+  }
+  // Don't recurse into nested facet types, even if they are symbolic. Leave
+  // their `.Self` as is.
+  if (context().insts().Is<SemIR::FacetType>(inst_id)) {
+    return FullySubstituted;
+  }
+
+  // For `.X` (which is `.Self.X`) replace the `.Self` in the query self
+  // position, and report it as `implicit`. Any `.Self` references in the
+  // specific interface would be replaced later and not treated as `implicit`.
+  //
+  // TODO: This all goes away when eval doesn't need to know about implicit
+  // .Self for diagnostics, once we diagnose invalid `.Self` in name lookup.
+  if (auto access =
+          context().insts().TryGetAs<SemIR::ImplWitnessAccess>(inst_id)) {
+    if (auto witness = context().insts().TryGetAs<SemIR::LookupImplWitness>(
+            access->witness_id)) {
+      if (auto bind = context().insts().TryGetAs<SemIR::SymbolicBinding>(
+              witness->query_self_inst_id)) {
+        const auto& entity_name =
+            context().entity_names().Get(bind->entity_name_id);
+        if (entity_name.name_id == SemIR::NameId::PeriodSelf) {
+          auto replacement_id =
+              GetReplacement(witness->query_self_inst_id, true);
+          auto new_witness =
+              Rebuild(access->witness_id,
+                      SemIR::LookupImplWitness{
+                          .type_id = witness->type_id,
+                          .query_self_inst_id = replacement_id,
+                          // Don't replace `.Self` in the interface specific
+                          // here. That is an explicit `.Self` use. We'll
+                          // revisit the instruction for that.
+                          .query_specific_interface_id =
+                              witness->query_specific_interface_id,
+                      });
+          auto new_access = Rebuild(inst_id, SemIR::ImplWitnessAccess{
+                                                 .type_id = access->type_id,
+                                                 .witness_id = new_witness,
+                                                 .index = access->index,
+                                             });
+          inst_id = new_access;
+          return SubstAgain;
+        }
+      }
+    }
+  }
+
+  if (auto bind_type =
+          context().insts().TryGetAs<SemIR::SymbolicBindingType>(inst_id)) {
+    auto bind = context().insts().GetAs<SemIR::SymbolicBinding>(
+        bind_type->facet_value_inst_id);
+    const auto& entity_name = context().entity_names().Get(bind.entity_name_id);
+    if (entity_name.name_id == SemIR::NameId::PeriodSelf) {
+      // We need to re-construct SymbolicBindingType, not just replace its
+      // facet instruction. If the new operand is a SymbolicBinding, we need
+      // to use its entity name.
+      inst_id = Rebuild(
+          inst_id,
+          SemIR::FacetAccessType{.type_id = SemIR::TypeType::TypeId,
+                                 .facet_value_inst_id = GetReplacement(
+                                     bind_type->facet_value_inst_id, false)});
+      return FullySubstituted;
+    }
+  }
+
+  if (auto bind = context().insts().TryGetAs<SemIR::SymbolicBinding>(inst_id)) {
+    const auto& entity_name =
+        context().entity_names().Get(bind->entity_name_id);
+    if (entity_name.name_id == SemIR::NameId::PeriodSelf) {
+      inst_id = GetReplacement(inst_id, false);
+      return FullySubstituted;
+    }
+  }
+
+  return SubstOperands;
+}
+
+auto SubstPeriodSelfCallbacks::Rebuild(SemIR::InstId orig_inst_id,
+                                       SemIR::Inst new_inst) -> SemIR::InstId {
+  return RebuildNewInst(SemIR::LocId(orig_inst_id), new_inst);
+}
+
+auto SubstPeriodSelfCallbacks::GetReplacement(SemIR::InstId period_self,
+                                              bool implicit) -> SemIR::InstId {
+  if (!ShouldReplace(implicit)) {
+    return period_self;
+  }
+
+  auto period_self_type_id = context().insts().Get(period_self).type_id();
+  CARBON_CHECK(context().types().Is<SemIR::FacetType>(period_self_type_id));
+
+  auto replacement_self_inst_id =
+      context().constant_values().GetInstId(period_self_replacement_id_);
+  auto replacement_type_id =
+      context().insts().Get(replacement_self_inst_id).type_id();
+  CARBON_CHECK(context().types().IsFacetType(replacement_type_id));
+
+  // If the replacement has the same type as `.Self`, use it directly.
+  if (replacement_type_id == period_self_type_id) {
+    return replacement_self_inst_id;
+  }
+
+  // If we have already converted the replacement to the type of `.Self`, use
+  // our previous conversion.
+  if (period_self_type_id == cached_replacement_type_id_) {
+    return cached_replacement_id_;
+  }
+
+  // Convert the replacement facet to the type of `.Self`.
+  cached_replacement_id_ = ConvertReplacement(
+      replacement_self_inst_id, replacement_type_id, period_self_type_id);
+  cached_replacement_type_id_ = period_self_type_id;
+  return cached_replacement_id_;
+}
+
+auto SubstPeriodSelfCallbacks::ConvertReplacement(
+    SemIR::InstId replacement_self_inst_id, SemIR::TypeId replacement_type_id,
+    SemIR::TypeId period_self_type_id) -> SemIR::InstId {
+  // TODO: Replace all empty facet types with TypeType.
+  if (period_self_type_id == GetEmptyFacetType(context())) {
+    // Convert to an empty facet type (representing TypeType); we don't need
+    // any witnesses.
+    return ConvertToValueOfType(context(), loc_id_, replacement_self_inst_id,
+                                period_self_type_id);
+  }
+
+  // We have a facet or a type, but we need more interfaces in the facet type.
+  // We will have to synthesize a symbolic witness for each interface.
+  //
+  // Why is this okay? The type of `.Self` comes from interfaces that are
+  // before it (to the left of it) in the facet type. The replacement for
+  // `.Self` will have to impl those interfaces in order to match the facet
+  // type, so we know that it is valid to construct these witnesses.
+
+  // Make the replacement into a type, which we will need for the FacetValue.
+  if (context().types().Is<SemIR::FacetType>(replacement_type_id)) {
+    replacement_self_inst_id = context().constant_values().GetInstId(
+        EvalOrAddInst<SemIR::FacetAccessType>(
+            context(), loc_id_,
+            {.type_id = SemIR::TypeType::TypeId,
+             .facet_value_inst_id = replacement_self_inst_id}));
+  }
+
+  auto period_self_facet_type =
+      context().types().GetAs<SemIR::FacetType>(period_self_type_id);
+  auto identified_period_self_type_id = RequireIdentifiedFacetType(
+      context(), loc_id_,
+      context().constant_values().Get(replacement_self_inst_id),
+      period_self_facet_type, [&](auto& /*builder*/) {
+        // The facet type containing this `.Self` should have already been
+        // identified, which would ensure that the type of `.Self` can be
+        // identified since it can only depend on things to the left of it
+        // inside the same facet type.
+        CARBON_FATAL("could not identify type of `.Self`");
+      });
+  const auto& identified_period_self_type =
+      context().identified_facet_types().Get(identified_period_self_type_id);
+  auto required_impls = identified_period_self_type.required_impls();
+  llvm::SmallVector<SemIR::InstId> witnesses;
+  witnesses.reserve(required_impls.size());
+  for (const auto& req : required_impls) {
+    witnesses.push_back(context().constant_values().GetInstId(
+        EvalOrAddInst<SemIR::LookupImplWitness>(
+            context(), loc_id_,
+            {.type_id =
+                 GetSingletonType(context(), SemIR::WitnessType::TypeInstId),
+             .query_self_inst_id =
+                 context().constant_values().GetInstId(req.self_facet_value),
+             .query_specific_interface_id = context().specific_interfaces().Add(
+                 req.specific_interface)})));
+  }
+  return context().constant_values().GetInstId(EvalOrAddInst<SemIR::FacetValue>(
+      context(), loc_id_,
+      {
+          .type_id = period_self_type_id,
+          .type_inst_id =
+              context().types().GetAsTypeInstId(replacement_self_inst_id),
+          .witnesses_block_id = context().inst_blocks().Add(witnesses),
+      }));
+}
+
+auto SubstPeriodSelf(Context& context, SubstPeriodSelfCallbacks& callbacks,
+                     SemIR::ConstantId const_id) -> SemIR::ConstantId {
+  // Don't replace `.Self` with itself; that is cyclical.
+  //
+  // If the types differ, we would try to convert the replacement to a `.Self`
+  // of the desired type in `const_id`, which is what we already have, so
+  // there's nothing we need to do. But trying to do that conversion recurses
+  // when the type of the `.Self` contains a `.Self`.
+  if (auto bind_type =
+          context.constant_values().TryGetInstAs<SemIR::SymbolicBinding>(
+              GetCanonicalFacetOrTypeValue(
+                  context, callbacks.period_self_replacement_id()))) {
+    if (context.entity_names().Get(bind_type->entity_name_id).name_id ==
+        SemIR::NameId::PeriodSelf) {
+      return const_id;
+    }
+  }
+
+  auto subst_id = SubstInst(
+      context, context.constant_values().GetInstId(const_id), callbacks);
+  return context.constant_values().Get(subst_id);
+}
+
+static auto SubstPeriodSelfInSpecific(Context& context,
+                                      SubstPeriodSelfCallbacks& callbacks,
+                                      SemIR::SpecificId specific_id)
+    -> SemIR::SpecificId {
+  if (!specific_id.has_value()) {
+    return specific_id;
+  }
+
+  const auto& specific = context.specifics().Get(specific_id);
+
+  // Substitute into the specific without having to construct a FacetType
+  // instruction just to hold the specific interface inside a constant id.
+  llvm::SmallVector<SemIR::InstId> args(
+      context.inst_blocks().Get(specific.args_id));
+  for (auto& arg_id : args) {
+    auto const_id = context.constant_values().Get(arg_id);
+    const_id = SubstPeriodSelf(context, callbacks, const_id);
+    arg_id = context.constant_values().GetInstId(const_id);
+  }
+  return MakeSpecific(context, callbacks.loc_id(), specific.generic_id, args);
+}
+
+auto SubstPeriodSelf(Context& context, SubstPeriodSelfCallbacks& callbacks,
+                     SemIR::SpecificInterface interface)
+    -> SemIR::SpecificInterface {
+  interface.specific_id =
+      SubstPeriodSelfInSpecific(context, callbacks, interface.specific_id);
+  return interface;
+}
+auto SubstPeriodSelf(Context& context, SubstPeriodSelfCallbacks& callbacks,
+                     SemIR::SpecificNamedConstraint constraint)
+    -> SemIR::SpecificNamedConstraint {
+  constraint.specific_id =
+      SubstPeriodSelfInSpecific(context, callbacks, constraint.specific_id);
+  return constraint;
+}
+
 }  // namespace Carbon::Check

toolchain/check/facet_type.h

@@ -8,6 +8,7 @@
 #include <compare>
 
 #include "toolchain/check/context.h"
+#include "toolchain/check/subst.h"
 #include "toolchain/sem_ir/entity_with_params_base.h"
 #include "toolchain/sem_ir/ids.h"
 
@@ -89,6 +90,53 @@ auto GetConstantFacetValueForTypeAndInterface(
     SemIR::SpecificInterface specific_interface, SemIR::InstId witness_id)
     -> SemIR::ConstantId;
 
+class SubstPeriodSelfCallbacks : public SubstInstCallbacks {
+ public:
+  explicit SubstPeriodSelfCallbacks(
+      Context* context, SemIR::LocId loc_id,
+      SemIR::ConstantId period_self_replacement_id);
+  auto Subst(SemIR::InstId& inst_id) -> SubstResult override;
+  auto Rebuild(SemIR::InstId orig_inst_id, SemIR::Inst new_inst)
+      -> SemIR::InstId override;
+
+  virtual auto ShouldReplace(bool /*implicit*/) -> bool { return true; }
+
+  auto loc_id() const -> SemIR::LocId { return loc_id_; }
+  auto period_self_replacement_id() const -> SemIR::ConstantId {
+    return period_self_replacement_id_;
+  }
+
+ private:
+  auto GetReplacement(SemIR::InstId period_self, bool implicit)
+      -> SemIR::InstId;
+  auto ConvertReplacement(SemIR::InstId replacement_self_inst_id,
+                          SemIR::TypeId replacement_type_id,
+                          SemIR::TypeId period_self_type_id) -> SemIR::InstId;
+
+  SemIR::LocId loc_id_;
+  SemIR::ConstantId period_self_replacement_id_;
+
+  // The last output of GetReplacement().
+  SemIR::InstId cached_replacement_id_ = SemIR::InstId::None;
+  // The type of the last output of GetReplacement(). If the type of `.Self`
+  // matches, we can reuse the `cached_replacement_id_`.
+  SemIR::TypeId cached_replacement_type_id_ = SemIR::TypeId::None;
+};
+
+// Replace all `.Self` references in `const_id`. The `callbacks` specifies the
+// facet to replace them with.
+auto SubstPeriodSelf(Context& context, SubstPeriodSelfCallbacks& callbacks,
+                     SemIR::ConstantId const_id) -> SemIR::ConstantId;
+
+// Replace all `.Self` references in the specific of the interface or named
+// constraint. The `callbacks` specifies the facet to replace them with.
+auto SubstPeriodSelf(Context& context, SubstPeriodSelfCallbacks& callbacks,
+                     SemIR::SpecificInterface interface)
+    -> SemIR::SpecificInterface;
+auto SubstPeriodSelf(Context& context, SubstPeriodSelfCallbacks& callbacks,
+                     SemIR::SpecificNamedConstraint constraint)
+    -> SemIR::SpecificNamedConstraint;
+
 }  // namespace Carbon::Check
 
 #endif  // CARBON_TOOLCHAIN_CHECK_FACET_TYPE_H_

toolchain/check/handle_require.cpp

@@ -5,6 +5,7 @@
 #include "toolchain/base/kind_switch.h"
 #include "toolchain/check/context.h"
 #include "toolchain/check/convert.h"
+#include "toolchain/check/facet_type.h"
 #include "toolchain/check/generic.h"
 #include "toolchain/check/handle.h"
 #include "toolchain/check/inst.h"
@@ -267,14 +268,91 @@ static auto ValidateRequire(Context& context, SemIR::LocId full_require_loc_id,
   return ValidateRequireResult{.identified_facet_type = &identified};
 }
 
+// Replace all `.Self` references with the self-type.
+static auto SubstPeriodSelfInConstraint(Context& context, SemIR::LocId loc_id,
+                                        SemIR::TypeInstId self_type_inst_id,
+                                        SemIR::TypeInstId constraint_inst_id)
+    -> SemIR::TypeInstId {
+  auto orig_facet_type = context.insts().GetAs<SemIR::FacetType>(
+      context.constant_values().GetConstantInstId(constraint_inst_id));
+  const auto& orig_info =
+      context.facet_types().Get(orig_facet_type.facet_type_id);
+
+  SubstPeriodSelfCallbacks callbacks(
+      &context, loc_id, context.constant_values().Get(self_type_inst_id));
+
+  auto replace_interface = [&](SemIR::SpecificInterface si) {
+    return SubstPeriodSelf(context, callbacks, si);
+  };
+  auto replace_constraint = [&](SemIR::SpecificNamedConstraint sc) {
+    return SubstPeriodSelf(context, callbacks, sc);
+  };
+  auto replace_type_impls_interface =
+      [&](SemIR::FacetTypeInfo::TypeImplsInterface impls)
+      -> SemIR::FacetTypeInfo::TypeImplsInterface {
+    auto self = SubstPeriodSelf(context, callbacks,
+                                context.constant_values().Get(impls.self_type));
+    auto interface =
+        SubstPeriodSelf(context, callbacks, impls.specific_interface);
+    return {context.constant_values().GetInstId(self), interface};
+  };
+  auto replace_type_impls_constraint =
+      [&](SemIR::FacetTypeInfo::TypeImplsNamedConstraint impls)
+      -> SemIR::FacetTypeInfo::TypeImplsNamedConstraint {
+    auto self = SubstPeriodSelf(context, callbacks,
+                                context.constant_values().Get(impls.self_type));
+    auto constraint =
+        SubstPeriodSelf(context, callbacks, impls.specific_named_constraint);
+    return {context.constant_values().GetInstId(self), constraint};
+  };
+
+  SemIR::FacetTypeInfo info;
+  llvm::append_range(
+      info.extend_constraints,
+      llvm::map_range(orig_info.extend_constraints, replace_interface));
+  llvm::append_range(
+      info.extend_named_constraints,
+      llvm::map_range(orig_info.extend_named_constraints, replace_constraint));
+  llvm::append_range(
+      info.self_impls_constraints,
+      llvm::map_range(orig_info.self_impls_constraints, replace_interface));
+  llvm::append_range(info.self_impls_named_constraints,
+                     llvm::map_range(orig_info.self_impls_named_constraints,
+                                     replace_constraint));
+  llvm::append_range(info.type_impls_interfaces,
+                     llvm::map_range(orig_info.type_impls_interfaces,
+                                     replace_type_impls_interface));
+  llvm::append_range(info.type_impls_named_constraints,
+                     llvm::map_range(orig_info.type_impls_named_constraints,
+                                     replace_type_impls_constraint));
+  // TODO: Replace .Self in rewrites too. We need to actually validate rewrite
+  // constraints from named constraints in impl lookup (see
+  // todo_fail_require_with_mismatching_rewrite_constraint.carbon).
+  llvm::append_range(info.rewrite_constraints, orig_info.rewrite_constraints);
+
+  info.Canonicalize();
+  if (info == orig_info) {
+    // Nothing was substituted, keep the original instruction.
+    //
+    // It is noteworthy that we keep the non-canonical instruction here, since
+    // it may have a symbolic value (which is attached to a generic, and can be
+    // updated by specifics). Returning the canonical constraint instruction
+    // would lose the attachment to the generic which would be incorrect.
+    return constraint_inst_id;
+  }
+
+  return AddTypeInst<SemIR::FacetType>(
+      context, loc_id,
+      {.type_id = SemIR::TypeType::TypeId,
+       .facet_type_id = context.facet_types().Add(info)});
+}
+
 auto HandleParseNode(Context& context, Parse::RequireDeclId node_id) -> bool {
   auto [constraint_node_id, constraint_inst_id] =
       context.node_stack().PopExprWithNodeId();
   auto [self_node_id, self_inst_id] =
       context.node_stack().PopWithNodeId<Parse::NodeCategory::RequireImpls>();
 
-  auto decl_block_id = context.inst_block_stack().Pop();
-
   // Process modifiers.
   auto introducer =
       context.decl_introducer_state_stack().Pop<Lex::TokenKind::Require>();
@@ -294,6 +372,7 @@ auto HandleParseNode(Context& context, Parse::RequireDeclId node_id) -> bool {
       auto scope_id = context.scope_stack().PeekNameScopeId();
       context.name_scopes().Get(scope_id).set_has_error();
     }
+    context.inst_block_stack().Pop();
     DiscardGenericDecl(context);
     return true;
   }
@@ -302,19 +381,32 @@ auto HandleParseNode(Context& context, Parse::RequireDeclId node_id) -> bool {
   if (identified_facet_type->required_impls().empty()) {
     // A `require T impls type` adds no actual constraints, so nothing to do.
     // This is not an error though.
+    context.inst_block_stack().Pop();
     DiscardGenericDecl(context);
     return true;
   }
 
-  // TODO: Substitute .Self here.
-  auto constraint_type_inst_id =
-      context.types().GetAsTypeInstId(constraint_inst_id);
+  // The identified facet type also replaced `.Self` references, but we want to
+  // store the full facet type not just the identified one. So we have to
+  // replace `.Self` references explicitly here in the canonical constraint. We
+  // do this after `ValidateRequire()` which has ensured the constraint is in
+  // fact a FacetType.
+  auto constraint_type_inst_id = SubstPeriodSelfInConstraint(
+      context, constraint_node_id, self_inst_id,
+      context.types().GetAsTypeInstId(constraint_inst_id));
+  // The replacement of `.Self` can create a new FacetType instruction which we
+  // want to be part of the require decl's inst block, so we defer the Pop until
+  // after the subst.
+  auto decl_block_id = context.inst_block_stack().Pop();
 
   auto require_impls_decl =
       SemIR::RequireImplsDecl{// To be filled in after.
                               .require_impls_id = SemIR::RequireImplsId::None,
                               .decl_block_id = decl_block_id};
   auto decl_id = AddPlaceholderInst(context, node_id, require_impls_decl);
+  // TODO: We don't need to store the `self_inst_id` anymore, since we've
+  // encoded it into the constraints of the facet type which was converted to
+  // the form `<Self> where .Self impls <Constraint>`.
   auto require_impls_id = context.require_impls().Add(
       {.self_id = self_inst_id,
        .facet_type_inst_id = constraint_type_inst_id,

toolchain/check/impl_lookup.cpp

@@ -28,6 +28,7 @@
 #include "toolchain/sem_ir/ids.h"
 #include "toolchain/sem_ir/impl.h"
 #include "toolchain/sem_ir/inst.h"
+#include "toolchain/sem_ir/type_iterator.h"
 #include "toolchain/sem_ir/typed_insts.h"
 
 namespace Carbon::Check {
@@ -357,138 +358,71 @@ static auto IdentifyQuerySelfFacetType(Context& context, SemIR::LocId loc_id,
                                 /*allow_partially_identified=*/true);
 }
 
-// Substitutes witnesess in place of `LookupImplWitness` queries into `.Self`,
-// when the witness is for the same interface as the one `.Self` is referring
-// to.
-//
-// This allows access to the `FacetType` and its constraints from the witness,
-// and allows `ImplWitnessAccess` instructions to be immediately resolved to a
-// more specific value when possible.
-class SubstWitnessesCallbacks : public SubstInstCallbacks {
+// Given a query `orig_inst_self` and `orig_interface`, try find a matching
+// witness from impl lookup to use for the query.
+static auto TryFindMatchingWitnessFromImplLookup(
+    Context& context, SemIR::LocId loc_id,
+    SemIR::ConstantId canonical_query_self_const_id,
+    llvm::ArrayRef<SemIR::IdentifiedFacetType::RequiredImpl> req_impls,
+    llvm::ArrayRef<SemIR::InstId> found_witness_inst_ids,
+    SemIR::ConstantId orig_const_self, SemIR::SpecificInterface orig_interface)
+    -> SemIR::InstId {
+  // The `req_impls` come from an IdentifiedFacetType so they have `.Self`
+  // replaced. We need to do the same for the self and interface in the
+  // `orig_witness` for comparing with them.
+  SubstPeriodSelfCallbacks callbacks(&context, loc_id,
+                                     canonical_query_self_const_id);
+  orig_const_self = SubstPeriodSelf(context, callbacks, orig_const_self);
+  orig_interface = SubstPeriodSelf(context, callbacks, orig_interface);
+
+  // Witnesses have a canonicalized self value. Perform the same
+  // canonicalization here so that we can compare them.
+  orig_const_self =
+      GetCanonicalQuerySelfForLookupImplWitness(context, orig_const_self);
+
+  for (auto [req_impl, found_witness_inst_id] :
+       llvm::zip_equal(req_impls, found_witness_inst_ids)) {
+    auto [req_const_self, req_interface] = req_impl;
+    if (req_const_self == orig_const_self && req_interface == orig_interface) {
+      return found_witness_inst_id;
+    }
+  }
+  return SemIR::InstId::None;
+}
+
+class SubstPeriodSelfInRewriteCallbacks : public SubstPeriodSelfCallbacks {
  public:
-  // `context` must not be null.
-  explicit SubstWitnessesCallbacks(
+  explicit SubstPeriodSelfInRewriteCallbacks(
       Context* context, SemIR::LocId loc_id,
-      SemIR::ConstantId query_self_const_id,
+      SemIR::ConstantId period_self_replacement_id,
       llvm::ArrayRef<SemIR::IdentifiedFacetType::RequiredImpl> req_impls,
       llvm::ArrayRef<SemIR::InstId> witness_inst_ids)
-      : SubstInstCallbacks(context),
-        loc_id_(loc_id),
-        canonical_query_self_const_id_(
-            GetCanonicalFacetOrTypeValue(*context, query_self_const_id)),
+      : SubstPeriodSelfCallbacks(context, loc_id, period_self_replacement_id),
         req_impls_(req_impls),
         witness_inst_ids_(witness_inst_ids) {}
 
-  auto Subst(SemIR::InstId& inst_id) -> SubstResult override {
-    // `FacetType` can be concrete even when it has rewrite constraints that
-    // have a symbolic dependency on `.Self`. See use of
-    // `GetConstantValueIgnoringPeriodSelf` in eval. So in order to recurse into
-    // `FacetType` we must check for it before the `is_concrete` early return.
-    if (context().insts().Is<SemIR::FacetType>(inst_id)) {
-      ++facet_type_depth_;
-      return SubstOperands;
-    }
-
-    if (context().constant_values().Get(inst_id).is_concrete()) {
-      return FullySubstituted;
-    }
-
-    auto access = context().insts().TryGetAs<SemIR::ImplWitnessAccess>(inst_id);
-    if (!access) {
-      return SubstOperands;
-    }
-
-    auto lookup =
-        context().insts().GetAs<SemIR::LookupImplWitness>(access->witness_id);
-    auto bind_name = context().insts().TryGetAs<SemIR::SymbolicBinding>(
-        lookup.query_self_inst_id);
-    if (!bind_name) {
-      return SubstOperands;
-    }
-
-    const auto& self_entity_name =
-        context().entity_names().Get(bind_name->entity_name_id);
-    if (self_entity_name.name_id != SemIR::NameId::PeriodSelf) {
-      return SubstOperands;
-    }
-
-    // TODO: Once we are numbering `EntityName`, (see the third model in
-    // https://docs.google.com/document/d/1Yt-i5AmF76LSvD4TrWRIAE_92kii6j5yFiW-S7ahzlg/edit?tab=t.0#heading=h.7urbxcq23olv)
-    // then verify that the index here is equal to the `facet_type_depth_`,
-    // which would mean that it is a reference to the top-level `Self`, which is
-    // being replaced with the impl lookup query self facet value (and then we
-    // use the witness derived from it).
-    //
-    // For now, we only substitute if depth == 0, which is incorrect inside
-    // nested facet types, as it can miss references in specifics up to the top
-    // level facet value.
-    if (facet_type_depth_ > 0) {
-      return SubstOperands;
-    }
-
-    auto witness_id =
-        FindWitnessForInterface(lookup.query_specific_interface_id);
-    if (!witness_id.has_value()) {
-      return SubstOperands;
-    }
-
-    inst_id = RebuildNewInst(
-        context().insts().GetLocIdForDesugaring(loc_id_),
-        SemIR::ImplWitnessAccess{.type_id = GetSingletonType(
-                                     context(), SemIR::WitnessType::TypeInstId),
-                                 .witness_id = witness_id,
-                                 .index = access->index});
-    // Once we replace a witness, we either have a concrete value or some
-    // reference to an associated constant that came from the witness's facet
-    // type. We don't want to substitute into the witness's facet type, so we
-    // don't recurse on whatever came from the witness.
-    return FullySubstituted;
-  }
-
   auto Rebuild(SemIR::InstId orig_inst_id, SemIR::Inst new_inst)
       -> SemIR::InstId override {
-    if (context().insts().Is<SemIR::FacetType>(orig_inst_id)) {
-      --facet_type_depth_;
+    // When rebuilding a witness where `.Self` was replaced, use a witness we
+    // found in impl lookup instead of performing impl lookup again.
+    if (auto lookup = new_inst.TryAs<SemIR::LookupImplWitness>()) {
+      auto witness = TryFindMatchingWitnessFromImplLookup(
+          context(), loc_id(), period_self_replacement_id(), req_impls_,
+          witness_inst_ids_,
+          context().constant_values().Get(lookup->query_self_inst_id),
+          context().specific_interfaces().Get(
+              lookup->query_specific_interface_id));
+      if (witness.has_value()) {
+        return witness;
+      }
     }
-    return RebuildNewInst(loc_id_, new_inst);
-  }
 
-  auto ReuseUnchanged(SemIR::InstId orig_inst_id) -> SemIR::InstId override {
-    if (context().insts().Is<SemIR::FacetType>(orig_inst_id)) {
-      --facet_type_depth_;
-    }
-    return orig_inst_id;
+    return SubstPeriodSelfCallbacks::Rebuild(orig_inst_id, new_inst);
   }
 
  private:
-  auto FindWitnessForInterface(SemIR::SpecificInterfaceId specific_interface_id)
-      -> SemIR::InstId {
-    auto lookup_query_interface =
-        context().specific_interfaces().Get(specific_interface_id);
-    for (auto [req_impl, witness_inst_id] :
-         llvm::zip_equal(req_impls_, witness_inst_ids_)) {
-      auto [req_self, req_interface] = req_impl;
-      // The `LookupImplWitness` is for `.Self`, so if the witness is for some
-      // type other than the query self, we can't use it for `.Self`.
-      if (req_self != canonical_query_self_const_id_) {
-        continue;
-      }
-      // If the `LookupImplWitness` for `.Self` is not looking for the same
-      // interface as we have a witness for, this is not the right witness to
-      // use to replace the lookup for `.Self`.
-      if (req_interface.interface_id != lookup_query_interface.interface_id) {
-        continue;
-      }
-      return witness_inst_id;
-    }
-    return SemIR::InstId::None;
-  }
-
-  SemIR::LocId loc_id_;
-  SemIR::ConstantId canonical_query_self_const_id_;
   llvm::ArrayRef<SemIR::IdentifiedFacetType::RequiredImpl> req_impls_;
   llvm::ArrayRef<SemIR::InstId> witness_inst_ids_;
-  int facet_type_depth_ = 0;
 };
 
 static auto VerifyQueryFacetTypeConstraints(
@@ -503,17 +437,30 @@ static auto VerifyQueryFacetTypeConstraints(
           .facet_type_id);
 
   if (!facet_type_info.rewrite_constraints.empty()) {
-    auto callbacks = SubstWitnessesCallbacks(
+    SubstPeriodSelfInRewriteCallbacks callbacks(
         &context, loc_id, query_self_const_id, req_impls, witness_inst_ids);
 
     for (const auto& rewrite : facet_type_info.rewrite_constraints) {
-      auto lhs_id = SubstInst(context, rewrite.lhs_id, callbacks);
-      auto rhs_id = SubstInst(context, rewrite.rhs_id, callbacks);
+      // Replace `.Self` in rewrite constraints with the query self in order to
+      // find the provided values of rewrite constraints from the query. This
+      // includes replacing `.Self` in LookupImplWitness instructions.
+      //
+      // When we have found a witness in impl lookup for the query in a
+      // LookupImplWitness insts, we need to use that witness directly instead
+      // of rebuilding (and reevaluating) the LookupImplWitness which will
+      // execute another impl lookup.
+
+      auto lhs_id = context.constant_values().GetInstId(SubstPeriodSelf(
+          context, callbacks, context.constant_values().Get(rewrite.lhs_id)));
+      auto rhs_id = context.constant_values().GetInstId(SubstPeriodSelf(
+          context, callbacks, context.constant_values().Get(rewrite.rhs_id)));
+
       if (lhs_id != rhs_id) {
         // TODO: Provide a diagnostic note and location for which rewrite
         // constraint was not satisfied, if a diagnostic is going to be
-        // displayed for the LookupImplWitessFailure. This will require plumbing
-        // through a callback that lets us add a Note to another diagnostic.
+        // displayed for the LookupImplWitness() failure. This may require
+        // plumbing through a callback that lets us add a Note to another
+        // diagnostic.
         return false;
       }
     }
@@ -1021,6 +968,33 @@ auto LookupImplWitness(Context& context, SemIR::LocId loc_id,
   return context.inst_blocks().AddCanonical(result_witness_ids);
 }
 
+auto GetCanonicalQuerySelfForLookupImplWitness(Context& context,
+                                               SemIR::ConstantId self,
+                                               SemIR::InstId* out_facet_value)
+    -> SemIR::ConstantId {
+  auto self_inst_id = context.constant_values().GetInstId(self);
+
+  // If the monomorphized query self is a FacetValue, we may get a witness from
+  // it under limited circumstances. If no final witness is found though, we
+  // don't need to preserve it for future evaluations, so we strip it from the
+  // LookupImplWitness instruction to reduce the number of distinct constant
+  // values.
+  if (auto facet_value =
+          context.insts().TryGetAs<SemIR::FacetValue>(self_inst_id)) {
+    if (out_facet_value) {
+      *out_facet_value = self_inst_id;
+    }
+    self_inst_id = facet_value->type_inst_id;
+  }
+
+  // The self value is canonicalized in order to produce a canonical
+  // LookupImplWitness instruction, avoiding multiple constant values for
+  // `<facet value>` and `<facet value> as type`, which always have the same
+  // lookup result.
+  return GetCanonicalFacetOrTypeValue(
+      context, context.constant_values().Get(self_inst_id));
+}
+
 // Record the query which found a final impl witness. It's illegal to
 // write a final impl afterward that would match the same query.
 static auto PoisonImplLookupQuery(Context& context, SemIR::LocId loc_id,

toolchain/check/impl_lookup.h

@@ -47,6 +47,17 @@ auto LookupMatchesImpl(Context& context, SemIR::LocId loc_id,
                        SemIR::SpecificInterface query_specific_interface,
                        SemIR::ImplId target_impl) -> bool;
 
+// Given a self facet, returns the canonical query self for a LookupImplWitness
+// instruction. The canonicalization looks through `FacetValue` and makes a
+// canonical form for `facet` and `facet as type`.
+//
+// If the input self facet is a `FacetValue` that is looked through, it can be
+// returned in `out_facet_value`, in order to preserve its facet type and
+// witnesses.
+auto GetCanonicalQuerySelfForLookupImplWitness(
+    Context& context, SemIR::ConstantId self,
+    SemIR::InstId* out_facet_value = nullptr) -> SemIR::ConstantId;
+
 // The kind of impl lookup being performed by a call to
 // `EvalLookupSingleFinalWitness`.
 enum class EvalImplLookupMode {

toolchain/check/testdata/facet/access.carbon

@@ -80,7 +80,7 @@ fn UseIndirect[T:! I](x: T) -> T {
 //@dump-sem-ir-end
 }
 
-// --- fail_todo_convert_from_period_self_to_full_facet_value.carbon
+// --- convert_from_period_self_to_full_facet_value.carbon
 library "[[@TEST_NAME]]";
 
 interface I {
@@ -88,15 +88,7 @@ interface I {
 }
 
 fn F(U:! I where .I1 = .Self) {
-  // CHECK:STDERR: fail_todo_convert_from_period_self_to_full_facet_value.carbon:[[@LINE+4]]:3: error: cannot convert type `U` that implements `I where .(I.I1) = .Self` into type implementing `I where .(I.I1) = U` [ConversionFailureFacetToFacet]
-  // CHECK:STDERR:   U as (I where .I1 = U);
-  // CHECK:STDERR:   ^~~~~~~~~~~~~~~~~~~~~~
-  // CHECK:STDERR:
   U as (I where .I1 = U);
-  // CHECK:STDERR: fail_todo_convert_from_period_self_to_full_facet_value.carbon:[[@LINE+4]]:3: error: cannot convert type `U` that implements `I where .(I.I1) = .Self` into type implementing `I where .(I.I1) = U` [ConversionFailureFacetToFacet]
-  // CHECK:STDERR:   (U as type) as (I where .I1 = U);
-  // CHECK:STDERR:   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-  // CHECK:STDERR:
   (U as type) as (I where .I1 = U);
 }
 
@@ -134,7 +126,7 @@ fn F(U:! I where .X = .Self, unused V: U) {
   F2(U.G());
 }
 
-// --- fail_todo_access_through_call.carbon
+// --- access_through_call.carbon
 library "[[@TEST_NAME]]";
 
 interface I {
@@ -147,55 +139,18 @@ fn F3[U:! I where .X = .Self](unused V: U*) {}
 
 fn F(U:! I where .X = .Self, unused V: U*) {
   // The returned value of `G` type `U` which has access to the methods of `I`.
-  //
-  // TODO: These should work.
-  // - The first `.` is on a NameRef of type FacetType for `I where .X = .Self`.
-  //   - This finds `G` through the FacetType.
-  // - The second `.` is on a Call of type FacetAccessType into `SymbolicBinding` with type FacetType for `I`.
-  //   - This finds `G` through the FacetType (impl lookup strips off FacetAccessType).
-  // - The third `.` is on a Call of type FacetAccessType into `ImplWitnessAccess` of `I.X` into `LookupImplWitness`, which has type `type`
-  //   - Can't make calls on an `ImplWitnessAccess`.
-  //   - We could expect that the constant value of the `ImplWitnessAccess` would
-  //     be the same type that we got for the second lookup.
-  // CHECK:STDERR: fail_todo_access_through_call.carbon:[[@LINE+4]]:3: error: type `.(I.X)` does not support qualified expressions [QualifiedExprUnsupported]
-  // CHECK:STDERR:   U.G()->G()->G();
-  // CHECK:STDERR:   ^~~~~~~~~~~~~
-  // CHECK:STDERR:
   U.G()->G()->G();
-  // CHECK:STDERR: fail_todo_access_through_call.carbon:[[@LINE+4]]:3: error: type `.(I.X)` does not support qualified expressions [QualifiedExprUnsupported]
-  // CHECK:STDERR:   (U as type).G()->G()->G();
-  // CHECK:STDERR:   ^~~~~~~~~~~~~~~~~~~~~~~
-  // CHECK:STDERR:
   (U as type).G()->G()->G();
 
   // The returned value of type `U` can be used as a value of type `U`.
-  //
-  // TODO: This should work.
-  // CHECK:STDERR: fail_todo_access_through_call.carbon:[[@LINE+4]]:6: error: type `.(I.X)` does not support qualified expressions [QualifiedExprUnsupported]
-  // CHECK:STDERR:   F2(U.G()->G()->G());
-  // CHECK:STDERR:      ^~~~~~~~~~~~~
-  // CHECK:STDERR:
   F2(U.G()->G()->G());
 
   // The constraints in the type `U` are preserved.
-  //
-  // TODO: These should work.
-  // CHECK:STDERR: fail_todo_access_through_call.carbon:[[@LINE+7]]:3: error: cannot convert type `.Self` that implements `I` into type implementing `I where .(I.X) = .Self` [ConversionFailureFacetToFacet]
-  // CHECK:STDERR:   F3(U.G());
-  // CHECK:STDERR:   ^~~~~~~~~
-  // CHECK:STDERR: fail_todo_access_through_call.carbon:[[@LINE-40]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
-  // CHECK:STDERR: fn F3[U:! I where .X = .Self](unused V: U*) {}
-  // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-  // CHECK:STDERR:
   F3(U.G());
-  // CHECK:STDERR: fail_todo_access_through_call.carbon:[[@LINE+4]]:6: error: type `.(I.X)` does not support qualified expressions [QualifiedExprUnsupported]
-  // CHECK:STDERR:   F3(U.G()->G()->G());
-  // CHECK:STDERR:      ^~~~~~~~~~~~~
-  // CHECK:STDERR:
   F3(U.G()->G()->G());
 }
 
-// --- fail_todo_compound_access_through_call.carbon
+// --- fail_compound_access_through_call.carbon
 library "[[@TEST_NAME]]";
 
 interface I {
@@ -203,30 +158,21 @@ interface I {
   fn G() -> X;
 }
 
-fn F(U:! I where .X = .Self) {
+fn F(U:! Core.Destroy & I where .X = .Self) {
   // Compound member lookup through a non-type value is possible for methods
   // which take a `self` parameter. But it's not possible for methods without
   // `self`. For those you need to go directly throug the type.
   // See: https://github.com/carbon-language/carbon-lang/issues/6025
 
-  // TODO: This step should work.
-  //
-  // CHECK:STDERR: fail_todo_compound_access_through_call.carbon:[[@LINE+7]]:14: error: cannot implicitly convert expression of type `.Self` to `U` [ConversionFailure]
-  // CHECK:STDERR:   let u: U = U.(I.G)();
-  // CHECK:STDERR:              ^~~~~~~~~
-  // CHECK:STDERR: fail_todo_compound_access_through_call.carbon:[[@LINE+4]]:14: note: type `.Self` does not implement interface `Core.ImplicitAs(U)` [MissingImplInMemberAccessInContext]
-  // CHECK:STDERR:   let u: U = U.(I.G)();
-  // CHECK:STDERR:              ^~~~~~~~~
-  // CHECK:STDERR:
   let u: U = U.(I.G)();
   // `u` is a non-type value. Can call methods with `self` through compound
   // member lookup, but can't call methods without `self`. See the
   // `compound_access_through_call_with_self_param.carbon` test for the former.
   //
-  // CHECK:STDERR: fail_todo_compound_access_through_call.carbon:[[@LINE+7]]:3: error: cannot implicitly convert non-type value of type `U` into type implementing `I` [ConversionFailureNonTypeToFacet]
+  // CHECK:STDERR: fail_compound_access_through_call.carbon:[[@LINE+7]]:3: error: cannot implicitly convert non-type value of type `U` into type implementing `I` [ConversionFailureNonTypeToFacet]
   // CHECK:STDERR:   u.(I.G)();
   // CHECK:STDERR:   ^~~~~~~
-  // CHECK:STDERR: fail_todo_compound_access_through_call.carbon:[[@LINE+4]]:3: note: type `U` does not implement interface `Core.ImplicitAs(I)` [MissingImplInMemberAccessInContext]
+  // CHECK:STDERR: fail_compound_access_through_call.carbon:[[@LINE+4]]:3: note: type `U` does not implement interface `Core.ImplicitAs(I)` [MissingImplInMemberAccessInContext]
   // CHECK:STDERR:   u.(I.G)();
   // CHECK:STDERR:   ^~~~~~~
   // CHECK:STDERR:
@@ -235,17 +181,17 @@ fn F(U:! I where .X = .Self) {
   // This is the same as the above, since G() returns a non-type value of type
   // `U`.
   //
-  // CHECK:STDERR: fail_todo_compound_access_through_call.carbon:[[@LINE+7]]:3: error: cannot implicitly convert non-type value of type `.Self` into type implementing `I` [ConversionFailureNonTypeToFacet]
+  // CHECK:STDERR: fail_compound_access_through_call.carbon:[[@LINE+7]]:3: error: cannot implicitly convert non-type value of type `U` into type implementing `I` [ConversionFailureNonTypeToFacet]
   // CHECK:STDERR:   U.(I.G)().(I.G)();
   // CHECK:STDERR:   ^~~~~~~~~~~~~~~
-  // CHECK:STDERR: fail_todo_compound_access_through_call.carbon:[[@LINE+4]]:3: note: type `.Self` does not implement interface `Core.ImplicitAs(I)` [MissingImplInMemberAccessInContext]
+  // CHECK:STDERR: fail_compound_access_through_call.carbon:[[@LINE+4]]:3: note: type `U` does not implement interface `Core.ImplicitAs(I)` [MissingImplInMemberAccessInContext]
   // CHECK:STDERR:   U.(I.G)().(I.G)();
   // CHECK:STDERR:   ^~~~~~~~~~~~~~~
   // CHECK:STDERR:
   U.(I.G)().(I.G)();
 }
 
-// --- fail_todo_compound_access_through_call_with_self_param.carbon
+// --- compound_access_through_call_with_self_param.carbon
 library "[[@TEST_NAME]]";
 
 interface I {
@@ -257,15 +203,6 @@ fn F(U:! I where .X = .Self, v: U) {
   // Compound member lookup through a non-type value is possible for methods
   // which take a `self` parameter.
 
-  // TODO: This should all work.
-
-  // CHECK:STDERR: fail_todo_compound_access_through_call_with_self_param.carbon:[[@LINE+7]]:15: error: cannot implicitly convert expression of type `.Self*` to `U*` [ConversionFailure]
-  // CHECK:STDERR:   let u: U* = v.(I.G)();
-  // CHECK:STDERR:               ^~~~~~~~~
-  // CHECK:STDERR: fail_todo_compound_access_through_call_with_self_param.carbon:[[@LINE+4]]:15: note: type `.Self*` does not implement interface `Core.ImplicitAs(U*)` [MissingImplInMemberAccessInContext]
-  // CHECK:STDERR:   let u: U* = v.(I.G)();
-  // CHECK:STDERR:               ^~~~~~~~~
-  // CHECK:STDERR:
   let u: U* = v.(I.G)();
   // `u` is a non-type value. Can call methods with `self` through compound
   // member lookup, but can't call methods without `self`. See the
@@ -831,11 +768,11 @@ fn F2(U:! Z) {
 // CHECK:STDOUT:   %AB: %facet_type.82c = symbolic_binding AB, 0 [symbolic]
 // CHECK:STDOUT:   %AB.binding.as_type: type = symbolic_binding_type AB, 0, %AB [symbolic]
 // CHECK:STDOUT:   %A.lookup_impl_witness.1b9: <witness> = lookup_impl_witness %AB, @A [symbolic]
+// CHECK:STDOUT:   %B.lookup_impl_witness.97b: <witness> = lookup_impl_witness %AB, @B [symbolic]
 // CHECK:STDOUT:   %.262: Core.Form = init_form %empty_tuple.type [concrete]
 // CHECK:STDOUT:   %pattern_type.cb1: type = pattern_type %empty_tuple.type [concrete]
 // CHECK:STDOUT:   %F.type: type = fn_type @F [concrete]
 // CHECK:STDOUT:   %F: %F.type = struct_value () [concrete]
-// CHECK:STDOUT:   %B.lookup_impl_witness.97b: <witness> = lookup_impl_witness %AB, @B [symbolic]
 // CHECK:STDOUT:   %.469: Core.Form = init_form %empty_struct_type [concrete]
 // CHECK:STDOUT:   %pattern_type.a96: type = pattern_type %empty_struct_type [concrete]
 // CHECK:STDOUT:   %G.type: type = fn_type @G [concrete]

toolchain/check/testdata/facet/early_rewrites.carbon

@@ -293,7 +293,7 @@ fn G(T:! J where .J1 = D) {
   F(T);
 }
 
-// --- fail_todo_early_rewrite_applied_extra_indirection.carbon
+// --- early_rewrite_applied_extra_indirection.carbon
 library "[[@TEST_NAME]]";
 
 interface Z {
@@ -310,20 +310,15 @@ impl () as Tuple {}
 class C(T:! Tuple) {}
 
 interface J {
-  // Implied: .Z1 == (), but this is also explicitly required for J1.
+  // .Z2 depends on an two nested accesses of rewrite constraints.
   let J1:! Y & Z where .Y1 = .Self and .Z1 = () and .Z2 = C(.Y1.Z1);
 }
 
 fn F(unused T:! J) {}
 
 class D;
-// Satisfies the implied constraint in J.J1.
 impl D as Z where .Z1 = () and .Z2 = C(()) {}
 impl D as Y where .Y1 = D {}
-// CHECK:STDERR: fail_todo_early_rewrite_applied_extra_indirection.carbon:[[@LINE+4]]:24: error: cannot convert type `D` into type implementing `Z & Y where .(Y.Y1) = .Self as Z and .(Z.Z1) = () and .(Z.Z2) = C(() as Tuple)` [ConversionFailureTypeToFacet]
-// CHECK:STDERR: fn G(T:! J where .J1 = D) {
-// CHECK:STDERR:                        ^
-// CHECK:STDERR:
 fn G(T:! J where .J1 = D) {
   F(T);
 }

toolchain/check/testdata/facet/period_self.carbon

@@ -54,25 +54,17 @@ interface I(T:! .Self) {
   fn G() -> T;
 }
 
-// --- fail_todo_convert_period_self_to_full_facet_value.carbon
+// --- convert_period_self_to_full_facet_value.carbon
 library "[[@TEST_NAME]]";
 
 interface I(T:! type) {}
 
 fn F(U:! I(.Self)) {
-  // CHECK:STDERR: fail_todo_convert_period_self_to_full_facet_value.carbon:[[@LINE+4]]:3: error: cannot convert type `U` that implements `I(.Self)` into type implementing `I(U)` [ConversionFailureFacetToFacet]
-  // CHECK:STDERR:   U as I(U);
-  // CHECK:STDERR:   ^~~~~~~~~
-  // CHECK:STDERR:
   U as I(U);
-  // CHECK:STDERR: fail_todo_convert_period_self_to_full_facet_value.carbon:[[@LINE+4]]:3: error: cannot convert type `U` that implements `I(.Self)` into type implementing `I(U)` [ConversionFailureFacetToFacet]
-  // CHECK:STDERR:   (U as type) as I(U);
-  // CHECK:STDERR:   ^~~~~~~~~~~~~~~~~~~
-  // CHECK:STDERR:
   (U as type) as I(U);
 }
 
-// --- fail_todo_convert_period_self_to_full_facet_value_with_assoc_constant.carbon
+// --- convert_period_self_to_full_facet_value_with_assoc_constant.carbon
 library "[[@TEST_NAME]]";
 
 interface I(T:! type) {
@@ -80,15 +72,7 @@ interface I(T:! type) {
 }
 
 fn F(U:! I(.Self) where .X = .Self) {
-  // CHECK:STDERR: fail_todo_convert_period_self_to_full_facet_value_with_assoc_constant.carbon:[[@LINE+4]]:3: error: cannot convert type `U` that implements `I(.Self) where .(I(.Self).X) = .Self` into type implementing `I(U) where .(I(U).X) = U` [ConversionFailureFacetToFacet]
-  // CHECK:STDERR:   U as (I(U) where .X = U);
-  // CHECK:STDERR:   ^~~~~~~~~~~~~~~~~~~~~~~~
-  // CHECK:STDERR:
   U as (I(U) where .X = U);
-  // CHECK:STDERR: fail_todo_convert_period_self_to_full_facet_value_with_assoc_constant.carbon:[[@LINE+4]]:3: error: cannot convert type `U` that implements `I(.Self) where .(I(.Self).X) = .Self` into type implementing `I(U) where .(I(U).X) = U` [ConversionFailureFacetToFacet]
-  // CHECK:STDERR:   (U as type) as (I(U) where .X = U);
-  // CHECK:STDERR:   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-  // CHECK:STDERR:
   (U as type) as (I(U) where .X = U);
 }
 
@@ -228,7 +212,7 @@ fn F(U:! I(.Self)) {
   let unused a: U = U.G();
 }
 
-// --- fail_todo_return_of_type_period_self_assoc_const_has_type_u.carbon
+// --- return_of_type_period_self_assoc_const_has_type_u.carbon
 library "[[@TEST_NAME]]";
 
 interface I {
@@ -236,14 +220,7 @@ interface I {
   fn G() -> X;
 }
 
-fn F(U:! I where .X = .Self) {
-  // CHECK:STDERR: fail_todo_return_of_type_period_self_assoc_const_has_type_u.carbon:[[@LINE+7]]:21: error: cannot implicitly convert expression of type `.Self` to `U` [ConversionFailure]
-  // CHECK:STDERR:   let unused a: U = U.G();
-  // CHECK:STDERR:                     ^~~~~
-  // CHECK:STDERR: fail_todo_return_of_type_period_self_assoc_const_has_type_u.carbon:[[@LINE+4]]:21: note: type `.Self` does not implement interface `Core.ImplicitAs(U)` [MissingImplInMemberAccessInContext]
-  // CHECK:STDERR:   let unused a: U = U.G();
-  // CHECK:STDERR:                     ^~~~~
-  // CHECK:STDERR:
+fn F(U:! Core.Destroy & I where .X = .Self) {
   let unused a: U = U.G();
 }
 
@@ -330,7 +307,7 @@ interface I(T:! Core.Destroy) {}
 // CHECK:STDERR:
 fn F(unused U:! Core.Destroy & I(.Self)) {}
 
-// --- fail_todo_compound_lookup_on_returned_period_self_parameter.carbon
+// --- compound_lookup_on_returned_period_self_parameter.carbon
 library "[[@TEST_NAME]]";
 
 interface I(T:! Core.Destroy) {
@@ -341,14 +318,160 @@ fn F[U:! Core.Destroy where .Self impls I(.Self)](u: U) {
   // This tests that both `I.G` is accessible and that `Destroy` is preserved;
   // we'd get an error for missing Destroy otherwise since G() returns an
   // initializing expression.
-
-  // CHECK:STDERR: fail_todo_compound_lookup_on_returned_period_self_parameter.carbon:[[@LINE+4]]:3: error: cannot access member of interface `I(U as Core.Destroy)` in type `U` that does not implement that interface [MissingImplInMemberAccess]
-  // CHECK:STDERR:   u.(I(U).G)().(I(U).G)().(I(U).G)();
-  // CHECK:STDERR:   ^~~~~~~~~~
-  // CHECK:STDERR:
   u.(I(U).G)().(I(U).G)().(I(U).G)();
 }
 
+// --- unambiguous_period_self.carbon
+library "[[@TEST_NAME]]";
+
+interface Z(T:! type) {}
+interface Y(T:! type) {
+  let Y1:! type;
+  let Y2:! type;
+}
+interface X(T:! type) {}
+
+class P;
+class Q(T:! type);
+class R(T:! type);
+
+fn A(unused T:! Z(.Self) where .Self impls (Y(.Self) where .Self impls X(.Self))) {}
+//                ^T as type   ^T as Z(T)     ^T as Z(T)   ^T as Z(T) & Y(T)
+//                                                                       ^ T as Z(T) & Y(T)
+
+fn B(unused T:! Z(.Self) where .Self impls (Y(.Self) where Q(.Self) impls X(.Self))) {}
+//                ^T as type   ^T as Z(T)     ^T as Z(T)     ^T as Z(T) & Y(T)
+//                                                                          ^ T as Z(T) & Y(T)
+
+fn C(unused T:! Z(.Self) where .Self impls (Y(.Self) where .Y1 = .Self)) {}
+//                ^T as type   ^T as Z(T)     ^T as Z(T)   ^T as Z(T) & Y(T)
+//                                                               ^ T as Z(T) & Y(T)
+
+// This introduces a different meaning of `.Self`, but we allow it here.
+fn D(unused T:! Z(.Self) where R(.Self) impls (Y(.Self) where .Self impls X(P))) {}
+//                ^T as type     ^T as Z(T)      ^T as Z(T)   ^R(T as Z(T)) as Y(T as Z(T))
+
+// This introduces a different meaning of `.Self`, but we allow it here.
+fn E(unused T:! Z(.Self) where R(.Self) impls (Y(.Self) where .Y1 = .Y2)) {}
+//                ^T as type     ^T as Z(T)      ^T as Z(T)   ^R(T as Z(T)) as Y(T as Z(T))
+//                                                                  ^R(T as Z(T)) as Y(T as Z(T))
+
+// --- fail_todo_period_self_impls_ambiguous_period_self_access_argument.carbon
+library "[[@TEST_NAME]]";
+
+interface Z(T:! type) {}
+interface Y(T:! type) {
+  let Y1:! type;
+}
+interface X(T:! type) {}
+
+class R(T:! type);
+
+// CHECK:STDERR: fail_todo_period_self_impls_ambiguous_period_self_access_argument.carbon:[[@LINE+4]]:32: error: `.Self` is ambiguous after nested `where` in `<type> impls ...` clause. [AmbiguousPeriodSelf]
+// CHECK:STDERR: fn C(unused T:! Z(.Self) where R(.Self) impls (Y(.Self) where .Self impls X(.Y1))) {}
+// CHECK:STDERR:                                ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR:
+fn C(unused T:! Z(.Self) where R(.Self) impls (Y(.Self) where .Self impls X(.Y1))) {}
+//                ^T as type     ^T as Z(T)      ^T as Z(T)   ^R(T as Z(T)) as Y(T as Z(T))
+//                                                                          ^ERROR: R(T as Z(T)) as Y(T as Z(T))
+
+// --- fail_type_impls_ambiguous_period_self_argument.carbon
+library "[[@TEST_NAME]]";
+
+interface Z(T:! type) {}
+interface Y(T:! type) {}
+interface X(T:! type) {}
+interface W {}
+
+class P;
+class Q(T:! type);
+class R(T:! type);
+
+// CHECK:STDERR: fail_type_impls_ambiguous_period_self_argument.carbon:[[@LINE+4]]:32: error: `.Self` is ambiguous after nested `where` in `<type> impls ...` clause. [AmbiguousPeriodSelf]
+// CHECK:STDERR: fn A(unused T:! Z(.Self) where R(.Self) impls (Y(.Self) where P impls X(.Self))) {}
+// CHECK:STDERR:                                ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR:
+fn A(unused T:! Z(.Self) where R(.Self) impls (Y(.Self) where P impls X(.Self))) {}
+//                ^T as type     ^T as Z(T)      ^T as Z(T)             ^ERROR: R(T as Z(T)) as Y(T as Z(T))
+
+// --- fail_ambiguous_period_self_argument_impls.carbon
+library "[[@TEST_NAME]]";
+
+interface Z(T:! type) {}
+interface Y(T:! type) {}
+interface X {}
+
+class Q(T:! type);
+class R(T:! type);
+
+// CHECK:STDERR: fail_ambiguous_period_self_argument_impls.carbon:[[@LINE+4]]:32: error: `.Self` is ambiguous after nested `where` in `<type> impls ...` clause. [AmbiguousPeriodSelf]
+// CHECK:STDERR: fn B(unused T:! Z(.Self) where R(.Self) impls (Y(.Self) where Q(.Self) impls X)) {}
+// CHECK:STDERR:                                ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR:
+fn B(unused T:! Z(.Self) where R(.Self) impls (Y(.Self) where Q(.Self) impls X)) {}
+//                ^T as type     ^T as Z(T)      ^T as Z(T)     ^ERROR: R(T as Z(T)) as Y(T as Z(T))
+
+// --- fail_period_self_impls_ambiguous_period_self_argument.carbon
+library "[[@TEST_NAME]]";
+
+interface Z(T:! type) {}
+interface Y(T:! type) {}
+interface X(T:! type) {}
+
+class R(T:! type);
+
+// CHECK:STDERR: fail_period_self_impls_ambiguous_period_self_argument.carbon:[[@LINE+4]]:32: error: `.Self` is ambiguous after nested `where` in `<type> impls ...` clause. [AmbiguousPeriodSelf]
+// CHECK:STDERR: fn C(unused T:! Z(.Self) where R(.Self) impls (Y(.Self) where .Self impls X(.Self))) {}
+// CHECK:STDERR:                                ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR:
+fn C(unused T:! Z(.Self) where R(.Self) impls (Y(.Self) where .Self impls X(.Self))) {}
+//                ^T as type     ^T as Z(T)      ^T as Z(T)   ^R(T as Z(T)) as Y(T as Z(T))
+//                                                                          ^ERROR: R(T as Z(T)) as Y(T as Z(T))
+
+// --- todo_fail_rewrite_rhs_ambiguous_period_self.carbon
+library "[[@TEST_NAME]]";
+
+interface Z(T:! type) {}
+interface Y(T:! type) {
+  let Y1:! type;
+}
+
+class R(T:! type);
+
+fn D(unused T:! Z(.Self) where R(.Self) impls (Y(.Self) where .Y1 = .Self)) {}
+//                ^T as type     ^T as Z(T)      ^T as Z(T)   ^R(T as Z(T)) as Y(T as Z(T))
+//                                                                  ^ERROR: R(T as Z(T)) as Y(T as Z(T))
+
+// --- impl_as_rewrite_with_period_self.carbon
+library "[[@TEST_NAME]]";
+
+interface Z {
+  let Z1:! type;
+}
+
+class C;
+impl C as Z where .Z1 = .Self {}
+
+fn F() {
+  C as (Z where .Z1 = C);
+}
+
+// --- impl_as_impls_with_period_self.carbon
+library "[[@TEST_NAME]]";
+
+interface Z {
+  let Z1:! type;
+}
+interface Y {}
+
+class C;
+impl C as Z where .Z1 = .Self {}
+impl C as Y {}
+
+fn F() {
+  C as (Z where .Z1 impls Y);
+}
+
 // CHECK:STDOUT: --- period_self_param.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
@@ -377,8 +500,9 @@ fn F[U:! Core.Destroy where .Self impls I(.Self)](u: U) {
 // CHECK:STDOUT:   %pattern_type.033: type = pattern_type %I_where.type [symbolic_self]
 // CHECK:STDOUT:   %T.706: %I_where.type = symbolic_binding T, 0 [symbolic]
 // CHECK:STDOUT:   %T.binding.as_type: type = symbolic_binding_type T, 0, %T.706 [symbolic]
-// CHECK:STDOUT:   %I.lookup_impl_witness.94d: <witness> = lookup_impl_witness %T.706, @I, @I(%.Self.binding.as_type.8db) [symbolic]
-// CHECK:STDOUT:   %I.facet: %I.type.bee = facet_value %T.binding.as_type, (%I.lookup_impl_witness.94d) [symbolic]
+// CHECK:STDOUT:   %facet_value: %type = facet_value %T.binding.as_type, () [symbolic]
+// CHECK:STDOUT:   %I.lookup_impl_witness.7f4: <witness> = lookup_impl_witness %T.706, @I, @I(%T.binding.as_type) [symbolic]
+// CHECK:STDOUT:   %I.facet: %I.type.bee = facet_value %T.binding.as_type, (%I.lookup_impl_witness.7f4) [symbolic]
 // CHECK:STDOUT:   %.262: Core.Form = init_form %empty_tuple.type [concrete]
 // CHECK:STDOUT:   %pattern_type.cb1: type = pattern_type %empty_tuple.type [concrete]
 // CHECK:STDOUT:   %F.type: type = fn_type @F [concrete]
@@ -403,12 +527,20 @@ fn F[U:! Core.Destroy where .Self impls I(.Self)](u: U) {
 // CHECK:STDOUT:     %return.patt: %pattern_type.cb1 = return_slot_pattern %return.param_patt, %impl.elem0.loc8_39 [concrete]
 // CHECK:STDOUT:   } {
 // CHECK:STDOUT:     %T.ref: %I_where.type = name_ref T, %T.loc8_7.2 [symbolic = %T.loc8_7.1 (constants.%T.706)]
-// CHECK:STDOUT:     %T.as_type: type = facet_access_type %T.ref [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
-// CHECK:STDOUT:     %.loc8_39.1: type = converted %T.ref, %T.as_type [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
+// CHECK:STDOUT:     %T.as_type.loc8_39.1: type = facet_access_type %T.ref [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
+// CHECK:STDOUT:     %.loc8_39.1: type = converted %T.ref, %T.as_type.loc8_39.1 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
 // CHECK:STDOUT:     %.loc8_39.2: %I.assoc_type.c03 = specific_constant @I1.%assoc0, @I.WithSelf(constants.%.Self.binding.as_type.8db, constants.%T.706) [symbolic_self = constants.%assoc0.fe4]
 // CHECK:STDOUT:     %I1.ref.loc8_39: %I.assoc_type.c03 = name_ref I1, %.loc8_39.2 [symbolic_self = constants.%assoc0.fe4]
-// CHECK:STDOUT:     %impl.elem0.loc8_39: type = impl_witness_access constants.%I.lookup_impl_witness.94d, element0 [concrete = constants.%empty_tuple.type]
-// CHECK:STDOUT:     %.loc8_39.3: Core.Form = init_form %impl.elem0.loc8_39 [concrete = constants.%.262]
+// CHECK:STDOUT:     %facet_value.loc8_39.2: %type = facet_value constants.%T.binding.as_type, () [symbolic = %facet_value.loc8_39.1 (constants.%facet_value)]
+// CHECK:STDOUT:     %.loc8_39.3: %type = converted constants.%T.binding.as_type, %facet_value.loc8_39.2 [symbolic = %facet_value.loc8_39.1 (constants.%facet_value)]
+// CHECK:STDOUT:     %T.as_type.loc8_39.2: type = facet_access_type constants.%T.706 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
+// CHECK:STDOUT:     %facet_value.loc8_39.3: %type = facet_value %T.as_type.loc8_39.2, () [symbolic = %facet_value.loc8_39.1 (constants.%facet_value)]
+// CHECK:STDOUT:     %.loc8_39.4: %type = converted constants.%T.706, %facet_value.loc8_39.3 [symbolic = %facet_value.loc8_39.1 (constants.%facet_value)]
+// CHECK:STDOUT:     %T.as_type.loc8_39.3: type = facet_access_type constants.%T.706 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
+// CHECK:STDOUT:     %facet_value.loc8_39.4: %type = facet_value %T.as_type.loc8_39.3, () [symbolic = %facet_value.loc8_39.1 (constants.%facet_value)]
+// CHECK:STDOUT:     %.loc8_39.5: %type = converted constants.%T.706, %facet_value.loc8_39.4 [symbolic = %facet_value.loc8_39.1 (constants.%facet_value)]
+// CHECK:STDOUT:     %impl.elem0.loc8_39: type = impl_witness_access constants.%I.lookup_impl_witness.7f4, element0 [concrete = constants.%empty_tuple.type]
+// CHECK:STDOUT:     %.loc8_39.6: Core.Form = init_form %impl.elem0.loc8_39 [concrete = constants.%.262]
 // CHECK:STDOUT:     %.loc8_19.1: type = splice_block %.loc8_19.2 [symbolic_self = constants.%I_where.type] {
 // CHECK:STDOUT:       <elided>
 // CHECK:STDOUT:       %I.ref: %I.type.609 = name_ref I, file.%I.decl [concrete = constants.%I.generic]
@@ -440,12 +572,15 @@ fn F[U:! Core.Destroy where .Self impls I(.Self)](u: U) {
 // CHECK:STDOUT:     %return.patt: %pattern_type.cb1 = return_slot_pattern %return.param_patt, %impl.elem0.loc12_47 [concrete]
 // CHECK:STDOUT:   } {
 // CHECK:STDOUT:     %T.ref: %I_where.type = name_ref T, %T.loc12_7.2 [symbolic = %T.loc12_7.1 (constants.%T.706)]
-// CHECK:STDOUT:     %T.as_type: type = facet_access_type %T.ref [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
-// CHECK:STDOUT:     %.loc12_47.1: type = converted %T.ref, %T.as_type [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
+// CHECK:STDOUT:     %T.as_type.loc12_47.1: type = facet_access_type %T.ref [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
+// CHECK:STDOUT:     %.loc12_47.1: type = converted %T.ref, %T.as_type.loc12_47.1 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
 // CHECK:STDOUT:     %.loc12_47.2: %I.assoc_type.c03 = specific_constant @I1.%assoc0, @I.WithSelf(constants.%.Self.binding.as_type.8db, constants.%T.706) [symbolic_self = constants.%assoc0.fe4]
 // CHECK:STDOUT:     %I1.ref.loc12_47: %I.assoc_type.c03 = name_ref I1, %.loc12_47.2 [symbolic_self = constants.%assoc0.fe4]
-// CHECK:STDOUT:     %impl.elem0.loc12_47: type = impl_witness_access constants.%I.lookup_impl_witness.94d, element0 [concrete = constants.%empty_tuple.type]
-// CHECK:STDOUT:     %.loc12_47.3: Core.Form = init_form %impl.elem0.loc12_47 [concrete = constants.%.262]
+// CHECK:STDOUT:     %T.as_type.loc12_47.2: type = facet_access_type constants.%T.706 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
+// CHECK:STDOUT:     %facet_value.loc12_47.2: %type = facet_value %T.as_type.loc12_47.2, () [symbolic = %facet_value.loc12_47.1 (constants.%facet_value)]
+// CHECK:STDOUT:     %.loc12_47.3: %type = converted constants.%T.706, %facet_value.loc12_47.2 [symbolic = %facet_value.loc12_47.1 (constants.%facet_value)]
+// CHECK:STDOUT:     %impl.elem0.loc12_47: type = impl_witness_access constants.%I.lookup_impl_witness.7f4, element0 [concrete = constants.%empty_tuple.type]
+// CHECK:STDOUT:     %.loc12_47.4: Core.Form = init_form %impl.elem0.loc12_47 [concrete = constants.%.262]
 // CHECK:STDOUT:     %.loc12_27.1: type = splice_block %.loc12_27.2 [symbolic_self = constants.%I_where.type] {
 // CHECK:STDOUT:       <elided>
 // CHECK:STDOUT:       %I.ref: %I.type.609 = name_ref I, file.%I.decl [concrete = constants.%I.generic]
@@ -502,6 +637,7 @@ fn F[U:! Core.Destroy where .Self impls I(.Self)](u: U) {
 // CHECK:STDOUT: generic fn @F(%T.loc8_7.2: %I_where.type) {
 // CHECK:STDOUT:   %T.loc8_7.1: %I_where.type = symbolic_binding T, 0 [symbolic = %T.loc8_7.1 (constants.%T.706)]
 // CHECK:STDOUT:   %T.binding.as_type: type = symbolic_binding_type T, 0, %T.loc8_7.1 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
+// CHECK:STDOUT:   %facet_value.loc8_39.1: %type = facet_value %T.binding.as_type, () [symbolic = %facet_value.loc8_39.1 (constants.%facet_value)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT:
@@ -517,6 +653,7 @@ fn F[U:! Core.Destroy where .Self impls I(.Self)](u: U) {
 // CHECK:STDOUT: generic fn @G(%T.loc12_7.2: %I_where.type) {
 // CHECK:STDOUT:   %T.loc12_7.1: %I_where.type = symbolic_binding T, 0 [symbolic = %T.loc12_7.1 (constants.%T.706)]
 // CHECK:STDOUT:   %T.binding.as_type: type = symbolic_binding_type T, 0, %T.loc12_7.1 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
+// CHECK:STDOUT:   %facet_value.loc12_47.1: %type = facet_value %T.binding.as_type, () [symbolic = %facet_value.loc12_47.1 (constants.%facet_value)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT:
@@ -564,6 +701,10 @@ fn F[U:! Core.Destroy where .Self impls I(.Self)](u: U) {
 // CHECK:STDOUT:   %assoc0 => constants.%assoc0.fe4
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
+// CHECK:STDOUT: specific @I(constants.%T.binding.as_type) {
+// CHECK:STDOUT:   %T.loc4_14.1 => constants.%T.binding.as_type
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
 // CHECK:STDOUT: specific @I.WithSelf(constants.%.Self.binding.as_type.8db, constants.%I.facet) {
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT:   %T => constants.%.Self.binding.as_type.8db
@@ -574,10 +715,12 @@ fn F[U:! Core.Destroy where .Self impls I(.Self)](u: U) {
 // CHECK:STDOUT: specific @F(constants.%T.706) {
 // CHECK:STDOUT:   %T.loc8_7.1 => constants.%T.706
 // CHECK:STDOUT:   %T.binding.as_type => constants.%T.binding.as_type
+// CHECK:STDOUT:   %facet_value.loc8_39.1 => constants.%facet_value
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @G(constants.%T.706) {
 // CHECK:STDOUT:   %T.loc12_7.1 => constants.%T.706
 // CHECK:STDOUT:   %T.binding.as_type => constants.%T.binding.as_type
+// CHECK:STDOUT:   %facet_value.loc12_47.1 => constants.%facet_value
 // CHECK:STDOUT: }
 // CHECK:STDOUT:

toolchain/check/testdata/facet/self_in_interface_param.carbon

@@ -43,7 +43,8 @@ fn G(_:! I(.Self) where .I1 = ()) {}
 // CHECK:STDOUT:   %pattern_type.033: type = pattern_type %I_where.type [symbolic_self]
 // CHECK:STDOUT:   %T.706: %I_where.type = symbolic_binding T, 0 [symbolic]
 // CHECK:STDOUT:   %T.binding.as_type: type = symbolic_binding_type T, 0, %T.706 [symbolic]
-// CHECK:STDOUT:   %I.lookup_impl_witness.94d: <witness> = lookup_impl_witness %T.706, @I, @I(%.Self.binding.as_type.8db) [symbolic]
+// CHECK:STDOUT:   %facet_value: %type = facet_value %T.binding.as_type, () [symbolic]
+// CHECK:STDOUT:   %I.lookup_impl_witness.7f4: <witness> = lookup_impl_witness %T.706, @I, @I(%T.binding.as_type) [symbolic]
 // CHECK:STDOUT:   %.262: Core.Form = init_form %empty_tuple.type [concrete]
 // CHECK:STDOUT:   %pattern_type.cb1: type = pattern_type %empty_tuple.type [concrete]
 // CHECK:STDOUT:   %F.type: type = fn_type @F [concrete]
@@ -57,12 +58,20 @@ fn G(_:! I(.Self) where .I1 = ()) {}
 // CHECK:STDOUT:     %return.patt: %pattern_type.cb1 = return_slot_pattern %return.param_patt, %impl.elem0.loc18_39 [concrete]
 // CHECK:STDOUT:   } {
 // CHECK:STDOUT:     %T.ref: %I_where.type = name_ref T, %T.loc18_7.2 [symbolic = %T.loc18_7.1 (constants.%T.706)]
-// CHECK:STDOUT:     %T.as_type: type = facet_access_type %T.ref [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
-// CHECK:STDOUT:     %.loc18_39.1: type = converted %T.ref, %T.as_type [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
+// CHECK:STDOUT:     %T.as_type.loc18_39.1: type = facet_access_type %T.ref [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
+// CHECK:STDOUT:     %.loc18_39.1: type = converted %T.ref, %T.as_type.loc18_39.1 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
 // CHECK:STDOUT:     %.loc18_39.2: %I.assoc_type.c03 = specific_constant @I1.%assoc0, @I.WithSelf(constants.%.Self.binding.as_type.8db, constants.%T.706) [symbolic_self = constants.%assoc0.fe4]
 // CHECK:STDOUT:     %I1.ref.loc18_39: %I.assoc_type.c03 = name_ref I1, %.loc18_39.2 [symbolic_self = constants.%assoc0.fe4]
-// CHECK:STDOUT:     %impl.elem0.loc18_39: type = impl_witness_access constants.%I.lookup_impl_witness.94d, element0 [concrete = constants.%empty_tuple.type]
-// CHECK:STDOUT:     %.loc18_39.3: Core.Form = init_form %impl.elem0.loc18_39 [concrete = constants.%.262]
+// CHECK:STDOUT:     %facet_value.loc18_39.2: %type = facet_value constants.%T.binding.as_type, () [symbolic = %facet_value.loc18_39.1 (constants.%facet_value)]
+// CHECK:STDOUT:     %.loc18_39.3: %type = converted constants.%T.binding.as_type, %facet_value.loc18_39.2 [symbolic = %facet_value.loc18_39.1 (constants.%facet_value)]
+// CHECK:STDOUT:     %T.as_type.loc18_39.2: type = facet_access_type constants.%T.706 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
+// CHECK:STDOUT:     %facet_value.loc18_39.3: %type = facet_value %T.as_type.loc18_39.2, () [symbolic = %facet_value.loc18_39.1 (constants.%facet_value)]
+// CHECK:STDOUT:     %.loc18_39.4: %type = converted constants.%T.706, %facet_value.loc18_39.3 [symbolic = %facet_value.loc18_39.1 (constants.%facet_value)]
+// CHECK:STDOUT:     %T.as_type.loc18_39.3: type = facet_access_type constants.%T.706 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
+// CHECK:STDOUT:     %facet_value.loc18_39.4: %type = facet_value %T.as_type.loc18_39.3, () [symbolic = %facet_value.loc18_39.1 (constants.%facet_value)]
+// CHECK:STDOUT:     %.loc18_39.5: %type = converted constants.%T.706, %facet_value.loc18_39.4 [symbolic = %facet_value.loc18_39.1 (constants.%facet_value)]
+// CHECK:STDOUT:     %impl.elem0.loc18_39: type = impl_witness_access constants.%I.lookup_impl_witness.7f4, element0 [concrete = constants.%empty_tuple.type]
+// CHECK:STDOUT:     %.loc18_39.6: Core.Form = init_form %impl.elem0.loc18_39 [concrete = constants.%.262]
 // CHECK:STDOUT:     %.loc18_19.1: type = splice_block %.loc18_19.2 [symbolic_self = constants.%I_where.type] {
 // CHECK:STDOUT:       <elided>
 // CHECK:STDOUT:       %I.ref: %I.type.609 = name_ref I, file.%I.decl [concrete = constants.%I.generic]
@@ -93,6 +102,7 @@ fn G(_:! I(.Self) where .I1 = ()) {}
 // CHECK:STDOUT: generic fn @F(%T.loc18_7.2: %I_where.type) {
 // CHECK:STDOUT:   %T.loc18_7.1: %I_where.type = symbolic_binding T, 0 [symbolic = %T.loc18_7.1 (constants.%T.706)]
 // CHECK:STDOUT:   %T.binding.as_type: type = symbolic_binding_type T, 0, %T.loc18_7.1 [symbolic = %T.binding.as_type (constants.%T.binding.as_type)]
+// CHECK:STDOUT:   %facet_value.loc18_39.1: %type = facet_value %T.binding.as_type, () [symbolic = %facet_value.loc18_39.1 (constants.%facet_value)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT:
@@ -108,5 +118,6 @@ fn G(_:! I(.Self) where .I1 = ()) {}
 // CHECK:STDOUT: specific @F(constants.%T.706) {
 // CHECK:STDOUT:   %T.loc18_7.1 => constants.%T.706
 // CHECK:STDOUT:   %T.binding.as_type => constants.%T.binding.as_type
+// CHECK:STDOUT:   %facet_value.loc18_39.1 => constants.%facet_value
 // CHECK:STDOUT: }
 // CHECK:STDOUT:

toolchain/check/testdata/facet/validate_impl_constraints.carbon

@@ -39,7 +39,7 @@ fn G(T:! I where .Self impls (I where .X = {})) {
   F(T);
 }
 
-// --- fail_todo_where_impls_tests_associated_constant_of_generic_type.carbon
+// --- fail_where_impls_tests_associated_constant_of_generic_type_non_final_impl.carbon
 library "[[@TEST_NAME]]";
 
 class C(U:! type) {}
@@ -55,16 +55,39 @@ 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 C(.Self) impls M and .(M.M0) = {}` [ConversionFailureFacetToFacet]
+  // We have no final impl for `C(T) as M`, so we don't know the value of
+  // `(C(T) as M).M0` concretely, so we don't know that it is `{}` and we can't
+  // convert assuming it is.
+  //
+  // CHECK:STDERR: fail_where_impls_tests_associated_constant_of_generic_type_non_final_impl.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `L` into type implementing `type where C(.Self) impls M and C(.Self).(M.M0) = {}` [ConversionFailureFacetToFacet]
   // CHECK:STDERR:   F(T);
   // CHECK:STDERR:   ^~~~
-  // 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: fail_where_impls_tests_associated_constant_of_generic_type_non_final_impl.carbon:[[@LINE-10]]: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:
   F(T);
 }
 
+// --- where_impls_tests_associated_constant_of_generic_type.carbon
+library "[[@TEST_NAME]]";
+
+class C(U:! type) {}
+
+// C(U) impls M if U impls L.
+interface L {}
+interface M { let M0:! type; }
+final impl forall [U:! L] C(U) as M where .M0 = {} {}
+
+// U requires that C(.Self) impls M.
+// - C(.Self) impls M can be rewritten as C(U) impls M.
+// - C(U) impls M if U impls L => Requires U impls L.
+fn F(unused U:! type where C(.Self) impls (M where .M0 = {})) {}
+
+fn G(T:! L) {
+  F(T);
+}
+
 // --- fail_where_impls_tests_associated_constant_of_generic_type_type_differs.carbon
 library "[[@TEST_NAME]]";
 
@@ -73,7 +96,7 @@ class C(U:! type) {}
 // C(U) impls M if U impls L.
 interface L {}
 interface M { let M0:! type; }
-impl forall [U:! L] C(U) as M where .M0 = () {}
+final impl forall [U:! L] C(U) as M where .M0 = () {}
 
 // U requires that C(.Self) impls M.
 // - C(.Self) impls M can be rewritten as C(U) impls M.
@@ -81,7 +104,7 @@ 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 C(.Self) impls M and .(M.M0) = {}` [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 C(.Self).(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]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
@@ -91,6 +114,81 @@ fn G(T:! L) {
   F(T);
 }
 
+// --- fail_where_impls_tests_associated_constant_of_generic_interface_non_final_impl.carbon
+library "[[@TEST_NAME]]";
+
+class C {}
+
+// C impls M(U) if U impls L.
+interface L {}
+interface M(U:! type) { let M0:! type; }
+impl forall [U:! L] C as M(U) where .M0 = {} {}
+
+// U requires that C impls M(.Self).
+// - C impls M(.Self) can be rewritten as C impls M(U).
+// - C impls M(U) if U impls L => Requires U impls L.
+fn F(unused U:! type where C impls (M(.Self) where .M0 = {})) {}
+
+fn G(T:! L) {
+  // We have no final impl for `C as M(T)`, so we don't know the value of
+  // `(C as M(T)).M0` concretely, so we don't know that it is `{}` and we can't
+  // convert assuming it is.
+  //
+  // CHECK:STDERR: fail_where_impls_tests_associated_constant_of_generic_interface_non_final_impl.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `L` into type implementing `type where C impls M(.Self) and C.(M(.Self).M0) = {}` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(T);
+  // CHECK:STDERR:   ^~~~
+  // CHECK:STDERR: fail_where_impls_tests_associated_constant_of_generic_interface_non_final_impl.carbon:[[@LINE-10]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
+  // CHECK:STDERR: fn F(unused U:! type where C impls (M(.Self) where .M0 = {})) {}
+  // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR:
+  F(T);
+}
+
+// --- where_impls_tests_associated_constant_of_generic_interface.carbon
+library "[[@TEST_NAME]]";
+
+class C {}
+
+// C impls M(U) if U impls L.
+interface L {}
+interface M(U:! type) { let M0:! type; }
+final impl forall [U:! L] C as M(U) where .M0 = {} {}
+
+// U requires that C impls M(.Self).
+// - C impls M(.Self) can be rewritten as C impls M(U).
+// - C impls M(U) if U impls L => Requires U impls L.
+fn F(unused U:! type where C impls (M(.Self) where .M0 = {})) {}
+
+fn G(T:! L) {
+  F(T);
+}
+
+// --- fail_where_impls_tests_associated_constant_of_generic_interface_type_differs.carbon
+library "[[@TEST_NAME]]";
+
+class C {}
+
+// C impls M(U) if U impls L.
+interface L {}
+interface M(U:! type) { let M0:! type; }
+final impl forall [U:! L] C as M(U) where .M0 = () {}
+
+// U requires that C impls M(.Self).
+// - C impls M(.Self) can be rewritten as C impls M(U).
+// - C impls M(U) if U impls L => Requires U impls L.
+fn F(unused U:! type where C impls (M(.Self) where .M0 = {})) {}
+
+fn G(T:! L) {
+  // CHECK:STDERR: fail_where_impls_tests_associated_constant_of_generic_interface_type_differs.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `L` into type implementing `type where C impls M(.Self) and C.(M(.Self).M0) = {}` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(T);
+  // CHECK:STDERR:   ^~~~
+  // CHECK:STDERR: fail_where_impls_tests_associated_constant_of_generic_interface_type_differs.carbon:[[@LINE-6]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
+  // CHECK:STDERR: fn F(unused U:! type where C impls (M(.Self) where .M0 = {})) {}
+  // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR:
+  F(T);
+}
+
 // --- self_in_interface_generic_param_unconstrained.carbon
 library "[[@TEST_NAME]]";
 
@@ -109,12 +207,13 @@ library "[[@TEST_NAME]]";
 interface Z {}
 interface I(T:! Z) {}
 
-// Implied constraint: .Self impls Z, which is satisfied and checked at the end
-// of the fn signature.
+// TODO: I(.Self) introduces an implied constraint `.Self impls Z`, which is
+// satisfied and checked at the end of the fn signature.
+//
 // CHECK:STDERR: fail_todo_self_in_interface_generic_param_constrained.carbon:[[@LINE+7]]:17: error: cannot convert type `.Self` that implements `type` into type implementing `Z` [ConversionFailureFacetToFacet]
 // CHECK:STDERR: fn F(unused T:! I(.Self) where .Self impls Z) {}
 // CHECK:STDERR:                 ^~~~~~~~
-// CHECK:STDERR: fail_todo_self_in_interface_generic_param_constrained.carbon:[[@LINE-7]]:13: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+// CHECK:STDERR: fail_todo_self_in_interface_generic_param_constrained.carbon:[[@LINE-8]]:13: note: initializing generic parameter `T` declared here [InitializingGenericParam]
 // CHECK:STDERR: interface I(T:! Z) {}
 // CHECK:STDERR:             ^~~~~
 // CHECK:STDERR:
@@ -123,7 +222,7 @@ fn F(unused T:! I(.Self) where .Self impls Z) {}
 // CHECK:STDERR: fail_todo_self_in_interface_generic_param_constrained.carbon:[[@LINE+7]]:14: error: cannot convert type `.Self` that implements `type` into type implementing `Z` [ConversionFailureFacetToFacet]
 // CHECK:STDERR: fn G(T:! Z & I(.Self)) {
 // CHECK:STDERR:              ^~~~~~~~
-// CHECK:STDERR: fail_todo_self_in_interface_generic_param_constrained.carbon:[[@LINE-16]]:13: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+// CHECK:STDERR: fail_todo_self_in_interface_generic_param_constrained.carbon:[[@LINE-17]]:13: note: initializing generic parameter `T` declared here [InitializingGenericParam]
 // CHECK:STDERR: interface I(T:! Z) {}
 // CHECK:STDERR:             ^~~~~
 // CHECK:STDERR:
@@ -131,7 +230,7 @@ fn G(T:! Z & I(.Self)) {
   F(T);
 }
 
-// --- fail_todo_where_period_self_rhs_sees_lhs.carbon
+// --- where_period_self_rhs_sees_lhs.carbon
 library "[[@TEST_NAME]]";
 
 interface Z {}
@@ -150,17 +249,10 @@ fn G() {
   impl C as Z {}
   impl C as Y {}
   impl C as X(C) {}
-  // CHECK:STDERR: fail_todo_where_period_self_rhs_sees_lhs.carbon:[[@LINE+7]]:3: error: cannot convert type `C` into type implementing `Z & N where .Self impls X(.Self as Z & Y)` [ConversionFailureTypeToFacet]
-  // CHECK:STDERR:   F(C);
-  // CHECK:STDERR:   ^~~~
-  // CHECK:STDERR: fail_todo_where_period_self_rhs_sees_lhs.carbon:[[@LINE-10]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
-  // CHECK:STDERR: fn F(_:! Z & N where .Self impls X(.Self)) {}
-  // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-  // CHECK:STDERR:
   F(C);
 }
 
-// --- fail_todo_where_type_rhs_sees_lhs.carbon
+// --- where_type_rhs_sees_lhs.carbon
 library "[[@TEST_NAME]]";
 
 interface Z {}
@@ -181,12 +273,125 @@ fn G() {
   impl C as Z {}
   impl C as Y {}
   impl R(C) as X(C) {}
-  // CHECK:STDERR: fail_todo_where_type_rhs_sees_lhs.carbon:[[@LINE+7]]:3: error: cannot convert type `C` into type implementing `Z & N where R(.Self as Z & Y) impls X(.Self as Z & Y)` [ConversionFailureTypeToFacet]
+  F(C);
+}
+
+// --- fail_todo_where_period_self_rhs_impls_nested_period_self.carbon
+library "[[@TEST_NAME]]";
+
+interface Z {}
+interface Y {}
+interface X(T:! Z & Y) {}
+
+constraint N {
+  require impls Y;
+}
+
+// TODO: The inner nested facet type (`N where...`) does not know about
+// constraints on the outer facet type (`Z where...`). But it should produce an
+// implied constraint that `.Self impls Z & Y` that is checked once the full
+// facet type is known.
+//
+// CHECK:STDERR: fail_todo_where_period_self_rhs_impls_nested_period_self.carbon:[[@LINE+7]]:51: error: cannot convert type `.Self` that implements `N` into type implementing `Z & Y` [ConversionFailureFacetToFacet]
+// CHECK:STDERR: fn F(_:! Z where .Self impls (N where .Self impls X(.Self))) {}
+// CHECK:STDERR:                                                   ^~~~~~~~
+// CHECK:STDERR: fail_todo_where_period_self_rhs_impls_nested_period_self.carbon:[[@LINE-14]]:13: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+// CHECK:STDERR: interface X(T:! Z & Y) {}
+// CHECK:STDERR:             ^~~~~~~~~
+// CHECK:STDERR:
+fn F(_:! Z where .Self impls (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);
+}
+
+// --- associated_const_impls_interface_with_period_self.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let I1:! type;
+}
+
+interface J(T:! I) {}
+
+// There is a .Self reference on the LHS and RHS of the `impls` constraint,
+// which must be replaced, each with `C as I`
+fn F(_:! I where .I1 impls J(.Self)) {}
+
+fn G() {
+  class C;
+  class D;
+
+  impl C as I where .I1 = D {}
+  impl D as J(C) {}
+
+  F(C);
+}
+
+// --- fail_concrete_witness_without_impl.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let I1:! type;
+}
+interface J {}
+
+fn F(_:! I where .I1 impls J) {}
+
+fn G() {
+  class C;
+
+  // This identifies `C as (I where .I1 impls J)`, which replaces `.Self.I1`
+  // with `C.(I.I1)`. This is a concrete lookup since C and I are both concrete,
+  // but it doesn't find anything as there is no impl.
+  //
+  // This tests that we correctly handle the case where the witness in an
+  // ImplWitnessAccess would become concrete without being able to provide any
+  // value, since it's still a `LookupImplWitness` type of witness.
+
+  // CHECK:STDERR: fail_concrete_witness_without_impl.carbon:[[@LINE+7]]:3: error: cannot convert type `C` into type implementing `I where .(I.I1) impls J` [ConversionFailureTypeToFacet]
   // CHECK:STDERR:   F(C);
   // CHECK:STDERR:   ^~~~
-  // CHECK:STDERR: fail_todo_where_type_rhs_sees_lhs.carbon:[[@LINE-10]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
-  // CHECK:STDERR: fn F(_:! Z & N where R(.Self) impls X(.Self)) {}
-  // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR: fail_concrete_witness_without_impl.carbon:[[@LINE-16]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
+  // CHECK:STDERR: fn F(_:! I where .I1 impls J) {}
+  // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   // CHECK:STDERR:
   F(C);
 }
+
+// --- fail_todo_convert_to_period_self_preserves_self_facet_impls.carbon
+library "[[@TEST_NAME]]";
+
+interface K {}
+interface J {}
+interface I {
+  let I1:! type;
+}
+
+fn F(unused U:! I & J where .I1 impls K) {}
+
+impl forall [T:! type] T as J {}
+
+fn G(T:! I where .I1 impls K) {
+  // Replaces `.Self` with `T`, which converts `T` to `I & J`. Doing so has to
+  // invent a witness for `J`, and this tests we do so without losing the
+  // information that `.I1 impls K`.
+  //
+  // TODO: When converting T to the type of U, the identified facet type
+  // includes `.Self.I1 impls K`, which is replaced with `T.I1 impls K`. The
+  // identified facet type of `T` also contains `T.I1 impls K` so we should find
+  // a witness for that.
+  //
+  // CHECK:STDERR: fail_todo_convert_to_period_self_preserves_self_facet_impls.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `I where .(I.I1) impls K` into type implementing `J & I where .(I.I1) impls K` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(T);
+  // CHECK:STDERR:   ^~~~
+  // CHECK:STDERR: fail_todo_convert_to_period_self_preserves_self_facet_impls.carbon:[[@LINE-17]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
+  // CHECK:STDERR: fn F(unused U:! I & J where .I1 impls K) {}
+  // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR:
+  F(T);
+}

toolchain/check/testdata/facet/validate_rewrite_constraints.carbon

@@ -1009,6 +1009,52 @@ fn G1() {
   }
 }
 
+// --- rewrite_rhs_satisfies_lhs_requirement.carbon
+library "[[@TEST_NAME]]";
+
+interface I(T:! type) {}
+interface J(T:! type) {
+  let J1:! I(T);
+}
+
+class C;
+constraint L {
+  // J(.Self).J1 requires that its RHS impls I(.Self), which is provided for
+  // here.
+  //
+  // We look for this witness in `L` because the assignment is to `J(.Self).J1`
+  // so we look in the facet type of `.Self` which is `L & J(.Self)`.
+  require C impls I(Self);
+}
+
+fn F(unused T:! L & J(.Self) where .J1 = C) {}
+
+fn G(T:! L & J(.Self) where .J1 = C) {
+  F(T);
+}
+
+// --- todo_fail_rewrite_rhs_does_not_satisfy_lhs_requirement.carbon
+library "[[@TEST_NAME]]";
+
+interface I(T:! type) {}
+interface J(T:! type) {
+  let J1:! I(T);
+}
+
+class C;
+constraint L {
+  // Without this, C does not impl I(T), which is required by J(T).J1.
+  // require C impls I(Self);
+}
+
+// TODO: This should be an error that C does not impl I(.Self). We don't yet try
+// convert the RHS of a rewrite to the type of the LHS when the LHS is symbolic.
+fn F(unused T:! L & J(.Self) where .J1 = C) {}
+
+fn G(T:! L & J(.Self) where .J1 = C) {
+  F(T);
+}
+
 // --- rewrite_requires_subst_in_nested_access_of_self.carbon
 library "[[@TEST_NAME]]";
 
@@ -1085,7 +1131,7 @@ fn G3(T:! I & J & K where .K1 = .Self and .J1 = .Self and .I2 = {}) {
   F(T);
 }
 
-// --- fail_todo_rewrite_requires_subst_in_nested_access_of_other.carbon
+// --- rewrite_requires_subst_in_nested_access_of_other.carbon
 library "[[@TEST_NAME]]";
 
 interface I {
@@ -1107,13 +1153,6 @@ interface K {
 fn F(unused U:! I, unused T:! J & K where .J2 = (.K1.J1).I1) {}
 
 fn G(U:! I where .I1 = (), T:! J & K where .K1 = .Self and .J1 = U and .J2 = ()) {
-  // CHECK:STDERR: fail_todo_rewrite_requires_subst_in_nested_access_of_other.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `J & K where .(J.J2) = () and .(K.K1) = .Self as J and .(J.J1) = U as I` into type implementing `J & K where .(J.J2) = .(K.K1).(J.J1).(I.I1)` [ConversionFailureFacetToFacet]
-  // CHECK:STDERR:   F(U, T);
-  // CHECK:STDERR:   ^~~~~~~
-  // CHECK:STDERR: fail_todo_rewrite_requires_subst_in_nested_access_of_other.carbon:[[@LINE-6]]:27: note: initializing generic parameter `T` declared here [InitializingGenericParam]
-  // CHECK:STDERR: fn F(unused U:! I, unused T:! J & K where .J2 = (.K1.J1).I1) {}
-  // CHECK:STDERR:                           ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-  // CHECK:STDERR:
   F(U, T);
 }
 
@@ -1309,3 +1348,68 @@ fn F(T:! I where .X = (I where .Y = {}), unused U:! T.X) {}
 fn G(T:! I where .X = (I where .Y = {}), U:! I where .Y = {}) {
   F(T, U);
 }
+
+// --- period_self_in_rewrite_values.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let I1:! type;
+  let I2:! type;
+  let I3:! type;
+  let I4:! type;
+}
+
+class E(T:! type) {}
+
+// * The LHS of `.I1` contains a `.Self` which is replaced by `C` to form
+//   `C.(I.I1)` and resolves to `()`.
+// * The RHS of `.I1` is `()` which then compares equal.
+fn F1(_:! I where .I1 = ()) {}
+
+// * The LHS of `.I2` contains a `.Self` which is replaced by `C` to form
+//   `C.(I.I1)` and resolves to `C`.
+// * The RHS of `.I2` is `.Self` which is replaced by `C` and then compares
+//   equal.
+fn F2(_:! I where .I2 = .Self) {}
+
+// * The LHS of `.I3` contains a `.Self` which is replaced by `C` to form
+//   `C.(I.I1)` and resolves to `E(C)`.
+// * The RHS of `.I3` contains a `.Self` which is replaced by `C` to form
+//   `E(C)`, and then compares equal.
+fn F3(_:! I where .I3 = E(.Self)) {}
+
+// * The LHS of `.I4` contains a `.Self` which is replaced by `C` to form
+//   `C.(I.I4)` and resolves to `.Self`. That `.Self` then is replaced by `C` so
+//   the LHS untimately resolves to `C`.
+// * The RHS of `.I4` is `.Self` which is replaced by `C` and then compares
+//   equal.
+fn F4(_:! I where .I4 = .Self) {}
+
+fn G() {
+  class C;
+  impl C as I where .I1 = () and .I2 = C and .I3 = E(C) and .I4 = .Self {}
+
+  F1(C);
+  F2(C);
+  F3(C);
+  F4(C);
+}
+
+// --- convert_to_period_self_preserves_self_facet_rewrite.carbon
+library "[[@TEST_NAME]]";
+
+interface J {}
+interface I {
+  let I1:! type;
+}
+
+fn F(unused U:! I & J where .I1 = {}) {}
+
+impl forall [T:! type] T as J {}
+
+fn G(T:! I where .I1 = {}) {
+  // Replaces `.Self` with `T`, which converts `T` to `I & J`. Doing so has to
+  // invent a witness for `J`, and this tests we do so without losing the
+  // information that `.I1 = {}`.
+  F(T);
+}

toolchain/check/testdata/impl/lookup/lookup_interface_with_enclosing_generic_inside_rewrite_constraint.carbon

@@ -449,7 +449,7 @@ fn F() {
 // CHECK:STDOUT:   %C.521: type = class_type @C, @C(%OuterParam) [symbolic]
 // CHECK:STDOUT:   %Y.impl_witness.26b: <witness> = impl_witness @C.as.Y.impl.%Y.impl_witness_table, @C.as.Y.impl(%OuterParam) [symbolic]
 // CHECK:STDOUT:   %require_complete.4a2: <witness> = require_complete_type %Y_where.type.b0f [symbolic]
-// CHECK:STDOUT:   %Y.facet: %Y.type.6ae = facet_value %C.521, (%Y.impl_witness.26b) [symbolic]
+// CHECK:STDOUT:   %Y.facet.892: %Y.type.6ae = facet_value %C.521, (%Y.impl_witness.26b) [symbolic]
 // CHECK:STDOUT:   %empty_struct_type: type = struct_type {} [concrete]
 // CHECK:STDOUT:   %complete_type.357: <witness> = complete_type_witness %empty_struct_type [concrete]
 // CHECK:STDOUT:   %Z1.impl_witness: <witness> = impl_witness @empty_tuple.type.as.Z1.impl.%Z1.impl_witness_table [concrete]
@@ -829,7 +829,7 @@ fn F() {
 // CHECK:STDOUT:   %Y.impl_witness.loc14_29.2 => constants.%Y.impl_witness.26b
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @Y.WithSelf(constants.%OuterParam, constants.%Y.facet) {
+// CHECK:STDOUT: specific @Y.WithSelf(constants.%OuterParam, constants.%Y.facet.892) {
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT:   %OuterParam => constants.%OuterParam
 // CHECK:STDOUT:   %Y.assoc_type => constants.%Y.assoc_type.aab

toolchain/check/testdata/named_constraint/require.carbon

@@ -554,6 +554,24 @@ fn F() {
   () as N;
 }
 
+// --- require_with_rewrite_constraint_period_self.carbon
+library "[[@TEST_NAME]]";
+
+interface Z(T:! type) {
+  let X:! type;
+}
+
+constraint N(T:! type) {
+  require T impls Z(Self) where .X = .Self;
+}
+
+// Will satisfy `() as N({})`.
+impl {} as Z(()) where .X = {} {}
+
+fn F() {
+  () as N({});
+}
+
 // --- todo_fail_require_with_mismatching_rewrite_constraint.carbon
 library "[[@TEST_NAME]]";
 
@@ -575,6 +593,112 @@ fn F() {
   () as N;
 }
 
+// --- todo_fail_require_with_mismatching_rewrite_constraint_period_self.carbon
+library "[[@TEST_NAME]]";
+
+interface Z(T:! type) {
+  let X:! type;
+}
+
+constraint N(T:! type) {
+  require T impls Z(Self) where .X = .Self;
+}
+
+// Will not satisfy `() as N({})` as the rewrite does not match.
+impl {} as Z(()) where .X = () {}
+
+fn F() {
+  // TODO: Should fail, but we're currently checking the requirements of `N`
+  // rather than of the identified facet type of `N` (which would include the
+  // require decl's requirements).
+  () as N({});
+}
+
+// --- fail_require_with_period_self_impls_not_satisfied.carbon
+library "[[@TEST_NAME]]";
+
+interface Z {}
+interface Y(T:! type) {}
+
+class C(T:! type);
+
+constraint N {
+  require impls Z where .Self impls Y(.Self);
+}
+
+fn F(_:! N) {}
+
+fn G(T:! Z) {
+  // CHECK:STDERR: fail_require_with_period_self_impls_not_satisfied.carbon:[[@LINE+4]]:3: error: cannot convert type `T` that implements `Z` into type implementing `N` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   T as N;
+  // CHECK:STDERR:   ^~~~~~
+  // CHECK:STDERR:
+  T as N;
+}
+
+// --- require_with_period_self_impls.carbon
+library "[[@TEST_NAME]]";
+
+interface Z {}
+interface Y(T:! type) {}
+
+class C(T:! type);
+
+//@dump-sem-ir-begin
+constraint N {
+  require impls Z where .Self impls Y(.Self);
+}
+//@dump-sem-ir-end
+
+fn F(_:! N) {}
+
+fn G(T:! Z & Y(.Self)) {
+  T as N;
+}
+
+// --- fail_require_with_specific_period_self_not_satisfied.carbon
+library "[[@TEST_NAME]]";
+
+interface Z {}
+interface Y(T:! type) {}
+
+class C(T:! type);
+
+constraint N {
+  require impls Z where C(.Self) impls Y(.Self);
+}
+
+fn F(_:! N) {}
+
+fn G(T:! Z) {
+  // CHECK:STDERR: fail_require_with_specific_period_self_not_satisfied.carbon:[[@LINE+4]]:3: error: cannot convert type `T` that implements `Z` into type implementing `N` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   T as N;
+  // CHECK:STDERR:   ^~~~~~
+  // CHECK:STDERR:
+  T as N;
+}
+
+// --- require_with_specific_period_self.carbon
+library "[[@TEST_NAME]]";
+
+interface Z {}
+interface Y(T:! type) {}
+
+class C(T:! type);
+
+//@dump-sem-ir-begin
+constraint N {
+  require impls Z where C(.Self) impls Y(.Self);
+}
+//@dump-sem-ir-end
+
+fn F(_:! N) {}
+
+fn G(T:! Z) {
+  impl C(T) as Y(T) {}
+  T as N;
+}
+
 // CHECK:STDOUT: --- extend.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
@@ -1245,3 +1369,195 @@ fn F() {
 // CHECK:STDOUT:   %Y_where.type => constants.%Y_where.type
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
+// CHECK:STDOUT: --- require_with_period_self_impls.carbon
+// CHECK:STDOUT:
+// CHECK:STDOUT: constants {
+// CHECK:STDOUT:   %Z.type: type = facet_type <@Z> [concrete]
+// CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
+// CHECK:STDOUT:   %.Self.c39: %type = symbolic_binding .Self [symbolic_self]
+// CHECK:STDOUT:   %Y.type.82b: type = generic_interface_type @Y [concrete]
+// CHECK:STDOUT:   %Y.generic: %Y.type.82b = struct_value () [concrete]
+// CHECK:STDOUT:   %N.type: type = facet_type <@N> [concrete]
+// CHECK:STDOUT:   %Self.550: %N.type = symbolic_binding Self, 0 [symbolic]
+// CHECK:STDOUT:   %Self.binding.as_type.5cb: type = symbolic_binding_type Self, 0, %Self.550 [symbolic]
+// CHECK:STDOUT:   %.Self.aac: %Z.type = symbolic_binding .Self [symbolic_self]
+// CHECK:STDOUT:   %.Self.binding.as_type.5a0: type = symbolic_binding_type .Self, %.Self.aac [symbolic_self]
+// CHECK:STDOUT:   %Y.type.dfc: type = facet_type <@Y, @Y(%.Self.binding.as_type.5a0)> [symbolic_self]
+// CHECK:STDOUT:   %Z_where.type.455: type = facet_type <@Z where .Self impls @Y, @Y(%.Self.binding.as_type.5a0)> [symbolic_self]
+// CHECK:STDOUT:   %Z_where.type.820: type = facet_type <@Z where .Self impls @Y, @Y(%Self.binding.as_type.5cb)> [symbolic]
+// CHECK:STDOUT:   %.Self.binding.as_type.8db: type = symbolic_binding_type .Self, %.Self.c39 [symbolic_self]
+// CHECK:STDOUT:   %facet_type: type = facet_type <@Z & @Y, @Y(%.Self.binding.as_type.8db)> [symbolic_self]
+// CHECK:STDOUT:   %T.e40: %facet_type = symbolic_binding T, 0 [symbolic]
+// CHECK:STDOUT:   %T.binding.as_type: type = symbolic_binding_type T, 0, %T.e40 [symbolic]
+// CHECK:STDOUT:   %Z_where.type.c36: type = facet_type <@Z where .Self impls @Y, @Y(%T.binding.as_type)> [symbolic]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: file {
+// CHECK:STDOUT:   %N.decl: type = constraint_decl @N [concrete = constants.%N.type] {} {}
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: constraint @N {
+// CHECK:STDOUT:   %Self: %N.type = symbolic_binding Self, 0 [symbolic = constants.%Self.550]
+// CHECK:STDOUT:   %N.WithSelf.decl = constraint_with_self_decl @N [concrete]
+// CHECK:STDOUT:
+// CHECK:STDOUT: !with Self:
+// CHECK:STDOUT:   %N.WithSelf.Self.binding.as_type.impls.Z_where.type.require.decl = require_decl @N.WithSelf.Self.binding.as_type.impls.Z_where.type.require [concrete] {
+// CHECK:STDOUT:     require %Self.as_type impls %Z_where.type.loc10_19.1
+// CHECK:STDOUT:   } {
+// CHECK:STDOUT:     %Self.as_type: type = facet_access_type @N.%Self [symbolic = %Self.binding.as_type (constants.%Self.binding.as_type.5cb)]
+// CHECK:STDOUT:     %Z.ref: type = name_ref Z, file.%Z.decl [concrete = constants.%Z.type]
+// CHECK:STDOUT:     <elided>
+// CHECK:STDOUT:     %.Self.ref.loc10_25: %Z.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self.aac]
+// CHECK:STDOUT:     %Y.ref: %Y.type.82b = name_ref Y, file.%Y.decl [concrete = constants.%Y.generic]
+// CHECK:STDOUT:     %.Self.ref.loc10_39: %Z.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self.aac]
+// CHECK:STDOUT:     %.Self.as_type.loc10_44: type = facet_access_type %.Self.ref.loc10_39 [symbolic_self = constants.%.Self.binding.as_type.5a0]
+// CHECK:STDOUT:     %.loc10_44: type = converted %.Self.ref.loc10_39, %.Self.as_type.loc10_44 [symbolic_self = constants.%.Self.binding.as_type.5a0]
+// CHECK:STDOUT:     %Y.type: type = facet_type <@Y, @Y(constants.%.Self.binding.as_type.5a0)> [symbolic_self = constants.%Y.type.dfc]
+// CHECK:STDOUT:     %.Self.as_type.loc10_25: type = facet_access_type %.Self.ref.loc10_25 [symbolic_self = constants.%.Self.binding.as_type.5a0]
+// CHECK:STDOUT:     %.loc10_25: type = converted %.Self.ref.loc10_25, %.Self.as_type.loc10_25 [symbolic_self = constants.%.Self.binding.as_type.5a0]
+// CHECK:STDOUT:     %.loc10_19: type = where_expr %.Self [symbolic_self = constants.%Z_where.type.455] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%Z.type
+// CHECK:STDOUT:       requirement_impls %.loc10_25, %Y.type
+// CHECK:STDOUT:     }
+// CHECK:STDOUT:     %Z_where.type.loc10_19.1: type = facet_type <@Z where .Self impls @Y, @Y(constants.%Self.binding.as_type.5cb)> [symbolic = %Z_where.type.loc10_19.2 (constants.%Z_where.type.820)]
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = %Self
+// CHECK:STDOUT:   .Z = <poisoned>
+// CHECK:STDOUT:   .Y = <poisoned>
+// CHECK:STDOUT:   .Z = <poisoned>
+// CHECK:STDOUT:   .Y = <poisoned>
+// CHECK:STDOUT:
+// CHECK:STDOUT: !requires:
+// CHECK:STDOUT:   @N.WithSelf.Self.binding.as_type.impls.Z_where.type.require {
+// CHECK:STDOUT:     require @N.WithSelf.Self.binding.as_type.impls.Z_where.type.require.%Self.as_type impls @N.WithSelf.Self.binding.as_type.impls.Z_where.type.require.%Z_where.type.loc10_19.1
+// CHECK:STDOUT:   }
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: generic require @N.WithSelf.Self.binding.as_type.impls.Z_where.type.require(@N.%Self: %N.type) {
+// CHECK:STDOUT:   %Self: %N.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.5cb)]
+// CHECK:STDOUT:   %Z_where.type.loc10_19.2: type = facet_type <@Z where .Self impls @Y, @Y(%Self.binding.as_type)> [symbolic = %Z_where.type.loc10_19.2 (constants.%Z_where.type.820)]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @N.WithSelf(constants.%Self.550) {
+// CHECK:STDOUT: !definition:
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @N.WithSelf.Self.binding.as_type.impls.Z_where.type.require(constants.%Self.550) {
+// CHECK:STDOUT:   %Self => constants.%Self.550
+// CHECK:STDOUT:   %Self.binding.as_type => constants.%Self.binding.as_type.5cb
+// CHECK:STDOUT:   %Z_where.type.loc10_19.2 => constants.%Z_where.type.820
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @N.WithSelf(constants.%T.e40) {
+// CHECK:STDOUT: !definition:
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @N.WithSelf.Self.binding.as_type.impls.Z_where.type.require(constants.%T.e40) {
+// CHECK:STDOUT:   %Self => constants.%T.e40
+// CHECK:STDOUT:   %Self.binding.as_type => constants.%T.binding.as_type
+// CHECK:STDOUT:   %Z_where.type.loc10_19.2 => constants.%Z_where.type.c36
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: --- require_with_specific_period_self.carbon
+// CHECK:STDOUT:
+// CHECK:STDOUT: constants {
+// CHECK:STDOUT:   %Z.type: type = facet_type <@Z> [concrete]
+// CHECK:STDOUT:   %Y.type.82b: type = generic_interface_type @Y [concrete]
+// CHECK:STDOUT:   %Y.generic: %Y.type.82b = struct_value () [concrete]
+// CHECK:STDOUT:   %C.type: type = generic_class_type @C [concrete]
+// CHECK:STDOUT:   %C.generic: %C.type = struct_value () [concrete]
+// CHECK:STDOUT:   %N.type: type = facet_type <@N> [concrete]
+// CHECK:STDOUT:   %Self.550: %N.type = symbolic_binding Self, 0 [symbolic]
+// CHECK:STDOUT:   %Self.binding.as_type: type = symbolic_binding_type Self, 0, %Self.550 [symbolic]
+// CHECK:STDOUT:   %.Self.aac: %Z.type = symbolic_binding .Self [symbolic_self]
+// CHECK:STDOUT:   %.Self.binding.as_type: type = symbolic_binding_type .Self, %.Self.aac [symbolic_self]
+// CHECK:STDOUT:   %C.646: type = class_type @C, @C(%.Self.binding.as_type) [symbolic_self]
+// CHECK:STDOUT:   %Y.type.dfc: type = facet_type <@Y, @Y(%.Self.binding.as_type)> [symbolic_self]
+// CHECK:STDOUT:   %Z_where.type.a6d533.1: type = facet_type <@Z where %C.646 impls @Y, @Y(%.Self.binding.as_type)> [symbolic_self]
+// CHECK:STDOUT:   %C.237: type = class_type @C, @C(%Self.binding.as_type) [symbolic]
+// CHECK:STDOUT:   %Z_where.type.a6d533.2: type = facet_type <@Z where %C.237 impls @Y, @Y(%Self.binding.as_type)> [symbolic]
+// CHECK:STDOUT:   %T.ea3: %Z.type = symbolic_binding T, 0 [symbolic]
+// CHECK:STDOUT:   %T.binding.as_type: type = symbolic_binding_type T, 0, %T.ea3 [symbolic]
+// CHECK:STDOUT:   %C.3e1: type = class_type @C, @C(%T.binding.as_type) [symbolic]
+// CHECK:STDOUT:   %Z_where.type.a6d533.3: type = facet_type <@Z where %C.3e1 impls @Y, @Y(%T.binding.as_type)> [symbolic]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: file {
+// CHECK:STDOUT:   %N.decl: type = constraint_decl @N [concrete = constants.%N.type] {} {}
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: constraint @N {
+// CHECK:STDOUT:   %Self: %N.type = symbolic_binding Self, 0 [symbolic = constants.%Self.550]
+// CHECK:STDOUT:   %N.WithSelf.decl = constraint_with_self_decl @N [concrete]
+// CHECK:STDOUT:
+// CHECK:STDOUT: !with Self:
+// CHECK:STDOUT:   %N.WithSelf.Self.binding.as_type.impls.Z_where.type.require.decl = require_decl @N.WithSelf.Self.binding.as_type.impls.Z_where.type.require [concrete] {
+// CHECK:STDOUT:     require %Self.as_type impls %Z_where.type.loc10_19.1
+// CHECK:STDOUT:   } {
+// CHECK:STDOUT:     %Self.as_type: type = facet_access_type @N.%Self [symbolic = %Self.binding.as_type (constants.%Self.binding.as_type)]
+// CHECK:STDOUT:     %Z.ref: type = name_ref Z, file.%Z.decl [concrete = constants.%Z.type]
+// CHECK:STDOUT:     <elided>
+// CHECK:STDOUT:     %C.ref: %C.type = name_ref C, file.%C.decl [concrete = constants.%C.generic]
+// CHECK:STDOUT:     %.Self.ref.loc10_27: %Z.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self.aac]
+// CHECK:STDOUT:     %.Self.as_type.loc10_32: type = facet_access_type %.Self.ref.loc10_27 [symbolic_self = constants.%.Self.binding.as_type]
+// CHECK:STDOUT:     %.loc10_32: type = converted %.Self.ref.loc10_27, %.Self.as_type.loc10_32 [symbolic_self = constants.%.Self.binding.as_type]
+// CHECK:STDOUT:     %C.loc10_32: type = class_type @C, @C(constants.%.Self.binding.as_type) [symbolic_self = constants.%C.646]
+// CHECK:STDOUT:     %Y.ref: %Y.type.82b = name_ref Y, file.%Y.decl [concrete = constants.%Y.generic]
+// CHECK:STDOUT:     %.Self.ref.loc10_42: %Z.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self.aac]
+// CHECK:STDOUT:     %.Self.as_type.loc10_47: type = facet_access_type %.Self.ref.loc10_42 [symbolic_self = constants.%.Self.binding.as_type]
+// CHECK:STDOUT:     %.loc10_47: type = converted %.Self.ref.loc10_42, %.Self.as_type.loc10_47 [symbolic_self = constants.%.Self.binding.as_type]
+// CHECK:STDOUT:     %Y.type: type = facet_type <@Y, @Y(constants.%.Self.binding.as_type)> [symbolic_self = constants.%Y.type.dfc]
+// CHECK:STDOUT:     %.loc10_19: type = where_expr %.Self [symbolic_self = constants.%Z_where.type.a6d533.1] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%Z.type
+// CHECK:STDOUT:       requirement_impls %C.loc10_32, %Y.type
+// CHECK:STDOUT:     }
+// CHECK:STDOUT:     %Z_where.type.loc10_19.1: type = facet_type <@Z where constants.%C.237 impls @Y, @Y(constants.%Self.binding.as_type)> [symbolic = %Z_where.type.loc10_19.2 (constants.%Z_where.type.a6d533.2)]
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = %Self
+// CHECK:STDOUT:   .Z = <poisoned>
+// CHECK:STDOUT:   .C = <poisoned>
+// CHECK:STDOUT:   .Y = <poisoned>
+// CHECK:STDOUT:   .Z = <poisoned>
+// CHECK:STDOUT:   .C = <poisoned>
+// CHECK:STDOUT:   .Y = <poisoned>
+// CHECK:STDOUT:
+// CHECK:STDOUT: !requires:
+// CHECK:STDOUT:   @N.WithSelf.Self.binding.as_type.impls.Z_where.type.require {
+// CHECK:STDOUT:     require @N.WithSelf.Self.binding.as_type.impls.Z_where.type.require.%Self.as_type impls @N.WithSelf.Self.binding.as_type.impls.Z_where.type.require.%Z_where.type.loc10_19.1
+// CHECK:STDOUT:   }
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: generic require @N.WithSelf.Self.binding.as_type.impls.Z_where.type.require(@N.%Self: %N.type) {
+// CHECK:STDOUT:   %Self: %N.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:   %C.loc10_19: type = class_type @C, @C(%Self.binding.as_type) [symbolic = %C.loc10_19 (constants.%C.237)]
+// CHECK:STDOUT:   %Z_where.type.loc10_19.2: type = facet_type <@Z where %C.loc10_19 impls @Y, @Y(%Self.binding.as_type)> [symbolic = %Z_where.type.loc10_19.2 (constants.%Z_where.type.a6d533.2)]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @N.WithSelf(constants.%Self.550) {
+// CHECK:STDOUT: !definition:
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @N.WithSelf.Self.binding.as_type.impls.Z_where.type.require(constants.%Self.550) {
+// CHECK:STDOUT:   %Self => constants.%Self.550
+// CHECK:STDOUT:   %Self.binding.as_type => constants.%Self.binding.as_type
+// CHECK:STDOUT:   %C.loc10_19 => constants.%C.237
+// CHECK:STDOUT:   %Z_where.type.loc10_19.2 => constants.%Z_where.type.a6d533.2
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @N.WithSelf(constants.%T.ea3) {
+// CHECK:STDOUT: !definition:
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @N.WithSelf.Self.binding.as_type.impls.Z_where.type.require(constants.%T.ea3) {
+// CHECK:STDOUT:   %Self => constants.%T.ea3
+// CHECK:STDOUT:   %Self.binding.as_type => constants.%T.binding.as_type
+// CHECK:STDOUT:   %C.loc10_19 => constants.%C.3e1
+// CHECK:STDOUT:   %Z_where.type.loc10_19.2 => constants.%Z_where.type.a6d533.3
+// CHECK:STDOUT: }
+// CHECK:STDOUT:

toolchain/check/type_completion.cpp

@@ -962,7 +962,7 @@ static auto GetSelfFacetValue(Context& context, SemIR::ConstantId self_const_id)
 }
 
 static auto IdentifyFacetType(Context& context, SemIR::LocId loc_id,
-                              SemIR::ConstantId self_const_id,
+                              SemIR::ConstantId initial_self_const_id,
                               const SemIR::FacetType& facet_type,
                               bool allow_partially_identified, bool diagnose)
     -> SemIR::IdentifiedFacetTypeId {
@@ -975,7 +975,7 @@ static auto IdentifyFacetType(Context& context, SemIR::LocId loc_id,
   // constant values into specifics).
   auto key =
       SemIR::IdentifiedFacetTypeKey{.facet_type_id = facet_type.facet_type_id,
-                                    .self_const_id = self_const_id};
+                                    .self_const_id = initial_self_const_id};
   if (auto identified_id = context.identified_facet_types().Lookup(key);
       identified_id.has_value()) {
     return identified_id;
@@ -989,13 +989,16 @@ static auto IdentifyFacetType(Context& context, SemIR::LocId loc_id,
 
   // Work queue.
   llvm::SmallVector<SelfImplsFacetType> work = {
-      {true, self_const_id, facet_type.facet_type_id}};
+      {true, initial_self_const_id, facet_type.facet_type_id}};
 
   // Outputs for the IdentifiedFacetType.
   bool partially_identified = false;
   llvm::SmallVector<SemIR::IdentifiedFacetType::RequiredImpl> extends;
   llvm::SmallVector<SemIR::IdentifiedFacetType::RequiredImpl> impls;
 
+  // `.Self` is always replaced with the top-level self type.
+  SubstPeriodSelfCallbacks callbacks(&context, loc_id, initial_self_const_id);
+
   while (!work.empty()) {
     SelfImplsFacetType next_impls = work.pop_back_val();
     bool facet_type_extends = next_impls.extend;
@@ -1005,13 +1008,19 @@ static auto IdentifyFacetType(Context& context, SemIR::LocId loc_id,
 
     auto self_and_interface = [&](SemIR::SpecificInterface interface)
         -> SemIR::IdentifiedFacetType::RequiredImpl {
-      return {self_const_id, interface};
+      // Note that we subst `.Self` in the interface, but we do not in the
+      // self type here, as that would be cyclical, replacing part of the self
+      // type with itself.
+      return {self_const_id, SubstPeriodSelf(context, callbacks, interface)};
     };
     auto type_and_interface =
-        [&](const SemIR::FacetTypeInfo::TypeImplsInterface& impls)
+        [&](SemIR::FacetTypeInfo::TypeImplsInterface impls)
         -> SemIR::IdentifiedFacetType::RequiredImpl {
-      return {context.constant_values().Get(impls.self_type),
-              impls.specific_interface};
+      auto self = SubstPeriodSelf(
+          context, callbacks, context.constant_values().Get(impls.self_type));
+      auto interface =
+          SubstPeriodSelf(context, callbacks, impls.specific_interface);
+      return {self, interface};
     };
 
     if (facet_type_extends) {

toolchain/diagnostics/kind.def

@@ -189,6 +189,7 @@ CARBON_DIAGNOSTIC_KIND(ExpectedAliasInitializer)
 // Where requirement diagnostics.
 CARBON_DIAGNOSTIC_KIND(ExpectedRequirementOperator)
 CARBON_DIAGNOSTIC_KIND(RequirementEqualAfterNonDesignator)
+CARBON_DIAGNOSTIC_KIND(AmbiguousPeriodSelf)
 
 // ============================================================================
 // Semantics diagnostics