Check equality constraints when checking whether a constraint is satisfied

explorer/interpreter/impl_scope.cpp

@@ -115,7 +115,7 @@ auto ImplScope::Resolve(Nonnull<const Value*> constraint_type,
       }
       Bindings local_bindings = bindings;
       local_bindings.Add(constraint->self_binding(), impl_type, witness);
-      SingleStepEqualityContext equality_ctx(&type_checker, this);
+      SingleStepEqualityContext equality_ctx(this);
       for (auto& equal : equals) {
         auto it = equal.values.begin();
         Nonnull<const Value*> first =
@@ -124,8 +124,9 @@ auto ImplScope::Resolve(Nonnull<const Value*> constraint_type,
           Nonnull<const Value*> current =
               type_checker.Substitute(local_bindings, *it);
           if (!ValueEqual(first, current, &equality_ctx)) {
-            return ProgramError(source_loc) << "could not determine that "
-                                            << *first << " == " << *current;
+            return ProgramError(source_loc)
+                   << "constraint requires that " << *first
+                   << " == " << *current << ", which is not known to be true";
           }
         }
       }
@@ -262,46 +263,7 @@ void ImplScope::Print(llvm::raw_ostream& out) const {
 auto SingleStepEqualityContext::VisitEqualValues(
     Nonnull<const Value*> value,
     llvm::function_ref<bool(Nonnull<const Value*>)> visitor) const -> bool {
-  if (auto trace_stream = type_checker_->trace_stream()) {
-    **trace_stream << "looking for values equal to " << *value << " in\n"
-                   << *impl_scope_;
-  }
-
-  if (!impl_scope_->VisitEqualValues(value, visitor)) {
-    return false;
-  }
-
-  // Also look up and visit the corresponding impl if this is an associated
-  // constant.
-  // TODO: Is this necessary?
-  if (auto* assoc = dyn_cast<AssociatedConstant>(value)) {
-    // Perform an impl lookup to see if we can resolve this constant.
-    // The source location doesn't matter, we're discarding the diagnostics.
-    if (auto* impl_witness = dyn_cast<ImplWitness>(&assoc->witness())) {
-      // Instantiate the impl to find the concrete constraint it implements.
-      Nonnull<const ConstraintType*> constraint =
-          impl_witness->declaration().constraint_type();
-      constraint = cast<ConstraintType>(
-          type_checker_->Substitute(impl_witness->bindings(), constraint));
-      if (auto trace_stream = type_checker_->trace_stream()) {
-        **trace_stream << "found constraint " << *constraint
-                       << " for associated constant " << *assoc << "\n";
-      }
-
-      // Look for the value of this constant within that constraint.
-      if (!constraint->VisitEqualValues(value, visitor)) {
-        return false;
-      }
-    } else {
-      if (auto trace_stream = type_checker_->trace_stream()) {
-        **trace_stream << "Could not resolve associated constant " << *assoc
-                       << ": witness " << assoc->witness()
-                       << " depends on a generic parameter\n";
-      }
-    }
-  }
-
-  return true;
+  return impl_scope_->VisitEqualValues(value, visitor);
 }
 
 }  // namespace Carbon

explorer/interpreter/impl_scope.h

@@ -158,20 +158,18 @@ class ImplScope {
 // scope.
 struct SingleStepEqualityContext : public EqualityContext {
  public:
-  SingleStepEqualityContext(Nonnull<const TypeChecker*> type_checker,
-                            Nonnull<const ImplScope*> impl_scope)
-      : type_checker_(type_checker), impl_scope_(impl_scope) {}
+  SingleStepEqualityContext(Nonnull<const ImplScope*> impl_scope)
+      : impl_scope_(impl_scope) {}
 
   // Visits the values that are equal to the given value and a single step away
-  // according to an equality constraint that is either scope or within a final
-  // impl corresponding to an associated constant. Stops and returns `false` if
-  // the visitor returns `false`, otherwise returns `true`.
+  // according to an equality constraint that is in the given impl scope. Stops
+  // and returns `false` if the visitor returns `false`, otherwise returns
+  // `true`.
   auto VisitEqualValues(Nonnull<const Value*> value,
                         llvm::function_ref<bool(Nonnull<const Value*>)> visitor)
       const -> bool override;
 
  private:
-  Nonnull<const TypeChecker*> type_checker_;
   Nonnull<const ImplScope*> impl_scope_;
 };
 

explorer/interpreter/interpreter.cpp

@@ -736,7 +736,7 @@ auto Interpreter::Convert(Nonnull<const Value*> value,
           return arena_->New<NominalClassValue>(inst_dest, value);
         }
         default: {
-          CARBON_CHECK(isa<VariableType, AssociatedConstant>(destination_type))
+          CARBON_CHECK(IsValueKindDependent(destination_type))
               << "Can't convert value " << *value << " to type "
               << *destination_type;
           return value;
@@ -771,7 +771,7 @@ auto Interpreter::Convert(Nonnull<const Value*> value,
           break;
         }
         default: {
-          CARBON_CHECK(isa<VariableType, AssociatedConstant>(destination_type))
+          CARBON_CHECK(IsValueKindDependent(destination_type))
               << "Can't convert value " << *value << " to type "
               << *destination_type;
           return value;

explorer/interpreter/type_checker.h

@@ -79,11 +79,6 @@ class TypeChecker {
                                    int impl_offset) const
       -> Nonnull<const Witness*>;
 
-  // Returns the trace stream, if one was provided.
-  auto trace_stream() const -> std::optional<Nonnull<llvm::raw_ostream*>> {
-    return trace_stream_;
-  }
-
  private:
   class ConstraintTypeBuilder;
   class SubstitutedGenericBindings;

explorer/interpreter/value.cpp

@@ -632,8 +632,7 @@ auto TypeEqual(Nonnull<const Value*> t1, Nonnull<const Value*> t2,
     return true;
   }
   if (t1->kind() != t2->kind()) {
-    if (isa<VariableType, AssociatedConstant>(t1) ||
-        isa<VariableType, AssociatedConstant>(t2)) {
+    if (IsValueKindDependent(t1) || IsValueKindDependent(t2)) {
       return ValueEqual(t1, t2, equality_ctx);
     }
     return false;
@@ -946,15 +945,15 @@ auto ValueEqual(Nonnull<const Value*> v1, Nonnull<const Value*> v2,
   // associated constant; otherwise we should be able to do better by looking
   // at the structures of the values.
   if (equality_ctx) {
-    if (isa<VariableType, AssociatedConstant>(v1)) {
+    if (IsValueKindDependent(v1)) {
       auto visitor = [&](Nonnull<const Value*> maybe_v2) {
         return !ValueStructurallyEqual(v2, maybe_v2, equality_ctx);
       };
       if (!(*equality_ctx)->VisitEqualValues(v1, visitor)) {
         return true;
       }
     }
-    if (isa<VariableType, AssociatedConstant>(v2)) {
+    if (IsValueKindDependent(v2)) {
       auto visitor = [&](Nonnull<const Value*> maybe_v1) {
         return !ValueStructurallyEqual(v1, maybe_v1, equality_ctx);
       };

explorer/interpreter/value.h

@@ -121,6 +121,13 @@ class Value {
   const Kind kind_;
 };
 
+// Returns whether the fully-resolved kind that this value will eventually have
+// is currently unknown, because it depends on a generic parameter.
+inline bool IsValueKindDependent(Nonnull<const Value*> type) {
+  return type->kind() == Value::Kind::VariableType ||
+         type->kind() == Value::Kind::AssociatedConstant;
+}
+
 // Base class for types holding contextual information by which we can
 // determine whether values are equal.
 class EqualityContext {

explorer/testdata/assoc_const/fail_different_type.carbon

@@ -21,7 +21,7 @@ external impl Bad as Iface where .T = Bad {}
 
 fn Main() -> i32 {
   F(Good);
-  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_different_type.carbon:[[@LINE+1]]: could not determine that class Bad == i32
+  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_different_type.carbon:[[@LINE+1]]: constraint requires that class Bad == i32, which is not known to be true
   F(Bad);
   return 0;
 }

explorer/testdata/assoc_const/fail_different_value.carbon

@@ -21,7 +21,7 @@ external impl Bad as Iface where .N = 4 {}
 
 fn Main() -> i32 {
   F(Good);
-  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_different_value.carbon:[[@LINE+1]]: could not determine that 4 == 5
+  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_different_value.carbon:[[@LINE+1]]: constraint requires that 4 == 5, which is not known to be true
   F(Bad);
   return 0;
 }

explorer/testdata/assoc_const/fail_equal_indirectly.carbon

@@ -0,0 +1,38 @@
+// 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
+//
+// RUN: %{not} %{explorer} %s | %{FileCheck-strict} %s
+// RUN: %{not} %{explorer-trace} %s | %{FileCheck-allow-unmatched} %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+interface Iface {
+  let T:! Type;
+}
+
+fn F[T:! Iface where .T == i32](x: T) {}
+
+class Class {
+  impl as Iface where .T = i32 {}
+}
+
+// OK, constraint on `F` rewritten to `T:! Iface where U == i32`, which we can
+// prove from the constraint on `U`.
+fn G[U:! Type where .Self == i32, T:! Iface where .T = U](x: T, y: U) {
+  F(x);
+}
+
+// Not OK: would require looking through two levels of `==`.
+fn H[U:! Type where .Self == i32, T:! Iface where .T == U](x: T, y: U) {
+  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_equal_indirectly.carbon:[[@LINE+1]]: constraint requires that (T).(Iface.T) == i32, which is not known to be true
+  F(x);
+}
+
+fn Main() -> i32 {
+  var x: Class = {};
+  G(x, 0);
+  H(x, 0);
+  return 0;
+}

explorer/testdata/assoc_const/fail_equal_to_dependent_type.carbon

@@ -0,0 +1,35 @@
+// 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
+//
+// RUN: %{not} %{explorer} %s | %{FileCheck-strict} %s
+// RUN: %{not} %{explorer-trace} %s | %{FileCheck-allow-unmatched} %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+interface Iface {
+  let T:! Type;
+}
+
+fn F[T:! Iface where .T == i32](x: T) {}
+
+fn G[T:! Iface where .T == i32](x: T) {
+  F(x);
+}
+
+fn H[T:! Iface](x: T) {
+  // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_equal_to_dependent_type.carbon:[[@LINE+1]]: constraint requires that (T).(Iface.T) == i32, which is not known to be true
+  F(x);
+}
+
+class Class {
+  impl as Iface where .T = i32 {}
+}
+
+fn Main() -> i32 {
+  var x: Class = {};
+  G(x);
+  H(x);
+  return 0;
+}