# coinductive trait semantics issues

## `NormalizesTo` encounters unexpected cycles

Proving `NormalizesTo` via an impl *must not* prove the super trait bounds, we otherwise get unproductive cycles:

trait Super<T> {}
trait Trait: Super<Self::Assoc> {
    type Assoc;
}

impl Super<u32> for u32 {}
impl Trait for u32 {
    type Assoc = u32;
}

- `u32: Trait` requires super trait bound
- `u32: Super<<u32 as Trait>::Assoc>` requires normalizing
- `<u32 as Trait>::Assoc` which would then require
- `u32: Super<<u32 as Trait>::Assoc>` yet again, causing a cycle

It is sound to not check the super trait bounds for `NormalizesTo` goals as we only elaborate trait goals. However, we currently do so by accident when computing `TraitGoalProvenVia` to merge candidates: [source](https://github.com/rust-lang/rust/blob/8c04e395952022a451138dc4dbead6dd6ae65203/compiler/rustc_next_trait_solver/src/solve/normalizes_to/mod.rs#L95-L101).

### Solution

Add a way to probe coinductively which treats the *act of entering a probe* as being coinductive. We should ideally check that this probe doesn't rely on any of the current inference state as this probe should be treated as a separate goal.

## Inductive cycles always resulting in errors is yikes

### Rigid associated types

trait Overflow {
    type Assoc;
}
impl<T> Overflow for T {
    type Assoc = <T as Overflow>::Assoc;
    //~^ ERROR: overflow
}

Normalizing the associated type of that impl results in an inductive cycle. This cycle causes normalization to fail. We still treat the associated item as rigid as `T: Overflow` does hold.

#### Solution

Change the way we compute whether an alias is supposed to be rigid, see https://github.com/rust-lang/rust/pull/136863.

### Ignored where-bounds

trait Foo {
    type Assoc: Copy;
}

fn is_copy<S: Copy>() {}
fn test<T: Foo<Assoc = <T as Foo>::Assoc>>() {
    is_copy::<T::Assoc>();
}

impl<T: Copy> Foo for T {
    type Assoc = Self;
}

fn main() {
    test::<u32>();
}

`T::Assoc` is treated as rigid inside of `test`. We pretty much entirely ignore the `Projection` where-clause as it always errors due to an inductive cycle. This example therefore compiles. This feels somewhat odd.

It interacts with https://github.com/rust-lang/trait-system-refactor-initiative/issues/1:

trait WithAssoc {
    type Assoc;
}

trait Trait<U> {
    fn foo()
    where
        Self: WithAssoc<Assoc = U>;
}

impl<T: WithAssoc> Trait<T::Assoc> for T {
    fn foo() {}
}

fn main() {}

This mostly erases the difference between assumptions and requirements as we no longer overflow when trying to apply a cyclic where-clause :thinking_face: this is very much out of cache for me, so I don't know whether this has deeper implications for the layout of the trait solver.

## This introduces a new item bounds unsoundness

A variation of https://github.com/rust-lang/rust/issues/135246, using cyclic reasoning
when normalizing the environment from the impl definition while checking the item bounds.

trait Trait<R>: Sized {
    type Proof: Trait<R, Proof = Self>;
}

// We need to use indirection here as we otherwise normalize
// `<L::Proof as Trait<R>>::Proof` before recursing into
// `R: Trait<R, Proof = <L::Proof as Trait<R>>::Proof>`.
trait Indir<L: Trait<R>, R>: Trait<R, Proof = <L::Proof as Trait<R>>::Proof> {}
impl<L, R> Indir<L, R> for R
where
    L: Trait<R>,
    R: Trait<R, Proof = <L::Proof as Trait<R>>::Proof>,
{}

impl<L, R> Trait<R> for L
where
    L: Trait<R>,
    R: Indir<L, R>,
 {
    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]);
    println!("{}", s); // ABC
}

## Proving super trait bounds has a very large performance cost

Proving `TyCtxt<'tcx>: Interner` requires proving the super trait bounds `TyCtxt<'tcx>: IrPrint<T>` for 12 different `T`. The impl for which requires proving
- `T: Copy` which requires proving
- the super trait bound `T: Clone` which requires proving
- `TyCtxt<'tcx>: Interner` cycle
- `TyCtxt<'tcx>: Interner` cycle
- `T: Sized`, this requires `<TyCtxt<'tcx> as Interner>::Assoc: Sized` for some of the `T`¹
- normalizing this does not directly cycle with `TyCtxt<'tcx>: Interner` but *also* requires proving `TyCtxt<'tcx>: IrPrint<T>` for the 12 `T` again

¹ proving `Sized` requires proving the `adt_sized_constraint` which is `Some(<I as Interner>::Assoc)` if that associated type is the last field of `T`, even if `Assoc` has a `Sized` item-bound. We only filter sized constraints by looking for `LastField: Sized` bounds in `predicates_of`. We do not look at item bounds or elaborated where-bounds.

#### TODO

We may want to treat some cycles as overflowing instead of hard errors. Likely by having some sort of 3 notions of productivity for cycles:

enum PathKind {
    Unproductive,
    Unknown,
    Productive,
}