Build a generic scope around where expressions (#8062)

A `where` expression can have symbolic references to `.Self` inside it,
but those references do not represent symbolic instructions that should
be part of an enclosing generic eval block. They are internal details of
the facet type, and as such they are PeriodSelfSymbolic, not Symbolic.
The WhereExpr evaluation is careful to produce a Symbolic constant value
only if it has symbolic dependencies on the LHS of the `where`, which
avoids leaking the symbolic nature of `.Self` into he facet type's
constant value.

But until now, those PeriodSelfSymbolic insts could still leak into the
enclosing eval block if they ended up in an operand of a Call
expression. A compile-time Call expr evaluates to a TemplateSymbolic
phase constant if it's not concrete, which includes PeriodSelfSymbolic,
because we don't want to evaluate the Call expr until the `.Self` gets
replaced during identify. But that means the Call constant value, and
its operands including PeriodSelfSymbolic constants, all end up in the
eval block. We fix this by making Call evaluate to a PeriodSelfSymbolic
phase if its input phase is PeriodSelfSymbolic. This keeps the RHS of
the `where` expression self-contained. If the facet type is concrete,
then it doesn't add any instructions to the enclosing eval block (which
may not exist at all in a non-generic context). Regardless, when we
identify the facet type and replace `.Self`, the dependent Call
expression will be rebuilt as well and it will evaluate as appropriate.

We also enclose the `where` expression in its own generic scope. This
means that instructions which are not part of the facet type do not end
up in an eval block. They may be symbolic instructions, and they will
not get updated by a specific when it's applied the enclosing generic
anymore. But since they are not part of the facet type their
substitution is not required.

The new test had an incorrectly elided SpecificImplFunction instruction
in the resulting semir, as SubstPeriodSelf was using the location of the
input canonical instructions as the location for the results which
resulted in an instruction without a location. We fix that by using
`loc_id_` in the subst rebuild.

Formatting now saw the initialization of a value from an `eval fn` call
to a function in a witness table, so it needed to be taught to look
through ImplWitnessAssociatedConstant (which is what we find in the
witness table).

toolchain/check/call.cpp

@@ -195,23 +195,21 @@ static auto BuildCalleeSpecificFunction(
     // This is an associated function in an interface; the callee is the
     // specific function in the impl that corresponds to the specific function
     // we deduced.
-    callee_id =
-        GetOrAddInst(context, SemIR::LocId(generic_callee_id),
-                     SemIR::SpecificImplFunction{
-                         .type_id = GetSingletonType(
-                             context, SemIR::SpecificFunctionType::TypeInstId),
-                         .callee_id = generic_callee_id,
-                         .specific_id = callee_specific_id});
+    callee_id = GetOrAddInst<SemIR::SpecificImplFunction>(
+        context, SemIR::LocId(generic_callee_id),
+        {.type_id =
+             GetSingletonType(context, SemIR::SpecificFunctionType::TypeInstId),
+         .callee_id = generic_callee_id,
+         .specific_id = callee_specific_id});
   } else {
     // This is a regular generic function. The callee is the specific function
     // we deduced.
-    callee_id =
-        GetOrAddInst(context, SemIR::LocId(generic_callee_id),
-                     SemIR::SpecificFunction{
-                         .type_id = GetSingletonType(
-                             context, SemIR::SpecificFunctionType::TypeInstId),
-                         .callee_id = generic_callee_id,
-                         .specific_id = callee_specific_id});
+    callee_id = GetOrAddInst<SemIR::SpecificFunction>(
+        context, SemIR::LocId(generic_callee_id),
+        {.type_id =
+             GetSingletonType(context, SemIR::SpecificFunctionType::TypeInstId),
+         .callee_id = generic_callee_id,
+         .specific_id = callee_specific_id});
   }
 
   // Add the `self` argument back if there was one.

toolchain/check/eval.cpp

@@ -2922,11 +2922,14 @@ static auto MakeConstantForCall(EvalContext& eval_context,
   // Handle calls to `eval` and `musteval` functions.
   if (evaluation_mode != SemIR::Function::EvaluationMode::None) {
     // A non-concrete call to `eval` or `musteval` is a template symbolic
-    // constant, regardless of the phase of the arguments.
+    // constant, unless it is only dependent on `.Self`. Then preserve that so
+    // a Call on the RHS of a `where` does not change the phase of the whole
+    // facet type.
     if (phase != Phase::Concrete) {
       CARBON_CHECK(phase <= Phase::TemplateSymbolic);
-      return MakeConstantResult(eval_context.context(), call,
-                                Phase::TemplateSymbolic);
+      phase = phase == Phase::PeriodSelfSymbolic ? Phase::PeriodSelfSymbolic
+                                                 : Phase::TemplateSymbolic;
+      return MakeConstantResult(eval_context.context(), call, phase);
     }
 
     // TODO: Instead of performing the call immediately, add it to a work queue

toolchain/check/handle_where.cpp

@@ -209,6 +209,7 @@ auto HandleParseNode(Context& context, Parse::WhereOperandId node_id) -> bool {
     }
   }
 
+  StartGenericDecl(context);
   return true;
 }
 
@@ -608,6 +609,16 @@ auto HandleParseNode(Context& context, Parse::WhereExprId node_id) -> bool {
       context, where_loc, requirements_id);
   requirements_id = ThawPeriodSelfInRequirements(context, requirements_id);
 
+  // We make and discard a generic because we may have instructions inside which
+  // are only PeriodSelfDependent. These should not be part of any enclosing
+  // generic. A facet type is only symbolic if it depends on symbolic values
+  // from outside the facet type (which are Symbolic rather than
+  // PeriodSelfSymbolic). If the resulting facet type is Symbolic, the Symbolic
+  // instructions that it depends on (which are being discarded in the eval
+  // block here) will be added as dependent instructions of the facet type in
+  // the enclosing generic.
+  DiscardGenericDecl(context);
+
   AddInstAndPush<SemIR::WhereExpr>(
       context, node_id,
       {.type_id = type_id, .requirements_id = requirements_id});

toolchain/check/period_self.cpp

@@ -101,14 +101,14 @@ class SubstPeriodSelfCallbacks : public SubstInstCallbacks {
     return SubstOperandsSkipType;
   }
 
-  auto Rebuild(SemIR::InstId orig_inst_id, SemIR::Inst new_inst)
+  auto Rebuild(SemIR::InstId /*orig_inst_id*/, SemIR::Inst new_inst)
       -> SemIR::InstId override {
     if (rebuild_callback_) {
       if (auto inst_id = rebuild_callback_(new_inst); inst_id.has_value()) {
         return inst_id;
       }
     }
-    return RebuildNewInst(SemIR::LocId(orig_inst_id), new_inst);
+    return RebuildNewInst(loc_id_, new_inst);
   }
 
  private:

toolchain/check/testdata/facet/period_self.carbon

@@ -797,7 +797,7 @@ interface Z(T: type);
 // CHECK:STDERR:
 fn F(generic _: C(Z(.Self))) {}
 
-// --- fail_todo_period_self_in_generic_argument.carbon
+// --- fail_todo_period_self_in_interface_generic_argument.carbon
 library "[[@TEST_NAME]]";
 
 interface Z {
@@ -811,11 +811,37 @@ interface Y(T: type) {
   eval fn YF() -> T;
 }
 
-// TODO: We crash if this impl is not generic, as the call to `.YF()` produces a
-// symbolic-dependent instruction, but there's no generic eval block for it.
-// CHECK:STDERR: fail_todo_period_self_in_generic_argument.carbon:[[@LINE+2]]:60-64: error: cannot convert type `.(Y(Z where .(Z.Z1) = ()).YF)()` that implements `Z where .(Z.Z1) = ()` into type implementing `Z where .(Z.Z1) = ()` [ConversionFailureFacetToFacet]
+// CHECK:STDERR: fail_todo_period_self_in_interface_generic_argument.carbon:[[@LINE+2]]:44-48: error: cannot convert type `.(Y(Z where .(Z.Z1) = ()).YF)()` that implements `Z where .(Z.Z1) = ()` into type implementing `Z where .(Z.Z1) = ()` [ConversionFailureFacetToFacet]
 // CHECK:STDERR:
-impl forall [T: type] T as Y(Z where .Z1 = ()) where .Y1 = .YF() {}
+impl () as Y(Z where .Z1 = ()) where .Y1 = .YF() {}
+
+// --- period_self_in_function_generic_argument.carbon
+library "[[@TEST_NAME]]";
+
+interface Z {
+  let Z1: type;
+}
+interface Y {
+  eval fn Y1(generic T: type) -> type;
+}
+
+// This uses the generic binding `T` to form symbolic instructions
+// inside the `where` expression. It also contains `.Self`. We don't
+// propagate `.Self` dependencies in the `where` expression up to the
+// impl's eval block, but we do need to propagate this symbolic call
+// to `T.Y1`.
+//@dump-sem-ir-begin
+impl forall [T: Y] T as Z where .Z1 = T.Y1(.Self) {}
+//@dump-sem-ir-end
+
+impl () as Y {
+  eval fn Y1(generic _: type) -> type {
+    return Self;
+  }
+}
+fn F() {
+  () as (Z where .Z1 = ());
+}
 
 // CHECK:STDOUT: --- period_self_param.carbon
 // CHECK:STDOUT:
@@ -1117,3 +1143,172 @@ impl forall [T: type] T as Y(Z where .Z1 = ()) where .Y1 = .YF() {}
 // CHECK:STDOUT:   %T.as_type.loc12_54.1 => constants.%T.as_type
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
+// CHECK:STDOUT: --- period_self_in_function_generic_argument.carbon
+// CHECK:STDOUT:
+// CHECK:STDOUT: constants {
+// CHECK:STDOUT:   type: type = facet_type <type> [concrete]
+// CHECK:STDOUT:   %Z.type: type = facet_type <@Z> [concrete]
+// CHECK:STDOUT:   %Z.assoc_type: type = assoc_entity_type @Z [concrete]
+// CHECK:STDOUT:   %assoc0.3fa: %Z.assoc_type = assoc_entity element0, @Z.WithSelf.%Z1 [concrete]
+// CHECK:STDOUT:   %Y.type: type = facet_type <@Y> [concrete]
+// CHECK:STDOUT:   %.Self.frozen.e58: type = symbolic_binding .Self [symbolic_self]
+// CHECK:STDOUT:   %empty_tuple.type: type = tuple_type () [concrete]
+// CHECK:STDOUT:   %Y.assoc_type: type = assoc_entity_type @Y [concrete]
+// CHECK:STDOUT:   %assoc0.3d6: %Y.assoc_type = assoc_entity element0, @Y.WithSelf.%Y.WithSelf.Y1.decl [concrete]
+// CHECK:STDOUT:   %pattern_type.cfb: type = pattern_type %Y.type [concrete]
+// CHECK:STDOUT:   %T.patt.dc7: %pattern_type.cfb = symbolic_binding_pattern T, 0 [symbolic]
+// CHECK:STDOUT:   %T.95b: %Y.type = symbolic_binding T, 0 [symbolic]
+// CHECK:STDOUT:   %T.as_type.917: type = facet_access_type %T.95b [symbolic]
+// CHECK:STDOUT:   %.Self.frozen.7b7: %Z.type = symbolic_binding .Self [symbolic_self]
+// CHECK:STDOUT:   %.Self.frozen.as_type: type = facet_access_type %.Self.frozen.7b7 [symbolic_self]
+// CHECK:STDOUT:   %.db1: <witness> = impl_self_witness %.Self.frozen.7b7, @Z [symbolic_self]
+// CHECK:STDOUT:   %impl.elem0.e1c: type = impl_witness_access %.db1, element0 [symbolic_self]
+// CHECK:STDOUT:   %Y.WithSelf.Y1.type.27a: type = fn_type @Y.WithSelf.Y1, @Y.WithSelf(%T.95b) [symbolic]
+// CHECK:STDOUT:   %Y.lookup_impl_witness: <witness> = lookup_impl_witness %T.95b, @Y [symbolic]
+// CHECK:STDOUT:   %.604: type = fn_type_with_self_type %Y.WithSelf.Y1.type.27a, %T.95b [symbolic]
+// CHECK:STDOUT:   %impl.elem0.aed: %.604 = impl_witness_access %Y.lookup_impl_witness, element0 [symbolic]
+// CHECK:STDOUT:   %specific_impl_fn.4bf: <specific function> = specific_impl_function %impl.elem0.aed, @Y.WithSelf.Y1(%T.95b, %.Self.frozen.as_type) [symbolic]
+// CHECK:STDOUT:   %Y.WithSelf.Y1.call.f9a: init type = call %specific_impl_fn.4bf() [template]
+// CHECK:STDOUT:   %.Self: %Z.type = symbolic_binding .Self [symbolic_self]
+// CHECK:STDOUT:   %.513: <witness> = impl_self_witness %.Self, @Z [symbolic_self]
+// CHECK:STDOUT:   %impl.elem0.ff0: type = impl_witness_access %.513, element0 [symbolic_self]
+// CHECK:STDOUT:   %.Self.as_type: type = facet_access_type %.Self [symbolic_self]
+// CHECK:STDOUT:   %specific_impl_fn.85a: <specific function> = specific_impl_function %impl.elem0.aed, @Y.WithSelf.Y1(%T.95b, %.Self.as_type) [symbolic]
+// CHECK:STDOUT:   %Y.WithSelf.Y1.call.09a: init type = call %specific_impl_fn.85a() [template]
+// CHECK:STDOUT:   %Z_where.type.75d: type = facet_type <@Z where %impl.elem0.ff0 = %Y.WithSelf.Y1.call.09a> [template]
+// CHECK:STDOUT:   %.ddc: <witness> = impl_self_witness %T.95b, @Z [symbolic]
+// CHECK:STDOUT:   %specific_impl_fn.bac: <specific function> = specific_impl_function %impl.elem0.aed, @Y.WithSelf.Y1(%T.95b, %T.as_type.917):identified [symbolic]
+// CHECK:STDOUT:   %Z.impl_witness.179: <witness> = impl_witness @T.as_type.as.Z.impl.%Z.impl_witness_table, @T.as_type.as.Z.impl(%T.95b) [symbolic]
+// CHECK:STDOUT:   %specific_impl_fn.d3c: <specific function> = specific_impl_function %impl.elem0.aed, @Y.WithSelf.Y1(%T.95b, %T.as_type.917) [symbolic]
+// CHECK:STDOUT:   %Y.WithSelf.Y1.call.bea: init type = call %specific_impl_fn.d3c() [template]
+// CHECK:STDOUT:   %Y.impl_witness: <witness> = impl_witness @empty_tuple.type.as.Y.impl.%Y.impl_witness_table [concrete]
+// CHECK:STDOUT:   %empty_tuple.type.as.Y.impl.Y1.type: type = fn_type @empty_tuple.type.as.Y.impl.Y1 [concrete]
+// CHECK:STDOUT:   %empty_tuple.type.as.Y.impl.Y1: %empty_tuple.type.as.Y.impl.Y1.type = struct_value () [concrete]
+// CHECK:STDOUT:   %Y.facet: %Y.type = facet_value %empty_tuple.type, (%Y.impl_witness) [concrete]
+// CHECK:STDOUT:   %Y.WithSelf.Y1.type.67a: type = fn_type @Y.WithSelf.Y1, @Y.WithSelf(%Y.facet) [concrete]
+// CHECK:STDOUT:   %.0ff: type = fn_type_with_self_type %Y.WithSelf.Y1.type.67a, %Y.facet [concrete]
+// CHECK:STDOUT:   %empty_tuple.type.as.Y.impl.Y1.specific_fn.700: <specific function> = specific_function %empty_tuple.type.as.Y.impl.Y1, @empty_tuple.type.as.Y.impl.Y1(%.Self.as_type) [symbolic_self]
+// CHECK:STDOUT:   %empty_tuple.type.as.Y.impl.Y1.call: init type = call %empty_tuple.type.as.Y.impl.Y1.specific_fn.700() [symbolic_self]
+// CHECK:STDOUT:   %Z_where.type.b3e: type = facet_type <@Z where %impl.elem0.ff0 = %empty_tuple.type.as.Y.impl.Y1.call> [concrete]
+// CHECK:STDOUT:   %empty_tuple.type.as.Y.impl.Y1.specific_fn.c56: <specific function> = specific_function %empty_tuple.type.as.Y.impl.Y1, @empty_tuple.type.as.Y.impl.Y1(%empty_tuple.type) [concrete]
+// CHECK:STDOUT:   %.78e: <witness> = impl_self_witness %empty_tuple.type, @Z [concrete]
+// CHECK:STDOUT:   %Z.impl_witness.a55: <witness> = impl_witness @T.as_type.as.Z.impl.%Z.impl_witness_table, @T.as_type.as.Z.impl(%Y.facet) [concrete]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: file {
+// CHECK:STDOUT:   impl_decl @T.as_type.as.Z.impl [concrete] {
+// CHECK:STDOUT:     %T.patt.loc16_15.1: %pattern_type.cfb = symbolic_binding_pattern T, 0 [symbolic = %T.patt.loc16_15.2 (constants.%T.patt.dc7)]
+// CHECK:STDOUT:   } {
+// CHECK:STDOUT:     %T.ref.loc16_20: %Y.type = name_ref T, %T.loc16_15.1 [symbolic = %T.loc16_15.2 (constants.%T.95b)]
+// CHECK:STDOUT:     %T.as_type.loc16_20.1: type = facet_access_type %T.ref.loc16_20 [symbolic = %T.as_type.loc16_20.2 (constants.%T.as_type.917)]
+// CHECK:STDOUT:     %.loc16_20: type = converted %T.ref.loc16_20, %T.as_type.loc16_20.1 [symbolic = %T.as_type.loc16_20.2 (constants.%T.as_type.917)]
+// CHECK:STDOUT:     %Z.ref: type = name_ref Z, file.%Z.decl [concrete = constants.%Z.type]
+// CHECK:STDOUT:     %.Self.frozen.loc16_27: %Z.type = symbolic_binding .Self [symbolic_self = constants.%.Self.frozen.7b7]
+// CHECK:STDOUT:     %base_facet_type = requirement_base_facet_type %Z.ref [concrete]
+// CHECK:STDOUT:     %.Self.ref.loc16_33: %Z.type = name_ref .Self, %.Self.frozen.loc16_27 [symbolic_self = constants.%.Self.frozen.7b7]
+// CHECK:STDOUT:     %.Self.as_type.loc16_33: type = facet_access_type %.Self.ref.loc16_33 [symbolic_self = constants.%.Self.frozen.as_type]
+// CHECK:STDOUT:     %.loc16_33: type = converted %.Self.ref.loc16_33, %.Self.as_type.loc16_33 [symbolic_self = constants.%.Self.frozen.as_type]
+// CHECK:STDOUT:     %Z1.ref: %Z.assoc_type = name_ref Z1, @Z1.%assoc0 [concrete = constants.%assoc0.3fa]
+// CHECK:STDOUT:     %impl.elem0.loc16_33.1: type = impl_witness_access constants.%.db1, element0 [symbolic_self = constants.%impl.elem0.e1c]
+// CHECK:STDOUT:     %T.ref.loc16_39: %Y.type = name_ref T, %T.loc16_15.1 [symbolic = constants.%T.95b]
+// CHECK:STDOUT:     %T.as_type.loc16_40: type = facet_access_type %T.ref.loc16_39 [symbolic = constants.%T.as_type.917]
+// CHECK:STDOUT:     %.loc16_40: type = converted %T.ref.loc16_39, %T.as_type.loc16_40 [symbolic = constants.%T.as_type.917]
+// CHECK:STDOUT:     %Y1.ref: %Y.assoc_type = name_ref Y1, @Y.WithSelf.%assoc0 [concrete = constants.%assoc0.3d6]
+// CHECK:STDOUT:     %impl.elem0.loc16_40: %.604 = impl_witness_access constants.%Y.lookup_impl_witness, element0 [symbolic = constants.%impl.elem0.aed]
+// CHECK:STDOUT:     %.Self.ref.loc16_44: %Z.type = name_ref .Self, %.Self.frozen.loc16_27 [symbolic_self = constants.%.Self.frozen.7b7]
+// CHECK:STDOUT:     %.Self.as_type.loc16_49: type = facet_access_type %.Self.ref.loc16_44 [symbolic_self = constants.%.Self.frozen.as_type]
+// CHECK:STDOUT:     %.loc16_49.1: type = converted %.Self.ref.loc16_44, %.Self.as_type.loc16_49 [symbolic_self = constants.%.Self.frozen.as_type]
+// CHECK:STDOUT:     %specific_impl_fn.loc16_40.1: <specific function> = specific_impl_function %impl.elem0.loc16_40, @Y.WithSelf.Y1(constants.%T.95b, constants.%.Self.frozen.as_type) [symbolic = constants.%specific_impl_fn.4bf]
+// CHECK:STDOUT:     %Y.WithSelf.Y1.call.loc16_49.1: init type = call %specific_impl_fn.loc16_40.1() [template = constants.%Y.WithSelf.Y1.call.f9a]
+// CHECK:STDOUT:     %.loc16_49.2: type = value_of_initializer %Y.WithSelf.Y1.call.loc16_49.1 [template = constants.%Y.WithSelf.Y1.call.f9a]
+// CHECK:STDOUT:     %.loc16_49.3: type = converted %Y.WithSelf.Y1.call.loc16_49.1, %.loc16_49.2 [template = constants.%Y.WithSelf.Y1.call.f9a]
+// CHECK:STDOUT:     %rewrite.loc16_37.1 = requirement_rewrite %impl.elem0.loc16_33.1, %.loc16_49.3 [concrete]
+// CHECK:STDOUT:     %impl.elem0.loc16_33.2: type = impl_witness_access constants.%.513, element0 [symbolic_self = constants.%impl.elem0.ff0]
+// CHECK:STDOUT:     %specific_impl_fn.loc16_40.2: <specific function> = specific_impl_function %impl.elem0.loc16_40, @Y.WithSelf.Y1(constants.%T.95b, constants.%.Self.as_type) [symbolic = constants.%specific_impl_fn.85a]
+// CHECK:STDOUT:     %Y.WithSelf.Y1.call.loc16_49.2: init type = call %specific_impl_fn.loc16_40.2() [template = constants.%Y.WithSelf.Y1.call.09a]
+// CHECK:STDOUT:     %.loc16_49.4: type = value_of_initializer %Y.WithSelf.Y1.call.loc16_49.2 [template = constants.%Y.WithSelf.Y1.call.09a]
+// CHECK:STDOUT:     %.loc16_49.5: type = converted %Y.WithSelf.Y1.call.loc16_49.1, %.loc16_49.4 [template = constants.%Y.WithSelf.Y1.call.09a]
+// CHECK:STDOUT:     %rewrite.loc16_37.2 = requirement_rewrite %impl.elem0.loc16_33.2, %.loc16_49.5 [concrete]
+// CHECK:STDOUT:     %.loc16_27.1: type = where_expr [template = %Z_where.type (constants.%Z_where.type.75d)] {
+// CHECK:STDOUT:       %base_facet_type = requirement_base_facet_type %Z.ref [concrete]
+// CHECK:STDOUT:       %rewrite.loc16_37.2 = requirement_rewrite %impl.elem0.loc16_33.2, %.loc16_49.5 [concrete]
+// CHECK:STDOUT:     }
+// CHECK:STDOUT:     %.loc16_17: type = splice_block %Y.ref [concrete = constants.%Y.type] {
+// CHECK:STDOUT:       %.Self.frozen.loc16_15: type = symbolic_binding .Self [symbolic_self = constants.%.Self.frozen.e58]
+// CHECK:STDOUT:       %Y.ref: type = name_ref Y, file.%Y.decl [concrete = constants.%Y.type]
+// CHECK:STDOUT:     }
+// CHECK:STDOUT:     %T.loc16_15.1: %Y.type = symbolic_binding T, 0 [symbolic = %T.loc16_15.2 (constants.%T.95b)]
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %specific_impl_fn: <specific function> = specific_impl_function constants.%impl.elem0.aed, @Y.WithSelf.Y1(constants.%T.95b, constants.%T.as_type.917):identified [symbolic = @T.as_type.as.Z.impl.%specific_impl_fn.loc16_27.2 (constants.%specific_impl_fn.bac)]
+// CHECK:STDOUT:   %.loc16: <witness> = impl_self_witness @T.as_type.as.Z.impl.%.loc16_20, @Z [symbolic = @T.as_type.as.Z.impl.%.loc16_51 (constants.%.ddc)]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: generic impl @T.as_type.as.Z.impl(%T.loc16_15.1: %Y.type) {
+// CHECK:STDOUT:   %T.patt.loc16_15.2: %pattern_type.cfb = symbolic_binding_pattern T, 0 [symbolic = %T.patt.loc16_15.2 (constants.%T.patt.dc7)]
+// CHECK:STDOUT:   %T.loc16_15.2: %Y.type = symbolic_binding T, 0 [symbolic = %T.loc16_15.2 (constants.%T.95b)]
+// CHECK:STDOUT:   %T.as_type.loc16_20.2: type = facet_access_type %T.loc16_15.2 [symbolic = %T.as_type.loc16_20.2 (constants.%T.as_type.917)]
+// CHECK:STDOUT:   %Y.WithSelf.Y1.type: type = fn_type @Y.WithSelf.Y1, @Y.WithSelf(%T.loc16_15.2) [symbolic = %Y.WithSelf.Y1.type (constants.%Y.WithSelf.Y1.type.27a)]
+// CHECK:STDOUT:   %.loc16_27.2: type = fn_type_with_self_type %Y.WithSelf.Y1.type, %T.loc16_15.2 [symbolic = %.loc16_27.2 (constants.%.604)]
+// CHECK:STDOUT:   %Y.lookup_impl_witness: <witness> = lookup_impl_witness %T.loc16_15.2, @Y [symbolic = %Y.lookup_impl_witness (constants.%Y.lookup_impl_witness)]
+// CHECK:STDOUT:   %impl.elem0.loc16_27: @T.as_type.as.Z.impl.%.loc16_27.2 (%.604) = impl_witness_access %Y.lookup_impl_witness, element0 [symbolic = %impl.elem0.loc16_27 (constants.%impl.elem0.aed)]
+// CHECK:STDOUT:   %specific_impl_fn.loc16_27.1: <specific function> = specific_impl_function %impl.elem0.loc16_27, @Y.WithSelf.Y1(%T.loc16_15.2, constants.%.Self.as_type) [symbolic = %specific_impl_fn.loc16_27.1 (constants.%specific_impl_fn.85a)]
+// CHECK:STDOUT:   %Y.WithSelf.Y1.call.loc16_27: init type = call %specific_impl_fn.loc16_27.1() [template = %Y.WithSelf.Y1.call.loc16_27 (constants.%Y.WithSelf.Y1.call.09a)]
+// CHECK:STDOUT:   %Z_where.type: type = facet_type <@Z where constants.%impl.elem0.ff0 = %Y.WithSelf.Y1.call.loc16_27> [template = %Z_where.type (constants.%Z_where.type.75d)]
+// CHECK:STDOUT:   %specific_impl_fn.loc16_27.2: <specific function> = specific_impl_function %impl.elem0.loc16_27, @Y.WithSelf.Y1(%T.loc16_15.2, %T.as_type.loc16_20.2):identified [symbolic = %specific_impl_fn.loc16_27.2 (constants.%specific_impl_fn.bac)]
+// CHECK:STDOUT:   %.loc16_51: <witness> = impl_self_witness %T.loc16_15.2, @Z [symbolic = %.loc16_51 (constants.%.ddc)]
+// CHECK:STDOUT:   %Z.impl_witness.loc16_51.2: <witness> = impl_witness %Z.impl_witness_table, @T.as_type.as.Z.impl(%T.loc16_15.2) [symbolic = %Z.impl_witness.loc16_51.2 (constants.%Z.impl_witness.179)]
+// CHECK:STDOUT:   %specific_impl_fn.loc16_51.2: <specific function> = specific_impl_function %impl.elem0.loc16_27, @Y.WithSelf.Y1(%T.loc16_15.2, %T.as_type.loc16_20.2) [symbolic = %specific_impl_fn.loc16_51.2 (constants.%specific_impl_fn.d3c)]
+// CHECK:STDOUT:   %Y.WithSelf.Y1.call.loc16_51: init type = call %specific_impl_fn.loc16_51.2() [template = %Y.WithSelf.Y1.call.loc16_51 (constants.%Y.WithSelf.Y1.call.bea)]
+// CHECK:STDOUT:
+// CHECK:STDOUT: !definition:
+// CHECK:STDOUT:
+// CHECK:STDOUT:   impl: %.loc16_20 as %Z.ref {
+// CHECK:STDOUT:     %Z.impl_witness_table = impl_witness_table (%impl_witness_assoc_constant), @T.as_type.as.Z.impl [concrete]
+// CHECK:STDOUT:     %Z.impl_witness.loc16_51.1: <witness> = impl_witness %Z.impl_witness_table, @T.as_type.as.Z.impl(constants.%T.95b) [symbolic = %Z.impl_witness.loc16_51.2 (constants.%Z.impl_witness.179)]
+// CHECK:STDOUT:     %specific_impl_fn.loc16_51.1: <specific function> = specific_impl_function constants.%impl.elem0.aed, @Y.WithSelf.Y1(constants.%T.95b, constants.%T.as_type.917) [symbolic = %specific_impl_fn.loc16_51.2 (constants.%specific_impl_fn.d3c)]
+// CHECK:STDOUT:     %impl_witness_assoc_constant: init type = impl_witness_assoc_constant constants.%Y.WithSelf.Y1.call.bea [template = %Y.WithSelf.Y1.call.loc16_51 (constants.%Y.WithSelf.Y1.call.bea)]
+// CHECK:STDOUT:
+// CHECK:STDOUT:   !members:
+// CHECK:STDOUT:     extend %Z.ref
+// CHECK:STDOUT:     witness = %Z.impl_witness.loc16_51.1
+// CHECK:STDOUT:   }
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @T.as_type.as.Z.impl(constants.%T.95b) {
+// CHECK:STDOUT:   %T.patt.loc16_15.2 => constants.%T.patt.dc7
+// CHECK:STDOUT:   %T.loc16_15.2 => constants.%T.95b
+// CHECK:STDOUT:   %T.as_type.loc16_20.2 => constants.%T.as_type.917
+// CHECK:STDOUT:   %Y.WithSelf.Y1.type => constants.%Y.WithSelf.Y1.type.27a
+// CHECK:STDOUT:   %.loc16_27.2 => constants.%.604
+// CHECK:STDOUT:   %Y.lookup_impl_witness => constants.%Y.lookup_impl_witness
+// CHECK:STDOUT:   %impl.elem0.loc16_27 => constants.%impl.elem0.aed
+// CHECK:STDOUT:   %specific_impl_fn.loc16_27.1 => constants.%specific_impl_fn.85a
+// CHECK:STDOUT:   %Y.WithSelf.Y1.call.loc16_27 => constants.%Y.WithSelf.Y1.call.09a
+// CHECK:STDOUT:   %Z_where.type => constants.%Z_where.type.75d
+// CHECK:STDOUT:   %specific_impl_fn.loc16_27.2 => constants.%specific_impl_fn.bac
+// CHECK:STDOUT:   %.loc16_51 => constants.%.ddc
+// CHECK:STDOUT:   %Z.impl_witness.loc16_51.2 => constants.%Z.impl_witness.179
+// CHECK:STDOUT:   %specific_impl_fn.loc16_51.2 => constants.%specific_impl_fn.d3c
+// CHECK:STDOUT:   %Y.WithSelf.Y1.call.loc16_51 => constants.%Y.WithSelf.Y1.call.bea
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @T.as_type.as.Z.impl(constants.%Y.facet) {
+// CHECK:STDOUT:   %T.patt.loc16_15.2 => constants.%T.patt.dc7
+// CHECK:STDOUT:   %T.loc16_15.2 => constants.%Y.facet
+// CHECK:STDOUT:   %T.as_type.loc16_20.2 => constants.%empty_tuple.type
+// CHECK:STDOUT:   %Y.WithSelf.Y1.type => constants.%Y.WithSelf.Y1.type.67a
+// CHECK:STDOUT:   %.loc16_27.2 => constants.%.0ff
+// CHECK:STDOUT:   %Y.lookup_impl_witness => constants.%Y.impl_witness
+// CHECK:STDOUT:   %impl.elem0.loc16_27 => constants.%empty_tuple.type.as.Y.impl.Y1
+// CHECK:STDOUT:   %specific_impl_fn.loc16_27.1 => constants.%empty_tuple.type.as.Y.impl.Y1.specific_fn.700
+// CHECK:STDOUT:   %Y.WithSelf.Y1.call.loc16_27 => constants.%empty_tuple.type.as.Y.impl.Y1.call
+// CHECK:STDOUT:   %Z_where.type => constants.%Z_where.type.b3e
+// CHECK:STDOUT:   %specific_impl_fn.loc16_27.2 => constants.%empty_tuple.type.as.Y.impl.Y1.specific_fn.c56
+// CHECK:STDOUT:   %.loc16_51 => constants.%.78e
+// CHECK:STDOUT:   %Z.impl_witness.loc16_51.2 => constants.%Z.impl_witness.a55
+// CHECK:STDOUT:   %specific_impl_fn.loc16_51.2 => constants.%empty_tuple.type.as.Y.impl.Y1.specific_fn.c56
+// CHECK:STDOUT:   %Y.WithSelf.Y1.call.loc16_51 => constants.%empty_tuple.type
+// CHECK:STDOUT:
+// CHECK:STDOUT: !definition:
+// CHECK:STDOUT: }
+// CHECK:STDOUT:

toolchain/check/testdata/for/actual.carbon

@@ -319,16 +319,13 @@ fn Read(generic y: Core.IntLiteral) {
 // CHECK:STDOUT: generic impl @IntRange.as.Iterate.impl(@IntRange.%N.loc4_17.2: Core.IntLiteral) {
 // CHECK:STDOUT:   %N: Core.IntLiteral = symbolic_binding N, 0 [symbolic = %N (constants.%N)]
 // CHECK:STDOUT:   %IntRange: type = class_type @IntRange, @IntRange(%N) [symbolic = %IntRange (constants.%IntRange.0bb)]
-// CHECK:STDOUT:   %Int.loc9_54.1: type = class_type @Int, @Int(%N) [symbolic = %Int.loc9_54.1 (constants.%Int.d4bbe0.1)]
-// CHECK:STDOUT:   %SubobjectDestroy.lookup_impl_witness: <witness> = lookup_impl_witness %Int.loc9_54.1, @SubobjectDestroy [symbolic = %SubobjectDestroy.lookup_impl_witness (constants.%SubobjectDestroy.lookup_impl_witness.f5e)]
-// CHECK:STDOUT:   %SubobjectDestroy.facet: %SubobjectDestroy.type = facet_value %Int.loc9_54.1, (%SubobjectDestroy.lookup_impl_witness) [symbolic = %SubobjectDestroy.facet (constants.%SubobjectDestroy.facet.cbf)]
-// CHECK:STDOUT:   %.loc9_54.1: require_specific_def_type = require_specific_def @T.as_type.as.DestroyImpl.impl(%SubobjectDestroy.facet) [symbolic = %.loc9_54.1 (constants.%.811)]
-// CHECK:STDOUT:   %DestroyImpl.lookup_impl_witness: <witness> = lookup_impl_witness %Int.loc9_54.1, @DestroyImpl [symbolic = %DestroyImpl.lookup_impl_witness (constants.%DestroyImpl.lookup_impl_witness.79f)]
-// CHECK:STDOUT:   %Destroy.facet.loc9_54.1: %Destroy.type = facet_value %Int.loc9_54.1, (%SubobjectDestroy.lookup_impl_witness, %DestroyImpl.lookup_impl_witness) [symbolic = %Destroy.facet.loc9_54.1 (constants.%Destroy.facet.0e1)]
-// CHECK:STDOUT:   %.loc9_85.1: require_specific_def_type = require_specific_def @Int.as.Copy.impl(%N) [symbolic = %.loc9_85.1 (constants.%.cbd)]
-// CHECK:STDOUT:   %Copy.lookup_impl_witness: <witness> = lookup_impl_witness %Int.loc9_54.1, @Copy [symbolic = %Copy.lookup_impl_witness (constants.%Copy.lookup_impl_witness.923)]
-// CHECK:STDOUT:   %facet_value.loc9_85.1: %facet_type.bd0 = facet_value %Int.loc9_54.1, (%SubobjectDestroy.lookup_impl_witness, %DestroyImpl.lookup_impl_witness, %Copy.lookup_impl_witness) [symbolic = %facet_value.loc9_85.1 (constants.%facet_value)]
-// CHECK:STDOUT:   %Iterate_where.type: type = facet_type <@Iterate where constants.%impl.elem1.af2 = %Destroy.facet.loc9_54.1 and constants.%impl.elem0.685 = %facet_value.loc9_85.1> [symbolic = %Iterate_where.type (constants.%Iterate_where.type.4d1)]
+// CHECK:STDOUT:   %Int.loc9_24: type = class_type @Int, @Int(%N) [symbolic = %Int.loc9_24 (constants.%Int.d4bbe0.1)]
+// CHECK:STDOUT:   %SubobjectDestroy.lookup_impl_witness: <witness> = lookup_impl_witness %Int.loc9_24, @SubobjectDestroy [symbolic = %SubobjectDestroy.lookup_impl_witness (constants.%SubobjectDestroy.lookup_impl_witness.f5e)]
+// CHECK:STDOUT:   %DestroyImpl.lookup_impl_witness: <witness> = lookup_impl_witness %Int.loc9_24, @DestroyImpl [symbolic = %DestroyImpl.lookup_impl_witness (constants.%DestroyImpl.lookup_impl_witness.79f)]
+// CHECK:STDOUT:   %Destroy.facet.loc9_24: %Destroy.type = facet_value %Int.loc9_24, (%SubobjectDestroy.lookup_impl_witness, %DestroyImpl.lookup_impl_witness) [symbolic = %Destroy.facet.loc9_24 (constants.%Destroy.facet.0e1)]
+// CHECK:STDOUT:   %Copy.lookup_impl_witness: <witness> = lookup_impl_witness %Int.loc9_24, @Copy [symbolic = %Copy.lookup_impl_witness (constants.%Copy.lookup_impl_witness.923)]
+// CHECK:STDOUT:   %facet_value.loc9_24: %facet_type.bd0 = facet_value %Int.loc9_24, (%SubobjectDestroy.lookup_impl_witness, %DestroyImpl.lookup_impl_witness, %Copy.lookup_impl_witness) [symbolic = %facet_value.loc9_24 (constants.%facet_value)]
+// CHECK:STDOUT:   %Iterate_where.type: type = facet_type <@Iterate where constants.%impl.elem1.af2 = %Destroy.facet.loc9_24 and constants.%impl.elem0.685 = %facet_value.loc9_24> [symbolic = %Iterate_where.type (constants.%Iterate_where.type.4d1)]
 // CHECK:STDOUT:   %.loc9_87: <witness> = impl_self_witness %IntRange, @Iterate [symbolic = %.loc9_87 (constants.%.712)]
 // CHECK:STDOUT:   %Iterate.impl_witness.loc9_87.2: <witness> = impl_witness %Iterate.impl_witness_table, @IntRange.as.Iterate.impl(%N) [symbolic = %Iterate.impl_witness.loc9_87.2 (constants.%Iterate.impl_witness)]
 // CHECK:STDOUT:
@@ -399,8 +396,8 @@ fn Read(generic y: Core.IntLiteral) {
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %Iterate.impl_witness_table = impl_witness_table (%impl_witness_assoc_constant.loc9_87.1, %impl_witness_assoc_constant.loc9_87.2, %IntRange.as.Iterate.impl.NewCursor.decl, %IntRange.as.Iterate.impl.Next.decl), @IntRange.as.Iterate.impl [concrete]
 // CHECK:STDOUT:     %Iterate.impl_witness.loc9_87.1: <witness> = impl_witness %Iterate.impl_witness_table, @IntRange.as.Iterate.impl(constants.%N) [symbolic = %Iterate.impl_witness.loc9_87.2 (constants.%Iterate.impl_witness)]
-// CHECK:STDOUT:     %impl_witness_assoc_constant.loc9_87.1: %facet_type.bd0 = impl_witness_assoc_constant constants.%facet_value [symbolic = %facet_value.loc9_85.1 (constants.%facet_value)]
-// CHECK:STDOUT:     %impl_witness_assoc_constant.loc9_87.2: %Destroy.type = impl_witness_assoc_constant constants.%Destroy.facet.0e1 [symbolic = %Destroy.facet.loc9_54.1 (constants.%Destroy.facet.0e1)]
+// CHECK:STDOUT:     %impl_witness_assoc_constant.loc9_87.1: %facet_type.bd0 = impl_witness_assoc_constant constants.%facet_value [symbolic = %facet_value.loc9_24 (constants.%facet_value)]
+// CHECK:STDOUT:     %impl_witness_assoc_constant.loc9_87.2: %Destroy.type = impl_witness_assoc_constant constants.%Destroy.facet.0e1 [symbolic = %Destroy.facet.loc9_24 (constants.%Destroy.facet.0e1)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   !members:
 // CHECK:STDOUT:     .N = <poisoned>
@@ -471,12 +468,12 @@ fn Read(generic y: Core.IntLiteral) {
 // CHECK:STDOUT:       %impl.elem1.loc9_30.1: %Destroy.type = impl_witness_access constants.%.052, element1 [symbolic_self = constants.%impl.elem1.d2c]
 // CHECK:STDOUT:       %Core.ref.loc9_44: <namespace> = name_ref Core, imports.%Core [concrete = imports.%Core]
 // CHECK:STDOUT:       %Int.ref.loc9_48: %Int.type = name_ref Int, imports.%Core.Int [concrete = constants.%Int.generic]
-// CHECK:STDOUT:       %.loc9_53: Core.IntLiteral = specific_constant @IntRange.%N.loc4_17.2, @IntRange(constants.%N) [symbolic = %N (constants.%N)]
-// CHECK:STDOUT:       %N.ref.loc9_53: Core.IntLiteral = name_ref N, %.loc9_53 [symbolic = %N (constants.%N)]
-// CHECK:STDOUT:       %Int.loc9_54.2: type = class_type @Int, @Int(constants.%N) [symbolic = %Int.loc9_54.1 (constants.%Int.d4bbe0.1)]
-// CHECK:STDOUT:       %Destroy.facet.loc9_54.2: %Destroy.type = facet_value %Int.loc9_54.2, (constants.%SubobjectDestroy.lookup_impl_witness.f5e, constants.%DestroyImpl.lookup_impl_witness.79f) [symbolic = %Destroy.facet.loc9_54.1 (constants.%Destroy.facet.0e1)]
-// CHECK:STDOUT:       %.loc9_54.2: %Destroy.type = converted %Int.loc9_54.2, %Destroy.facet.loc9_54.2 [symbolic = %Destroy.facet.loc9_54.1 (constants.%Destroy.facet.0e1)]
-// CHECK:STDOUT:       %rewrite.loc9_42.1 = requirement_rewrite %impl.elem1.loc9_30.1, %.loc9_54.2 [concrete]
+// CHECK:STDOUT:       %.loc9_53: Core.IntLiteral = specific_constant @IntRange.%N.loc4_17.2, @IntRange(constants.%N) [symbolic = constants.%N]
+// CHECK:STDOUT:       %N.ref.loc9_53: Core.IntLiteral = name_ref N, %.loc9_53 [symbolic = constants.%N]
+// CHECK:STDOUT:       %Int.loc9_54: type = class_type @Int, @Int(constants.%N) [symbolic = constants.%Int.d4bbe0.1]
+// CHECK:STDOUT:       %Destroy.facet.loc9_54: %Destroy.type = facet_value %Int.loc9_54, (constants.%SubobjectDestroy.lookup_impl_witness.f5e, constants.%DestroyImpl.lookup_impl_witness.79f) [symbolic = constants.%Destroy.facet.0e1]
+// CHECK:STDOUT:       %.loc9_54: %Destroy.type = converted %Int.loc9_54, %Destroy.facet.loc9_54 [symbolic = constants.%Destroy.facet.0e1]
+// CHECK:STDOUT:       %rewrite.loc9_42.1 = requirement_rewrite %impl.elem1.loc9_30.1, %.loc9_54 [concrete]
 // CHECK:STDOUT:       %.Self.ref.loc9_60: %Iterate.type = name_ref .Self, %.Self.frozen [symbolic_self = constants.%.Self.frozen.bdd]
 // CHECK:STDOUT:       %.Self.as_type.loc9_60: type = facet_access_type %.Self.ref.loc9_60 [symbolic_self = constants.%.Self.frozen.as_type]
 // CHECK:STDOUT:       %.loc9_60: type = converted %.Self.ref.loc9_60, %.Self.as_type.loc9_60 [symbolic_self = constants.%.Self.frozen.as_type]
@@ -484,20 +481,20 @@ fn Read(generic y: Core.IntLiteral) {
 // CHECK:STDOUT:       %impl.elem0.loc9_60.1: %facet_type.bd0 = impl_witness_access constants.%.052, element0 [symbolic_self = constants.%impl.elem0.a07]
 // CHECK:STDOUT:       %Core.ref.loc9_75: <namespace> = name_ref Core, imports.%Core [concrete = imports.%Core]
 // CHECK:STDOUT:       %Int.ref.loc9_79: %Int.type = name_ref Int, imports.%Core.Int [concrete = constants.%Int.generic]
-// CHECK:STDOUT:       %.loc9_84: Core.IntLiteral = specific_constant @IntRange.%N.loc4_17.2, @IntRange(constants.%N) [symbolic = %N (constants.%N)]
-// CHECK:STDOUT:       %N.ref.loc9_84: Core.IntLiteral = name_ref N, %.loc9_84 [symbolic = %N (constants.%N)]
-// CHECK:STDOUT:       %Int.loc9_85: type = class_type @Int, @Int(constants.%N) [symbolic = %Int.loc9_54.1 (constants.%Int.d4bbe0.1)]
-// CHECK:STDOUT:       %facet_value.loc9_85.2: %facet_type.bd0 = facet_value %Int.loc9_85, (constants.%SubobjectDestroy.lookup_impl_witness.f5e, constants.%DestroyImpl.lookup_impl_witness.79f, constants.%Copy.lookup_impl_witness.923) [symbolic = %facet_value.loc9_85.1 (constants.%facet_value)]
-// CHECK:STDOUT:       %.loc9_85.2: %facet_type.bd0 = converted %Int.loc9_85, %facet_value.loc9_85.2 [symbolic = %facet_value.loc9_85.1 (constants.%facet_value)]
-// CHECK:STDOUT:       %rewrite.loc9_73.1 = requirement_rewrite %impl.elem0.loc9_60.1, %.loc9_85.2 [concrete]
+// CHECK:STDOUT:       %.loc9_84: Core.IntLiteral = specific_constant @IntRange.%N.loc4_17.2, @IntRange(constants.%N) [symbolic = constants.%N]
+// CHECK:STDOUT:       %N.ref.loc9_84: Core.IntLiteral = name_ref N, %.loc9_84 [symbolic = constants.%N]
+// CHECK:STDOUT:       %Int.loc9_85: type = class_type @Int, @Int(constants.%N) [symbolic = constants.%Int.d4bbe0.1]
+// CHECK:STDOUT:       %facet_value.loc9_85: %facet_type.bd0 = facet_value %Int.loc9_85, (constants.%SubobjectDestroy.lookup_impl_witness.f5e, constants.%DestroyImpl.lookup_impl_witness.79f, constants.%Copy.lookup_impl_witness.923) [symbolic = constants.%facet_value]
+// CHECK:STDOUT:       %.loc9_85: %facet_type.bd0 = converted %Int.loc9_85, %facet_value.loc9_85 [symbolic = constants.%facet_value]
+// CHECK:STDOUT:       %rewrite.loc9_73.1 = requirement_rewrite %impl.elem0.loc9_60.1, %.loc9_85 [concrete]
 // CHECK:STDOUT:       %impl.elem1.loc9_30.2: %Destroy.type = impl_witness_access constants.%.327, element1 [symbolic_self = constants.%impl.elem1.af2]
-// CHECK:STDOUT:       %rewrite.loc9_42.2 = requirement_rewrite %impl.elem1.loc9_30.2, %.loc9_54.2 [concrete]
+// CHECK:STDOUT:       %rewrite.loc9_42.2 = requirement_rewrite %impl.elem1.loc9_30.2, %.loc9_54 [concrete]
 // CHECK:STDOUT:       %impl.elem0.loc9_60.2: %facet_type.bd0 = impl_witness_access constants.%.327, element0 [symbolic_self = constants.%impl.elem0.685]
-// CHECK:STDOUT:       %rewrite.loc9_73.2 = requirement_rewrite %impl.elem0.loc9_60.2, %.loc9_85.2 [concrete]
+// CHECK:STDOUT:       %rewrite.loc9_73.2 = requirement_rewrite %impl.elem0.loc9_60.2, %.loc9_85 [concrete]
 // CHECK:STDOUT:       %.loc9_24: type = where_expr [symbolic = %Iterate_where.type (constants.%Iterate_where.type.4d1)] {
 // CHECK:STDOUT:         %base_facet_type = requirement_base_facet_type %Iterate.ref [concrete]
-// CHECK:STDOUT:         %rewrite.loc9_42.2 = requirement_rewrite %impl.elem1.loc9_30.2, %.loc9_54.2 [concrete]
-// CHECK:STDOUT:         %rewrite.loc9_73.2 = requirement_rewrite %impl.elem0.loc9_60.2, %.loc9_85.2 [concrete]
+// CHECK:STDOUT:         %rewrite.loc9_42.2 = requirement_rewrite %impl.elem1.loc9_30.2, %.loc9_54 [concrete]
+// CHECK:STDOUT:         %rewrite.loc9_73.2 = requirement_rewrite %impl.elem0.loc9_60.2, %.loc9_85 [concrete]
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %.loc9: <witness> = impl_self_witness @IntRange.as.Iterate.impl.%Self.ref, @Iterate [symbolic = @IntRange.as.Iterate.impl.%.loc9_87 (constants.%.712)]
@@ -859,15 +856,12 @@ fn Read(generic y: Core.IntLiteral) {
 // CHECK:STDOUT: specific @IntRange.as.Iterate.impl(constants.%N) {
 // CHECK:STDOUT:   %N => constants.%N
 // CHECK:STDOUT:   %IntRange => constants.%IntRange.0bb
-// CHECK:STDOUT:   %Int.loc9_54.1 => constants.%Int.d4bbe0.1
+// CHECK:STDOUT:   %Int.loc9_24 => constants.%Int.d4bbe0.1
 // CHECK:STDOUT:   %SubobjectDestroy.lookup_impl_witness => constants.%SubobjectDestroy.lookup_impl_witness.f5e
-// CHECK:STDOUT:   %SubobjectDestroy.facet => constants.%SubobjectDestroy.facet.cbf
-// CHECK:STDOUT:   %.loc9_54.1 => constants.%.811
 // CHECK:STDOUT:   %DestroyImpl.lookup_impl_witness => constants.%DestroyImpl.lookup_impl_witness.79f
-// CHECK:STDOUT:   %Destroy.facet.loc9_54.1 => constants.%Destroy.facet.0e1
-// CHECK:STDOUT:   %.loc9_85.1 => constants.%.cbd
+// CHECK:STDOUT:   %Destroy.facet.loc9_24 => constants.%Destroy.facet.0e1
 // CHECK:STDOUT:   %Copy.lookup_impl_witness => constants.%Copy.lookup_impl_witness.923
-// CHECK:STDOUT:   %facet_value.loc9_85.1 => constants.%facet_value
+// CHECK:STDOUT:   %facet_value.loc9_24 => constants.%facet_value
 // CHECK:STDOUT:   %Iterate_where.type => constants.%Iterate_where.type.4d1
 // CHECK:STDOUT:   %.loc9_87 => constants.%.712
 // CHECK:STDOUT:   %Iterate.impl_witness.loc9_87.2 => constants.%Iterate.impl_witness

toolchain/check/testdata/generic/dot_self_symbolic_type.carbon

@@ -87,7 +87,6 @@ fn H(generic T: type) {
 // CHECK:STDOUT:   %.Self.frozen.b15: %A.type.fa003b.2 = symbolic_binding .Self [symbolic]
 // CHECK:STDOUT:   %A.assoc_type.3230b8.2: type = assoc_entity_type @A, @A(%CC) [symbolic]
 // CHECK:STDOUT:   %assoc0.4c905d.2: %A.assoc_type.3230b8.2 = assoc_entity element0, @A.WithSelf.%X [symbolic]
-// CHECK:STDOUT:   %require_complete.792: <witness> = require_complete_type %A.type.fa003b.2 [symbolic]
 // CHECK:STDOUT:   %.Self.frozen.as_type: type = facet_access_type %.Self.frozen.b15 [symbolic]
 // CHECK:STDOUT:   %A.lookup_impl_witness.030: <witness> = lookup_impl_witness %.Self.frozen.b15, @A, @A(%CC) [symbolic]
 // CHECK:STDOUT:   %impl.elem0.fba: type = impl_witness_access %A.lookup_impl_witness.030, element0 [symbolic]
@@ -140,20 +139,20 @@ fn H(generic T: type) {
 // CHECK:STDOUT:         %A.type.loc11_30.2: type = facet_type <@A, @A(constants.%CC)> [symbolic = %A.type.loc11_30.1 (constants.%A.type.fa003b.2)]
 // CHECK:STDOUT:         %.Self.frozen.loc11_32.2: @C.F.%A.type.loc11_30.1 (%A.type.fa003b.2) = symbolic_binding .Self [symbolic = %.Self.frozen.loc11_32.1 (constants.%.Self.frozen.b15)]
 // CHECK:STDOUT:         %base_facet_type = requirement_base_facet_type %A.type.loc11_30.2 [concrete]
-// CHECK:STDOUT:         %.Self.ref: @C.F.%A.type.loc11_30.1 (%A.type.fa003b.2) = name_ref .Self, %.Self.frozen.loc11_32.2 [symbolic = %.Self.frozen.loc11_32.1 (constants.%.Self.frozen.b15)]
-// CHECK:STDOUT:         %.Self.as_type: type = facet_access_type %.Self.ref [symbolic = %.Self.frozen.as_type (constants.%.Self.frozen.as_type)]
-// CHECK:STDOUT:         %.loc11_38.1: type = converted %.Self.ref, %.Self.as_type [symbolic = %.Self.frozen.as_type (constants.%.Self.frozen.as_type)]
-// CHECK:STDOUT:         %.loc11_38.2: @C.F.%A.assoc_type (%A.assoc_type.3230b8.2) = specific_constant @X.%assoc0, @A.WithSelf(constants.%CC, constants.%.Self.frozen.b15) [symbolic = %assoc0 (constants.%assoc0.4c905d.2)]
-// CHECK:STDOUT:         %X.ref: @C.F.%A.assoc_type (%A.assoc_type.3230b8.2) = name_ref X, %.loc11_38.2 [symbolic = %assoc0 (constants.%assoc0.4c905d.2)]
-// CHECK:STDOUT:         %impl.elem0.loc11_38.3: type = impl_witness_access constants.%A.lookup_impl_witness.030, element0 [symbolic = %impl.elem0.loc11_38.1 (constants.%impl.elem0.fba)]
-// CHECK:STDOUT:         %.loc11_43: type = specific_constant @C.%CC.loc6_11.2, @C(constants.%CC) [symbolic = %CC (constants.%CC)]
-// CHECK:STDOUT:         %CC.ref.loc11_43: type = name_ref CC, %.loc11_43 [symbolic = %CC (constants.%CC)]
-// CHECK:STDOUT:         %rewrite.loc11_41.1 = requirement_rewrite %impl.elem0.loc11_38.3, %CC.ref.loc11_43 [concrete]
-// CHECK:STDOUT:         %impl.elem0.loc11_38.4: type = impl_witness_access constants.%A.lookup_impl_witness.9e772d.1, element0 [symbolic = %impl.elem0.loc11_38.2 (constants.%impl.elem0.7f79de.1)]
-// CHECK:STDOUT:         %rewrite.loc11_41.2 = requirement_rewrite %impl.elem0.loc11_38.4, %CC.ref.loc11_43 [concrete]
+// CHECK:STDOUT:         %.Self.ref: %A.type.fa003b.2 = name_ref .Self, %.Self.frozen.loc11_32.2 [symbolic = constants.%.Self.frozen.b15]
+// CHECK:STDOUT:         %.Self.as_type: type = facet_access_type %.Self.ref [symbolic = constants.%.Self.frozen.as_type]
+// CHECK:STDOUT:         %.loc11_38.1: type = converted %.Self.ref, %.Self.as_type [symbolic = constants.%.Self.frozen.as_type]
+// CHECK:STDOUT:         %.loc11_38.2: %A.assoc_type.3230b8.2 = specific_constant @X.%assoc0, @A.WithSelf(constants.%CC, constants.%.Self.frozen.b15) [symbolic = constants.%assoc0.4c905d.2]
+// CHECK:STDOUT:         %X.ref: %A.assoc_type.3230b8.2 = name_ref X, %.loc11_38.2 [symbolic = constants.%assoc0.4c905d.2]
+// CHECK:STDOUT:         %impl.elem0.loc11_38.1: type = impl_witness_access constants.%A.lookup_impl_witness.030, element0 [symbolic = constants.%impl.elem0.fba]
+// CHECK:STDOUT:         %.loc11_43: type = specific_constant @C.%CC.loc6_11.2, @C(constants.%CC) [symbolic = constants.%CC]
+// CHECK:STDOUT:         %CC.ref.loc11_43: type = name_ref CC, %.loc11_43 [symbolic = constants.%CC]
+// CHECK:STDOUT:         %rewrite.loc11_41.1 = requirement_rewrite %impl.elem0.loc11_38.1, %CC.ref.loc11_43 [concrete]
+// CHECK:STDOUT:         %impl.elem0.loc11_38.2: type = impl_witness_access constants.%A.lookup_impl_witness.9e772d.1, element0 [symbolic = constants.%impl.elem0.7f79de.1]
+// CHECK:STDOUT:         %rewrite.loc11_41.2 = requirement_rewrite %impl.elem0.loc11_38.2, %CC.ref.loc11_43 [concrete]
 // CHECK:STDOUT:         %.loc11_32.2: type = where_expr [symbolic = %A_where.type (constants.%A_where.type.ff151a.1)] {
 // CHECK:STDOUT:           %base_facet_type = requirement_base_facet_type %A.type.loc11_30.2 [concrete]
-// CHECK:STDOUT:           %rewrite.loc11_41.2 = requirement_rewrite %impl.elem0.loc11_38.4, %CC.ref.loc11_43 [concrete]
+// CHECK:STDOUT:           %rewrite.loc11_41.2 = requirement_rewrite %impl.elem0.loc11_38.2, %CC.ref.loc11_43 [concrete]
 // CHECK:STDOUT:         }
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:       %T.loc11_24.2: @C.F.%A_where.type (%A_where.type.ff151a.1) = symbolic_binding T, 1 [symbolic = %T.loc11_24.1 (constants.%T.5e2)]
@@ -191,16 +190,10 @@ fn H(generic T: type) {
 // CHECK:STDOUT:   %CC: type = symbolic_binding CC, 0 [symbolic = %CC (constants.%CC)]
 // CHECK:STDOUT:   %A.type.loc11_30.1: type = facet_type <@A, @A(%CC)> [symbolic = %A.type.loc11_30.1 (constants.%A.type.fa003b.2)]
 // CHECK:STDOUT:   %.Self.frozen.loc11_32.1: @C.F.%A.type.loc11_30.1 (%A.type.fa003b.2) = symbolic_binding .Self [symbolic = %.Self.frozen.loc11_32.1 (constants.%.Self.frozen.b15)]
-// CHECK:STDOUT:   %require_complete: <witness> = require_complete_type %A.type.loc11_30.1 [symbolic = %require_complete (constants.%require_complete.792)]
-// CHECK:STDOUT:   %.Self.frozen.as_type: type = facet_access_type %.Self.frozen.loc11_32.1 [symbolic = %.Self.frozen.as_type (constants.%.Self.frozen.as_type)]
-// CHECK:STDOUT:   %A.assoc_type: type = assoc_entity_type @A, @A(%CC) [symbolic = %A.assoc_type (constants.%A.assoc_type.3230b8.2)]
-// CHECK:STDOUT:   %assoc0: @C.F.%A.assoc_type (%A.assoc_type.3230b8.2) = assoc_entity element0, @A.WithSelf.%X [symbolic = %assoc0 (constants.%assoc0.4c905d.2)]
-// CHECK:STDOUT:   %A.lookup_impl_witness.loc11_38.1: <witness> = lookup_impl_witness %.Self.frozen.loc11_32.1, @A, @A(%CC) [symbolic = %A.lookup_impl_witness.loc11_38.1 (constants.%A.lookup_impl_witness.030)]
-// CHECK:STDOUT:   %impl.elem0.loc11_38.1: type = impl_witness_access %A.lookup_impl_witness.loc11_38.1, element0 [symbolic = %impl.elem0.loc11_38.1 (constants.%impl.elem0.fba)]
 // CHECK:STDOUT:   %.Self: @C.F.%A.type.loc11_30.1 (%A.type.fa003b.2) = symbolic_binding .Self [symbolic = %.Self (constants.%.Self.8ed243.1)]
-// CHECK:STDOUT:   %A.lookup_impl_witness.loc11_38.2: <witness> = lookup_impl_witness %.Self, @A, @A(%CC) [symbolic = %A.lookup_impl_witness.loc11_38.2 (constants.%A.lookup_impl_witness.9e772d.1)]
-// CHECK:STDOUT:   %impl.elem0.loc11_38.2: type = impl_witness_access %A.lookup_impl_witness.loc11_38.2, element0 [symbolic = %impl.elem0.loc11_38.2 (constants.%impl.elem0.7f79de.1)]
-// CHECK:STDOUT:   %A_where.type: type = facet_type <@A, @A(%CC) where %impl.elem0.loc11_38.2 = %CC> [symbolic = %A_where.type (constants.%A_where.type.ff151a.1)]
+// CHECK:STDOUT:   %A.lookup_impl_witness: <witness> = lookup_impl_witness %.Self, @A, @A(%CC) [symbolic = %A.lookup_impl_witness (constants.%A.lookup_impl_witness.9e772d.1)]
+// CHECK:STDOUT:   %impl.elem0.loc11_32: type = impl_witness_access %A.lookup_impl_witness, element0 [symbolic = %impl.elem0.loc11_32 (constants.%impl.elem0.7f79de.1)]
+// CHECK:STDOUT:   %A_where.type: type = facet_type <@A, @A(%CC) where %impl.elem0.loc11_32 = %CC> [symbolic = %A_where.type (constants.%A_where.type.ff151a.1)]
 // CHECK:STDOUT:   %pattern_type: type = pattern_type %A_where.type [symbolic = %pattern_type (constants.%pattern_type.957)]
 // CHECK:STDOUT:   %T.patt.loc11_24.2: @C.F.%pattern_type (%pattern_type.957) = symbolic_binding_pattern T, 1 [symbolic = %T.patt.loc11_24.2 (constants.%T.patt.9e9)]
 // CHECK:STDOUT:   %T.loc11_24.1: @C.F.%A_where.type (%A_where.type.ff151a.1) = symbolic_binding T, 1 [symbolic = %T.loc11_24.1 (constants.%T.5e2)]
@@ -249,15 +242,9 @@ fn H(generic T: type) {
 // CHECK:STDOUT:   %CC => constants.%CC
 // CHECK:STDOUT:   %A.type.loc11_30.1 => constants.%A.type.fa003b.2
 // CHECK:STDOUT:   %.Self.frozen.loc11_32.1 => constants.%.Self.frozen.b15
-// CHECK:STDOUT:   %require_complete => constants.%require_complete.792
-// CHECK:STDOUT:   %.Self.frozen.as_type => constants.%.Self.frozen.as_type
-// CHECK:STDOUT:   %A.assoc_type => constants.%A.assoc_type.3230b8.2
-// CHECK:STDOUT:   %assoc0 => constants.%assoc0.4c905d.2
-// CHECK:STDOUT:   %A.lookup_impl_witness.loc11_38.1 => constants.%A.lookup_impl_witness.030
-// CHECK:STDOUT:   %impl.elem0.loc11_38.1 => constants.%impl.elem0.fba
 // CHECK:STDOUT:   %.Self => constants.%.Self.8ed243.1
-// CHECK:STDOUT:   %A.lookup_impl_witness.loc11_38.2 => constants.%A.lookup_impl_witness.9e772d.1
-// CHECK:STDOUT:   %impl.elem0.loc11_38.2 => constants.%impl.elem0.7f79de.1
+// CHECK:STDOUT:   %A.lookup_impl_witness => constants.%A.lookup_impl_witness.9e772d.1
+// CHECK:STDOUT:   %impl.elem0.loc11_32 => constants.%impl.elem0.7f79de.1
 // CHECK:STDOUT:   %A_where.type => constants.%A_where.type.ff151a.1
 // CHECK:STDOUT:   %pattern_type => constants.%pattern_type.957
 // CHECK:STDOUT:   %T.patt.loc11_24.2 => constants.%T.patt.9e9
@@ -334,7 +321,6 @@ fn H(generic T: type) {
 // CHECK:STDOUT:   %B.type.d1b: type = generic_interface_type @B [concrete]
 // CHECK:STDOUT:   %B.generic: %B.type.d1b = struct_value () [concrete]
 // CHECK:STDOUT:   %.Self.frozen.b15: %A.type.fa003b.1 = symbolic_binding .Self [symbolic]
-// CHECK:STDOUT:   %require_complete.792: <witness> = require_complete_type %A.type.fa003b.1 [symbolic]
 // CHECK:STDOUT:   %.Self.frozen.as_type: type = facet_access_type %.Self.frozen.b15 [symbolic]
 // CHECK:STDOUT:   %A.lookup_impl_witness.030: <witness> = lookup_impl_witness %.Self.frozen.b15, @A, @A(%AA) [symbolic]
 // CHECK:STDOUT:   %impl.elem0.fba: type = impl_witness_access %A.lookup_impl_witness.030, element0 [symbolic]
@@ -399,16 +385,16 @@ fn H(generic T: type) {
 // CHECK:STDOUT:       %A.type.loc9_32.1: type = facet_type <@A, @A(constants.%AA)> [symbolic = %A.type.loc9_32.2 (constants.%A.type.fa003b.1)]
 // CHECK:STDOUT:       %.Self.frozen.loc9_34.1: @BB.as_type.as.B.impl.%A.type.loc9_32.2 (%A.type.fa003b.1) = symbolic_binding .Self [symbolic = %.Self.frozen.loc9_34.2 (constants.%.Self.frozen.b15)]
 // CHECK:STDOUT:       %base_facet_type = requirement_base_facet_type %A.type.loc9_32.1 [concrete]
-// CHECK:STDOUT:       %.Self.ref: @BB.as_type.as.B.impl.%A.type.loc9_32.2 (%A.type.fa003b.1) = name_ref .Self, %.Self.frozen.loc9_34.1 [symbolic = %.Self.frozen.loc9_34.2 (constants.%.Self.frozen.b15)]
-// CHECK:STDOUT:       %.Self.as_type: type = facet_access_type %.Self.ref [symbolic = %.Self.frozen.as_type (constants.%.Self.frozen.as_type)]
-// CHECK:STDOUT:       %.loc9_40.1: type = converted %.Self.ref, %.Self.as_type [symbolic = %.Self.frozen.as_type (constants.%.Self.frozen.as_type)]
-// CHECK:STDOUT:       %.loc9_40.2: @BB.as_type.as.B.impl.%A.assoc_type (%A.assoc_type) = specific_constant @X.%assoc0, @A.WithSelf(constants.%AA, constants.%.Self.frozen.b15) [symbolic = %assoc0 (constants.%assoc0)]
-// CHECK:STDOUT:       %X.ref: @BB.as_type.as.B.impl.%A.assoc_type (%A.assoc_type) = name_ref X, %.loc9_40.2 [symbolic = %assoc0 (constants.%assoc0)]
-// CHECK:STDOUT:       %impl.elem0.loc9_40.1: type = impl_witness_access constants.%A.lookup_impl_witness.030, element0 [symbolic = %impl.elem0.loc9_40.3 (constants.%impl.elem0.fba)]
+// CHECK:STDOUT:       %.Self.ref: %A.type.fa003b.1 = name_ref .Self, %.Self.frozen.loc9_34.1 [symbolic = constants.%.Self.frozen.b15]
+// CHECK:STDOUT:       %.Self.as_type: type = facet_access_type %.Self.ref [symbolic = constants.%.Self.frozen.as_type]
+// CHECK:STDOUT:       %.loc9_40.1: type = converted %.Self.ref, %.Self.as_type [symbolic = constants.%.Self.frozen.as_type]
+// CHECK:STDOUT:       %.loc9_40.2: %A.assoc_type = specific_constant @X.%assoc0, @A.WithSelf(constants.%AA, constants.%.Self.frozen.b15) [symbolic = constants.%assoc0]
+// CHECK:STDOUT:       %X.ref: %A.assoc_type = name_ref X, %.loc9_40.2 [symbolic = constants.%assoc0]
+// CHECK:STDOUT:       %impl.elem0.loc9_40.1: type = impl_witness_access constants.%A.lookup_impl_witness.030, element0 [symbolic = constants.%impl.elem0.fba]
 // CHECK:STDOUT:       %.loc9_46.1: %empty_tuple.type = tuple_literal () [concrete = constants.%empty_tuple]
 // CHECK:STDOUT:       %.loc9_46.2: type = converted %.loc9_46.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:       %rewrite.loc9_43.1 = requirement_rewrite %impl.elem0.loc9_40.1, %.loc9_46.2 [concrete]
-// CHECK:STDOUT:       %impl.elem0.loc9_40.2: type = impl_witness_access constants.%A.lookup_impl_witness.9e772d.1, element0 [symbolic = %impl.elem0.loc9_40.4 (constants.%impl.elem0.7f79de.1)]
+// CHECK:STDOUT:       %impl.elem0.loc9_40.2: type = impl_witness_access constants.%A.lookup_impl_witness.9e772d.1, element0 [symbolic = constants.%impl.elem0.7f79de.1]
 // CHECK:STDOUT:       %rewrite.loc9_43.2 = requirement_rewrite %impl.elem0.loc9_40.2, %.loc9_46.2 [concrete]
 // CHECK:STDOUT:       %.loc9_34.2: type = where_expr [symbolic = %A_where.type (constants.%A_where.type.83dbed.1)] {
 // CHECK:STDOUT:         %base_facet_type = requirement_base_facet_type %A.type.loc9_32.1 [concrete]
@@ -425,16 +411,10 @@ fn H(generic T: type) {
 // CHECK:STDOUT:   %AA.loc9_16.2: type = symbolic_binding AA, 0 [symbolic = %AA.loc9_16.2 (constants.%AA)]
 // CHECK:STDOUT:   %A.type.loc9_32.2: type = facet_type <@A, @A(%AA.loc9_16.2)> [symbolic = %A.type.loc9_32.2 (constants.%A.type.fa003b.1)]
 // CHECK:STDOUT:   %.Self.frozen.loc9_34.2: @BB.as_type.as.B.impl.%A.type.loc9_32.2 (%A.type.fa003b.1) = symbolic_binding .Self [symbolic = %.Self.frozen.loc9_34.2 (constants.%.Self.frozen.b15)]
-// CHECK:STDOUT:   %require_complete.loc9_40: <witness> = require_complete_type %A.type.loc9_32.2 [symbolic = %require_complete.loc9_40 (constants.%require_complete.792)]
-// CHECK:STDOUT:   %.Self.frozen.as_type: type = facet_access_type %.Self.frozen.loc9_34.2 [symbolic = %.Self.frozen.as_type (constants.%.Self.frozen.as_type)]
-// CHECK:STDOUT:   %A.assoc_type: type = assoc_entity_type @A, @A(%AA.loc9_16.2) [symbolic = %A.assoc_type (constants.%A.assoc_type)]
-// CHECK:STDOUT:   %assoc0: @BB.as_type.as.B.impl.%A.assoc_type (%A.assoc_type) = assoc_entity element0, @A.WithSelf.%X [symbolic = %assoc0 (constants.%assoc0)]
-// CHECK:STDOUT:   %A.lookup_impl_witness.loc9_40.1: <witness> = lookup_impl_witness %.Self.frozen.loc9_34.2, @A, @A(%AA.loc9_16.2) [symbolic = %A.lookup_impl_witness.loc9_40.1 (constants.%A.lookup_impl_witness.030)]
-// CHECK:STDOUT:   %impl.elem0.loc9_40.3: type = impl_witness_access %A.lookup_impl_witness.loc9_40.1, element0 [symbolic = %impl.elem0.loc9_40.3 (constants.%impl.elem0.fba)]
 // CHECK:STDOUT:   %.Self: @BB.as_type.as.B.impl.%A.type.loc9_32.2 (%A.type.fa003b.1) = symbolic_binding .Self [symbolic = %.Self (constants.%.Self.8ed243.1)]
-// CHECK:STDOUT:   %A.lookup_impl_witness.loc9_40.2: <witness> = lookup_impl_witness %.Self, @A, @A(%AA.loc9_16.2) [symbolic = %A.lookup_impl_witness.loc9_40.2 (constants.%A.lookup_impl_witness.9e772d.1)]
-// CHECK:STDOUT:   %impl.elem0.loc9_40.4: type = impl_witness_access %A.lookup_impl_witness.loc9_40.2, element0 [symbolic = %impl.elem0.loc9_40.4 (constants.%impl.elem0.7f79de.1)]
-// CHECK:STDOUT:   %A_where.type: type = facet_type <@A, @A(%AA.loc9_16.2) where %impl.elem0.loc9_40.4 = constants.%empty_tuple.type> [symbolic = %A_where.type (constants.%A_where.type.83dbed.1)]
+// CHECK:STDOUT:   %A.lookup_impl_witness: <witness> = lookup_impl_witness %.Self, @A, @A(%AA.loc9_16.2) [symbolic = %A.lookup_impl_witness (constants.%A.lookup_impl_witness.9e772d.1)]
+// CHECK:STDOUT:   %impl.elem0.loc9_34: type = impl_witness_access %A.lookup_impl_witness, element0 [symbolic = %impl.elem0.loc9_34 (constants.%impl.elem0.7f79de.1)]
+// CHECK:STDOUT:   %A_where.type: type = facet_type <@A, @A(%AA.loc9_16.2) where %impl.elem0.loc9_34 = constants.%empty_tuple.type> [symbolic = %A_where.type (constants.%A_where.type.83dbed.1)]
 // CHECK:STDOUT:   %pattern_type: type = pattern_type %A_where.type [symbolic = %pattern_type (constants.%pattern_type.9b5)]
 // CHECK:STDOUT:   %BB.patt.loc9_26.2: @BB.as_type.as.B.impl.%pattern_type (%pattern_type.9b5) = symbolic_binding_pattern BB, 1 [symbolic = %BB.patt.loc9_26.2 (constants.%BB.patt.954)]
 // CHECK:STDOUT:   %BB.loc9_26.2: @BB.as_type.as.B.impl.%A_where.type (%A_where.type.83dbed.1) = symbolic_binding BB, 1 [symbolic = %BB.loc9_26.2 (constants.%BB.a11)]
@@ -445,7 +425,7 @@ fn H(generic T: type) {
 // CHECK:STDOUT:   %B.impl_witness.loc9_62.2: <witness> = impl_witness %B.impl_witness_table, @BB.as_type.as.B.impl(%AA.loc9_16.2, %BB.loc9_26.2) [symbolic = %B.impl_witness.loc9_62.2 (constants.%B.impl_witness.089)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
-// CHECK:STDOUT:   %require_complete.loc9_60: <witness> = require_complete_type %B.type.loc9_60.2 [symbolic = %require_complete.loc9_60 (constants.%require_complete.58dcfe.1)]
+// CHECK:STDOUT:   %require_complete: <witness> = require_complete_type %B.type.loc9_60.2 [symbolic = %require_complete (constants.%require_complete.58dcfe.1)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   impl: %.loc9_49 as %B.type.loc9_60.1 {
 // CHECK:STDOUT:     %B.impl_witness_table = impl_witness_table (), @BB.as_type.as.B.impl [concrete]
@@ -505,15 +485,9 @@ fn H(generic T: type) {
 // CHECK:STDOUT:   %AA.loc9_16.2 => constants.%AA
 // CHECK:STDOUT:   %A.type.loc9_32.2 => constants.%A.type.fa003b.1
 // CHECK:STDOUT:   %.Self.frozen.loc9_34.2 => constants.%.Self.frozen.b15
-// CHECK:STDOUT:   %require_complete.loc9_40 => constants.%require_complete.792
-// CHECK:STDOUT:   %.Self.frozen.as_type => constants.%.Self.frozen.as_type
-// CHECK:STDOUT:   %A.assoc_type => constants.%A.assoc_type
-// CHECK:STDOUT:   %assoc0 => constants.%assoc0
-// CHECK:STDOUT:   %A.lookup_impl_witness.loc9_40.1 => constants.%A.lookup_impl_witness.030
-// CHECK:STDOUT:   %impl.elem0.loc9_40.3 => constants.%impl.elem0.fba
 // CHECK:STDOUT:   %.Self => constants.%.Self.8ed243.1
-// CHECK:STDOUT:   %A.lookup_impl_witness.loc9_40.2 => constants.%A.lookup_impl_witness.9e772d.1
-// CHECK:STDOUT:   %impl.elem0.loc9_40.4 => constants.%impl.elem0.7f79de.1
+// CHECK:STDOUT:   %A.lookup_impl_witness => constants.%A.lookup_impl_witness.9e772d.1
+// CHECK:STDOUT:   %impl.elem0.loc9_34 => constants.%impl.elem0.7f79de.1
 // CHECK:STDOUT:   %A_where.type => constants.%A_where.type.83dbed.1
 // CHECK:STDOUT:   %pattern_type => constants.%pattern_type.9b5
 // CHECK:STDOUT:   %BB.patt.loc9_26.2 => constants.%BB.patt.954

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

@@ -117,7 +117,6 @@ fn F() {
 // CHECK:STDOUT:   %Y.assoc_type.edf: type = assoc_entity_type @Y, @Y(%OuterParam) [symbolic]
 // CHECK:STDOUT:   %assoc0.05f: %Y.assoc_type.edf = assoc_entity element0, @Y.WithSelf.%T [symbolic]
 // CHECK:STDOUT:   %.Self.frozen.b95: %Y.type.eff = symbolic_binding .Self [symbolic]
-// CHECK:STDOUT:   %require_complete: <witness> = require_complete_type %Y.type.eff [symbolic]
 // CHECK:STDOUT:   %.Self.frozen.as_type.55f: type = facet_access_type %.Self.frozen.b95 [symbolic]
 // CHECK:STDOUT:   %Y.lookup_impl_witness.eba: <witness> = lookup_impl_witness %.Self.frozen.b95, @Y, @Y(%OuterParam) [symbolic]
 // CHECK:STDOUT:   %impl.elem0.29d: type = impl_witness_access %Y.lookup_impl_witness.eba, element0 [symbolic]
@@ -132,7 +131,7 @@ fn F() {
 // CHECK:STDOUT:   %Outer.G.type.c4a: type = fn_type @Outer.G, @Outer(%OuterParam) [symbolic]
 // CHECK:STDOUT:   %Outer.G.5d7: %Outer.G.type.c4a = struct_value () [symbolic]
 // CHECK:STDOUT:   %empty_struct_type: type = struct_type {} [concrete]
-// CHECK:STDOUT:   %complete_type.357: <witness> = complete_type_witness %empty_struct_type [concrete]
+// CHECK:STDOUT:   %complete_type: <witness> = complete_type_witness %empty_struct_type [concrete]
 // CHECK:STDOUT:   %C: type = class_type @C [concrete]
 // CHECK:STDOUT:   %Outer.b30: type = class_type @Outer, @Outer(%empty_tuple.type) [concrete]
 // CHECK:STDOUT:   %Y.type.d7b: type = facet_type <@Y, @Y(%empty_tuple.type)> [concrete]
@@ -158,9 +157,6 @@ fn F() {
 // CHECK:STDOUT:   %impl.elem0.b95: type = impl_witness_access %Y.lookup_impl_witness.b19, element0 [symbolic_self]
 // CHECK:STDOUT:   %Y_where.type.6ce: type = facet_type <@Y, @Y(%empty_tuple.type) where %impl.elem0.b95 = %empty_tuple.type> [concrete]
 // CHECK:STDOUT:   %facet_value: %Y_where.type.6ce = facet_value %C, (%Y.impl_witness) [concrete]
-// CHECK:STDOUT:   %complete_type.2cf: <witness> = complete_type_witness %Y.type.d7b [concrete]
-// CHECK:STDOUT:   %Y.lookup_impl_witness.e35: <witness> = lookup_impl_witness %.Self.frozen.62f, @Y, @Y(%empty_tuple.type) [symbolic_self]
-// CHECK:STDOUT:   %impl.elem0.798: type = impl_witness_access %Y.lookup_impl_witness.e35, element0 [symbolic_self]
 // CHECK:STDOUT:   %pattern_type.f97: type = pattern_type %Y_where.type.6ce [concrete]
 // CHECK:STDOUT:   %H.patt.7ee: %pattern_type.f97 = symbolic_binding_pattern H, 1 [symbolic]
 // CHECK:STDOUT:   %Outer.G.specific_fn: <specific function> = specific_function %Outer.G.371, @Outer.G(%empty_tuple.type, %facet_value) [concrete]
@@ -275,25 +271,25 @@ fn F() {
 // CHECK:STDOUT:         %Y.ref: type = name_ref Y, %.loc54_26 [symbolic = %Y.type (constants.%Y.type.eff)]
 // CHECK:STDOUT:         %.Self.frozen.loc54_28.2: @Outer.G.%Y.type (%Y.type.eff) = symbolic_binding .Self [symbolic = %.Self.frozen.loc54_28.1 (constants.%.Self.frozen.b95)]
 // CHECK:STDOUT:         %base_facet_type = requirement_base_facet_type %Y.ref [concrete]
-// CHECK:STDOUT:         %.Self.ref: @Outer.G.%Y.type (%Y.type.eff) = name_ref .Self, %.Self.frozen.loc54_28.2 [symbolic = %.Self.frozen.loc54_28.1 (constants.%.Self.frozen.b95)]
-// CHECK:STDOUT:         %.Self.as_type: type = facet_access_type %.Self.ref [symbolic = %.Self.frozen.as_type (constants.%.Self.frozen.as_type.55f)]
-// CHECK:STDOUT:         %.loc54_34.1: type = converted %.Self.ref, %.Self.as_type [symbolic = %.Self.frozen.as_type (constants.%.Self.frozen.as_type.55f)]
-// CHECK:STDOUT:         %.loc54_34.2: @Outer.G.%Y.assoc_type (%Y.assoc_type.edf) = specific_constant @T.%assoc0, @Y.WithSelf(constants.%OuterParam, constants.%.Self.frozen.b95) [symbolic = %assoc0 (constants.%assoc0.05f)]
-// CHECK:STDOUT:         %T.ref: @Outer.G.%Y.assoc_type (%Y.assoc_type.edf) = name_ref T, %.loc54_34.2 [symbolic = %assoc0 (constants.%assoc0.05f)]
-// CHECK:STDOUT:         %impl.elem0.loc54_34.3: type = impl_witness_access constants.%Y.lookup_impl_witness.eba, element0 [symbolic = %impl.elem0.loc54_34.1 (constants.%impl.elem0.29d)]
+// CHECK:STDOUT:         %.Self.ref: %Y.type.eff = name_ref .Self, %.Self.frozen.loc54_28.2 [symbolic = constants.%.Self.frozen.b95]
+// CHECK:STDOUT:         %.Self.as_type: type = facet_access_type %.Self.ref [symbolic = constants.%.Self.frozen.as_type.55f]
+// CHECK:STDOUT:         %.loc54_34.1: type = converted %.Self.ref, %.Self.as_type [symbolic = constants.%.Self.frozen.as_type.55f]
+// CHECK:STDOUT:         %.loc54_34.2: %Y.assoc_type.edf = specific_constant @T.%assoc0, @Y.WithSelf(constants.%OuterParam, constants.%.Self.frozen.b95) [symbolic = constants.%assoc0.05f]
+// CHECK:STDOUT:         %T.ref: %Y.assoc_type.edf = name_ref T, %.loc54_34.2 [symbolic = constants.%assoc0.05f]
+// CHECK:STDOUT:         %impl.elem0.loc54_34.1: type = impl_witness_access constants.%Y.lookup_impl_witness.eba, element0 [symbolic = constants.%impl.elem0.29d]
 // CHECK:STDOUT:         %.loc54_40.1: %empty_tuple.type = tuple_literal () [concrete = constants.%empty_tuple]
 // CHECK:STDOUT:         %.loc54_40.2: type = converted %.loc54_40.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
-// CHECK:STDOUT:         %rewrite.loc54_37.1 = requirement_rewrite %impl.elem0.loc54_34.3, %.loc54_40.2 [concrete]
-// CHECK:STDOUT:         %impl.elem0.loc54_34.4: type = impl_witness_access constants.%Y.lookup_impl_witness.f46, element0 [symbolic = %impl.elem0.loc54_34.2 (constants.%impl.elem0.d7a)]
-// CHECK:STDOUT:         %rewrite.loc54_37.2 = requirement_rewrite %impl.elem0.loc54_34.4, %.loc54_40.2 [concrete]
+// CHECK:STDOUT:         %rewrite.loc54_37.1 = requirement_rewrite %impl.elem0.loc54_34.1, %.loc54_40.2 [concrete]
+// CHECK:STDOUT:         %impl.elem0.loc54_34.2: type = impl_witness_access constants.%Y.lookup_impl_witness.f46, element0 [symbolic = constants.%impl.elem0.d7a]
+// CHECK:STDOUT:         %rewrite.loc54_37.2 = requirement_rewrite %impl.elem0.loc54_34.2, %.loc54_40.2 [concrete]
 // CHECK:STDOUT:         %.loc54_28.2: type = where_expr [symbolic = %Y_where.type (constants.%Y_where.type.fa0)] {
 // CHECK:STDOUT:           %base_facet_type = requirement_base_facet_type %Y.ref [concrete]
-// CHECK:STDOUT:           %rewrite.loc54_37.2 = requirement_rewrite %impl.elem0.loc54_34.4, %.loc54_40.2 [concrete]
+// CHECK:STDOUT:           %rewrite.loc54_37.2 = requirement_rewrite %impl.elem0.loc54_34.2, %.loc54_40.2 [concrete]
 // CHECK:STDOUT:         }
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:       %H.loc54_24.2: @Outer.G.%Y_where.type (%Y_where.type.fa0) = symbolic_binding H, 1 [symbolic = %H.loc54_24.1 (constants.%H)]
 // CHECK:STDOUT:     }
-// CHECK:STDOUT:     %complete_type: <witness> = complete_type_witness constants.%empty_struct_type [concrete = constants.%complete_type.357]
+// CHECK:STDOUT:     %complete_type: <witness> = complete_type_witness constants.%empty_struct_type [concrete = constants.%complete_type]
 // CHECK:STDOUT:     complete_type_witness = %complete_type
 // CHECK:STDOUT:
 // CHECK:STDOUT:   !members:
@@ -309,16 +305,10 @@ fn F() {
 // CHECK:STDOUT:   %OuterParam: type = symbolic_binding OuterParam, 0 [symbolic = %OuterParam (constants.%OuterParam)]
 // CHECK:STDOUT:   %Y.type: type = facet_type <@Y, @Y(%OuterParam)> [symbolic = %Y.type (constants.%Y.type.eff)]
 // CHECK:STDOUT:   %.Self.frozen.loc54_28.1: @Outer.G.%Y.type (%Y.type.eff) = symbolic_binding .Self [symbolic = %.Self.frozen.loc54_28.1 (constants.%.Self.frozen.b95)]
-// CHECK:STDOUT:   %require_complete: <witness> = require_complete_type %Y.type [symbolic = %require_complete (constants.%require_complete)]
-// CHECK:STDOUT:   %.Self.frozen.as_type: type = facet_access_type %.Self.frozen.loc54_28.1 [symbolic = %.Self.frozen.as_type (constants.%.Self.frozen.as_type.55f)]
-// CHECK:STDOUT:   %Y.assoc_type: type = assoc_entity_type @Y, @Y(%OuterParam) [symbolic = %Y.assoc_type (constants.%Y.assoc_type.edf)]
-// CHECK:STDOUT:   %assoc0: @Outer.G.%Y.assoc_type (%Y.assoc_type.edf) = assoc_entity element0, @Y.WithSelf.%T [symbolic = %assoc0 (constants.%assoc0.05f)]
-// CHECK:STDOUT:   %Y.lookup_impl_witness.loc54_34.1: <witness> = lookup_impl_witness %.Self.frozen.loc54_28.1, @Y, @Y(%OuterParam) [symbolic = %Y.lookup_impl_witness.loc54_34.1 (constants.%Y.lookup_impl_witness.eba)]
-// CHECK:STDOUT:   %impl.elem0.loc54_34.1: type = impl_witness_access %Y.lookup_impl_witness.loc54_34.1, element0 [symbolic = %impl.elem0.loc54_34.1 (constants.%impl.elem0.29d)]
 // CHECK:STDOUT:   %.Self: @Outer.G.%Y.type (%Y.type.eff) = symbolic_binding .Self [symbolic = %.Self (constants.%.Self.273)]
-// CHECK:STDOUT:   %Y.lookup_impl_witness.loc54_34.2: <witness> = lookup_impl_witness %.Self, @Y, @Y(%OuterParam) [symbolic = %Y.lookup_impl_witness.loc54_34.2 (constants.%Y.lookup_impl_witness.f46)]
-// CHECK:STDOUT:   %impl.elem0.loc54_34.2: type = impl_witness_access %Y.lookup_impl_witness.loc54_34.2, element0 [symbolic = %impl.elem0.loc54_34.2 (constants.%impl.elem0.d7a)]
-// CHECK:STDOUT:   %Y_where.type: type = facet_type <@Y, @Y(%OuterParam) where %impl.elem0.loc54_34.2 = constants.%empty_tuple.type> [symbolic = %Y_where.type (constants.%Y_where.type.fa0)]
+// CHECK:STDOUT:   %Y.lookup_impl_witness: <witness> = lookup_impl_witness %.Self, @Y, @Y(%OuterParam) [symbolic = %Y.lookup_impl_witness (constants.%Y.lookup_impl_witness.f46)]
+// CHECK:STDOUT:   %impl.elem0.loc54_28: type = impl_witness_access %Y.lookup_impl_witness, element0 [symbolic = %impl.elem0.loc54_28 (constants.%impl.elem0.d7a)]
+// CHECK:STDOUT:   %Y_where.type: type = facet_type <@Y, @Y(%OuterParam) where %impl.elem0.loc54_28 = constants.%empty_tuple.type> [symbolic = %Y_where.type (constants.%Y_where.type.fa0)]
 // CHECK:STDOUT:   %pattern_type: type = pattern_type %Y_where.type [symbolic = %pattern_type (constants.%pattern_type.b98)]
 // CHECK:STDOUT:   %H.patt.loc54_24.2: @Outer.G.%pattern_type (%pattern_type.b98) = symbolic_binding_pattern H, 1 [symbolic = %H.patt.loc54_24.2 (constants.%H.patt.314)]
 // CHECK:STDOUT:   %H.loc54_24.1: @Outer.G.%Y_where.type (%Y_where.type.fa0) = symbolic_binding H, 1 [symbolic = %H.loc54_24.1 (constants.%H)]
@@ -382,15 +372,9 @@ fn F() {
 // CHECK:STDOUT:   %OuterParam => constants.%OuterParam
 // CHECK:STDOUT:   %Y.type => constants.%Y.type.eff
 // CHECK:STDOUT:   %.Self.frozen.loc54_28.1 => constants.%.Self.frozen.b95
-// CHECK:STDOUT:   %require_complete => constants.%require_complete
-// CHECK:STDOUT:   %.Self.frozen.as_type => constants.%.Self.frozen.as_type.55f
-// CHECK:STDOUT:   %Y.assoc_type => constants.%Y.assoc_type.edf
-// CHECK:STDOUT:   %assoc0 => constants.%assoc0.05f
-// CHECK:STDOUT:   %Y.lookup_impl_witness.loc54_34.1 => constants.%Y.lookup_impl_witness.eba
-// CHECK:STDOUT:   %impl.elem0.loc54_34.1 => constants.%impl.elem0.29d
 // CHECK:STDOUT:   %.Self => constants.%.Self.273
-// CHECK:STDOUT:   %Y.lookup_impl_witness.loc54_34.2 => constants.%Y.lookup_impl_witness.f46
-// CHECK:STDOUT:   %impl.elem0.loc54_34.2 => constants.%impl.elem0.d7a
+// CHECK:STDOUT:   %Y.lookup_impl_witness => constants.%Y.lookup_impl_witness.f46
+// CHECK:STDOUT:   %impl.elem0.loc54_28 => constants.%impl.elem0.d7a
 // CHECK:STDOUT:   %Y_where.type => constants.%Y_where.type.fa0
 // CHECK:STDOUT:   %pattern_type => constants.%pattern_type.b98
 // CHECK:STDOUT:   %H.patt.loc54_24.2 => constants.%H.patt.314
@@ -439,15 +423,9 @@ fn F() {
 // CHECK:STDOUT:   %OuterParam => constants.%empty_tuple.type
 // CHECK:STDOUT:   %Y.type => constants.%Y.type.d7b
 // CHECK:STDOUT:   %.Self.frozen.loc54_28.1 => constants.%.Self.frozen.62f
-// CHECK:STDOUT:   %require_complete => constants.%complete_type.2cf
-// CHECK:STDOUT:   %.Self.frozen.as_type => constants.%.Self.frozen.as_type.a06
-// CHECK:STDOUT:   %Y.assoc_type => constants.%Y.assoc_type.7d9
-// CHECK:STDOUT:   %assoc0 => constants.%assoc0.559
-// CHECK:STDOUT:   %Y.lookup_impl_witness.loc54_34.1 => constants.%Y.lookup_impl_witness.e35
-// CHECK:STDOUT:   %impl.elem0.loc54_34.1 => constants.%impl.elem0.798
 // CHECK:STDOUT:   %.Self => constants.%.Self.37b
-// CHECK:STDOUT:   %Y.lookup_impl_witness.loc54_34.2 => constants.%Y.lookup_impl_witness.b19
-// CHECK:STDOUT:   %impl.elem0.loc54_34.2 => constants.%impl.elem0.b95
+// CHECK:STDOUT:   %Y.lookup_impl_witness => constants.%Y.lookup_impl_witness.b19
+// CHECK:STDOUT:   %impl.elem0.loc54_28 => constants.%impl.elem0.b95
 // CHECK:STDOUT:   %Y_where.type => constants.%Y_where.type.6ce
 // CHECK:STDOUT:   %pattern_type => constants.%pattern_type.f97
 // CHECK:STDOUT:   %H.patt.loc54_24.2 => constants.%H.patt.7ee
@@ -478,7 +456,7 @@ fn F() {
 // CHECK:STDOUT:   %assoc0.b45: %Y.assoc_type.5d5 = assoc_entity element0, @Y.WithSelf.%T [symbolic]
 // CHECK:STDOUT:   %.Self.frozen.39e: %Y.type.9a0 = symbolic_binding .Self [symbolic]
 // CHECK:STDOUT:   %require_complete: <witness> = require_complete_type %Y.type.9a0 [symbolic]
-// CHECK:STDOUT:   %.Self.frozen.as_type.618: type = facet_access_type %.Self.frozen.39e [symbolic]
+// CHECK:STDOUT:   %.Self.frozen.as_type: type = facet_access_type %.Self.frozen.39e [symbolic]
 // CHECK:STDOUT:   %Y.lookup_impl_witness.580: <witness> = lookup_impl_witness %.Self.frozen.39e, @Y, @Y(%OuterParam) [symbolic]
 // CHECK:STDOUT:   %impl.elem0.be8: type = impl_witness_access %Y.lookup_impl_witness.580, element0 [symbolic]
 // CHECK:STDOUT:   %empty_tuple: %empty_tuple.type = tuple_value () [concrete]
@@ -532,21 +510,16 @@ fn F() {
 // CHECK:STDOUT:   %impl.elem0.186: type = impl_witness_access %Y.lookup_impl_witness.0bd, element0 [symbolic_self]
 // CHECK:STDOUT:   %Y_where.type.677: type = facet_type <@Y, @Y(%Z1.facet) where %impl.elem0.186 = %empty_tuple.type> [concrete]
 // CHECK:STDOUT:   %.Self.frozen.126: %Y.type.30f = symbolic_binding .Self [symbolic_self]
-// CHECK:STDOUT:   %Self.4a2: %Y.type.30f = symbolic_binding Self, 1 [symbolic]
-// CHECK:STDOUT:   %Y.assoc_type.104: type = assoc_entity_type @Y, @Y(%Z1.facet) [concrete]
-// CHECK:STDOUT:   %assoc0.2bd: %Y.assoc_type.104 = assoc_entity element0, @Y.WithSelf.%T [concrete]
-// CHECK:STDOUT:   %complete_type.d0d: <witness> = complete_type_witness %Y.type.30f [concrete]
-// CHECK:STDOUT:   %.Self.frozen.as_type.746: type = facet_access_type %.Self.frozen.126 [symbolic_self]
-// CHECK:STDOUT:   %.03e: <witness> = impl_self_witness %.Self.frozen.126, @Y, @Y(%Z1.facet) [symbolic_self]
-// CHECK:STDOUT:   %impl.elem0.ad3: type = impl_witness_access %.03e, element0 [symbolic_self]
 // CHECK:STDOUT:   %.4bb: <witness> = impl_self_witness %.Self.1da, @Y, @Y(%Z1.facet) [symbolic_self]
 // CHECK:STDOUT:   %impl.elem0.eb1: type = impl_witness_access %.4bb, element0 [symbolic_self]
 // CHECK:STDOUT:   %Y_where.type.d3d: type = facet_type <@Y, @Y(%Z1.facet) where %impl.elem0.eb1 = %empty_tuple.type> [concrete]
 // CHECK:STDOUT:   %.9bc: <witness> = impl_self_witness %C.d9e, @Y, @Y(%Z1.facet) [concrete]
 // CHECK:STDOUT:   %Y.impl_witness.1b2: <witness> = impl_witness @C.as.Y.impl.%Y.impl_witness_table, @C.as.Y.impl(%Z1.facet) [concrete]
+// CHECK:STDOUT:   %Self.4a2: %Y.type.30f = symbolic_binding Self, 1 [symbolic]
+// CHECK:STDOUT:   %Y.assoc_type.104: type = assoc_entity_type @Y, @Y(%Z1.facet) [concrete]
+// CHECK:STDOUT:   %assoc0.2bd: %Y.assoc_type.104 = assoc_entity element0, @Y.WithSelf.%T [concrete]
+// CHECK:STDOUT:   %complete_type.d0d: <witness> = complete_type_witness %Y.type.30f [concrete]
 // CHECK:STDOUT:   %facet_value.c7c: %Y_where.type.677 = facet_value %C.d9e, (%Y.impl_witness.1b2) [concrete]
-// CHECK:STDOUT:   %Y.lookup_impl_witness.a66: <witness> = lookup_impl_witness %.Self.frozen.126, @Y, @Y(%Z1.facet) [symbolic_self]
-// CHECK:STDOUT:   %impl.elem0.e0b: type = impl_witness_access %Y.lookup_impl_witness.a66, element0 [symbolic_self]
 // CHECK:STDOUT:   %pattern_type.285: type = pattern_type %Y_where.type.677 [concrete]
 // CHECK:STDOUT:   %H.patt.305: %pattern_type.285 = symbolic_binding_pattern H, 1 [symbolic]
 // CHECK:STDOUT:   %Outer.G.specific_fn: <specific function> = specific_function %Outer.G.550, @Outer.G(%Z1.facet, %facet_value.c7c) [concrete]
@@ -649,20 +622,15 @@ fn F() {
 // CHECK:STDOUT:   %C: type = class_type @C, @C(%OuterParam) [symbolic = %C (constants.%C.5f2)]
 // CHECK:STDOUT:   %Y.type: type = facet_type <@Y, @Y(%OuterParam)> [symbolic = %Y.type (constants.%Y.type.9a0)]
 // CHECK:STDOUT:   %.Self.frozen.loc14_15.2: @C.as.Y.impl.%Y.type (%Y.type.9a0) = symbolic_binding .Self [symbolic = %.Self.frozen.loc14_15.2 (constants.%.Self.frozen.39e)]
-// CHECK:STDOUT:   %require_complete: <witness> = require_complete_type %Y.type [symbolic = %require_complete (constants.%require_complete)]
-// CHECK:STDOUT:   %.Self.frozen.as_type: type = facet_access_type %.Self.frozen.loc14_15.2 [symbolic = %.Self.frozen.as_type (constants.%.Self.frozen.as_type.618)]
-// CHECK:STDOUT:   %Y.assoc_type: type = assoc_entity_type @Y, @Y(%OuterParam) [symbolic = %Y.assoc_type (constants.%Y.assoc_type.5d5)]
-// CHECK:STDOUT:   %assoc0: @C.as.Y.impl.%Y.assoc_type (%Y.assoc_type.5d5) = assoc_entity element0, @Y.WithSelf.%T [symbolic = %assoc0 (constants.%assoc0.b45)]
-// CHECK:STDOUT:   %.loc14_21.3: <witness> = impl_self_witness %.Self.frozen.loc14_15.2, @Y, @Y(%OuterParam) [symbolic = %.loc14_21.3 (constants.%.eeb)]
-// CHECK:STDOUT:   %impl.elem0.loc14_21.3: type = impl_witness_access %.loc14_21.3, element0 [symbolic = %impl.elem0.loc14_21.3 (constants.%impl.elem0.756)]
 // CHECK:STDOUT:   %.Self: @C.as.Y.impl.%Y.type (%Y.type.9a0) = symbolic_binding .Self [symbolic = %.Self (constants.%.Self.2b6)]
-// CHECK:STDOUT:   %.loc14_21.4: <witness> = impl_self_witness %.Self, @Y, @Y(%OuterParam) [symbolic = %.loc14_21.4 (constants.%.66e)]
-// CHECK:STDOUT:   %impl.elem0.loc14_21.4: type = impl_witness_access %.loc14_21.4, element0 [symbolic = %impl.elem0.loc14_21.4 (constants.%impl.elem0.295)]
-// CHECK:STDOUT:   %Y_where.type: type = facet_type <@Y, @Y(%OuterParam) where %impl.elem0.loc14_21.4 = constants.%empty_tuple.type> [symbolic = %Y_where.type (constants.%Y_where.type.aa4)]
+// CHECK:STDOUT:   %.loc14_15.2: <witness> = impl_self_witness %.Self, @Y, @Y(%OuterParam) [symbolic = %.loc14_15.2 (constants.%.66e)]
+// CHECK:STDOUT:   %impl.elem0.loc14_15: type = impl_witness_access %.loc14_15.2, element0 [symbolic = %impl.elem0.loc14_15 (constants.%impl.elem0.295)]
+// CHECK:STDOUT:   %Y_where.type: type = facet_type <@Y, @Y(%OuterParam) where %impl.elem0.loc14_15 = constants.%empty_tuple.type> [symbolic = %Y_where.type (constants.%Y_where.type.aa4)]
 // CHECK:STDOUT:   %.loc14_29: <witness> = impl_self_witness %C, @Y, @Y(%OuterParam) [symbolic = %.loc14_29 (constants.%.6b3)]
 // CHECK:STDOUT:   %Y.impl_witness.loc14_29.2: <witness> = impl_witness %Y.impl_witness_table, @C.as.Y.impl(%OuterParam) [symbolic = %Y.impl_witness.loc14_29.2 (constants.%Y.impl_witness.d75)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
+// CHECK:STDOUT:   %require_complete: <witness> = require_complete_type %Y.type [symbolic = %require_complete (constants.%require_complete)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   impl: %C.ref as %Y.ref {
 // CHECK:STDOUT:     %Y.impl_witness_table = impl_witness_table (%impl_witness_assoc_constant), @C.as.Y.impl [concrete]
@@ -714,20 +682,20 @@ fn F() {
 // CHECK:STDOUT:         %Y.ref: type = name_ref Y, %.loc11_26 [symbolic = %Y.type (constants.%Y.type.9a0)]
 // CHECK:STDOUT:         %.Self.frozen.loc11_28.2: @Outer.G.%Y.type (%Y.type.9a0) = symbolic_binding .Self [symbolic = %.Self.frozen.loc11_28.1 (constants.%.Self.frozen.39e)]
 // CHECK:STDOUT:         %base_facet_type = requirement_base_facet_type %Y.ref [concrete]
-// CHECK:STDOUT:         %.Self.ref: @Outer.G.%Y.type (%Y.type.9a0) = name_ref .Self, %.Self.frozen.loc11_28.2 [symbolic = %.Self.frozen.loc11_28.1 (constants.%.Self.frozen.39e)]
-// CHECK:STDOUT:         %.Self.as_type: type = facet_access_type %.Self.ref [symbolic = %.Self.frozen.as_type (constants.%.Self.frozen.as_type.618)]
-// CHECK:STDOUT:         %.loc11_34.1: type = converted %.Self.ref, %.Self.as_type [symbolic = %.Self.frozen.as_type (constants.%.Self.frozen.as_type.618)]
-// CHECK:STDOUT:         %.loc11_34.2: @Outer.G.%Y.assoc_type (%Y.assoc_type.5d5) = specific_constant @T.%assoc0, @Y.WithSelf(constants.%OuterParam, constants.%.Self.frozen.39e) [symbolic = %assoc0 (constants.%assoc0.b45)]
-// CHECK:STDOUT:         %T.ref: @Outer.G.%Y.assoc_type (%Y.assoc_type.5d5) = name_ref T, %.loc11_34.2 [symbolic = %assoc0 (constants.%assoc0.b45)]
-// CHECK:STDOUT:         %impl.elem0.loc11_34.3: type = impl_witness_access constants.%Y.lookup_impl_witness.580, element0 [symbolic = %impl.elem0.loc11_34.1 (constants.%impl.elem0.be8)]
+// CHECK:STDOUT:         %.Self.ref: %Y.type.9a0 = name_ref .Self, %.Self.frozen.loc11_28.2 [symbolic = constants.%.Self.frozen.39e]
+// CHECK:STDOUT:         %.Self.as_type: type = facet_access_type %.Self.ref [symbolic = constants.%.Self.frozen.as_type]
+// CHECK:STDOUT:         %.loc11_34.1: type = converted %.Self.ref, %.Self.as_type [symbolic = constants.%.Self.frozen.as_type]
+// CHECK:STDOUT:         %.loc11_34.2: %Y.assoc_type.5d5 = specific_constant @T.%assoc0, @Y.WithSelf(constants.%OuterParam, constants.%.Self.frozen.39e) [symbolic = constants.%assoc0.b45]
+// CHECK:STDOUT:         %T.ref: %Y.assoc_type.5d5 = name_ref T, %.loc11_34.2 [symbolic = constants.%assoc0.b45]
+// CHECK:STDOUT:         %impl.elem0.loc11_34.1: type = impl_witness_access constants.%Y.lookup_impl_witness.580, element0 [symbolic = constants.%impl.elem0.be8]
 // CHECK:STDOUT:         %.loc11_40.1: %empty_tuple.type = tuple_literal () [concrete = constants.%empty_tuple]
 // CHECK:STDOUT:         %.loc11_40.2: type = converted %.loc11_40.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
-// CHECK:STDOUT:         %rewrite.loc11_37.1 = requirement_rewrite %impl.elem0.loc11_34.3, %.loc11_40.2 [concrete]
-// CHECK:STDOUT:         %impl.elem0.loc11_34.4: type = impl_witness_access constants.%Y.lookup_impl_witness.00e, element0 [symbolic = %impl.elem0.loc11_34.2 (constants.%impl.elem0.43a)]
-// CHECK:STDOUT:         %rewrite.loc11_37.2 = requirement_rewrite %impl.elem0.loc11_34.4, %.loc11_40.2 [concrete]
+// CHECK:STDOUT:         %rewrite.loc11_37.1 = requirement_rewrite %impl.elem0.loc11_34.1, %.loc11_40.2 [concrete]
+// CHECK:STDOUT:         %impl.elem0.loc11_34.2: type = impl_witness_access constants.%Y.lookup_impl_witness.00e, element0 [symbolic = constants.%impl.elem0.43a]
+// CHECK:STDOUT:         %rewrite.loc11_37.2 = requirement_rewrite %impl.elem0.loc11_34.2, %.loc11_40.2 [concrete]
 // CHECK:STDOUT:         %.loc11_28.2: type = where_expr [symbolic = %Y_where.type (constants.%Y_where.type.352)] {
 // CHECK:STDOUT:           %base_facet_type = requirement_base_facet_type %Y.ref [concrete]
-// CHECK:STDOUT:           %rewrite.loc11_37.2 = requirement_rewrite %impl.elem0.loc11_34.4, %.loc11_40.2 [concrete]
+// CHECK:STDOUT:           %rewrite.loc11_37.2 = requirement_rewrite %impl.elem0.loc11_34.2, %.loc11_40.2 [concrete]
 // CHECK:STDOUT:         }
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:       %H.loc11_24.2: @Outer.G.%Y_where.type (%Y_where.type.352) = symbolic_binding H, 1 [symbolic = %H.loc11_24.1 (constants.%H)]
@@ -740,18 +708,18 @@ fn F() {
 // CHECK:STDOUT:       %Y.ref: type = name_ref Y, %.loc14_13 [symbolic = %Y.type (constants.%Y.type.9a0)]
 // CHECK:STDOUT:       %.Self.frozen.loc14_15.1: @C.as.Y.impl.%Y.type (%Y.type.9a0) = symbolic_binding .Self [symbolic = %.Self.frozen.loc14_15.2 (constants.%.Self.frozen.39e)]
 // CHECK:STDOUT:       %base_facet_type = requirement_base_facet_type %Y.ref [concrete]
-// CHECK:STDOUT:       %.Self.ref: @C.as.Y.impl.%Y.type (%Y.type.9a0) = name_ref .Self, %.Self.frozen.loc14_15.1 [symbolic = %.Self.frozen.loc14_15.2 (constants.%.Self.frozen.39e)]
-// CHECK:STDOUT:       %.Self.as_type: type = facet_access_type %.Self.ref [symbolic = %.Self.frozen.as_type (constants.%.Self.frozen.as_type.618)]
-// CHECK:STDOUT:       %.loc14_21.1: type = converted %.Self.ref, %.Self.as_type [symbolic = %.Self.frozen.as_type (constants.%.Self.frozen.as_type.618)]
-// CHECK:STDOUT:       %.loc14_21.2: @C.as.Y.impl.%Y.assoc_type (%Y.assoc_type.5d5) = specific_constant @T.%assoc0, @Y.WithSelf(constants.%OuterParam, constants.%.Self.frozen.39e) [symbolic = %assoc0 (constants.%assoc0.b45)]
-// CHECK:STDOUT:       %T.ref: @C.as.Y.impl.%Y.assoc_type (%Y.assoc_type.5d5) = name_ref T, %.loc14_21.2 [symbolic = %assoc0 (constants.%assoc0.b45)]
-// CHECK:STDOUT:       %impl.elem0.loc14_21.1: type = impl_witness_access constants.%.eeb, element0 [symbolic = %impl.elem0.loc14_21.3 (constants.%impl.elem0.756)]
+// CHECK:STDOUT:       %.Self.ref: %Y.type.9a0 = name_ref .Self, %.Self.frozen.loc14_15.1 [symbolic = constants.%.Self.frozen.39e]
+// CHECK:STDOUT:       %.Self.as_type: type = facet_access_type %.Self.ref [symbolic = constants.%.Self.frozen.as_type]
+// CHECK:STDOUT:       %.loc14_21.1: type = converted %.Self.ref, %.Self.as_type [symbolic = constants.%.Self.frozen.as_type]
+// CHECK:STDOUT:       %.loc14_21.2: %Y.assoc_type.5d5 = specific_constant @T.%assoc0, @Y.WithSelf(constants.%OuterParam, constants.%.Self.frozen.39e) [symbolic = constants.%assoc0.b45]
+// CHECK:STDOUT:       %T.ref: %Y.assoc_type.5d5 = name_ref T, %.loc14_21.2 [symbolic = constants.%assoc0.b45]
+// CHECK:STDOUT:       %impl.elem0.loc14_21.1: type = impl_witness_access constants.%.eeb, element0 [symbolic = constants.%impl.elem0.756]
 // CHECK:STDOUT:       %.loc14_27.1: %empty_tuple.type = tuple_literal () [concrete = constants.%empty_tuple]
 // CHECK:STDOUT:       %.loc14_27.2: type = converted %.loc14_27.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:       %rewrite.loc14_24.1 = requirement_rewrite %impl.elem0.loc14_21.1, %.loc14_27.2 [concrete]
-// CHECK:STDOUT:       %impl.elem0.loc14_21.2: type = impl_witness_access constants.%.66e, element0 [symbolic = %impl.elem0.loc14_21.4 (constants.%impl.elem0.295)]
+// CHECK:STDOUT:       %impl.elem0.loc14_21.2: type = impl_witness_access constants.%.66e, element0 [symbolic = constants.%impl.elem0.295]
 // CHECK:STDOUT:       %rewrite.loc14_24.2 = requirement_rewrite %impl.elem0.loc14_21.2, %.loc14_27.2 [concrete]
-// CHECK:STDOUT:       %.loc14_15: type = where_expr [symbolic = %Y_where.type (constants.%Y_where.type.aa4)] {
+// CHECK:STDOUT:       %.loc14_15.1: type = where_expr [symbolic = %Y_where.type (constants.%Y_where.type.aa4)] {
 // CHECK:STDOUT:         %base_facet_type = requirement_base_facet_type %Y.ref [concrete]
 // CHECK:STDOUT:         %rewrite.loc14_24.2 = requirement_rewrite %impl.elem0.loc14_21.2, %.loc14_27.2 [concrete]
 // CHECK:STDOUT:       }
@@ -776,16 +744,10 @@ fn F() {
 // CHECK:STDOUT:   %OuterParam: %Z1.type = symbolic_binding OuterParam, 0 [symbolic = %OuterParam (constants.%OuterParam)]
 // CHECK:STDOUT:   %Y.type: type = facet_type <@Y, @Y(%OuterParam)> [symbolic = %Y.type (constants.%Y.type.9a0)]
 // CHECK:STDOUT:   %.Self.frozen.loc11_28.1: @Outer.G.%Y.type (%Y.type.9a0) = symbolic_binding .Self [symbolic = %.Self.frozen.loc11_28.1 (constants.%.Self.frozen.39e)]
-// CHECK:STDOUT:   %require_complete: <witness> = require_complete_type %Y.type [symbolic = %require_complete (constants.%require_complete)]
-// CHECK:STDOUT:   %.Self.frozen.as_type: type = facet_access_type %.Self.frozen.loc11_28.1 [symbolic = %.Self.frozen.as_type (constants.%.Self.frozen.as_type.618)]
-// CHECK:STDOUT:   %Y.assoc_type: type = assoc_entity_type @Y, @Y(%OuterParam) [symbolic = %Y.assoc_type (constants.%Y.assoc_type.5d5)]
-// CHECK:STDOUT:   %assoc0: @Outer.G.%Y.assoc_type (%Y.assoc_type.5d5) = assoc_entity element0, @Y.WithSelf.%T [symbolic = %assoc0 (constants.%assoc0.b45)]
-// CHECK:STDOUT:   %Y.lookup_impl_witness.loc11_34.1: <witness> = lookup_impl_witness %.Self.frozen.loc11_28.1, @Y, @Y(%OuterParam) [symbolic = %Y.lookup_impl_witness.loc11_34.1 (constants.%Y.lookup_impl_witness.580)]
-// CHECK:STDOUT:   %impl.elem0.loc11_34.1: type = impl_witness_access %Y.lookup_impl_witness.loc11_34.1, element0 [symbolic = %impl.elem0.loc11_34.1 (constants.%impl.elem0.be8)]
 // CHECK:STDOUT:   %.Self: @Outer.G.%Y.type (%Y.type.9a0) = symbolic_binding .Self [symbolic = %.Self (constants.%.Self.2b6)]
-// CHECK:STDOUT:   %Y.lookup_impl_witness.loc11_34.2: <witness> = lookup_impl_witness %.Self, @Y, @Y(%OuterParam) [symbolic = %Y.lookup_impl_witness.loc11_34.2 (constants.%Y.lookup_impl_witness.00e)]
-// CHECK:STDOUT:   %impl.elem0.loc11_34.2: type = impl_witness_access %Y.lookup_impl_witness.loc11_34.2, element0 [symbolic = %impl.elem0.loc11_34.2 (constants.%impl.elem0.43a)]
-// CHECK:STDOUT:   %Y_where.type: type = facet_type <@Y, @Y(%OuterParam) where %impl.elem0.loc11_34.2 = constants.%empty_tuple.type> [symbolic = %Y_where.type (constants.%Y_where.type.352)]
+// CHECK:STDOUT:   %Y.lookup_impl_witness: <witness> = lookup_impl_witness %.Self, @Y, @Y(%OuterParam) [symbolic = %Y.lookup_impl_witness (constants.%Y.lookup_impl_witness.00e)]
+// CHECK:STDOUT:   %impl.elem0.loc11_28: type = impl_witness_access %Y.lookup_impl_witness, element0 [symbolic = %impl.elem0.loc11_28 (constants.%impl.elem0.43a)]
+// CHECK:STDOUT:   %Y_where.type: type = facet_type <@Y, @Y(%OuterParam) where %impl.elem0.loc11_28 = constants.%empty_tuple.type> [symbolic = %Y_where.type (constants.%Y_where.type.352)]
 // CHECK:STDOUT:   %pattern_type: type = pattern_type %Y_where.type [symbolic = %pattern_type (constants.%pattern_type.8be)]
 // CHECK:STDOUT:   %H.patt.loc11_24.2: @Outer.G.%pattern_type (%pattern_type.8be) = symbolic_binding_pattern H, 1 [symbolic = %H.patt.loc11_24.2 (constants.%H.patt.57a)]
 // CHECK:STDOUT:   %H.loc11_24.1: @Outer.G.%Y_where.type (%Y_where.type.352) = symbolic_binding H, 1 [symbolic = %H.loc11_24.1 (constants.%H)]
@@ -885,15 +847,9 @@ fn F() {
 // CHECK:STDOUT:   %OuterParam => constants.%OuterParam
 // CHECK:STDOUT:   %Y.type => constants.%Y.type.9a0
 // CHECK:STDOUT:   %.Self.frozen.loc11_28.1 => constants.%.Self.frozen.39e
-// CHECK:STDOUT:   %require_complete => constants.%require_complete
-// CHECK:STDOUT:   %.Self.frozen.as_type => constants.%.Self.frozen.as_type.618
-// CHECK:STDOUT:   %Y.assoc_type => constants.%Y.assoc_type.5d5
-// CHECK:STDOUT:   %assoc0 => constants.%assoc0.b45
-// CHECK:STDOUT:   %Y.lookup_impl_witness.loc11_34.1 => constants.%Y.lookup_impl_witness.580
-// CHECK:STDOUT:   %impl.elem0.loc11_34.1 => constants.%impl.elem0.be8
 // CHECK:STDOUT:   %.Self => constants.%.Self.2b6
-// CHECK:STDOUT:   %Y.lookup_impl_witness.loc11_34.2 => constants.%Y.lookup_impl_witness.00e
-// CHECK:STDOUT:   %impl.elem0.loc11_34.2 => constants.%impl.elem0.43a
+// CHECK:STDOUT:   %Y.lookup_impl_witness => constants.%Y.lookup_impl_witness.00e
+// CHECK:STDOUT:   %impl.elem0.loc11_28 => constants.%impl.elem0.43a
 // CHECK:STDOUT:   %Y_where.type => constants.%Y_where.type.352
 // CHECK:STDOUT:   %pattern_type => constants.%pattern_type.8be
 // CHECK:STDOUT:   %H.patt.loc11_24.2 => constants.%H.patt.57a
@@ -907,15 +863,9 @@ fn F() {
 // CHECK:STDOUT:   %C => constants.%C.5f2
 // CHECK:STDOUT:   %Y.type => constants.%Y.type.9a0
 // CHECK:STDOUT:   %.Self.frozen.loc14_15.2 => constants.%.Self.frozen.39e
-// CHECK:STDOUT:   %require_complete => constants.%require_complete
-// CHECK:STDOUT:   %.Self.frozen.as_type => constants.%.Self.frozen.as_type.618
-// CHECK:STDOUT:   %Y.assoc_type => constants.%Y.assoc_type.5d5
-// CHECK:STDOUT:   %assoc0 => constants.%assoc0.b45
-// CHECK:STDOUT:   %.loc14_21.3 => constants.%.eeb
-// CHECK:STDOUT:   %impl.elem0.loc14_21.3 => constants.%impl.elem0.756
 // CHECK:STDOUT:   %.Self => constants.%.Self.2b6
-// CHECK:STDOUT:   %.loc14_21.4 => constants.%.66e
-// CHECK:STDOUT:   %impl.elem0.loc14_21.4 => constants.%impl.elem0.295
+// CHECK:STDOUT:   %.loc14_15.2 => constants.%.66e
+// CHECK:STDOUT:   %impl.elem0.loc14_15 => constants.%impl.elem0.295
 // CHECK:STDOUT:   %Y_where.type => constants.%Y_where.type.aa4
 // CHECK:STDOUT:   %.loc14_29 => constants.%.6b3
 // CHECK:STDOUT:   %Y.impl_witness.loc14_29.2 => constants.%Y.impl_witness.d75
@@ -961,20 +911,15 @@ fn F() {
 // CHECK:STDOUT:   %C => constants.%C.d9e
 // CHECK:STDOUT:   %Y.type => constants.%Y.type.30f
 // CHECK:STDOUT:   %.Self.frozen.loc14_15.2 => constants.%.Self.frozen.126
-// CHECK:STDOUT:   %require_complete => constants.%complete_type.d0d
-// CHECK:STDOUT:   %.Self.frozen.as_type => constants.%.Self.frozen.as_type.746
-// CHECK:STDOUT:   %Y.assoc_type => constants.%Y.assoc_type.104
-// CHECK:STDOUT:   %assoc0 => constants.%assoc0.2bd
-// CHECK:STDOUT:   %.loc14_21.3 => constants.%.03e
-// CHECK:STDOUT:   %impl.elem0.loc14_21.3 => constants.%impl.elem0.ad3
 // CHECK:STDOUT:   %.Self => constants.%.Self.1da
-// CHECK:STDOUT:   %.loc14_21.4 => constants.%.4bb
-// CHECK:STDOUT:   %impl.elem0.loc14_21.4 => constants.%impl.elem0.eb1
+// CHECK:STDOUT:   %.loc14_15.2 => constants.%.4bb
+// CHECK:STDOUT:   %impl.elem0.loc14_15 => constants.%impl.elem0.eb1
 // CHECK:STDOUT:   %Y_where.type => constants.%Y_where.type.d3d
 // CHECK:STDOUT:   %.loc14_29 => constants.%.9bc
 // CHECK:STDOUT:   %Y.impl_witness.loc14_29.2 => constants.%Y.impl_witness.1b2
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
+// CHECK:STDOUT:   %require_complete => constants.%complete_type.d0d
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @Y.WithSelf(constants.%Z1.facet, constants.%Self.6f0) {
@@ -988,15 +933,9 @@ fn F() {
 // CHECK:STDOUT:   %OuterParam => constants.%Z1.facet
 // CHECK:STDOUT:   %Y.type => constants.%Y.type.30f
 // CHECK:STDOUT:   %.Self.frozen.loc11_28.1 => constants.%.Self.frozen.126
-// CHECK:STDOUT:   %require_complete => constants.%complete_type.d0d
-// CHECK:STDOUT:   %.Self.frozen.as_type => constants.%.Self.frozen.as_type.746
-// CHECK:STDOUT:   %Y.assoc_type => constants.%Y.assoc_type.104
-// CHECK:STDOUT:   %assoc0 => constants.%assoc0.2bd
-// CHECK:STDOUT:   %Y.lookup_impl_witness.loc11_34.1 => constants.%Y.lookup_impl_witness.a66
-// CHECK:STDOUT:   %impl.elem0.loc11_34.1 => constants.%impl.elem0.e0b
 // CHECK:STDOUT:   %.Self => constants.%.Self.1da
-// CHECK:STDOUT:   %Y.lookup_impl_witness.loc11_34.2 => constants.%Y.lookup_impl_witness.0bd
-// CHECK:STDOUT:   %impl.elem0.loc11_34.2 => constants.%impl.elem0.186
+// CHECK:STDOUT:   %Y.lookup_impl_witness => constants.%Y.lookup_impl_witness.0bd
+// CHECK:STDOUT:   %impl.elem0.loc11_28 => constants.%impl.elem0.186
 // CHECK:STDOUT:   %Y_where.type => constants.%Y_where.type.677
 // CHECK:STDOUT:   %pattern_type => constants.%pattern_type.285
 // CHECK:STDOUT:   %H.patt.loc11_24.2 => constants.%H.patt.305

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

@@ -195,18 +195,18 @@ fn F[T: Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT:     %Z.type.loc9_40.1: type = facet_type <@Z, @Z(constants.%S)> [symbolic = %Z.type.loc9_40.2 (constants.%Z.type.83d)]
 // CHECK:STDOUT:     %.Self.frozen.loc9_42.1: @T.as.Z.impl.7e7.%Z.type.loc9_40.2 (%Z.type.83d) = symbolic_binding .Self [symbolic = %.Self.frozen.loc9_42.2 (constants.%.Self.frozen.04c)]
 // CHECK:STDOUT:     %base_facet_type = requirement_base_facet_type %Z.type.loc9_40.1 [concrete]
-// CHECK:STDOUT:     %.Self.ref: @T.as.Z.impl.7e7.%Z.type.loc9_40.2 (%Z.type.83d) = name_ref .Self, %.Self.frozen.loc9_42.1 [symbolic = %.Self.frozen.loc9_42.2 (constants.%.Self.frozen.04c)]
-// CHECK:STDOUT:     %.Self.as_type: type = facet_access_type %.Self.ref [symbolic = %.Self.frozen.as_type (constants.%.Self.frozen.as_type.def)]
-// CHECK:STDOUT:     %.loc9_48.1: type = converted %.Self.ref, %.Self.as_type [symbolic = %.Self.frozen.as_type (constants.%.Self.frozen.as_type.def)]
-// CHECK:STDOUT:     %.loc9_48.2: @T.as.Z.impl.7e7.%Z.assoc_type (%Z.assoc_type.f08) = specific_constant @X.%assoc0, @Z.WithSelf(constants.%S, constants.%.Self.frozen.04c) [symbolic = %assoc0 (constants.%assoc0.f21)]
-// CHECK:STDOUT:     %X.ref: @T.as.Z.impl.7e7.%Z.assoc_type (%Z.assoc_type.f08) = name_ref X, %.loc9_48.2 [symbolic = %assoc0 (constants.%assoc0.f21)]
-// CHECK:STDOUT:     %impl.elem0.loc9_48.1: type = impl_witness_access constants.%.c4e, element0 [symbolic = %impl.elem0.loc9_48.3 (constants.%impl.elem0.77c)]
+// CHECK:STDOUT:     %.Self.ref: %Z.type.83d = name_ref .Self, %.Self.frozen.loc9_42.1 [symbolic = constants.%.Self.frozen.04c]
+// CHECK:STDOUT:     %.Self.as_type: type = facet_access_type %.Self.ref [symbolic = constants.%.Self.frozen.as_type.def]
+// CHECK:STDOUT:     %.loc9_48.1: type = converted %.Self.ref, %.Self.as_type [symbolic = constants.%.Self.frozen.as_type.def]
+// CHECK:STDOUT:     %.loc9_48.2: %Z.assoc_type.f08 = specific_constant @X.%assoc0, @Z.WithSelf(constants.%S, constants.%.Self.frozen.04c) [symbolic = constants.%assoc0.f21]
+// CHECK:STDOUT:     %X.ref: %Z.assoc_type.f08 = name_ref X, %.loc9_48.2 [symbolic = constants.%assoc0.f21]
+// CHECK:STDOUT:     %impl.elem0.loc9_48.1: type = impl_witness_access constants.%.c4e, element0 [symbolic = constants.%impl.elem0.77c]
 // CHECK:STDOUT:     %.loc9_54.1: %empty_tuple.type = tuple_literal () [concrete = constants.%empty_tuple]
 // CHECK:STDOUT:     %.loc9_54.2: type = converted %.loc9_54.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:     %rewrite.loc9_51.1 = requirement_rewrite %impl.elem0.loc9_48.1, %.loc9_54.2 [concrete]
-// CHECK:STDOUT:     %impl.elem0.loc9_48.2: type = impl_witness_access constants.%.b6e, element0 [symbolic = %impl.elem0.loc9_48.4 (constants.%impl.elem0.6b8)]
+// CHECK:STDOUT:     %impl.elem0.loc9_48.2: type = impl_witness_access constants.%.b6e, element0 [symbolic = constants.%impl.elem0.6b8]
 // CHECK:STDOUT:     %rewrite.loc9_51.2 = requirement_rewrite %impl.elem0.loc9_48.2, %.loc9_54.2 [concrete]
-// CHECK:STDOUT:     %.loc9_42: type = where_expr [symbolic = %Z_where.type (constants.%Z_where.type.270)] {
+// CHECK:STDOUT:     %.loc9_42.1: type = where_expr [symbolic = %Z_where.type (constants.%Z_where.type.270)] {
 // CHECK:STDOUT:       %base_facet_type = requirement_base_facet_type %Z.type.loc9_40.1 [concrete]
 // CHECK:STDOUT:       %rewrite.loc9_51.2 = requirement_rewrite %impl.elem0.loc9_48.2, %.loc9_54.2 [concrete]
 // CHECK:STDOUT:     }
@@ -237,7 +237,7 @@ fn F[T: Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT:     %.loc11_45.2: %Z.assoc_type.714 = specific_constant @X.%assoc0, @Z.WithSelf(constants.%C, constants.%.Self.frozen.738) [concrete = constants.%assoc0.fd2]
 // CHECK:STDOUT:     %X.ref: %Z.assoc_type.714 = name_ref X, %.loc11_45.2 [concrete = constants.%assoc0.fd2]
 // CHECK:STDOUT:     %impl.elem0.loc11_45.1: type = impl_witness_access constants.%.869, element0 [symbolic_self = constants.%impl.elem0.dd4]
-// CHECK:STDOUT:     %T.ref.loc11_50: type = name_ref T, %T.loc11_21.1 [symbolic = %T.loc11_21.2 (constants.%T.67d)]
+// CHECK:STDOUT:     %T.ref.loc11_50: type = name_ref T, %T.loc11_21.1 [symbolic = constants.%T.67d]
 // CHECK:STDOUT:     %rewrite.loc11_48.1 = requirement_rewrite %impl.elem0.loc11_45.1, %T.ref.loc11_50 [concrete]
 // CHECK:STDOUT:     %impl.elem0.loc11_45.2: type = impl_witness_access constants.%.449, element0 [symbolic_self = constants.%impl.elem0.8b9]
 // CHECK:STDOUT:     %rewrite.loc11_48.2 = requirement_rewrite %impl.elem0.loc11_45.2, %T.ref.loc11_50 [concrete]
@@ -307,20 +307,15 @@ fn F[T: Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT:   %S.loc9_24.2: type = symbolic_binding S, 1 [symbolic = %S.loc9_24.2 (constants.%S)]
 // CHECK:STDOUT:   %Z.type.loc9_40.2: type = facet_type <@Z, @Z(%S.loc9_24.2)> [symbolic = %Z.type.loc9_40.2 (constants.%Z.type.83d)]
 // CHECK:STDOUT:   %.Self.frozen.loc9_42.2: @T.as.Z.impl.7e7.%Z.type.loc9_40.2 (%Z.type.83d) = symbolic_binding .Self [symbolic = %.Self.frozen.loc9_42.2 (constants.%.Self.frozen.04c)]
-// CHECK:STDOUT:   %require_complete: <witness> = require_complete_type %Z.type.loc9_40.2 [symbolic = %require_complete (constants.%require_complete.dc6)]
-// CHECK:STDOUT:   %.Self.frozen.as_type: type = facet_access_type %.Self.frozen.loc9_42.2 [symbolic = %.Self.frozen.as_type (constants.%.Self.frozen.as_type.def)]
-// CHECK:STDOUT:   %Z.assoc_type: type = assoc_entity_type @Z, @Z(%S.loc9_24.2) [symbolic = %Z.assoc_type (constants.%Z.assoc_type.f08)]
-// CHECK:STDOUT:   %assoc0: @T.as.Z.impl.7e7.%Z.assoc_type (%Z.assoc_type.f08) = assoc_entity element0, @Z.WithSelf.%X [symbolic = %assoc0 (constants.%assoc0.f21)]
-// CHECK:STDOUT:   %.loc9_48.3: <witness> = impl_self_witness %.Self.frozen.loc9_42.2, @Z, @Z(%S.loc9_24.2) [symbolic = %.loc9_48.3 (constants.%.c4e)]
-// CHECK:STDOUT:   %impl.elem0.loc9_48.3: type = impl_witness_access %.loc9_48.3, element0 [symbolic = %impl.elem0.loc9_48.3 (constants.%impl.elem0.77c)]
 // CHECK:STDOUT:   %.Self: @T.as.Z.impl.7e7.%Z.type.loc9_40.2 (%Z.type.83d) = symbolic_binding .Self [symbolic = %.Self (constants.%.Self.66b)]
-// CHECK:STDOUT:   %.loc9_48.4: <witness> = impl_self_witness %.Self, @Z, @Z(%S.loc9_24.2) [symbolic = %.loc9_48.4 (constants.%.b6e)]
-// CHECK:STDOUT:   %impl.elem0.loc9_48.4: type = impl_witness_access %.loc9_48.4, element0 [symbolic = %impl.elem0.loc9_48.4 (constants.%impl.elem0.6b8)]
-// CHECK:STDOUT:   %Z_where.type: type = facet_type <@Z, @Z(%S.loc9_24.2) where %impl.elem0.loc9_48.4 = constants.%empty_tuple.type> [symbolic = %Z_where.type (constants.%Z_where.type.270)]
+// CHECK:STDOUT:   %.loc9_42.2: <witness> = impl_self_witness %.Self, @Z, @Z(%S.loc9_24.2) [symbolic = %.loc9_42.2 (constants.%.b6e)]
+// CHECK:STDOUT:   %impl.elem0.loc9_42: type = impl_witness_access %.loc9_42.2, element0 [symbolic = %impl.elem0.loc9_42 (constants.%impl.elem0.6b8)]
+// CHECK:STDOUT:   %Z_where.type: type = facet_type <@Z, @Z(%S.loc9_24.2) where %impl.elem0.loc9_42 = constants.%empty_tuple.type> [symbolic = %Z_where.type (constants.%Z_where.type.270)]
 // CHECK:STDOUT:   %.loc9_56: <witness> = impl_self_witness %T.loc9_15.2, @Z, @Z(%S.loc9_24.2) [symbolic = %.loc9_56 (constants.%.a4f)]
 // CHECK:STDOUT:   %Z.impl_witness.loc9_56.2: <witness> = impl_witness %Z.impl_witness_table, @T.as.Z.impl.7e7(%T.loc9_15.2, %S.loc9_24.2) [symbolic = %Z.impl_witness.loc9_56.2 (constants.%Z.impl_witness.793)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
+// CHECK:STDOUT:   %require_complete: <witness> = require_complete_type %Z.type.loc9_40.2 [symbolic = %require_complete (constants.%require_complete.dc6)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   impl: %T.ref as %Z.type.loc9_40.1 {
 // CHECK:STDOUT:     %Z.impl_witness_table = impl_witness_table (%impl_witness_assoc_constant), @T.as.Z.impl.7e7 [concrete]
@@ -430,15 +425,9 @@ fn F[T: Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT:   %S.loc9_24.2 => constants.%S
 // CHECK:STDOUT:   %Z.type.loc9_40.2 => constants.%Z.type.83d
 // CHECK:STDOUT:   %.Self.frozen.loc9_42.2 => constants.%.Self.frozen.04c
-// CHECK:STDOUT:   %require_complete => constants.%require_complete.dc6
-// CHECK:STDOUT:   %.Self.frozen.as_type => constants.%.Self.frozen.as_type.def
-// CHECK:STDOUT:   %Z.assoc_type => constants.%Z.assoc_type.f08
-// CHECK:STDOUT:   %assoc0 => constants.%assoc0.f21
-// CHECK:STDOUT:   %.loc9_48.3 => constants.%.c4e
-// CHECK:STDOUT:   %impl.elem0.loc9_48.3 => constants.%impl.elem0.77c
 // CHECK:STDOUT:   %.Self => constants.%.Self.66b
-// CHECK:STDOUT:   %.loc9_48.4 => constants.%.b6e
-// CHECK:STDOUT:   %impl.elem0.loc9_48.4 => constants.%impl.elem0.6b8
+// CHECK:STDOUT:   %.loc9_42.2 => constants.%.b6e
+// CHECK:STDOUT:   %impl.elem0.loc9_42 => constants.%impl.elem0.6b8
 // CHECK:STDOUT:   %Z_where.type => constants.%Z_where.type.270
 // CHECK:STDOUT:   %.loc9_56 => constants.%.a4f
 // CHECK:STDOUT:   %Z.impl_witness.loc9_56.2 => constants.%Z.impl_witness.793
@@ -641,18 +630,18 @@ fn F[T: Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT:     %Z.type.loc10_40.1: type = facet_type <@Z, @Z(constants.%S)> [symbolic = %Z.type.loc10_40.2 (constants.%Z.type.83d)]
 // CHECK:STDOUT:     %.Self.frozen.loc10_42.1: @T.as.Z.impl.7e7.%Z.type.loc10_40.2 (%Z.type.83d) = symbolic_binding .Self [symbolic = %.Self.frozen.loc10_42.2 (constants.%.Self.frozen.04c)]
 // CHECK:STDOUT:     %base_facet_type = requirement_base_facet_type %Z.type.loc10_40.1 [concrete]
-// CHECK:STDOUT:     %.Self.ref: @T.as.Z.impl.7e7.%Z.type.loc10_40.2 (%Z.type.83d) = name_ref .Self, %.Self.frozen.loc10_42.1 [symbolic = %.Self.frozen.loc10_42.2 (constants.%.Self.frozen.04c)]
-// CHECK:STDOUT:     %.Self.as_type: type = facet_access_type %.Self.ref [symbolic = %.Self.frozen.as_type (constants.%.Self.frozen.as_type.def)]
-// CHECK:STDOUT:     %.loc10_48.1: type = converted %.Self.ref, %.Self.as_type [symbolic = %.Self.frozen.as_type (constants.%.Self.frozen.as_type.def)]
-// CHECK:STDOUT:     %.loc10_48.2: @T.as.Z.impl.7e7.%Z.assoc_type (%Z.assoc_type.f08) = specific_constant @X.%assoc0, @Z.WithSelf(constants.%S, constants.%.Self.frozen.04c) [symbolic = %assoc0 (constants.%assoc0.f21)]
-// CHECK:STDOUT:     %X.ref: @T.as.Z.impl.7e7.%Z.assoc_type (%Z.assoc_type.f08) = name_ref X, %.loc10_48.2 [symbolic = %assoc0 (constants.%assoc0.f21)]
-// CHECK:STDOUT:     %impl.elem0.loc10_48.1: type = impl_witness_access constants.%.c4e, element0 [symbolic = %impl.elem0.loc10_48.3 (constants.%impl.elem0.77c)]
+// CHECK:STDOUT:     %.Self.ref: %Z.type.83d = name_ref .Self, %.Self.frozen.loc10_42.1 [symbolic = constants.%.Self.frozen.04c]
+// CHECK:STDOUT:     %.Self.as_type: type = facet_access_type %.Self.ref [symbolic = constants.%.Self.frozen.as_type.def]
+// CHECK:STDOUT:     %.loc10_48.1: type = converted %.Self.ref, %.Self.as_type [symbolic = constants.%.Self.frozen.as_type.def]
+// CHECK:STDOUT:     %.loc10_48.2: %Z.assoc_type.f08 = specific_constant @X.%assoc0, @Z.WithSelf(constants.%S, constants.%.Self.frozen.04c) [symbolic = constants.%assoc0.f21]
+// CHECK:STDOUT:     %X.ref: %Z.assoc_type.f08 = name_ref X, %.loc10_48.2 [symbolic = constants.%assoc0.f21]
+// CHECK:STDOUT:     %impl.elem0.loc10_48.1: type = impl_witness_access constants.%.c4e, element0 [symbolic = constants.%impl.elem0.77c]
 // CHECK:STDOUT:     %.loc10_54.1: %empty_tuple.type = tuple_literal () [concrete = constants.%empty_tuple]
 // CHECK:STDOUT:     %.loc10_54.2: type = converted %.loc10_54.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
 // CHECK:STDOUT:     %rewrite.loc10_51.1 = requirement_rewrite %impl.elem0.loc10_48.1, %.loc10_54.2 [concrete]
-// CHECK:STDOUT:     %impl.elem0.loc10_48.2: type = impl_witness_access constants.%.b6e, element0 [symbolic = %impl.elem0.loc10_48.4 (constants.%impl.elem0.6b8)]
+// CHECK:STDOUT:     %impl.elem0.loc10_48.2: type = impl_witness_access constants.%.b6e, element0 [symbolic = constants.%impl.elem0.6b8]
 // CHECK:STDOUT:     %rewrite.loc10_51.2 = requirement_rewrite %impl.elem0.loc10_48.2, %.loc10_54.2 [concrete]
-// CHECK:STDOUT:     %.loc10_42: type = where_expr [symbolic = %Z_where.type (constants.%Z_where.type.270)] {
+// CHECK:STDOUT:     %.loc10_42.1: type = where_expr [symbolic = %Z_where.type (constants.%Z_where.type.270)] {
 // CHECK:STDOUT:       %base_facet_type = requirement_base_facet_type %Z.type.loc10_40.1 [concrete]
 // CHECK:STDOUT:       %rewrite.loc10_51.2 = requirement_rewrite %impl.elem0.loc10_48.2, %.loc10_54.2 [concrete]
 // CHECK:STDOUT:     }
@@ -683,7 +672,7 @@ fn F[T: Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT:     %.loc12_39.2: %Z.assoc_type.714 = specific_constant @X.%assoc0, @Z.WithSelf(constants.%C, constants.%.Self.frozen.738) [concrete = constants.%assoc0.fd2]
 // CHECK:STDOUT:     %X.ref: %Z.assoc_type.714 = name_ref X, %.loc12_39.2 [concrete = constants.%assoc0.fd2]
 // CHECK:STDOUT:     %impl.elem0.loc12_39.1: type = impl_witness_access constants.%.869, element0 [symbolic_self = constants.%impl.elem0.dd4]
-// CHECK:STDOUT:     %T.ref.loc12_44: type = name_ref T, %T.loc12_15.1 [symbolic = %T.loc12_15.2 (constants.%T.67d)]
+// CHECK:STDOUT:     %T.ref.loc12_44: type = name_ref T, %T.loc12_15.1 [symbolic = constants.%T.67d]
 // CHECK:STDOUT:     %rewrite.loc12_42.1 = requirement_rewrite %impl.elem0.loc12_39.1, %T.ref.loc12_44 [concrete]
 // CHECK:STDOUT:     %impl.elem0.loc12_39.2: type = impl_witness_access constants.%.449, element0 [symbolic_self = constants.%impl.elem0.8b9]
 // CHECK:STDOUT:     %rewrite.loc12_42.2 = requirement_rewrite %impl.elem0.loc12_39.2, %T.ref.loc12_44 [concrete]
@@ -764,20 +753,15 @@ fn F[T: Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT:   %S.loc10_24.2: type = symbolic_binding S, 1 [symbolic = %S.loc10_24.2 (constants.%S)]
 // CHECK:STDOUT:   %Z.type.loc10_40.2: type = facet_type <@Z, @Z(%S.loc10_24.2)> [symbolic = %Z.type.loc10_40.2 (constants.%Z.type.83d)]
 // CHECK:STDOUT:   %.Self.frozen.loc10_42.2: @T.as.Z.impl.7e7.%Z.type.loc10_40.2 (%Z.type.83d) = symbolic_binding .Self [symbolic = %.Self.frozen.loc10_42.2 (constants.%.Self.frozen.04c)]
-// CHECK:STDOUT:   %require_complete: <witness> = require_complete_type %Z.type.loc10_40.2 [symbolic = %require_complete (constants.%require_complete.dc6)]
-// CHECK:STDOUT:   %.Self.frozen.as_type: type = facet_access_type %.Self.frozen.loc10_42.2 [symbolic = %.Self.frozen.as_type (constants.%.Self.frozen.as_type.def)]
-// CHECK:STDOUT:   %Z.assoc_type: type = assoc_entity_type @Z, @Z(%S.loc10_24.2) [symbolic = %Z.assoc_type (constants.%Z.assoc_type.f08)]
-// CHECK:STDOUT:   %assoc0: @T.as.Z.impl.7e7.%Z.assoc_type (%Z.assoc_type.f08) = assoc_entity element0, @Z.WithSelf.%X [symbolic = %assoc0 (constants.%assoc0.f21)]
-// CHECK:STDOUT:   %.loc10_48.3: <witness> = impl_self_witness %.Self.frozen.loc10_42.2, @Z, @Z(%S.loc10_24.2) [symbolic = %.loc10_48.3 (constants.%.c4e)]
-// CHECK:STDOUT:   %impl.elem0.loc10_48.3: type = impl_witness_access %.loc10_48.3, element0 [symbolic = %impl.elem0.loc10_48.3 (constants.%impl.elem0.77c)]
 // CHECK:STDOUT:   %.Self: @T.as.Z.impl.7e7.%Z.type.loc10_40.2 (%Z.type.83d) = symbolic_binding .Self [symbolic = %.Self (constants.%.Self.66b)]
-// CHECK:STDOUT:   %.loc10_48.4: <witness> = impl_self_witness %.Self, @Z, @Z(%S.loc10_24.2) [symbolic = %.loc10_48.4 (constants.%.b6e)]
-// CHECK:STDOUT:   %impl.elem0.loc10_48.4: type = impl_witness_access %.loc10_48.4, element0 [symbolic = %impl.elem0.loc10_48.4 (constants.%impl.elem0.6b8)]
-// CHECK:STDOUT:   %Z_where.type: type = facet_type <@Z, @Z(%S.loc10_24.2) where %impl.elem0.loc10_48.4 = constants.%empty_tuple.type> [symbolic = %Z_where.type (constants.%Z_where.type.270)]
+// CHECK:STDOUT:   %.loc10_42.2: <witness> = impl_self_witness %.Self, @Z, @Z(%S.loc10_24.2) [symbolic = %.loc10_42.2 (constants.%.b6e)]
+// CHECK:STDOUT:   %impl.elem0.loc10_42: type = impl_witness_access %.loc10_42.2, element0 [symbolic = %impl.elem0.loc10_42 (constants.%impl.elem0.6b8)]
+// CHECK:STDOUT:   %Z_where.type: type = facet_type <@Z, @Z(%S.loc10_24.2) where %impl.elem0.loc10_42 = constants.%empty_tuple.type> [symbolic = %Z_where.type (constants.%Z_where.type.270)]
 // CHECK:STDOUT:   %.loc10_56: <witness> = impl_self_witness %T.loc10_15.2, @Z, @Z(%S.loc10_24.2) [symbolic = %.loc10_56 (constants.%.a4f)]
 // CHECK:STDOUT:   %Z.impl_witness.loc10_56.2: <witness> = impl_witness %Z.impl_witness_table, @T.as.Z.impl.7e7(%T.loc10_15.2, %S.loc10_24.2) [symbolic = %Z.impl_witness.loc10_56.2 (constants.%Z.impl_witness.793)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
+// CHECK:STDOUT:   %require_complete: <witness> = require_complete_type %Z.type.loc10_40.2 [symbolic = %require_complete (constants.%require_complete.dc6)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   impl: %T.ref as %Z.type.loc10_40.1 {
 // CHECK:STDOUT:     %Z.impl_witness_table = impl_witness_table (%impl_witness_assoc_constant), @T.as.Z.impl.7e7 [concrete]
@@ -900,15 +884,9 @@ fn F[T: Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT:   %S.loc10_24.2 => constants.%S
 // CHECK:STDOUT:   %Z.type.loc10_40.2 => constants.%Z.type.83d
 // CHECK:STDOUT:   %.Self.frozen.loc10_42.2 => constants.%.Self.frozen.04c
-// CHECK:STDOUT:   %require_complete => constants.%require_complete.dc6
-// CHECK:STDOUT:   %.Self.frozen.as_type => constants.%.Self.frozen.as_type.def
-// CHECK:STDOUT:   %Z.assoc_type => constants.%Z.assoc_type.f08
-// CHECK:STDOUT:   %assoc0 => constants.%assoc0.f21
-// CHECK:STDOUT:   %.loc10_48.3 => constants.%.c4e
-// CHECK:STDOUT:   %impl.elem0.loc10_48.3 => constants.%impl.elem0.77c
 // CHECK:STDOUT:   %.Self => constants.%.Self.66b
-// CHECK:STDOUT:   %.loc10_48.4 => constants.%.b6e
-// CHECK:STDOUT:   %impl.elem0.loc10_48.4 => constants.%impl.elem0.6b8
+// CHECK:STDOUT:   %.loc10_42.2 => constants.%.b6e
+// CHECK:STDOUT:   %impl.elem0.loc10_42 => constants.%impl.elem0.6b8
 // CHECK:STDOUT:   %Z_where.type => constants.%Z_where.type.270
 // CHECK:STDOUT:   %.loc10_56 => constants.%.a4f
 // CHECK:STDOUT:   %Z.impl_witness.loc10_56.2 => constants.%Z.impl_witness.793
@@ -1057,14 +1035,14 @@ fn F[T: Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT:     %.loc7_44: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.frozen.as_type]
 // CHECK:STDOUT:     %Type.ref: %Ptr.assoc_type = name_ref Type, @Type.%assoc0 [concrete = constants.%assoc0.b1a]
 // CHECK:STDOUT:     %impl.elem0.loc7_44.1: type = impl_witness_access constants.%.c6b, element0 [symbolic_self = constants.%impl.elem0.949]
-// CHECK:STDOUT:     %U.ref.loc7_52: type = name_ref U, %U.loc7_21.1 [symbolic = %U.loc7_21.2 (constants.%U.67d)]
-// CHECK:STDOUT:     %ptr.loc7_53.1: type = ptr_type %U.ref.loc7_52 [symbolic = %ptr.loc7_53.2 (constants.%ptr.e8f8f9.1)]
-// CHECK:STDOUT:     %rewrite.loc7_50.1 = requirement_rewrite %impl.elem0.loc7_44.1, %ptr.loc7_53.1 [concrete]
+// CHECK:STDOUT:     %U.ref.loc7_52: type = name_ref U, %U.loc7_21.1 [symbolic = constants.%U.67d]
+// CHECK:STDOUT:     %ptr.loc7_53: type = ptr_type %U.ref.loc7_52 [symbolic = constants.%ptr.e8f8f9.1]
+// CHECK:STDOUT:     %rewrite.loc7_50.1 = requirement_rewrite %impl.elem0.loc7_44.1, %ptr.loc7_53 [concrete]
 // CHECK:STDOUT:     %impl.elem0.loc7_44.2: type = impl_witness_access constants.%.51f, element0 [symbolic_self = constants.%impl.elem0.406]
-// CHECK:STDOUT:     %rewrite.loc7_50.2 = requirement_rewrite %impl.elem0.loc7_44.2, %ptr.loc7_53.1 [concrete]
+// CHECK:STDOUT:     %rewrite.loc7_50.2 = requirement_rewrite %impl.elem0.loc7_44.2, %ptr.loc7_53 [concrete]
 // CHECK:STDOUT:     %.loc7_38: type = where_expr [symbolic = %Ptr_where.type (constants.%Ptr_where.type.774fa9.1)] {
 // CHECK:STDOUT:       %base_facet_type = requirement_base_facet_type %Ptr.ref [concrete]
-// CHECK:STDOUT:       %rewrite.loc7_50.2 = requirement_rewrite %impl.elem0.loc7_44.2, %ptr.loc7_53.1 [concrete]
+// CHECK:STDOUT:       %rewrite.loc7_50.2 = requirement_rewrite %impl.elem0.loc7_44.2, %ptr.loc7_53 [concrete]
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %.loc7_23.1: type = splice_block %.loc7_23.2 [concrete = type] {
 // CHECK:STDOUT:       %.Self.frozen.loc7_21: type = symbolic_binding .Self [symbolic_self = constants.%.Self.frozen.e58]
@@ -1120,8 +1098,8 @@ fn F[T: Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT: generic final impl @U.as.Ptr.impl(%U.loc7_21.1: type) {
 // CHECK:STDOUT:   %U.patt.loc7_21.2: %pattern_type.9a5 = symbolic_binding_pattern U, 0 [symbolic = %U.patt.loc7_21.2 (constants.%U.patt.3a0)]
 // CHECK:STDOUT:   %U.loc7_21.2: type = symbolic_binding U, 0 [symbolic = %U.loc7_21.2 (constants.%U.67d)]
-// CHECK:STDOUT:   %ptr.loc7_53.2: type = ptr_type %U.loc7_21.2 [symbolic = %ptr.loc7_53.2 (constants.%ptr.e8f8f9.1)]
-// CHECK:STDOUT:   %Ptr_where.type: type = facet_type <@Ptr where constants.%impl.elem0.406 = %ptr.loc7_53.2> [symbolic = %Ptr_where.type (constants.%Ptr_where.type.774fa9.1)]
+// CHECK:STDOUT:   %ptr.loc7_38: type = ptr_type %U.loc7_21.2 [symbolic = %ptr.loc7_38 (constants.%ptr.e8f8f9.1)]
+// CHECK:STDOUT:   %Ptr_where.type: type = facet_type <@Ptr where constants.%impl.elem0.406 = %ptr.loc7_38> [symbolic = %Ptr_where.type (constants.%Ptr_where.type.774fa9.1)]
 // CHECK:STDOUT:   %.loc7_55: <witness> = impl_self_witness %U.loc7_21.2, @Ptr [symbolic = %.loc7_55 (constants.%.f8fe26.1)]
 // CHECK:STDOUT:   %Ptr.impl_witness.loc7_55.2: <witness> = impl_witness %Ptr.impl_witness_table, @U.as.Ptr.impl(%U.loc7_21.2) [symbolic = %Ptr.impl_witness.loc7_55.2 (constants.%Ptr.impl_witness.5a17a2.1)]
 // CHECK:STDOUT:
@@ -1130,7 +1108,7 @@ fn F[T: Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT:   final impl: %U.ref.loc7_29 as %Ptr.ref {
 // CHECK:STDOUT:     %Ptr.impl_witness_table = impl_witness_table (%impl_witness_assoc_constant), @U.as.Ptr.impl [concrete]
 // CHECK:STDOUT:     %Ptr.impl_witness.loc7_55.1: <witness> = impl_witness %Ptr.impl_witness_table, @U.as.Ptr.impl(constants.%U.67d) [symbolic = %Ptr.impl_witness.loc7_55.2 (constants.%Ptr.impl_witness.5a17a2.1)]
-// CHECK:STDOUT:     %impl_witness_assoc_constant: type = impl_witness_assoc_constant constants.%ptr.e8f8f9.1 [symbolic = %ptr.loc7_53.2 (constants.%ptr.e8f8f9.1)]
+// CHECK:STDOUT:     %impl_witness_assoc_constant: type = impl_witness_assoc_constant constants.%ptr.e8f8f9.1 [symbolic = %ptr.loc7_38 (constants.%ptr.e8f8f9.1)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   !members:
 // CHECK:STDOUT:     extend %Ptr.ref
@@ -1192,7 +1170,7 @@ fn F[T: Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT: specific @U.as.Ptr.impl(constants.%U.67d) {
 // CHECK:STDOUT:   %U.patt.loc7_21.2 => constants.%U.patt.3a0
 // CHECK:STDOUT:   %U.loc7_21.2 => constants.%U.67d
-// CHECK:STDOUT:   %ptr.loc7_53.2 => constants.%ptr.e8f8f9.1
+// CHECK:STDOUT:   %ptr.loc7_38 => constants.%ptr.e8f8f9.1
 // CHECK:STDOUT:   %Ptr_where.type => constants.%Ptr_where.type.774fa9.1
 // CHECK:STDOUT:   %.loc7_55 => constants.%.f8fe26.1
 // CHECK:STDOUT:   %Ptr.impl_witness.loc7_55.2 => constants.%Ptr.impl_witness.5a17a2.1
@@ -1205,7 +1183,7 @@ fn F[T: Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT: specific @U.as.Ptr.impl(constants.%T.67d) {
 // CHECK:STDOUT:   %U.patt.loc7_21.2 => constants.%U.patt.3a0
 // CHECK:STDOUT:   %U.loc7_21.2 => constants.%T.67d
-// CHECK:STDOUT:   %ptr.loc7_53.2 => constants.%ptr.e8f8f9.2
+// CHECK:STDOUT:   %ptr.loc7_38 => constants.%ptr.e8f8f9.2
 // CHECK:STDOUT:   %Ptr_where.type => constants.%Ptr_where.type.774fa9.2
 // CHECK:STDOUT:   %.loc7_55 => constants.%.f8fe26.2
 // CHECK:STDOUT:   %Ptr.impl_witness.loc7_55.2 => constants.%Ptr.impl_witness.5a17a2.2
@@ -1316,14 +1294,14 @@ fn F[T: Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT:     %.loc7_44: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.frozen.as_type]
 // CHECK:STDOUT:     %Type.ref: %Ptr.assoc_type = name_ref Type, @Type.%assoc0 [concrete = constants.%assoc0.b1a]
 // CHECK:STDOUT:     %impl.elem0.loc7_44.1: type = impl_witness_access constants.%.c6b, element0 [symbolic_self = constants.%impl.elem0.949]
-// CHECK:STDOUT:     %U.ref.loc7_52: type = name_ref U, %U.loc7_21.1 [symbolic = %U.loc7_21.2 (constants.%U.67d)]
-// CHECK:STDOUT:     %ptr.loc7_53.1: type = ptr_type %U.ref.loc7_52 [symbolic = %ptr.loc7_53.2 (constants.%ptr.e8f8f9.1)]
-// CHECK:STDOUT:     %rewrite.loc7_50.1 = requirement_rewrite %impl.elem0.loc7_44.1, %ptr.loc7_53.1 [concrete]
+// CHECK:STDOUT:     %U.ref.loc7_52: type = name_ref U, %U.loc7_21.1 [symbolic = constants.%U.67d]
+// CHECK:STDOUT:     %ptr.loc7_53: type = ptr_type %U.ref.loc7_52 [symbolic = constants.%ptr.e8f8f9.1]
+// CHECK:STDOUT:     %rewrite.loc7_50.1 = requirement_rewrite %impl.elem0.loc7_44.1, %ptr.loc7_53 [concrete]
 // CHECK:STDOUT:     %impl.elem0.loc7_44.2: type = impl_witness_access constants.%.51f, element0 [symbolic_self = constants.%impl.elem0.406]
-// CHECK:STDOUT:     %rewrite.loc7_50.2 = requirement_rewrite %impl.elem0.loc7_44.2, %ptr.loc7_53.1 [concrete]
+// CHECK:STDOUT:     %rewrite.loc7_50.2 = requirement_rewrite %impl.elem0.loc7_44.2, %ptr.loc7_53 [concrete]
 // CHECK:STDOUT:     %.loc7_38: type = where_expr [symbolic = %Ptr_where.type (constants.%Ptr_where.type.774)] {
 // CHECK:STDOUT:       %base_facet_type = requirement_base_facet_type %Ptr.ref [concrete]
-// CHECK:STDOUT:       %rewrite.loc7_50.2 = requirement_rewrite %impl.elem0.loc7_44.2, %ptr.loc7_53.1 [concrete]
+// CHECK:STDOUT:       %rewrite.loc7_50.2 = requirement_rewrite %impl.elem0.loc7_44.2, %ptr.loc7_53 [concrete]
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %.loc7_23.1: type = splice_block %.loc7_23.2 [concrete = type] {
 // CHECK:STDOUT:       %.Self.frozen.loc7_21: type = symbolic_binding .Self [symbolic_self = constants.%.Self.frozen.e58]
@@ -1382,8 +1360,8 @@ fn F[T: Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT: generic final impl @U.as.Ptr.impl(%U.loc7_21.1: type) {
 // CHECK:STDOUT:   %U.patt.loc7_21.2: %pattern_type.9a5 = symbolic_binding_pattern U, 0 [symbolic = %U.patt.loc7_21.2 (constants.%U.patt.3a0)]
 // CHECK:STDOUT:   %U.loc7_21.2: type = symbolic_binding U, 0 [symbolic = %U.loc7_21.2 (constants.%U.67d)]
-// CHECK:STDOUT:   %ptr.loc7_53.2: type = ptr_type %U.loc7_21.2 [symbolic = %ptr.loc7_53.2 (constants.%ptr.e8f8f9.1)]
-// CHECK:STDOUT:   %Ptr_where.type: type = facet_type <@Ptr where constants.%impl.elem0.406 = %ptr.loc7_53.2> [symbolic = %Ptr_where.type (constants.%Ptr_where.type.774)]
+// CHECK:STDOUT:   %ptr.loc7_38: type = ptr_type %U.loc7_21.2 [symbolic = %ptr.loc7_38 (constants.%ptr.e8f8f9.1)]
+// CHECK:STDOUT:   %Ptr_where.type: type = facet_type <@Ptr where constants.%impl.elem0.406 = %ptr.loc7_38> [symbolic = %Ptr_where.type (constants.%Ptr_where.type.774)]
 // CHECK:STDOUT:   %.loc7_55: <witness> = impl_self_witness %U.loc7_21.2, @Ptr [symbolic = %.loc7_55 (constants.%.f8f)]
 // CHECK:STDOUT:   %Ptr.impl_witness.loc7_55.2: <witness> = impl_witness %Ptr.impl_witness_table, @U.as.Ptr.impl(%U.loc7_21.2) [symbolic = %Ptr.impl_witness.loc7_55.2 (constants.%Ptr.impl_witness.5a1)]
 // CHECK:STDOUT:
@@ -1392,7 +1370,7 @@ fn F[T: Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT:   final impl: %U.ref.loc7_29 as %Ptr.ref {
 // CHECK:STDOUT:     %Ptr.impl_witness_table = impl_witness_table (%impl_witness_assoc_constant), @U.as.Ptr.impl [concrete]
 // CHECK:STDOUT:     %Ptr.impl_witness.loc7_55.1: <witness> = impl_witness %Ptr.impl_witness_table, @U.as.Ptr.impl(constants.%U.67d) [symbolic = %Ptr.impl_witness.loc7_55.2 (constants.%Ptr.impl_witness.5a1)]
-// CHECK:STDOUT:     %impl_witness_assoc_constant: type = impl_witness_assoc_constant constants.%ptr.e8f8f9.1 [symbolic = %ptr.loc7_53.2 (constants.%ptr.e8f8f9.1)]
+// CHECK:STDOUT:     %impl_witness_assoc_constant: type = impl_witness_assoc_constant constants.%ptr.e8f8f9.1 [symbolic = %ptr.loc7_38 (constants.%ptr.e8f8f9.1)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   !members:
 // CHECK:STDOUT:     extend %Ptr.ref
@@ -1453,7 +1431,7 @@ fn F[T: Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT: specific @U.as.Ptr.impl(constants.%U.67d) {
 // CHECK:STDOUT:   %U.patt.loc7_21.2 => constants.%U.patt.3a0
 // CHECK:STDOUT:   %U.loc7_21.2 => constants.%U.67d
-// CHECK:STDOUT:   %ptr.loc7_53.2 => constants.%ptr.e8f8f9.1
+// CHECK:STDOUT:   %ptr.loc7_38 => constants.%ptr.e8f8f9.1
 // CHECK:STDOUT:   %Ptr_where.type => constants.%Ptr_where.type.774
 // CHECK:STDOUT:   %.loc7_55 => constants.%.f8f
 // CHECK:STDOUT:   %Ptr.impl_witness.loc7_55.2 => constants.%Ptr.impl_witness.5a1
@@ -1470,7 +1448,7 @@ fn F[T: Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT: specific @U.as.Ptr.impl(constants.%T.as_type.468) {
 // CHECK:STDOUT:   %U.patt.loc7_21.2 => constants.%U.patt.3a0
 // CHECK:STDOUT:   %U.loc7_21.2 => constants.%T.as_type.468
-// CHECK:STDOUT:   %ptr.loc7_53.2 => constants.%ptr.ac4
+// CHECK:STDOUT:   %ptr.loc7_38 => constants.%ptr.ac4
 // CHECK:STDOUT:   %Ptr_where.type => constants.%Ptr_where.type.c27
 // CHECK:STDOUT:   %.loc7_55 => constants.%.d24
 // CHECK:STDOUT:   %Ptr.impl_witness.loc7_55.2 => constants.%Ptr.impl_witness.a83
@@ -1576,14 +1554,14 @@ fn F[T: Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT:     %.loc7_44: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.frozen.as_type]
 // CHECK:STDOUT:     %Type.ref: %Ptr.assoc_type = name_ref Type, @Type.%assoc0 [concrete = constants.%assoc0.b1a]
 // CHECK:STDOUT:     %impl.elem0.loc7_44.1: type = impl_witness_access constants.%.c6b, element0 [symbolic_self = constants.%impl.elem0.949]
-// CHECK:STDOUT:     %U.ref.loc7_52: type = name_ref U, %U.loc7_21.1 [symbolic = %U.loc7_21.2 (constants.%U.67d)]
-// CHECK:STDOUT:     %ptr.loc7_53.1: type = ptr_type %U.ref.loc7_52 [symbolic = %ptr.loc7_53.2 (constants.%ptr.e8f8f9.1)]
-// CHECK:STDOUT:     %rewrite.loc7_50.1 = requirement_rewrite %impl.elem0.loc7_44.1, %ptr.loc7_53.1 [concrete]
+// CHECK:STDOUT:     %U.ref.loc7_52: type = name_ref U, %U.loc7_21.1 [symbolic = constants.%U.67d]
+// CHECK:STDOUT:     %ptr.loc7_53: type = ptr_type %U.ref.loc7_52 [symbolic = constants.%ptr.e8f8f9.1]
+// CHECK:STDOUT:     %rewrite.loc7_50.1 = requirement_rewrite %impl.elem0.loc7_44.1, %ptr.loc7_53 [concrete]
 // CHECK:STDOUT:     %impl.elem0.loc7_44.2: type = impl_witness_access constants.%.51f, element0 [symbolic_self = constants.%impl.elem0.406]
-// CHECK:STDOUT:     %rewrite.loc7_50.2 = requirement_rewrite %impl.elem0.loc7_44.2, %ptr.loc7_53.1 [concrete]
+// CHECK:STDOUT:     %rewrite.loc7_50.2 = requirement_rewrite %impl.elem0.loc7_44.2, %ptr.loc7_53 [concrete]
 // CHECK:STDOUT:     %.loc7_38: type = where_expr [symbolic = %Ptr_where.type (constants.%Ptr_where.type.774)] {
 // CHECK:STDOUT:       %base_facet_type = requirement_base_facet_type %Ptr.ref [concrete]
-// CHECK:STDOUT:       %rewrite.loc7_50.2 = requirement_rewrite %impl.elem0.loc7_44.2, %ptr.loc7_53.1 [concrete]
+// CHECK:STDOUT:       %rewrite.loc7_50.2 = requirement_rewrite %impl.elem0.loc7_44.2, %ptr.loc7_53 [concrete]
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %.loc7_23.1: type = splice_block %.loc7_23.2 [concrete = type] {
 // CHECK:STDOUT:       %.Self.frozen.loc7_21: type = symbolic_binding .Self [symbolic_self = constants.%.Self.frozen.e58]
@@ -1641,8 +1619,8 @@ fn F[T: Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT: generic final impl @U.as.Ptr.impl(%U.loc7_21.1: type) {
 // CHECK:STDOUT:   %U.patt.loc7_21.2: %pattern_type.9a5 = symbolic_binding_pattern U, 0 [symbolic = %U.patt.loc7_21.2 (constants.%U.patt.3a0)]
 // CHECK:STDOUT:   %U.loc7_21.2: type = symbolic_binding U, 0 [symbolic = %U.loc7_21.2 (constants.%U.67d)]
-// CHECK:STDOUT:   %ptr.loc7_53.2: type = ptr_type %U.loc7_21.2 [symbolic = %ptr.loc7_53.2 (constants.%ptr.e8f8f9.1)]
-// CHECK:STDOUT:   %Ptr_where.type: type = facet_type <@Ptr where constants.%impl.elem0.406 = %ptr.loc7_53.2> [symbolic = %Ptr_where.type (constants.%Ptr_where.type.774)]
+// CHECK:STDOUT:   %ptr.loc7_38: type = ptr_type %U.loc7_21.2 [symbolic = %ptr.loc7_38 (constants.%ptr.e8f8f9.1)]
+// CHECK:STDOUT:   %Ptr_where.type: type = facet_type <@Ptr where constants.%impl.elem0.406 = %ptr.loc7_38> [symbolic = %Ptr_where.type (constants.%Ptr_where.type.774)]
 // CHECK:STDOUT:   %.loc7_55: <witness> = impl_self_witness %U.loc7_21.2, @Ptr [symbolic = %.loc7_55 (constants.%.f8f)]
 // CHECK:STDOUT:   %Ptr.impl_witness.loc7_55.2: <witness> = impl_witness %Ptr.impl_witness_table, @U.as.Ptr.impl(%U.loc7_21.2) [symbolic = %Ptr.impl_witness.loc7_55.2 (constants.%Ptr.impl_witness.5a1)]
 // CHECK:STDOUT:
@@ -1651,7 +1629,7 @@ fn F[T: Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT:   final impl: %U.ref.loc7_29 as %Ptr.ref {
 // CHECK:STDOUT:     %Ptr.impl_witness_table = impl_witness_table (%impl_witness_assoc_constant), @U.as.Ptr.impl [concrete]
 // CHECK:STDOUT:     %Ptr.impl_witness.loc7_55.1: <witness> = impl_witness %Ptr.impl_witness_table, @U.as.Ptr.impl(constants.%U.67d) [symbolic = %Ptr.impl_witness.loc7_55.2 (constants.%Ptr.impl_witness.5a1)]
-// CHECK:STDOUT:     %impl_witness_assoc_constant: type = impl_witness_assoc_constant constants.%ptr.e8f8f9.1 [symbolic = %ptr.loc7_53.2 (constants.%ptr.e8f8f9.1)]
+// CHECK:STDOUT:     %impl_witness_assoc_constant: type = impl_witness_assoc_constant constants.%ptr.e8f8f9.1 [symbolic = %ptr.loc7_38 (constants.%ptr.e8f8f9.1)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   !members:
 // CHECK:STDOUT:     extend %Ptr.ref
@@ -1712,7 +1690,7 @@ fn F[T: Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT: specific @U.as.Ptr.impl(constants.%U.67d) {
 // CHECK:STDOUT:   %U.patt.loc7_21.2 => constants.%U.patt.3a0
 // CHECK:STDOUT:   %U.loc7_21.2 => constants.%U.67d
-// CHECK:STDOUT:   %ptr.loc7_53.2 => constants.%ptr.e8f8f9.1
+// CHECK:STDOUT:   %ptr.loc7_38 => constants.%ptr.e8f8f9.1
 // CHECK:STDOUT:   %Ptr_where.type => constants.%Ptr_where.type.774
 // CHECK:STDOUT:   %.loc7_55 => constants.%.f8f
 // CHECK:STDOUT:   %Ptr.impl_witness.loc7_55.2 => constants.%Ptr.impl_witness.5a1
@@ -1725,7 +1703,7 @@ fn F[T: Ptr](var t: T) -> T.(Ptr.Type) {
 // CHECK:STDOUT: specific @U.as.Ptr.impl(constants.%T.as_type.468) {
 // CHECK:STDOUT:   %U.patt.loc7_21.2 => constants.%U.patt.3a0
 // CHECK:STDOUT:   %U.loc7_21.2 => constants.%T.as_type.468
-// CHECK:STDOUT:   %ptr.loc7_53.2 => constants.%ptr.ac4
+// CHECK:STDOUT:   %ptr.loc7_38 => constants.%ptr.ac4
 // CHECK:STDOUT:   %Ptr_where.type => constants.%Ptr_where.type.c27
 // CHECK:STDOUT:   %.loc7_55 => constants.%.d24
 // CHECK:STDOUT:   %Ptr.impl_witness.loc7_55.2 => constants.%Ptr.impl_witness.a83

toolchain/check/testdata/interface/observe.carbon

@@ -525,10 +525,10 @@ fn F[W: A, X: I(W)](x: X) {
 // CHECK:STDOUT:     %c: @Transitive.WithSelf.TakesC.%as_type (%as_type.95b) = wrapper_binding c, %c.param
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %assoc4: %Transitive.assoc_type = assoc_entity element4, %Transitive.WithSelf.TakesC.decl [concrete = constants.%assoc4]
-// CHECK:STDOUT:   %impl.elem0.loc16: %facet_type.6ce = impl_witness_access constants.%Transitive.lookup_impl_witness, element0 [symbolic = %impl.elem0.loc10 (constants.%impl.elem0)]
-// CHECK:STDOUT:   %A.ref: %facet_type.6ce = name_ref A, %impl.elem0.loc16 [symbolic = %impl.elem0.loc10 (constants.%impl.elem0)]
-// CHECK:STDOUT:   %impl.elem1.loc16: %facet_type.40a = impl_witness_access constants.%Transitive.lookup_impl_witness, element1 [symbolic = %impl.elem1.loc11 (constants.%impl.elem1)]
-// CHECK:STDOUT:   %B.ref: %facet_type.40a = name_ref B, %impl.elem1.loc16 [symbolic = %impl.elem1.loc11 (constants.%impl.elem1)]
+// CHECK:STDOUT:   %impl.elem0.loc16_11.1: %facet_type.6ce = impl_witness_access constants.%Transitive.lookup_impl_witness, element0 [symbolic = %impl.elem0.loc16_11.2 (constants.%impl.elem0)]
+// CHECK:STDOUT:   %A.ref: %facet_type.6ce = name_ref A, %impl.elem0.loc16_11.1 [symbolic = %impl.elem0.loc16_11.2 (constants.%impl.elem0)]
+// CHECK:STDOUT:   %impl.elem1.loc16_16.1: %facet_type.40a = impl_witness_access constants.%Transitive.lookup_impl_witness, element1 [symbolic = %impl.elem1.loc16_16.2 (constants.%impl.elem1)]
+// CHECK:STDOUT:   %B.ref: %facet_type.40a = name_ref B, %impl.elem1.loc16_16.1 [symbolic = %impl.elem1.loc16_16.2 (constants.%impl.elem1)]
 // CHECK:STDOUT:   %B.as_type.loc16_16.1: type = facet_access_type %B.ref [symbolic = %as_type.loc16_16 (constants.%as_type.a97)]
 // CHECK:STDOUT:   %.loc16_16.1: type = converted %B.ref, %B.as_type.loc16_16.1 [symbolic = %as_type.loc16_16 (constants.%as_type.a97)]
 // CHECK:STDOUT:   %A.as_type: type = facet_access_type %A.ref [symbolic = %as_type.loc16_11 (constants.%as_type.e89)]
@@ -838,7 +838,7 @@ fn F[W: A, X: I(W)](x: X) {
 // CHECK:STDOUT:       %.Self.frozen.loc9_17: %B.type = symbolic_binding .Self [symbolic_self = constants.%.Self.frozen.f7e]
 // CHECK:STDOUT:       %base_facet_type.loc9_17 = requirement_base_facet_type %B.ref [concrete]
 // CHECK:STDOUT:       %.Self.ref.loc9_23.1: %B.type = name_ref .Self, %.Self.frozen.loc9_17 [symbolic_self = constants.%.Self.frozen.f7e]
-// CHECK:STDOUT:       %T.ref.loc9: %A.type = name_ref T, %T.loc9_7.2 [symbolic = %T.loc9_7.1 (constants.%T)]
+// CHECK:STDOUT:       %T.ref.loc9: %A.type = name_ref T, %T.loc9_7.2 [symbolic = constants.%T]
 // CHECK:STDOUT:       %equiv.loc9_29.1 = requirement_equivalent %.Self.ref.loc9_23.1, %T.ref.loc9 [concrete]
 // CHECK:STDOUT:       %.Self.loc9_17: %B.type = symbolic_binding .Self [symbolic_self = constants.%.Self.263]
 // CHECK:STDOUT:       %.Self.ref.loc9_23.2: %B.type = name_ref .Self, %.Self.loc9_17 [symbolic_self = constants.%.Self.263]
@@ -855,7 +855,7 @@ fn F[W: A, X: I(W)](x: X) {
 // CHECK:STDOUT:       %.Self.frozen.loc9_40: %C.type = symbolic_binding .Self [symbolic_self = constants.%.Self.frozen.8d7]
 // CHECK:STDOUT:       %base_facet_type.loc9_40 = requirement_base_facet_type %C.ref [concrete]
 // CHECK:STDOUT:       %.Self.ref.loc9_46.1: %C.type = name_ref .Self, %.Self.frozen.loc9_40 [symbolic_self = constants.%.Self.frozen.8d7]
-// CHECK:STDOUT:       %U.ref.loc9: %B_where.type = name_ref U, %U.loc9_13.2 [symbolic = %U.loc9_13.1 (constants.%U)]
+// CHECK:STDOUT:       %U.ref.loc9: %B_where.type = name_ref U, %U.loc9_13.2 [symbolic = constants.%U]
 // CHECK:STDOUT:       %equiv.loc9_52.1 = requirement_equivalent %.Self.ref.loc9_46.1, %U.ref.loc9 [concrete]
 // CHECK:STDOUT:       %.Self.loc9_40: %C.type = symbolic_binding .Self [symbolic_self = constants.%.Self.a25]
 // CHECK:STDOUT:       %.Self.ref.loc9_46.2: %C.type = name_ref .Self, %.Self.loc9_40 [symbolic_self = constants.%.Self.a25]
@@ -1106,8 +1106,8 @@ fn F[W: A, X: I(W)](x: X) {
 // CHECK:STDOUT:     %assoc3.loc12_24.1: @I.WithSelf.%I.assoc_type (%I.assoc_type) = assoc_entity element3, %I.WithSelf.TakesT.decl [symbolic = %assoc3.loc12_24.2 (constants.%assoc3)]
 // CHECK:STDOUT:     %.loc14_11.1: %A.type = specific_constant @I.%T.loc7_14.2, @I(constants.%T) [symbolic = %T (constants.%T)]
 // CHECK:STDOUT:     %T.ref: %A.type = name_ref T, %.loc14_11.1 [symbolic = %T (constants.%T)]
-// CHECK:STDOUT:     %impl.elem0.loc14: %facet_type.dee = impl_witness_access constants.%I.lookup_impl_witness, element0 [symbolic = %impl.elem0.loc9 (constants.%impl.elem0)]
-// CHECK:STDOUT:     %U.ref: %facet_type.dee = name_ref U, %impl.elem0.loc14 [symbolic = %impl.elem0.loc9 (constants.%impl.elem0)]
+// CHECK:STDOUT:     %impl.elem0.loc14_16.1: %facet_type.dee = impl_witness_access constants.%I.lookup_impl_witness, element0 [symbolic = %impl.elem0.loc14_16.2 (constants.%impl.elem0)]
+// CHECK:STDOUT:     %U.ref: %facet_type.dee = name_ref U, %impl.elem0.loc14_16.1 [symbolic = %impl.elem0.loc14_16.2 (constants.%impl.elem0)]
 // CHECK:STDOUT:     %U.as_type.loc14_16.1: type = facet_access_type %U.ref [symbolic = %as_type.loc14_16 (constants.%as_type.a64)]
 // CHECK:STDOUT:     %.loc14_16.1: type = converted %U.ref, %U.as_type.loc14_16.1 [symbolic = %as_type.loc14_16 (constants.%as_type.a64)]
 // CHECK:STDOUT:     %T.as_type.loc14_11.1: type = facet_access_type %T.ref [symbolic = %T.as_type.loc14_11.2 (constants.%T.as_type)]

toolchain/check/testdata/interface/require.carbon

@@ -864,9 +864,9 @@ interface Z(T: type) {
 // CHECK:STDOUT:     %.loc10_25: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.frozen.as_type]
 // CHECK:STDOUT:     %Y1.ref: %Y.assoc_type = name_ref Y1, @Y1.%assoc0 [concrete = constants.%assoc0]
 // CHECK:STDOUT:     %impl.elem0.loc10_25.1: type = impl_witness_access constants.%Y.lookup_impl_witness.94c, element0 [symbolic_self = constants.%impl.elem0.74a]
-// CHECK:STDOUT:     %Self.ref: %Z.type = name_ref Self, @Z.%Self [symbolic = %Self (constants.%Self.cb6)]
-// CHECK:STDOUT:     %Self.as_type.loc10_31: type = facet_access_type %Self.ref [symbolic = %Self.as_type.loc10_11.2 (constants.%Self.as_type)]
-// CHECK:STDOUT:     %.loc10_31: type = converted %Self.ref, %Self.as_type.loc10_31 [symbolic = %Self.as_type.loc10_11.2 (constants.%Self.as_type)]
+// CHECK:STDOUT:     %Self.ref: %Z.type = name_ref Self, @Z.%Self [symbolic = constants.%Self.cb6]
+// CHECK:STDOUT:     %Self.as_type.loc10_31: type = facet_access_type %Self.ref [symbolic = constants.%Self.as_type]
+// CHECK:STDOUT:     %.loc10_31: type = converted %Self.ref, %Self.as_type.loc10_31 [symbolic = constants.%Self.as_type]
 // CHECK:STDOUT:     %rewrite.loc10_29.1 = requirement_rewrite %impl.elem0.loc10_25.1, %.loc10_31 [concrete]
 // CHECK:STDOUT:     %impl.elem0.loc10_25.2: type = impl_witness_access constants.%Y.lookup_impl_witness.9c7, element0 [symbolic_self = constants.%impl.elem0.591]
 // CHECK:STDOUT:     %rewrite.loc10_29.2 = requirement_rewrite %impl.elem0.loc10_25.2, %.loc10_31 [concrete]

toolchain/check/testdata/named_constraint/require.carbon

@@ -1392,9 +1392,9 @@ constraint N {
 // CHECK:STDOUT:     %.loc10_25: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.frozen.as_type]
 // CHECK:STDOUT:     %Y1.ref: %Y.assoc_type = name_ref Y1, @Y1.%assoc0 [concrete = constants.%assoc0]
 // CHECK:STDOUT:     %impl.elem0.loc10_25.1: type = impl_witness_access constants.%Y.lookup_impl_witness.94c, element0 [symbolic_self = constants.%impl.elem0.74a]
-// CHECK:STDOUT:     %Self.ref: %Z.type = name_ref Self, @Z.%Self [symbolic = %Self (constants.%Self.d87)]
-// CHECK:STDOUT:     %Self.as_type.loc10_31: type = facet_access_type %Self.ref [symbolic = %Self.as_type.loc10_11.2 (constants.%Self.as_type)]
-// CHECK:STDOUT:     %.loc10_31: type = converted %Self.ref, %Self.as_type.loc10_31 [symbolic = %Self.as_type.loc10_11.2 (constants.%Self.as_type)]
+// CHECK:STDOUT:     %Self.ref: %Z.type = name_ref Self, @Z.%Self [symbolic = constants.%Self.d87]
+// CHECK:STDOUT:     %Self.as_type.loc10_31: type = facet_access_type %Self.ref [symbolic = constants.%Self.as_type]
+// CHECK:STDOUT:     %.loc10_31: type = converted %Self.ref, %Self.as_type.loc10_31 [symbolic = constants.%Self.as_type]
 // CHECK:STDOUT:     %rewrite.loc10_29.1 = requirement_rewrite %impl.elem0.loc10_25.1, %.loc10_31 [concrete]
 // CHECK:STDOUT:     %impl.elem0.loc10_25.2: type = impl_witness_access constants.%Y.lookup_impl_witness.9c7, element0 [symbolic_self = constants.%impl.elem0.591]
 // CHECK:STDOUT:     %rewrite.loc10_29.2 = requirement_rewrite %impl.elem0.loc10_25.2, %.loc10_31 [concrete]

toolchain/check/testdata/operators/overloaded/index_with_prelude.carbon

@@ -96,7 +96,7 @@ let x: i32 = c[0];
 // CHECK:STDOUT:   %.Self.frozen.b2d: %IndexWith.type.a14 = symbolic_binding .Self [symbolic_self]
 // CHECK:STDOUT:   %IndexWith.assoc_type.e71: type = assoc_entity_type @IndexWith, @IndexWith(%SubscriptType.f8f) [concrete]
 // CHECK:STDOUT:   %assoc0.fda: %IndexWith.assoc_type.e71 = assoc_entity element0, imports.%Core.import_ref.fc2 [concrete]
-// CHECK:STDOUT:   %.Self.frozen.as_type.05c: type = facet_access_type %.Self.frozen.b2d [symbolic_self]
+// CHECK:STDOUT:   %.Self.frozen.as_type: type = facet_access_type %.Self.frozen.b2d [symbolic_self]
 // CHECK:STDOUT:   %assoc0.276285.2: %IndexWith.assoc_type.783 = assoc_entity element0, imports.%Core.import_ref.6b6e53.2 [symbolic]
 // CHECK:STDOUT:   %.1aa: <witness> = impl_self_witness %.Self.frozen.b2d, @IndexWith, @IndexWith(%SubscriptType.f8f) [symbolic_self]
 // CHECK:STDOUT:   %impl.elem0.c37: type = impl_witness_access %.1aa, element0 [symbolic_self]
@@ -172,8 +172,8 @@ let x: i32 = c[0];
 // CHECK:STDOUT:     %.Self.frozen: %IndexWith.type.a14 = symbolic_binding .Self [symbolic_self = constants.%.Self.frozen.b2d]
 // CHECK:STDOUT:     %base_facet_type = requirement_base_facet_type %IndexWith.type [concrete]
 // CHECK:STDOUT:     %.Self.ref: %IndexWith.type.a14 = name_ref .Self, %.Self.frozen [symbolic_self = constants.%.Self.frozen.b2d]
-// CHECK:STDOUT:     %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.frozen.as_type.05c]
-// CHECK:STDOUT:     %.loc8_47.1: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.frozen.as_type.05c]
+// CHECK:STDOUT:     %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.frozen.as_type]
+// CHECK:STDOUT:     %.loc8_47.1: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.frozen.as_type]
 // CHECK:STDOUT:     %.loc8_47.2: %IndexWith.assoc_type.e71 = specific_constant imports.%Core.import_ref.ef0, @IndexWith.WithSelf(constants.%SubscriptType.f8f, constants.%.Self.frozen.b2d) [concrete = constants.%assoc0.fda]
 // CHECK:STDOUT:     %ElementType.ref.loc8_47: %IndexWith.assoc_type.e71 = name_ref ElementType, %.loc8_47.2 [concrete = constants.%assoc0.fda]
 // CHECK:STDOUT:     %impl.elem0.loc8_47.1: type = impl_witness_access constants.%.1aa, element0 [symbolic_self = constants.%impl.elem0.c37]
@@ -315,7 +315,7 @@ let x: i32 = c[0];
 // CHECK:STDOUT:   %.Self.frozen.dd6: %IndexWith.type.06b = symbolic_binding .Self [symbolic_self]
 // CHECK:STDOUT:   %IndexWith.assoc_type.223: type = assoc_entity_type @IndexWith, @IndexWith(Core.IntLiteral) [concrete]
 // CHECK:STDOUT:   %assoc0.a00: %IndexWith.assoc_type.223 = assoc_entity element0, imports.%Core.import_ref.fc2 [concrete]
-// CHECK:STDOUT:   %.Self.frozen.as_type.748: type = facet_access_type %.Self.frozen.dd6 [symbolic_self]
+// CHECK:STDOUT:   %.Self.frozen.as_type: type = facet_access_type %.Self.frozen.dd6 [symbolic_self]
 // CHECK:STDOUT:   %assoc0.276285.2: %IndexWith.assoc_type.783 = assoc_entity element0, imports.%Core.import_ref.6b6e53.2 [symbolic]
 // CHECK:STDOUT:   %.601: <witness> = impl_self_witness %.Self.frozen.dd6, @IndexWith, @IndexWith(Core.IntLiteral) [symbolic_self]
 // CHECK:STDOUT:   %impl.elem0.500: type = impl_witness_access %.601, element0 [symbolic_self]
@@ -388,8 +388,8 @@ let x: i32 = c[0];
 // CHECK:STDOUT:     %.Self.frozen: %IndexWith.type.06b = symbolic_binding .Self [symbolic_self = constants.%.Self.frozen.dd6]
 // CHECK:STDOUT:     %base_facet_type = requirement_base_facet_type %IndexWith.type [concrete]
 // CHECK:STDOUT:     %.Self.ref: %IndexWith.type.06b = name_ref .Self, %.Self.frozen [symbolic_self = constants.%.Self.frozen.dd6]
-// CHECK:STDOUT:     %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.frozen.as_type.748]
-// CHECK:STDOUT:     %.loc8_54.1: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.frozen.as_type.748]
+// CHECK:STDOUT:     %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.frozen.as_type]
+// CHECK:STDOUT:     %.loc8_54.1: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.frozen.as_type]
 // CHECK:STDOUT:     %.loc8_54.2: %IndexWith.assoc_type.223 = specific_constant imports.%Core.import_ref.ef0, @IndexWith.WithSelf(Core.IntLiteral, constants.%.Self.frozen.dd6) [concrete = constants.%assoc0.a00]
 // CHECK:STDOUT:     %ElementType.ref: %IndexWith.assoc_type.223 = name_ref ElementType, %.loc8_54.2 [concrete = constants.%assoc0.a00]
 // CHECK:STDOUT:     %impl.elem0.loc8_54.1: type = impl_witness_access constants.%.601, element0 [symbolic_self = constants.%impl.elem0.500]
@@ -523,7 +523,7 @@ let x: i32 = c[0];
 // CHECK:STDOUT:   %.Self.frozen.b2d: %IndexWith.type.a14 = symbolic_binding .Self [symbolic_self]
 // CHECK:STDOUT:   %IndexWith.assoc_type.e71: type = assoc_entity_type @IndexWith, @IndexWith(%SubscriptType.f8f) [concrete]
 // CHECK:STDOUT:   %assoc0.fda: %IndexWith.assoc_type.e71 = assoc_entity element0, imports.%Core.import_ref.fc2 [concrete]
-// CHECK:STDOUT:   %.Self.frozen.as_type.05c: type = facet_access_type %.Self.frozen.b2d [symbolic_self]
+// CHECK:STDOUT:   %.Self.frozen.as_type: type = facet_access_type %.Self.frozen.b2d [symbolic_self]
 // CHECK:STDOUT:   %assoc0.276285.2: %IndexWith.assoc_type.783 = assoc_entity element0, imports.%Core.import_ref.6b6e53.2 [symbolic]
 // CHECK:STDOUT:   %.1aa: <witness> = impl_self_witness %.Self.frozen.b2d, @IndexWith, @IndexWith(%SubscriptType.f8f) [symbolic_self]
 // CHECK:STDOUT:   %impl.elem0.c37: type = impl_witness_access %.1aa, element0 [symbolic_self]
@@ -594,8 +594,8 @@ let x: i32 = c[0];
 // CHECK:STDOUT:     %.Self.frozen: %IndexWith.type.a14 = symbolic_binding .Self [symbolic_self = constants.%.Self.frozen.b2d]
 // CHECK:STDOUT:     %base_facet_type = requirement_base_facet_type %IndexWith.type [concrete]
 // CHECK:STDOUT:     %.Self.ref: %IndexWith.type.a14 = name_ref .Self, %.Self.frozen [symbolic_self = constants.%.Self.frozen.b2d]
-// CHECK:STDOUT:     %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.frozen.as_type.05c]
-// CHECK:STDOUT:     %.loc8_47.1: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.frozen.as_type.05c]
+// CHECK:STDOUT:     %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.frozen.as_type]
+// CHECK:STDOUT:     %.loc8_47.1: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.frozen.as_type]
 // CHECK:STDOUT:     %.loc8_47.2: %IndexWith.assoc_type.e71 = specific_constant imports.%Core.import_ref.ef0, @IndexWith.WithSelf(constants.%SubscriptType.f8f, constants.%.Self.frozen.b2d) [concrete = constants.%assoc0.fda]
 // CHECK:STDOUT:     %ElementType.ref.loc8_47: %IndexWith.assoc_type.e71 = name_ref ElementType, %.loc8_47.2 [concrete = constants.%assoc0.fda]
 // CHECK:STDOUT:     %impl.elem0.loc8_47.1: type = impl_witness_access constants.%.1aa, element0 [symbolic_self = constants.%impl.elem0.c37]

toolchain/check/testdata/where_expr/dot_self_index.carbon

@@ -39,7 +39,6 @@ fn G(U: Empty(i32) where .A = i32*) {
 // CHECK:STDOUT:   %.Self.frozen.3b0: %Empty.type.f57232.2 = symbolic_binding .Self [symbolic]
 // CHECK:STDOUT:   %Empty.assoc_type.52a113.2: type = assoc_entity_type @Empty, @Empty(%T) [symbolic]
 // CHECK:STDOUT:   %assoc0.280be6.2: %Empty.assoc_type.52a113.2 = assoc_entity element0, @Empty.WithSelf.%A [symbolic]
-// CHECK:STDOUT:   %require_complete.4f0: <witness> = require_complete_type %Empty.type.f57232.2 [symbolic]
 // CHECK:STDOUT:   %.Self.frozen.as_type.dd3: type = facet_access_type %.Self.frozen.3b0 [symbolic]
 // CHECK:STDOUT:   %Empty.lookup_impl_witness.cfd: <witness> = lookup_impl_witness %.Self.frozen.3b0, @Empty, @Empty(%T) [symbolic]
 // CHECK:STDOUT:   %impl.elem0.14d: type = impl_witness_access %Empty.lookup_impl_witness.cfd, element0 [symbolic]
@@ -60,11 +59,6 @@ fn G(U: Empty(i32) where .A = i32*) {
 // CHECK:STDOUT:   %i32: type = class_type @Int, @Int(%int_32) [concrete]
 // CHECK:STDOUT:   %Empty.type.650: type = facet_type <@Empty, @Empty(%i32)> [concrete]
 // CHECK:STDOUT:   %.Self.frozen.322: %Empty.type.650 = symbolic_binding .Self [symbolic_self]
-// CHECK:STDOUT:   %Empty.assoc_type.aa2: type = assoc_entity_type @Empty, @Empty(%i32) [concrete]
-// CHECK:STDOUT:   %assoc0.490: %Empty.assoc_type.aa2 = assoc_entity element0, @Empty.WithSelf.%A [concrete]
-// CHECK:STDOUT:   %.Self.frozen.as_type.e1c: type = facet_access_type %.Self.frozen.322 [symbolic_self]
-// CHECK:STDOUT:   %Empty.lookup_impl_witness.14f: <witness> = lookup_impl_witness %.Self.frozen.322, @Empty, @Empty(%i32) [symbolic_self]
-// CHECK:STDOUT:   %impl.elem0.b94: type = impl_witness_access %Empty.lookup_impl_witness.14f, element0 [symbolic_self]
 // CHECK:STDOUT:   %ptr.a17: type = ptr_type %i32 [concrete]
 // CHECK:STDOUT:   %.Self.245: %Empty.type.650 = symbolic_binding .Self [symbolic_self]
 // CHECK:STDOUT:   %Empty.lookup_impl_witness.041: <witness> = lookup_impl_witness %.Self.245, @Empty, @Empty(%i32) [symbolic_self]
@@ -72,7 +66,6 @@ fn G(U: Empty(i32) where .A = i32*) {
 // CHECK:STDOUT:   %Empty_where.type.69a: type = facet_type <@Empty, @Empty(%i32) where %impl.elem0.69f = %ptr.a17> [concrete]
 // CHECK:STDOUT:   %pattern_type.574: type = pattern_type %Empty_where.type.69a [concrete]
 // CHECK:STDOUT:   %U.param_patt.a03: %pattern_type.574 = value_param_pattern [concrete]
-// CHECK:STDOUT:   %complete_type.967: <witness> = complete_type_witness %Empty.type.650 [concrete]
 // CHECK:STDOUT:   %U.patt.7363b8.2: %pattern_type.574 = wrapper_binding_pattern U, %U.param_patt.a03 [concrete]
 // CHECK:STDOUT:   %complete_type.348: <witness> = complete_type_witness %Empty_where.type.69a [concrete]
 // CHECK:STDOUT: }
@@ -96,20 +89,20 @@ fn G(U: Empty(i32) where .A = i32*) {
 // CHECK:STDOUT:       %Empty.type.loc21_40.2: type = facet_type <@Empty, @Empty(constants.%T)> [symbolic = %Empty.type.loc21_40.1 (constants.%Empty.type.f57232.2)]
 // CHECK:STDOUT:       %.Self.frozen.loc21_42.2: @H.%Empty.type.loc21_40.1 (%Empty.type.f57232.2) = symbolic_binding .Self [symbolic = %.Self.frozen.loc21_42.1 (constants.%.Self.frozen.3b0)]
 // CHECK:STDOUT:       %base_facet_type = requirement_base_facet_type %Empty.type.loc21_40.2 [concrete]
-// CHECK:STDOUT:       %.Self.ref: @H.%Empty.type.loc21_40.1 (%Empty.type.f57232.2) = name_ref .Self, %.Self.frozen.loc21_42.2 [symbolic = %.Self.frozen.loc21_42.1 (constants.%.Self.frozen.3b0)]
-// CHECK:STDOUT:       %.Self.as_type: type = facet_access_type %.Self.ref [symbolic = %.Self.frozen.as_type (constants.%.Self.frozen.as_type.dd3)]
-// CHECK:STDOUT:       %.loc21_48.1: type = converted %.Self.ref, %.Self.as_type [symbolic = %.Self.frozen.as_type (constants.%.Self.frozen.as_type.dd3)]
-// CHECK:STDOUT:       %.loc21_48.2: @H.%Empty.assoc_type (%Empty.assoc_type.52a113.2) = specific_constant @A.%assoc0, @Empty.WithSelf(constants.%T, constants.%.Self.frozen.3b0) [symbolic = %assoc0 (constants.%assoc0.280be6.2)]
-// CHECK:STDOUT:       %A.ref: @H.%Empty.assoc_type (%Empty.assoc_type.52a113.2) = name_ref A, %.loc21_48.2 [symbolic = %assoc0 (constants.%assoc0.280be6.2)]
-// CHECK:STDOUT:       %impl.elem0.loc21_48.3: type = impl_witness_access constants.%Empty.lookup_impl_witness.cfd, element0 [symbolic = %impl.elem0.loc21_48.1 (constants.%impl.elem0.14d)]
-// CHECK:STDOUT:       %T.ref.loc21_53: type = name_ref T, %T.loc21_15.2 [symbolic = %T.loc21_15.1 (constants.%T)]
-// CHECK:STDOUT:       %ptr.loc21_54.2: type = ptr_type %T.ref.loc21_53 [symbolic = %ptr.loc21_54.1 (constants.%ptr.e8f)]
-// CHECK:STDOUT:       %rewrite.loc21_51.1 = requirement_rewrite %impl.elem0.loc21_48.3, %ptr.loc21_54.2 [concrete]
-// CHECK:STDOUT:       %impl.elem0.loc21_48.4: type = impl_witness_access constants.%Empty.lookup_impl_witness.ea2, element0 [symbolic = %impl.elem0.loc21_48.2 (constants.%impl.elem0.2a8)]
-// CHECK:STDOUT:       %rewrite.loc21_51.2 = requirement_rewrite %impl.elem0.loc21_48.4, %ptr.loc21_54.2 [concrete]
+// CHECK:STDOUT:       %.Self.ref: %Empty.type.f57232.2 = name_ref .Self, %.Self.frozen.loc21_42.2 [symbolic = constants.%.Self.frozen.3b0]
+// CHECK:STDOUT:       %.Self.as_type: type = facet_access_type %.Self.ref [symbolic = constants.%.Self.frozen.as_type.dd3]
+// CHECK:STDOUT:       %.loc21_48.1: type = converted %.Self.ref, %.Self.as_type [symbolic = constants.%.Self.frozen.as_type.dd3]
+// CHECK:STDOUT:       %.loc21_48.2: %Empty.assoc_type.52a113.2 = specific_constant @A.%assoc0, @Empty.WithSelf(constants.%T, constants.%.Self.frozen.3b0) [symbolic = constants.%assoc0.280be6.2]
+// CHECK:STDOUT:       %A.ref: %Empty.assoc_type.52a113.2 = name_ref A, %.loc21_48.2 [symbolic = constants.%assoc0.280be6.2]
+// CHECK:STDOUT:       %impl.elem0.loc21_48.1: type = impl_witness_access constants.%Empty.lookup_impl_witness.cfd, element0 [symbolic = constants.%impl.elem0.14d]
+// CHECK:STDOUT:       %T.ref.loc21_53: type = name_ref T, %T.loc21_15.2 [symbolic = constants.%T]
+// CHECK:STDOUT:       %ptr.loc21_54: type = ptr_type %T.ref.loc21_53 [symbolic = constants.%ptr.e8f]
+// CHECK:STDOUT:       %rewrite.loc21_51.1 = requirement_rewrite %impl.elem0.loc21_48.1, %ptr.loc21_54 [concrete]
+// CHECK:STDOUT:       %impl.elem0.loc21_48.2: type = impl_witness_access constants.%Empty.lookup_impl_witness.ea2, element0 [symbolic = constants.%impl.elem0.2a8]
+// CHECK:STDOUT:       %rewrite.loc21_51.2 = requirement_rewrite %impl.elem0.loc21_48.2, %ptr.loc21_54 [concrete]
 // CHECK:STDOUT:       %.loc21_42.2: type = where_expr [symbolic = %Empty_where.type (constants.%Empty_where.type.4e8)] {
 // CHECK:STDOUT:         %base_facet_type = requirement_base_facet_type %Empty.type.loc21_40.2 [concrete]
-// CHECK:STDOUT:         %rewrite.loc21_51.2 = requirement_rewrite %impl.elem0.loc21_48.4, %ptr.loc21_54.2 [concrete]
+// CHECK:STDOUT:         %rewrite.loc21_51.2 = requirement_rewrite %impl.elem0.loc21_48.2, %ptr.loc21_54 [concrete]
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %U: @H.%Empty_where.type (%Empty_where.type.4e8) = wrapper_binding U, %U.param
@@ -126,17 +119,11 @@ fn G(U: Empty(i32) where .A = i32*) {
 // CHECK:STDOUT:   %T.loc21_15.1: type = symbolic_binding T, 0 [symbolic = %T.loc21_15.1 (constants.%T)]
 // CHECK:STDOUT:   %Empty.type.loc21_40.1: type = facet_type <@Empty, @Empty(%T.loc21_15.1)> [symbolic = %Empty.type.loc21_40.1 (constants.%Empty.type.f57232.2)]
 // CHECK:STDOUT:   %.Self.frozen.loc21_42.1: @H.%Empty.type.loc21_40.1 (%Empty.type.f57232.2) = symbolic_binding .Self [symbolic = %.Self.frozen.loc21_42.1 (constants.%.Self.frozen.3b0)]
-// CHECK:STDOUT:   %require_complete.loc21_48: <witness> = require_complete_type %Empty.type.loc21_40.1 [symbolic = %require_complete.loc21_48 (constants.%require_complete.4f0)]
-// CHECK:STDOUT:   %.Self.frozen.as_type: type = facet_access_type %.Self.frozen.loc21_42.1 [symbolic = %.Self.frozen.as_type (constants.%.Self.frozen.as_type.dd3)]
-// CHECK:STDOUT:   %Empty.assoc_type: type = assoc_entity_type @Empty, @Empty(%T.loc21_15.1) [symbolic = %Empty.assoc_type (constants.%Empty.assoc_type.52a113.2)]
-// CHECK:STDOUT:   %assoc0: @H.%Empty.assoc_type (%Empty.assoc_type.52a113.2) = assoc_entity element0, @Empty.WithSelf.%A [symbolic = %assoc0 (constants.%assoc0.280be6.2)]
-// CHECK:STDOUT:   %Empty.lookup_impl_witness.loc21_48.1: <witness> = lookup_impl_witness %.Self.frozen.loc21_42.1, @Empty, @Empty(%T.loc21_15.1) [symbolic = %Empty.lookup_impl_witness.loc21_48.1 (constants.%Empty.lookup_impl_witness.cfd)]
-// CHECK:STDOUT:   %impl.elem0.loc21_48.1: type = impl_witness_access %Empty.lookup_impl_witness.loc21_48.1, element0 [symbolic = %impl.elem0.loc21_48.1 (constants.%impl.elem0.14d)]
-// CHECK:STDOUT:   %ptr.loc21_54.1: type = ptr_type %T.loc21_15.1 [symbolic = %ptr.loc21_54.1 (constants.%ptr.e8f)]
 // CHECK:STDOUT:   %.Self: @H.%Empty.type.loc21_40.1 (%Empty.type.f57232.2) = symbolic_binding .Self [symbolic = %.Self (constants.%.Self.4bb)]
-// CHECK:STDOUT:   %Empty.lookup_impl_witness.loc21_48.2: <witness> = lookup_impl_witness %.Self, @Empty, @Empty(%T.loc21_15.1) [symbolic = %Empty.lookup_impl_witness.loc21_48.2 (constants.%Empty.lookup_impl_witness.ea2)]
-// CHECK:STDOUT:   %impl.elem0.loc21_48.2: type = impl_witness_access %Empty.lookup_impl_witness.loc21_48.2, element0 [symbolic = %impl.elem0.loc21_48.2 (constants.%impl.elem0.2a8)]
-// CHECK:STDOUT:   %Empty_where.type: type = facet_type <@Empty, @Empty(%T.loc21_15.1) where %impl.elem0.loc21_48.2 = %ptr.loc21_54.1> [symbolic = %Empty_where.type (constants.%Empty_where.type.4e8)]
+// CHECK:STDOUT:   %Empty.lookup_impl_witness: <witness> = lookup_impl_witness %.Self, @Empty, @Empty(%T.loc21_15.1) [symbolic = %Empty.lookup_impl_witness (constants.%Empty.lookup_impl_witness.ea2)]
+// CHECK:STDOUT:   %impl.elem0.loc21_42: type = impl_witness_access %Empty.lookup_impl_witness, element0 [symbolic = %impl.elem0.loc21_42 (constants.%impl.elem0.2a8)]
+// CHECK:STDOUT:   %ptr.loc21_42: type = ptr_type %T.loc21_15.1 [symbolic = %ptr.loc21_42 (constants.%ptr.e8f)]
+// CHECK:STDOUT:   %Empty_where.type: type = facet_type <@Empty, @Empty(%T.loc21_15.1) where %impl.elem0.loc21_42 = %ptr.loc21_42> [symbolic = %Empty_where.type (constants.%Empty_where.type.4e8)]
 // CHECK:STDOUT:   %pattern_type: type = pattern_type %Empty_where.type [symbolic = %pattern_type (constants.%pattern_type.67b)]
 // CHECK:STDOUT:   %U.param_patt.loc21_31.2: @H.%pattern_type (%pattern_type.67b) = value_param_pattern [symbolic = %U.param_patt.loc21_31.2 (constants.%U.param_patt.6e9)]
 // CHECK:STDOUT:   %U.patt.loc21_31.2: @H.%pattern_type (%pattern_type.67b) = wrapper_binding_pattern U, %U.param_patt.loc21_31.2 [symbolic = %U.patt.loc21_31.2 (constants.%U.patt.a80)]
@@ -144,7 +131,7 @@ fn G(U: Empty(i32) where .A = i32*) {
 // CHECK:STDOUT:   %V.loc21_73.1: type = symbolic_binding V, 1 [symbolic = %V.loc21_73.1 (constants.%V)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
-// CHECK:STDOUT:   %require_complete.loc21_31: <witness> = require_complete_type %Empty_where.type [symbolic = %require_complete.loc21_31 (constants.%require_complete.980)]
+// CHECK:STDOUT:   %require_complete: <witness> = require_complete_type %Empty_where.type [symbolic = %require_complete (constants.%require_complete.980)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   fn(%U.param: @H.%Empty_where.type (%Empty_where.type.4e8)) {
 // CHECK:STDOUT:   !entry:
@@ -157,16 +144,10 @@ fn G(U: Empty(i32) where .A = i32*) {
 // CHECK:STDOUT:   %T.loc21_15.1 => constants.%T
 // CHECK:STDOUT:   %Empty.type.loc21_40.1 => constants.%Empty.type.f57232.2
 // CHECK:STDOUT:   %.Self.frozen.loc21_42.1 => constants.%.Self.frozen.3b0
-// CHECK:STDOUT:   %require_complete.loc21_48 => constants.%require_complete.4f0
-// CHECK:STDOUT:   %.Self.frozen.as_type => constants.%.Self.frozen.as_type.dd3
-// CHECK:STDOUT:   %Empty.assoc_type => constants.%Empty.assoc_type.52a113.2
-// CHECK:STDOUT:   %assoc0 => constants.%assoc0.280be6.2
-// CHECK:STDOUT:   %Empty.lookup_impl_witness.loc21_48.1 => constants.%Empty.lookup_impl_witness.cfd
-// CHECK:STDOUT:   %impl.elem0.loc21_48.1 => constants.%impl.elem0.14d
-// CHECK:STDOUT:   %ptr.loc21_54.1 => constants.%ptr.e8f
 // CHECK:STDOUT:   %.Self => constants.%.Self.4bb
-// CHECK:STDOUT:   %Empty.lookup_impl_witness.loc21_48.2 => constants.%Empty.lookup_impl_witness.ea2
-// CHECK:STDOUT:   %impl.elem0.loc21_48.2 => constants.%impl.elem0.2a8
+// CHECK:STDOUT:   %Empty.lookup_impl_witness => constants.%Empty.lookup_impl_witness.ea2
+// CHECK:STDOUT:   %impl.elem0.loc21_42 => constants.%impl.elem0.2a8
+// CHECK:STDOUT:   %ptr.loc21_42 => constants.%ptr.e8f
 // CHECK:STDOUT:   %Empty_where.type => constants.%Empty_where.type.4e8
 // CHECK:STDOUT:   %pattern_type => constants.%pattern_type.67b
 // CHECK:STDOUT:   %U.param_patt.loc21_31.2 => constants.%U.param_patt.6e9
@@ -180,16 +161,10 @@ fn G(U: Empty(i32) where .A = i32*) {
 // CHECK:STDOUT:   %T.loc21_15.1 => constants.%i32
 // CHECK:STDOUT:   %Empty.type.loc21_40.1 => constants.%Empty.type.650
 // CHECK:STDOUT:   %.Self.frozen.loc21_42.1 => constants.%.Self.frozen.322
-// CHECK:STDOUT:   %require_complete.loc21_48 => constants.%complete_type.967
-// CHECK:STDOUT:   %.Self.frozen.as_type => constants.%.Self.frozen.as_type.e1c
-// CHECK:STDOUT:   %Empty.assoc_type => constants.%Empty.assoc_type.aa2
-// CHECK:STDOUT:   %assoc0 => constants.%assoc0.490
-// CHECK:STDOUT:   %Empty.lookup_impl_witness.loc21_48.1 => constants.%Empty.lookup_impl_witness.14f
-// CHECK:STDOUT:   %impl.elem0.loc21_48.1 => constants.%impl.elem0.b94
-// CHECK:STDOUT:   %ptr.loc21_54.1 => constants.%ptr.a17
 // CHECK:STDOUT:   %.Self => constants.%.Self.245
-// CHECK:STDOUT:   %Empty.lookup_impl_witness.loc21_48.2 => constants.%Empty.lookup_impl_witness.041
-// CHECK:STDOUT:   %impl.elem0.loc21_48.2 => constants.%impl.elem0.69f
+// CHECK:STDOUT:   %Empty.lookup_impl_witness => constants.%Empty.lookup_impl_witness.041
+// CHECK:STDOUT:   %impl.elem0.loc21_42 => constants.%impl.elem0.69f
+// CHECK:STDOUT:   %ptr.loc21_42 => constants.%ptr.a17
 // CHECK:STDOUT:   %Empty_where.type => constants.%Empty_where.type.69a
 // CHECK:STDOUT:   %pattern_type => constants.%pattern_type.574
 // CHECK:STDOUT:   %U.param_patt.loc21_31.2 => constants.%U.param_patt.a03
@@ -198,6 +173,6 @@ fn G(U: Empty(i32) where .A = i32*) {
 // CHECK:STDOUT:   %V.loc21_73.1 => bool
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
-// CHECK:STDOUT:   %require_complete.loc21_31 => constants.%complete_type.348
+// CHECK:STDOUT:   %require_complete => constants.%complete_type.348
 // CHECK:STDOUT: }
 // CHECK:STDOUT:

toolchain/sem_ir/expr_info.cpp

@@ -294,6 +294,13 @@ auto FindStorageArgForInitializerInSpecific(const File& sem_ir, InstId init_id,
         init_id = init.result_id;
         continue;
       }
+      case CARBON_KIND(ImplWitnessAssociatedConstant init): {
+        if (!allow_transitive) {
+          return {ir, InstId::None};
+        }
+        init_id = init.inst_id;
+        continue;
+      }
       case CARBON_KIND(UpdateInit init): {
         if (!allow_transitive) {
           return {ir, InstId::None};