Function chalk_solve::clauses::dyn_ty::build_dyn_self_ty_clauses
source ยท pub(super) fn build_dyn_self_ty_clauses<I: Interner>(
db: &dyn RustIrDatabase<I>,
builder: &mut ClauseBuilder<'_, I>,
self_ty: Ty<I>,
)
Expand description
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, ()) },