Item-bounds can be used to non-productively prove themselves

This issue has been discovered by @steffahn in https://github.com/rust-lang/rust/issues/135011#issuecomment-2574201519

// We only check that GAT where-clauses of the *trait* while normalizing;
// normalizing `<T as Trait<U>>::Proof` to `U` trivially succeeds.
trait Trait<R>: Sized {
    type Proof: Trait<R, Proof = Self>;
}
impl<L, R> Trait<R> for L {
    // We prove that the impl item is compatible with the trait in the
    // env of the trait, which is pretty much empty.
    //
    // `L: Trait<R>` is trivial
    // `R: Trait<R, Proof = <L::Proof as Trait<R>>::Proof>` normalizes to
    // `R: Trait<R, Proof = <R as Trait<R>>::Proof>` normalizes to
    // `R: Trait<R, Proof = R>` is trivial
    //
    // Proving the item-bound holds assumes the *impl where-bounds*.
    // For this we normalize the where-bound `R: Trait<R, Proof = <L::Proof as Trait<R>>::Proof>`
    // by using the item-bound of `L::Proof`: `R: Trait<R, Proof = L>` 💀¹. Proving the
    // item-bound of `<L as Trait<R>>::Proof` is now trivial.
    type Proof
        = R
    where
        L: Trait<R>,
        R: Trait<R, Proof = <L::Proof as Trait<R>>::Proof>;
}
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]);
    println!("{}", s); // ABC
}

What's happening at ¹ is that proving that the item-bounds of an associated type is able
to assume the item-bounds of exactly that associated type. This is non-productive cyclic reasoning.

You've found a new way to exploit https://github.com/rust-lang/trait-system-refactor-initiative/issues/62, answering the question posed in https://github.com/rust-lang/trait-system-refactor-initiative/issues/116 😊

Originally posted by @lcnr in #135011

Start with the Rust reproducer in this issue and read the linked trait-system refactor discussions #62 and #116, along with issue #135011. Trace associated-type item-bound normalization and define done as preventing this non-productive cyclic reasoning without rejecting valid bounds; the payload names no specific source file or test.