From ed1a949b47316b443338780e1bf56c1f82c3346b Mon Sep 17 00:00:00 2001
From: Dana Jansens <danakj@orodu.net>
Date: Fri, 15 May 2026 16:31:28 -0400
Subject: [PATCH] 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.
---
 toolchain/check/facet_type.cpp                | 26 ++++++++++---------
 .../facet/validate_rewrite_constraints.carbon | 21 +++++++++++++++
 2 files changed, 35 insertions(+), 12 deletions(-)

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<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;
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);
+}