Don't require intercrate mode for negative coherence

This commit is contained in:
Michael Goulet 2023-11-19 19:19:51 +00:00
parent 19a5e1dfc6
commit 253f5023c3
7 changed files with 19 additions and 41 deletions

View File

@ -65,8 +65,15 @@ impl<'tcx> InferCtxt<'tcx> {
/// Forks the inference context, creating a new inference context with the same inference
/// variables in the same state. This can be used to "branch off" many tests from the same
/// common state. Used in coherence.
/// common state.
pub fn fork(&self) -> Self {
self.fork_with_intercrate(self.intercrate)
}
/// Forks the inference context, creating a new inference context with the same inference
/// variables in the same state, except possibly changing the intercrate mode. This can be
/// used to "branch off" many tests from the same common state. Used in negative coherence.
pub fn fork_with_intercrate(&self, intercrate: bool) -> Self {
Self {
tcx: self.tcx,
defining_use_anchor: self.defining_use_anchor,
@ -81,7 +88,7 @@ impl<'tcx> InferCtxt<'tcx> {
tainted_by_errors: self.tainted_by_errors.clone(),
err_count_on_creation: self.err_count_on_creation,
universe: self.universe.clone(),
intercrate: self.intercrate,
intercrate,
next_trait_solver: self.next_trait_solver,
}
}

View File

@ -397,6 +397,8 @@ fn impl_intersection_has_negative_obligation(
) -> bool {
debug!("negative_impl(impl1_def_id={:?}, impl2_def_id={:?})", impl1_def_id, impl2_def_id);
// N.B. We need to unify impl headers *with* intercrate mode, even if proving negative predicates
// do not need intercrate mode enabled.
let ref infcx = tcx.infer_ctxt().intercrate(true).with_next_trait_solver(true).build();
let root_universe = infcx.universe();
assert_eq!(root_universe, ty::UniverseIndex::ROOT);
@ -554,7 +556,11 @@ fn try_prove_negated_where_clause<'tcx>(
return false;
};
let ref infcx = root_infcx.fork();
// N.B. We don't need to use intercrate mode here because we're trying to prove
// the *existence* of a negative goal, not the non-existence of a positive goal.
// Without this, we over-eagerly register coherence ambiguity candidates when
// impl candidates do exist.
let ref infcx = root_infcx.fork_with_intercrate(false);
let ocx = ObligationCtxt::new(infcx);
ocx.register_obligation(Obligation::new(

View File

@ -1,10 +1,4 @@
// known-bug: unknown
// This fails because we currently perform negative coherence in coherence mode.
// This means that when looking for a negative predicate, we also assemble a
// coherence-unknowable predicate. Since confirming the negative impl has region
// obligations, we don't prefer the impl over the unknowable predicate
// unconditionally and instead flounder.
// check-pass
#![feature(negative_impls)]
#![feature(rustc_attrs)]

View File

@ -1,11 +0,0 @@
error[E0119]: conflicting implementations of trait `Bar` for type `&_`
--> $DIR/coherence-overlap-with-regions.rs:20:1
|
LL | impl<T: Foo> Bar for T {}
| ---------------------- first implementation here
LL | impl<T> Bar for &T where T: 'static {}
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ conflicting implementation for `&_`
error: aborting due to previous error
For more information about this error, try `rustc --explain E0119`.

View File

@ -1,5 +1,5 @@
error[E0119]: conflicting implementations of trait `Bar` for type `&_`
--> $DIR/negative-coherence-considering-regions.rs:22:1
--> $DIR/negative-coherence-considering-regions.rs:16:1
|
LL | impl<T> Bar for T where T: Foo {}
| ------------------------------ first implementation here

View File

@ -1,11 +1,5 @@
// revisions: any_lt static_lt
//[static_lt] known-bug: unknown
// This fails because we currently perform negative coherence in coherence mode.
// This means that when looking for a negative predicate, we also assemble a
// coherence-unknowable predicate. Since confirming the negative impl has region
// obligations, we don't prefer the impl over the unknowable predicate
// unconditionally and instead flounder.
//[static_lt] check-pass
#![feature(negative_impls)]
#![feature(with_negative_coherence)]

View File

@ -1,12 +0,0 @@
error[E0119]: conflicting implementations of trait `Bar` for type `&'static _`
--> $DIR/negative-coherence-considering-regions.rs:26:1
|
LL | impl<T> Bar for T where T: Foo {}
| ------------------------------ first implementation here
...
LL | impl<T> Bar for &'static T {}
| ^^^^^^^^^^^^^^^^^^^^^^^^^^ conflicting implementation for `&'static _`
error: aborting due to previous error
For more information about this error, try `rustc --explain E0119`.