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.

Wrote some of my thoughts in https://gist.github.com/lcnr/acb6e4935cdc5821146a5119687c05f0