From a539558158fd35b28a526671dcf41ffc113c4faa Mon Sep 17 00:00:00 2001 From: lcnr Date: Thu, 29 Feb 2024 10:46:28 +0100 Subject: [PATCH] add implied bounds doc (#1915) * add implied bounds doc * lazy type aliases also have explicit implied bounds --- src/SUMMARY.md | 1 + src/traits/implied-bounds.md | 84 ++++++++++++++++++++++++++++++++++++ 2 files changed, 85 insertions(+) create mode 100644 src/traits/implied-bounds.md diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 82e0d79aa..8140dc9f0 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -120,6 +120,7 @@ - [Interactions with turbofishing](./turbofishing-and-early-late-bound.md) - [Higher-ranked trait bounds](./traits/hrtb.md) - [Caching subtleties](./traits/caching.md) + - [Implied bounds](./traits/implied-bounds.md) - [Specialization](./traits/specialization.md) - [Chalk-based trait solving](./traits/chalk.md) - [Lowering to logic](./traits/lowering-to-logic.md) diff --git a/src/traits/implied-bounds.md b/src/traits/implied-bounds.md new file mode 100644 index 000000000..911553ad3 --- /dev/null +++ b/src/traits/implied-bounds.md @@ -0,0 +1,84 @@ +# 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][nostatic]. + + [`fn inferred_outlives_of`]: https://github.com/rust-lang/rust/blob/5b8bc568d28b2e922290c9a966b3231d0ce9398b/compiler/rustc_hir_analysis/src/outlives/mod.rs#L20 + [`fn inferred_outlives_crate`]: https://github.com/rust-lang/rust/blob/5b8bc568d28b2e922290c9a966b3231d0ce9398b/compiler/rustc_hir_analysis/src/outlives/mod.rs#L83 + [`fn insert_required_predicates_to_be_wf`]: https://github.com/rust-lang/rust/blob/5b8bc568d28b2e922290c9a966b3231d0ce9398b/compiler/rustc_hir_analysis/src/outlives/implicit_infer.rs#L89 + [`fn check_explicit_predicates`]: https://github.com/rust-lang/rust/blob/5b8bc568d28b2e922290c9a966b3231d0ce9398b/compiler/rustc_hir_analysis/src/outlives/implicit_infer.rs#L238 + [`fn insert_outlives_predicate`]: https://github.com/rust-lang/rust/blob/5b8bc568d28b2e922290c9a966b3231d0ce9398b/compiler/rustc_hir_analysis/src/outlives/utils.rs#L15 + [nostatic]: https://github.com/rust-lang/rust/blob/5b8bc568d28b2e922290c9a966b3231d0ce9398b/compiler/rustc_hir_analysis/src/outlives/utils.rs#L159-L165 + +## 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][mir]. +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`][boundsfromty]. + +MIR borrowck adds the outlives constraints for both the normalized and unnormalized types, +lexical region resolution [only uses the unnormalized types][notnorm]. + +[`fn OutlivesEnvironment::with_bounds`]: https://github.com/rust-lang/rust/blob/5b8bc568d28b2e922290c9a966b3231d0ce9398b/compiler/rustc_infer/src/infer/outlives/env.rs#L90-L97 +[`fn UniversalRegionRelationsBuilder::add_implied_bounds`]: https://github.com/rust-lang/rust/blob/5b8bc568d28b2e922290c9a966b3231d0ce9398b/compiler/rustc_borrowck/src/type_check/free_region_relations.rs#L316 +[mir]: https://github.com/rust-lang/rust/blob/91cae1dcdcf1a31bd8a92e4a63793d65cfe289bb/compiler/rustc_borrowck/src/type_check/free_region_relations.rs#L258-L332 +[`fn assumed_wf_types`]: https://github.com/rust-lang/rust/blob/5b8bc568d28b2e922290c9a966b3231d0ce9398b/compiler/rustc_ty_utils/src/implied_bounds.rs#L21 +[`fn implied_outlives_bounds`]: https://github.com/rust-lang/rust/blob/5b8bc568d28b2e922290c9a966b3231d0ce9398b/compiler/rustc_traits/src/implied_outlives_bounds.rs#L18C4-L18C27 +[boundsfromty]: https://github.com/rust-lang/rust/blob/5b8bc568d28b2e922290c9a966b3231d0ce9398b/compiler/rustc_trait_selection/src/traits/query/type_op/implied_outlives_bounds.rs#L95-L96 +[notnorm]: https://github.com/rust-lang/rust/blob/91cae1dcdcf1a31bd8a92e4a63793d65cfe289bb/compiler/rustc_trait_selection/src/traits/engine.rs#L227-L250 + +### 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: +- by using subtyping: [#25860] +- by using super trait upcasting for a higher ranked trait bound: [#84591] +- by being able to normalize a projection when using an impl while not being able + to normalize it when checking the impl: [#100051] + +[#25860]: https://github.com/rust-lang/rust/issues/25860 +[#84591]: https://github.com/rust-lang/rust/issues/84591 +[#100051]: https://github.com/rust-lang/rust/issues/100051 \ No newline at end of file