Improve error message.

explorer/interpreter/impl_scope.cpp

@@ -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";
           }
         }
       }

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: {{.*}}//usr/local/google/home/richardsmith/carbon-lang/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;
+}