diff --git a/toolchain/check/facet_type.cpp b/toolchain/check/facet_type.cpp index d366e2da7421..0e94e6ace0b5 100644 --- a/toolchain/check/facet_type.cpp +++ b/toolchain/check/facet_type.cpp @@ -177,21 +177,23 @@ class SubstImplWitnessAccessCallbacks : public SubstInstCallbacks { return SubstResult::SubstOperands; } - // If the access is going through a nested `ImplWitnessAccess`, that - // access needs to be resolved to a facet value first. If it can't be - // resolved then the outer one can not be either. - if (auto lookup = context().insts().TryGetAs( - rhs_access->inst.witness_id)) { - if (context().insts().Is( - lookup->query_self_inst_id)) { - substs_in_progress_.push_back(rhs_inst_id); - return SubstResult::SubstOperandsAndRetry; - } - } - auto* rewrite_value = rewrite_values_->FindRef(context(), rhs_access->inst_id); if (!rewrite_value) { + // The access is going through a nested `ImplWitnessAccess`, and we could + // not find a rewrite to replace the combined access. So we need to try + // replace the outer one and then try the combined one again. If the outer + // access doesn't get replaced by any rewrite, then the combined access + // won't be either. + if (auto lookup = context().insts().TryGetAs( + rhs_access->inst.witness_id)) { + if (context().insts().Is( + lookup->query_self_inst_id)) { + substs_in_progress_.push_back(rhs_inst_id); + return SubstResult::SubstOperandsAndRetry; + } + } + // The RHS refers to an associated constant for which there is no rewrite // rule. return SubstResult::FullySubstituted; diff --git a/toolchain/check/testdata/facet/validate_rewrite_constraints.carbon b/toolchain/check/testdata/facet/validate_rewrite_constraints.carbon index c683202193fe..52940f1b56b7 100644 --- a/toolchain/check/testdata/facet/validate_rewrite_constraints.carbon +++ b/toolchain/check/testdata/facet/validate_rewrite_constraints.carbon @@ -1413,3 +1413,24 @@ fn G(T:! I where .I1 = {}) { // information that `.I1 = {}`. F(T); } + +// --- resolve_nested_impl_witness_access.carbon +library "[[@TEST_NAME]]"; + +interface Y { + let Y1:! type; +} +interface Z { + let Z1:! Y; + let Z2:! type; +} + +fn G(_:! Z where .Z2 = ()) {} + +// Split the assignment of .Y1 and the use of it into separate facet types so +// that the early rewrite application doesn't get to see the value of .Y1 where +// it's used. Then rewrite constraint resolution has to do the replacement of +// .Z1.Y1 so that we know .Z2 = () as required by G. +fn F(T:! (Z where .Z1 impls (Y where .Y1 = ())) & (Z where .Z2 = .Z1.Y1)) { + G(T); +}