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

[lcnr]

This issue has been discovered by @steffahn in #135011 (comment)

// 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 rust-lang/trait-system-refactor-initiative#62, answering the question posed in rust-lang/trait-system-refactor-initiative#116 😊

Originally posted by @lcnr in #135011

[lcnr]

Fixing this requires making this cyclic reasoning explicit. To avoid accidental breakage this is blocked on implementing the new cycle semantics. This is blocked on the new trait solver.