Function chalk_solve::clauses::dyn_ty::build_dyn_self_ty_clauses

pub(super) fn build_dyn_self_ty_clauses<I: Interner>(
    db: &dyn RustIrDatabase<I>,
    builder: &mut ClauseBuilder<'_, I>,
    self_ty: Ty<I>
)

If the self type S of an Implemented goal is a dyn trait type, we wish to generate program-clauses that indicates that it implements its own traits. For example, a dyn Write type implements Write and so on.

To see how this works, consider as an example the type dyn Fn(&u8). This is really shorthand for dyn for<'a> Fn<(&'a u8), Output = ()>, and we represent that type as something like this:

dyn(exists<T> {
    forall<'a> { Implemented(T: Fn<'a>) },
    forall<'a> { AliasEq(<T as Fn<'a>>::Output, ()) },
})

so what we will do is to generate one program clause for each of the conditions. Thus we get two program clauses:

forall<'a> { Implemented(dyn Fn(&u8): Fn<(&'a u8)>) }

and

forall<'a> { AliasEq(<dyn Fn(&u8) as Fn<'a>>::Output, ()) },