Function chalk_solve::wf::compute_assoc_ty_goal

source ·
fn compute_assoc_ty_goal<I: Interner>(
    db: &dyn RustIrDatabase<I>,
    assoc_ty_id: AssociatedTyValueId<I>,
) -> Option<Goal<I>>
Expand description

Associated type values are special because they can be parametric (independently of the impl), so we issue a special goal which is quantified using the binders of the associated type value, for example in:

trait Foo {
    type Item<'a>: Clone where Self: 'a
}

impl<T> Foo for Box<T> {
    type Item<'a> = Box<&'a T>;
}

we would issue the following subgoal: forall<'a> { WellFormed(Box<&'a T>) }.

Note that there is no binder for T in the above: the goal we generate is expected to be exected in the context of the larger WF goal for the impl, which already has such a binder. So the entire goal for the impl might be:

forall<T> {
    WellFormed(Box<T>) /* this comes from the impl, not this routine */,
    forall<'a> { WellFormed(Box<&'a T>) },
}