Avoid incorrect conflicting assignment diags in rewrite constraints (#5686)

When building a FacetType from an existing FacetType, don't diagnose
rewrite constraints that are compatible with the existing FacetType.

To do this, we consider two RHS as identical[1] if they have the same
constant value after substituting from available rewrite constraints in
the being-constructed FacetType, since the syntactic representation of
the RHS is lost during eval.

[1]
https://docs.google.com/document/d/1Yt-i5AmF76LSvD4TrWRIAE_92kii6j5yFiW-S7ahzlg/edit?tab=t.0#heading=h.qti4vn50zwy

Author: danakj

toolchain/check/eval.cpp

@@ -634,11 +634,13 @@ static auto GetConstantFacetTypeInfo(EvalContext& eval_context,
              GetConstantValue(eval_context, interface.specific_id, phase)});
   }
 
-  // Rewrite constraints are resolved first before evaluation, so that we can
-  // work with the `ImplWitnessAccess` references to `.Self` without them
-  // evaluating to a value. It also ensures that any errors inserted during
-  // resolution will be seen by GetConstantValueIgnoringPeriodSelf() which will
-  // update the phase accordingly.
+  // Rewrite constraints are resolved first before replacing them with their
+  // canonical instruction, so that in a `WhereExpr` we can work with the
+  // `ImplWitnessAccess` references to `.Self` on the LHS of the constraints
+  // rather than the value of the associated constant they reference. It also
+  // ensures that any errors inserted during resolution will be seen by
+  // GetConstantValueIgnoringPeriodSelf() which will update the phase
+  // accordingly.
   info.rewrite_constraints = orig.rewrite_constraints;
   ResolveFacetTypeRewriteConstraints(eval_context.context(), loc_id,
                                      info.rewrite_constraints);

toolchain/check/eval_inst.cpp

@@ -16,6 +16,7 @@
 #include "toolchain/check/type.h"
 #include "toolchain/check/type_completion.h"
 #include "toolchain/diagnostics/diagnostic.h"
+#include "toolchain/parse/typed_nodes.h"
 #include "toolchain/sem_ir/expr_info.h"
 #include "toolchain/sem_ir/ids.h"
 #include "toolchain/sem_ir/pattern.h"

toolchain/check/facet_type.cpp

@@ -381,12 +381,8 @@ class SubstImplWitnessAccessCallbacks : public SubstInstCallbacks {
         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;
-    }
-
     if (!context().insts().Is<SemIR::ImplWitnessAccess>(rhs_inst_id)) {
-      return false;
+      return context().constant_values().Get(rhs_inst_id).is_concrete();
     }
 
     // TODO: We could consider something better than linear search here, such as
@@ -413,11 +409,13 @@ class SubstImplWitnessAccessCallbacks : public SubstInstCallbacks {
         } else {
           rhs_inst_id = search_constraint.rhs_id;
         }
-        return true;
       }
     }
 
-    return false;
+    // Never recurse into ImplWitnessAccess, we don't want to substitute into
+    // FacetTypes found within. We only substitute ImplWitnessAccesses that
+    // appear directly on the RHS.
+    return true;
   }
 
   auto Rebuild(SemIR::InstId /*orig_inst_id*/, SemIR::Inst new_inst) const
@@ -439,6 +437,43 @@ auto ResolveFacetTypeRewriteConstraints(
     return;
   }
 
+  while (true) {
+    bool applied_rewrite = false;
+
+    for (auto& constraint : rewrites) {
+      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);
+      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, rewrites,
+                                                    &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;
+    }
+  }
+
   // We sort the constraints so that we can find different values being written
   // to the same LHS by looking at consecutive rewrite constraints.
   //
@@ -509,43 +544,6 @@ auto ResolveFacetTypeRewriteConstraints(
       next.rhs_id = SemIR::ErrorInst::InstId;
     }
   }
-
-  while (true) {
-    bool applied_rewrite = false;
-
-    for (auto& constraint : rewrites) {
-      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);
-      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, rewrites,
-                                                    &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;
-    }
-  }
 }
 
 }  // namespace Carbon::Check

toolchain/check/testdata/facet/facet_assoc_const.carbon

@@ -206,24 +206,16 @@ fn G(T:! M where .X = () and .Y = ()) {
   F(T);
 }
 
-// --- fail_todo_repeated_with_bitand.carbon
+// --- repeated_with_bitand.carbon
 library "[[@TEST_NAME]]";
 
 interface M { let X:! type; let Y:! type; }
 
-// CHECK:STDERR: fail_todo_repeated_with_bitand.carbon:[[@LINE+4]]:10: error: associated constant `.(M.X)` given two different values `.(M.Y)` and `()` [AssociatedConstantWithDifferentValues]
-// CHECK:STDERR: fn F(T:! (M where .X = .Y) & (M where .X = .Y and .Y = ())) -> T.X {
-// CHECK:STDERR:          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-// CHECK:STDERR:
-fn F(T:! (M where .X = .Y) & (M where .X = .Y and .Y = ())) -> T.X {
+fn F1(T:! (M where .X = .Y) & (M where .X = .Y and .Y = ())) -> T.X {
   return ();
 }
 
-// CHECK:STDERR: fail_todo_repeated_with_bitand.carbon:[[@LINE+4]]:10: error: associated constant `.(M.X)` given two different values `.(M.Y)` and `()` [AssociatedConstantWithDifferentValues]
-// CHECK:STDERR: fn F(T:! (M where .X = .Y and .Y = ()) & (M where .X = .Y)) -> T.X {
-// CHECK:STDERR:          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-// CHECK:STDERR:
-fn F(T:! (M where .X = .Y and .Y = ()) & (M where .X = .Y)) -> T.X {
+fn F2(T:! (M where .X = .Y and .Y = ()) & (M where .X = .Y)) -> T.X {
   return ();
 }
 

toolchain/check/testdata/facet/nested_facet_types.carbon

@@ -43,7 +43,7 @@ interface Z {
 
 fn F(FF:! ((Z where .T = .U) where .T = .U) where .T = .U) {}
 
-// --- fail_todo_nested_facet_types_same_two_associated.carbon
+// --- nested_facet_types_same_two_associated.carbon
 library "[[@TEST_NAME]]";
 
 interface Z {
@@ -52,12 +52,6 @@ interface Z {
   let V:! type;
 }
 
-// TODO: There should not be a diagnostic here.
-//
-// CHECK:STDERR: fail_todo_nested_facet_types_same_two_associated.carbon:[[@LINE+4]]:12: error: associated constant `.(Z.T)` given two different values `.(Z.V)` and `.(Z.U)` [AssociatedConstantWithDifferentValues]
-// CHECK:STDERR: fn F(FF:! ((Z where .T = .U and .U = .V) where .T = .U and .U = .V) where .T = .U and .U = .V) {}
-// CHECK:STDERR:            ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-// CHECK:STDERR:
 fn F(FF:! ((Z where .T = .U and .U = .V) where .T = .U and .U = .V) where .T = .U and .U = .V) {}
 
 // --- fail_nested_facet_types_different.carbon
@@ -183,21 +177,39 @@ interface Z {
 // CHECK:STDERR:
 fn F(FF:! (((Z where .V = {}) where .T = .U) where .S = .U) & (Z where .S = {})) {}
 
-// --- fail_todo_repeated_with_value_available.carbon
+// --- repeated_with_value_available.carbon
 library "[[@TEST_NAME]]";
 
 interface Z { let X:! type; let Y:! type; }
 
-// Verify that the `.Y = ()` does not get applied to `.X = .Y` prematurely, as
-// that would lead to `.X = () and .X = .Y` when combined with the outer `where`
-// expression, which would be an error.
-//
-// TODO: There should be no diagnostic here.
-//
-// CHECK:STDERR: fail_todo_repeated_with_value_available.carbon:[[@LINE+4]]:10: error: associated constant `.(Z.X)` given two different values `()` and `.(Z.Y)` [AssociatedConstantWithDifferentValues]
-// CHECK:STDERR: fn F(T:! ((Z where .Y = ()) where .X = .Y) where .X = .Y) -> T.X {
-// CHECK:STDERR:          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-// CHECK:STDERR:
 fn F(T:! ((Z where .Y = ()) where .X = .Y) where .X = .Y) -> T.X {
   return ();
 }
+
+class C(T:! type) { adapt (); }
+
+fn F1(T:! (Z where .Y = C(()) and .X = C(.Y)) where .X = C(C(()))) -> T.X {
+  return () as C(C(()));
+}
+
+fn F2(T:! ((Z where .Y = C(())) where .X = C(.Y)) where .X = C(C(()))) -> T.X {
+  return () as C(C(()));
+}
+
+fn F3(T:! Z where .Y = C(()) and .X = C(.Y) and .X = C(C(()))) -> T.X {
+  return () as C(C(()));
+}
+
+// --- conflicting_syntax_same_value.carbon
+
+library "[[@TEST_NAME]]";
+
+interface Z { let X:! type; let Y:! type; }
+
+fn F1(T:! ((Z where .Y = ()) where .X = .Y) where .X = ()) -> T.X {
+  return ();
+}
+
+fn F2(T:! ((Z where .Y = ()) where .X = ()) where .X = .Y) -> T.X {
+  return ();
+}