Compare ImplWitnessAccess into Self as canonical constants (#5883)

This makes all `.Self` references in a facet type canonically the same (which will remain true iff they refer to the same `Self` type in the future), removing the need to do more complex comparisons between them using the EntityName, interface, and index. This allows the comparison of types containing `.Self` references to be done correctly regardless of where the `.Self` appears, as such type expressions will all be canonically equal if they otherwise equal now, regardless of whether they are written in the context where `.Self` could have seen different `Self` facet types. In order to retain access to constraints on a base `.Self` facet type, in the case of applying `where` to an existing facet type, we: - Give the base facet type as a `RequirementBaseFacetType` constraint so that eval of `WhereExpr` can find and copy all the constraints off of it. - Introduce eager/early rewrite constraint resolution, which allows a constraint to eagerly resolve access to earlier rewrite constraints (`where .A = () and .B = .A` is eagerly transformed into `where .A = () and .B = ()`) before the full constraint resolution step. This allows use of rewrite constraints in larger type expressions, such as `where .A = () and .B = C(.A)` and `C` will know that the argument is `()`.
2026-09-24 21:10:12 +01:00 · 2025-08-08 18:36:39 +00:00
parent edcc24ecf7
commit 3d77c4441b
39 changed files with 558 additions and 207 deletions
@@ -229,6 +229,13 @@ class Context {
    return poisoned_concrete_impl_lookup_queries_;
  }

+  // A stack that tracks the rewrite constraints from a `where` expression being
+  // checked. The back of the stack is the currently checked `where` expression.
+  auto rewrites_stack()
+      -> llvm::SmallVector<Map<SemIR::ConstantId, SemIR::InstId>>& {
+    return rewrites_stack_;
+  }
+
  // --------------------------------------------------------------------------
  // Directly expose SemIR::File data accessors for brevity in calls.
  // --------------------------------------------------------------------------
@@ -423,6 +430,11 @@ class Context {
  // results at the end of the file. Any difference is diagnosed.
  llvm::SmallVector<PoisonedConcreteImplLookupQuery>
      poisoned_concrete_impl_lookup_queries_;
+
+  // A map from an ImplWitnessAccess on the LHS of a rewrite constraint to its
+  // value on the RHS. Used during checking of a `where` expression to allow
+  // constraints to access values from earlier constraints.
+  llvm::SmallVector<Map<SemIR::ConstantId, SemIR::InstId>> rewrites_stack_;
 };

 }  // namespace Carbon::Check
@@ -18,6 +18,7 @@
 #include "toolchain/check/facet_type.h"
 #include "toolchain/check/generic.h"
 #include "toolchain/check/import_ref.h"
+#include "toolchain/check/name_lookup.h"
 #include "toolchain/check/type.h"
 #include "toolchain/check/type_completion.h"
 #include "toolchain/diagnostics/diagnostic.h"
@@ -637,6 +638,13 @@ static auto GetConstantFacetTypeInfo(EvalContext& eval_context,
  // canonical instruction, so that in a `WhereExpr` we can work with the
  // `ImplWitnessAccess` references to `.Self` on the LHS of the constraints
  // rather than the value of the associated constant they reference.
+  //
+  // This also implies that we may find `ImplWitnessAccessSubstituted`
+  // instructions in the LHS and RHS of these constraints, which are preserved
+  // to maintain them as an unresolved reference to an associated constant, but
+  // which must be handled gracefully during resolution. They will be replaced
+  // with the constant value of the `ImplWitnessAccess` below when they are
+  // substituted with a constant value.
  info.rewrite_constraints = orig.rewrite_constraints;
  if (!ResolveFacetTypeRewriteConstraints(eval_context.context(), loc_id,
                                          info.rewrite_constraints)) {
@@ -2049,31 +2057,32 @@ auto TryEvalTypedInst<SemIR::WhereExpr>(EvalContext& eval_context,
  auto typed_inst = inst.As<SemIR::WhereExpr>();

  Phase phase = Phase::Concrete;
-  SemIR::TypeId base_facet_type_id =
-      eval_context.GetTypeOfInst(typed_inst.period_self_id);
-  SemIR::Inst base_facet_inst =
-      eval_context.types().GetAsInst(base_facet_type_id);
  SemIR::FacetTypeInfo info = {.other_requirements = false};

-  // `where` provides that the base facet is an error, `type`, or a facet
-  // type.
-  if (auto facet_type = base_facet_inst.TryAs<SemIR::FacetType>()) {
-    info = eval_context.facet_types().Get(facet_type->facet_type_id);
-  } else if (base_facet_type_id == SemIR::ErrorInst::TypeId) {
-    return SemIR::ErrorInst::ConstantId;
-  } else {
-    CARBON_CHECK(base_facet_type_id == SemIR::TypeType::TypeId,
-                 "Unexpected type_id: {0}, inst: {1}", base_facet_type_id,
-                 base_facet_inst);
-  }
-
  // Add the constraints from the `WhereExpr` instruction into `info`.
  if (typed_inst.requirements_id.has_value()) {
    auto insts = eval_context.inst_blocks().Get(typed_inst.requirements_id);
    for (auto inst_id : insts) {
-      if (auto rewrite =
-              eval_context.insts().TryGetAs<SemIR::RequirementRewrite>(
+      if (auto base =
+              eval_context.insts().TryGetAs<SemIR::RequirementBaseFacetType>(
                  inst_id)) {
+        if (base->base_type_inst_id == SemIR::ErrorInst::TypeInstId) {
+          return SemIR::ErrorInst::ConstantId;
+        }
+
+        if (auto base_facet_type =
+                eval_context.insts().TryGetAs<SemIR::FacetType>(
+                    base->base_type_inst_id)) {
+          const auto& base_info =
+              eval_context.facet_types().Get(base_facet_type->facet_type_id);
+          info.extend_constraints.append(base_info.extend_constraints);
+          info.self_impls_constraints.append(base_info.self_impls_constraints);
+          info.rewrite_constraints.append(base_info.rewrite_constraints);
+          info.other_requirements |= base_info.other_requirements;
+        }
+      } else if (auto rewrite =
+                     eval_context.insts().TryGetAs<SemIR::RequirementRewrite>(
+                         inst_id)) {
        info.rewrite_constraints.push_back(
            {.lhs_id = rewrite->lhs_id, .rhs_id = rewrite->rhs_id});
      } else if (auto impls =
@@ -333,6 +333,13 @@ auto EvalConstantInst(Context& context, SemIR::InstId inst_id,
  return ConstantEvalResult::NewSamePhase(inst);
 }

+auto EvalConstantInst(Context& context,
+                      SemIR::ImplWitnessAccessSubstituted inst)
+    -> ConstantEvalResult {
+  return ConstantEvalResult::Existing(
+      context.constant_values().Get(inst.value_id));
+}
+
 auto EvalConstantInst(Context& context,
                      SemIR::ImplWitnessAssociatedConstant inst)
    -> ConstantEvalResult {
@@ -24,9 +24,11 @@ namespace Carbon::Check {

 auto FacetTypeFromInterface(Context& context, SemIR::InterfaceId interface_id,
                            SemIR::SpecificId specific_id) -> SemIR::FacetType {
-  SemIR::FacetTypeId facet_type_id = context.facet_types().Add(
+  auto info =
      SemIR::FacetTypeInfo{.extend_constraints = {{interface_id, specific_id}},
-                           .other_requirements = false});
+                           .other_requirements = false};
+  info.Canonicalize();
+  SemIR::FacetTypeId facet_type_id = context.facet_types().Add(info);
  return {.type_id = SemIR::TypeType::TypeId, .facet_type_id = facet_type_id};
 }

@@ -58,6 +60,16 @@ static auto IncompleteFacetTypeDiagnosticBuilder(
  }
 }

+auto GetImplWitnessAccessWithoutSubstitution(Context& context,
+                                             SemIR::InstId inst_id)
+    -> SemIR::InstId {
+  if (auto inst = context.insts().TryGetAs<SemIR::ImplWitnessAccessSubstituted>(
+          inst_id)) {
+    return inst->impl_witness_access_id;
+  }
+  return inst_id;
+}
+
 auto InitialFacetTypeImplWitness(
    Context& context, SemIR::LocId witness_loc_id,
    SemIR::TypeInstId facet_type_inst_id, SemIR::TypeInstId self_type_inst_id,
@@ -123,8 +135,8 @@ auto InitialFacetTypeImplWitness(
  }

  for (auto rewrite : facet_type_info.rewrite_constraints) {
-    auto access =
-        context.insts().GetAs<SemIR::ImplWitnessAccess>(rewrite.lhs_id);
+    auto access = context.insts().GetAs<SemIR::ImplWitnessAccess>(
+        GetImplWitnessAccessWithoutSubstitution(context, rewrite.lhs_id));
    if (!WitnessQueryMatchesInterface(context, access.witness_id,
                                      interface_to_witness)) {
      continue;
@@ -252,6 +264,9 @@ auto AllocateFacetTypeImplWitness(Context& context,
 }

 namespace {
+// TODO: This class should go away, and we should just use the constant value of
+// the ImplWitnessAccess as a key in AccessRewriteValues, but that requires
+// changing its API to work with InstId instead of ImplWitnessAccess.
 struct FacetTypeConstraintValue {
  SemIR::EntityNameId entity_name_id;
  SemIR::ElementIndex access_index;
@@ -280,32 +295,6 @@ static auto GetFacetTypeConstraintValue(Context& context,
  return std::nullopt;
 }

-// Returns true if two values in a rewrite constraint are equivalent. Two
-// `ImplWitnessAccess` instructions that refer to the same associated constant
-// through the same facet value are treated as equivalent.
-static auto CompareFacetTypeConstraintValues(Context& context,
-                                             SemIR::InstId lhs_id,
-                                             SemIR::InstId rhs_id) -> bool {
-  if (lhs_id == rhs_id) {
-    return true;
-  }
-
-  auto lhs_access = context.insts().TryGetAs<SemIR::ImplWitnessAccess>(lhs_id);
-  auto rhs_access = context.insts().TryGetAs<SemIR::ImplWitnessAccess>(rhs_id);
-  if (lhs_access && rhs_access) {
-    auto lhs_access_value = GetFacetTypeConstraintValue(context, *lhs_access);
-    auto rhs_access_value = GetFacetTypeConstraintValue(context, *rhs_access);
-    // We do *not* want to get the evaluated result of `ImplWitnessAccess` here,
-    // we want to keep them as a reference to an associated constant for the
-    // resolution phase.
-    return lhs_access_value && rhs_access_value &&
-           *lhs_access_value == *rhs_access_value;
-  }
-
-  return context.constant_values().GetConstantInstId(lhs_id) ==
-         context.constant_values().GetConstantInstId(rhs_id);
-}
-
 // A mapping of each associated constant (represented as `ImplWitnessAccess`) to
 // its value (represented as an `InstId`). Used to track rewrite constraints,
 // with the LHS mapping to the resolved value of the RHS.
@@ -349,9 +338,10 @@ class AccessRewriteValues {

  auto SetFullyRewritten(Context& context, Value& value, SemIR::InstId inst_id)
      -> void {
-    CARBON_CHECK(
-        value.state == BeingRewritten ||
-        CompareFacetTypeConstraintValues(context, value.inst_id, inst_id));
+    if (value.state == FullyRewritten) {
+      CARBON_CHECK(context.constant_values().Get(value.inst_id) ==
+                   context.constant_values().Get(inst_id));
+    }
    value = {FullyRewritten, inst_id};
  }

@@ -459,13 +449,22 @@ class SubstImplWitnessAccessCallbacks : public SubstInstCallbacks {
        // There's no ImplWitnessAccess that we care about inside this
        // instruction.
        return SubstResult::FullySubstituted;
-      } else {
-        // SubstOperands will result in a Rebuild or ReuseUnchanged callback, so
-        // push the non-ImplWitnessAccess to get proper bracketing, allowing us
-        // to pop it in the paired callback.
-        substs_in_progress_.push_back(rhs_inst_id);
-        return SubstResult::SubstOperands;
      }
+      if (auto subst =
+              context().insts().TryGetAs<SemIR::ImplWitnessAccessSubstituted>(
+                  rhs_inst_id)) {
+        // The reference to an associated constant was eagerly replaced with the
+        // value of an earlier rewrite constraint, but may need further
+        // substitution if it contains an `ImplWitnessAccess`.
+        rhs_inst_id = subst->value_id;
+        substs_in_progress_.push_back(rhs_inst_id);
+        return SubstResult::SubstAgain;
+      }
+      // SubstOperands will result in a Rebuild or ReuseUnchanged callback, so
+      // push the non-ImplWitnessAccess to get proper bracketing, allowing us
+      // to pop it in the paired callback.
+      substs_in_progress_.push_back(rhs_inst_id);
+      return SubstResult::SubstOperands;
    }

    // If the access is going through a nested `ImplWitnessAccess`, that
@@ -581,8 +580,8 @@ auto ResolveFacetTypeRewriteConstraints(
  AccessRewriteValues rewrite_values;

  for (auto& constraint : rewrites) {
-    auto lhs_access =
-        context.insts().TryGetAs<SemIR::ImplWitnessAccess>(constraint.lhs_id);
+    auto lhs_access = context.insts().TryGetAs<SemIR::ImplWitnessAccess>(
+        GetImplWitnessAccessWithoutSubstitution(context, constraint.lhs_id));
    if (!lhs_access) {
      continue;
    }
@@ -591,8 +590,8 @@ auto ResolveFacetTypeRewriteConstraints(
  }

  for (auto& constraint : rewrites) {
-    auto lhs_access =
-        context.insts().TryGetAs<SemIR::ImplWitnessAccess>(constraint.lhs_id);
+    auto lhs_access = context.insts().TryGetAs<SemIR::ImplWitnessAccess>(
+        GetImplWitnessAccessWithoutSubstitution(context, constraint.lhs_id));
    if (!lhs_access) {
      continue;
    }
@@ -610,33 +609,40 @@ auto ResolveFacetTypeRewriteConstraints(
      return false;
    }

-    if (lhs_rewrite_value->state == AccessRewriteValues::FullyRewritten &&
-        !CompareFacetTypeConstraintValues(context, lhs_rewrite_value->inst_id,
-                                          rhs_subst_inst_id)) {
-      if (lhs_rewrite_value->inst_id != SemIR::ErrorInst::InstId) {
-        CARBON_DIAGNOSTIC(AssociatedConstantWithDifferentValues, Error,
-                          "associated constant {0} given two different "
-                          "values {1} and {2}",
-                          InstIdAsConstant, InstIdAsConstant, InstIdAsConstant);
-        // Use inst id ordering as a simple proxy for source ordering, to
-        // try to name the values in the same order they appear in the facet
-        // type.
-        auto source_order1 =
-            lhs_rewrite_value->inst_id.index < rhs_subst_inst_id.index
-                ? lhs_rewrite_value->inst_id
-                : rhs_subst_inst_id;
-        auto source_order2 =
-            lhs_rewrite_value->inst_id.index >= rhs_subst_inst_id.index
-                ? lhs_rewrite_value->inst_id
-                : rhs_subst_inst_id;
-        // TODO: It would be nice to note the places where the values are
-        // assigned but rewrite constraint instructions are from canonical
-        // constant values, and have no locations. We'd need to store a
-        // location along with them in the rewrite constraints.
-        context.emitter().Emit(loc_id, AssociatedConstantWithDifferentValues,
-                               constraint.lhs_id, source_order1, source_order2);
+    if (lhs_rewrite_value->state == AccessRewriteValues::FullyRewritten) {
+      auto rhs_existing_const_id =
+          context.constant_values().Get(lhs_rewrite_value->inst_id);
+      auto rhs_subst_const_id =
+          context.constant_values().Get(rhs_subst_inst_id);
+      if (rhs_subst_const_id != rhs_existing_const_id) {
+        if (rhs_existing_const_id != SemIR::ErrorInst::ConstantId) {
+          CARBON_DIAGNOSTIC(AssociatedConstantWithDifferentValues, Error,
+                            "associated constant {0} given two different "
+                            "values {1} and {2}",
+                            InstIdAsConstant, InstIdAsConstant,
+                            InstIdAsConstant);
+          // Use inst id ordering as a simple proxy for source ordering, to
+          // try to name the values in the same order they appear in the facet
+          // type.
+          auto source_order1 =
+              lhs_rewrite_value->inst_id.index < rhs_subst_inst_id.index
+                  ? lhs_rewrite_value->inst_id
+                  : rhs_subst_inst_id;
+          auto source_order2 =
+              lhs_rewrite_value->inst_id.index >= rhs_subst_inst_id.index
+                  ? lhs_rewrite_value->inst_id
+                  : rhs_subst_inst_id;
+          // TODO: It would be nice to note the places where the values are
+          // assigned but rewrite constraint instructions are from canonical
+          // constant values, and have no locations. We'd need to store a
+          // location along with them in the rewrite constraints.
+          context.emitter().Emit(loc_id, AssociatedConstantWithDifferentValues,
+                                 GetImplWitnessAccessWithoutSubstitution(
+                                     context, constraint.lhs_id),
+                                 source_order1, source_order2);
+        }
+        return false;
      }
-      return false;
    }

    rewrite_values.SetFullyRewritten(context, *lhs_rewrite_value,
@@ -652,8 +658,8 @@ auto ResolveFacetTypeRewriteConstraints(
  for (size_t i = 0; i < keep_size;) {
    auto& constraint = rewrites[i];

-    auto lhs_access =
-        context.insts().TryGetAs<SemIR::ImplWitnessAccess>(constraint.lhs_id);
+    auto lhs_access = context.insts().TryGetAs<SemIR::ImplWitnessAccess>(
+        GetImplWitnessAccessWithoutSubstitution(context, constraint.lhs_id));
    if (!lhs_access) {
      ++i;
      continue;
@@ -18,6 +18,16 @@ namespace Carbon::Check {
 auto FacetTypeFromInterface(Context& context, SemIR::InterfaceId interface_id,
                            SemIR::SpecificId specific_id) -> SemIR::FacetType;

+// Given an ImplWitnessAccessSubstituted, returns the InstId of the
+// ImplWitnessAccess. Otherwise, returns the input `inst_id` unchanged.
+//
+// This must be used when accessing the LHS of a rewrite constraint which has
+// not yet been resolved in order to preserve which associated constant is being
+// rewritten.
+auto GetImplWitnessAccessWithoutSubstitution(Context& context,
+                                             SemIR::InstId inst_id)
+    -> SemIR::InstId;
+
 // Creates a impl witness instruction for a facet type. The facet type is
 // required to be complete if `is_definition` is true or the facet type has
 // rewrites. Otherwise a placeholder witness is created, and
@@ -4,10 +4,14 @@

 #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"
+#include "toolchain/check/type.h"
+#include "toolchain/sem_ir/facet_type_info.h"
 #include "toolchain/sem_ir/ids.h"
+#include "toolchain/sem_ir/inst.h"
 #include "toolchain/sem_ir/typed_insts.h"

 namespace Carbon::Check {
@@ -17,14 +21,32 @@ auto HandleParseNode(Context& context, Parse::WhereOperandId node_id) -> bool {
  // is being modified by the `where` operator. It would be `MyInterface` in
  // `MyInterface where .Member = i32`.
  auto [self_node, self_id] = context.node_stack().PopExprWithNodeId();
-  auto self_type_id = ExprAsType(context, self_node, self_id).type_id;
+  auto self_with_constraints_type_id =
+      ExprAsType(context, self_node, self_id).type_id;
  // Only facet types may have `where` restrictions.
-  if (self_type_id != SemIR::ErrorInst::TypeId &&
-      !context.types().IsFacetType(self_type_id)) {
+  if (self_with_constraints_type_id != SemIR::ErrorInst::TypeId &&
+      !context.types().IsFacetType(self_with_constraints_type_id)) {
    CARBON_DIAGNOSTIC(WhereOnNonFacetType, Error,
                      "left argument of `where` operator must be a facet type");
    context.emitter().Emit(self_node, WhereOnNonFacetType);
-    self_type_id = SemIR::ErrorInst::TypeId;
+    self_with_constraints_type_id = SemIR::ErrorInst::TypeId;
+  }
+
+  // Strip off any constraints provided by a `WhereExpr` from the `Self` facet
+  // type. For a facet type like `I & J where .X = .Y`, this will reduce it down
+  // to just `I & J`.
+  //
+  // Any references to `.Self` in constraints for the current `WhereExpr` will
+  // not see constraints in the `Self` facet type, but they will resolve to
+  // values through the constraints explicitly when they are combined together.
+  auto self_without_constraints_type_id = self_with_constraints_type_id;
+  if (auto facet_type = context.types().TryGetAs<SemIR::FacetType>(
+          self_without_constraints_type_id)) {
+    const auto& info = context.facet_types().Get(facet_type->facet_type_id);
+    auto stripped_info =
+        SemIR::FacetTypeInfo{.extend_constraints = info.extend_constraints};
+    stripped_info.Canonicalize();
+    self_without_constraints_type_id = GetFacetType(context, stripped_info);
  }

  // Introduce a name scope so that we can remove the `.Self` entry we are
@@ -32,29 +54,63 @@ auto HandleParseNode(Context& context, Parse::WhereOperandId node_id) -> bool {
  context.scope_stack().PushForSameRegion();
  // Introduce `.Self` as a symbolic binding. Its type is the value of the
  // expression to the left of `where`, so `MyInterface` in the example above.
+  //
+  // It uses the `Self` type _without_ any constraints so that the `Self` is the
+  // same at all levels of a nested facet type such as:
+  //   `(Z where .X = {}) where .X = {}`.
  auto entity_name_id = context.entity_names().AddCanonical(
      {.name_id = SemIR::NameId::PeriodSelf,
       .parent_scope_id = context.scope_stack().PeekNameScopeId()});
-  auto inst_id = AddInst(
+  auto period_self_inst_id = AddInst(
      context, SemIR::LocIdAndInst::NoLoc<SemIR::BindSymbolicName>({
-                   .type_id = self_type_id,
+                   .type_id = self_without_constraints_type_id,
                   .entity_name_id = entity_name_id,
                   // `None` because there is no equivalent non-symbolic value.
                   .value_id = SemIR::InstId::None,
               }));
-  auto existing =
-      context.scope_stack().LookupOrAddName(SemIR::NameId::PeriodSelf, inst_id);
+  auto existing = context.scope_stack().LookupOrAddName(
+      SemIR::NameId::PeriodSelf, period_self_inst_id);
  // Shouldn't have any names in newly created scope.
  CARBON_CHECK(!existing.has_value());

  // Save the `.Self` symbolic binding on the node stack. It will become the
  // first argument to the `WhereExpr` instruction.
-  context.node_stack().Push(node_id, inst_id);
+  context.node_stack().Push(node_id, period_self_inst_id);

  // Going to put each requirement on `args_type_info_stack`, so we can have an
  // inst block with the varying number of requirements but keeping other
  // instructions on the current inst block from the `inst_block_stack()`.
  context.args_type_info_stack().Push();
+
+  // Pass along all the constraints from the base facet type to be added to the
+  // resulting facet type.
+  context.args_type_info_stack().AddInstId(
+      AddInstInNoBlock<SemIR::RequirementBaseFacetType>(
+          context, SemIR::LocId(node_id),
+          {.base_type_inst_id =
+               context.types().GetInstId(self_with_constraints_type_id)}));
+
+  // Add a context stack for tracking rewrite constraints, that will be used to
+  // allow later constraints to read from them eagerly.
+  context.rewrites_stack().emplace_back();
+
+  // Make rewrite constraints from the self facet type available immediately to
+  // expressions in rewrite constraints for this `where` expression.
+  if (auto self_facet_type = context.types().TryGetAs<SemIR::FacetType>(
+          self_with_constraints_type_id)) {
+    const auto& base_facet_type_info =
+        context.facet_types().Get(self_facet_type->facet_type_id);
+    for (const auto& rewrite : base_facet_type_info.rewrite_constraints) {
+      if (rewrite.lhs_id != SemIR::ErrorInst::InstId) {
+        context.rewrites_stack().back().Insert(
+            context.constant_values().Get(
+                GetImplWitnessAccessWithoutSubstitution(context,
+                                                        rewrite.lhs_id)),
+            rewrite.rhs_id);
+      }
+    }
+  }
+
  return true;
 }

@@ -83,6 +139,17 @@ auto HandleParseNode(Context& context, Parse::RequirementEqualId node_id)
  context.args_type_info_stack().AddInstId(
      AddInstInNoBlock<SemIR::RequirementRewrite>(
          context, node_id, {.lhs_id = lhs_id, .rhs_id = rhs_id}));
+
+  if (lhs_id != SemIR::ErrorInst::InstId) {
+    // Track the value of the rewrite so further constraints can use it
+    // immediately, before they are evaluated. This happens directly where the
+    // `ImplWitnessAccess` that refers to the rewrite constraint would have been
+    // created, and the value of the constraint will be used instead.
+    context.rewrites_stack().back().Insert(
+        context.constant_values().Get(
+            GetImplWitnessAccessWithoutSubstitution(context, lhs_id)),
+        rhs_id);
+  }
  return true;
 }

@@ -135,6 +202,7 @@ auto HandleParseNode(Context& /*context*/, Parse::RequirementAndId /*node_id*/)
 }

 auto HandleParseNode(Context& context, Parse::WhereExprId node_id) -> bool {
+  context.rewrites_stack().pop_back();
  // Remove `PeriodSelf` from name lookup, undoing the `Push` done for the
  // `WhereOperand`.
  context.scope_stack().Pop();
@@ -347,6 +347,20 @@ static auto LookupMemberNameInScope(Context& context, SemIR::LocId loc_id,
    }
  }

+  if (!context.rewrites_stack().empty()) {
+    if (auto access =
+            context.insts().TryGetAs<SemIR::ImplWitnessAccess>(member_id)) {
+      if (auto result = context.rewrites_stack().back().Lookup(
+              context.constant_values().Get(member_id))) {
+        return GetOrAddInst<SemIR::ImplWitnessAccessSubstituted>(
+            context, loc_id,
+            {.type_id = access->type_id,
+             .impl_witness_access_id = member_id,
+             .value_id = result.value()});
+      }
+    }
+  }
+
  return member_id;
 }

@@ -390,6 +390,7 @@ fn F(U:! type, V:! type where {} impls Core.ImplicitAs(.Self)) {
 // CHECK:STDOUT:       %ImplicitAs.type.loc9: type = facet_type <@ImplicitAs, @ImplicitAs(constants.%.Self)> [symbolic_self = constants.%ImplicitAs.type.aba]
 // CHECK:STDOUT:       %.loc9_32.2: type = converted %.loc9_32.1, constants.%empty_struct_type [concrete = constants.%empty_struct_type]
 // CHECK:STDOUT:       %.loc9_25.2: type = where_expr %.Self [concrete = constants.%type_where] {
+// CHECK:STDOUT:         requirement_base_facet_type type
 // CHECK:STDOUT:         requirement_impls %.loc9_32.2, %ImplicitAs.type.loc9
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -524,6 +524,7 @@ fn G(AB:! A & B where .X = () and .Y = {}) -> AB.Y {
 // CHECK:STDOUT:       %.loc6_25.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:       %.loc6_25.2: type = converted %.loc6_25.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:       %.loc6_13.2: type = where_expr %.Self [concrete = constants.%A_where.type] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%A.type
 // CHECK:STDOUT:         requirement_rewrite %impl.elem0.loc6_19, %.loc6_25.2
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -637,6 +638,7 @@ fn G(AB:! A & B where .X = () and .Y = {}) -> AB.Y {
 // CHECK:STDOUT:       %.loc14_41.1: %empty_struct_type = struct_literal ()
 // CHECK:STDOUT:       %.loc14_41.2: type = converted %.loc14_41.1, constants.%empty_struct_type [concrete = constants.%empty_struct_type]
 // CHECK:STDOUT:       %.loc14_17.2: type = where_expr %.Self [concrete = constants.%facet_type.6d1] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%facet_type.938
 // CHECK:STDOUT:         requirement_rewrite %impl.elem0.loc14_23, %.loc14_29.2
 // CHECK:STDOUT:         requirement_rewrite %impl.elem0.loc14_35, %.loc14_41.2
 // CHECK:STDOUT:       }
@@ -679,6 +681,7 @@ fn G(AB:! A & B where .X = () and .Y = {}) -> AB.Y {
 // CHECK:STDOUT:       %.loc18_41.1: %empty_struct_type = struct_literal ()
 // CHECK:STDOUT:       %.loc18_41.2: type = converted %.loc18_41.1, constants.%empty_struct_type [concrete = constants.%empty_struct_type]
 // CHECK:STDOUT:       %.loc18_17.2: type = where_expr %.Self [concrete = constants.%facet_type.6d1] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%facet_type.938
 // CHECK:STDOUT:         requirement_rewrite %impl.elem0.loc18_23, %.loc18_29.2
 // CHECK:STDOUT:         requirement_rewrite %impl.elem0.loc18_35, %.loc18_41.2
 // CHECK:STDOUT:       }
@@ -796,6 +796,7 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:       %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:       %.loc9_31: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:       %.loc9_25.2: type = where_expr %.Self [concrete = constants.%A.type] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%A.type
 // CHECK:STDOUT:         requirement_impls %.loc9_31, type
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -936,6 +937,7 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:       %.Self: type = bind_symbolic_name .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.Self.ref: type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.loc4_33.2: type = where_expr %.Self [concrete = constants.%type] {
+// CHECK:STDOUT:         requirement_base_facet_type type
 // CHECK:STDOUT:         requirement_impls %.Self.ref, type
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -960,6 +962,7 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:       %.Self: type = bind_symbolic_name .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.Self.ref: type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.loc9_41.2: type = where_expr %.Self [concrete = constants.%type] {
+// CHECK:STDOUT:         requirement_base_facet_type type
 // CHECK:STDOUT:         requirement_impls %.Self.ref, type
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -1115,6 +1118,7 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:       %.Self: type = bind_symbolic_name .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.Self.ref: type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.loc3_36.2: type = where_expr %.Self [concrete = constants.%type] {
+// CHECK:STDOUT:         requirement_base_facet_type type
 // CHECK:STDOUT:         requirement_impls %.Self.ref, type
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -1144,6 +1148,7 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:       %.Self: type = bind_symbolic_name .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.Self.ref: type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.loc8_37.2: type = where_expr %.Self [concrete = constants.%type] {
+// CHECK:STDOUT:         requirement_base_facet_type type
 // CHECK:STDOUT:         requirement_impls %.Self.ref, type
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -101,6 +101,13 @@ class C(T:! Z where .Z1 = ()) {}

 interface J {
  // Implied: .Z1 == (), but this is also explicitly required for J1.
+  // CHECK:STDERR: fail_todo_nested_constraint_visible_in_type_parameter.carbon:[[@LINE+7]]:43: error: cannot convert type `.Self` that implements `Z` into type implementing `Z where .(Z.Z1) = ()` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   let J1:! (Z where .Z1 = ()) where .Z2 = C(.Self);
+  // CHECK:STDERR:                                           ^~~~~~~~
+  // CHECK:STDERR: fail_todo_nested_constraint_visible_in_type_parameter.carbon:[[@LINE-7]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: class C(T:! Z where .Z1 = ()) {}
+  // CHECK:STDERR:         ^
+  // CHECK:STDERR:
  let J1:! (Z where .Z1 = ()) where .Z2 = C(.Self);
 }

@@ -111,15 +118,11 @@ class D;
 // CHECK:STDERR: fail_todo_nested_constraint_visible_in_type_parameter.carbon:[[@LINE+7]]:38: error: cannot convert type `.Self` that implements `Z` into type implementing `Z where .(Z.Z1) = ()` [ConversionFailureFacetToFacet]
 // CHECK:STDERR: impl D as Z where .Z1 = () and .Z2 = C(.Self) {}
 // CHECK:STDERR:                                      ^~~~~~~~
-// CHECK:STDERR: fail_todo_nested_constraint_visible_in_type_parameter.carbon:[[@LINE-14]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+// CHECK:STDERR: fail_todo_nested_constraint_visible_in_type_parameter.carbon:[[@LINE-21]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
 // CHECK:STDERR: class C(T:! Z where .Z1 = ()) {}
 // CHECK:STDERR:         ^
 // CHECK:STDERR:
 impl D as Z where .Z1 = () and .Z2 = C(.Self) {}
-// CHECK:STDERR: fail_todo_nested_constraint_visible_in_type_parameter.carbon:[[@LINE+4]]:24: error: cannot convert type `D` into type implementing `Z where .(Z.Z1) = () and .(Z.Z2) = C(.Self)` [ConversionFailureTypeToFacet]
-// CHECK:STDERR: fn G(T:! J where .J1 = D) {
-// CHECK:STDERR:                        ^
-// CHECK:STDERR:
 fn G(T:! J where .J1 = D) {
  F(T);
 }
@@ -238,7 +241,7 @@ fn G(T:! J where .J1 = D) {
  F(T);
 }

-// --- fail_todo_early_rewrite_applied.carbon
+// --- early_rewrite_applied.carbon
 library "[[@TEST_NAME]]";

 interface Z {
@@ -252,13 +255,6 @@ class C(T:! Tuple) {}

 interface J {
  // Implied: .Z1 == (), but this is also explicitly required for J1.
-  // CHECK:STDERR: fail_todo_early_rewrite_applied.carbon:[[@LINE+7]]:39: error: cannot convert type `.(Z.Z1)` into type implementing `Tuple` [ConversionFailureTypeToFacet]
-  // CHECK:STDERR:   let J1:! Z where .Z1 = () and .Z2 = C(.Z1);
-  // CHECK:STDERR:                                       ^~~~~~
-  // CHECK:STDERR: fail_todo_early_rewrite_applied.carbon:[[@LINE-7]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
-  // CHECK:STDERR: class C(T:! Tuple) {}
-  // CHECK:STDERR:         ^
-  // CHECK:STDERR:
  let J1:! Z where .Z1 = () and .Z2 = C(.Z1);
 }

@@ -271,6 +267,32 @@ fn G(T:! J where .J1 = D) {
  F(T);
 }

+// --- early_rewrite_applied_from_nested_self.carbon
+library "[[@TEST_NAME]]";
+
+interface Z {
+  let Z1:! type;
+  let Z2:! type;
+}
+
+interface Tuple {}
+impl () as Tuple {}
+class C(T:! Tuple) {}
+
+interface J {
+  // Implied: .Z1 == (), but this is also explicitly required for J1.
+  let J1:! (Z where .Z1 = ()) where .Z2 = C(.Z1);
+}
+
+fn F(T:! J) {}
+
+class D;
+// Satisfies the implied constraint in J.J1.
+impl D as Z where .Z1 = () and .Z2 = C(()) {}
+fn G(T:! J where .J1 = D) {
+  F(T);
+}
+
 // --- fail_todo_early_rewrite_applied_extra_indirection.carbon
 library "[[@TEST_NAME]]";

@@ -289,13 +311,6 @@ class C(T:! Tuple) {}

 interface J {
  // Implied: .Z1 == (), but this is also explicitly required for J1.
-  // CHECK:STDERR: fail_todo_early_rewrite_applied_extra_indirection.carbon:[[@LINE+7]]:59: error: cannot convert type `.(Y.Y1).(Z.Z1)` into type implementing `Tuple` [ConversionFailureTypeToFacet]
-  // CHECK:STDERR:   let J1:! Y & Z where .Y1 = .Self and .Z1 = () and .Z2 = C(.Y1.Z1);
-  // CHECK:STDERR:                                                           ^~~~~~~~~
-  // CHECK:STDERR: fail_todo_early_rewrite_applied_extra_indirection.carbon:[[@LINE-7]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
-  // CHECK:STDERR: class C(T:! Tuple) {}
-  // CHECK:STDERR:         ^
-  // CHECK:STDERR:
  let J1:! Y & Z where .Y1 = .Self and .Z1 = () and .Z2 = C(.Y1.Z1);
 }

@@ -305,6 +320,10 @@ 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);
 }
@@ -328,13 +347,6 @@ class C(T:! Tuple) {}

 interface J {
  // Implied: .Y1 impls Tuple, but this is also explicitly required for J1.
-  // CHECK:STDERR: fail_todo_resolved_constraint_visible_in_type_parameter.carbon:[[@LINE+7]]:76: error: cannot convert type `.(Z.Z2)` into type implementing `Tuple` [ConversionFailureTypeToFacet]
-  // CHECK:STDERR:   let J1:! Z & Y where .Y1 = () and .Z1 = .Self and .Z2 = .Z1.Y1 and .Z3 = C(.Z2);
-  // CHECK:STDERR:                                                                            ^~~~~~
-  // CHECK:STDERR: fail_todo_resolved_constraint_visible_in_type_parameter.carbon:[[@LINE-7]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
-  // CHECK:STDERR: class C(T:! Tuple) {}
-  // CHECK:STDERR:         ^
-  // CHECK:STDERR:
  let J1:! Z & Y where .Y1 = () and .Z1 = .Self and .Z2 = .Z1.Y1 and .Z3 = C(.Z2);
 }

@@ -348,6 +360,10 @@ impl D as Y where .Y1 = () {}
 // CHECK:STDERR:                         ^~~~~
 // CHECK:STDERR:
 impl D as Z where .Z1 = .Self and .Z2 = () and .Z3 = C(()) {}
+// CHECK:STDERR: fail_todo_resolved_constraint_visible_in_type_parameter.carbon:[[@LINE+4]]:24: error: cannot convert type `D` into type implementing `Y & Z where .(Y.Y1) = () and .(Z.Z1) = .Self as Y and .(Z.Z2) = () and .(Z.Z3) = 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);
 }
@@ -277,7 +277,7 @@ interface M { let X:! type; let Y:! type; let Z:! type; }
 // The value of .X and .Y becomes <error> but .Z is still valid.
 //
 //@dump-sem-ir-begin
-// CHECK:STDERR: fail_cycle.carbon:[[@LINE+4]]:10: error: found cycle in facet type constraint for `.(M.X)` [FacetTypeConstraintCycle]
+// CHECK:STDERR: fail_cycle.carbon:[[@LINE+4]]:10: error: found cycle in facet type constraint for `.(M.Y)` [FacetTypeConstraintCycle]
 // CHECK:STDERR: fn F(T:! M where .X = .Y and .Y = .X and .Z = ()) {}
 // CHECK:STDERR:          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 // CHECK:STDERR:
@@ -297,7 +297,7 @@ interface J {

 // This fails because it resolves to `.X1 = .X1` which is cyclical.
 //
-// CHECK:STDERR: fail_cycle_between_interfaces.carbon:[[@LINE+4]]:10: error: found cycle in facet type constraint for `.(I.X1)` [FacetTypeConstraintCycle]
+// CHECK:STDERR: fail_cycle_between_interfaces.carbon:[[@LINE+4]]:10: error: found cycle in facet type constraint for `.(J.X3)` [FacetTypeConstraintCycle]
 // CHECK:STDERR: fn G(T:! I & J where .X1 = .X3 and .X2 = .X1 and .X3 = .X2) {}
 // CHECK:STDERR:          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 // CHECK:STDERR:
@@ -313,7 +313,7 @@ interface I {

 // This fails because it resolves to `.X1 = .X1**` which is cyclical.
 //
-// CHECK:STDERR: fail_indirect_cycle.carbon:[[@LINE+4]]:10: error: found cycle in facet type constraint for `.(I.X1)` [FacetTypeConstraintCycle]
+// CHECK:STDERR: fail_indirect_cycle.carbon:[[@LINE+4]]:10: error: found cycle in facet type constraint for `.(I.X2)` [FacetTypeConstraintCycle]
 // CHECK:STDERR: fn F(T:! I where .X1 = .X2* and .X2 = .X1*);
 // CHECK:STDERR:          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 // CHECK:STDERR:
@@ -322,7 +322,7 @@ fn F(T:! I where .X1 = .X2* and .X2 = .X1*);
 class C(T:! type);
 // This fails because it resolves to `.X1 = C(C(.X1))` which is cyclical.
 //
-// CHECK:STDERR: fail_indirect_cycle.carbon:[[@LINE+4]]:10: error: found cycle in facet type constraint for `.(I.X1)` [FacetTypeConstraintCycle]
+// CHECK:STDERR: fail_indirect_cycle.carbon:[[@LINE+4]]:10: error: found cycle in facet type constraint for `.(I.X2)` [FacetTypeConstraintCycle]
 // CHECK:STDERR: fn G(T:! I where .X1 = C(.X2) and .X2 = C(.X1));
 // CHECK:STDERR:          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 // CHECK:STDERR:
@@ -342,7 +342,7 @@ class C(T:! type, U:! type);
 // This fails because it resolves to `.X1 = C(C(.X3, .X1), .X3)` which is
 // cyclical.
 //
-// CHECK:STDERR: fail_complex_indirect_cycle.carbon:[[@LINE+4]]:10: error: found cycle in facet type constraint for `.(I.X1)` [FacetTypeConstraintCycle]
+// CHECK:STDERR: fail_complex_indirect_cycle.carbon:[[@LINE+4]]:10: error: found cycle in facet type constraint for `.(I.X2)` [FacetTypeConstraintCycle]
 // CHECK:STDERR: fn F(T:! I where .X1 = C(.X2, .X3) and .X2 = C(.X3, .X1));
 // CHECK:STDERR:          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 // CHECK:STDERR:
@@ -403,7 +403,7 @@ interface Z {
 // approach can recursively rebuild the RHS values from the ground up
 // repeatedly.
 fn F(
-    // CHECK:STDERR: fail_exponential_large_cycle.carbon:[[@LINE+4]]:9: error: found cycle in facet type constraint for `.(Z.T9)` [FacetTypeConstraintCycle]
+    // CHECK:STDERR: fail_exponential_large_cycle.carbon:[[@LINE+4]]:9: error: found cycle in facet type constraint for `.(Z.T0)` [FacetTypeConstraintCycle]
    // CHECK:STDERR:     T:! Z where
    // CHECK:STDERR:         ^~~~~~~
    // CHECK:STDERR:
@@ -535,7 +535,7 @@ interface Z {
  let T3:! type;
 }

-// CHECK:STDERR: fail_cycle_with_unrelated_associated_constant.carbon:[[@LINE+4]]:10: error: found cycle in facet type constraint for `.(Z.T0)` [FacetTypeConstraintCycle]
+// CHECK:STDERR: fail_cycle_with_unrelated_associated_constant.carbon:[[@LINE+4]]:10: error: found cycle in facet type constraint for `.(Z.T1)` [FacetTypeConstraintCycle]
 // CHECK:STDERR: fn F(T:! Z where .T0 = .T1 and .T1 = .T0 and .T2 = .T3) {}
 // CHECK:STDERR:          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 // CHECK:STDERR:
@@ -554,13 +554,13 @@ interface Z {

 // TODO: There should only be one diagnostic here.
 //
-// CHECK:STDERR: fail_cycle_with_branching_in_rhs.carbon:[[@LINE+4]]:10: error: found cycle in facet type constraint for `.(Z.T1)` [FacetTypeConstraintCycle]
+// CHECK:STDERR: fail_cycle_with_branching_in_rhs.carbon:[[@LINE+4]]:10: error: found cycle in facet type constraint for `.(Z.T3)` [FacetTypeConstraintCycle]
 // CHECK:STDERR: fn F(T:! Z where .T0 = .T1 and .T1 = (.T2, .T3) and .T2 = .T4 and .T3 = .T1) {}
 // CHECK:STDERR:          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 // CHECK:STDERR:
 fn F(T:! Z where .T0 = .T1 and .T1 = (.T2, .T3) and .T2 = .T4 and .T3 = .T1) {}

-// CHECK:STDERR: fail_cycle_with_branching_in_rhs.carbon:[[@LINE+4]]:10: error: found cycle in facet type constraint for `.(Z.T0)` [FacetTypeConstraintCycle]
+// CHECK:STDERR: fail_cycle_with_branching_in_rhs.carbon:[[@LINE+4]]:10: error: found cycle in facet type constraint for `.(Z.T1)` [FacetTypeConstraintCycle]
 // CHECK:STDERR: fn G(T:! Z where .T0 = .T1 and .T1 = (.T2, .T3) and .T2 = .T4 and .T3 = .T0) {}
 // CHECK:STDERR:          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 // CHECK:STDERR:
@@ -705,6 +705,7 @@ fn F(T:! I & J where .I1 = .J1.I2) {}
 // CHECK:STDOUT:       %.Self.as_type.loc13_35: type = facet_access_type %.Self.ref.loc13_35 [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:       %.loc13_35: type = converted %.Self.ref.loc13_35, %.Self.as_type.loc13_35 [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:       %impl.elem0.loc13_35: type = impl_witness_access constants.%M.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
+// CHECK:STDOUT:       %impl.elem0.subst: type = impl_witness_access_substituted %impl.elem0.loc13_35, %impl.elem1.loc13_23 [symbolic_self = constants.%impl.elem1]
 // CHECK:STDOUT:       %.Self.ref.loc13_42: %M.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %Z.ref: %M.assoc_type = name_ref Z, @Z.%assoc2 [concrete = constants.%assoc2]
 // CHECK:STDOUT:       %.Self.as_type.loc13_42: type = facet_access_type %.Self.ref.loc13_42 [symbolic_self = constants.%.Self.as_type]
@@ -713,8 +714,9 @@ fn F(T:! I & J where .I1 = .J1.I2) {}
 // CHECK:STDOUT:       %.loc13_48.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:       %.loc13_48.2: type = converted %.loc13_48.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:       %.loc13_12.2: type = where_expr %.Self [concrete = <error>] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%M.type
 // CHECK:STDOUT:         requirement_rewrite %impl.elem0.loc13_18, %impl.elem1.loc13_23
-// CHECK:STDOUT:         requirement_rewrite %impl.elem1.loc13_30, %impl.elem0.loc13_35
+// CHECK:STDOUT:         requirement_rewrite %impl.elem1.loc13_30, %impl.elem0.subst
 // CHECK:STDOUT:         requirement_rewrite %impl.elem2, %.loc13_48.2
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -54,7 +54,7 @@ interface Z {

 fn F(FF:! ((Z where .T = .U and .U = .V) where .T = .U and .U = .V) where .T = .U and .U = .V) {}

-// --- fail_todo_nested_facet_types_same_associated_in_generic_parameter.carbon
+// --- nested_facet_types_same_associated_in_generic_parameter.carbon
 library "[[@TEST_NAME]]";

 interface Z {
@@ -63,10 +63,6 @@ interface Z {
 }
 class C(T:! type) {}

-// CHECK:STDERR: fail_todo_nested_facet_types_same_associated_in_generic_parameter.carbon:[[@LINE+4]]:12: error: associated constant `.(Z.T)` given two different values `C(.(Z.U))` and `C(.(Z.U))` [AssociatedConstantWithDifferentValues]
-// CHECK:STDERR: fn F(FF:! ((Z where .T = C(.U)) where .T = C(.U)) where .T = C(.U)) {}
-// CHECK:STDERR:            ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-// CHECK:STDERR:
 fn F(FF:! ((Z where .T = C(.U)) where .T = C(.U)) where .T = C(.U)) {}

 // --- fail_nested_facet_types_different.carbon
@@ -143,7 +139,7 @@ interface Z {
  let U:! type;
 }

-// CHECK:STDERR: fail_nested_facet_type_cycle.carbon:[[@LINE+4]]:11: error: found cycle in facet type constraint for `.(Z.T)` [FacetTypeConstraintCycle]
+// CHECK:STDERR: fail_nested_facet_type_cycle.carbon:[[@LINE+4]]:11: error: found cycle in facet type constraint for `.(Z.U)` [FacetTypeConstraintCycle]
 // CHECK:STDERR: fn F(FF:! (Z where .T = .U) where .U = .T) {}
 // CHECK:STDERR:           ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 // CHECK:STDERR:
@@ -231,7 +227,6 @@ fn F3(T:! Z where .Y = C(()) and .X = C(.Y) and .X = C(C(()))) -> T.X {
 }

 // --- conflicting_syntax_same_value.carbon
-
 library "[[@TEST_NAME]]";

 interface Z { let X:! type; let Y:! type; }
@@ -243,3 +238,33 @@ fn F1(T:! ((Z where .Y = ()) where .X = .Y) where .X = ()) -> T.X {
 fn F2(T:! ((Z where .Y = ()) where .X = ()) where .X = .Y) -> T.X {
  return ();
 }
+
+// --- nested_impls_repeated.carbon
+library "[[@TEST_NAME]]";
+
+interface Y {}
+interface Z {
+  let T:! type;
+  let U:! type;
+}
+class C(T:! type) {}
+
+fn F(FF:! ((Y where .Self impls (Z where .T = C(.U)))
+                where .Self impls (Z where .T = C(.U)))
+                  where .Self impls (Z where .T = C(.U))) {}
+
+// --- nested_impl_unique.carbon
+library "[[@TEST_NAME]]";
+
+interface Y {
+  let Y1:! type;
+}
+interface Z {
+  let Z1:! type;
+  let Z2:! type;
+}
+class C(T:! type) { adapt (); }
+
+fn F(FF:! ((Y where .Y1 = ()) where .Self impls (Z where .Z1 = C(.Z2) and .Z2 = ()))) -> FF.(Z.Z1) {
+  return () as C(());
+}
@@ -217,26 +217,26 @@ fn Read() {
 // CHECK:STDOUT:   %Core.import_ref.1c9: %Iterate.assoc_type = import_ref Core//prelude/iterate, loc12_18, loaded [concrete = constants.%assoc0.724]
 // CHECK:STDOUT:   %Core.import_ref.ed6: %Iterate.assoc_type = import_ref Core//prelude/iterate, loc13_17, loaded [concrete = constants.%assoc1.02e]
 // CHECK:STDOUT:   %Core.import_ref.9e6: type = import_ref Core//prelude/iterate, loc13_17, loaded [concrete = %CursorType]
-// CHECK:STDOUT:   %Core.import_ref.f49c: @Optional.%Optional.None.type (%Optional.None.type.ef2) = import_ref Core//prelude/iterate, inst134 [indirect], loaded [symbolic = @Optional.%Optional.None (constants.%Optional.None.fd6)]
+// CHECK:STDOUT:   %Core.import_ref.f49: @Optional.%Optional.None.type (%Optional.None.type.ef2) = import_ref Core//prelude/iterate, inst134 [indirect], loaded [symbolic = @Optional.%Optional.None (constants.%Optional.None.fd6)]
 // CHECK:STDOUT:   %Core.import_ref.1a8: @Optional.%Optional.Some.type (%Optional.Some.type.b2c) = import_ref Core//prelude/iterate, inst135 [indirect], loaded [symbolic = @Optional.%Optional.Some (constants.%Optional.Some.d0d)]
-// CHECK:STDOUT:   %Core.import_ref.cf4: @Core.IntLiteral.as.ImplicitAs.impl.%Core.IntLiteral.as.ImplicitAs.impl.Convert.type (%Core.IntLiteral.as.ImplicitAs.impl.Convert.type.0f9) = import_ref Core//prelude/iterate, inst474 [indirect], loaded [symbolic = @Core.IntLiteral.as.ImplicitAs.impl.%Core.IntLiteral.as.ImplicitAs.impl.Convert (constants.%Core.IntLiteral.as.ImplicitAs.impl.Convert.f06)]
+// CHECK:STDOUT:   %Core.import_ref.cf4: @Core.IntLiteral.as.ImplicitAs.impl.%Core.IntLiteral.as.ImplicitAs.impl.Convert.type (%Core.IntLiteral.as.ImplicitAs.impl.Convert.type.0f9) = import_ref Core//prelude/iterate, inst475 [indirect], loaded [symbolic = @Core.IntLiteral.as.ImplicitAs.impl.%Core.IntLiteral.as.ImplicitAs.impl.Convert (constants.%Core.IntLiteral.as.ImplicitAs.impl.Convert.f06)]
 // CHECK:STDOUT:   %ImplicitAs.impl_witness_table.2b9 = impl_witness_table (%Core.import_ref.cf4), @Core.IntLiteral.as.ImplicitAs.impl [concrete]
-// CHECK:STDOUT:   %Core.import_ref.741: @Int.as.Destroy.impl.%Int.as.Destroy.impl.Op.type (%Int.as.Destroy.impl.Op.type) = import_ref Core//prelude/iterate, inst443 [indirect], loaded [symbolic = @Int.as.Destroy.impl.%Int.as.Destroy.impl.Op (constants.%Int.as.Destroy.impl.Op)]
+// CHECK:STDOUT:   %Core.import_ref.741: @Int.as.Destroy.impl.%Int.as.Destroy.impl.Op.type (%Int.as.Destroy.impl.Op.type) = import_ref Core//prelude/iterate, inst444 [indirect], loaded [symbolic = @Int.as.Destroy.impl.%Int.as.Destroy.impl.Op (constants.%Int.as.Destroy.impl.Op)]
 // CHECK:STDOUT:   %Destroy.impl_witness_table.1b4 = impl_witness_table (%Core.import_ref.741), @Int.as.Destroy.impl [concrete]
-// CHECK:STDOUT:   %Core.import_ref.19a: @OrderedWith.%OrderedWith.assoc_type (%OrderedWith.assoc_type.03c) = import_ref Core//prelude/iterate, inst854 [indirect], loaded [symbolic = @OrderedWith.%assoc0 (constants.%assoc0.5db)]
-// CHECK:STDOUT:   %Core.import_ref.b2b: @Int.as.OrderedWith.impl.db3.%Int.as.OrderedWith.impl.Less.type (%Int.as.OrderedWith.impl.Less.type.2c7) = import_ref Core//prelude/iterate, inst943 [indirect], loaded [symbolic = @Int.as.OrderedWith.impl.db3.%Int.as.OrderedWith.impl.Less (constants.%Int.as.OrderedWith.impl.Less.a5a)]
-// CHECK:STDOUT:   %Core.import_ref.ab6 = import_ref Core//prelude/iterate, inst944 [indirect], unloaded
-// CHECK:STDOUT:   %Core.import_ref.875 = import_ref Core//prelude/iterate, inst945 [indirect], unloaded
-// CHECK:STDOUT:   %Core.import_ref.82b = import_ref Core//prelude/iterate, inst946 [indirect], unloaded
+// CHECK:STDOUT:   %Core.import_ref.19a: @OrderedWith.%OrderedWith.assoc_type (%OrderedWith.assoc_type.03c) = import_ref Core//prelude/iterate, inst855 [indirect], loaded [symbolic = @OrderedWith.%assoc0 (constants.%assoc0.5db)]
+// CHECK:STDOUT:   %Core.import_ref.b2b: @Int.as.OrderedWith.impl.db3.%Int.as.OrderedWith.impl.Less.type (%Int.as.OrderedWith.impl.Less.type.2c7) = import_ref Core//prelude/iterate, inst944 [indirect], loaded [symbolic = @Int.as.OrderedWith.impl.db3.%Int.as.OrderedWith.impl.Less (constants.%Int.as.OrderedWith.impl.Less.a5a)]
+// CHECK:STDOUT:   %Core.import_ref.ab6 = import_ref Core//prelude/iterate, inst945 [indirect], unloaded
+// CHECK:STDOUT:   %Core.import_ref.875 = import_ref Core//prelude/iterate, inst946 [indirect], unloaded
+// CHECK:STDOUT:   %Core.import_ref.82b = import_ref Core//prelude/iterate, inst947 [indirect], unloaded
 // CHECK:STDOUT:   %OrderedWith.impl_witness_table.476 = impl_witness_table (%Core.import_ref.b2b, %Core.import_ref.ab6, %Core.import_ref.875, %Core.import_ref.82b), @Int.as.OrderedWith.impl.db3 [concrete]
-// CHECK:STDOUT:   %Core.import_ref.13d: @OrderedWith.%OrderedWith.Less.type (%OrderedWith.Less.type.f19) = import_ref Core//prelude/iterate, inst1918 [indirect], loaded [symbolic = @OrderedWith.%OrderedWith.Less (constants.%OrderedWith.Less.02e)]
+// CHECK:STDOUT:   %Core.import_ref.13d: @OrderedWith.%OrderedWith.Less.type (%OrderedWith.Less.type.f19) = import_ref Core//prelude/iterate, inst1919 [indirect], loaded [symbolic = @OrderedWith.%OrderedWith.Less (constants.%OrderedWith.Less.02e)]
 // CHECK:STDOUT:   %CursorType: type = assoc_const_decl @CursorType [concrete] {}
 // CHECK:STDOUT:   %Core.import_ref.4f9: type = import_ref Core//prelude/iterate, loc12_18, loaded [concrete = %ElementType]
 // CHECK:STDOUT:   %ElementType: type = assoc_const_decl @ElementType [concrete] {}
 // CHECK:STDOUT:   %Core.Optional: %Optional.type = import_ref Core//prelude/types/optional, Optional, loaded [concrete = constants.%Optional.generic]
 // CHECK:STDOUT:   %Core.Destroy: type = import_ref Core//prelude/destroy, Destroy, loaded [concrete = constants.%Destroy.type]
 // CHECK:STDOUT:   %Core.OrderedWith: %OrderedWith.type.270 = import_ref Core//prelude/operators/comparison, OrderedWith, loaded [concrete = constants.%OrderedWith.generic]
-// CHECK:STDOUT:   %Core.import_ref.d49 = import_ref Core//prelude/iterate, inst6636 [indirect], unloaded
+// CHECK:STDOUT:   %Core.import_ref.d49 = import_ref Core//prelude/iterate, inst6637 [indirect], unloaded
 // CHECK:STDOUT:   %Core.Inc: type = import_ref Core//prelude/operators/arithmetic, Inc, loaded [concrete = constants.%Inc.type]
 // CHECK:STDOUT:   %Core.ImplicitAs: %ImplicitAs.type.cc7 = import_ref Core//prelude/operators/as, ImplicitAs, loaded [concrete = constants.%ImplicitAs.generic]
 // CHECK:STDOUT: }
@@ -451,6 +451,7 @@ fn Read() {
 // CHECK:STDOUT:       %N.ref.loc9_84: Core.IntLiteral = name_ref N, @IntRange.%N.loc4_16.2 [symbolic = %N (constants.%N.c80)]
 // CHECK:STDOUT:       %Int.loc9_85: type = class_type @Int, @Int(constants.%N.c80) [symbolic = %Int.loc9_54.1 (constants.%Int.49d0e6.1)]
 // CHECK:STDOUT:       %.loc9_24: type = where_expr %.Self [symbolic = %Iterate_where.type (constants.%Iterate_where.type.fce)] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%Iterate.type
 // CHECK:STDOUT:         requirement_rewrite %impl.elem1, %Int.loc9_54.2
 // CHECK:STDOUT:         requirement_rewrite %impl.elem0, %Int.loc9_85
 // CHECK:STDOUT:       }
@@ -667,7 +668,7 @@ fn Read() {
 // CHECK:STDOUT:     %N.ref.loc17: Core.IntLiteral = name_ref N, @IntRange.%N.loc4_16.2 [symbolic = %N (constants.%N.c80)]
 // CHECK:STDOUT:     %Int.loc17: type = class_type @Int, @Int(constants.%N.c80) [symbolic = %Int.loc11_43.1 (constants.%Int.49d0e6.1)]
 // CHECK:STDOUT:     %Optional.loc17: type = class_type @Optional, @Optional(constants.%Int.49d0e6.1) [symbolic = %Optional.loc11_75.1 (constants.%Optional.708)]
-// CHECK:STDOUT:     %.loc17: @IntRange.as.Iterate.impl.Next.%Optional.None.type (%Optional.None.type.73a) = specific_constant imports.%Core.import_ref.f49c, @Optional(constants.%Int.49d0e6.1) [symbolic = %Optional.None (constants.%Optional.None.83e)]
+// CHECK:STDOUT:     %.loc17: @IntRange.as.Iterate.impl.Next.%Optional.None.type (%Optional.None.type.73a) = specific_constant imports.%Core.import_ref.f49, @Optional(constants.%Int.49d0e6.1) [symbolic = %Optional.None (constants.%Optional.None.83e)]
 // CHECK:STDOUT:     %None.ref: @IntRange.as.Iterate.impl.Next.%Optional.None.type (%Optional.None.type.73a) = name_ref None, %.loc17 [symbolic = %Optional.None (constants.%Optional.None.83e)]
 // CHECK:STDOUT:     %Optional.None.specific_fn.loc17_42.1: <specific function> = specific_function %None.ref, @Optional.None(constants.%Int.49d0e6.1) [symbolic = %Optional.None.specific_fn.loc17_42.2 (constants.%Optional.None.specific_fn.82b)]
 // CHECK:STDOUT:     %.loc11_47.3: ref @IntRange.as.Iterate.impl.Next.%Optional.loc11_75.1 (%Optional.708) = splice_block %return {}
@@ -995,7 +996,7 @@ fn Read() {
 // CHECK:STDOUT:   %Main.import_ref.0c8 = import_ref Main//lib, loc9_87, unloaded
 // CHECK:STDOUT:   %Main.import_ref.f1e294.3: Core.IntLiteral = import_ref Main//lib, loc4_16, loaded [symbolic = @IntRange.%N (constants.%N.c80)]
 // CHECK:STDOUT:   %Main.import_ref.dae: type = import_ref Main//lib, loc9_8, loaded [symbolic = @IntRange.as.Iterate.impl.%IntRange (constants.%IntRange.349)]
-// CHECK:STDOUT:   %Main.import_ref.35b: type = import_ref Main//lib, loc9_24, loaded [symbolic = @IntRange.as.Iterate.impl.%Iterate_where.type (constants.%Iterate_where.type.2cb)]
+// CHECK:STDOUT:   %Main.import_ref.ce4: type = import_ref Main//lib, loc9_24, loaded [symbolic = @IntRange.as.Iterate.impl.%Iterate_where.type (constants.%Iterate_where.type.2cb)]
 // CHECK:STDOUT:   %Main.import_ref.e3faa9.1 = import_ref Main//lib, loc9_87, unloaded
 // CHECK:STDOUT:   %Main.import_ref.e3faa9.2 = import_ref Main//lib, loc9_87, unloaded
 // CHECK:STDOUT:   %Main.import_ref.11c = import_ref Main//lib, loc10_47, unloaded
@@ -1003,11 +1004,11 @@ fn Read() {
 // CHECK:STDOUT:   %Iterate.impl_witness_table.b32 = impl_witness_table (%Main.import_ref.e3faa9.1, %Main.import_ref.e3faa9.2, %Main.import_ref.11c, %Main.import_ref.f97), @IntRange.as.Iterate.impl [concrete]
 // CHECK:STDOUT:   %Main.import_ref.f1e294.4: Core.IntLiteral = import_ref Main//lib, loc4_16, loaded [symbolic = @IntRange.%N (constants.%N.c80)]
 // CHECK:STDOUT:   %Main.import_ref.f1e294.5: Core.IntLiteral = import_ref Main//lib, loc4_16, loaded [symbolic = @IntRange.%N (constants.%N.c80)]
-// CHECK:STDOUT:   %Main.import_ref.026 = import_ref Main//lib, inst1891 [indirect], unloaded
+// CHECK:STDOUT:   %Main.import_ref.026 = import_ref Main//lib, inst1892 [indirect], unloaded
 // CHECK:STDOUT:   %Main.import_ref.921 = import_ref Main//lib, loc4_39, unloaded
 // CHECK:STDOUT:   %Main.import_ref.f1e294.6: Core.IntLiteral = import_ref Main//lib, loc4_16, loaded [symbolic = @IntRange.%N (constants.%N.c80)]
 // CHECK:STDOUT:   %Main.import_ref.e9a: type = import_ref Main//lib, inst40 [no loc], loaded [symbolic = constants.%IntRange.349]
-// CHECK:STDOUT:   %Main.import_ref.cb9: type = import_ref Main//lib, inst298 [no loc], loaded [concrete = constants.%Destroy.type]
+// CHECK:STDOUT:   %Main.import_ref.cb9: type = import_ref Main//lib, inst299 [no loc], loaded [concrete = constants.%Destroy.type]
 // CHECK:STDOUT:   %Main.import_ref.b63 = import_ref Main//lib, loc4_39, unloaded
 // CHECK:STDOUT:   %Destroy.impl_witness_table.901 = impl_witness_table (%Main.import_ref.b63), @IntRange.as.Destroy.impl [concrete]
 // CHECK:STDOUT:   %Main.import_ref.f1e294.7: Core.IntLiteral = import_ref Main//lib, loc4_16, loaded [symbolic = @IntRange.%N (constants.%N.c80)]
@@ -1039,7 +1040,7 @@ fn Read() {
 // CHECK:STDOUT:   %IntRange.as.Iterate.impl.Next.type: type = fn_type @IntRange.as.Iterate.impl.Next, @IntRange.as.Iterate.impl(%N) [symbolic = %IntRange.as.Iterate.impl.Next.type (constants.%IntRange.as.Iterate.impl.Next.type)]
 // CHECK:STDOUT:   %IntRange.as.Iterate.impl.Next: @IntRange.as.Iterate.impl.%IntRange.as.Iterate.impl.Next.type (%IntRange.as.Iterate.impl.Next.type) = struct_value () [symbolic = %IntRange.as.Iterate.impl.Next (constants.%IntRange.as.Iterate.impl.Next)]
 // CHECK:STDOUT:
-// CHECK:STDOUT:   impl: imports.%Main.import_ref.dae as imports.%Main.import_ref.35b {
+// CHECK:STDOUT:   impl: imports.%Main.import_ref.dae as imports.%Main.import_ref.ce4 {
 // CHECK:STDOUT:   !members:
 // CHECK:STDOUT:     witness = imports.%Main.import_ref.0c8
 // CHECK:STDOUT:   }
@@ -186,8 +186,8 @@ fn Run() {
 // CHECK:STDOUT:   %Main.import_ref.57b: @EmptyRange.as.Iterate.impl.%EmptyRange.as.Iterate.impl.NewCursor.type (%EmptyRange.as.Iterate.impl.NewCursor.type.f5f) = import_ref Main//empty_range, loc8_38, loaded [symbolic = @EmptyRange.as.Iterate.impl.%EmptyRange.as.Iterate.impl.NewCursor (constants.%EmptyRange.as.Iterate.impl.NewCursor.ec1)]
 // CHECK:STDOUT:   %Main.import_ref.170: @EmptyRange.as.Iterate.impl.%EmptyRange.as.Iterate.impl.Next.type (%EmptyRange.as.Iterate.impl.Next.type.264) = import_ref Main//empty_range, loc11_58, loaded [symbolic = @EmptyRange.as.Iterate.impl.%EmptyRange.as.Iterate.impl.Next (constants.%EmptyRange.as.Iterate.impl.Next.08e)]
 // CHECK:STDOUT:   %Iterate.impl_witness_table = impl_witness_table (%Main.import_ref.6ce, %Main.import_ref.999, %Main.import_ref.57b, %Main.import_ref.170), @EmptyRange.as.Iterate.impl [concrete]
-// CHECK:STDOUT:   %Main.import_ref.7f9: @Optional.%Optional.HasValue.type (%Optional.HasValue.type.f81) = import_ref Main//empty_range, inst137 [indirect], loaded [symbolic = @Optional.%Optional.HasValue (constants.%Optional.HasValue.6fd)]
-// CHECK:STDOUT:   %Main.import_ref.d10: @Optional.%Optional.Get.type (%Optional.Get.type.b8f) = import_ref Main//empty_range, inst138 [indirect], loaded [symbolic = @Optional.%Optional.Get (constants.%Optional.Get.9c8)]
+// CHECK:STDOUT:   %Main.import_ref.7f9: @Optional.%Optional.HasValue.type (%Optional.HasValue.type.f81) = import_ref Main//empty_range, inst138 [indirect], loaded [symbolic = @Optional.%Optional.HasValue (constants.%Optional.HasValue.6fd)]
+// CHECK:STDOUT:   %Main.import_ref.d10: @Optional.%Optional.Get.type (%Optional.Get.type.b8f) = import_ref Main//empty_range, inst139 [indirect], loaded [symbolic = @Optional.%Optional.Get (constants.%Optional.Get.9c8)]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: fn @Run() {
@@ -343,8 +343,8 @@ fn Run() {
 // CHECK:STDOUT:   %Main.import_ref.57b: @EmptyRange.as.Iterate.impl.%EmptyRange.as.Iterate.impl.NewCursor.type (%EmptyRange.as.Iterate.impl.NewCursor.type.f5f) = import_ref Main//empty_range, loc8_38, loaded [symbolic = @EmptyRange.as.Iterate.impl.%EmptyRange.as.Iterate.impl.NewCursor (constants.%EmptyRange.as.Iterate.impl.NewCursor.ec1)]
 // CHECK:STDOUT:   %Main.import_ref.170: @EmptyRange.as.Iterate.impl.%EmptyRange.as.Iterate.impl.Next.type (%EmptyRange.as.Iterate.impl.Next.type.264) = import_ref Main//empty_range, loc11_58, loaded [symbolic = @EmptyRange.as.Iterate.impl.%EmptyRange.as.Iterate.impl.Next (constants.%EmptyRange.as.Iterate.impl.Next.08e)]
 // CHECK:STDOUT:   %Iterate.impl_witness_table = impl_witness_table (%Main.import_ref.6ce, %Main.import_ref.999, %Main.import_ref.57b, %Main.import_ref.170), @EmptyRange.as.Iterate.impl [concrete]
-// CHECK:STDOUT:   %Main.import_ref.7f9: @Optional.%Optional.HasValue.type (%Optional.HasValue.type.f81) = import_ref Main//empty_range, inst137 [indirect], loaded [symbolic = @Optional.%Optional.HasValue (constants.%Optional.HasValue.6fd)]
-// CHECK:STDOUT:   %Main.import_ref.d10: @Optional.%Optional.Get.type (%Optional.Get.type.b8f) = import_ref Main//empty_range, inst138 [indirect], loaded [symbolic = @Optional.%Optional.Get (constants.%Optional.Get.9c8)]
+// CHECK:STDOUT:   %Main.import_ref.7f9: @Optional.%Optional.HasValue.type (%Optional.HasValue.type.f81) = import_ref Main//empty_range, inst138 [indirect], loaded [symbolic = @Optional.%Optional.HasValue (constants.%Optional.HasValue.6fd)]
+// CHECK:STDOUT:   %Main.import_ref.d10: @Optional.%Optional.Get.type (%Optional.Get.type.b8f) = import_ref Main//empty_range, inst139 [indirect], loaded [symbolic = @Optional.%Optional.Get (constants.%Optional.Get.9c8)]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: fn @Run() {
@@ -509,8 +509,8 @@ fn Run() {
 // CHECK:STDOUT:   %Main.import_ref.57b: @EmptyRange.as.Iterate.impl.%EmptyRange.as.Iterate.impl.NewCursor.type (%EmptyRange.as.Iterate.impl.NewCursor.type.f5f) = import_ref Main//empty_range, loc8_38, loaded [symbolic = @EmptyRange.as.Iterate.impl.%EmptyRange.as.Iterate.impl.NewCursor (constants.%EmptyRange.as.Iterate.impl.NewCursor.ec1)]
 // CHECK:STDOUT:   %Main.import_ref.170: @EmptyRange.as.Iterate.impl.%EmptyRange.as.Iterate.impl.Next.type (%EmptyRange.as.Iterate.impl.Next.type.264) = import_ref Main//empty_range, loc11_58, loaded [symbolic = @EmptyRange.as.Iterate.impl.%EmptyRange.as.Iterate.impl.Next (constants.%EmptyRange.as.Iterate.impl.Next.08e)]
 // CHECK:STDOUT:   %Iterate.impl_witness_table = impl_witness_table (%Main.import_ref.6ce, %Main.import_ref.999, %Main.import_ref.57b, %Main.import_ref.170), @EmptyRange.as.Iterate.impl [concrete]
-// CHECK:STDOUT:   %Main.import_ref.7f9: @Optional.%Optional.HasValue.type (%Optional.HasValue.type.f81) = import_ref Main//empty_range, inst137 [indirect], loaded [symbolic = @Optional.%Optional.HasValue (constants.%Optional.HasValue.6fd)]
-// CHECK:STDOUT:   %Main.import_ref.d10: @Optional.%Optional.Get.type (%Optional.Get.type.b8f) = import_ref Main//empty_range, inst138 [indirect], loaded [symbolic = @Optional.%Optional.Get (constants.%Optional.Get.9c8)]
+// CHECK:STDOUT:   %Main.import_ref.7f9: @Optional.%Optional.HasValue.type (%Optional.HasValue.type.f81) = import_ref Main//empty_range, inst138 [indirect], loaded [symbolic = @Optional.%Optional.HasValue (constants.%Optional.HasValue.6fd)]
+// CHECK:STDOUT:   %Main.import_ref.d10: @Optional.%Optional.Get.type (%Optional.Get.type.b8f) = import_ref Main//empty_range, inst139 [indirect], loaded [symbolic = @Optional.%Optional.Get (constants.%Optional.Get.9c8)]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: fn @Run() {
@@ -694,8 +694,8 @@ fn Run() {
 // CHECK:STDOUT:   %Main.import_ref.57b: @EmptyRange.as.Iterate.impl.%EmptyRange.as.Iterate.impl.NewCursor.type (%EmptyRange.as.Iterate.impl.NewCursor.type.f5f) = import_ref Main//empty_range, loc8_38, loaded [symbolic = @EmptyRange.as.Iterate.impl.%EmptyRange.as.Iterate.impl.NewCursor (constants.%EmptyRange.as.Iterate.impl.NewCursor.ec1)]
 // CHECK:STDOUT:   %Main.import_ref.170: @EmptyRange.as.Iterate.impl.%EmptyRange.as.Iterate.impl.Next.type (%EmptyRange.as.Iterate.impl.Next.type.264) = import_ref Main//empty_range, loc11_58, loaded [symbolic = @EmptyRange.as.Iterate.impl.%EmptyRange.as.Iterate.impl.Next (constants.%EmptyRange.as.Iterate.impl.Next.08e)]
 // CHECK:STDOUT:   %Iterate.impl_witness_table = impl_witness_table (%Main.import_ref.6ce, %Main.import_ref.999, %Main.import_ref.57b, %Main.import_ref.170), @EmptyRange.as.Iterate.impl [concrete]
-// CHECK:STDOUT:   %Main.import_ref.7f9: @Optional.%Optional.HasValue.type (%Optional.HasValue.type.f81) = import_ref Main//empty_range, inst137 [indirect], loaded [symbolic = @Optional.%Optional.HasValue (constants.%Optional.HasValue.6fd)]
-// CHECK:STDOUT:   %Main.import_ref.d10: @Optional.%Optional.Get.type (%Optional.Get.type.b8f) = import_ref Main//empty_range, inst138 [indirect], loaded [symbolic = @Optional.%Optional.Get (constants.%Optional.Get.9c8)]
+// CHECK:STDOUT:   %Main.import_ref.7f9: @Optional.%Optional.HasValue.type (%Optional.HasValue.type.f81) = import_ref Main//empty_range, inst138 [indirect], loaded [symbolic = @Optional.%Optional.HasValue (constants.%Optional.HasValue.6fd)]
+// CHECK:STDOUT:   %Main.import_ref.d10: @Optional.%Optional.Get.type (%Optional.Get.type.b8f) = import_ref Main//empty_range, inst139 [indirect], loaded [symbolic = @Optional.%Optional.Get (constants.%Optional.Get.9c8)]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: fn @Run() {
@@ -147,6 +147,7 @@ fn H(T:! type) {
 // CHECK:STDOUT:         %impl.elem0.loc11_24.2: type = impl_witness_access constants.%A.lookup_impl_witness.4e49fb.1, element0 [symbolic = %impl.elem0.loc11_24.1 (constants.%impl.elem0.452c56.1)]
 // CHECK:STDOUT:         %CC.ref.loc11_29: type = name_ref CC, @C.%CC.loc6_9.2 [symbolic = %CC (constants.%CC)]
 // CHECK:STDOUT:         %.loc11_18.2: type = where_expr %.Self.2 [symbolic = %A_where.type (constants.%A_where.type.5b404c.1)] {
+// CHECK:STDOUT:           requirement_base_facet_type constants.%A.type.75a876.2
 // CHECK:STDOUT:           requirement_rewrite %impl.elem0.loc11_24.2, %CC.ref.loc11_29
 // CHECK:STDOUT:         }
 // CHECK:STDOUT:       }
@@ -383,6 +384,7 @@ fn H(T:! type) {
 // CHECK:STDOUT:       %.loc9_48.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:       %.loc9_48.2: type = converted %.loc9_48.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:       %.loc9_36.2: type = where_expr %.Self.1 [symbolic = %A_where.type (constants.%A_where.type.812090.1)] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%A.type.75a876.1
 // CHECK:STDOUT:         requirement_rewrite %impl.elem0.loc9_42.1, %.loc9_48.2
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -183,6 +183,7 @@ fn CallF() {
 // CHECK:STDOUT:     %empty_struct: %empty_struct_type = struct_value () [concrete = constants.%empty_struct]
 // CHECK:STDOUT:     %.loc8_26.2: %empty_struct_type = converted %.loc8_26.1, %empty_struct [concrete = constants.%empty_struct]
 // CHECK:STDOUT:     %.loc8_14: type = where_expr %.Self [concrete = constants.%I_where.type.6ef] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %.loc8_26.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -201,6 +202,7 @@ fn CallF() {
 // CHECK:STDOUT:     %impl.elem0: %.Self.as_type = impl_witness_access constants.%I.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0.d8c]
 // CHECK:STDOUT:     %int_0: Core.IntLiteral = int_value 0 [concrete = constants.%int_0.5c6]
 // CHECK:STDOUT:     %.loc10_15: type = where_expr %.Self [concrete = constants.%I_where.type.3d4] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %int_0
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -323,6 +325,7 @@ fn CallF() {
 // CHECK:STDOUT:     %impl.elem0: %.Self.as_type = impl_witness_access constants.%I.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
 // CHECK:STDOUT:     %int_0: Core.IntLiteral = int_value 0 [concrete = constants.%int_0]
 // CHECK:STDOUT:     %.loc15_14: type = where_expr %.Self [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %int_0
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -463,6 +466,7 @@ fn CallF() {
 // CHECK:STDOUT:     %empty_tuple: %empty_tuple.type = tuple_value () [concrete = constants.%empty_tuple]
 // CHECK:STDOUT:     %.loc18_25.2: %empty_tuple.type = converted %.loc18_25.1, %empty_tuple [concrete = constants.%empty_tuple]
 // CHECK:STDOUT:     %.loc18_13: type = where_expr %.Self [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %.loc18_25.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -672,6 +676,7 @@ fn CallF() {
 // CHECK:STDOUT:     %impl.elem0: <error> = impl_witness_access constants.%I.lookup_impl_witness, element0 [concrete = <error>]
 // CHECK:STDOUT:     %.loc15_30: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:     %.loc15_18: type = where_expr %.Self [concrete = <error>] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type.057
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, <error>
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -818,6 +823,7 @@ fn CallF() {
 // CHECK:STDOUT:       %empty_struct: %empty_struct_type = struct_value () [concrete = constants.%empty_struct]
 // CHECK:STDOUT:       %.loc8_60.2: %empty_struct_type = converted %.loc8_60.1, %empty_struct [concrete = constants.%empty_struct]
 // CHECK:STDOUT:       %.loc8_12.2: type = where_expr %.Self [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:         requirement_impls %.loc8_19.2, %ImplicitAs.type
 // CHECK:STDOUT:         requirement_rewrite %impl.elem0, %.loc8_60.2
 // CHECK:STDOUT:       }
@@ -163,6 +163,7 @@ impl {.a: bool} as type where .Self impls I {}
 // CHECK:STDOUT:     %.Self: type = bind_symbolic_name .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:     %.Self.ref: type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:     %.loc8_18: type = where_expr %.Self [concrete = constants.%type] {
+// CHECK:STDOUT:       requirement_base_facet_type type
 // CHECK:STDOUT:       requirement_impls %.Self.ref, type
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -210,6 +211,7 @@ impl {.a: bool} as type where .Self impls I {}
 // CHECK:STDOUT:     %.Self.ref: type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:     %I.ref: type = name_ref I, file.%I.decl [concrete = constants.%I.type]
 // CHECK:STDOUT:     %.loc10_25: type = where_expr %.Self [concrete = constants.%type_where] {
+// CHECK:STDOUT:       requirement_base_facet_type type
 // CHECK:STDOUT:       requirement_impls %.Self.ref, %I.ref
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -170,6 +170,7 @@ impl C as J where .Self impls Incomplete and .T = ();
 // CHECK:STDOUT:     %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:     %.loc15_19: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:     %.loc15_13: type = where_expr %.Self [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_impls %.loc15_19, %Incomplete.ref
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -243,6 +244,7 @@ impl C as J where .Self impls Incomplete and .T = ();
 // CHECK:STDOUT:     %.loc15_52.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:     %.loc15_52.2: type = converted %.loc15_52.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:     %.loc15_13: type = where_expr %.Self [concrete = constants.%J_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%J.type
 // CHECK:STDOUT:       requirement_impls %.loc15_19, %Incomplete.ref
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %.loc15_52.2
 // CHECK:STDOUT:     }
@@ -529,6 +529,7 @@ interface I {
 // CHECK:STDOUT:     %.loc6_26.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:     %.loc6_26.2: type = converted %.loc6_26.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:     %.loc6_14: type = where_expr %.Self.2 [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc6, %.loc6_26.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -548,6 +549,7 @@ interface I {
 // CHECK:STDOUT:     %.loc8_26.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:     %.loc8_26.2: type = converted %.loc8_26.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:     %.loc8_14: type = where_expr %.Self.1 [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc8, %.loc8_26.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -639,6 +641,7 @@ interface I {
 // CHECK:STDOUT:     %.loc7_25.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:     %.loc7_25.2: type = converted %.loc7_25.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:     %.loc7_13: type = where_expr %.Self.2 [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc7, %.loc7_25.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -671,6 +674,7 @@ interface I {
 // CHECK:STDOUT:     %.loc11_25.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:     %.loc11_25.2: type = converted %.loc11_25.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:     %.loc11_13: type = where_expr %.Self.1 [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc11, %.loc11_25.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -799,6 +803,7 @@ interface I {
 // CHECK:STDOUT:     %.loc7_25.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:     %.loc7_25.2: type = converted %.loc7_25.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:     %.loc7_13: type = where_expr %.Self.2 [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc7, %.loc7_25.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -833,6 +838,7 @@ interface I {
 // CHECK:STDOUT:     %.loc11_25.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:     %.loc11_25.2: type = converted %.loc11_25.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:     %.loc11_13: type = where_expr %.Self.1 [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc11, %.loc11_25.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -1078,6 +1084,7 @@ interface I {
 // CHECK:STDOUT:     %.Self.ref.loc13: %I.type = name_ref .Self, %.Self.2 [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:     %C.ref.loc13: type = name_ref C, file.%C.decl.loc4 [concrete = constants.%C]
 // CHECK:STDOUT:     %.loc13: type = where_expr %.Self.2 [concrete = <error>] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite <error>, <error>
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -1091,6 +1098,7 @@ interface I {
 // CHECK:STDOUT:     %T.ref: <error> = name_ref T, <error> [concrete = <error>]
 // CHECK:STDOUT:     %C.ref.loc21: type = name_ref C, file.%C.decl.loc4 [concrete = constants.%C]
 // CHECK:STDOUT:     %.loc21: type = where_expr %.Self.1 [concrete = <error>] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %T.ref, <error>
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -1246,6 +1254,7 @@ interface I {
 // CHECK:STDOUT:     %impl.elem0.loc8: type = impl_witness_access constants.%I.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
 // CHECK:STDOUT:     %C.ref.loc8_27: type = name_ref C, file.%C.decl.loc6 [concrete = constants.%C]
 // CHECK:STDOUT:     %.loc8_16: type = where_expr %.Self.2 [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type.e7a
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc8, %C.ref.loc8_27
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -1267,6 +1276,7 @@ interface I {
 // CHECK:STDOUT:     %impl.elem0.loc11: type = impl_witness_access constants.%I.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
 // CHECK:STDOUT:     %C.ref.loc11_27: type = name_ref C, file.%C.decl.loc6 [concrete = constants.%C]
 // CHECK:STDOUT:     %.loc11_16: type = where_expr %.Self.1 [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type.e7a
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc11, %C.ref.loc11_27
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -1742,6 +1752,7 @@ interface I {
 // CHECK:STDOUT:     %.loc9_25.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:     %.loc9_25.2: type = converted %.loc9_25.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:     %.loc9_13: type = where_expr %.Self.2 [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc9, %.loc9_25.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -1760,6 +1771,7 @@ interface I {
 // CHECK:STDOUT:     %.loc18_25.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:     %.loc18_25.2: type = converted %.loc18_25.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:     %.loc18_13: type = where_expr %.Self.1 [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc18, %.loc18_25.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -2398,6 +2410,7 @@ interface I {
 // CHECK:STDOUT:       %impl.elem0.loc12: type = impl_witness_access constants.%I.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
 // CHECK:STDOUT:       %C.ref.loc12_28: type = name_ref C, @I.F.%C.decl [symbolic = %C (constants.%C)]
 // CHECK:STDOUT:       %.loc12_17: type = where_expr %.Self.2 [symbolic = %I_where.type (constants.%I_where.type)] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:         requirement_rewrite %impl.elem0.loc12, %C.ref.loc12_28
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -2415,6 +2428,7 @@ interface I {
 // CHECK:STDOUT:       %impl.elem0.loc21: type = impl_witness_access constants.%I.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
 // CHECK:STDOUT:       %C.ref.loc21_28: type = name_ref C, @I.F.%C.decl [symbolic = %C (constants.%C)]
 // CHECK:STDOUT:       %.loc21_17: type = where_expr %.Self.1 [symbolic = %I_where.type (constants.%I_where.type)] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:         requirement_rewrite %impl.elem0.loc21, %C.ref.loc21_28
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -255,7 +255,7 @@ interface M { let X:! type; let Y:! type; let Z:! type; }
 // The value of .X and .Y becomes <error> but .Z is still valid.
 //
 //@dump-sem-ir-begin
-// CHECK:STDERR: fail_cycle.carbon:[[@LINE+4]]:12: error: found cycle in facet type constraint for `.(M.X)` [FacetTypeConstraintCycle]
+// CHECK:STDERR: fail_cycle.carbon:[[@LINE+4]]:12: error: found cycle in facet type constraint for `.(M.Y)` [FacetTypeConstraintCycle]
 // CHECK:STDERR: impl () as M where .X = .Y and .Y = .X and .Z = () {}
 // CHECK:STDERR:            ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 // CHECK:STDERR:
@@ -439,6 +439,7 @@ fn G() {
 // CHECK:STDOUT:     %.Self.as_type.loc13_42: type = facet_access_type %.Self.ref.loc13_42 [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:     %.loc13_42: type = converted %.Self.ref.loc13_42, %.Self.as_type.loc13_42 [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:     %impl.elem0.loc13_42: type = impl_witness_access constants.%L.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
+// CHECK:STDOUT:     %impl.elem0.subst.loc13_42: type = impl_witness_access_substituted %impl.elem0.loc13_42, %.loc13_36.5 [concrete = constants.%tuple.type.2d5]
 // CHECK:STDOUT:     %.loc13_49: %empty_struct_type = struct_literal ()
 // CHECK:STDOUT:     %.loc13_53: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:     %.loc13_57: %empty_tuple.type = tuple_literal ()
@@ -452,6 +453,7 @@ fn G() {
 // CHECK:STDOUT:     %.Self.as_type.loc13_64: type = facet_access_type %.Self.ref.loc13_64 [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:     %.loc13_64: type = converted %.Self.ref.loc13_64, %.Self.as_type.loc13_64 [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:     %impl.elem0.loc13_64: type = impl_witness_access constants.%L.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
+// CHECK:STDOUT:     %impl.elem0.subst.loc13_64: type = impl_witness_access_substituted %impl.elem0.loc13_64, %.loc13_36.5 [concrete = constants.%tuple.type.2d5]
 // CHECK:STDOUT:     %.loc13_71: %empty_struct_type = struct_literal ()
 // CHECK:STDOUT:     %.loc13_75: %empty_struct_type = struct_literal ()
 // CHECK:STDOUT:     %.loc13_79: %empty_tuple.type = tuple_literal ()
@@ -465,6 +467,7 @@ fn G() {
 // CHECK:STDOUT:     %.Self.as_type.loc13_86: type = facet_access_type %.Self.ref.loc13_86 [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:     %.loc13_86: type = converted %.Self.ref.loc13_86, %.Self.as_type.loc13_86 [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:     %impl.elem0.loc13_86: type = impl_witness_access constants.%L.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
+// CHECK:STDOUT:     %impl.elem0.subst.loc13_86: type = impl_witness_access_substituted %impl.elem0.loc13_86, %.loc13_36.5 [concrete = constants.%tuple.type.2d5]
 // CHECK:STDOUT:     %.loc13_93: %empty_struct_type = struct_literal ()
 // CHECK:STDOUT:     %.loc13_97: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:     %.loc13_101: %empty_struct_type = struct_literal ()
@@ -474,10 +477,11 @@ fn G() {
 // CHECK:STDOUT:     %.loc13_102.4: type = converted %.loc13_101, constants.%empty_struct_type [concrete = constants.%empty_struct_type]
 // CHECK:STDOUT:     %.loc13_102.5: type = converted %.loc13_102.1, constants.%tuple.type.bd8 [concrete = constants.%tuple.type.bd8]
 // CHECK:STDOUT:     %.loc13_14: type = where_expr %.Self [concrete = <error>] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%L.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc13_20, %.loc13_36.5
-// CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc13_42, %.loc13_58.5
-// CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc13_64, %.loc13_80.5
-// CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc13_86, %.loc13_102.5
+// CHECK:STDOUT:       requirement_rewrite %impl.elem0.subst.loc13_42, %.loc13_58.5
+// CHECK:STDOUT:       requirement_rewrite %impl.elem0.subst.loc13_64, %.loc13_80.5
+// CHECK:STDOUT:       requirement_rewrite %impl.elem0.subst.loc13_86, %.loc13_102.5
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
@@ -530,6 +534,7 @@ fn G() {
 // CHECK:STDOUT:     %.Self.as_type.loc13_37: type = facet_access_type %.Self.ref.loc13_37 [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:     %.loc13_37: type = converted %.Self.ref.loc13_37, %.Self.as_type.loc13_37 [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:     %impl.elem0.loc13_37: type = impl_witness_access constants.%M.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
+// CHECK:STDOUT:     %impl.elem0.subst: type = impl_witness_access_substituted %impl.elem0.loc13_37, %impl.elem1.loc13_25 [symbolic_self = constants.%impl.elem1]
 // CHECK:STDOUT:     %.Self.ref.loc13_44: %M.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:     %Z.ref: %M.assoc_type = name_ref Z, @Z.%assoc2 [concrete = constants.%assoc2]
 // CHECK:STDOUT:     %.Self.as_type.loc13_44: type = facet_access_type %.Self.ref.loc13_44 [symbolic_self = constants.%.Self.as_type]
@@ -538,8 +543,9 @@ fn G() {
 // CHECK:STDOUT:     %.loc13_50.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:     %.loc13_50.2: type = converted %.loc13_50.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:     %.loc13_14: type = where_expr %.Self [concrete = <error>] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%M.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc13_20, %impl.elem1.loc13_25
-// CHECK:STDOUT:       requirement_rewrite %impl.elem1.loc13_32, %impl.elem0.loc13_37
+// CHECK:STDOUT:       requirement_rewrite %impl.elem1.loc13_32, %impl.elem0.subst
 // CHECK:STDOUT:       requirement_rewrite %impl.elem2, %.loc13_50.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -176,6 +176,7 @@ impl () as I where .X = {.a = true, .b = (1, 2)} and .X = {.a = false, .b = (3,
 // CHECK:STDOUT:     %.Self.as_type.loc6_54: type = facet_access_type %.Self.ref.loc6_54 [symbolic_self = constants.%.Self.as_type.541]
 // CHECK:STDOUT:     %.loc6_54: type = converted %.Self.ref.loc6_54, %.Self.as_type.loc6_54 [symbolic_self = constants.%.Self.as_type.541]
 // CHECK:STDOUT:     %impl.elem0.loc6_54: %struct_type.a.b.fe2 = impl_witness_access constants.%I.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0.74b]
+// CHECK:STDOUT:     %impl.elem0.subst: %struct_type.a.b.fe2 = impl_witness_access_substituted %impl.elem0.loc6_54, %.loc6_48.3 [concrete = constants.%struct]
 // CHECK:STDOUT:     %false: bool = bool_literal false [concrete = constants.%false]
 // CHECK:STDOUT:     %.loc6_65: bool = not %false [concrete = constants.%true]
 // CHECK:STDOUT:     %int_3: Core.IntLiteral = int_value 3 [concrete = constants.%int_3]
@@ -213,8 +214,9 @@ impl () as I where .X = {.a = true, .b = (1, 2)} and .X = {.a = false, .b = (3,
 // CHECK:STDOUT:     %struct.loc6_95: %struct_type.a.b.fe2 = struct_value (%.loc6_65, %.loc6_95.2) [concrete = constants.%struct]
 // CHECK:STDOUT:     %.loc6_95.3: %struct_type.a.b.fe2 = converted %.loc6_95.1, %struct.loc6_95 [concrete = constants.%struct]
 // CHECK:STDOUT:     %.loc6_14: type = where_expr %.Self [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc6_20, %.loc6_48.3
-// CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc6_54, %.loc6_95.3
+// CHECK:STDOUT:       requirement_rewrite %impl.elem0.subst, %.loc6_95.3
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %I.impl_witness_table = impl_witness_table (%impl_witness_assoc_constant), @empty_tuple.type.as.I.impl [concrete]
@@ -367,6 +369,7 @@ impl () as I where .X = {.a = true, .b = (1, 2)} and .X = {.a = false, .b = (3,
 // CHECK:STDOUT:     %.Self.as_type.loc10_54: type = facet_access_type %.Self.ref.loc10_54 [symbolic_self = constants.%.Self.as_type.541]
 // CHECK:STDOUT:     %.loc10_54: type = converted %.Self.ref.loc10_54, %.Self.as_type.loc10_54 [symbolic_self = constants.%.Self.as_type.541]
 // CHECK:STDOUT:     %impl.elem0.loc10_54: %struct_type.a.b.fe2 = impl_witness_access constants.%I.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0.74b]
+// CHECK:STDOUT:     %impl.elem0.subst: %struct_type.a.b.fe2 = impl_witness_access_substituted %impl.elem0.loc10_54, %.loc10_48.3 [concrete = constants.%struct.682]
 // CHECK:STDOUT:     %false: bool = bool_literal false [concrete = constants.%false]
 // CHECK:STDOUT:     %int_3: Core.IntLiteral = int_value 3 [concrete = constants.%int_3.1ba]
 // CHECK:STDOUT:     %int_4: Core.IntLiteral = int_value 4 [concrete = constants.%int_4.0c1]
@@ -391,8 +394,9 @@ impl () as I where .X = {.a = true, .b = (1, 2)} and .X = {.a = false, .b = (3,
 // CHECK:STDOUT:     %struct.loc10_83: %struct_type.a.b.fe2 = struct_value (%false, %.loc10_83.2) [concrete = constants.%struct.68c]
 // CHECK:STDOUT:     %.loc10_83.3: %struct_type.a.b.fe2 = converted %.loc10_83.1, %struct.loc10_83 [concrete = constants.%struct.68c]
 // CHECK:STDOUT:     %.loc10_14: type = where_expr %.Self [concrete = <error>] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc10_20, %.loc10_48.3
-// CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc10_54, %.loc10_83.3
+// CHECK:STDOUT:       requirement_rewrite %impl.elem0.subst, %.loc10_83.3
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
@@ -360,6 +360,7 @@ impl CD as IF where .F = 0 {
 // CHECK:STDOUT:     %.loc5_26.1: %empty_struct_type = struct_literal ()
 // CHECK:STDOUT:     %.loc5_26.2: type = converted %.loc5_26.1, constants.%empty_struct_type [concrete = constants.%empty_struct_type]
 // CHECK:STDOUT:     %.loc5_14: type = where_expr %.Self [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %.loc5_26.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -448,6 +449,7 @@ impl CD as IF where .F = 0 {
 // CHECK:STDOUT:     %.loc5_26.1: %empty_struct_type = struct_literal ()
 // CHECK:STDOUT:     %.loc5_26.2: type = converted %.loc5_26.1, constants.%empty_struct_type [concrete = constants.%empty_struct_type]
 // CHECK:STDOUT:     %.loc5_14: type = where_expr %.Self.2 [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc5, %.loc5_26.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -466,6 +468,7 @@ impl CD as IF where .F = 0 {
 // CHECK:STDOUT:     %.loc6_26.1: %empty_struct_type = struct_literal ()
 // CHECK:STDOUT:     %.loc6_26.2: type = converted %.loc6_26.1, constants.%empty_struct_type [concrete = constants.%empty_struct_type]
 // CHECK:STDOUT:     %.loc6_14: type = where_expr %.Self.1 [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc6, %.loc6_26.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -558,6 +561,7 @@ impl CD as IF where .F = 0 {
 // CHECK:STDOUT:     %.loc10_26.1: %empty_struct_type = struct_literal ()
 // CHECK:STDOUT:     %.loc10_26.2: type = converted %.loc10_26.1, constants.%empty_struct_type [concrete = constants.%empty_struct_type]
 // CHECK:STDOUT:     %.loc10_14: type = where_expr %.Self [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %.loc10_26.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -651,6 +655,7 @@ impl CD as IF where .F = 0 {
 // CHECK:STDOUT:     %.loc9_26.1: %empty_struct_type = struct_literal ()
 // CHECK:STDOUT:     %.loc9_26.2: type = converted %.loc9_26.1, constants.%empty_struct_type [concrete = constants.%empty_struct_type]
 // CHECK:STDOUT:     %.loc9_14: type = where_expr %.Self [concrete = constants.%I_where.type.8c8] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %.loc9_26.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -669,6 +674,7 @@ impl CD as IF where .F = 0 {
 // CHECK:STDOUT:     %.loc10_26.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:     %.loc10_26.2: type = converted %.loc10_26.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:     %.loc10_14: type = where_expr %.Self [concrete = constants.%I_where.type.cba] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %.loc10_26.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -790,6 +796,7 @@ impl CD as IF where .F = 0 {
 // CHECK:STDOUT:     %impl.elem2: type = impl_witness_access constants.%I3.lookup_impl_witness, element2 [symbolic_self = constants.%impl.elem2]
 // CHECK:STDOUT:     %BAD2.ref: <error> = name_ref BAD2, <error> [concrete = <error>]
 // CHECK:STDOUT:     %.loc17_15: type = where_expr %.Self [concrete = <error>] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I3.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, <error>
 // CHECK:STDOUT:       requirement_rewrite %impl.elem1, %struct_type.a
 // CHECK:STDOUT:       requirement_rewrite %impl.elem2, <error>
@@ -820,6 +827,7 @@ impl CD as IF where .F = 0 {
 // CHECK:STDOUT:     %impl.elem2: type = impl_witness_access constants.%I3.lookup_impl_witness, element2 [symbolic_self = constants.%impl.elem2]
 // CHECK:STDOUT:     %BAD4.ref: <error> = name_ref BAD4, <error> [concrete = <error>]
 // CHECK:STDOUT:     %.loc27_15: type = where_expr %.Self [concrete = <error>] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I3.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %struct_type.b
 // CHECK:STDOUT:       requirement_rewrite %impl.elem1, <error>
 // CHECK:STDOUT:       requirement_rewrite %impl.elem2, <error>
@@ -928,6 +936,7 @@ impl CD as IF where .F = 0 {
 // CHECK:STDOUT:     %.loc5_26.1: %empty_struct_type = struct_literal ()
 // CHECK:STDOUT:     %.loc5_26.2: type = converted %.loc5_26.1, constants.%empty_struct_type [concrete = constants.%empty_struct_type]
 // CHECK:STDOUT:     %.loc5_14: type = where_expr %.Self [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %.loc5_26.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -1027,11 +1036,13 @@ impl CD as IF where .F = 0 {
 // CHECK:STDOUT:     %.Self.as_type.loc10_32: type = facet_access_type %.Self.ref.loc10_32 [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:     %.loc10_32: type = converted %.Self.ref.loc10_32, %.Self.as_type.loc10_32 [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:     %impl.elem0.loc10_32: type = impl_witness_access constants.%I.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
+// CHECK:STDOUT:     %impl.elem0.subst: type = impl_witness_access_substituted %impl.elem0.loc10_32, %.loc10_26.2 [concrete = constants.%empty_struct_type]
 // CHECK:STDOUT:     %.loc10_38.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:     %.loc10_38.2: type = converted %.loc10_38.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:     %.loc10_14: type = where_expr %.Self [concrete = <error>] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc10_20, %.loc10_26.2
-// CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc10_32, %.loc10_38.2
+// CHECK:STDOUT:       requirement_rewrite %impl.elem0.subst, %.loc10_38.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
@@ -1119,11 +1130,13 @@ impl CD as IF where .F = 0 {
 // CHECK:STDOUT:     %.Self.as_type.loc10_34: type = facet_access_type %.Self.ref.loc10_34 [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:     %.loc10_34: type = converted %.Self.ref.loc10_34, %.Self.as_type.loc10_34 [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:     %impl.elem0.loc10_34: type = impl_witness_access constants.%I.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
+// CHECK:STDOUT:     %impl.elem0.subst: type = impl_witness_access_substituted %impl.elem0.loc10_34, <error> [concrete = <error>]
 // CHECK:STDOUT:     %.loc10_40.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:     %.loc10_40.2: type = converted %.loc10_40.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:     %.loc10_14: type = where_expr %.Self [concrete = <error>] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc10_20, <error>
-// CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc10_34, %.loc10_40.2
+// CHECK:STDOUT:       requirement_rewrite %impl.elem0.subst, %.loc10_40.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
@@ -1211,10 +1224,12 @@ impl CD as IF where .F = 0 {
 // CHECK:STDOUT:     %.Self.as_type.loc10_32: type = facet_access_type %.Self.ref.loc10_32 [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:     %.loc10_32: type = converted %.Self.ref.loc10_32, %.Self.as_type.loc10_32 [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:     %impl.elem0.loc10_32: type = impl_witness_access constants.%I.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
+// CHECK:STDOUT:     %impl.elem0.subst: type = impl_witness_access_substituted %impl.elem0.loc10_32, %.loc10_26.2 [concrete = constants.%empty_struct_type]
 // CHECK:STDOUT:     %BAD6.ref: <error> = name_ref BAD6, <error> [concrete = <error>]
 // CHECK:STDOUT:     %.loc10_14: type = where_expr %.Self [concrete = <error>] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc10_20, %.loc10_26.2
-// CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc10_32, <error>
+// CHECK:STDOUT:       requirement_rewrite %impl.elem0.subst, <error>
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
@@ -1302,10 +1317,12 @@ impl CD as IF where .F = 0 {
 // CHECK:STDOUT:     %.Self.as_type.loc14_34: type = facet_access_type %.Self.ref.loc14_34 [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:     %.loc14_34: type = converted %.Self.ref.loc14_34, %.Self.as_type.loc14_34 [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:     %impl.elem0.loc14_34: type = impl_witness_access constants.%I.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
+// CHECK:STDOUT:     %impl.elem0.subst: type = impl_witness_access_substituted %impl.elem0.loc14_34, <error> [concrete = <error>]
 // CHECK:STDOUT:     %BAD8.ref: <error> = name_ref BAD8, <error> [concrete = <error>]
 // CHECK:STDOUT:     %.loc14_14: type = where_expr %.Self [concrete = <error>] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc14_20, <error>
-// CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc14_34, <error>
+// CHECK:STDOUT:       requirement_rewrite %impl.elem0.subst, <error>
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
@@ -1394,11 +1411,13 @@ impl CD as IF where .F = 0 {
 // CHECK:STDOUT:     %.Self.as_type.loc6_32: type = facet_access_type %.Self.ref.loc6_32 [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:     %.loc6_32: type = converted %.Self.ref.loc6_32, %.Self.as_type.loc6_32 [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:     %impl.elem0.loc6_32: type = impl_witness_access constants.%I.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
+// CHECK:STDOUT:     %impl.elem0.subst: type = impl_witness_access_substituted %impl.elem0.loc6_32, %.loc6_26.2 [concrete = constants.%empty_struct_type]
 // CHECK:STDOUT:     %.loc6_38.1: %empty_struct_type = struct_literal ()
 // CHECK:STDOUT:     %.loc6_38.2: type = converted %.loc6_38.1, constants.%empty_struct_type [concrete = constants.%empty_struct_type]
 // CHECK:STDOUT:     %.loc6_14: type = where_expr %.Self [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc6_20, %.loc6_26.2
-// CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc6_32, %.loc6_38.2
+// CHECK:STDOUT:       requirement_rewrite %impl.elem0.subst, %.loc6_38.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %I.impl_witness_table = impl_witness_table (%impl_witness_assoc_constant), @CB.as.I.impl [concrete]
@@ -1493,6 +1512,7 @@ impl CD as IF where .F = 0 {
 // CHECK:STDOUT:     %struct: %struct_type.a.225 = struct_value (%.loc6_39.2) [concrete = constants.%struct]
 // CHECK:STDOUT:     %.loc6_39.3: %struct_type.a.225 = converted %.loc6_39.1, %struct [concrete = constants.%struct]
 // CHECK:STDOUT:     %.loc6_20: type = where_expr %.Self [concrete = constants.%NonType_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%NonType.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %.loc6_39.3
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -1617,6 +1637,7 @@ impl CD as IF where .F = 0 {
 // CHECK:STDOUT:     %impl.elem0: %.c5b = impl_witness_access constants.%IF.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
 // CHECK:STDOUT:     %int_0: Core.IntLiteral = int_value 0 [concrete = constants.%int_0]
 // CHECK:STDOUT:     %.loc10_15: type = where_expr %.Self [concrete = constants.%IF_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%IF.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %int_0
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -197,6 +197,7 @@ fn F() {
 // CHECK:STDOUT:     %.loc58_35.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:     %.loc58_35.2: type = converted %.loc58_35.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:     %.loc58_23: type = where_expr %.Self [concrete = constants.%Y_where.type.8eb] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%Y.type.080
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %.loc58_35.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -290,6 +291,7 @@ fn F() {
 // CHECK:STDOUT:         %.loc54_26.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:         %.loc54_26.2: type = converted %.loc54_26.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:         %.loc54_14.2: type = where_expr %.Self.2 [symbolic = %Y_where.type (constants.%Y_where.type.324)] {
+// CHECK:STDOUT:           requirement_base_facet_type constants.%Y.type.49b
 // CHECK:STDOUT:           requirement_rewrite %impl.elem0.loc54_20.2, %.loc54_26.2
 // CHECK:STDOUT:         }
 // CHECK:STDOUT:       }
@@ -699,6 +701,7 @@ fn F() {
 // CHECK:STDOUT:         %.loc11_26.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:         %.loc11_26.2: type = converted %.loc11_26.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:         %.loc11_14.2: type = where_expr %.Self.2 [symbolic = %Y_where.type (constants.%Y_where.type.fee)] {
+// CHECK:STDOUT:           requirement_base_facet_type constants.%Y.type.5e4
 // CHECK:STDOUT:           requirement_rewrite %impl.elem0.loc11_20.2, %.loc11_26.2
 // CHECK:STDOUT:         }
 // CHECK:STDOUT:       }
@@ -720,6 +723,7 @@ fn F() {
 // CHECK:STDOUT:       %.loc14_27.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:       %.loc14_27.2: type = converted %.loc14_27.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:       %.loc14_15: type = where_expr %.Self.1 [symbolic = %Y_where.type (constants.%Y_where.type.fee)] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%Y.type.5e4
 // CHECK:STDOUT:         requirement_rewrite %impl.elem0.loc14_21.1, %.loc14_27.2
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -196,6 +196,7 @@ fn F[T:! Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT:     %.loc9_56.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:     %.loc9_56.2: type = converted %.loc9_56.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:     %.loc9_44: type = where_expr %.Self.1 [symbolic = %Z_where.type (constants.%Z_where.type.80d)] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%Z.type.8e9
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc9_50.1, %.loc9_56.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %T.loc9_14.1: type = bind_symbolic_name T, 0 [symbolic = %T.loc9_14.2 (constants.%T.8b3)]
@@ -220,6 +221,7 @@ fn F[T:! Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT:     %impl.elem0: type = impl_witness_access constants.%Z.lookup_impl_witness.9cc, element0 [symbolic_self = constants.%impl.elem0.e29]
 // CHECK:STDOUT:     %T.ref.loc11_51: type = name_ref T, %T.loc11_20.1 [symbolic = %T.loc11_20.2 (constants.%T.8b3)]
 // CHECK:STDOUT:     %.loc11_40: type = where_expr %.Self [symbolic = %Z_where.type (constants.%Z_where.type.692)] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%Z.type.049
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %T.ref.loc11_51
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %T.loc11_20.1: type = bind_symbolic_name T, 0 [symbolic = %T.loc11_20.2 (constants.%T.8b3)]
@@ -563,6 +565,7 @@ fn F[T:! Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT:     %.loc10_56.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:     %.loc10_56.2: type = converted %.loc10_56.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:     %.loc10_44: type = where_expr %.Self.1 [symbolic = %Z_where.type (constants.%Z_where.type.80d)] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%Z.type.8e9
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc10_50.1, %.loc10_56.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %T.loc10_14.1: type = bind_symbolic_name T, 0 [symbolic = %T.loc10_14.2 (constants.%T.8b3)]
@@ -587,6 +590,7 @@ fn F[T:! Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT:     %impl.elem0: type = impl_witness_access constants.%Z.lookup_impl_witness.9cc, element0 [symbolic_self = constants.%impl.elem0.e29]
 // CHECK:STDOUT:     %T.ref.loc12_45: type = name_ref T, %T.loc12_14.1 [symbolic = %T.loc12_14.2 (constants.%T.8b3)]
 // CHECK:STDOUT:     %.loc12_34: type = where_expr %.Self [symbolic = %Z_where.type (constants.%Z_where.type.692)] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%Z.type.049
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %T.ref.loc12_45
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %T.loc12_14.1: type = bind_symbolic_name T, 0 [symbolic = %T.loc12_14.2 (constants.%T.8b3)]
@@ -876,6 +880,7 @@ fn F[T:! Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT:     %U.ref.loc7_53: type = name_ref U, %U.loc7_20.1 [symbolic = %U.loc7_20.2 (constants.%U)]
 // CHECK:STDOUT:     %ptr.loc7_54.1: type = ptr_type %U.ref.loc7_53 [symbolic = %ptr.loc7_54.2 (constants.%ptr.79f131.1)]
 // CHECK:STDOUT:     %.loc7_39: type = where_expr %.Self [symbolic = %Ptr_where.type (constants.%Ptr_where.type.bd48cc.1)] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%Ptr.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %ptr.loc7_54.1
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %U.loc7_20.1: type = bind_symbolic_name U, 0 [symbolic = %U.loc7_20.2 (constants.%U)]
@@ -1053,6 +1058,7 @@ fn F[T:! Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT:     %U.ref.loc7_53: type = name_ref U, %U.loc7_20.1 [symbolic = %U.loc7_20.2 (constants.%U)]
 // CHECK:STDOUT:     %ptr.loc7_54.1: type = ptr_type %U.ref.loc7_53 [symbolic = %ptr.loc7_54.2 (constants.%ptr.79f)]
 // CHECK:STDOUT:     %.loc7_39: type = where_expr %.Self [symbolic = %Ptr_where.type (constants.%Ptr_where.type.bd4)] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%Ptr.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %ptr.loc7_54.1
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %U.loc7_20.1: type = bind_symbolic_name U, 0 [symbolic = %U.loc7_20.2 (constants.%U)]
@@ -1236,6 +1242,7 @@ fn F[T:! Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT:     %U.ref.loc7_53: type = name_ref U, %U.loc7_20.1 [symbolic = %U.loc7_20.2 (constants.%U)]
 // CHECK:STDOUT:     %ptr.loc7_54.1: type = ptr_type %U.ref.loc7_53 [symbolic = %ptr.loc7_54.2 (constants.%ptr.79f)]
 // CHECK:STDOUT:     %.loc7_39: type = where_expr %.Self [symbolic = %Ptr_where.type (constants.%Ptr_where.type.bd4)] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%Ptr.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %ptr.loc7_54.1
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %U.loc7_20.1: type = bind_symbolic_name U, 0 [symbolic = %U.loc7_20.2 (constants.%U)]
@@ -409,6 +409,7 @@ fn F() {
 // CHECK:STDOUT:     %int_32: Core.IntLiteral = int_value 32 [concrete = constants.%int_32]
 // CHECK:STDOUT:     %i32: type = class_type @Int, @Int(constants.%int_32) [concrete = constants.%i32]
 // CHECK:STDOUT:     %.loc8_14: type = where_expr %.Self [concrete = constants.%J_where.type.b64] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%J.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %i32
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -444,6 +445,7 @@ fn F() {
 // CHECK:STDOUT:     %impl.elem0: type = impl_witness_access constants.%J.lookup_impl_witness.25c, element0 [symbolic_self = constants.%impl.elem0.83f]
 // CHECK:STDOUT:     %C.ref.loc21_24: type = name_ref C, file.%C.decl [concrete = constants.%C]
 // CHECK:STDOUT:     %.loc21_13: type = where_expr %.Self [concrete = constants.%J_where.type.0bc] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%J.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %C.ref.loc21_24
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -782,6 +784,7 @@ fn F() {
 // CHECK:STDOUT:     %int_32: Core.IntLiteral = int_value 32 [concrete = constants.%int_32]
 // CHECK:STDOUT:     %i32: type = class_type @Int, @Int(constants.%int_32) [concrete = constants.%i32]
 // CHECK:STDOUT:     %.loc10_13: type = where_expr %.Self [concrete = constants.%J_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%J.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %i32
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -1298,6 +1301,7 @@ fn F() {
 // CHECK:STDOUT:     %int_32: Core.IntLiteral = int_value 32 [concrete = constants.%int_32]
 // CHECK:STDOUT:     %i32: type = class_type @Int, @Int(constants.%int_32) [concrete = constants.%i32]
 // CHECK:STDOUT:     %.loc10_20: type = where_expr %.Self [concrete = constants.%J_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%J.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %i32
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -2226,6 +2230,7 @@ fn F() {
 // CHECK:STDOUT:       %int_32.loc8_37: Core.IntLiteral = int_value 32 [concrete = constants.%int_32]
 // CHECK:STDOUT:       %i32.loc8_37: type = class_type @Int, @Int(constants.%int_32) [concrete = constants.%i32]
 // CHECK:STDOUT:       %.loc8_26.2: type = where_expr %.Self [concrete = constants.%J_where.type] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%J.type
 // CHECK:STDOUT:         requirement_rewrite %impl.elem0.loc8, %i32.loc8_37
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -2518,6 +2523,7 @@ fn F() {
 // CHECK:STDOUT:     %int_32: Core.IntLiteral = int_value 32 [concrete = constants.%int_32]
 // CHECK:STDOUT:     %i32: type = class_type @Int, @Int(constants.%int_32) [concrete = constants.%i32]
 // CHECK:STDOUT:     %.loc9_20: type = where_expr %.Self [concrete = constants.%J_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%J.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %i32
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -2660,6 +2666,7 @@ fn F() {
 // CHECK:STDOUT:     %.loc22_28.1: %empty_struct_type = struct_literal ()
 // CHECK:STDOUT:     %.loc22_28.2: type = converted %.loc22_28.1, constants.%empty_struct_type [concrete = constants.%empty_struct_type]
 // CHECK:STDOUT:     %.loc22_15: type = where_expr %.Self [concrete = constants.%J2_where.type.9e1] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%J2.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %.loc22_28.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -2678,6 +2685,7 @@ fn F() {
 // CHECK:STDOUT:     %impl.elem0: type = impl_witness_access constants.%J2.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
 // CHECK:STDOUT:     %C2.ref.loc38_27: type = name_ref C2, file.%C2.decl [concrete = constants.%C2]
 // CHECK:STDOUT:     %.loc38_15: type = where_expr %.Self [concrete = constants.%J2_where.type.df9] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%J2.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %C2.ref.loc38_27
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -2965,6 +2973,7 @@ fn F() {
 // CHECK:STDOUT:     %.loc8_31.2: type = converted %.loc8_31.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:     %struct_type.a: type = struct_type {.a: %empty_tuple.type} [concrete = constants.%struct_type.a]
 // CHECK:STDOUT:     %.loc8_14: type = where_expr %.Self [concrete = constants.%K_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%K.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %struct_type.a
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -3172,6 +3181,7 @@ fn F() {
 // CHECK:STDOUT:     %struct: %struct_type.b.347 = struct_value (%.loc8_33.2) [concrete = constants.%struct]
 // CHECK:STDOUT:     %.loc8_33.3: %struct_type.b.347 = converted %.loc8_33.1, %struct [concrete = constants.%struct]
 // CHECK:STDOUT:     %.loc8_14: type = where_expr %.Self [concrete = constants.%M_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%M.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %.loc8_33.3
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -3341,6 +3351,7 @@ fn F() {
 // CHECK:STDOUT:     %struct: %struct_type.b.86f = struct_value (%.loc10_36.2) [concrete = constants.%struct.0f3]
 // CHECK:STDOUT:     %.loc10_36.3: %struct_type.b.86f = converted %.loc10_36.1, %struct [concrete = constants.%struct.0f3]
 // CHECK:STDOUT:     %.loc10_17: type = where_expr %.Self [concrete = constants.%M_where.type.d04] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%M.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %.loc10_36.3
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -3365,6 +3376,7 @@ fn F() {
 // CHECK:STDOUT:     %struct: %struct_type.b.86f = struct_value (%.loc16_36.2) [concrete = constants.%struct.c94]
 // CHECK:STDOUT:     %.loc16_36.3: %struct_type.b.86f = converted %.loc16_36.1, %struct [concrete = constants.%struct.c94]
 // CHECK:STDOUT:     %.loc16_17: type = where_expr %.Self [concrete = constants.%M_where.type.eda] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%M.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %.loc16_36.3
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -3675,6 +3687,7 @@ fn F() {
 // CHECK:STDOUT:     %.loc8_25.1: %i32 = value_of_initializer %Core.IntLiteral.as.ImplicitAs.impl.Convert.call [concrete = constants.%int_2.ef8]
 // CHECK:STDOUT:     %.loc8_25.2: %i32 = converted %int_2, %.loc8_25.1 [concrete = constants.%int_2.ef8]
 // CHECK:STDOUT:     %.loc8_14: type = where_expr %.Self [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc8_20, %.loc8_25.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
@@ -3909,6 +3922,7 @@ fn F() {
 // CHECK:STDOUT:     %T.ref.loc9_44: type = name_ref T, %T.loc9_14.1 [symbolic = %T.loc9_14.2 (constants.%T)]
 // CHECK:STDOUT:     %C.loc9_45.1: type = class_type @C, @C(constants.%T) [symbolic = %C.loc9_45.2 (constants.%C.f2e)]
 // CHECK:STDOUT:     %.loc9_31: type = where_expr %.Self [symbolic = %Z_where.type (constants.%Z_where.type.585)] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%Z.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %C.loc9_45.1
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %T.loc9_14.1: type = bind_symbolic_name T, 0 [symbolic = %T.loc9_14.2 (constants.%T)]
@@ -322,6 +322,7 @@ interface C {
 // CHECK:STDOUT:     %.loc11_43.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:     %.loc11_43.2: type = converted %.loc11_43.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:     %.loc11_30: type = where_expr %.Self [concrete = constants.%I2_where.type] {
+// CHECK:STDOUT:       requirement_base_facet_type constants.%I2.type
 // CHECK:STDOUT:       requirement_rewrite %impl.elem0, %.loc11_43.2
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %J2.ref: type = name_ref J2, file.%J2.decl.loc9 [concrete = constants.%J2.type]
@@ -73,6 +73,7 @@ let U: (type where .Self impls type).missing = {};
 // CHECK:STDOUT:     %.Self: type = bind_symbolic_name .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:     %.Self.ref: type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:     %.loc8: type = where_expr %.Self [concrete = constants.%type] {
+// CHECK:STDOUT:       requirement_base_facet_type type
 // CHECK:STDOUT:       requirement_impls %.Self.ref, type
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %missing.ref: <error> = name_ref missing, <error> [concrete = <error>]
@@ -212,6 +212,7 @@ fn F() {
 // CHECK:STDOUT:       %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:       %.loc7_18: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:       %.loc7_12.2: type = where_expr %.Self [concrete = constants.%I.type] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:         requirement_impls %.loc7_18, type
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -228,6 +229,7 @@ fn F() {
 // CHECK:STDOUT:       %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:       %.loc13_18: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:       %.loc13_12.2: type = where_expr %.Self [concrete = constants.%I.type] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:         requirement_impls %.loc13_18, %Type.ref
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -280,6 +282,7 @@ fn F() {
 // CHECK:STDOUT:       %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:       %.loc14_18: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:       %.loc14_12.2: type = where_expr %.Self [concrete = <error>] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:         requirement_impls %.loc14_18, <error>
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -337,6 +340,7 @@ fn F() {
 // CHECK:STDOUT:       %.Self.ref: %I.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self.258]
 // CHECK:STDOUT:       %.loc12_37: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:       %.loc12_21.2: type = where_expr %.Self [concrete = constants.%I_where.type.cad] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:         requirement_equivalent %.Self.ref, %.loc12_37
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -353,6 +357,7 @@ fn F() {
 // CHECK:STDOUT:       %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.as_type.78d]
 // CHECK:STDOUT:       %.loc14_22: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.as_type.78d]
 // CHECK:STDOUT:       %.loc14_16.2: type = where_expr %.Self [concrete = constants.%J_where.type] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%J.type
 // CHECK:STDOUT:         requirement_impls %.loc14_22, %I.ref
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -375,6 +380,7 @@ fn F() {
 // CHECK:STDOUT:       %impl.elem0: type = impl_witness_access constants.%I.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
 // CHECK:STDOUT:       %.loc16_50: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:       %.loc16_14.2: type = where_expr %.Self [concrete = constants.%I_where.type.427] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:         requirement_impls %.loc16_20, %J.ref
 // CHECK:STDOUT:         requirement_equivalent %impl.elem0, %.loc16_50
 // CHECK:STDOUT:       }
@@ -452,6 +458,7 @@ fn F() {
 // CHECK:STDOUT:       %as_type: type = facet_access_type %impl.elem0 [symbolic_self = constants.%as_type]
 // CHECK:STDOUT:       %.loc12_36.2: type = converted %impl.elem0, %as_type [symbolic_self = constants.%as_type]
 // CHECK:STDOUT:       %.loc12_30.2: type = where_expr %.Self [concrete = constants.%K_where.type] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%K.type
 // CHECK:STDOUT:         requirement_impls %.loc12_36.2, %M.ref
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -489,6 +496,7 @@ fn F() {
 // CHECK:STDOUT:       %.Self.ref: type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %I.ref: <error> = name_ref I, <error> [concrete = <error>]
 // CHECK:STDOUT:       %.loc9_23.2: type = where_expr %.Self [concrete = <error>] {
+// CHECK:STDOUT:         requirement_base_facet_type type
 // CHECK:STDOUT:         requirement_impls %.Self.ref, <error>
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -173,6 +173,7 @@ fn G(T:! type where C(()) impls I(.Self)) {}
 // CHECK:STDOUT:       %.Self.ref: %I.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self.258]
 // CHECK:STDOUT:       %.loc9_37: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:       %.loc9_21.2: type = where_expr %.Self [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:         requirement_equivalent %.Self.ref, %.loc9_37
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -191,6 +192,7 @@ fn G(T:! type where C(()) impls I(.Self)) {}
 // CHECK:STDOUT:       %impl.elem0: type = impl_witness_access constants.%I.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
 // CHECK:STDOUT:       %.loc11_41: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:       %.loc11_23.2: type = where_expr %.Self [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:         requirement_equivalent %impl.elem0, %.loc11_41
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -204,6 +206,7 @@ fn G(T:! type where C(()) impls I(.Self)) {}
 // CHECK:STDOUT:       %.Self.ref: type = name_ref .Self, %.Self [symbolic_self = constants.%.Self.644]
 // CHECK:STDOUT:       %I.ref: type = name_ref I, file.%I.decl [concrete = constants.%I.type]
 // CHECK:STDOUT:       %.loc13_27.2: type = where_expr %.Self [concrete = constants.%type_where] {
+// CHECK:STDOUT:         requirement_base_facet_type type
 // CHECK:STDOUT:         requirement_impls %.Self.ref, %I.ref
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -89,6 +89,7 @@ fn G(U: Empty(i32) where .A = i32*) {
 // CHECK:STDOUT:       %T.ref.loc21_39: type = name_ref T, %T.loc21_6.2 [symbolic = %T.loc21_6.1 (constants.%T)]
 // CHECK:STDOUT:       %ptr.loc21_40.2: type = ptr_type %T.ref.loc21_39 [symbolic = %ptr.loc21_40.1 (constants.%ptr.79f)]
 // CHECK:STDOUT:       %.loc21_28.2: type = where_expr %.Self.2 [symbolic = %Empty_where.type (constants.%Empty_where.type.b73)] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%Empty.type.3e5fde.2
 // CHECK:STDOUT:         requirement_rewrite %impl.elem0.loc21_34.2, %ptr.loc21_40.2
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -133,7 +133,7 @@ fn Calls() {
  // CHECK:STDERR:
  Equal(bool);

-  // CHECK:STDERR: fail_import_rewrites.carbon:[[@LINE+8]]:3: error: cannot convert type `i32` into type implementing `A where .(A.B) = bool and .(A.C) = ()` [ConversionFailureTypeToFacet]
+  // CHECK:STDERR: fail_import_rewrites.carbon:[[@LINE+8]]:3: error: cannot convert type `i32` into type implementing `A where .(A.C) = () and .(A.B) = bool` [ConversionFailureTypeToFacet]
  // CHECK:STDERR:   NestedRewrite(i32);
  // CHECK:STDERR:   ^~~~~~~~~~~~~~~~~~
  // CHECK:STDERR: fail_import_rewrites.carbon:[[@LINE-17]]:1: in import [InImport]
@@ -255,6 +255,7 @@ let K: (E where .F = .Self.G) = bool;
 // CHECK:STDOUT:       %.loc9_28.1: %empty_struct_type = struct_literal ()
 // CHECK:STDOUT:       %.loc9_28.2: type = converted %.loc9_28.1, constants.%empty_struct_type [concrete = constants.%empty_struct_type]
 // CHECK:STDOUT:       %.loc9_16.2: type = where_expr %.Self [concrete = constants.%N_where.type] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%N.type
 // CHECK:STDOUT:         requirement_rewrite %impl.elem0, %.loc9_28.2
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -279,21 +280,18 @@ let K: (E where .F = .Self.G) = bool;
 // CHECK:STDOUT:   %A.assoc_type: type = assoc_entity_type @A [concrete]
 // CHECK:STDOUT:   %assoc0: %A.assoc_type = assoc_entity element0, @A.%B [concrete]
 // CHECK:STDOUT:   %assoc1: %A.assoc_type = assoc_entity element1, @A.%C [concrete]
-// CHECK:STDOUT:   %.Self.3ca: %A.type = bind_symbolic_name .Self [symbolic_self]
-// CHECK:STDOUT:   %.Self.as_type.adb: type = facet_access_type %.Self.3ca [symbolic_self]
-// CHECK:STDOUT:   %A.lookup_impl_witness.5ad: <witness> = lookup_impl_witness %.Self.3ca, @A [symbolic_self]
-// CHECK:STDOUT:   %impl.elem0: type = impl_witness_access %A.lookup_impl_witness.5ad, element0 [symbolic_self]
+// CHECK:STDOUT:   %.Self: %A.type = bind_symbolic_name .Self [symbolic_self]
+// CHECK:STDOUT:   %.Self.as_type: type = facet_access_type %.Self [symbolic_self]
+// CHECK:STDOUT:   %A.lookup_impl_witness: <witness> = lookup_impl_witness %.Self, @A [symbolic_self]
+// CHECK:STDOUT:   %impl.elem0: type = impl_witness_access %A.lookup_impl_witness, element0 [symbolic_self]
 // CHECK:STDOUT:   %Bool.type: type = fn_type @Bool [concrete]
 // CHECK:STDOUT:   %Bool: %Bool.type = struct_value () [concrete]
 // CHECK:STDOUT:   %A_where.type.ef7: type = facet_type <@A where %impl.elem0 = bool> [concrete]
-// CHECK:STDOUT:   %.Self.60a: %A_where.type.ef7 = bind_symbolic_name .Self [symbolic_self]
-// CHECK:STDOUT:   %.Self.as_type.e64: type = facet_access_type %.Self.60a [symbolic_self]
-// CHECK:STDOUT:   %A.lookup_impl_witness.138: <witness> = lookup_impl_witness %.Self.60a, @A [symbolic_self]
-// CHECK:STDOUT:   %impl.elem1: type = impl_witness_access %A.lookup_impl_witness.138, element1 [symbolic_self]
+// CHECK:STDOUT:   %impl.elem1: type = impl_witness_access %A.lookup_impl_witness, element1 [symbolic_self]
 // CHECK:STDOUT:   %empty_tuple.type: type = tuple_type () [concrete]
-// CHECK:STDOUT:   %A_where.type.2d0: type = facet_type <@A where %impl.elem0 = bool and %impl.elem1 = %empty_tuple.type> [concrete]
-// CHECK:STDOUT:   %D: %A_where.type.2d0 = bind_symbolic_name D, 0 [symbolic]
-// CHECK:STDOUT:   %pattern_type.24c: type = pattern_type %A_where.type.2d0 [concrete]
+// CHECK:STDOUT:   %A_where.type.7c3: type = facet_type <@A where %impl.elem0 = bool and %impl.elem1 = %empty_tuple.type> [concrete]
+// CHECK:STDOUT:   %D: %A_where.type.7c3 = bind_symbolic_name D, 0 [symbolic]
+// CHECK:STDOUT:   %pattern_type.e7b: type = pattern_type %A_where.type.7c3 [concrete]
 // CHECK:STDOUT:   %NestedRewrite.type: type = fn_type @NestedRewrite [concrete]
 // CHECK:STDOUT:   %NestedRewrite: %NestedRewrite.type = struct_value () [concrete]
 // CHECK:STDOUT: }
@@ -303,40 +301,42 @@ let K: (E where .F = .Self.G) = bool;
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
 // CHECK:STDOUT:   %NestedRewrite.decl: %NestedRewrite.type = fn_decl @NestedRewrite [concrete = constants.%NestedRewrite] {
-// CHECK:STDOUT:     %D.patt: %pattern_type.24c = symbolic_binding_pattern D, 0 [concrete]
+// CHECK:STDOUT:     %D.patt: %pattern_type.e7b = symbolic_binding_pattern D, 0 [concrete]
 // CHECK:STDOUT:   } {
-// CHECK:STDOUT:     %.loc10_42.1: type = splice_block %.loc10_42.2 [concrete = constants.%A_where.type.2d0] {
+// CHECK:STDOUT:     %.loc10_42.1: type = splice_block %.loc10_42.2 [concrete = constants.%A_where.type.7c3] {
 // CHECK:STDOUT:       %A.ref: type = name_ref A, file.%A.decl [concrete = constants.%A.type]
 // CHECK:STDOUT:       <elided>
-// CHECK:STDOUT:       %.Self.ref.loc10_31: %A.type = name_ref .Self, %.Self.1 [symbolic_self = constants.%.Self.3ca]
+// CHECK:STDOUT:       %.Self.ref.loc10_31: %A.type = name_ref .Self, %.Self.1 [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %B.ref: %A.assoc_type = name_ref B, @B.%assoc0 [concrete = constants.%assoc0]
-// CHECK:STDOUT:       %.Self.as_type.loc10_31: type = facet_access_type %.Self.ref.loc10_31 [symbolic_self = constants.%.Self.as_type.adb]
-// CHECK:STDOUT:       %.loc10_31: type = converted %.Self.ref.loc10_31, %.Self.as_type.loc10_31 [symbolic_self = constants.%.Self.as_type.adb]
-// CHECK:STDOUT:       %impl.elem0: type = impl_witness_access constants.%A.lookup_impl_witness.5ad, element0 [symbolic_self = constants.%impl.elem0]
+// CHECK:STDOUT:       %.Self.as_type.loc10_31: type = facet_access_type %.Self.ref.loc10_31 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:       %.loc10_31: type = converted %.Self.ref.loc10_31, %.Self.as_type.loc10_31 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:       %impl.elem0: type = impl_witness_access constants.%A.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
 // CHECK:STDOUT:       %Bool.call: init type = call constants.%Bool() [concrete = bool]
 // CHECK:STDOUT:       %.loc10_36.1: type = value_of_initializer %Bool.call [concrete = bool]
 // CHECK:STDOUT:       %.loc10_36.2: type = converted %Bool.call, %.loc10_36.1 [concrete = bool]
 // CHECK:STDOUT:       %.loc10_25: type = where_expr %.Self.1 [concrete = constants.%A_where.type.ef7] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%A.type
 // CHECK:STDOUT:         requirement_rewrite %impl.elem0, %.loc10_36.2
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:       <elided>
-// CHECK:STDOUT:       %.Self.ref.loc10_48: %A_where.type.ef7 = name_ref .Self, %.Self.2 [symbolic_self = constants.%.Self.60a]
+// CHECK:STDOUT:       %.Self.ref.loc10_48: %A.type = name_ref .Self, %.Self.2 [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %C.ref: %A.assoc_type = name_ref C, @C.%assoc1 [concrete = constants.%assoc1]
-// CHECK:STDOUT:       %.Self.as_type.loc10_48: type = facet_access_type %.Self.ref.loc10_48 [symbolic_self = constants.%.Self.as_type.e64]
-// CHECK:STDOUT:       %.loc10_48: type = converted %.Self.ref.loc10_48, %.Self.as_type.loc10_48 [symbolic_self = constants.%.Self.as_type.e64]
-// CHECK:STDOUT:       %impl.elem1: type = impl_witness_access constants.%A.lookup_impl_witness.138, element1 [symbolic_self = constants.%impl.elem1]
+// CHECK:STDOUT:       %.Self.as_type.loc10_48: type = facet_access_type %.Self.ref.loc10_48 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:       %.loc10_48: type = converted %.Self.ref.loc10_48, %.Self.as_type.loc10_48 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:       %impl.elem1: type = impl_witness_access constants.%A.lookup_impl_witness, element1 [symbolic_self = constants.%impl.elem1]
 // CHECK:STDOUT:       %.loc10_54.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:       %.loc10_54.2: type = converted %.loc10_54.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
-// CHECK:STDOUT:       %.loc10_42.2: type = where_expr %.Self.2 [concrete = constants.%A_where.type.2d0] {
+// CHECK:STDOUT:       %.loc10_42.2: type = where_expr %.Self.2 [concrete = constants.%A_where.type.7c3] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%A_where.type.ef7
 // CHECK:STDOUT:         requirement_rewrite %impl.elem1, %.loc10_54.2
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
-// CHECK:STDOUT:     %D.loc10_18.2: %A_where.type.2d0 = bind_symbolic_name D, 0 [symbolic = %D.loc10_18.1 (constants.%D)]
+// CHECK:STDOUT:     %D.loc10_18.2: %A_where.type.7c3 = bind_symbolic_name D, 0 [symbolic = %D.loc10_18.1 (constants.%D)]
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: generic fn @NestedRewrite(%D.loc10_18.2: %A_where.type.2d0) {
-// CHECK:STDOUT:   %D.loc10_18.1: %A_where.type.2d0 = bind_symbolic_name D, 0 [symbolic = %D.loc10_18.1 (constants.%D)]
+// CHECK:STDOUT: generic fn @NestedRewrite(%D.loc10_18.2: %A_where.type.7c3) {
+// CHECK:STDOUT:   %D.loc10_18.1: %A_where.type.7c3 = bind_symbolic_name D, 0 [symbolic = %D.loc10_18.1 (constants.%D)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   fn();
 // CHECK:STDOUT: }
@@ -387,6 +387,7 @@ let K: (E where .F = .Self.G) = bool;
 // CHECK:STDOUT:       %int_32: Core.IntLiteral = int_value 32 [concrete = constants.%int_32]
 // CHECK:STDOUT:       %i32: type = class_type @Int, @Int(constants.%int_32) [concrete = constants.%i32]
 // CHECK:STDOUT:       %.loc9_21.2: type = where_expr %.Self [concrete = constants.%E_where.type] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%E.type
 // CHECK:STDOUT:         requirement_rewrite %impl.elem0, %i32
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -410,11 +411,13 @@ let K: (E where .F = .Self.G) = bool;
 // CHECK:STDOUT:       %.Self.as_type.loc11_45: type = facet_access_type %.Self.ref.loc11_45 [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:       %.loc11_45: type = converted %.Self.ref.loc11_45, %.Self.as_type.loc11_45 [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:       %impl.elem0.loc11_45: type = impl_witness_access constants.%E.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
+// CHECK:STDOUT:       %impl.elem0.subst: type = impl_witness_access_substituted %impl.elem0.loc11_45, %i32.loc11_37 [concrete = constants.%i32]
 // CHECK:STDOUT:       %int_32.loc11_50: Core.IntLiteral = int_value 32 [concrete = constants.%int_32]
 // CHECK:STDOUT:       %i32.loc11_50: type = class_type @Int, @Int(constants.%int_32) [concrete = constants.%i32]
 // CHECK:STDOUT:       %.loc11_26.2: type = where_expr %.Self [concrete = constants.%E_where.type] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%E.type
 // CHECK:STDOUT:         requirement_rewrite %impl.elem0.loc11_32, %i32.loc11_37
-// CHECK:STDOUT:         requirement_rewrite %impl.elem0.loc11_45, %i32.loc11_50
+// CHECK:STDOUT:         requirement_rewrite %impl.elem0.subst, %i32.loc11_50
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %H.loc11_20.2: %E_where.type = bind_symbolic_name H, 0 [symbolic = %H.loc11_20.1 (constants.%H)]
@@ -522,6 +525,7 @@ let K: (E where .F = .Self.G) = bool;
 // CHECK:STDOUT:       %.loc10_46.1: type = value_of_initializer %Bool.call [concrete = bool]
 // CHECK:STDOUT:       %.loc10_46.2: type = converted %Bool.call, %.loc10_46.1 [concrete = bool]
 // CHECK:STDOUT:       %.loc10_23.2: type = where_expr %.Self [concrete = constants.%J_where.type] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%J.type
 // CHECK:STDOUT:         requirement_rewrite %impl.elem0, %.loc10_35.2
 // CHECK:STDOUT:         requirement_rewrite %impl.elem1, %.loc10_46.2
 // CHECK:STDOUT:       }
@@ -550,6 +554,7 @@ let K: (E where .F = .Self.G) = bool;
 // CHECK:STDOUT:       %.loc12_45.1: %empty_tuple.type = tuple_literal ()
 // CHECK:STDOUT:       %.loc12_45.2: type = converted %.loc12_45.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:       %.loc12_19.2: type = where_expr %.Self [concrete = constants.%J_where.type] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%J.type
 // CHECK:STDOUT:         requirement_rewrite %impl.elem1, %.loc12_30.2
 // CHECK:STDOUT:         requirement_rewrite %impl.elem0, %.loc12_45.2
 // CHECK:STDOUT:       }
@@ -55,6 +55,7 @@ fn NotGenericF(U: I where .T == i32) {}
 // CHECK:STDOUT:       %int_32: Core.IntLiteral = int_value 32 [concrete = constants.%int_32]
 // CHECK:STDOUT:       %i32: type = class_type @Int, @Int(constants.%int_32) [concrete = constants.%i32]
 // CHECK:STDOUT:       %.loc17_21.2: type = where_expr %.Self [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:         requirement_base_facet_type constants.%I.type
 // CHECK:STDOUT:         requirement_equivalent %impl.elem0, %i32
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
@@ -7,6 +7,7 @@
 #include "toolchain/check/eval.h"
 #include "toolchain/check/facet_type.h"
 #include "toolchain/check/type_completion.h"
+#include "toolchain/sem_ir/facet_type_info.h"

 namespace Carbon::Check {

@@ -157,6 +158,12 @@ auto GetInterfaceType(Context& context, SemIR::InterfaceId interface_id,
      FacetTypeFromInterface(context, interface_id, specific_id).facet_type_id);
 }

+auto GetFacetType(Context& context, const SemIR::FacetTypeInfo& info)
+    -> SemIR::TypeId {
+  return GetTypeImpl<SemIR::FacetType>(context,
+                                       context.facet_types().Add(info));
+}
+
 auto GetPointerType(Context& context, SemIR::TypeInstId pointee_type_id)
    -> SemIR::TypeId {
  return GetTypeImpl<SemIR::PointerType>(context, pointee_type_id);
@@ -77,6 +77,10 @@ auto GetGenericInterfaceType(Context& context, SemIR::InterfaceId interface_id,
 auto GetInterfaceType(Context& context, SemIR::InterfaceId interface_id,
                      SemIR::SpecificId specific_id) -> SemIR::TypeId;

+// Gets the facet type for the given `info`.
+auto GetFacetType(Context& context, const SemIR::FacetTypeInfo& info)
+    -> SemIR::TypeId;
+
 // Returns a pointer type whose pointee type is `pointee_type_id`.
 auto GetPointerType(Context& context, SemIR::TypeInstId pointee_type_id)
    -> SemIR::TypeId;
@@ -35,6 +35,7 @@ auto GetExprCategory(const File& file, InstId inst_id) -> ExprCategory {
      case Namespace::Kind:
      case OutParamPattern::Kind:
      case RefParamPattern::Kind:
+      case RequirementBaseFacetType::Kind:
      case RequirementEquivalent::Kind:
      case RequirementImpls::Kind:
      case RequirementRewrite::Kind:
@@ -124,6 +125,7 @@ auto GetExprCategory(const File& file, InstId inst_id) -> ExprCategory {
      case LookupImplWitness::Kind:
      case ImplWitness::Kind:
      case ImplWitnessAccess::Kind:
+      case ImplWitnessAccessSubstituted::Kind:
      case ImplWitnessTable::Kind:
      case ImplWitnessTablePlaceholder::Kind:
      case ImportCppDecl::Kind:
@@ -76,6 +76,7 @@ CARBON_SEM_IR_INST_KIND(ImplDecl)
 CARBON_SEM_IR_INST_KIND(LookupImplWitness)
 CARBON_SEM_IR_INST_KIND(ImplWitness)
 CARBON_SEM_IR_INST_KIND(ImplWitnessAccess)
+CARBON_SEM_IR_INST_KIND(ImplWitnessAccessSubstituted)
 CARBON_SEM_IR_INST_KIND(ImplWitnessAssociatedConstant)
 CARBON_SEM_IR_INST_KIND(ImplWitnessTable)
 CARBON_SEM_IR_INST_KIND(ImplWitnessTablePlaceholder)
@@ -104,6 +105,7 @@ CARBON_SEM_IR_INST_KIND(RefParam)
 CARBON_SEM_IR_INST_KIND(RefParamPattern)
 CARBON_SEM_IR_INST_KIND(RefineTypeAction)
 CARBON_SEM_IR_INST_KIND(RequireCompleteType)
+CARBON_SEM_IR_INST_KIND(RequirementBaseFacetType)
 CARBON_SEM_IR_INST_KIND(RequirementEquivalent)
 CARBON_SEM_IR_INST_KIND(RequirementImpls)
 CARBON_SEM_IR_INST_KIND(RequirementRewrite)
@@ -895,6 +895,15 @@ auto InstNamer::NamingContext::NameInst() -> void {
      AddInstName(out.TakeStr());
      return;
    }
+    case CARBON_KIND(ImplWitnessAccessSubstituted inst): {
+      // TODO: Include information about the impl?
+      RawStringOstream out;
+      auto access = sem_ir().insts().GetAs<ImplWitnessAccess>(
+          inst.impl_witness_access_id);
+      out << "impl.elem" << access.index.index << ".subst";
+      AddInstName(out.TakeStr());
+      return;
+    }
    case ImplWitnessAssociatedConstant::Kind: {
      AddInstName("impl_witness_assoc_constant");
      return;
@@ -844,6 +844,26 @@ struct ImplWitnessAccess {
  ElementIndex index;
 };

+// A substituted value to use in place of an ImplWitnessAccess (which comes from
+// the RHS of a rewrite constraint in the same facet type), while preserving the
+// original reference to an associated constant as an ImplWitnessAccess. This
+// allows the substitution to occur on the LHS of rewrite constraints without
+// losing what is being rewritten by them.
+struct ImplWitnessAccessSubstituted {
+  static constexpr auto Kind =
+      InstKind::ImplWitnessAccessSubstituted.Define<Parse::NodeId>(
+          {.ir_name = "impl_witness_access_substituted",
+           .is_type = InstIsType::Maybe,
+           .constant_kind = InstConstantKind::SymbolicOnly,
+           .is_lowered = false});
+
+  TypeId type_id;
+  // The ImplWitnessAccess instruction that this was created from.
+  InstId impl_witness_access_id;
+  // The value instruction to use in place of the ImplWitnessAccess.
+  InstId value_id;
+};
+
 // An instruction that just points to an associated constant, which exists to
 // live inside the generic for an `impl` and be rewritten in the generic eval
 // block, unlike the instruction which it points to. This allows a symbolic
@@ -1273,7 +1293,29 @@ struct RequireCompleteType {
  TypeInstId complete_type_inst_id;
 };

-// An `expr == expr` clause in a `where` expression or `require` declaration.
+// A requirement that `.Self` implements a facet type, specified as the first
+// operand of a `where` expression. This is always the first requirement in a
+// requirement block for a `where` expression.
+//
+// Any constraints in the base facet type are available to other constraint
+// operands in the `where` expression, and also become a part of the resulting
+// facet type.
+struct RequirementBaseFacetType {
+  static constexpr auto Kind =
+      InstKind::RequirementBaseFacetType.Define<Parse::NodeId>(
+          {.ir_name = "requirement_base_facet_type",
+           .constant_kind = InstConstantKind::Never,
+           .is_lowered = false});
+
+  // No type since not an expression
+
+  // A FacetType, the TypeType singleton, or an ErrorInst.
+  TypeInstId base_type_inst_id;
+};
+
+// A requirement that two expressions evaluate to the same constant, as
+// specified by an `expr == expr` clause in a `where` expression or `require`
+// declaration.
 struct RequirementEquivalent {
  static constexpr auto Kind =
      InstKind::RequirementEquivalent.Define<Parse::RequirementEqualEqualId>(
@@ -1286,7 +1328,9 @@ struct RequirementEquivalent {
  InstId rhs_id;
 };

-// An `expr impls expr` clause in a `where` expression or `require` declaration.
+// A requirement that the LHS expression is a facet type that implements the
+// interface on the RHS and meets any constraints in the RHS, as specified by an
+// `expr impls expr` clause in a `where` expression or `require` declaration.
 struct RequirementImpls {
  static constexpr auto Kind =
      InstKind::RequirementImpls.Define<Parse::RequirementImplsId>(
@@ -1299,7 +1343,9 @@ struct RequirementImpls {
  InstId rhs_id;
 };

-// A `.M = expr` clause in a `where` expression or `require` declaration.
+// A requirement that assigns the expression on the RHS to the associated
+// constant named on the LHS, as specified by a `.M = expr` clause in a `where`
+// expression or `require` declaration.
 struct RequirementRewrite {
  static constexpr auto Kind =
      InstKind::RequirementRewrite.Define<Parse::RequirementEqualId>(