More tests for early rewrite application and implied constraints (#5892)

Attempting to capture all the use cases described in [open discussion
2025-07-31](https://docs.google.com/document/d/1Yt-i5AmF76LSvD4TrWRIAE_92kii6j5yFiW-S7ahzlg/edit?tab=t.0#heading=h.lup43xycic7t).

toolchain/check/testdata/facet/early_rewrites.carbon

@@ -13,9 +13,11 @@
 // Tests where `ImplWitnessAccess` on the RHS of a rewrite constraint is used in
 // other constraints within the same facet type in ways that require the RHS to
 // be evaluated to a concrete value before the facet type is resolved (such as
-// by passing it as a parameter to a generic class).
+// by passing it as a parameter to a generic class). This can be done either by
+// eagerly reading rewrite constraints from the same facet type, or by relying
+// on implied constraints which are checked later.
 
-// --- nested_constraint_visible_in_type_parameter.carbon
+// --- fail_todo_implied_constraint_on_self.carbon
 library "[[@TEST_NAME]]";
 
 interface Z {
@@ -26,9 +28,140 @@ interface Z {
 class C(T:! Z where .Z1 = ()) {}
 
 interface J {
+  // Implied: .Z1 == ()
+  // CHECK:STDERR: fail_todo_implied_constraint_on_self.carbon:[[@LINE+7]]:26: error: cannot convert type `.Self` that implements `Z` into type implementing `Z where .(Z.Z1) = ()` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   let J1:! Z where .Z2 = C(.Self);
+  // CHECK:STDERR:                          ^~~~~~~~
+  // CHECK:STDERR: fail_todo_implied_constraint_on_self.carbon:[[@LINE-7]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: class C(T:! Z where .Z1 = ()) {}
+  // CHECK:STDERR:         ^
+  // CHECK:STDERR:
+  let J1:! Z where .Z2 = C(.Self);
+}
+
+fn F(T:! J) {}
+
+class D;
+// Satisfies the implied constraint in J.J1.
+// CHECK:STDERR: fail_todo_implied_constraint_on_self.carbon:[[@LINE+7]]:38: error: cannot convert type `.Self` that implements `Z` into type implementing `Z where .(Z.Z1) = ()` [ConversionFailureFacetToFacet]
+// CHECK:STDERR: impl D as Z where .Z1 = () and .Z2 = C(.Self) {}
+// CHECK:STDERR:                                      ^~~~~~~~
+// CHECK:STDERR: fail_todo_implied_constraint_on_self.carbon:[[@LINE-21]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+// CHECK:STDERR: class C(T:! Z where .Z1 = ()) {}
+// CHECK:STDERR:         ^
+// CHECK:STDERR:
+impl D as Z where .Z1 = () and .Z2 = C(.Self) {}
+fn G(T:! J where .J1 = D) {
+  F(T);
+}
+
+// --- fail_todo_implied_constraint_on_associated_constant.carbon
+library "[[@TEST_NAME]]";
+
+interface Z {
+  let Z1:! type;
+  let Z2:! type;
+}
+
+interface Tuple {}
+impl () as Tuple {}
+
+class C(T:! Tuple) {}
+
+interface J {
+  // Implied: .Z1 impls Tuple
+  // CHECK:STDERR: fail_todo_implied_constraint_on_associated_constant.carbon:[[@LINE+7]]:26: error: cannot convert type `.(Z.Z1)` into type implementing `Tuple` [ConversionFailureTypeToFacet]
+  // CHECK:STDERR:   let J1:! Z where .Z2 = C(.Z1);
+  // CHECK:STDERR:                          ^~~~~~
+  // CHECK:STDERR: fail_todo_implied_constraint_on_associated_constant.carbon:[[@LINE-7]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: class C(T:! Tuple) {}
+  // CHECK:STDERR:         ^
+  // CHECK:STDERR:
+  let J1:! Z where .Z2 = C(.Z1);
+}
+
+fn F(T:! J) {}
+
+class D;
+// Satisfies the implied constraint in J.J1.
+impl D as Z where .Z1 = () and .Z2 = C(()) {}
+fn G(T:! J where .J1 = D) {
+  F(T);
+}
+
+// --- fail_todo_nested_constraint_visible_in_type_parameter.carbon
+library "[[@TEST_NAME]]";
+
+interface Z {
+  let Z1:! type;
+  let Z2:! type;
+}
+
+class C(T:! Z where .Z1 = ()) {}
+
+interface J {
+  // Implied: .Z1 == (), but this is also explicitly required for J1.
   let J1:! (Z where .Z1 = ()) where .Z2 = C(.Self);
 }
 
+fn F(T:! J) {}
+
+class D;
+// Satisfies the implied constraint in J.J1.
+// CHECK:STDERR: fail_todo_nested_constraint_visible_in_type_parameter.carbon:[[@LINE+7]]:38: error: cannot convert type `.Self` that implements `Z` into type implementing `Z where .(Z.Z1) = ()` [ConversionFailureFacetToFacet]
+// CHECK:STDERR: impl D as Z where .Z1 = () and .Z2 = C(.Self) {}
+// CHECK:STDERR:                                      ^~~~~~~~
+// CHECK:STDERR: fail_todo_nested_constraint_visible_in_type_parameter.carbon:[[@LINE-14]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+// CHECK:STDERR: class C(T:! Z where .Z1 = ()) {}
+// CHECK:STDERR:         ^
+// CHECK:STDERR:
+impl D as Z where .Z1 = () and .Z2 = C(.Self) {}
+// CHECK:STDERR: fail_todo_nested_constraint_visible_in_type_parameter.carbon:[[@LINE+4]]:24: error: cannot convert type `D` into type implementing `Z where .(Z.Z1) = () and .(Z.Z2) = C(.Self)` [ConversionFailureTypeToFacet]
+// CHECK:STDERR: fn G(T:! J where .J1 = D) {
+// CHECK:STDERR:                        ^
+// CHECK:STDERR:
+fn G(T:! J where .J1 = D) {
+  F(T);
+}
+
+// --- fail_todo_outer_nested_constraint_visible_in_type_parameter.carbon
+library "[[@TEST_NAME]]";
+
+interface Z {
+  let Z1:! type;
+  let Z2:! type;
+}
+
+class C(T:! Z where .Z1 = ()) {}
+
+interface J {
+  // Implied: .Z1 == (), but this is also explicitly required for J1.
+  // CHECK:STDERR: fail_todo_outer_nested_constraint_visible_in_type_parameter.carbon:[[@LINE+7]]:27: error: cannot convert type `.Self` that implements `Z` into type implementing `Z where .(Z.Z1) = ()` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   let J1:! (Z where .Z2 = C(.Self)) where .Z1 = ();
+  // CHECK:STDERR:                           ^~~~~~~~
+  // CHECK:STDERR: fail_todo_outer_nested_constraint_visible_in_type_parameter.carbon:[[@LINE-7]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: class C(T:! Z where .Z1 = ()) {}
+  // CHECK:STDERR:         ^
+  // CHECK:STDERR:
+  let J1:! (Z where .Z2 = C(.Self)) where .Z1 = ();
+}
+
+fn F(T:! J) {}
+
+class D;
+// Satisfies the implied constraint in J.J1.
+// CHECK:STDERR: fail_todo_outer_nested_constraint_visible_in_type_parameter.carbon:[[@LINE+7]]:38: error: cannot convert type `.Self` that implements `Z` into type implementing `Z where .(Z.Z1) = ()` [ConversionFailureFacetToFacet]
+// CHECK:STDERR: impl D as Z where .Z1 = () and .Z2 = C(.Self) {}
+// CHECK:STDERR:                                      ^~~~~~~~
+// CHECK:STDERR: fail_todo_outer_nested_constraint_visible_in_type_parameter.carbon:[[@LINE-21]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+// CHECK:STDERR: class C(T:! Z where .Z1 = ()) {}
+// CHECK:STDERR:         ^
+// CHECK:STDERR:
+impl D as Z where .Z1 = () and .Z2 = C(.Self) {}
+fn G(T:! J where .J1 = D) {
+  F(T);
+}
+
 // --- fail_todo_earlier_constraint_visible_in_type_parameter.carbon
 library "[[@TEST_NAME]]";
 
@@ -39,20 +172,34 @@ interface Z {
 
 class C(T:! Z where .Z1 = ()) {}
 
-// TODO: Should this pass? Or do we need a `where` between .Z1 and .Z2 to make
-// .Z1's value visible to .Z2?
-// See https://github.com/carbon-language/carbon-lang/issues/5884.
 interface J {
+  // Implied: .Z1 == (), but this is also explicitly required for J1.
   // CHECK:STDERR: fail_todo_earlier_constraint_visible_in_type_parameter.carbon:[[@LINE+7]]:39: error: cannot convert type `.Self` that implements `Z` into type implementing `Z where .(Z.Z1) = ()` [ConversionFailureFacetToFacet]
   // CHECK:STDERR:   let J1:! Z where .Z1 = () and .Z2 = C(.Self);
   // CHECK:STDERR:                                       ^~~~~~~~
-  // CHECK:STDERR: fail_todo_earlier_constraint_visible_in_type_parameter.carbon:[[@LINE-9]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fail_todo_earlier_constraint_visible_in_type_parameter.carbon:[[@LINE-7]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
   // CHECK:STDERR: class C(T:! Z where .Z1 = ()) {}
   // CHECK:STDERR:         ^
   // CHECK:STDERR:
   let J1:! Z where .Z1 = () and .Z2 = C(.Self);
 }
 
+fn F(T:! J) {}
+
+class D;
+// Satisfies the implied constraint in J.J1.
+// CHECK:STDERR: fail_todo_earlier_constraint_visible_in_type_parameter.carbon:[[@LINE+7]]:38: error: cannot convert type `.Self` that implements `Z` into type implementing `Z where .(Z.Z1) = ()` [ConversionFailureFacetToFacet]
+// CHECK:STDERR: impl D as Z where .Z1 = () and .Z2 = C(.Self) {}
+// CHECK:STDERR:                                      ^~~~~~~~
+// CHECK:STDERR: fail_todo_earlier_constraint_visible_in_type_parameter.carbon:[[@LINE-21]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+// CHECK:STDERR: class C(T:! Z where .Z1 = ()) {}
+// CHECK:STDERR:         ^
+// CHECK:STDERR:
+impl D as Z where .Z1 = () and .Z2 = C(.Self) {}
+fn G(T:! J where .J1 = D) {
+  F(T);
+}
+
 // --- fail_todo_later_constraint_visible_in_type_parameter.carbon
 library "[[@TEST_NAME]]";
 
@@ -63,20 +210,105 @@ interface Z {
 
 class C(T:! Z where .Z1 = ()) {}
 
-// TODO: Should this pass? Or do we need a `where` between .Z1 and .Z2 to make
-// .Z1's value visible to .Z2?
-// See https://github.com/carbon-language/carbon-lang/issues/5884.
 interface J {
+  // Implied: .Z1 == (), but this is also explicitly required for J1.
   // CHECK:STDERR: fail_todo_later_constraint_visible_in_type_parameter.carbon:[[@LINE+7]]:26: error: cannot convert type `.Self` that implements `Z` into type implementing `Z where .(Z.Z1) = ()` [ConversionFailureFacetToFacet]
   // CHECK:STDERR:   let J1:! Z where .Z2 = C(.Self) and .Z1 = ();
   // CHECK:STDERR:                          ^~~~~~~~
-  // CHECK:STDERR: fail_todo_later_constraint_visible_in_type_parameter.carbon:[[@LINE-9]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fail_todo_later_constraint_visible_in_type_parameter.carbon:[[@LINE-7]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
   // CHECK:STDERR: class C(T:! Z where .Z1 = ()) {}
   // CHECK:STDERR:         ^
   // CHECK:STDERR:
   let J1:! Z where .Z2 = C(.Self) and .Z1 = ();
 }
 
+fn F(T:! J) {}
+
+class D;
+// Satisfies the implied constraint in J.J1.
+// CHECK:STDERR: fail_todo_later_constraint_visible_in_type_parameter.carbon:[[@LINE+7]]:38: error: cannot convert type `.Self` that implements `Z` into type implementing `Z where .(Z.Z1) = ()` [ConversionFailureFacetToFacet]
+// CHECK:STDERR: impl D as Z where .Z1 = () and .Z2 = C(.Self) {}
+// CHECK:STDERR:                                      ^~~~~~~~
+// CHECK:STDERR: fail_todo_later_constraint_visible_in_type_parameter.carbon:[[@LINE-21]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+// CHECK:STDERR: class C(T:! Z where .Z1 = ()) {}
+// CHECK:STDERR:         ^
+// CHECK:STDERR:
+impl D as Z where .Z1 = () and .Z2 = C(.Self) {}
+fn G(T:! J where .J1 = D) {
+  F(T);
+}
+
+// --- fail_todo_early_rewrite_applied.carbon
+library "[[@TEST_NAME]]";
+
+interface Z {
+  let Z1:! type;
+  let Z2:! type;
+}
+
+interface Tuple {}
+impl () as Tuple {}
+class C(T:! Tuple) {}
+
+interface J {
+  // Implied: .Z1 == (), but this is also explicitly required for J1.
+  // CHECK:STDERR: fail_todo_early_rewrite_applied.carbon:[[@LINE+7]]:39: error: cannot convert type `.(Z.Z1)` into type implementing `Tuple` [ConversionFailureTypeToFacet]
+  // CHECK:STDERR:   let J1:! Z where .Z1 = () and .Z2 = C(.Z1);
+  // CHECK:STDERR:                                       ^~~~~~
+  // CHECK:STDERR: fail_todo_early_rewrite_applied.carbon:[[@LINE-7]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: class C(T:! Tuple) {}
+  // CHECK:STDERR:         ^
+  // CHECK:STDERR:
+  let J1:! Z where .Z1 = () and .Z2 = C(.Z1);
+}
+
+fn F(T:! J) {}
+
+class D;
+// Satisfies the implied constraint in J.J1.
+impl D as Z where .Z1 = () and .Z2 = C(()) {}
+fn G(T:! J where .J1 = D) {
+  F(T);
+}
+
+// --- fail_todo_early_rewrite_applied_extra_indirection.carbon
+library "[[@TEST_NAME]]";
+
+interface Z {
+  let Z1:! type;
+  let Z2:! type;
+}
+
+interface Y {
+  let Y1:! Z;
+}
+
+interface Tuple {}
+impl () as Tuple {}
+class C(T:! Tuple) {}
+
+interface J {
+  // Implied: .Z1 == (), but this is also explicitly required for J1.
+  // CHECK:STDERR: fail_todo_early_rewrite_applied_extra_indirection.carbon:[[@LINE+7]]:59: error: cannot convert type `.(Y.Y1).(Z.Z1)` into type implementing `Tuple` [ConversionFailureTypeToFacet]
+  // CHECK:STDERR:   let J1:! Y & Z where .Y1 = .Self and .Z1 = () and .Z2 = C(.Y1.Z1);
+  // CHECK:STDERR:                                                           ^~~~~~~~~
+  // CHECK:STDERR: fail_todo_early_rewrite_applied_extra_indirection.carbon:[[@LINE-7]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: class C(T:! Tuple) {}
+  // CHECK:STDERR:         ^
+  // CHECK:STDERR:
+  let J1:! Y & Z where .Y1 = .Self and .Z1 = () and .Z2 = C(.Y1.Z1);
+}
+
+fn F(T:! J) {}
+
+class D;
+// Satisfies the implied constraint in J.J1.
+impl D as Z where .Z1 = () and .Z2 = C(()) {}
+impl D as Y where .Y1 = D {}
+fn G(T:! J where .J1 = D) {
+  F(T);
+}
+
 // --- fail_todo_resolved_constraint_visible_in_type_parameter.carbon
 library "[[@TEST_NAME]]";
 
@@ -94,16 +326,28 @@ interface Tuple {}
 impl () as Tuple {}
 class C(T:! Tuple) {}
 
-// TODO: Should this pass? Or do we need a `where` between .Z2 and .Z3 to make
-// .Z2's value visible to .Z3?
-// See https://github.com/carbon-language/carbon-lang/issues/5884.
 interface J {
-  // CHECK:STDERR: fail_todo_resolved_constraint_visible_in_type_parameter.carbon:[[@LINE+7]]:80: error: cannot convert type `.(Z.Z2)` into type implementing `Tuple` [ConversionFailureTypeToFacet]
-  // CHECK:STDERR:   let J1:! (Z & Y where .Y1 = ()) where .Z1 = .Self and .Z2 = .Z1.Y1 and .Z3 = C(.Z2);
-  // CHECK:STDERR:                                                                                ^~~~~~
-  // CHECK:STDERR: fail_todo_resolved_constraint_visible_in_type_parameter.carbon:[[@LINE-9]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // Implied: .Y1 impls Tuple, but this is also explicitly required for J1.
+  // CHECK:STDERR: fail_todo_resolved_constraint_visible_in_type_parameter.carbon:[[@LINE+7]]:76: error: cannot convert type `.(Z.Z2)` into type implementing `Tuple` [ConversionFailureTypeToFacet]
+  // CHECK:STDERR:   let J1:! Z & Y where .Y1 = () and .Z1 = .Self and .Z2 = .Z1.Y1 and .Z3 = C(.Z2);
+  // CHECK:STDERR:                                                                            ^~~~~~
+  // CHECK:STDERR: fail_todo_resolved_constraint_visible_in_type_parameter.carbon:[[@LINE-7]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
   // CHECK:STDERR: class C(T:! Tuple) {}
   // CHECK:STDERR:         ^
   // CHECK:STDERR:
-  let J1:! (Z & Y where .Y1 = ()) where .Z1 = .Self and .Z2 = .Z1.Y1 and .Z3 = C(.Z2);
+  let J1:! Z & Y where .Y1 = () and .Z1 = .Self and .Z2 = .Z1.Y1 and .Z3 = C(.Z2);
+}
+
+fn F(T:! J) {}
+
+class D;
+// Satisfies the implied constraint in J.J1.
+impl D as Y where .Y1 = () {}
+// CHECK:STDERR: fail_todo_resolved_constraint_visible_in_type_parameter.carbon:[[@LINE+4]]:25: error: cannot convert type `.Self` that implements `Z` into type implementing `Y` [ConversionFailureFacetToFacet]
+// CHECK:STDERR: impl D as Z where .Z1 = .Self and .Z2 = () and .Z3 = C(()) {}
+// CHECK:STDERR:                         ^~~~~
+// CHECK:STDERR:
+impl D as Z where .Z1 = .Self and .Z2 = () and .Z3 = C(()) {}
+fn G(T:! J where .J1 = D) {
+  F(T);
 }

toolchain/check/testdata/impl/impl_assoc_const.carbon

@@ -344,6 +344,49 @@ interface M { let X:! type; }
 
 impl () as M where .X = (M where .X = (M where .X = {})) {}
 
+// --- fail_todo_period_self_impl_lookup.carbon
+library "[[@TEST_NAME]]";
+
+interface Y {}
+interface Z {
+    let Z1:! Y;
+}
+
+class C;
+impl C as Y {}
+// CHECK:STDERR: fail_todo_period_self_impl_lookup.carbon:[[@LINE+4]]:25: error: cannot convert type `.Self` that implements `Z` into type implementing `Y` [ConversionFailureFacetToFacet]
+// CHECK:STDERR: impl C as Z where .Z1 = .Self {}
+// CHECK:STDERR:                         ^~~~~
+// CHECK:STDERR:
+impl C as Z where .Z1 = .Self {}
+
+// --- fail_todo_period_self_compared_with_concrete_self.carbon
+library "[[@TEST_NAME]]";
+
+interface Y {}
+interface Z {
+    let Z1:! Y;
+}
+
+class C;
+impl C as Y {}
+impl C as Z where .Z1 = C {}
+
+// CHECK:STDERR: fail_todo_period_self_compared_with_concrete_self.carbon:[[@LINE+4]]:24: error: cannot convert type `.Self` that implements `Z` into type implementing `Y` [ConversionFailureFacetToFacet]
+// CHECK:STDERR: fn F(T:! Z where .Z1 = .Self) {}
+// CHECK:STDERR:                        ^~~~~
+// CHECK:STDERR:
+fn F(T:! Z where .Z1 = .Self) {}
+fn G() {
+  F(C);
+
+  // CHECK:STDERR: fail_todo_period_self_compared_with_concrete_self.carbon:[[@LINE+4]]:23: error: cannot convert type `.Self` that implements `Z` into type implementing `Y` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   C as (Z where .Z1 = .Self);
+  // CHECK:STDERR:                       ^~~~~
+  // CHECK:STDERR:
+  C as (Z where .Z1 = .Self);
+}
+
 // CHECK:STDOUT: --- fail_many_different.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {