Implied bounds
We currently add implied region bounds to avoid explicit annotations. e.g.
fn foo<'a, T>(x: &'a T) can freely assume that T: 'a holds without specifying it.
There are two kinds of implied bounds: explicit and implicit. Explicit implied bounds
get added to the fn predicates_of of the relevant item while implicit ones are
handled... well... implicitly.
explicit implied bounds
The explicit implied bounds are computed in fn inferred_outlives_of. Only ADTs and
lazy type aliases have explicit implied bounds which are computed via a fixpoint algorithm
in the fn inferred_outlives_crate query.
We use fn insert_required_predicates_to_be_wf on all fields of all ADTs in the crate.
This function computes the outlives bounds for each component of the field using a
separate implementation.
For ADTs, trait objects, and associated types the initially required predicates are
computed in fn check_explicit_predicates. This simply uses fn explicit_predicates_of
without elaborating them.
Region predicates are added via fn insert_outlives_predicate. This function takes
an outlives predicate, decomposes it and adds the components as explicit predicates only
if the outlived region is a region parameter. It does not add 'static requirements.
implicit implied bounds
As we are unable to handle implications in binders yet, we cannot simply add the outlives requirements of impls and functions as explicit predicates.
using implicit implied bounds as assumptions
These bounds are not added to the ParamEnv of the affected item itself. For lexical
region resolution they are added using fn OutlivesEnvironment::with_bounds.
Similarly,during MIR borrowck we add them using
fn UniversalRegionRelationsBuilder::add_implied_bounds.
We add implied bounds for the function signature and impl header in MIR borrowck.
Outside of MIR borrowck we add the outlives requirements for the types returned by the
fn assumed_wf_types query.
The assumed outlives constraints for implicit bounds are computed using the
fn implied_outlives_bounds query. This directly
extracts the required outlives bounds from fn wf::obligations.
MIR borrowck adds the outlives constraints for both the normalized and unnormalized types, lexical region resolution only uses the unnormalized types.
proving implicit implied bounds
As the implicit implied bounds are not included in fn predicates_of we have to
separately make sure they actually hold. We generally handle this by checking that
all used types are well formed by emitting WellFormed predicates.
We cannot emit WellFormed predicates when instantiating impls, as this would result
in - currently often inductive - trait solver cycles. We also do not emit constraints
involving higher ranked regions as we're lacking the implied bounds from their binder.
This results in multiple unsoundnesses: