the provisional cache incorrectly handles inductive overflow

[lcnr]

see https://github.com/rust-lang/rust/pull/114287/files#r1283008717, need to look into this and fix it.

this also affects ProjectionPredicate(AliasTy { args: [uint::UTerm, uint::UTerm, bit::B1], def_id: DefId(0:936 ~ typenum[0ab6]::private::PrivateSetBit::Output) }, Term::Ty(<uint::UInt<uint::UTerm, bit::B1> as core::ops::Shl<uint::UTerm>>::Output)) in type num, so probably a more general issue with ProjectionPredicates, idk :shrug:

[lcnr]

an affected test is

trait Overflow {
    type Assoc;
}
impl<T> Overflow for T {
    type Assoc = <T as Overflow>::Assoc;
}

trait Trait {}
impl<T: Overflow<Assoc = U>, U> Trait for T {}
struct LocalTy;
impl Trait for LocalTy {}

fn main() {}

results in

unstable result: unstable certainty
original goal: Canonical { value: QueryInput { goal: Goal { predicate: Binder { value: ProjectionPredicate(AliasTy { args: [LocalTy], def_id: DefId(0:4 ~ main[6b46]::Overflow::Assoc) }, Term::Ty(^1_0)), bound_vars: [] }, param_env: ParamEnv { caller_bounds: [], reveal: UserFacing } }, anchor: Bubble, predefined_opaques_in_body: PredefinedOpaques(PredefinedOpaquesData { opaque_types: [] }) }, max_universe: U0, variables: [CanonicalVarInfo { kind: Ty(General(U0)) }] },
original result: Canonical { value: Response { certainty: Yes, var_values: CanonicalVarValues { var_values: [<LocalTy as Overflow>::Assoc] }, external_constraints: ExternalConstraints(ExternalConstraintsData { region_constraints: QueryRegionConstraints { outlives: [], member_constraints: [] }, opaque_types: [] }) }, max_universe: U0, variables: [] }
re-canonicalized goal: Canonical { value: QueryInput { goal: Goal { predicate: Binder { value: ProjectionPredicate(AliasTy { args: [LocalTy], def_id: DefId(0:4 ~ main[6b46]::Overflow::Assoc) }, Term::Ty(<LocalTy as Overflow>::Assoc)), bound_vars: [] }, param_env: ParamEnv { caller_bounds: [], reveal: UserFacing } }, anchor: Bubble, predefined_opaques_in_body: PredefinedOpaques(PredefinedOpaquesData { opaque_types: [] }) }, max_universe: U0, variables: [] }
second response: Ok(Canonical { value: Response { certainty: Maybe(Overflow), var_values: CanonicalVarValues { var_values: [] }, external_constraints: ExternalConstraints(ExternalConstraintsData { region_constraints: QueryRegionConstraints { outlives: [], member_constraints: [] }, opaque_types: [] }) }, max_universe: U0, variables: [] })

[lcnr]

further minimized, currently writing about what's broken here

trait Overflow {
    type Assoc: ?Sized;
}
impl<T: ?Sized> Overflow for T {
    type Assoc = <T as Overflow>::Assoc;
}

fn foo<T: Overflow<Assoc = <() as Overflow>::Assoc + ?Sized>>() {}

fn main() {
    foo::<()>();
}

[lcnr]

the provisional cache does not correctly handle inductive cycles

#![feature(trivial_bounds, marker_trait_attr)]

struct Root;
struct MultipleCandidates;

#[marker]
trait Trait {}
impl Trait for Root
where
    MultipleCandidates: Trait,
    MultipleCandidates: Trait,
{}

impl Trait for MultipleCandidates
where
    Root: Trait,
{}
impl Trait for MultipleCandidates {}

fn impls_trait<T: Trait>() {}

fn main() {
    impls_trait::<Root>();
}

has the proof tree:

Root: Trait proven via impl

• MultipleCandidates: Trait
  • impl overflow
    • Root: Trait (inductive cycle ~> OVERFLOW)
  • impl trivial
    • YES
  • merge responses ~> YES
• MultipleCandidates: Trait
  • still in provisional cache ~> OVERFLOW :exclamation:

to explain the issue a bit more: we keep MultipleCandidates: Trait in the provisional cache, even after proving it, because it depends on something higher up on the stack. However, its result is not OVERFLOW even though it was involved in an inductive cycle

[lcnr]

another example where we get OVERFLOW instead of NoSolution:

#![feature(trivial_bounds, marker_trait_attr)]

struct MultipleCandidates;
struct MultipleNested;
struct DoesNotImpl;

#[marker]
trait Trait {}

impl Trait for MultipleCandidates
where
    MultipleNested: Trait
{}

impl Trait for MultipleCandidates
where
    MultipleNested: Trait,
{}

impl Trait for MultipleNested
where
    MultipleCandidates: Trait,
    DoesNotImpl: Trait,
{}

fn impls_trait<T: Trait>() {}

fn main() {
    impls_trait::<MultipleCandidates>();
}

this time we have 2 identical impls for MultipleCandidates which depend on MultipleNested with 2 nested goals: one inductive cycle, one which is known not to hold. We reject the first MultipleCandidates impl correctly. For the second impl, MultipleNested: Trait is ambig instead of NoSolution

[lcnr]

need to add these as tests/check whether we already added them, then it can be closed

[lcnr]

already added, closing