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.

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

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,
}