From 68f2802c08ab717381b7bfc4aeedff0b53a222fc Mon Sep 17 00:00:00 2001
From: lcnr <rust@lcnr.de>
Date: Thu, 13 Feb 2025 11:03:45 +0100
Subject: [PATCH] add variation of the #135246 unsoundness

---
 ...bound-via-impl-where-clause.current.stderr | 25 +++++++
 ...em-bound-via-impl-where-clause.next.stderr | 69 +++++++++++++++++++
 .../item-bound-via-impl-where-clause.rs       | 30 ++++++++
 3 files changed, 124 insertions(+)
 create mode 100644 tests/ui/traits/next-solver/cycles/coinduction/item-bound-via-impl-where-clause.current.stderr
 create mode 100644 tests/ui/traits/next-solver/cycles/coinduction/item-bound-via-impl-where-clause.next.stderr
 create mode 100644 tests/ui/traits/next-solver/cycles/coinduction/item-bound-via-impl-where-clause.rs

diff --git a/tests/ui/traits/next-solver/cycles/coinduction/item-bound-via-impl-where-clause.current.stderr b/tests/ui/traits/next-solver/cycles/coinduction/item-bound-via-impl-where-clause.current.stderr
new file mode 100644
index 0000000000000..87dd66a72e143
--- /dev/null
+++ b/tests/ui/traits/next-solver/cycles/coinduction/item-bound-via-impl-where-clause.current.stderr
@@ -0,0 +1,25 @@
+error[E0275]: overflow evaluating the requirement `<Vec<u8> as Trait<String>>::Proof == _`
+  --> $DIR/item-bound-via-impl-where-clause.rs:24:21
+   |
+LL |     let s: String = transmute::<_, String>(vec![65_u8, 66, 67]);
+   |                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |
+note: required for `Vec<u8>` to implement `Trait<String>`
+  --> $DIR/item-bound-via-impl-where-clause.rs:14:12
+   |
+LL | impl<L, R> Trait<R> for L
+   |            ^^^^^^^^     ^
+...
+LL |     R: Trait<R, Proof = <L::Proof as Trait<R>>::Proof>
+   |                 ------------------------------------- unsatisfied trait bound introduced here
+   = note: 1 redundant requirement hidden
+   = note: required for `Vec<u8>` to implement `Trait<String>`
+note: required by a bound in `transmute`
+  --> $DIR/item-bound-via-impl-where-clause.rs:22:17
+   |
+LL | fn transmute<L: Trait<R>, R>(r: L) -> <L::Proof as Trait<R>>::Proof { r }
+   |                 ^^^^^^^^ required by this bound in `transmute`
+
+error: aborting due to 1 previous error
+
+For more information about this error, try `rustc --explain E0275`.
diff --git a/tests/ui/traits/next-solver/cycles/coinduction/item-bound-via-impl-where-clause.next.stderr b/tests/ui/traits/next-solver/cycles/coinduction/item-bound-via-impl-where-clause.next.stderr
new file mode 100644
index 0000000000000..e55a17065c9c1
--- /dev/null
+++ b/tests/ui/traits/next-solver/cycles/coinduction/item-bound-via-impl-where-clause.next.stderr
@@ -0,0 +1,69 @@
+error[E0271]: type mismatch resolving `<String as Trait<String>>::Proof normalizes-to String`
+  --> $DIR/item-bound-via-impl-where-clause.rs:24:33
+   |
+LL |     let s: String = transmute::<_, String>(vec![65_u8, 66, 67]);
+   |                                 ^ types differ
+   |
+note: required for `String` to implement `Trait<String>`
+  --> $DIR/item-bound-via-impl-where-clause.rs:14:12
+   |
+LL | impl<L, R> Trait<R> for L
+   |            ^^^^^^^^     ^
+...
+LL |     R: Trait<R, Proof = <L::Proof as Trait<R>>::Proof>
+   |                 ------------------------------------- unsatisfied trait bound introduced here
+   = note: 2 redundant requirements hidden
+   = note: required for `Vec<u8>` to implement `Trait<String>`
+note: required by a bound in `transmute`
+  --> $DIR/item-bound-via-impl-where-clause.rs:22:17
+   |
+LL | fn transmute<L: Trait<R>, R>(r: L) -> <L::Proof as Trait<R>>::Proof { r }
+   |                 ^^^^^^^^ required by this bound in `transmute`
+
+error[E0271]: type mismatch resolving `<String as Trait<String>>::Proof normalizes-to String`
+  --> $DIR/item-bound-via-impl-where-clause.rs:24:21
+   |
+LL |     let s: String = transmute::<_, String>(vec![65_u8, 66, 67]);
+   |                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ types differ
+   |
+note: required for `String` to implement `Trait<String>`
+  --> $DIR/item-bound-via-impl-where-clause.rs:14:12
+   |
+LL | impl<L, R> Trait<R> for L
+   |            ^^^^^^^^     ^
+...
+LL |     R: Trait<R, Proof = <L::Proof as Trait<R>>::Proof>
+   |                 ------------------------------------- unsatisfied trait bound introduced here
+   = note: 1 redundant requirement hidden
+   = note: required for `Vec<u8>` to implement `Trait<String>`
+note: required by a bound in `Trait`
+  --> $DIR/item-bound-via-impl-where-clause.rs:11:17
+   |
+LL | trait Trait<R>: Sized {
+   |                 ^^^^^ required by this bound in `Trait`
+
+error[E0271]: type mismatch resolving `<String as Trait<String>>::Proof == _`
+  --> $DIR/item-bound-via-impl-where-clause.rs:24:21
+   |
+LL |     let s: String = transmute::<_, String>(vec![65_u8, 66, 67]);
+   |                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ type mismatch resolving `<String as Trait<String>>::Proof == _`
+   |
+note: types differ
+  --> $DIR/item-bound-via-impl-where-clause.rs:20:11
+   |
+LL |         = R;
+   |           ^
+note: required for `String` to implement `Trait<String>`
+  --> $DIR/item-bound-via-impl-where-clause.rs:14:12
+   |
+LL | impl<L, R> Trait<R> for L
+   |            ^^^^^^^^     ^
+...
+LL |     R: Trait<R, Proof = <L::Proof as Trait<R>>::Proof>
+   |                 ------------------------------------- unsatisfied trait bound introduced here
+   = note: 2 redundant requirements hidden
+   = note: required for `Vec<u8>` to implement `Trait<String>`
+
+error: aborting due to 3 previous errors
+
+For more information about this error, try `rustc --explain E0271`.
diff --git a/tests/ui/traits/next-solver/cycles/coinduction/item-bound-via-impl-where-clause.rs b/tests/ui/traits/next-solver/cycles/coinduction/item-bound-via-impl-where-clause.rs
new file mode 100644
index 0000000000000..632858f0cf818
--- /dev/null
+++ b/tests/ui/traits/next-solver/cycles/coinduction/item-bound-via-impl-where-clause.rs
@@ -0,0 +1,30 @@
+//@ revisions: current next
+//@ ignore-compare-mode-next-solver (explicit revisions)
+//@[next] compile-flags: -Znext-solver
+
+// A variation of #135246 where the cyclic bounds are part of
+// the impl instead of the impl associated item.
+//
+// This has never been an unsound and fails with a non-productive
+// cycle when normalizing the expected term of the projection goal.
+
+trait Trait<R>: Sized {
+    type Proof: Trait<R, Proof = Self>;
+}
+impl<L, R> Trait<R> for L
+where
+    L: Trait<R>,
+    R: Trait<R, Proof = <L::Proof as Trait<R>>::Proof>
+ {
+    type Proof
+        = R;
+}
+fn transmute<L: Trait<R>, R>(r: L) -> <L::Proof as Trait<R>>::Proof { r }
+fn main() {
+    let s: String = transmute::<_, String>(vec![65_u8, 66, 67]);
+    //[current]~^ ERROR overflow evaluating the requirement
+    //[next]~^^ ERROR type mismatch resolving `<String as Trait<String>>::Proof normalizes-to String`
+    //[next]~| ERROR type mismatch resolving `<String as Trait<String>>::Proof normalizes-to String`
+    //[next]~| ERROR type mismatch resolving `<String as Trait<String>>::Proof == _`
+    println!("{}", s);
+}