Skip to content

implied bounds: explicitly state which types are assumed to be wf #100676

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Aug 22, 2022
Merged
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
compare_predicate_entailment move comment
  • Loading branch information
lcnr committed Aug 17, 2022
commit f57e6fa453341a8012f0cdf951e0cd10f5e58ab0
129 changes: 66 additions & 63 deletions compiler/rustc_typeck/src/check/compare_method.rs
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,72 @@ pub(crate) fn compare_impl_method<'tcx>(
}
}

/// 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.
fn compare_predicate_entailment<'tcx>(
tcx: TyCtxt<'tcx>,
impl_m: &ty::AssocItem,
Expand All @@ -96,69 +162,6 @@ fn compare_predicate_entailment<'tcx>(
},
);

// This code is best explained by example. Consider a trait:
//
// trait Trait<'t, T> {
// fn method<'a, M>(t: &'t T, m: &'a M) -> Self;
// }
//
// And an impl:
//
// impl<'i, 'j, U> Trait<'j, &'i U> for Foo {
// fn method<'b, N>(t: &'j &'i U, m: &'b N) -> Foo;
// }
//
// We wish to decide if those two method types are compatible.
//
// 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 in
// a fresh FulfillmentCtxt, and invoke select_all_or_error.

// Create mapping from impl to placeholder.
let impl_to_placeholder_substs = InternalSubsts::identity_for_item(tcx, impl_m.def_id);

Expand Down