Open lcnr opened 1 month ago
concrete example where relying on guidance is difficult:
trait Trait<'a> {
type Assoc;
}
impl Trait<'static> for u32 {
type Assoc = u32;
}
fn bar<'a, T: Trait<'a>>() -> T::Assoc { todo!() }
fn foo<'a>()
where
u32: Trait<'a>,
{
bar::<u32>();
}
Proving u32: Trait<'0>
in foo
has two candidates: the where-bound, constraining '0
to 'a
and the impl, constraining '0
to 'static
. we could return region constraints here.
Normalizing <u32 as Trait<'0>::Assoc
also has two possible candidates (kinda):
'a
, no normalization'static
, normalize to u32
The region constraints from normalization should be the same as from proving the trait bound. We could handle this by disabling the impl candidate here while making sure we don't exclusively return the param_env
candidate constraints
We currently incompletely prefer where-bounds over impls when proving trait goals and while normalizing. This causes multiple issues, so we discussed not applying this guidance immediately but returning them to the caller. At this point guidance would only be applied in the root, e.g. by the
FnCtxt
.issues solved/improved by avoiding eager guidance
text
Returning guidance only works for inference variables from the input, as they have to be constrained by the caller. This means that guidance when normalizing is incredibly hard to solve.
Imagine we have
<Vec<T> as Trait>::Assoc eq <Vec<U> as Trait>::Assoc
with where-bounds normalizing the associated types tou32
and an impl normalizing toT/U
.Then normalizing
<Vec<T> as Trait>::Assoc to ?infer
would result in ambiguity with guidance constraining?infer
tou32
. The actual inference variables remain fully unconstrained however, allowing us to equate them. There's no way we can return this guidance from the alias-relate goal to allow the root to optionally apply it as the root cannot name the unconstrained inference variables created for normalization.