AliasBound + ParamEnv candidate eq modulo regions

[lcnr]

fixed by preferring where-bounds over alias-bounds

pub trait QueryDb<'d>: Sized {
    type DynDb: HasQueryGroup<Self::Group>;

    type Group: QueryGroup;
}

pub trait QueryGroup: Sized {
    type DynDb: HasQueryGroup<Self>;
}

pub trait HasQueryGroup<G>
where
    G: QueryGroup,
{
}

pub trait EqualDynDb<'d, IQ: QueryDb<'d>>: QueryDb<'d> {}

impl<'d, IQ, Q> EqualDynDb<'d, IQ> for Q
where
    Q: QueryDb<'d, DynDb = IQ::DynDb, Group = IQ::Group>,
    Q::DynDb: HasQueryGroup<IQ::Group>,
    IQ: QueryDb<'d>,
{
}

fn main() {}

results in

error[E0283]: type annotations needed: cannot satisfy `Q: EqualDynDb<'d, IQ>`
  --> src/main.rs:28:40
   |
28 | impl<'d, IQ, Q> EqualDynDb<'d, IQ> for Q
   |                                        ^
   |
   = note: cannot satisfy `Q: EqualDynDb<'d, IQ>`
   = help: the trait `EqualDynDb<'_, IQ>` is implemented for `Q`

error: aborting due to 1 previous error

minimized from salsa

feels related to #89 but also affects nightly

[lcnr]

minimized

trait Bound<'a> {}
trait Trait<'a> {
    type Assoc: Bound<'a>;
}

fn foo<'a, T>()
where
    T: Trait<'a>,
    <T as Trait<'a>>::Assoc: Bound<'a>,
{}

checking that foo is wf tries to prove exists<'0, '1> <T as Trait<'0>>::Assoc: Bound<'1> after uniquification. The AliasBound candidate ends up requiring '0 == '1 while the where bound candidate equates '0 and '1 with the lts from the <T as Trait<'a>>::Assoc: Bound<'a>, where-bound, which are also uniquified to different lifetimes: <T as Trait<'2>>::Assoc: Bound<'3>

Thanks to @BoxyUwU for actually figuring this out ❤️

[lcnr]

notes:

We first considered that this should be solvable by not uniquifying regions in the ParamEnv, only doing so for the goal. This does not solve this issue, as inside of the query we'd still have a where bound <T as Trait<'env_a>>::Assoc: Bound<'env_a> for a goal <T as Trait<'0>>::Assoc: Bound<'1>. So both the AliasBound and the ParamEnv goal still result in non-trivial region constraints.

We already dedup equal clauses in the param env, which is why T: Trait<'a> + Trait<'a> does not result in ambiguity and neither does T: Trait<'a> + SuperTrait<'a>. We could therefore use structural equality checks to throw out where-bounds when constructing the param-env if they are equal to alias-bounds of their self-type. This must only be done if the self-type is a rigid alias. It does add some complexity.

Alternatively: open a PR to salsa removing the trivial-bound 😁 and check whether this pattern is more widespread

[lcnr]

further thought: this pattern is likely also possible when checking that the impl item where-bounds are implied by the instantiated trait item where-bounds. should get a test for that. In this case it is not possible to simply remove the trivial where-bound

[lcnr]

from @BoxyUwU this affects compute_predicate_entailment as well https://rust.godbolt.org/z/En4s6W1qd

[BoxyUwU]

We should make sure we write a test that alias bounds from a nested alias as the self type also are factored into this (i.e. decide whether we want to filter those out too or not and then have a test that will fail if we change that behaviour). Something like <<T as OtherRigid<'a>>::OtherAssoc> as Rigid>::Assoc: Bound<'a> where OtherRigid is defined with a type OtherAssoc: Rigid<Assoc: Bound<'a>>

[BoxyUwU]

Another noteworthy thing is that the solver doesnt assemble alias bounds for non rigid aliases so if we have a where clause like <T as Alias<'a>>::Assoc: Bound<'a> where the alias is normalizeable and Assoc has an item bound of Bound<'a> then filtering that where clause out is removing a bound that is not actually something that already gets assembled. The normalized form ought to just be able to prove the Bound<'a> on anyway as we would have had to have done that in an env with where clauses that all hold if <T as Alias<'a>>::Assoc is wf.

• It is unclear to me whether we want the param_env query (or wherever we do this filtering) to be figuring out whether aliases in the env are rigid or not as this would require actually running solver logic with the unfiltered env which means that we do not always run the solver with these bounds removed
• It probably is possible to write an example where the explicit bound on the non rigid alias is not able to be proved on the normalized form due to incompleteness(?).

[lcnr]

This impacts core:

trait Pattern<'a> {
    type Searcher: Searcher<'a>;
}

trait Searcher<'a> {}

fn rsplit_terminator<'a, P>()
where
    P: Pattern<'a>,
    P::Searcher: Searcher<'a>,
{
}