Resolve nested ImplWitnessAccesses in rewrite constraints (#7213)

We were assuming that a nested access meant that we'd resolve the outer
one, then the inner one. But it may be that we can just resolve the
entire nested access together. Previously if we encountered this, it led
to a CHECK failure. Now we correctly resolve it.
This commit is contained in:
Dana Jansens
2026-05-15 20:31:28 +00:00
committed by GitHub
parent e041afd98d
commit ed1a949b47
2 changed files with 35 additions and 12 deletions
+14 -12
View File
@@ -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<SemIR::LookupImplWitness>(
rhs_access->inst.witness_id)) {
if (context().insts().Is<SemIR::ImplWitnessAccess>(
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<SemIR::LookupImplWitness>(
rhs_access->inst.witness_id)) {
if (context().insts().Is<SemIR::ImplWitnessAccess>(
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;
@@ -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);
}