diff options
| author | Michael Goulet <michael@errs.io> | 2023-11-19 19:14:35 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2023-11-19 19:14:35 -0800 |
| commit | 40a781b179be13cfbe89d0fdfd42632da6eb1e7b (patch) | |
| tree | 5a0ba7d8e8084477e8fac380d99ee45ee7d82e0a /compiler | |
| parent | e6a3ca0c657a6c37e309fd8c9f0cc41d13478e20 (diff) | |
| parent | 488dcb7af3fc394ca438da2a9fe8a40dcae06948 (diff) | |
| download | rust-40a781b179be13cfbe89d0fdfd42632da6eb1e7b.tar.gz rust-40a781b179be13cfbe89d0fdfd42632da6eb1e7b.zip | |
Rollup merge of #117994 - compiler-errors:throw-away-regions-in-coherence, r=lcnr
Ignore but do not assume region obligations from unifying headers in negative coherence Partly addresses a FIXME that was added in #112875. Just as we can throw away the nested trait/projection obligations from unifying two impl headers, we can also just throw away the region obligations too. I removed part of the FIXME that was incorrect, namely: > Given that the only region constraints we get are involving inference regions in the root, it shouldn't matter, but still sus. This is not true when unifying `fn(A)` and `for<'b> fn(&'b B)` which ends up with placeholder region outlives from non-root universes. I'm pretty sure this is okay, though it would be nice if we were to use them as assumptions. See the `explicit` revision of the test I committed, which still fails. Fixes #117986 r? lcnr, feel free to reassign tho.
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/rustc_trait_selection/src/traits/coherence.rs | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/compiler/rustc_trait_selection/src/traits/coherence.rs b/compiler/rustc_trait_selection/src/traits/coherence.rs index 7ca33ae41c0..16e44c0006a 100644 --- a/compiler/rustc_trait_selection/src/traits/coherence.rs +++ b/compiler/rustc_trait_selection/src/traits/coherence.rs @@ -408,7 +408,7 @@ fn impl_intersection_has_negative_obligation( // Equate the headers to find their intersection (the general type, with infer vars, // that may apply both impls). - let Some(_equate_obligations) = + let Some(equate_obligations) = equate_impl_headers(infcx, param_env, &impl1_header, &impl2_header) else { return false; @@ -416,6 +416,13 @@ fn impl_intersection_has_negative_obligation( plug_infer_with_placeholders(infcx, universe, (impl1_header.impl_args, impl2_header.impl_args)); + // FIXME(with_negative_coherence): the infcx has constraints from equating + // the impl headers. We should use these constraints as assumptions, not as + // requirements, when proving the negated where clauses below. + drop(equate_obligations); + drop(infcx.take_registered_region_obligations()); + drop(infcx.take_and_reset_region_constraints()); + util::elaborate(tcx, tcx.predicates_of(impl2_def_id).instantiate(tcx, impl2_header.impl_args)) .any(|(clause, _)| try_prove_negated_where_clause(infcx, clause, param_env)) } @@ -541,14 +548,6 @@ fn try_prove_negated_where_clause<'tcx>( return false; }; - // FIXME(with_negative_coherence): the infcx has region contraints from equating - // the impl headers as requirements. Given that the only region constraints we - // get are involving inference regions in the root, it shouldn't matter, but - // still sus. - // - // We probably should just throw away the region obligations registered up until - // now, or ideally use them as assumptions when proving the region obligations - // that we get from proving the negative predicate below. let ref infcx = root_infcx.fork(); let ocx = ObligationCtxt::new(infcx); |
