Skip to content

Commit

Permalink
Rollup merge of rust-lang#121193 - compiler-errors:coherence-fulfillm…
Browse files Browse the repository at this point in the history
…ent, r=lcnr

Use fulfillment in next trait solver coherence

Use fulfillment in the new trait solver's `impl_intersection_has_impossible_obligation` routine. This means that inference that falls out of processing other obligations can influence whether we can determine if an obligation is impossible to satisfy. See the committed test.

This should be completely sound, since evaluation and fulfillment both respect intercrate mode equally.

We run the risk of breaking coherence later if we were to change the rules of fulfillment and/or inference during coherence, but this is a problem which affects evaluation, as nested obligations from a trait goal are processed together and can influence each other in the same way.

r? lcnr
cc rust-lang#114862

Also changed obligationctxt -> fulfillmentctxt because it feels kind of redundant to use an ocx here. I don't really care enough and can change it back if it really matters much.
  • Loading branch information
matthiaskrgr authored Feb 17, 2024
2 parents 7f3cf08 + 228441d commit 7436a6a
Show file tree
Hide file tree
Showing 5 changed files with 97 additions and 37 deletions.
8 changes: 5 additions & 3 deletions compiler/rustc_trait_selection/src/solve/inspect/analyse.rs
Original file line number Diff line number Diff line change
Expand Up @@ -223,8 +223,10 @@ impl<'tcx> InferCtxt<'tcx> {
goal: Goal<'tcx, ty::Predicate<'tcx>>,
visitor: &mut V,
) -> ControlFlow<V::BreakTy> {
let (_, proof_tree) = self.evaluate_root_goal(goal, GenerateProofTree::Yes);
let proof_tree = proof_tree.unwrap();
visitor.visit_goal(&InspectGoal::new(self, 0, &proof_tree))
self.probe(|_| {
let (_, proof_tree) = self.evaluate_root_goal(goal, GenerateProofTree::Yes);
let proof_tree = proof_tree.unwrap();
visitor.visit_goal(&InspectGoal::new(self, 0, &proof_tree))
})
}
}
70 changes: 36 additions & 34 deletions compiler/rustc_trait_selection/src/traits/coherence.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,23 +8,21 @@ use crate::infer::outlives::env::OutlivesEnvironment;
use crate::infer::InferOk;
use crate::regions::InferCtxtRegionExt;
use crate::solve::inspect::{InspectGoal, ProofTreeInferCtxtExt, ProofTreeVisitor};
use crate::solve::{deeply_normalize_for_diagnostics, inspect};
use crate::traits::engine::TraitEngineExt;
use crate::traits::query::evaluate_obligation::InferCtxtExt;
use crate::solve::{deeply_normalize_for_diagnostics, inspect, FulfillmentCtxt};
use crate::traits::engine::TraitEngineExt as _;
use crate::traits::select::IntercrateAmbiguityCause;
use crate::traits::structural_normalize::StructurallyNormalizeExt;
use crate::traits::NormalizeExt;
use crate::traits::SkipLeakCheck;
use crate::traits::{
Obligation, ObligationCause, ObligationCtxt, PredicateObligation, PredicateObligations,
SelectionContext,
Obligation, ObligationCause, PredicateObligation, PredicateObligations, SelectionContext,
};
use rustc_data_structures::fx::FxIndexSet;
use rustc_errors::Diagnostic;
use rustc_hir::def::DefKind;
use rustc_hir::def_id::{DefId, LOCAL_CRATE};
use rustc_infer::infer::{DefineOpaqueTypes, InferCtxt, TyCtxtInferExt};
use rustc_infer::traits::{util, TraitEngine};
use rustc_infer::traits::{util, TraitEngine, TraitEngineExt};
use rustc_middle::traits::query::NoSolution;
use rustc_middle::traits::solve::{CandidateSource, Certainty, Goal};
use rustc_middle::traits::specialization_graph::OverlapMode;
Expand Down Expand Up @@ -310,29 +308,35 @@ fn equate_impl_headers<'tcx>(
fn impl_intersection_has_impossible_obligation<'a, 'cx, 'tcx>(
selcx: &mut SelectionContext<'cx, 'tcx>,
obligations: &'a [PredicateObligation<'tcx>],
) -> Option<&'a PredicateObligation<'tcx>> {
) -> Option<PredicateObligation<'tcx>> {
let infcx = selcx.infcx;

obligations.iter().find(|obligation| {
let evaluation_result = if infcx.next_trait_solver() {
infcx.evaluate_obligation(obligation)
} else {
if infcx.next_trait_solver() {
let mut fulfill_cx = FulfillmentCtxt::new(infcx);
fulfill_cx.register_predicate_obligations(infcx, obligations.iter().cloned());

// We only care about the obligations that are *definitely* true errors.
// Ambiguities do not prove the disjointness of two impls.
let mut errors = fulfill_cx.select_where_possible(infcx);
errors.pop().map(|err| err.obligation)
} else {
obligations.iter().cloned().find(|obligation| {
// We use `evaluate_root_obligation` to correctly track intercrate
// ambiguity clauses. We cannot use this in the new solver.
selcx.evaluate_root_obligation(obligation)
};

match evaluation_result {
Ok(result) => !result.may_apply(),
// If overflow occurs, we need to conservatively treat the goal as possibly holding,
// since there can be instantiations of this goal that don't overflow and result in
// success. This isn't much of a problem in the old solver, since we treat overflow
// fatally (this still can be encountered: <https://github.com/rust-lang/rust/issues/105231>),
// but in the new solver, this is very important for correctness, since overflow
// *must* be treated as ambiguity for completeness.
Err(_overflow) => false,
}
})
let evaluation_result = selcx.evaluate_root_obligation(obligation);

match evaluation_result {
Ok(result) => !result.may_apply(),
// If overflow occurs, we need to conservatively treat the goal as possibly holding,
// since there can be instantiations of this goal that don't overflow and result in
// success. This isn't much of a problem in the old solver, since we treat overflow
// fatally (this still can be encountered: <https://github.com/rust-lang/rust/issues/105231>),
// but in the new solver, this is very important for correctness, since overflow
// *must* be treated as ambiguity for completeness.
Err(_overflow) => false,
}
})
}
}

/// Check if both impls can be satisfied by a common type by considering whether
Expand Down Expand Up @@ -522,15 +526,13 @@ fn try_prove_negated_where_clause<'tcx>(
// 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(
infcx.tcx,
ObligationCause::dummy(),
param_env,
negative_predicate,
));
if !ocx.select_all_or_error().is_empty() {
let mut fulfill_cx = FulfillmentCtxt::new(infcx);

fulfill_cx.register_predicate_obligation(
infcx,
Obligation::new(infcx.tcx, ObligationCause::dummy(), param_env, negative_predicate),
);
if !fulfill_cx.select_all_or_error(infcx).is_empty() {
return false;
}

Expand Down
20 changes: 20 additions & 0 deletions tests/ui/coherence/coherent-due-to-fulfill.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
//@ compile-flags: -Znext-solver=coherence
//@ check-pass

trait Mirror {
type Assoc;
}
impl<T> Mirror for T {
type Assoc = T;
}

trait Foo {}
trait Bar {}

// self type starts out as `?0` but is constrained to `()`
// due to the where clause below. Because `(): Bar` does not
// hold in intercrate mode, we can prove the impls disjoint.
impl<T> Foo for T where (): Mirror<Assoc = T> {}
impl<T> Foo for T where T: Bar {}

fn main() {}
22 changes: 22 additions & 0 deletions tests/ui/coherence/incoherent-even-though-we-fulfill.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
//@ compile-flags: -Znext-solver=coherence

trait Mirror {
type Assoc;
}
impl<T> Mirror for T {
type Assoc = T;
}

trait Foo {}

// Even though using fulfillment in coherence allows us to figure out that
// `?T = ()`, we still treat it as incoherent because `(): Iterator` may be
// added upstream.
impl<T> Foo for T where (): Mirror<Assoc = T> {}
//~^ NOTE first implementation here
impl<T> Foo for T where T: Iterator {}
//~^ ERROR conflicting implementations of trait `Foo` for type `()`
//~| NOTE conflicting implementation for `()`
//~| NOTE upstream crates may add a new impl of trait `std::iter::Iterator` for type `()` in future versions

fn main() {}
14 changes: 14 additions & 0 deletions tests/ui/coherence/incoherent-even-though-we-fulfill.stderr
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
error[E0119]: conflicting implementations of trait `Foo` for type `()`
--> $DIR/incoherent-even-though-we-fulfill.rs:17:1
|
LL | impl<T> Foo for T where (): Mirror<Assoc = T> {}
| --------------------------------------------- first implementation here
LL |
LL | impl<T> Foo for T where T: Iterator {}
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ conflicting implementation for `()`
|
= note: upstream crates may add a new impl of trait `std::iter::Iterator` for type `()` in future versions

error: aborting due to 1 previous error

For more information about this error, try `rustc --explain E0119`.

0 comments on commit 7436a6a

Please sign in to comment.