Resolve the RHS of rewrite constraints in facets (#5639)

If the RHS of a rewrite constraint refers to an associated constant,
pull the value for that constant from other rewrite constraints. We
repeat this each time a RHS value is changed until we reach a fixed
point, as per the "Rewrite constraint resolution" rule:
https://docs.carbon-lang.dev/docs/design/generics/appendix-rewrite-constraints.html#rewrite-constraint-resolution

While replacing references to associated constants in the RHS, if the
reference is to the LHS of the same rewrite constraint, we diagnose it
as a cycle which has no fixed point, and replace reference to the
associated constant with `ErrorInst`.

toolchain/check/facet_type.cpp

@@ -5,10 +5,12 @@
 #include "toolchain/check/facet_type.h"
 
 #include "toolchain/check/convert.h"
+#include "toolchain/check/diagnostic_helpers.h"
 #include "toolchain/check/generic.h"
 #include "toolchain/check/import_ref.h"
 #include "toolchain/check/inst.h"
 #include "toolchain/check/interface.h"
+#include "toolchain/check/subst.h"
 #include "toolchain/check/type.h"
 #include "toolchain/check/type_completion.h"
 #include "toolchain/sem_ir/ids.h"
@@ -281,44 +283,152 @@ auto IsPeriodSelf(Context& context, SemIR::InstId inst_id) -> bool {
   return false;
 }
 
-auto ResolveRewriteConstraintsAndCanonicalize(Context& context,
-                                              SemIR::LocId loc_id,
-                                              SemIR::FacetTypeInfo& facet_type)
-    -> void {
+// If `inst_id` is the ID of an `ImplWitnessAccess` into `.Self`, return it.
+// Otherwise, returns `nullopt`.
+static auto TryGetImplWitnessAccessOfPeriodSelf(Context& context,
+                                                SemIR::InstId inst_id)
+    -> std::optional<SemIR::ImplWitnessAccess> {
+  auto lhs_access = context.insts().TryGetAs<SemIR::ImplWitnessAccess>(inst_id);
+  if (!lhs_access) {
+    return std::nullopt;
+  }
+  auto lhs_lookup = context.insts().TryGetAs<SemIR::LookupImplWitness>(
+      lhs_access->witness_id);
+  if (!lhs_lookup) {
+    return std::nullopt;
+  }
+  if (!IsPeriodSelf(context, lhs_lookup->query_self_inst_id)) {
+    return std::nullopt;
+  }
+  return lhs_access;
+}
+
+// To be used for substituting into the RHS of a rewrite constraint.
+//
+// It will substitute any `ImplWitnessAccess` into `.Self` (a reference to an
+// associated constant) with the RHS of another rewrite constraint that writes
+// to the same associated constant. For example:
+// ```
+// Z where .X = () and .Y = .X
+// ```
+// Here the second `.X` is an `ImplWitnessAccess` which would be substituted by
+// finding the first rewrite constraint, where the LHS is for the same
+// associated constant and using its RHS. So the substitution would produce:
+// ```
+// Z where .X = () and .Y = ()
+// ```
+//
+// This additionally diagnoses cycles when the `ImplWitnessAccess` is reading
+// from the same rewrite constraint, and is thus assigning to the associated
+// constant a value that refers to the same associated constant, such as with
+// `Z where .X = C(.X)`. In the event of a cycle, the `ImplWitnessAccess` is
+// replaced with `ErrorInst` so that further evaluation of the
+// `ImplWitnessAccess` will not loop infinitely.
+class SubstImplWitnessAccessCallbacks : public SubstInstCallbacks {
+ public:
+  // The `facet_type_info` is for the facet whose rewrite constraints are being
+  // substituted, and where it looks for rewritten values to substitute from.
+  //
+  // The `substituting_constraint` is the rewrite constraint for which the RHS
+  // is being substituted with the value from another rewrite constraint, if
+  // possible. That is, `.Y = .X` in the example in the class docs.
+  explicit SubstImplWitnessAccessCallbacks(
+      Context* context, SemIR::LocId loc_id,
+      const SemIR::FacetTypeInfo* facet_type_info,
+      const SemIR::FacetTypeInfo::RewriteConstraint* substituting_constraint)
+      : SubstInstCallbacks(context),
+        loc_id_(loc_id),
+        facet_type_info_(*facet_type_info),
+        substituting_constraint_(substituting_constraint) {}
+
+  auto Subst(SemIR::InstId& rhs_inst_id) const -> bool override {
+    if (context().constant_values().Get(rhs_inst_id).is_concrete()) {
+      return true;
+    }
+
+    auto rhs_access =
+        TryGetImplWitnessAccessOfPeriodSelf(context(), rhs_inst_id);
+    if (!rhs_access) {
+      return false;
+    }
+
+    // TODO: We could consider replacing this loop, which makes for an O(N^2)
+    // algorithm with something more efficient for searching, such as a map.
+    // However that would probably require heap allocations which may be worse
+    // overall since the number of rewrite constraints is generally low.
+    for (const auto& search_constraint : facet_type_info_.rewrite_constraints) {
+      auto search_lhs_access = TryGetImplWitnessAccessOfPeriodSelf(
+          context(), search_constraint.lhs_id);
+      if (!search_lhs_access) {
+        continue;
+      }
+
+      if (search_lhs_access->witness_id == rhs_access->witness_id &&
+          search_lhs_access->index == rhs_access->index) {
+        if (&search_constraint == substituting_constraint_) {
+          if (search_constraint.rhs_id != SemIR::ErrorInst::InstId) {
+            CARBON_DIAGNOSTIC(FacetTypeConstraintCycle, Error,
+                              "found cycle in facet type constraint for {0}",
+                              InstIdAsConstant);
+            // TODO: It would be nice to note the places where the values are
+            // assigned but rewrite constraint instructions are from canonical
+            // constant values, and have no locations. We'd need to store a
+            // location along with them in the rewrite constraints, and track
+            // propagation of locations here, which may imply heap allocations.
+            context().emitter().Emit(loc_id_, FacetTypeConstraintCycle,
+                                     substituting_constraint_->lhs_id);
+            rhs_inst_id = SemIR::ErrorInst::InstId;
+          }
+        } else {
+          rhs_inst_id = search_constraint.rhs_id;
+        }
+        return true;
+      }
+    }
+
+    return false;
+  }
+
+  auto Rebuild(SemIR::InstId /*orig_inst_id*/, SemIR::Inst new_inst) const
+      -> SemIR::InstId override {
+    return RebuildNewInst(loc_id_, new_inst);
+  }
+
+ private:
+  SemIR::LocId loc_id_;
+  const SemIR::FacetTypeInfo& facet_type_info_;
+  const SemIR::FacetTypeInfo::RewriteConstraint* substituting_constraint_;
+};
+
+auto ResolveRewriteConstraintsAndCanonicalize(
+    Context& context, SemIR::LocId loc_id,
+    SemIR::FacetTypeInfo& facet_type_info) -> void {
   // This operation sorts and dedupes the rewrite constraints. They are sorted
   // primarily by the `lhs_id`, then by the `rhs_id`.
-  facet_type.Canonicalize();
+  facet_type_info.Canonicalize();
 
-  if (facet_type.rewrite_constraints.empty()) {
+  if (facet_type_info.rewrite_constraints.empty()) {
     return;
   }
 
-  for (size_t i = 0; i < facet_type.rewrite_constraints.size() - 1; ++i) {
-    auto& constraint = facet_type.rewrite_constraints[i];
+  for (size_t i = 0; i < facet_type_info.rewrite_constraints.size() - 1; ++i) {
+    auto& constraint = facet_type_info.rewrite_constraints[i];
     if (constraint.lhs_id == SemIR::ErrorInst::InstId ||
         constraint.rhs_id == SemIR::ErrorInst::InstId) {
       continue;
     }
 
     auto lhs_access =
-        context.insts().TryGetAs<SemIR::ImplWitnessAccess>(constraint.lhs_id);
+        TryGetImplWitnessAccessOfPeriodSelf(context, constraint.lhs_id);
     if (!lhs_access) {
       continue;
     }
-    auto lhs_lookup = context.insts().TryGetAs<SemIR::LookupImplWitness>(
-        lhs_access->witness_id);
-    if (!lhs_lookup) {
-      continue;
-    }
-    if (!IsPeriodSelf(context, lhs_lookup->query_self_inst_id)) {
-      continue;
-    }
 
     // This loop moves `i` to the last position with the same LHS value, so that
     // we don't diagnose more than once within the same contiguous range of
     // assignments to a single LHS value.
-    for (; i < facet_type.rewrite_constraints.size() - 1; ++i) {
-      auto& next = facet_type.rewrite_constraints[i + 1];
+    for (; i < facet_type_info.rewrite_constraints.size() - 1; ++i) {
+      auto& next = facet_type_info.rewrite_constraints[i + 1];
       if (constraint.lhs_id != next.lhs_id) {
         break;
       }
@@ -345,9 +455,46 @@ auto ResolveRewriteConstraintsAndCanonicalize(Context& context,
     }
   }
 
+  while (true) {
+    bool applied_rewrite = false;
+
+    for (auto& constraint : facet_type_info.rewrite_constraints) {
+      if (constraint.lhs_id == SemIR::ErrorInst::InstId ||
+          constraint.rhs_id == SemIR::ErrorInst::InstId) {
+        continue;
+      }
+
+      auto lhs_access =
+          TryGetImplWitnessAccessOfPeriodSelf(context, constraint.lhs_id);
+      if (!lhs_access) {
+        continue;
+      }
+
+      // Replace any `ImplWitnessAccess` in the RHS of this constraint with the
+      // RHS of another constraint that sets the value of the associated
+      // constant being accessed in the RHS.
+      auto subst_inst_id =
+          SubstInst(context, constraint.rhs_id,
+                    SubstImplWitnessAccessCallbacks(
+                        &context, loc_id, &facet_type_info, &constraint));
+      if (subst_inst_id != constraint.rhs_id) {
+        constraint.rhs_id = subst_inst_id;
+        if (constraint.rhs_id != SemIR::ErrorInst::InstId) {
+          // If the RHS is replaced with a non-error value, we need to do
+          // another pass so that the new RHS value can continue to propagate.
+          applied_rewrite = true;
+        }
+      }
+    }
+
+    if (!applied_rewrite) {
+      break;
+    }
+  }
+
   // Canonicalize again, as we may have inserted errors into the rewrite
-  // constraints, and these could change sorting order.
-  facet_type.Canonicalize();
+  // constraints, and these could change sorting order and need to be deduped.
+  facet_type_info.Canonicalize();
 }
 
 }  // namespace Carbon::Check

toolchain/check/subst.cpp

@@ -19,6 +19,18 @@ auto SubstInstCallbacks::RebuildType(SemIR::TypeInstId type_inst_id) const
   return context().types().GetTypeIdForTypeInstId(type_inst_id);
 }
 
+auto SubstInstCallbacks::RebuildNewInst(SemIR::LocId loc_id,
+                                        SemIR::Inst new_inst) const
+    -> SemIR::InstId {
+  auto const_id = EvalOrAddInst(
+      context(), SemIR::LocIdAndInst::UncheckedLoc(loc_id, new_inst));
+  CARBON_CHECK(const_id.has_value(),
+               "Substitution into constant produced non-constant");
+  CARBON_CHECK(const_id.is_constant(),
+               "Substitution into constant produced runtime value");
+  return context().constant_values().GetInstId(const_id);
+}
+
 namespace {
 
 // Information about an instruction that we are substituting into.
@@ -393,13 +405,7 @@ class SubstConstantCallbacks final : public SubstInstCallbacks {
   // Rebuilds an instruction by building a new constant.
   auto Rebuild(SemIR::InstId /*old_inst_id*/, SemIR::Inst new_inst) const
       -> SemIR::InstId override {
-    auto const_id = EvalOrAddInst(
-        context(), SemIR::LocIdAndInst::UncheckedLoc(loc_id_, new_inst));
-    CARBON_CHECK(const_id.has_value(),
-                 "Substitution into constant produced non-constant");
-    CARBON_CHECK(const_id.is_constant(),
-                 "Substitution into constant produced runtime value");
-    return context().constant_values().GetInstId(const_id);
+    return RebuildNewInst(loc_id_, new_inst);
   }
 
  private:

toolchain/check/subst.h

@@ -45,6 +45,12 @@ class SubstInstCallbacks {
     return orig_inst_id;
   }
 
+  // Builds a new constant by evaluating `new_inst`, and returns its `InstId`.
+  //
+  // This can be used to implement `Rebuild` in straightforward cases.
+  auto RebuildNewInst(SemIR::LocId loc_id, SemIR::Inst new_inst) const
+      -> SemIR::InstId;
+
  private:
   Context* context_;
 };

toolchain/check/testdata/facet/facet_assoc_const.carbon

@@ -196,23 +196,34 @@ interface M { let X:! type; }
 // CHECK:STDERR:
 fn F(T:! M where .X = {} and .X = () and .X = {}) {}
 
-// --- todo_fail_cycle_single.carbon
+// --- fail_cycle_single.carbon
 library "[[@TEST_NAME]]";
 
 interface M { let X:! type; }
 
-// TODO: This should fail, as it resolves to `.X = .X` which is cyclical.
+// CHECK:STDERR: fail_cycle_single.carbon:[[@LINE+4]]:10: error: found cycle in facet type constraint for `.(M.X)` [FacetTypeConstraintCycle]
+// CHECK:STDERR: fn F(T:! M where .X = .X) {}
+// CHECK:STDERR:          ^~~~~~~~~~~~~~~
+// CHECK:STDERR:
 fn F(T:! M where .X = .X) {}
 
-// --- todo_fail_cycle.carbon
+// --- fail_cycle.carbon
 library "[[@TEST_NAME]]";
 
-interface M { let X:! type; let Y:! type; }
+interface M { let X:! type; let Y:! type; let Z:! type; }
 
-// TODO: This should fail, as it resolves to `.X = .X` which is cyclical.
-fn F(T:! M where .X = .Y and .Y = .X) {}
+// This fails because it resolves to `.X = .X` which is cyclical.
+// The value of .X and .Y becomes <error> but .Z is still valid.
+//
+//@dump-sem-ir-begin
+// CHECK:STDERR: fail_cycle.carbon:[[@LINE+4]]:10: error: found cycle in facet type constraint for `.(M.X)` [FacetTypeConstraintCycle]
+// CHECK:STDERR: fn F(T:! M where .X = .Y and .Y = .X and .Z = ()) {}
+// CHECK:STDERR:          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR:
+fn F(T:! M where .X = .Y and .Y = .X and .Z = ()) {}
+//@dump-sem-ir-end
 
-// --- todo_fail_cycle_between_interfaces.carbon
+// --- fail_cycle_between_interfaces.carbon
 library "[[@TEST_NAME]]";
 
 interface I {
@@ -223,10 +234,15 @@ interface J {
   let X3:! type;
 }
 
-// TODO: This should fail, as it resolves to `.X1 = .X1` which is cyclical.
+// This fails because it resolves to `.X1 = .X1` which is cyclical.
+//
+// CHECK:STDERR: fail_cycle_between_interfaces.carbon:[[@LINE+4]]:10: error: found cycle in facet type constraint for `.(I.X2)` [FacetTypeConstraintCycle]
+// CHECK:STDERR: fn G(T:! I & J where .X1 = .X3 and .X2 = .X1 and .X3 = .X2) {}
+// CHECK:STDERR:          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR:
 fn G(T:! I & J where .X1 = .X3 and .X2 = .X1 and .X3 = .X2) {}
 
-// --- todo_fail_indirect_cycle.carbon
+// --- fail_indirect_cycle.carbon
 library "[[@TEST_NAME]]";
 
 interface I {
@@ -234,15 +250,24 @@ interface I {
   let X2:! type;
 }
 
-// TODO: This should fail, as it resolves to `.X1 = .X1**` which is cyclical.
+// This fails because it resolves to `.X1 = .X1**` which is cyclical.
+//
+// CHECK:STDERR: fail_indirect_cycle.carbon:[[@LINE+4]]:10: error: found cycle in facet type constraint for `.(I.X1)` [FacetTypeConstraintCycle]
+// CHECK:STDERR: fn F(T:! I where .X1 = .X2* and .X2 = .X1*);
+// CHECK:STDERR:          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR:
 fn F(T:! I where .X1 = .X2* and .X2 = .X1*);
 
 class C(T:! type);
-// TODO: This should fail, as it resolves to `.X1 = C(C(.X1))` which is
-// cyclical.
+// This fails because it resolves to `.X1 = C(C(.X1))` which is cyclical.
+//
+// CHECK:STDERR: fail_indirect_cycle.carbon:[[@LINE+4]]:10: error: found cycle in facet type constraint for `.(I.X1)` [FacetTypeConstraintCycle]
+// CHECK:STDERR: fn G(T:! I where .X1 = C(.X2) and .X2 = C(.X1));
+// CHECK:STDERR:          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR:
 fn G(T:! I where .X1 = C(.X2) and .X2 = C(.X1));
 
-// --- todo_fail_complex_indirect_cycle.carbon
+// --- fail_complex_indirect_cycle.carbon
 library "[[@TEST_NAME]]";
 
 interface I {
@@ -253,8 +278,13 @@ interface I {
 
 class C(T:! type, U:! type);
 
-// TODO: This should fail, as it resolves to `.X1 = C(C(.X3, .X1), .X3)` which
-// is cyclical.
+// This fails because it resolves to `.X1 = C(C(.X3, .X1), .X3)` which is
+// cyclical.
+//
+// CHECK:STDERR: fail_complex_indirect_cycle.carbon:[[@LINE+4]]:10: error: found cycle in facet type constraint for `.(I.X1)` [FacetTypeConstraintCycle]
+// CHECK:STDERR: fn F(T:! I where .X1 = C(.X2, .X3) and .X2 = C(.X3, .X1));
+// CHECK:STDERR:          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR:
 fn F(T:! I where .X1 = C(.X2, .X3) and .X2 = C(.X3, .X1));
 
 // --- non-type.carbon
@@ -287,3 +317,88 @@ interface N {
 // CHECK:STDERR:          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 // CHECK:STDERR:
 fn F(T:! N where .Y = {.a = {}} and .Y = {.a = ()}) {}
+
+// CHECK:STDOUT: --- fail_cycle.carbon
+// CHECK:STDOUT:
+// CHECK:STDOUT: constants {
+// CHECK:STDOUT:   %M.type: type = facet_type <@M> [concrete]
+// CHECK:STDOUT:   %M.assoc_type: type = assoc_entity_type @M [concrete]
+// CHECK:STDOUT:   %assoc0: %M.assoc_type = assoc_entity element0, @M.%X [concrete]
+// CHECK:STDOUT:   %assoc1: %M.assoc_type = assoc_entity element1, @M.%Y [concrete]
+// CHECK:STDOUT:   %assoc2: %M.assoc_type = assoc_entity element2, @M.%Z [concrete]
+// CHECK:STDOUT:   %.Self: %M.type = bind_symbolic_name .Self [symbolic_self]
+// CHECK:STDOUT:   %.Self.as_type: type = facet_access_type %.Self [symbolic_self]
+// CHECK:STDOUT:   %M.lookup_impl_witness: <witness> = lookup_impl_witness %.Self, @M [symbolic_self]
+// CHECK:STDOUT:   %impl.elem0: type = impl_witness_access %M.lookup_impl_witness, element0 [symbolic_self]
+// CHECK:STDOUT:   %impl.elem1: type = impl_witness_access %M.lookup_impl_witness, element1 [symbolic_self]
+// CHECK:STDOUT:   %impl.elem2: type = impl_witness_access %M.lookup_impl_witness, element2 [symbolic_self]
+// CHECK:STDOUT:   %empty_tuple.type: type = tuple_type () [concrete]
+// CHECK:STDOUT:   %M_where.type: type = facet_type <@M where %impl.elem0 = <error> and %impl.elem1 = <error> and %impl.elem2 = %empty_tuple.type> [concrete]
+// CHECK:STDOUT:   %T: %M_where.type = bind_symbolic_name T, 0 [symbolic]
+// CHECK:STDOUT:   %pattern_type: type = pattern_type %M_where.type [concrete]
+// CHECK:STDOUT:   %F.type: type = fn_type @F [concrete]
+// CHECK:STDOUT:   %F: %F.type = struct_value () [concrete]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: imports {
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: file {
+// CHECK:STDOUT:   %F.decl: %F.type = fn_decl @F [concrete = constants.%F] {
+// CHECK:STDOUT:     %T.patt: %pattern_type = symbolic_binding_pattern T, 0 [concrete]
+// CHECK:STDOUT:   } {
+// CHECK:STDOUT:     %.loc13_12.1: type = splice_block %.loc13_12.2 [concrete = constants.%M_where.type] {
+// CHECK:STDOUT:       %M.ref: type = name_ref M, file.%M.decl [concrete = constants.%M.type]
+// CHECK:STDOUT:       <elided>
+// CHECK:STDOUT:       %.Self.ref.loc13_18: %M.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:       %X.ref.loc13_18: %M.assoc_type = name_ref X, @X.%assoc0 [concrete = constants.%assoc0]
+// CHECK:STDOUT:       %.Self.as_type.loc13_18: type = facet_access_type %.Self.ref.loc13_18 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:       %.loc13_18: type = converted %.Self.ref.loc13_18, %.Self.as_type.loc13_18 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:       %impl.elem0.loc13_18: type = impl_witness_access constants.%M.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
+// CHECK:STDOUT:       %.Self.ref.loc13_23: %M.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:       %Y.ref.loc13_23: %M.assoc_type = name_ref Y, @Y.%assoc1 [concrete = constants.%assoc1]
+// CHECK:STDOUT:       %.Self.as_type.loc13_23: type = facet_access_type %.Self.ref.loc13_23 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:       %.loc13_23: type = converted %.Self.ref.loc13_23, %.Self.as_type.loc13_23 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:       %impl.elem1.loc13_23: type = impl_witness_access constants.%M.lookup_impl_witness, element1 [symbolic_self = constants.%impl.elem1]
+// CHECK:STDOUT:       %.Self.ref.loc13_30: %M.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:       %Y.ref.loc13_30: %M.assoc_type = name_ref Y, @Y.%assoc1 [concrete = constants.%assoc1]
+// CHECK:STDOUT:       %.Self.as_type.loc13_30: type = facet_access_type %.Self.ref.loc13_30 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:       %.loc13_30: type = converted %.Self.ref.loc13_30, %.Self.as_type.loc13_30 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:       %impl.elem1.loc13_30: type = impl_witness_access constants.%M.lookup_impl_witness, element1 [symbolic_self = constants.%impl.elem1]
+// CHECK:STDOUT:       %.Self.ref.loc13_35: %M.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:       %X.ref.loc13_35: %M.assoc_type = name_ref X, @X.%assoc0 [concrete = constants.%assoc0]
+// CHECK:STDOUT:       %.Self.as_type.loc13_35: type = facet_access_type %.Self.ref.loc13_35 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:       %.loc13_35: type = converted %.Self.ref.loc13_35, %.Self.as_type.loc13_35 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:       %impl.elem0.loc13_35: type = impl_witness_access constants.%M.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
+// CHECK:STDOUT:       %.Self.ref.loc13_42: %M.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:       %Z.ref: %M.assoc_type = name_ref Z, @Z.%assoc2 [concrete = constants.%assoc2]
+// CHECK:STDOUT:       %.Self.as_type.loc13_42: type = facet_access_type %.Self.ref.loc13_42 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:       %.loc13_42: type = converted %.Self.ref.loc13_42, %.Self.as_type.loc13_42 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:       %impl.elem2: type = impl_witness_access constants.%M.lookup_impl_witness, element2 [symbolic_self = constants.%impl.elem2]
+// CHECK:STDOUT:       %.loc13_48.1: %empty_tuple.type = tuple_literal ()
+// CHECK:STDOUT:       %.loc13_48.2: type = converted %.loc13_48.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
+// CHECK:STDOUT:       %.loc13_12.2: type = where_expr %.Self [concrete = constants.%M_where.type] {
+// CHECK:STDOUT:         requirement_rewrite %impl.elem0.loc13_18, %impl.elem1.loc13_23
+// CHECK:STDOUT:         requirement_rewrite %impl.elem1.loc13_30, %impl.elem0.loc13_35
+// CHECK:STDOUT:         requirement_rewrite %impl.elem2, %.loc13_48.2
+// CHECK:STDOUT:       }
+// CHECK:STDOUT:     }
+// CHECK:STDOUT:     %T.loc13_6.1: %M_where.type = bind_symbolic_name T, 0 [symbolic = %T.loc13_6.2 (constants.%T)]
+// CHECK:STDOUT:   }
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: generic fn @F(%T.loc13_6.1: %M_where.type) {
+// CHECK:STDOUT:   %T.loc13_6.2: %M_where.type = bind_symbolic_name T, 0 [symbolic = %T.loc13_6.2 (constants.%T)]
+// CHECK:STDOUT:
+// CHECK:STDOUT: !definition:
+// CHECK:STDOUT:
+// CHECK:STDOUT:   fn() {
+// CHECK:STDOUT:   !entry:
+// CHECK:STDOUT:     return
+// CHECK:STDOUT:   }
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @F(constants.%T) {
+// CHECK:STDOUT:   %T.loc13_6.2 => constants.%T
+// CHECK:STDOUT: }
+// CHECK:STDOUT:

toolchain/check/testdata/impl/impl_assoc_const.carbon

@@ -229,21 +229,34 @@ interface M { let X:! type; }
 // CHECK:STDERR:
 impl () as M where .X = {} and .X = () and .X = {} {}
 
-// --- todo_fail_cycle_single.carbon
+// --- fail_cycle_single.carbon
 library "[[@TEST_NAME]]";
 
 interface M { let X:! type; }
 
-// TODO: This should fail, as it resolves to `.X = .X` which is cyclical.
+// This fails because it resolves to `.X = .X` which is cyclical.
+//
+// CHECK:STDERR: fail_cycle_single.carbon:[[@LINE+4]]:12: error: found cycle in facet type constraint for `.(M.X)` [FacetTypeConstraintCycle]
+// CHECK:STDERR: impl () as M where .X = .X {}
+// CHECK:STDERR:            ^~~~~~~~~~~~~~~
+// CHECK:STDERR:
 impl () as M where .X = .X {}
 
-// --- todo_fail_cycle.carbon
+// --- fail_cycle.carbon
 library "[[@TEST_NAME]]";
 
-interface M { let X:! type; let Y:! type; }
+interface M { let X:! type; let Y:! type; let Z:! type; }
 
-// TODO: This should fail, as it resolves to `.X = .X` which is cyclical.
-impl () as M where .X = .Y and .Y = .X {}
+// This fails because it resolves to `.X = .X` which is cyclical.
+// The value of .X and .Y becomes <error> but .Z is still valid.
+//
+//@dump-sem-ir-begin
+// CHECK:STDERR: fail_cycle.carbon:[[@LINE+4]]:12: error: found cycle in facet type constraint for `.(M.X)` [FacetTypeConstraintCycle]
+// CHECK:STDERR: impl () as M where .X = .Y and .Y = .X and .Z = () {}
+// CHECK:STDERR:            ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR:
+impl () as M where .X = .Y and .Y = .X and .Z = () {}
+//@dump-sem-ir-end
 
 // --- fail_todo_cycle_between_interfaces.carbon
 library "[[@TEST_NAME]]";
@@ -256,7 +269,7 @@ interface J {
   let X3:! type;
 }
 
-// TODO: This should fail, due to a cyclic definition of each value. But right
+// TODO: This should fail due to a cyclic definition of each value. But right
 // now it's failing due to compound member access in a rewrite constraint not
 // working.
 //
@@ -414,3 +427,71 @@ impl CD as IF where .F = 0 {
 // CHECK:STDOUT:   witness = file.%L.impl_witness
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
+// CHECK:STDOUT: --- fail_cycle.carbon
+// CHECK:STDOUT:
+// CHECK:STDOUT: constants {
+// CHECK:STDOUT:   %M.type: type = facet_type <@M> [concrete]
+// CHECK:STDOUT:   %M.assoc_type: type = assoc_entity_type @M [concrete]
+// CHECK:STDOUT:   %assoc0: %M.assoc_type = assoc_entity element0, @M.%X [concrete]
+// CHECK:STDOUT:   %assoc1: %M.assoc_type = assoc_entity element1, @M.%Y [concrete]
+// CHECK:STDOUT:   %assoc2: %M.assoc_type = assoc_entity element2, @M.%Z [concrete]
+// CHECK:STDOUT:   %empty_tuple.type: type = tuple_type () [concrete]
+// CHECK:STDOUT:   %.Self: %M.type = bind_symbolic_name .Self [symbolic_self]
+// CHECK:STDOUT:   %.Self.as_type: type = facet_access_type %.Self [symbolic_self]
+// CHECK:STDOUT:   %M.lookup_impl_witness: <witness> = lookup_impl_witness %.Self, @M [symbolic_self]
+// CHECK:STDOUT:   %impl.elem0: type = impl_witness_access %M.lookup_impl_witness, element0 [symbolic_self]
+// CHECK:STDOUT:   %impl.elem1: type = impl_witness_access %M.lookup_impl_witness, element1 [symbolic_self]
+// CHECK:STDOUT:   %impl.elem2: type = impl_witness_access %M.lookup_impl_witness, element2 [symbolic_self]
+// CHECK:STDOUT:   %M_where.type: type = facet_type <@M where %impl.elem0 = <error> and %impl.elem1 = <error> and %impl.elem2 = %empty_tuple.type> [concrete]
+// CHECK:STDOUT:   %M.impl_witness: <witness> = impl_witness file.%M.impl_witness_table [concrete]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: file {
+// CHECK:STDOUT:   impl_decl @impl [concrete] {} {
+// CHECK:STDOUT:     %.loc13_7.1: %empty_tuple.type = tuple_literal ()
+// CHECK:STDOUT:     %.loc13_7.2: type = converted %.loc13_7.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
+// CHECK:STDOUT:     %M.ref: type = name_ref M, file.%M.decl [concrete = constants.%M.type]
+// CHECK:STDOUT:     <elided>
+// CHECK:STDOUT:     %.Self.ref.loc13_20: %M.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %X.ref.loc13_20: %M.assoc_type = name_ref X, @X.%assoc0 [concrete = constants.%assoc0]
+// CHECK:STDOUT:     %.Self.as_type.loc13_20: type = facet_access_type %.Self.ref.loc13_20 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:     %.loc13_20: type = converted %.Self.ref.loc13_20, %.Self.as_type.loc13_20 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:     %impl.elem0.loc13_20: type = impl_witness_access constants.%M.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
+// CHECK:STDOUT:     %.Self.ref.loc13_25: %M.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %Y.ref.loc13_25: %M.assoc_type = name_ref Y, @Y.%assoc1 [concrete = constants.%assoc1]
+// CHECK:STDOUT:     %.Self.as_type.loc13_25: type = facet_access_type %.Self.ref.loc13_25 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:     %.loc13_25: type = converted %.Self.ref.loc13_25, %.Self.as_type.loc13_25 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:     %impl.elem1.loc13_25: type = impl_witness_access constants.%M.lookup_impl_witness, element1 [symbolic_self = constants.%impl.elem1]
+// CHECK:STDOUT:     %.Self.ref.loc13_32: %M.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %Y.ref.loc13_32: %M.assoc_type = name_ref Y, @Y.%assoc1 [concrete = constants.%assoc1]
+// CHECK:STDOUT:     %.Self.as_type.loc13_32: type = facet_access_type %.Self.ref.loc13_32 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:     %.loc13_32: type = converted %.Self.ref.loc13_32, %.Self.as_type.loc13_32 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:     %impl.elem1.loc13_32: type = impl_witness_access constants.%M.lookup_impl_witness, element1 [symbolic_self = constants.%impl.elem1]
+// CHECK:STDOUT:     %.Self.ref.loc13_37: %M.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %X.ref.loc13_37: %M.assoc_type = name_ref X, @X.%assoc0 [concrete = constants.%assoc0]
+// CHECK:STDOUT:     %.Self.as_type.loc13_37: type = facet_access_type %.Self.ref.loc13_37 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:     %.loc13_37: type = converted %.Self.ref.loc13_37, %.Self.as_type.loc13_37 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:     %impl.elem0.loc13_37: type = impl_witness_access constants.%M.lookup_impl_witness, element0 [symbolic_self = constants.%impl.elem0]
+// CHECK:STDOUT:     %.Self.ref.loc13_44: %M.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %Z.ref: %M.assoc_type = name_ref Z, @Z.%assoc2 [concrete = constants.%assoc2]
+// CHECK:STDOUT:     %.Self.as_type.loc13_44: type = facet_access_type %.Self.ref.loc13_44 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:     %.loc13_44: type = converted %.Self.ref.loc13_44, %.Self.as_type.loc13_44 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:     %impl.elem2: type = impl_witness_access constants.%M.lookup_impl_witness, element2 [symbolic_self = constants.%impl.elem2]
+// CHECK:STDOUT:     %.loc13_50.1: %empty_tuple.type = tuple_literal ()
+// CHECK:STDOUT:     %.loc13_50.2: type = converted %.loc13_50.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
+// CHECK:STDOUT:     %.loc13_14: type = where_expr %.Self [concrete = constants.%M_where.type] {
+// CHECK:STDOUT:       requirement_rewrite %impl.elem0.loc13_20, %impl.elem1.loc13_25
+// CHECK:STDOUT:       requirement_rewrite %impl.elem1.loc13_32, %impl.elem0.loc13_37
+// CHECK:STDOUT:       requirement_rewrite %impl.elem2, %.loc13_50.2
+// CHECK:STDOUT:     }
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %M.impl_witness_table = impl_witness_table (<error>, <error>, %impl_witness_assoc_constant), @impl [concrete]
+// CHECK:STDOUT:   %M.impl_witness: <witness> = impl_witness %M.impl_witness_table [concrete = constants.%M.impl_witness]
+// CHECK:STDOUT:   %impl_witness_assoc_constant: type = impl_witness_assoc_constant constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: impl @impl: %.loc13_7.2 as %.loc13_14 {
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   witness = file.%M.impl_witness
+// CHECK:STDOUT: }
+// CHECK:STDOUT:

toolchain/diagnostics/diagnostic_kind.def

@@ -482,6 +482,7 @@ CARBON_DIAGNOSTIC_KIND(WhereOnNonFacetType)
 CARBON_DIAGNOSTIC_KIND(AssociatedConstantNotConstantAfterConversion)
 CARBON_DIAGNOSTIC_KIND(AssociatedConstantWithDifferentValues)
 CARBON_DIAGNOSTIC_KIND(RewriteForAssociatedFunction)
+CARBON_DIAGNOSTIC_KIND(FacetTypeConstraintCycle)
 
 // Facet type combination.
 CARBON_DIAGNOSTIC_KIND(FacetTypeRequiredForTypeAndOperator)