Function compare_method_predicate_entailment

fn compare_method_predicate_entailment<'tcx>(
    tcx: TyCtxt<'tcx>,
    impl_m: AssocItem,
    trait_m: AssocItem,
    impl_trait_ref: TraitRef<'tcx>,
) -> Result<(), ErrorGuaranteed>

This function is best explained by example. Consider a trait with its implementation:

trait Trait<'t, T> {
    // `trait_m`
    fn method<'a, M>(t: &'t T, m: &'a M) -> Self;
}

struct Foo;

impl<'i, 'j, U> Trait<'j, &'i U> for Foo {
    // `impl_m`
    fn method<'b, N>(t: &'j &'i U, m: &'b N) -> Foo { 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_args, that maps the trait type parameters to impl type parameters. This is taken from the impl trait reference:

trait_to_impl_args = {'t => 'j, T => &'i U, Self => Foo}

We create a mapping dummy_args 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_args = {'i => 'i0, U => U0, N => N0 }

Now we can apply placeholder_args 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 N0) -> Foo

We now want to extract and instantiate the type of the trait method and compare it. To do so, we must create a compound instantiation by combining trait_to_impl_args and impl_to_placeholder_args, and also adding a mapping for the method type parameters. We extend the mapping to also include the method parameters.

trait_to_placeholder_args = { T => &'i0 U0, Self => Foo, M => N0 }

Applying this to the trait method type yields:

<'a> fn(t: &'i0 U0, m: &'a N0) -> 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 generic parameters to ensure that all declared bounds are satisfied by the implementation’s method.

We do this by creating a parameter environment which contains a generic parameter corresponding to impl_to_placeholder_args. We then build trait_to_placeholder_args 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.