From 9a90f19c60f2d5ff453ea3fcc2350cadcb727940 Mon Sep 17 00:00:00 2001
From: Dana Jansens <danakj@orodu.net>
Date: Fri, 13 Feb 2026 13:47:48 -0500
Subject: [PATCH] Add two tests for how a non-self require decl in an interface
 connects (#6737)

A non-self require decl in an interface does not mean that a type
implementing that interface also implements the required interface. But
it does mean that whatever the self-type is will implement the required
interface.
---
 .../check/testdata/interface/require.carbon   | 44 +++++++++++++++++++
 1 file changed, 44 insertions(+)

diff --git a/toolchain/check/testdata/interface/require.carbon b/toolchain/check/testdata/interface/require.carbon
index 6ce0b262ed04..0da30abd4f66 100644
--- a/toolchain/check/testdata/interface/require.carbon
+++ b/toolchain/check/testdata/interface/require.carbon
@@ -173,6 +173,50 @@ interface Z {
 }
 //@dump-sem-ir-end
 
+// --- fail_non_self_doesnt_provide_witness_for_self.carbon
+library "[[@TEST_NAME]]";
+
+interface Y {
+  fn YY();
+}
+
+class C(T:! type);
+
+interface Z {
+  require C(Self) impls Y;
+}
+
+fn F(T:! Z) {
+  // This fails because `T impls Z` implies that `C(T) impls Y`, not that
+  // `T impls Y`.
+  // CHECK:STDERR: fail_non_self_doesnt_provide_witness_for_self.carbon:[[@LINE+4]]:3: error: cannot convert type `T` that implements `Z` into type implementing `Y` [ConversionFailureFacetToFacet]
+  // CHECK:STDERR:   T.(Y.YY)();
+  // CHECK:STDERR:   ^~~~~~~~
+  // CHECK:STDERR:
+  T.(Y.YY)();
+}
+
+// --- fail_todo_non_self_provide_witness_for_non_self.carbon
+library "[[@TEST_NAME]]";
+
+interface Y {
+  fn YY();
+}
+
+class C(T:! type);
+
+interface Z {
+  require C(Self) impls Y;
+}
+
+fn F(T:! Z) {
+  // CHECK:STDERR: fail_todo_non_self_provide_witness_for_non_self.carbon:[[@LINE+4]]:3: error: cannot convert type `C(T)` into type implementing `Y` [ConversionFailureTypeToFacet]
+  // CHECK:STDERR:   C(T).(Y.YY)();
+  // CHECK:STDERR:   ^~~~~~~~~~~
+  // CHECK:STDERR:
+  C(T).(Y.YY)();
+}
+
 // --- require_impls_where.carbon
 library "[[@TEST_NAME]]";