Skip to content

Commit 15e6565

Browse files
Implement fix in try_promote_type_test_subject + add a test.
Fix in question: We only propagate `T: 'ub` requirements when 'ub actually outlives the lower bounds of the type test. If none of the non-local upper bounds outlive it, then we propagate all of them.
1 parent eaf4e74 commit 15e6565

2 files changed

Lines changed: 52 additions & 1 deletion

File tree

compiler/rustc_borrowck/src/region_infer/mod.rs

Lines changed: 27 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -713,9 +713,35 @@ impl<'tcx> RegionInferenceContext<'tcx> {
713713
for ur in self.scc_values.universal_regions_outlived_by(r_scc) {
714714
found_outlived_universal_region = true;
715715
debug!("universal_region_outlived_by ur={:?}", ur);
716-
let non_local_ub = self.universal_region_relations.non_local_upper_bounds(ur);
716+
let mut non_local_ub = self.universal_region_relations.non_local_upper_bounds(ur);
717717
debug!(?non_local_ub);
718718

719+
// We don't need to propagate every `T: 'ub` for soundness:
720+
// Say we have the following outlives constraints given (`'b: 'a` == `a -> b`):
721+
//
722+
// a
723+
// \
724+
// -> c
725+
// /
726+
// b
727+
//
728+
// And we are doing the type test `T: 'a`.
729+
//
730+
// The `lower_bound_universal_regions` of `'a` are `['a, 'c]`. The `upper_bounds` of `'a`
731+
// is `['a]`, so we propagate `T: 'a`.
732+
// The `upper_bounds` of `'c` are `['a, 'b]`, propagating `T: 'a` is correct;
733+
// `T: 'b` is redundant because it provides no value to proving `T: 'a`.
734+
//
735+
// So we filter the set of upper_bounds to regions already outliving `lower_bound`,
736+
// but if this subset is empty, we fall back to the original one.
737+
let subset: Vec<_> = non_local_ub
738+
.iter()
739+
.copied()
740+
.filter(|ub| self.eval_outlives(*ub, lower_bound))
741+
.collect();
742+
non_local_ub = if subset.is_empty() { non_local_ub } else { subset };
743+
debug!(?non_local_ub, "upper_bounds after filtering");
744+
719745
// This is slightly too conservative. To show T: '1, given `'2: '1`
720746
// and `'3: '1` we only need to prove that T: '2 *or* T: '3, but to
721747
// avoid potential non-determinism we approximate this by requiring
Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
//@ check-pass
2+
// This test checks that the compiler doesn't propagate `T: 'b` during the `T: 'a` type test.
3+
// If it did, it would fail to compile, even though the program is sound.
4+
5+
struct Arg<'a: 'c, 'b: 'c, 'c, T> {
6+
field: *mut (&'a (), &'b (), &'c (), T),
7+
}
8+
9+
impl<'a, 'b, 'c, T> Arg<'a, 'b, 'c, T> {
10+
fn constrain(self)
11+
where
12+
T: 'a,
13+
{
14+
}
15+
}
16+
17+
fn takes_closure<'a, 'b, T>(_: impl for<'c> FnOnce(Arg<'a, 'b, 'c, T>)) {}
18+
19+
// We have `'a: 'c` and `'b: 'c`, requiring `T: 'a` in `constrain` should not need
20+
// `T: 'b` here.
21+
fn error<'a, 'b, T: 'a>() {
22+
takes_closure::<'a, 'b, T>(|arg| arg.constrain());
23+
}
24+
25+
fn main() {}

0 commit comments

Comments
 (0)