fn compare_predicate_entailment<'tcx>(
tcx: TyCtxt<'tcx>,
impl_m: &AssocItem,
impl_m_span: Span,
trait_m: &AssocItem,
impl_trait_ref: TraitRef<'tcx>
) -> Result<(), ErrorGuaranteed>
Expand description
This function is best explained by example. Consider a trait:
trait Trait<'t, T> {
// `trait_m`
fn method<'a, M>(t: &'t T, m: &'a M) -> Self;
}
And an impl:
impl<'i, 'j, U> Trait<'j, &'i U> for Foo {
// `impl_m`
fn method<'b, N>(t: &'j &'i U, m: &'b N) -> Foo;
}
We wish to decide if those two method types are compatible.
For this we have to show that, assuming the bounds of the impl hold, the
bounds of trait_m
imply the bounds of impl_m
.
We start out with trait_to_impl_substs
, that maps the trait
type parameters to impl type parameters. This is taken from the
impl trait reference:
trait_to_impl_substs = {'t => 'j, T => &'i U, Self => Foo}
We create a mapping dummy_substs
that maps from the impl type
parameters to fresh types and regions. For type parameters,
this is the identity transform, but we could as well use any
placeholder types. For regions, we convert from bound to free
regions (Note: but only early-bound regions, i.e., those
declared on the impl or used in type parameter bounds).
impl_to_placeholder_substs = {'i => 'i0, U => U0, N => N0 }
Now we can apply placeholder_substs
to the type of the impl method
to yield a new function type in terms of our fresh, placeholder
types:
<'b> fn(t: &'i0 U0, m: &'b) -> Foo
We now want to extract and substitute the type of the trait
method and compare it. To do so, we must create a compound
substitution by combining trait_to_impl_substs
and
impl_to_placeholder_substs
, and also adding a mapping for the method
type parameters. We extend the mapping to also include
the method parameters.
trait_to_placeholder_substs = { T => &'i0 U0, Self => Foo, M => N0 }
Applying this to the trait method type yields:
<'a> fn(t: &'i0 U0, m: &'a) -> Foo
This type is also the same but the name of the bound region ('a
vs 'b
). However, the normal subtyping rules on fn types handle
this kind of equivalency just fine.
We now use these substitutions to ensure that all declared bounds are satisfied by the implementation’s method.
We do this by creating a parameter environment which contains a
substitution corresponding to impl_to_placeholder_substs
. We then build
trait_to_placeholder_substs
and use it to convert the predicates contained
in the trait_m
generics to the placeholder form.
Finally we register each of these predicates as an obligation and check that they hold.