1
Fork 0

Use separate infcx to solve obligations during negative coherence

This commit is contained in:
Michael Goulet 2022-08-20 03:23:23 +00:00
parent e1b28cd2f1
commit ba7272959d
4 changed files with 26 additions and 15 deletions

View file

@ -342,10 +342,8 @@ fn equate<'cx, 'tcx>(
}; };
let selcx = &mut SelectionContext::new(&infcx); let selcx = &mut SelectionContext::new(&infcx);
let opt_failing_obligation = obligations let opt_failing_obligation =
.into_iter() obligations.into_iter().chain(more_obligations).find(|o| negative_impl_exists(selcx, o));
.chain(more_obligations)
.find(|o| negative_impl_exists(selcx, impl_env, o));
if let Some(failing_obligation) = opt_failing_obligation { if let Some(failing_obligation) = opt_failing_obligation {
debug!("overlap: obligation unsatisfiable {:?}", failing_obligation); debug!("overlap: obligation unsatisfiable {:?}", failing_obligation);
@ -359,18 +357,15 @@ fn equate<'cx, 'tcx>(
#[instrument(level = "debug", skip(selcx))] #[instrument(level = "debug", skip(selcx))]
fn negative_impl_exists<'cx, 'tcx>( fn negative_impl_exists<'cx, 'tcx>(
selcx: &SelectionContext<'cx, 'tcx>, selcx: &SelectionContext<'cx, 'tcx>,
param_env: ty::ParamEnv<'tcx>,
o: &PredicateObligation<'tcx>, o: &PredicateObligation<'tcx>,
) -> bool { ) -> bool {
let infcx = &selcx.infcx().fork(); if resolve_negative_obligation(selcx.infcx().fork(), o) {
if resolve_negative_obligation(infcx, param_env, o) {
return true; return true;
} }
// Try to prove a negative obligation exists for super predicates // Try to prove a negative obligation exists for super predicates
for o in util::elaborate_predicates(infcx.tcx, iter::once(o.predicate)) { for o in util::elaborate_predicates(selcx.tcx(), iter::once(o.predicate)) {
if resolve_negative_obligation(infcx, param_env, &o) { if resolve_negative_obligation(selcx.infcx().fork(), &o) {
return true; return true;
} }
} }
@ -380,8 +375,7 @@ fn negative_impl_exists<'cx, 'tcx>(
#[instrument(level = "debug", skip(infcx))] #[instrument(level = "debug", skip(infcx))]
fn resolve_negative_obligation<'cx, 'tcx>( fn resolve_negative_obligation<'cx, 'tcx>(
infcx: &InferCtxt<'cx, 'tcx>, infcx: InferCtxt<'cx, 'tcx>,
param_env: ty::ParamEnv<'tcx>,
o: &PredicateObligation<'tcx>, o: &PredicateObligation<'tcx>,
) -> bool { ) -> bool {
let tcx = infcx.tcx; let tcx = infcx.tcx;
@ -390,7 +384,8 @@ fn resolve_negative_obligation<'cx, 'tcx>(
return false; return false;
}; };
let errors = super::fully_solve_obligation(infcx, o); let param_env = o.param_env;
let errors = super::fully_solve_obligation(&infcx, o);
if !errors.is_empty() { if !errors.is_empty() {
return false; return false;
} }

View file

@ -1,10 +1,15 @@
// revisions: stock with_negative_coherence
#![feature(negative_impls)] #![feature(negative_impls)]
#![cfg_attr(with_negative_coherence, feature(with_negative_coherence))]
// FIXME: this should compile // FIXME: this should compile
trait MyPredicate<'a> {} trait MyPredicate<'a> {}
impl<'a, T> !MyPredicate<'a> for &T where T: 'a {}
impl<'a, T> !MyPredicate<'a> for &'a T where T: 'a {}
trait MyTrait<'a> {} trait MyTrait<'a> {}
impl<'a, T: MyPredicate<'a>> MyTrait<'a> for T {} impl<'a, T: MyPredicate<'a>> MyTrait<'a> for T {}
impl<'a, T> MyTrait<'a> for &'a T {} impl<'a, T> MyTrait<'a> for &'a T {}
//~^ ERROR: conflicting implementations of trait `MyTrait<'_>` for type `&_` //~^ ERROR: conflicting implementations of trait `MyTrait<'_>` for type `&_`

View file

@ -1,5 +1,5 @@
error[E0119]: conflicting implementations of trait `MyTrait<'_>` for type `&_` error[E0119]: conflicting implementations of trait `MyTrait<'_>` for type `&_`
--> $DIR/coherence-negative-outlives-lifetimes.rs:9:1 --> $DIR/coherence-negative-outlives-lifetimes.rs:14:1
| |
LL | impl<'a, T: MyPredicate<'a>> MyTrait<'a> for T {} LL | impl<'a, T: MyPredicate<'a>> MyTrait<'a> for T {}
| ---------------------------------------------- first implementation here | ---------------------------------------------- first implementation here

View file

@ -0,0 +1,11 @@
error[E0119]: conflicting implementations of trait `MyTrait<'_>` for type `&_`
--> $DIR/coherence-negative-outlives-lifetimes.rs:14:1
|
LL | impl<'a, T: MyPredicate<'a>> MyTrait<'a> for T {}
| ---------------------------------------------- first implementation here
LL | impl<'a, T> MyTrait<'a> for &'a T {}
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ conflicting implementation for `&_`
error: aborting due to previous error
For more information about this error, try `rustc --explain E0119`.