Verify rewrite constraints in impl lookup (#5617)

In order to verify rewrite constraints at the end of
`LookupImplWitness()` we need to replace references to associated
constants in the query facet type with values that come from the query's
self. To do this, we find any `ImplWitnessAccess` that is a reference to
`.Self` and replace its witness with the witness found through the impl
lookup process, if the interfaces match. This allows the
`ImplWitnessAccess` to resolve to a concrete value if that witness was
concrete. Then we just need to compare that for each rewrite constraint
the lhs and rhs are the same constant value. If they differ, the self
provided a different value for one side (either through its own facet
value constraints or through an associated impl), or the self did not
provide a value at all.

For now, only .Self references in the top-level facet type are
rewritten. Nested facet types are not, even if they contain a .Self
reference up to the top level facet value. This will be addressed by
adding numbering to the EntityName of of .Self in a BindSymbolicName.
See the third model in
https://docs.google.com/document/d/1Yt-i5AmF76LSvD4TrWRIAE_92kii6j5yFiW-S7ahzlg/edit?tab=t.0
for the plan. For now, there is a TODO addressing this.

toolchain/check/impl_lookup.cpp

@@ -13,10 +13,12 @@
 #include "toolchain/check/deduce.h"
 #include "toolchain/check/diagnostic_helpers.h"
 #include "toolchain/check/eval.h"
+#include "toolchain/check/facet_type.h"
 #include "toolchain/check/generic.h"
 #include "toolchain/check/impl.h"
 #include "toolchain/check/import_ref.h"
 #include "toolchain/check/inst.h"
+#include "toolchain/check/subst.h"
 #include "toolchain/check/type.h"
 #include "toolchain/check/type_completion.h"
 #include "toolchain/check/type_structure.h"
@@ -349,6 +351,164 @@ static auto LookupImplWitnessInSelfFacetValue(
   return EvalImplLookupResult::MakeNonFinal();
 }
 
+// Substitutes witnesess in place of `LookupImplWitness` queries into `.Self`,
+// when the witness is for the same interface as the one `.Self` is referring
+// to.
+//
+// This allows access to the `FacetType` and its constraints from the witness,
+// and allows `ImplWitnessAccess` instructions to be immediately resolved to a
+// more specific value when possible.
+class SubstWitnessesCallbacks : public SubstInstCallbacks {
+ public:
+  // `context` must not be null.
+  explicit SubstWitnessesCallbacks(
+      Context* context, SemIR::LocId loc_id,
+      llvm::ArrayRef<SemIR::SpecificInterface> interfaces,
+      llvm::ArrayRef<SemIR::InstId> witness_inst_ids)
+      : SubstInstCallbacks(context),
+        loc_id_(loc_id),
+        interfaces_(interfaces),
+        witness_inst_ids_(witness_inst_ids) {}
+
+  auto Subst(SemIR::InstId& inst_id) -> SubstResult override {
+    // `FacetType` can be concrete even when it has rewrite constraints that
+    // have a symbolic dependency on `.Self`. See use of
+    // `GetConstantValueIgnoringPeriodSelf` in eval. So in order to recurse into
+    // `FacetType` we must check for it before the `is_concrete` early return.
+    if (context().insts().Is<SemIR::FacetType>(inst_id)) {
+      ++facet_type_depth_;
+      return SubstOperands;
+    }
+
+    if (context().constant_values().Get(inst_id).is_concrete()) {
+      return FullySubstituted;
+    }
+
+    auto access = context().insts().TryGetAs<SemIR::ImplWitnessAccess>(inst_id);
+    if (!access) {
+      return SubstOperands;
+    }
+
+    auto lookup =
+        context().insts().GetAs<SemIR::LookupImplWitness>(access->witness_id);
+    auto bind_name = context().insts().TryGetAs<SemIR::BindSymbolicName>(
+        lookup.query_self_inst_id);
+    if (!bind_name) {
+      return SubstOperands;
+    }
+
+    const auto& self_entity_name =
+        context().entity_names().Get(bind_name->entity_name_id);
+    if (self_entity_name.name_id != SemIR::NameId::PeriodSelf) {
+      return SubstOperands;
+    }
+
+    // TODO: Once we are numbering `EntityName`, (see the third model in
+    // https://docs.google.com/document/d/1Yt-i5AmF76LSvD4TrWRIAE_92kii6j5yFiW-S7ahzlg/edit?tab=t.0#heading=h.7urbxcq23olv)
+    // then verify that the index here is equal to the `facet_type_depth_`,
+    // which would mean that it is a reference to the top-level `Self`, which is
+    // being replaced with the impl lookup query self facet value (and then we
+    // use the witness derived from it).
+    //
+    // For now, we only substitute if depth == 0, which is incorrect inside
+    // nested facet types, as it can miss references in specifics up to the top
+    // level facet value.
+    if (facet_type_depth_ > 0) {
+      return SubstOperands;
+    }
+
+    auto witness_id =
+        FindWitnessForInterface(lookup.query_specific_interface_id);
+    if (!witness_id.has_value()) {
+      return SubstOperands;
+    }
+
+    inst_id = RebuildNewInst(
+        context().insts().GetLocIdForDesugaring(loc_id_),
+        SemIR::ImplWitnessAccess{.type_id = GetSingletonType(
+                                     context(), SemIR::WitnessType::TypeInstId),
+                                 .witness_id = witness_id,
+                                 .index = access->index});
+    // Once we replace a witness, we either have a concrete value or some
+    // reference to an associated constant that came from the witness's facet
+    // type. We don't want to substitute into the witness's facet type, so we
+    // don't recurse on whatever came from the witness.
+    return FullySubstituted;
+  }
+
+  auto Rebuild(SemIR::InstId orig_inst_id, SemIR::Inst new_inst)
+      -> SemIR::InstId override {
+    if (context().insts().Is<SemIR::FacetType>(orig_inst_id)) {
+      --facet_type_depth_;
+    }
+    return RebuildNewInst(loc_id_, new_inst);
+  }
+
+  auto ReuseUnchanged(SemIR::InstId orig_inst_id) -> SemIR::InstId override {
+    if (context().insts().Is<SemIR::FacetType>(orig_inst_id)) {
+      --facet_type_depth_;
+    }
+    return orig_inst_id;
+  }
+
+ private:
+  auto FindWitnessForInterface(SemIR::SpecificInterfaceId specific_interface_id)
+      -> SemIR::InstId {
+    auto lookup_query_interface =
+        context().specific_interfaces().Get(specific_interface_id);
+    for (auto [interface, witness_inst_id] :
+         llvm::zip(interfaces_, witness_inst_ids_)) {
+      // If the `LookupImplWitness` for `.Self` is not looking for the same
+      // interface as we have a witness for, this is not the right witness to
+      // use to replace the lookup for `.Self`.
+      if (interface.interface_id == lookup_query_interface.interface_id) {
+        return witness_inst_id;
+      }
+    }
+    return SemIR::InstId::None;
+  }
+
+  SemIR::LocId loc_id_;
+  llvm::ArrayRef<SemIR::SpecificInterface> interfaces_;
+  llvm::ArrayRef<SemIR::InstId> witness_inst_ids_;
+  int facet_type_depth_ = 0;
+};
+
+static auto VerifyQueryFacetTypeConstraints(
+    Context& context, SemIR::LocId loc_id,
+    SemIR::InstId query_facet_type_inst_id,
+    llvm::ArrayRef<SemIR::SpecificInterface> interfaces,
+    llvm::ArrayRef<SemIR::InstId> witness_inst_ids) -> bool {
+  CARBON_CHECK(context.insts().Is<SemIR::FacetType>(query_facet_type_inst_id));
+
+  const auto& facet_type_info = context.facet_types().Get(
+      context.insts()
+          .GetAs<SemIR::FacetType>(query_facet_type_inst_id)
+          .facet_type_id);
+
+  if (!facet_type_info.rewrite_constraints.empty()) {
+    auto callbacks =
+        SubstWitnessesCallbacks(&context, loc_id, interfaces, witness_inst_ids);
+
+    for (const auto& rewrite : facet_type_info.rewrite_constraints) {
+      auto lhs_id = SubstInst(context, rewrite.lhs_id, callbacks);
+      auto rhs_id = SubstInst(context, rewrite.rhs_id, callbacks);
+      if (lhs_id != rhs_id) {
+        // TODO: Provide a diagnostic note and location for which rewrite
+        // constraint was not satisfied, if a diagnostic is going to be
+        // displayed for the LookupImplWitessFailure. This will require plumbing
+        // through a callback that lets us add a Note to another diagnostic.
+        return false;
+      }
+    }
+  }
+
+  // TODO: Validate that the witnesses satisfy the other requirements in the
+  // `facet_type_info`.
+
+  return true;
+}
+
 // Begin a search for an impl declaration matching the query. We do this by
 // creating an LookupImplWitness instruction and evaluating. If it's able to
 // find a final concrete impl, then it will evaluate to that `ImplWitness` but
@@ -459,8 +619,14 @@ auto LookupImplWitness(Context& context, SemIR::LocId loc_id,
     return SemIR::InstBlockId::None;
   }
 
-  // TODO: Validate that the witness satisfies the other requirements in
-  // `interface_const_id`.
+  // Verify rewrite constraints in the query constraint are satisfied after
+  // applying the rewrites from the found witnesses.
+  if (!VerifyQueryFacetTypeConstraints(
+          context, loc_id,
+          context.constant_values().GetInstId(query_facet_type_const_id),
+          interfaces, result_witness_ids)) {
+    return SemIR::InstBlockId::None;
+  }
 
   return context.inst_blocks().AddCanonical(result_witness_ids);
 }

toolchain/check/testdata/facet/early_rewrites.carbon

@@ -29,7 +29,7 @@ interface J {
   let J1:! (Z where .Z1 = ()) where .Z2 = C(.Self);
 }
 
-// --- todo_earlier_constraint_visible_in_type_parameter.carbon
+// --- fail_todo_earlier_constraint_visible_in_type_parameter.carbon
 library "[[@TEST_NAME]]";
 
 interface Z {
@@ -43,10 +43,17 @@ class C(T:! Z where .Z1 = ()) {}
 // .Z1's value visible to .Z2?
 // See https://github.com/carbon-language/carbon-lang/issues/5884.
 interface J {
+  // 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: class C(T:! Z where .Z1 = ()) {}
+  // CHECK:STDERR:         ^
+  // CHECK:STDERR:
   let J1:! Z where .Z1 = () and .Z2 = C(.Self);
 }
 
-// --- todo_later_constraint_visible_in_type_parameter.carbon
+// --- fail_todo_later_constraint_visible_in_type_parameter.carbon
 library "[[@TEST_NAME]]";
 
 interface Z {
@@ -60,6 +67,13 @@ class C(T:! Z where .Z1 = ()) {}
 // .Z1's value visible to .Z2?
 // See https://github.com/carbon-language/carbon-lang/issues/5884.
 interface J {
+  // 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: class C(T:! Z where .Z1 = ()) {}
+  // CHECK:STDERR:         ^
+  // CHECK:STDERR:
   let J1:! Z where .Z2 = C(.Self) and .Z1 = ();
 }
 

toolchain/check/testdata/facet/facet_assoc_const.carbon

@@ -136,19 +136,21 @@ fn G(T:! M & L, a: T.W) -> () { return a; }
 fn H(T:! L where .W = {}, a: T.W) -> {} { return a; }
 
 fn F(T:! M & (L where .W = {}), a: T.W) {
-  // TODO: One of `b` or `c` must fail, because `T.W` is either found to be `()` from
+  // One of `b` or `c` must fail, because `T.W` is either found to be `()` from
   // the impl or `{}` from the facet type of T.
 
   let b: () = G(T, a);
-  // CHECK:STDERR: fail_two_different_combined_from_final_impl_and_facet.carbon:[[@LINE+10]]:15: error: cannot implicitly convert expression of type `()` to `{}` [ConversionFailure]
-  // CHECK:STDERR:   let c: {} = H(T, a);
-  // CHECK:STDERR:               ^~~~~~~
-  // CHECK:STDERR: fail_two_different_combined_from_final_impl_and_facet.carbon:[[@LINE+7]]:15: note: type `()` does not implement interface `Core.ImplicitAs({})` [MissingImplInMemberAccessNote]
+  // TODO: This diagnostic sucks. Can we make the facet type's value take
+  // precidence over final, since that's what is written in the code and more
+  // likely to show up in diagnostics? Or should we diagnose `T` as being
+  // invalid directly, where we can see both `.W` values and print them?
+  //
+  // CHECK:STDERR: fail_two_different_combined_from_final_impl_and_facet.carbon:[[@LINE+7]]:15: error: cannot convert type `T` that implements `L & M where .(L.W) = {}` into type implementing `L where .(L.W) = {}` [ConversionFailureFacetToFacet]
   // CHECK:STDERR:   let c: {} = H(T, a);
   // CHECK:STDERR:               ^~~~~~~
-  // CHECK:STDERR: fail_two_different_combined_from_final_impl_and_facet.carbon:[[@LINE-13]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
+  // CHECK:STDERR: fail_two_different_combined_from_final_impl_and_facet.carbon:[[@LINE-15]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
   // CHECK:STDERR: fn H(T:! L where .W = {}, a: T.W) -> {} { return a; }
-  // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR:      ^
   // CHECK:STDERR:
   let c: {} = H(T, a);
 }

toolchain/check/testdata/facet/named_constant.carbon

@@ -0,0 +1,195 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// INCLUDE-FILE: toolchain/testing/testdata/min_prelude/facet_types.carbon
+//
+// AUTOUPDATE
+// TIP: To test this file alone, run:
+// TIP:   bazel test //toolchain/testing:file_test --test_arg=--file_tests=toolchain/check/testdata/facet/named_constant.carbon
+// TIP: To dump output, run:
+// TIP:   bazel run //toolchain/testing:file_test -- --dump_output --file_tests=toolchain/check/testdata/facet/named_constant.carbon
+
+// --- fail_todo_named_constant_in_rewrite.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X:! type;
+  let Y:! type;
+}
+
+fn Test() {
+  let Constant:! type = ();
+
+  fn F(T:! I where .X = Constant) {}
+
+  fn G(T:! I where .X = Constant) {
+    // TODO: The facet type T in G should match the facet type T in F.
+    // CHECK:STDERR: fail_todo_named_constant_in_rewrite.carbon:[[@LINE+7]]:5: error: cannot deduce value for generic parameter `Constant` [DeductionIncomplete]
+    // CHECK:STDERR:     F(T);
+    // CHECK:STDERR:     ^~~~
+    // CHECK:STDERR: fail_todo_named_constant_in_rewrite.carbon:[[@LINE-7]]:3: note: while deducing parameters of generic declared here [DeductionGenericHere]
+    // CHECK:STDERR:   fn F(T:! I where .X = Constant) {}
+    // CHECK:STDERR:   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+    // CHECK:STDERR:
+    F(T);
+  }
+}
+
+// --- fail_todo_named_constant_two_levels_in_rewrite.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X:! type;
+  let Y:! type;
+}
+
+fn Test() {
+  let Constant2:! type = ();
+  let Constant:! type = (Constant2, );
+
+  fn F(T:! I where .X = Constant) {}
+
+  fn G(T:! I where .X = Constant) {
+    // TODO: The facet type T in G should match the facet type T in F.
+    // CHECK:STDERR: fail_todo_named_constant_two_levels_in_rewrite.carbon:[[@LINE+7]]:5: error: cannot deduce value for generic parameter `Constant2` [DeductionIncomplete]
+    // CHECK:STDERR:     F(T);
+    // CHECK:STDERR:     ^~~~
+    // CHECK:STDERR: fail_todo_named_constant_two_levels_in_rewrite.carbon:[[@LINE-7]]:3: note: while deducing parameters of generic declared here [DeductionGenericHere]
+    // CHECK:STDERR:   fn F(T:! I where .X = Constant) {}
+    // CHECK:STDERR:   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+    // CHECK:STDERR:
+    F(T);
+  }
+}
+
+// --- fail_todo_named_constant_in_rewrite_callee.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X:! type;
+  let Y:! type;
+}
+
+fn Test() {
+  let Constant:! type = ();
+
+  fn F(T:! I where .X = Constant) {}
+
+  fn G(T:! I where .X = ()) {
+    // TODO: The facet type T in G should match the facet type T in F.
+    // CHECK:STDERR: fail_todo_named_constant_in_rewrite_callee.carbon:[[@LINE+7]]:5: error: cannot deduce value for generic parameter `Constant` [DeductionIncomplete]
+    // CHECK:STDERR:     F(T);
+    // CHECK:STDERR:     ^~~~
+    // CHECK:STDERR: fail_todo_named_constant_in_rewrite_callee.carbon:[[@LINE-7]]:3: note: while deducing parameters of generic declared here [DeductionGenericHere]
+    // CHECK:STDERR:   fn F(T:! I where .X = Constant) {}
+    // CHECK:STDERR:   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+    // CHECK:STDERR:
+    F(T);
+  }
+}
+
+// --- fail_todo_named_constant_in_rewrite_caller.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X:! type;
+  let Y:! type;
+}
+
+fn Test() {
+  let Constant:! type = ();
+
+  fn F(T:! I where .X = ()) {}
+
+  fn G(T:! I where .X = Constant) {
+    // TODO: The facet type T in G should match the facet type T in F.
+    // CHECK:STDERR: fail_todo_named_constant_in_rewrite_caller.carbon:[[@LINE+7]]:5: error: cannot convert type `T` that implements `I where .(I.X) = Constant` into type implementing `I where .(I.X) = ()` [ConversionFailureFacetToFacet]
+    // CHECK:STDERR:     F(T);
+    // CHECK:STDERR:     ^~~~
+    // CHECK:STDERR: fail_todo_named_constant_in_rewrite_caller.carbon:[[@LINE-7]]:8: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+    // CHECK:STDERR:   fn F(T:! I where .X = ()) {}
+    // CHECK:STDERR:        ^
+    // CHECK:STDERR:
+    F(T);
+  }
+}
+
+// --- fail_todo_named_constant_in_nested_facet_type.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X:! type;
+  let Y:! type;
+}
+
+fn Test() {
+  let Constant:! type = ();
+
+  // TODO: The .Self reference in each .X should be different, there should be
+  // no cycle here.
+  // CHECK:STDERR: fail_todo_named_constant_in_nested_facet_type.carbon:[[@LINE+4]]:12: error: found cycle in facet type constraint for `.(I.X)` [FacetTypeConstraintCycle]
+  // CHECK:STDERR:   fn F(T:! I where .X = (I where .X = Constant)) {}
+  // CHECK:STDERR:            ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR:
+  fn F(T:! I where .X = (I where .X = Constant)) {}
+
+  // CHECK:STDERR: fail_todo_named_constant_in_nested_facet_type.carbon:[[@LINE+4]]:12: error: found cycle in facet type constraint for `.(I.X)` [FacetTypeConstraintCycle]
+  // CHECK:STDERR:   fn G(T:! I where .X = (I where .X = Constant)) {
+  // CHECK:STDERR:            ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR:
+  fn G(T:! I where .X = (I where .X = Constant)) {
+    // TODO: The facet type T in G should match the facet type T in F.
+    F(T);
+  }
+}
+
+// --- fail_todo_named_constant_in_nested_facet_type_caller.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X:! type;
+  let Y:! type;
+}
+
+fn Test() {
+  let Constant:! type = ();
+
+  fn F(T:! I where .X = (I where .X = ())) {}
+
+  // TODO: The .Self reference in each .X should be different, there should be
+  // no cycle here.
+  // CHECK:STDERR: fail_todo_named_constant_in_nested_facet_type_caller.carbon:[[@LINE+4]]:12: error: found cycle in facet type constraint for `.(I.X)` [FacetTypeConstraintCycle]
+  // CHECK:STDERR:   fn G(T:! I where .X = (I where .X = Constant)) {
+  // CHECK:STDERR:            ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR:
+  fn G(T:! I where .X = (I where .X = Constant)) {
+    // TODO: The facet type T in G should match the facet type T in F.
+    F(T);
+  }
+}
+
+// --- fail_named_constant_in_nested_facet_type_callee.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X:! type;
+  let Y:! type;
+}
+
+fn Test() {
+  let Constant:! type = ();
+
+  // TODO: The .Self reference in each .X should be different, there should be
+  // no cycle here.
+  // CHECK:STDERR: fail_named_constant_in_nested_facet_type_callee.carbon:[[@LINE+4]]:12: error: found cycle in facet type constraint for `.(I.X)` [FacetTypeConstraintCycle]
+  // CHECK:STDERR:   fn F(T:! I where .X = (I where .X = Constant)) {}
+  // CHECK:STDERR:            ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR:
+  fn F(T:! I where .X = (I where .X = Constant)) {}
+
+  fn G(T:! I where .X = (I where .X = ())) {
+    // TODO: The facet type T in G should match the facet type T in F.
+    F(T);
+  }
+}

toolchain/check/testdata/facet/validate_impl_constraints.carbon

@@ -10,26 +10,82 @@
 // TIP: To dump output, run:
 // TIP:   bazel run //toolchain/testing:file_test -- --dump_output --file_tests=toolchain/check/testdata/facet/validate_impl_constraints.carbon
 
+// --- self_impls_modifies_assoc_constant.carbon
+library "[[@TEST_NAME]]";
+
+interface I { let X:! type; }
+
+fn F(T:! I where .X = ()) {}
+
+fn G(T:! I where .Self impls (I where .X = ())) {
+  F(T);
+}
+
+// --- fail_self_impls_modifies_assoc_constant_type_differs.carbon
+library "[[@TEST_NAME]]";
+
+interface I { let X:! type; }
+
+fn F(T:! I where .X = ()) {}
+
+fn G(T:! I where .Self impls (I where .X = {})) {
+  // CHECK:STDERR: fail_self_impls_modifies_assoc_constant_type_differs.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `I where .(I.X) = {}` into type implementing `I where .(I.X) = ()` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(T);
+  // CHECK:STDERR:   ^~~~
+  // CHECK:STDERR: fail_self_impls_modifies_assoc_constant_type_differs.carbon:[[@LINE-6]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(T:! I where .X = ()) {}
+  // CHECK:STDERR:      ^
+  // CHECK:STDERR:
+  F(T);
+}
+
 // --- fail_todo_where_impls_tests_associated_constant_of_generic_type.carbon
+library "[[@TEST_NAME]]";
 
 class C(U:! type) {}
 
 // C(U) impls M if U impls L.
 interface L {}
-interface M {}
-impl forall [U:! L] C(U) as M {}
+interface M { let M0:! type; }
+impl forall [U:! L] C(U) as M where .M0 = {} {}
 
 // U requires that C(.Self) impls M.
 // - C(.Self) impls M can be rewritten as C(U) impls M.
 // - C(U) impls M if U impls L => Requires U impls L.
-fn F(U:! type where C(.Self) impls M) {}
+fn F(U:! type where C(.Self) impls (M where .M0 = {})) {}
 
 fn G(T:! L) {
   // CHECK:STDERR: fail_todo_where_impls_tests_associated_constant_of_generic_type.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `L` into type implementing `type where...` [ConversionFailureFacetToFacet]
   // CHECK:STDERR:   F(T);
   // CHECK:STDERR:   ^~~~
   // CHECK:STDERR: fail_todo_where_impls_tests_associated_constant_of_generic_type.carbon:[[@LINE-6]]:6: note: initializing generic parameter `U` declared here [InitializingGenericParam]
-  // CHECK:STDERR: fn F(U:! type where C(.Self) impls M) {}
+  // CHECK:STDERR: fn F(U:! type where C(.Self) impls (M where .M0 = {})) {}
+  // CHECK:STDERR:      ^
+  // CHECK:STDERR:
+  F(T);
+}
+
+// --- fail_where_impls_tests_associated_constant_of_generic_type_type_differs.carbon
+library "[[@TEST_NAME]]";
+
+class C(U:! type) {}
+
+// C(U) impls M if U impls L.
+interface L {}
+interface M { let M0:! type; }
+impl forall [U:! L] C(U) as M where .M0 = () {}
+
+// U requires that C(.Self) impls M.
+// - C(.Self) impls M can be rewritten as C(U) impls M.
+// - C(U) impls M if U impls L => Requires U impls L.
+fn F(U:! type where C(.Self) impls (M where .M0 = {})) {}
+
+fn G(T:! L) {
+  // CHECK:STDERR: fail_where_impls_tests_associated_constant_of_generic_type_type_differs.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `L` into type implementing `type where...` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(T);
+  // CHECK:STDERR:   ^~~~
+  // CHECK:STDERR: fail_where_impls_tests_associated_constant_of_generic_type_type_differs.carbon:[[@LINE-6]]:6: note: initializing generic parameter `U` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(U:! type where C(.Self) impls (M where .M0 = {})) {}
   // CHECK:STDERR:      ^
   // CHECK:STDERR:
   F(T);

toolchain/check/testdata/facet/validate_rewrite_constraints.carbon

@@ -0,0 +1,1361 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// INCLUDE-FILE: toolchain/testing/testdata/min_prelude/facet_types.carbon
+//
+// AUTOUPDATE
+// TIP: To test this file alone, run:
+// TIP:   bazel test //toolchain/testing:file_test --test_arg=--file_tests=toolchain/check/testdata/facet/validate_rewrite_constraints.carbon
+// TIP: To dump output, run:
+// TIP:   bazel run //toolchain/testing:file_test -- --dump_output --file_tests=toolchain/check/testdata/facet/validate_rewrite_constraints.carbon
+
+// --- facet_value.carbon
+library "[[@TEST_NAME]]";
+
+interface I { let X:! type; }
+
+fn F(T:! I where .X = ()) {}
+
+fn G(T:! I where .X = ()) {
+  F(T);
+}
+
+// --- generic_interface_facet_value.carbon
+library "[[@TEST_NAME]]";
+
+interface I(T:! type) { let X:! type; }
+
+class C;
+final impl forall [T:! type] T as I(()) where .X = () {}
+final impl forall [T:! type] T as I({}) where .X = {} {}
+
+fn F(U:! type, T:! I(U) where .X = ()) {}
+fn G() {
+  F((), C);
+}
+
+// --- fail_generic_interface_facet_value_wrong_specific_impl.carbon
+library "[[@TEST_NAME]]";
+
+interface I(T:! type) { let X:! type; }
+
+class C;
+final impl forall [T:! type] T as I(()) where .X = () {}
+final impl forall [T:! type] T as I({}) where .X = {} {}
+
+fn F(U:! type, T:! I(U) where .X = ()) {}
+fn G() {
+  // This finds the impl where `.X = {}`, but F requires that `.X = ()`.
+  //
+  // CHECK:STDERR: fail_generic_interface_facet_value_wrong_specific_impl.carbon:[[@LINE+7]]:3: error: cannot convert type `C` into type implementing `I({}) where .(I({}).X) = ()` [ConversionFailureTypeToFacet]
+  // CHECK:STDERR:   F({}, C);
+  // CHECK:STDERR:   ^~~~~~~~
+  // CHECK:STDERR: fail_generic_interface_facet_value_wrong_specific_impl.carbon:[[@LINE-7]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
+  // CHECK:STDERR: fn F(U:! type, T:! I(U) where .X = ()) {}
+  // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR:
+  F({}, C);
+}
+
+// --- dependent_rules.carbon
+library "[[@TEST_NAME]]";
+
+interface I { let X:! type; }
+interface J { let Y:! type; }
+
+fn F(T:! I & J where .X = .Y) {
+  // Allowed since `T impls I`, `T impls J`, and has constraint providing
+  // T.(I.X) = T.(J.Y)`.
+  F(T);
+}
+
+// --- fail_convert.carbon
+library "[[@TEST_NAME]]";
+
+interface I { let X:! type; }
+
+fn F(T:! I where .X = {.a: (), .b: {}}) {}
+
+fn H() {
+  class C;
+  impl C as I where .X = {.b: {}, .a: ()} {}
+  // CHECK:STDERR: fail_convert.carbon:[[@LINE+7]]:3: error: cannot convert type `C` into type implementing `I where .(I.X) = {.a: (), .b: {}}` [ConversionFailureTypeToFacet]
+  // CHECK:STDERR:   F(C);
+  // CHECK:STDERR:   ^~~~
+  // CHECK:STDERR: fail_convert.carbon:[[@LINE-8]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(T:! I where .X = {.a: (), .b: {}}) {}
+  // CHECK:STDERR:      ^
+  // CHECK:STDERR:
+  F(C);
+}
+
+fn G(T:! I where .X = {.b: {}, .a: ()}) {
+  // CHECK:STDERR: fail_convert.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `I where .(I.X) = {.b: {}, .a: ()}` into type implementing `I where .(I.X) = {.a: (), .b: {}}` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(T);
+  // CHECK:STDERR:   ^~~~
+  // CHECK:STDERR: fail_convert.carbon:[[@LINE-19]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(T:! I where .X = {.a: (), .b: {}}) {}
+  // CHECK:STDERR:      ^
+  // CHECK:STDERR:
+  F(T);
+}
+
+// --- fail_todo_dependent_rules_compound.carbon
+library "[[@TEST_NAME]]";
+
+interface I { let X:! type; }
+interface J { let Y:! type; }
+
+// CHECK:STDERR: fail_todo_dependent_rules_compound.carbon:[[@LINE+8]]:23: error: expected identifier or `Self` after `.` [ExpectedIdentifierOrSelfAfterPeriod]
+// CHECK:STDERR: fn F(T:! I & J where .(I.X) = .(J.Y)) {
+// CHECK:STDERR:                       ^
+// CHECK:STDERR:
+// CHECK:STDERR: fail_todo_dependent_rules_compound.carbon:[[@LINE+4]]:23: error: semantics TODO: `handle invalid parse trees in `check`` [SemanticsTodo]
+// CHECK:STDERR: fn F(T:! I & J where .(I.X) = .(J.Y)) {
+// CHECK:STDERR:                       ^
+// CHECK:STDERR:
+fn F(T:! I & J where .(I.X) = .(J.Y)) {
+  // Allowed since `T impls I`, `T impls J`, and has constraint providing
+  // T.(I.X) = T.(J.Y)`.
+  F(T);
+}
+
+// --- parameterized_interface.carbon
+library "[[@TEST_NAME]]";
+
+interface I(T:! type) { let X:! type; }
+
+final impl forall [J:! I(()) where .X = ()] J as I({}) where .X = {} {}
+
+fn F(T:! I({}) where .X = {}) {}
+
+fn G(T:! I(()) where .X = ()) {
+  F(T);
+}
+
+// --- fail_todo_parameterized_interface_compound.carbon
+library "[[@TEST_NAME]]";
+
+interface I(T:! type) { let X:! type; }
+
+final impl forall [J:! I(())] J as I({}) where .X = {} {}
+
+// CHECK:STDERR: fail_todo_parameterized_interface_compound.carbon:[[@LINE+8]]:31: error: expected identifier or `Self` after `.` [ExpectedIdentifierOrSelfAfterPeriod]
+// CHECK:STDERR: fn F(T:! I(()) & I({}) where .(I(()).X) = () and .(I({}).X) = {}) {}
+// CHECK:STDERR:                               ^
+// CHECK:STDERR:
+// CHECK:STDERR: fail_todo_parameterized_interface_compound.carbon:[[@LINE+4]]:31: error: semantics TODO: `handle invalid parse trees in `check`` [SemanticsTodo]
+// CHECK:STDERR: fn F(T:! I(()) & I({}) where .(I(()).X) = () and .(I({}).X) = {}) {}
+// CHECK:STDERR:                               ^
+// CHECK:STDERR:
+fn F(T:! I(()) & I({}) where .(I(()).X) = () and .(I({}).X) = {}) {}
+
+fn G(T:! I(()) where .X = ()) {
+  F(T);
+}
+
+// --- fail_parameterized_interface_with_wrong_where_in_impl_deduction.carbon
+library "[[@TEST_NAME]]";
+
+interface I(T:! type) { let X:! type; }
+
+final impl forall [J:! I(()) where .X = {}] J as I({}) where .X = {} {}
+
+fn F(T:! I({}) where .X = {}) {}
+
+fn G(T:! I(()) where .X = ()) {
+  // CHECK:STDERR: fail_parameterized_interface_with_wrong_where_in_impl_deduction.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `I(()) where .(I(()).X) = ()` into type implementing `I({}) where .(I({}).X) = {}` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(T);
+  // CHECK:STDERR:   ^~~~
+  // CHECK:STDERR: fail_parameterized_interface_with_wrong_where_in_impl_deduction.carbon:[[@LINE-6]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(T:! I({}) where .X = {}) {}
+  // CHECK:STDERR:      ^
+  // CHECK:STDERR:
+  F(T);
+}
+
+// --- source_rhs_is_assoc_constant.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X1:! type;
+  let X2:! type;
+}
+
+fn F(T:! I where .X1 = () and .X2 = ()) {}
+
+fn G() {
+  class C;
+  impl C as I where .X1 = .X2 and .X2 = () {}
+  F(C);
+}
+
+fn H(T:! I where .X1 = .X2 and .X2 = ()) {
+  F(T);
+}
+
+// --- target_rhs_is_assoc_constant.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X1:! type;
+  let X2:! type;
+}
+
+fn F(T:! I where .X1 = .X2 and .X2 = ()) {}
+
+fn G() {
+  class C;
+  impl C as I where .X1 = () and .X2 = () {}
+  F(C);
+}
+
+fn H(T:! I where .X1 = () and .X2 = ()) {
+  F(T);
+}
+
+// --- both_rhs_is_assoc_constant.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X1:! type;
+  let X2:! type;
+}
+
+fn F(T:! I where .X1 = .X2 and .X2 = ()) {}
+
+fn G() {
+  class C1;
+  impl C1 as I where .X1 = .X2 and .X2 = () {}
+  F(C1);
+
+  class C2;
+  impl C2 as I where .X1 = () and .X2 = .X1 {}
+  F(C2);
+}
+
+fn H1(T:! I where .X1 = .X2 and .X2 = ()) {
+  F(T);
+}
+
+fn H2(T:! I where .X1 = () and .X2 = .X1) {
+  F(T);
+}
+
+// --- fail_error_in_witness_table.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X1:! type;
+  let X2:! type;
+}
+
+fn F(T:! I where .X1 = .X2) {}
+
+class C;
+// .X2 is not set in the impl definition, so its value is an ErrorInst
+// in the impl's witness table.
+//
+// CHECK:STDERR: fail_error_in_witness_table.carbon:[[@LINE+7]]:1: error: associated constant X2 not given a value in impl of interface I [ImplAssociatedConstantNeedsValue]
+// CHECK:STDERR: impl C as I where .X1 = () {}
+// CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR: fail_error_in_witness_table.carbon:[[@LINE-12]]:7: note: associated constant declared here [AssociatedConstantHere]
+// CHECK:STDERR:   let X2:! type;
+// CHECK:STDERR:       ^~~~~~~~~
+// CHECK:STDERR:
+impl C as I where .X1 = () {}
+
+fn G() {
+  // CHECK:STDERR: fail_error_in_witness_table.carbon:[[@LINE+7]]:3: error: cannot convert type `C` into type implementing `I where .(I.X1) = .(I.X2)` [ConversionFailureTypeToFacet]
+  // CHECK:STDERR:   F(C);
+  // CHECK:STDERR:   ^~~~
+  // CHECK:STDERR: fail_error_in_witness_table.carbon:[[@LINE-19]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(T:! I where .X1 = .X2) {}
+  // CHECK:STDERR:      ^
+  // CHECK:STDERR:
+  F(C);
+}
+
+// --- impl_provides_rewrite_requirements.carbon
+library "[[@TEST_NAME]]";
+
+interface I {}
+interface J { let Y:! type; }
+
+class C;
+
+final impl forall [T:! I] T as J where .Y = C {}
+
+fn F(T:! I & J where .Y = C) {}
+fn G(T:! I) {
+  F(T);
+}
+
+// --- facet_provides_rewrite_requirements.carbon
+library "[[@TEST_NAME]]";
+
+interface I {}
+interface J { let Y:! type; }
+
+class C;
+
+final impl forall [T:! J] T as I {}
+
+fn F(T:! I & J where .Y = C) {}
+fn G(T:! J where .Y = C) {
+  F(T);
+}
+
+// --- fail_non_final_impl_deduce.carbon
+library "[[@TEST_NAME]]";
+
+interface I { let X:! type; }
+
+impl forall [U:! type] U as I where .X = () {}
+
+fn F(T:! I where .X = ()) {}
+
+class C(T:! type);
+
+fn G(T:! type) {
+  // The type `C(T)` is generic so that the resulting impl witness will not be
+  // effectively final.
+  //
+  // CHECK:STDERR: fail_non_final_impl_deduce.carbon:[[@LINE+7]]:3: error: cannot convert type `C(T)` into type implementing `I where .(I.X) = ()` [ConversionFailureTypeToFacet]
+  // CHECK:STDERR:   F(C(T));
+  // CHECK:STDERR:   ^~~~~~~
+  // CHECK:STDERR: fail_non_final_impl_deduce.carbon:[[@LINE-11]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(T:! I where .X = ()) {}
+  // CHECK:STDERR:      ^
+  // CHECK:STDERR:
+  F(C(T));
+}
+
+// --- fail_non_final_impl_explicit.carbon
+library "[[@TEST_NAME]]";
+
+interface I { let X:! type; }
+
+impl forall [U:! type] U as I where .X = () {}
+
+class C(T:! type);
+
+fn F(T:! type) {
+  // The type `C(T)` is generic so that the resulting impl witness will not be
+  // effectively final.
+  //
+  // CHECK:STDERR: fail_non_final_impl_explicit.carbon:[[@LINE+4]]:3: error: cannot convert type `C(T)` into type implementing `I where .(I.X) = ()` [ConversionFailureTypeToFacet]
+  // CHECK:STDERR:   C(T) as (I where .X = ());
+  // CHECK:STDERR:   ^~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR:
+  C(T) as (I where .X = ());
+}
+
+// --- concrete_query_non_final_impl_deduce.carbon
+library "[[@TEST_NAME]]";
+
+interface I { let X:! type; }
+
+impl forall [U:! type] U as I where .X = () {}
+
+fn F(T:! I where .X = ()) {}
+
+fn G() {
+  class C;
+  F(C);
+}
+
+// --- concrete_query_non_final_impl_explicit_as.carbon
+library "[[@TEST_NAME]]";
+
+interface I { let X:! type; }
+
+impl forall [U:! type] U as I where .X = () {}
+
+fn F() {
+class C;
+  C as (I where .X = ());
+}
+
+// --- final_impl_deduce.carbon
+library "[[@TEST_NAME]]";
+
+interface I { let X:! type; }
+
+final impl forall [U:! type] U as I where .X = () {}
+
+fn F(T:! I where .X = ()) {}
+
+fn G() {
+  class C;
+  F(C);
+}
+
+// --- final_impl_explicit_as.carbon
+library "[[@TEST_NAME]]";
+
+interface I { let X:! type; }
+
+final impl forall [U:! type] U as I where .X = () {}
+
+fn F() {
+  class C;
+  C as (I where .X = ());
+}
+
+// --- concrete_specialization_impl_deduce.carbon
+library "[[@TEST_NAME]]";
+
+interface I { let X:! type; }
+
+class C;
+impl C as I where .X = () {}
+
+fn F(T:! I where .X = ()) {}
+fn G() {
+  F(C);
+}
+
+// --- concrete_specialization_impl_explicit_as.carbon
+library "[[@TEST_NAME]]";
+
+interface I { let X:! type; }
+
+class C;
+impl C as I where .X = () {}
+
+fn F() {
+  C as (I where .X = ());
+}
+
+// --- rewrite_value_in_class_param.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X:! type;
+  let Y:! type;
+}
+
+class C(T:! type);
+
+fn F(T:! I where .X = C(.Y)) {}
+
+fn G(T:! I where .X = C(()) and .Y = ()) {
+  F(T);
+}
+
+// --- fail_wrong_rewrite_value_in_class_param.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X:! type;
+  let Y:! type;
+}
+
+class C(T:! type);
+
+fn F(T:! I where .X = C(.Y)) {}
+
+fn G(T:! I where .X = C(()) and .Y = {}) {
+  // CHECK:STDERR: fail_wrong_rewrite_value_in_class_param.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `I where .(I.X) = C(()) and .(I.Y) = {}` into type implementing `I where .(I.X) = C(.(I.Y))` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(T);
+  // CHECK:STDERR:   ^~~~
+  // CHECK:STDERR: fail_wrong_rewrite_value_in_class_param.carbon:[[@LINE-6]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(T:! I where .X = C(.Y)) {}
+  // CHECK:STDERR:      ^
+  // CHECK:STDERR:
+  F(T);
+}
+
+// --- function_in_interface_ignored.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X:! type;
+  fn F();
+}
+
+fn F(T:! I where .X = ()) {}
+
+fn G(T:! I where .X = ()) {
+  F(T);
+}
+
+// --- function_as_rewrite_value.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X:! type;
+  let Y:! X;
+  fn A();
+}
+
+fn F(T:! I where .Y = .A) {}
+
+fn G(T:! I where .Y = .A) {
+  F(T);
+}
+
+// --- fail_wrong_function_as_rewrite_value.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X:! type;
+  let Y:! X;
+  fn A();
+  fn B();
+}
+
+fn F(T:! I where .Y = .A) {}
+
+fn G(T:! I where .Y = .B) {
+  // CHECK:STDERR: fail_wrong_function_as_rewrite_value.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `I where .(I.Y) = .(I.B)` into type implementing `I where .(I.Y) = .(I.A)` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(T);
+  // CHECK:STDERR:   ^~~~
+  // CHECK:STDERR: fail_wrong_function_as_rewrite_value.carbon:[[@LINE-6]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(T:! I where .Y = .A) {}
+  // CHECK:STDERR:      ^
+  // CHECK:STDERR:
+  F(T);
+}
+
+// --- fail_wrong_function_as_rewrite_value_in_other_interface.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X:! type;
+  let Y:! X;
+  fn A();
+}
+
+interface J {
+  let J1:! type;
+  let J2:! type;
+  // B has the same index in J as A does in I, ensuring the index is not enough
+  // for comparing them.
+  fn B();
+}
+
+fn F(T:! I & J where .Y = .A) {}
+
+fn G(T:! I & J where .Y = .B) {
+  // CHECK:STDERR: fail_wrong_function_as_rewrite_value_in_other_interface.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `I & J where .(I.Y) = .(J.B)` into type implementing `I & J where .(I.Y) = .(I.A)` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(T);
+  // CHECK:STDERR:   ^~~~
+  // CHECK:STDERR: fail_wrong_function_as_rewrite_value_in_other_interface.carbon:[[@LINE-6]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(T:! I & J where .Y = .A) {}
+  // CHECK:STDERR:      ^
+  // CHECK:STDERR:
+  F(T);
+}
+
+// --- recursive_facet.carbon
+library "[[@TEST_NAME]]";
+
+interface I { let X:! type; }
+interface K(Y:! type) {  }
+
+fn F(T:! I where .X = {.k: K(I where .X = ())}) {}
+
+fn G(T:! I where .X = {.k: K(I where .X = ())}) {
+  F(T);
+}
+
+// --- fail_facet_type_concrete_types_match_blanket_impl_concrete_types.carbon
+library "[[@TEST_NAME]]";
+
+interface A { let X:! type; }
+interface B { let Y:! type; }
+
+interface C(BB:! B) { let AX:! type; let BY:! type; }
+
+impl forall [AA:! A, BB:! B] AA as C(BB) where .AX = () and .BY = {} {}
+
+fn F(AA:! A where .X = (), BB:! B where .Y = {}) {
+  // The types match but there may be a specialization that specifies different
+  // types and would be prefered for a specific `AA` or `BB`.
+  //
+  // CHECK:STDERR: fail_facet_type_concrete_types_match_blanket_impl_concrete_types.carbon:[[@LINE+4]]:3: error: cannot convert type `AA` that implements `A where .(A.X) = ()` into type implementing `C(BB as B) where .(C(BB as B).AX) = () and .(C(BB as B).BY) = {}` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   AA as (C(BB) where .AX = () and .BY = {});
+  // CHECK:STDERR:   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR:
+  AA as (C(BB) where .AX = () and .BY = {});
+}
+
+// --- fail_facet_type_concrete_types_become_blank_impl_types.carbon
+library "[[@TEST_NAME]]";
+
+interface A { let X:! type; }
+interface B { let Y:! type; }
+
+interface C(BB:! B) { let AX:! type; let BY:! type; }
+
+impl forall [AA:! A, BB:! B] AA as C(BB) where .AX = AA.X and .BY = BB.Y {}
+
+fn F(AA:! A where .X = (), BB:! B where .Y = {}) {
+  // The types match but there may be a specialization that specifies different
+  // types and would be prefered for a specific `AA` or `BB`.
+  //
+  // CHECK:STDERR: fail_facet_type_concrete_types_become_blank_impl_types.carbon:[[@LINE+4]]:3: error: cannot convert type `AA` that implements `A where .(A.X) = ()` into type implementing `C(BB as B) where .(C(BB as B).AX) = () and .(C(BB as B).BY) = {}` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   AA as (C(BB) where .AX = () and .BY = {});
+  // CHECK:STDERR:   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR:
+  AA as (C(BB) where .AX = () and .BY = {});
+}
+
+// --- facet_type_concrete_types_match_final_blanket_impl_concrete_types.carbon
+library "[[@TEST_NAME]]";
+
+interface A { let X:! type; }
+interface B { let Y:! type; }
+
+interface C(BB:! B) { let AX:! type; let BY:! type; }
+
+final impl forall [AA:! A, BB:! B] AA as C(BB) where .AX = () and .BY = {} {}
+
+fn F(AA:! A where .X = (), BB:! B where .Y = {}) {
+  AA as (C(BB) where .AX = () and .BY = {});
+}
+
+// --- facet_type_concrete_types_become_final_blanket_impl_types.carbon
+library "[[@TEST_NAME]]";
+
+interface A { let X:! type; }
+interface B { let Y:! type; }
+
+interface C(BB:! B) { let AX:! type; let BY:! type; }
+
+final impl forall [AA:! A, BB:! B] AA as C(BB) where .AX = AA.X and .BY = BB.Y {}
+
+fn F(AA:! A where .X = (), BB:! B where .Y = {}) {
+  AA as (C(BB) where .AX = () and .BY = {});
+}
+
+// --- fail_facet_type_concrete_types_become_final_blanket_impl_types_wrong_types.carbon
+library "[[@TEST_NAME]]";
+
+interface A { let X:! type; }
+interface B { let Y:! type; }
+
+interface C(BB:! B) { let AX:! type; let BY:! type; }
+
+final impl forall [AA:! A, BB:! B] AA as C(BB) where .AX = AA.X and .BY = BB.Y {}
+
+fn F(AA:! A where .X = (), BB:! B where .Y = {}) {
+  // CHECK:STDERR: fail_facet_type_concrete_types_become_final_blanket_impl_types_wrong_types.carbon:[[@LINE+4]]:3: error: cannot convert type `AA` that implements `A where .(A.X) = ()` into type implementing `C(BB as B) where .(C(BB as B).AX) = {} and .(C(BB as B).BY) = ()` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   AA as (C(BB) where .AX = {} and .BY = ());
+  // CHECK:STDERR:   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR:
+  AA as (C(BB) where .AX = {} and .BY = ());
+}
+
+// --- chain_in_target.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X1:! type;
+  let X2:! type;
+  let X3:! type;
+}
+
+class C(T:! type);
+
+fn F(T:! I where .X1 = .X3 and .X2 = C(.X3) and .X3 = ()) {}
+
+fn G(T:! I where .X1 = () and .X2 = C(()) and .X3 = ()) {
+  F(T);
+}
+
+// --- chain_in_source.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X1:! type;
+  let X2:! type;
+  let X3:! type;
+}
+
+class C(T:! type);
+
+fn F(T:! I where .X1 = () and .X2 = C(()) and .X3 = .X1) {}
+
+fn G(T:! I where .X1 = .X3 and .X2 = C(.X1) and .X3 = ()) {
+  F(T);
+}
+
+// --- reference_other_facet_value.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X1:! type;
+  let X2:! type;
+}
+
+fn F(U:! I where .X1 = {}, T:! I where .X1 = () and .X2 = U.X1) {}
+
+fn G(U:! I where .X1 = {} and .X2 = (), T:! I where .X1 = U.X2 and .X2 = {}) {
+  F(U, T);
+}
+
+// --- fail_todo_value_through_self_value.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  // TODO: This should not be diagnosed.
+  //
+  // CHECK:STDERR: fail_todo_value_through_self_value.carbon:[[@LINE+7]]:12: error: associated constant has incomplete type `I` [IncompleteTypeInAssociatedConstantDecl]
+  // CHECK:STDERR:   let X1:! I;
+  // CHECK:STDERR:            ^
+  // CHECK:STDERR: fail_todo_value_through_self_value.carbon:[[@LINE-6]]:1: note: interface is currently being defined [InterfaceIncompleteWithinDefinition]
+  // CHECK:STDERR: interface I {
+  // CHECK:STDERR: ^~~~~~~~~~~~~
+  // CHECK:STDERR:
+  let X1:! I;
+  let X2:! type;
+  let X3:! type;
+}
+
+fn F(T:! I where .X1 = .Self and .X2 = .X1.X3 and .X3 = ());
+
+fn G(T:! I where .X1 = .Self and .X2 = () and .X3 = ()) {
+  F(T);
+}
+
+fn H(T:! I where .X1 = .Self and .X2 = .X1.X3 and .X3 = ()) {
+  G(T);
+}
+
+// --- associated_constant_is_facet_type_of_same_interface.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let A:! type;
+  let X:! type;
+}
+
+class C;
+
+// This looks for a bug where `.Self.A` resolves to `C` from `.T.A` in the
+// incoming facet value, which is incorrect. It should be `.T.X.A` which
+// resolves to `{}`.
+fn F(U:! I where .X = (I where .A = {})) {}
+
+fn G(T:! I where .X = (I where .A = {}) and .A = C) {
+  F(T);
+}
+
+// --- rewrite_requires_subst_in_rhs.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X:! type;
+  let Y:! type;
+}
+
+class C(T:! type);
+
+fn F(T:! I where .X = C(.Y)) {}
+
+fn G(T:! I where .X = C({}) and .Y = {}) {
+  F(T);
+}
+
+// --- fail_todo_rewrite_requires_subst_in_nested_facet_type.carbon
+library "[[@TEST_NAME]]";
+
+interface I(T:! type) {
+  let X:! type;
+  let Y:! type;
+}
+
+class C;
+
+fn F(T:! I(C) where .X = (I(.Y) where .Y = ())) {}
+
+fn G(T:! I(C) where .X = (I({}) where .Y = ()) and .Y = {}) {
+  // TODO: The T in G should match the T in F, once the .Self reference to the
+  // top level facet value in `I(.Y)` is correctly substituted by tracking that
+  // it is a .Self reference to the top level Self.
+  // CHECK:STDERR: fail_todo_rewrite_requires_subst_in_nested_facet_type.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `I(C) where .(I(C).X) = I({}) where .(I({}).Y) = () and .(I(C).Y) = {}` into type implementing `I(C) where .(I(C).X) = I(.(I(C).Y)) where .(I(.(I(C).Y)).Y) = ()` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(T);
+  // CHECK:STDERR:   ^~~~
+  // CHECK:STDERR: fail_todo_rewrite_requires_subst_in_nested_facet_type.carbon:[[@LINE-9]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(T:! I(C) where .X = (I(.Y) where .Y = ())) {}
+  // CHECK:STDERR:      ^
+  // CHECK:STDERR:
+  F(T);
+}
+
+fn G2(T:! I(C) where .X = (I(.Y) where .Y = ()) and .Y = {}) {
+  F(T);
+}
+
+// --- fail_rewrite_requires_subst_in_nested_facet_type_types_differ.carbon
+library "[[@TEST_NAME]]";
+
+interface I(T:! type) {
+  let X:! type;
+  let Y:! type;
+}
+
+fn F(T:! I({}) where .X = (I(.Y) where .X = ())) {}
+
+// I(.Y) is I({}) which doesn't match I(()).
+fn G(T:! I({}) where .X = (I(()) where .X = ()) and .Y = {}) {
+  // CHECK:STDERR: fail_rewrite_requires_subst_in_nested_facet_type_types_differ.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `I({}) where .(I({}).X) = I(()) where .(I(()).X) = () and .(I({}).Y) = {}` into type implementing `I({}) where .(I({}).X) = I(.(I({}).Y)) where .(I(.(I({}).Y)).X) = ()` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(T);
+  // CHECK:STDERR:   ^~~~
+  // CHECK:STDERR: fail_rewrite_requires_subst_in_nested_facet_type_types_differ.carbon:[[@LINE-7]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(T:! I({}) where .X = (I(.Y) where .X = ())) {}
+  // CHECK:STDERR:      ^
+  // CHECK:STDERR:
+  F(T);
+}
+
+// --- facet_type_in_assoc_constant.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X:! type;
+  let Y:! type;
+}
+
+fn F(T:! I where .X = (I where .X = () and .Y = ())) {}
+
+fn G(T:! I where .X = (I where .X = .Y and .Y = ())) {
+  F(T);
+}
+
+// --- fail_facet_type_in_assoc_constant_differs.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X:! type;
+  let Y:! type;
+  let Z:! type;
+}
+
+fn F(T:! I where .X = (I where .X = .Y)) {}
+
+fn G(T:! I where .X = (I where .X = () and .Y = () and .Z = {})) {
+  // CHECK:STDERR: fail_facet_type_in_assoc_constant_differs.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `I where .(I.X) = I where .(I.X) = () and .(I.Y) = () and .(I.Z) = {}` into type implementing `I where .(I.X) = I where .(I.X) = .(I.Y)` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(T);
+  // CHECK:STDERR:   ^~~~
+  // CHECK:STDERR: fail_facet_type_in_assoc_constant_differs.carbon:[[@LINE-6]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(T:! I where .X = (I where .X = .Y)) {}
+  // CHECK:STDERR:      ^
+  // CHECK:STDERR:
+  F(T);
+}
+
+// --- nested_facet_type_in_assoc_constant.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X:! type;
+  let Y:! type;
+  let Z:! type;
+}
+
+fn F(T:! I where .X = (I where .Y = (I where .X = () and .Y = ()))) {}
+
+fn G(T:! I where .X = (I where .Y = (I where .X = .Y and .Y = ()))) {
+  F(T);
+}
+
+// --- fail_nested_facet_type_assigns_same_assoc_constant.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X:! type;
+  let Y:! type;
+}
+
+fn F(T:! I where .Y = ()) {}
+
+// The `.Y = ()` is on a different `.Self` than `T` (an unattached self), so
+// should not satisfy `F`.
+fn G(T:! I where .X = (I where .Y = ())) {
+  // CHECK:STDERR: fail_nested_facet_type_assigns_same_assoc_constant.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `I where .(I.X) = I where .(I.Y) = ()` into type implementing `I where .(I.Y) = ()` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(T);
+  // CHECK:STDERR:   ^~~~
+  // CHECK:STDERR: fail_nested_facet_type_assigns_same_assoc_constant.carbon:[[@LINE-8]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(T:! I where .Y = ()) {}
+  // CHECK:STDERR:      ^
+  // CHECK:STDERR:
+  F(T);
+}
+
+// --- fail_nested_facet_type_in_assoc_constant_differs.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X:! type;
+  let Y:! type;
+  let Z:! type;
+}
+
+fn F(T:! I where .X = (I where .Y = (I where .X = .Y))) {}
+
+// `.X = .Y` does not match `.X = () and .Y = ()` as they are different resolved
+// facet types.
+fn G(T:! I where .X = (I where .Y = (I where .X = () and .Y = ()))) {
+  // CHECK:STDERR: fail_nested_facet_type_in_assoc_constant_differs.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `I where .(I.X) = I where .(I.Y) = I where .(I.X) = () and .(I.Y) = ()` into type implementing `I where .(I.X) = I where .(I.Y) = I where .(I.X) = .(I.Y)` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(T);
+  // CHECK:STDERR:   ^~~~
+  // CHECK:STDERR: fail_nested_facet_type_in_assoc_constant_differs.carbon:[[@LINE-8]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(T:! I where .X = (I where .Y = (I where .X = .Y))) {}
+  // CHECK:STDERR:      ^
+  // CHECK:STDERR:
+  F(T);
+}
+
+// The extra .Z rewrite makes a different resolved facet type which does not
+// match.
+fn G2(T:! I where .X = (I where .Y = (I where .X = .Y and .Z = {}))) {
+  // CHECK:STDERR: fail_nested_facet_type_in_assoc_constant_differs.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `I where .(I.X) = I where .(I.Y) = I where .(I.X) = .(I.Y) and .(I.Z) = {}` into type implementing `I where .(I.X) = I where .(I.Y) = I where .(I.X) = .(I.Y)` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(T);
+  // CHECK:STDERR:   ^~~~
+  // CHECK:STDERR: fail_nested_facet_type_in_assoc_constant_differs.carbon:[[@LINE-21]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(T:! I where .X = (I where .Y = (I where .X = .Y))) {}
+  // CHECK:STDERR:      ^
+  // CHECK:STDERR:
+  F(T);
+}
+
+// --- fail_nested_facet_type_from_constant.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X:! type;
+  let Y:! type;
+}
+
+fn F(T:! I where .X = (I where .Y = (I where .X = .Y, ))) {}
+
+// References to named constants in a facet type don't work at all. If they did,
+// then when the `Constant` facet type is put into the RHS of a rewrite
+// constraint, its references to `.Self` must be modified to not refer to the
+// top level `.Self` which is `T`. If done correctly, they will match the
+// `.Self` references in the same position in the parameter of `F`. If not, the
+// `.X` within becomes self-referential and makes a cycle.
+
+fn G1() {
+  let Constant:! type = I where .X = .Y;
+
+  fn G(T:! I where .X = (I where .Y = (Constant, ))) {
+    // CHECK:STDERR: fail_nested_facet_type_from_constant.carbon:[[@LINE+7]]:5: error: cannot convert type `T` that implements `I where .(I.X) = I where .(I.Y) = (Constant,)` into type implementing `I where .(I.X) = I where .(I.Y) = (I where .(I.X) = .(I.Y),)` [ConversionFailureFacetToFacet]
+    // CHECK:STDERR:     F(T);
+    // CHECK:STDERR:     ^~~~
+    // CHECK:STDERR: fail_nested_facet_type_from_constant.carbon:[[@LINE-16]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+    // CHECK:STDERR: fn F(T:! I where .X = (I where .Y = (I where .X = .Y, ))) {}
+    // CHECK:STDERR:      ^
+    // CHECK:STDERR:
+    F(T);
+  }
+}
+
+fn G2() {
+  let Constant:! type = (I where .X = .Y, );
+
+  fn G(T:! I where .X = (I where .Y = Constant)) {
+    // CHECK:STDERR: fail_nested_facet_type_from_constant.carbon:[[@LINE+7]]:5: error: cannot convert type `T` that implements `I where .(I.X) = I where .(I.Y) = Constant` into type implementing `I where .(I.X) = I where .(I.Y) = (I where .(I.X) = .(I.Y),)` [ConversionFailureFacetToFacet]
+    // CHECK:STDERR:     F(T);
+    // CHECK:STDERR:     ^~~~
+    // CHECK:STDERR: fail_nested_facet_type_from_constant.carbon:[[@LINE-31]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+    // CHECK:STDERR: fn F(T:! I where .X = (I where .Y = (I where .X = .Y, ))) {}
+    // CHECK:STDERR:      ^
+    // CHECK:STDERR:
+    F(T);
+  }
+}
+
+fn G3() {
+  let Constant:! type = I where .Y = (I where .X = .Y, );
+
+  fn G(T:! I where .X = Constant) {
+    // CHECK:STDERR: fail_nested_facet_type_from_constant.carbon:[[@LINE+7]]:5: error: cannot convert type `T` that implements `I where .(I.X) = Constant` into type implementing `I where .(I.X) = I where .(I.Y) = (I where .(I.X) = .(I.Y),)` [ConversionFailureFacetToFacet]
+    // CHECK:STDERR:     F(T);
+    // CHECK:STDERR:     ^~~~
+    // CHECK:STDERR: fail_nested_facet_type_from_constant.carbon:[[@LINE-46]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+    // CHECK:STDERR: fn F(T:! I where .X = (I where .Y = (I where .X = .Y, ))) {}
+    // CHECK:STDERR:      ^
+    // CHECK:STDERR:
+    F(T);
+  }
+}
+
+fn G4() {
+  let Constant2:! type = (I where .X = .Y, );
+  let Constant:! type = Constant2;
+
+  fn G(T:! I where .X = (I where .Y = Constant)) {
+    // CHECK:STDERR: fail_nested_facet_type_from_constant.carbon:[[@LINE+7]]:5: error: cannot convert type `T` that implements `I where .(I.X) = I where .(I.Y) = Constant` into type implementing `I where .(I.X) = I where .(I.Y) = (I where .(I.X) = .(I.Y),)` [ConversionFailureFacetToFacet]
+    // CHECK:STDERR:     F(T);
+    // CHECK:STDERR:     ^~~~
+    // CHECK:STDERR: fail_nested_facet_type_from_constant.carbon:[[@LINE-62]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+    // CHECK:STDERR: fn F(T:! I where .X = (I where .Y = (I where .X = .Y, ))) {}
+    // CHECK:STDERR:      ^
+    // CHECK:STDERR:
+    F(T);
+  }
+}
+
+fn G5() {
+  let Constant2:! type = I where .X = .Y;
+  let Constant:! type = (Constant2, );
+
+  fn G(T:! I where .X = (I where .Y = Constant)) {
+    // CHECK:STDERR: fail_nested_facet_type_from_constant.carbon:[[@LINE+7]]:5: error: cannot convert type `T` that implements `I where .(I.X) = I where .(I.Y) = Constant` into type implementing `I where .(I.X) = I where .(I.Y) = (I where .(I.X) = .(I.Y),)` [ConversionFailureFacetToFacet]
+    // CHECK:STDERR:     F(T);
+    // CHECK:STDERR:     ^~~~
+    // CHECK:STDERR: fail_nested_facet_type_from_constant.carbon:[[@LINE-78]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+    // CHECK:STDERR: fn F(T:! I where .X = (I where .Y = (I where .X = .Y, ))) {}
+    // CHECK:STDERR:      ^
+    // CHECK:STDERR:
+    F(T);
+  }
+}
+
+fn G6() {
+  let Constant2:! type = (I where .X = .Y, );
+  let Constant:! type = I where .Y = Constant2;
+
+  fn G(T:! I where .X = Constant) {
+    // CHECK:STDERR: fail_nested_facet_type_from_constant.carbon:[[@LINE+7]]:5: error: cannot convert type `T` that implements `I where .(I.X) = Constant` into type implementing `I where .(I.X) = I where .(I.Y) = (I where .(I.X) = .(I.Y),)` [ConversionFailureFacetToFacet]
+    // CHECK:STDERR:     F(T);
+    // CHECK:STDERR:     ^~~~
+    // CHECK:STDERR: fail_nested_facet_type_from_constant.carbon:[[@LINE-94]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+    // CHECK:STDERR: fn F(T:! I where .X = (I where .Y = (I where .X = .Y, ))) {}
+    // CHECK:STDERR:      ^
+    // CHECK:STDERR:
+    F(T);
+  }
+}
+
+// ---fail_nested_facet_type_from_constant_differs.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X:! type;
+  let Y:! type;
+}
+
+fn F(T:! I where .X = (I where .Y = (I where .X = .Y, ))) {}
+
+fn G1() {
+  let Constant:! type = I where .X = () and .Y = ();
+
+  fn G(T:! I where .X = (I where .Y = (Constant, ))) {
+    // CHECK:STDERR: fail_nested_facet_type_from_constant_differs.carbon:[[@LINE+7]]:5: error: cannot convert type `T` that implements `I where .(I.X) = I where .(I.Y) = (Constant,)` into type implementing `I where .(I.X) = I where .(I.Y) = (I where .(I.X) = .(I.Y),)` [ConversionFailureFacetToFacet]
+    // CHECK:STDERR:     F(T);
+    // CHECK:STDERR:     ^~~~
+    // CHECK:STDERR: fail_nested_facet_type_from_constant_differs.carbon:[[@LINE-9]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+    // CHECK:STDERR: fn F(T:! I where .X = (I where .Y = (I where .X = .Y, ))) {}
+    // CHECK:STDERR:      ^
+    // CHECK:STDERR:
+    F(T);
+  }
+}
+
+// --- rewrite_requires_subst_in_nested_access_of_self.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let I1:! type;
+  let I2:! type;
+}
+
+interface J {
+  let J1:! I;
+}
+
+interface K {
+  let K1:! J;
+}
+
+fn F(T:! I & J & K where .K1 = .Self and .J1 = .Self and .I1 = (.K1.J1).I2) {}
+
+fn G(T:! I & J & K where .K1 = .Self and .J1 = .Self and .I1 = .I2) {
+  F(T);
+}
+
+// --- fail_rewrite_requires_subst_in_nested_access_of_self_wrong_type.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let I1:! type;
+  let I2:! type;
+}
+
+interface J {
+  let J1:! I;
+}
+
+interface K {
+  let K1:! J;
+}
+
+fn F(T:! I & J & K where .K1 = .Self and .J1 = .Self and .I1 = (.K1.J1).I2) {}
+
+// F's requirement I1 = I2 is not met, as I1 = () and I2 = {}
+fn G(T:! I & J & K where .K1 = .Self and .J1 = .Self and .I1 = () and .I2 = {}) {
+  // CHECK:STDERR: fail_rewrite_requires_subst_in_nested_access_of_self_wrong_type.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `I & J & K where .(K.K1) = .Self as J and .(J.J1) = .Self as I and .(I.I1) = () and .(I.I2) = {}` into type implementing `I & J & K where .(K.K1) = .Self as J and .(J.J1) = .Self as I and .(I.I1) = .(I.I2)` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(T);
+  // CHECK:STDERR:   ^~~~
+  // CHECK:STDERR: fail_rewrite_requires_subst_in_nested_access_of_self_wrong_type.carbon:[[@LINE-7]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(T:! I & J & K where .K1 = .Self and .J1 = .Self and .I1 = (.K1.J1).I2) {}
+  // CHECK:STDERR:      ^
+  // CHECK:STDERR:
+  F(T);
+}
+
+// F's requirement I1 = I2 is not met, as I1 = {} and I2 is unspecified
+fn G2(T:! I & J & K where .K1 = .Self and .J1 = .Self and .I1 = {}) {
+  // CHECK:STDERR: fail_rewrite_requires_subst_in_nested_access_of_self_wrong_type.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `I & J & K where .(K.K1) = .Self as J and .(J.J1) = .Self as I and .(I.I1) = {}` into type implementing `I & J & K where .(K.K1) = .Self as J and .(J.J1) = .Self as I and .(I.I1) = .(I.I2)` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(T);
+  // CHECK:STDERR:   ^~~~
+  // CHECK:STDERR: fail_rewrite_requires_subst_in_nested_access_of_self_wrong_type.carbon:[[@LINE-19]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(T:! I & J & K where .K1 = .Self and .J1 = .Self and .I1 = (.K1.J1).I2) {}
+  // CHECK:STDERR:      ^
+  // CHECK:STDERR:
+  F(T);
+}
+
+// F's requirement I1 = I2 is not met, as I2 = {} and I1 is unspecified
+fn G3(T:! I & J & K where .K1 = .Self and .J1 = .Self and .I2 = {}) {
+  // CHECK:STDERR: fail_rewrite_requires_subst_in_nested_access_of_self_wrong_type.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `I & J & K where .(K.K1) = .Self as J and .(J.J1) = .Self as I and .(I.I2) = {}` into type implementing `I & J & K where .(K.K1) = .Self as J and .(J.J1) = .Self as I and .(I.I1) = .(I.I2)` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(T);
+  // CHECK:STDERR:   ^~~~
+  // CHECK:STDERR: fail_rewrite_requires_subst_in_nested_access_of_self_wrong_type.carbon:[[@LINE-31]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(T:! I & J & K where .K1 = .Self and .J1 = .Self and .I1 = (.K1.J1).I2) {}
+  // CHECK:STDERR:      ^
+  // CHECK:STDERR:
+  F(T);
+}
+
+// --- fail_todo_rewrite_requires_subst_in_nested_access_of_other.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let I1:! type;
+}
+
+interface J {
+  let J1:! I;
+  let J2:! type;
+}
+
+interface K {
+  let K1:! J;
+}
+
+// .K1.J1 is an ImplWitnessAccess into Self. The Self witness will be subst'd in
+// for `U` and it will eval to the ImplWitnessAccess inside of `U.I1`. Then that
+// will need to be subst'd to find the value of I1 in U's witness.
+fn F(U:! I, T:! J & K where .J2 = (.K1.J1).I1) {}
+
+fn G(U:! I where .I1 = (), T:! J & K where .K1 = .Self and .J1 = U and .J2 = ()) {
+  // CHECK:STDERR: fail_todo_rewrite_requires_subst_in_nested_access_of_other.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `J & K where .(J.J2) = () and .(K.K1) = .Self as J and .(J.J1) = U as I` into type implementing `J & K where .(J.J2) = .(K.K1).(J.J1).(I.I1)` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(U, T);
+  // CHECK:STDERR:   ^~~~~~~
+  // CHECK:STDERR: fail_todo_rewrite_requires_subst_in_nested_access_of_other.carbon:[[@LINE-6]]:13: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(U:! I, T:! J & K where .J2 = (.K1.J1).I1) {}
+  // CHECK:STDERR:             ^
+  // CHECK:STDERR:
+  F(U, T);
+}
+
+// --- fail_rewrite_requires_subst_in_nested_access_of_other_wrong_type.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let I1:! type;
+}
+
+interface J {
+  let J1:! I;
+  let J2:! type;
+}
+
+interface K {
+  let K1:! J;
+}
+
+fn F(U:! I, T:! J & K where .J2 = (.K1.J1).I1) {}
+
+// F's requirement J2 = I1 is not met as J2 = () and I1 = {}
+fn G(U:! I where .I1 = {}, T:! J & K where .K1 = .Self and .J1 = U and .J2 = ()) {
+  // CHECK:STDERR: fail_rewrite_requires_subst_in_nested_access_of_other_wrong_type.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `J & K where .(J.J2) = () and .(K.K1) = .Self as J and .(J.J1) = U as I` into type implementing `J & K where .(J.J2) = .(K.K1).(J.J1).(I.I1)` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(U, T);
+  // CHECK:STDERR:   ^~~~~~~
+  // CHECK:STDERR: fail_rewrite_requires_subst_in_nested_access_of_other_wrong_type.carbon:[[@LINE-7]]:13: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(U:! I, T:! J & K where .J2 = (.K1.J1).I1) {}
+  // CHECK:STDERR:             ^
+  // CHECK:STDERR:
+  F(U, T);
+}
+
+// F's requirement J2 = I1 is not met as J2 = () and I1 is unspecified
+fn G2(U:! I, T:! J & K where .K1 = .Self and .J1 = U and .J2 = ()) {
+  // CHECK:STDERR: fail_rewrite_requires_subst_in_nested_access_of_other_wrong_type.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `J & K where .(J.J2) = () and .(K.K1) = .Self as J and .(J.J1) = U` into type implementing `J & K where .(J.J2) = .(K.K1).(J.J1).(I.I1)` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(U, T);
+  // CHECK:STDERR:   ^~~~~~~
+  // CHECK:STDERR: fail_rewrite_requires_subst_in_nested_access_of_other_wrong_type.carbon:[[@LINE-19]]:13: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(U:! I, T:! J & K where .J2 = (.K1.J1).I1) {}
+  // CHECK:STDERR:             ^
+  // CHECK:STDERR:
+  F(U, T);
+}
+
+// F's requirement J2 = I1 is not met as I1 = {} and J2 is unspecified
+fn G3(U:! I where .I1 = {}, T:! J & K where .K1 = .Self and .J1 = U) {
+  // CHECK:STDERR: fail_rewrite_requires_subst_in_nested_access_of_other_wrong_type.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `J & K where .(K.K1) = .Self as J and .(J.J1) = U as I` into type implementing `J & K where .(J.J2) = .(K.K1).(J.J1).(I.I1)` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(U, T);
+  // CHECK:STDERR:   ^~~~~~~
+  // CHECK:STDERR: fail_rewrite_requires_subst_in_nested_access_of_other_wrong_type.carbon:[[@LINE-31]]:13: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(U:! I, T:! J & K where .J2 = (.K1.J1).I1) {}
+  // CHECK:STDERR:             ^
+  // CHECK:STDERR:
+  F(U, T);
+}
+
+// --- rewrite_requires_subst_in_nested_access_of_other_with_two_witnesses.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let I1:! type;
+}
+
+interface J {
+  let J1:! type;
+}
+
+interface K {
+  let K1:! J & I;
+  let K2:! type;
+  let K3:! type;
+}
+
+fn F(U:! I & J, T:! K where .K2 = .K1.I1 and .K3 = .K1.J1) {}
+
+fn G(U:! I & J where .I1 = () and .J1 = {}, T:! K where .K1 = U and .K2 = () and .K3 = {}) {
+  F(U, T);
+}
+
+// --- fail_rewrite_requires_subst_in_nested_access_of_other_with_two_witnesses_wrong_type.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let I1:! type;
+}
+
+interface J {
+  let J1:! type;
+}
+
+interface K {
+  let K1:! J & I;
+  let K2:! type;
+  let K3:! type;
+}
+
+fn F(U:! I & J, T:! K where .K2 = .K1.I1 and .K3 = .K1.J1) {}
+
+// K2 = I1 fails since K2 = {} and I1 = ()
+fn G(U:! I & J where .I1 = () and .J1 = {}, T:! K where .K1 = U and .K2 = {} and .K3 = {}) {
+  // CHECK:STDERR: fail_rewrite_requires_subst_in_nested_access_of_other_with_two_witnesses_wrong_type.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `K where .(K.K2) = {} and .(K.K1) = U as I & J and .(K.K3) = {}` into type implementing `K where .(K.K2) = .(K.K1).(I.I1) and .(K.K3) = .(K.K1).(J.J1)` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(U, T);
+  // CHECK:STDERR:   ^~~~~~~
+  // CHECK:STDERR: fail_rewrite_requires_subst_in_nested_access_of_other_with_two_witnesses_wrong_type.carbon:[[@LINE-7]]:17: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(U:! I & J, T:! K where .K2 = .K1.I1 and .K3 = .K1.J1) {}
+  // CHECK:STDERR:                 ^
+  // CHECK:STDERR:
+  F(U, T);
+}
+
+// K2 = I1 fails since I1 = () and K2 is unspecified.
+fn G2(U:! I & J where .I1 = () and .J1 = {}, T:! K where .K1 = U and .K3 = {}) {
+  // CHECK:STDERR: fail_rewrite_requires_subst_in_nested_access_of_other_with_two_witnesses_wrong_type.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `K where .(K.K1) = U as I & J and .(K.K3) = {}` into type implementing `K where .(K.K2) = .(K.K1).(I.I1) and .(K.K3) = .(K.K1).(J.J1)` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(U, T);
+  // CHECK:STDERR:   ^~~~~~~
+  // CHECK:STDERR: fail_rewrite_requires_subst_in_nested_access_of_other_with_two_witnesses_wrong_type.carbon:[[@LINE-19]]:17: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(U:! I & J, T:! K where .K2 = .K1.I1 and .K3 = .K1.J1) {}
+  // CHECK:STDERR:                 ^
+  // CHECK:STDERR:
+  F(U, T);
+}
+
+// K2 = I1 fails since K2 = () and I1 is unspecified.
+fn G3(U:! I & J where .J1 = {}, T:! K where .K1 = U and .K2 = () and .K3 = {}) {
+  // CHECK:STDERR: fail_rewrite_requires_subst_in_nested_access_of_other_with_two_witnesses_wrong_type.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `K where .(K.K2) = () and .(K.K1) = U as I & J and .(K.K3) = {}` into type implementing `K where .(K.K2) = .(K.K1).(I.I1) and .(K.K3) = .(K.K1).(J.J1)` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(U, T);
+  // CHECK:STDERR:   ^~~~~~~
+  // CHECK:STDERR: fail_rewrite_requires_subst_in_nested_access_of_other_with_two_witnesses_wrong_type.carbon:[[@LINE-31]]:17: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(U:! I & J, T:! K where .K2 = .K1.I1 and .K3 = .K1.J1) {}
+  // CHECK:STDERR:                 ^
+  // CHECK:STDERR:
+  F(U, T);
+}
+
+// K3 = J1 fails since J1 = {} and K3 is unspecified.
+fn G4(U:! I & J where .I1 = () and .J1 = {}, T:! K where .K1 = U and .K2 = ()) {
+  // CHECK:STDERR: fail_rewrite_requires_subst_in_nested_access_of_other_with_two_witnesses_wrong_type.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `K where .(K.K2) = () and .(K.K1) = U as I & J` into type implementing `K where .(K.K2) = .(K.K1).(I.I1) and .(K.K3) = .(K.K1).(J.J1)` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(U, T);
+  // CHECK:STDERR:   ^~~~~~~
+  // CHECK:STDERR: fail_rewrite_requires_subst_in_nested_access_of_other_with_two_witnesses_wrong_type.carbon:[[@LINE-43]]:17: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(U:! I & J, T:! K where .K2 = .K1.I1 and .K3 = .K1.J1) {}
+  // CHECK:STDERR:                 ^
+  // CHECK:STDERR:
+  F(U, T);
+}
+
+// K3 = J1 fails since K3 = {} and J1 is unspecified.
+fn G5(U:! I & J where .I1 = (), T:! K where .K1 = U and .K2 = () and .K3 = {}) {
+  // CHECK:STDERR: fail_rewrite_requires_subst_in_nested_access_of_other_with_two_witnesses_wrong_type.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `K where .(K.K2) = () and .(K.K1) = U as I & J and .(K.K3) = {}` into type implementing `K where .(K.K2) = .(K.K1).(I.I1) and .(K.K3) = .(K.K1).(J.J1)` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(U, T);
+  // CHECK:STDERR:   ^~~~~~~
+  // CHECK:STDERR: fail_rewrite_requires_subst_in_nested_access_of_other_with_two_witnesses_wrong_type.carbon:[[@LINE-55]]:17: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(U:! I & J, T:! K where .K2 = .K1.I1 and .K3 = .K1.J1) {}
+  // CHECK:STDERR:                 ^
+  // CHECK:STDERR:
+  F(U, T);
+}
+
+// --- fail_target_rewrites_dont_apply_to_source.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let I1:! type;
+  let I2:! type;
+  let I3:! type;
+  let I4:! type;
+}
+
+fn F(T:! I where .I1 = () and .I2 = ()) {}
+
+fn G(T:! I where .I1 = .I2) {
+  // CHECK:STDERR: fail_target_rewrites_dont_apply_to_source.carbon:[[@LINE+7]]:3: error: cannot convert type `T` that implements `I where .(I.I1) = .(I.I2)` into type implementing `I where .(I.I1) = () and .(I.I2) = ()` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   F(T);
+  // CHECK:STDERR:   ^~~~
+  // CHECK:STDERR: fail_target_rewrites_dont_apply_to_source.carbon:[[@LINE-6]]:6: note: initializing generic parameter `T` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn F(T:! I where .I1 = () and .I2 = ()) {}
+  // CHECK:STDERR:      ^
+  // CHECK:STDERR:
+  F(T);
+}
+
+// --- nested_facet_type_used_as_root_facet_type.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let X:! type;
+  let Y:! type;
+}
+
+fn F(T:! I where .X = (I where .Y = {}), U:! T.X) {}
+
+fn G(T:! I where .X = (I where .Y = {}), U:! I where .Y = {}) {
+  F(T, U);
+}

toolchain/check/testdata/impl/impl_assoc_const.carbon

@@ -337,6 +337,13 @@ impl CD as IF where .F = 0 {
   fn F() {}
 }
 
+// --- facet_type_in_assoc_constant.carbon
+library "[[@TEST_NAME]]";
+
+interface M { let X:! type; }
+
+impl () as M where .X = (M where .X = (M where .X = {})) {}
+
 // CHECK:STDOUT: --- fail_many_different.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {

toolchain/check/testdata/where_expr/equal_rewrite.carbon

@@ -72,7 +72,7 @@ fn Reversed(N:! J where .L = bool and .K = ()) {
   Alphabetical(N);
 }
 
-// --- todo_fail_rewrites_mismatch_right.carbon
+// --- fail_rewrites_mismatch_right.carbon
 
 library "[[@TEST_NAME]]";
 
@@ -83,11 +83,17 @@ interface O {
 fn WithInteger(Q:! O where .P = i32) {}
 
 fn WithBool(R:! O where .P = bool) {
-  // TODO: This should fail.
+  // CHECK:STDERR: fail_rewrites_mismatch_right.carbon:[[@LINE+7]]:3: error: cannot convert type `R` that implements `O where .(O.P) = bool` into type implementing `O where .(O.P) = i32` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   WithInteger(R);
+  // CHECK:STDERR:   ^~~~~~~~~~~~~~
+  // CHECK:STDERR: fail_rewrites_mismatch_right.carbon:[[@LINE-6]]:16: note: initializing generic parameter `Q` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn WithInteger(Q:! O where .P = i32) {}
+  // CHECK:STDERR:                ^
+  // CHECK:STDERR:
   WithInteger(R);
 }
 
-// --- todo_fail_rewrites_mismatch_left.carbon
+// --- fail_rewrites_mismatch_left.carbon
 
 library "[[@TEST_NAME]]";
 
@@ -99,7 +105,13 @@ interface S {
 fn WithT(V:! S where .T = ()) {}
 
 fn WithU(W:! S where .U = ()) {
-  // TODO: This should fail.
+  // CHECK:STDERR: fail_rewrites_mismatch_left.carbon:[[@LINE+7]]:3: error: cannot convert type `W` that implements `S where .(S.U) = ()` into type implementing `S where .(S.T) = ()` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   WithT(W);
+  // CHECK:STDERR:   ^~~~~~~~
+  // CHECK:STDERR: fail_rewrites_mismatch_left.carbon:[[@LINE-6]]:10: note: initializing generic parameter `V` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fn WithT(V:! S where .T = ()) {}
+  // CHECK:STDERR:          ^
+  // CHECK:STDERR:
   WithT(W);
 }