new solver cleanup + coherence

This commit is contained in:
lcnr 2023-03-21 16:26:23 +01:00
parent a01b4cc9f3
commit 47f24a881b
18 changed files with 203 additions and 52 deletions

View File

@ -63,14 +63,13 @@ impl Certainty {
(Certainty::Yes, Certainty::Yes) => Certainty::Yes,
(Certainty::Yes, Certainty::Maybe(_)) => other,
(Certainty::Maybe(_), Certainty::Yes) => self,
(Certainty::Maybe(MaybeCause::Overflow), Certainty::Maybe(MaybeCause::Overflow)) => {
(Certainty::Maybe(MaybeCause::Ambiguity), Certainty::Maybe(MaybeCause::Ambiguity)) => {
Certainty::Maybe(MaybeCause::Overflow)
}
// If at least one of the goals is ambiguous, hide the overflow as the ambiguous goal
// may still result in failure.
(Certainty::Maybe(MaybeCause::Ambiguity), Certainty::Maybe(_))
| (Certainty::Maybe(_), Certainty::Maybe(MaybeCause::Ambiguity)) => {
Certainty::Maybe(MaybeCause::Ambiguity)
(Certainty::Maybe(MaybeCause::Ambiguity), Certainty::Maybe(MaybeCause::Overflow))
| (Certainty::Maybe(MaybeCause::Overflow), Certainty::Maybe(MaybeCause::Ambiguity))
| (Certainty::Maybe(MaybeCause::Overflow), Certainty::Maybe(MaybeCause::Overflow)) => {
Certainty::Maybe(MaybeCause::Overflow)
}
}
}

View File

@ -2,7 +2,8 @@
#[cfg(doc)]
use super::trait_goals::structural_traits::*;
use super::EvalCtxt;
use super::{EvalCtxt, SolverMode};
use crate::traits::coherence;
use itertools::Itertools;
use rustc_hir::def_id::DefId;
use rustc_infer::traits::query::NoSolution;
@ -87,6 +88,8 @@ pub(super) enum CandidateSource {
pub(super) trait GoalKind<'tcx>: TypeFoldable<TyCtxt<'tcx>> + Copy + Eq {
fn self_ty(self) -> Ty<'tcx>;
fn trait_ref(self, tcx: TyCtxt<'tcx>) -> ty::TraitRef<'tcx>;
fn with_self_ty(self, tcx: TyCtxt<'tcx>, self_ty: Ty<'tcx>) -> Self;
fn trait_def_id(self, tcx: TyCtxt<'tcx>) -> DefId;
@ -244,15 +247,16 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
self.assemble_object_bound_candidates(goal, &mut candidates);
self.assemble_coherence_unknowable_candidates(goal, &mut candidates);
candidates
}
/// If the self type of a goal is a projection, computing the relevant candidates is difficult.
///
/// To deal with this, we first try to normalize the self type and add the candidates for the normalized
/// self type to the list of candidates in case that succeeds. Note that we can't just eagerly return in
/// this case as projections as self types add
// FIXME complete the unfinished sentence above
/// self type to the list of candidates in case that succeeds. We also have to consider candidates with the
/// projection as a self type as well
fn assemble_candidates_after_normalizing_self_ty<G: GoalKind<'tcx>>(
&mut self,
goal: Goal<'tcx, G>,
@ -468,14 +472,40 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
}
}
fn assemble_coherence_unknowable_candidates<G: GoalKind<'tcx>>(
&mut self,
goal: Goal<'tcx, G>,
candidates: &mut Vec<Candidate<'tcx>>,
) {
match self.solver_mode() {
SolverMode::Normal => return,
SolverMode::Coherence => {
let trait_ref = goal.predicate.trait_ref(self.tcx());
match coherence::trait_ref_is_knowable(self.tcx(), trait_ref) {
Ok(()) => {}
Err(_) => match self
.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
{
Ok(result) => candidates
.push(Candidate { source: CandidateSource::BuiltinImpl, result }),
// FIXME: This will be reachable at some point if we're in
// `assemble_candidates_after_normalizing_self_ty` and we get a
// universe error. We'll deal with it at this point.
Err(NoSolution) => bug!("coherence candidate resulted in NoSolution"),
},
}
}
}
}
#[instrument(level = "debug", skip(self), ret)]
pub(super) fn merge_candidates_and_discard_reservation_impls(
pub(super) fn merge_candidates(
&mut self,
mut candidates: Vec<Candidate<'tcx>>,
) -> QueryResult<'tcx> {
match candidates.len() {
0 => return Err(NoSolution),
1 => return Ok(self.discard_reservation_impl(candidates.pop().unwrap()).result),
1 => return Ok(candidates.pop().unwrap().result),
_ => {}
}
@ -483,10 +513,8 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
let mut i = 0;
'outer: while i < candidates.len() {
for j in (0..candidates.len()).filter(|&j| i != j) {
if self.trait_candidate_should_be_dropped_in_favor_of(
&candidates[i],
&candidates[j],
) {
if self.candidate_should_be_dropped_in_favor_of(&candidates[i], &candidates[j])
{
debug!(candidate = ?candidates[i], "Dropping candidate #{}/{}", i, candidates.len());
candidates.swap_remove(i);
continue 'outer;
@ -511,11 +539,10 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
}
}
// FIXME: What if there are >1 candidates left with the same response, and one is a reservation impl?
Ok(self.discard_reservation_impl(candidates.pop().unwrap()).result)
Ok(candidates.pop().unwrap().result)
}
fn trait_candidate_should_be_dropped_in_favor_of(
fn candidate_should_be_dropped_in_favor_of(
&self,
candidate: &Candidate<'tcx>,
other: &Candidate<'tcx>,
@ -528,20 +555,4 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
| (CandidateSource::BuiltinImpl, _) => false,
}
}
fn discard_reservation_impl(&mut self, mut candidate: Candidate<'tcx>) -> Candidate<'tcx> {
if let CandidateSource::Impl(def_id) = candidate.source {
if let ty::ImplPolarity::Reservation = self.tcx().impl_polarity(def_id) {
debug!("Selected reservation impl");
// We assemble all candidates inside of a probe so by
// making a new canonical response here our result will
// have no constraints.
candidate.result = self
.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
.unwrap();
}
}
candidate
}
}

View File

@ -17,6 +17,7 @@ use rustc_span::DUMMY_SP;
use std::ops::ControlFlow;
use super::search_graph::{self, OverflowHandler};
use super::SolverMode;
use super::{search_graph::SearchGraph, Goal};
pub struct EvalCtxt<'a, 'tcx> {
@ -78,7 +79,9 @@ impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
&self,
goal: Goal<'tcx, ty::Predicate<'tcx>>,
) -> Result<(bool, Certainty), NoSolution> {
let mut search_graph = search_graph::SearchGraph::new(self.tcx);
let mode = if self.intercrate { SolverMode::Coherence } else { SolverMode::Normal };
let mut search_graph = search_graph::SearchGraph::new(self.tcx, mode);
let mut ecx = EvalCtxt {
search_graph: &mut search_graph,
@ -101,6 +104,10 @@ impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
}
impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
pub(super) fn solver_mode(&self) -> SolverMode {
self.search_graph.solver_mode()
}
/// The entry point of the solver.
///
/// This function deals with (coinductive) cycles, overflow, and caching

View File

@ -9,10 +9,6 @@
//! FIXME(@lcnr): Write that section. If you read this before then ask me
//! about it on zulip.
// FIXME: Instead of using `infcx.canonicalize_query` we have to add a new routine which
// preserves universes and creates a unique var (in the highest universe) for each
// appearance of a region.
// FIXME: uses of `infcx.at` need to enable deferred projection equality once that's implemented.
use rustc_hir::def_id::DefId;
@ -41,6 +37,19 @@ mod trait_goals;
pub use eval_ctxt::{EvalCtxt, InferCtxtEvalExt};
pub use fulfill::FulfillmentCtxt;
#[derive(Debug, Clone, Copy)]
enum SolverMode {
/// Ordinary trait solving, using everywhere except for coherence.
Normal,
/// Trait solving during coherence. There are a few notable differences
/// between coherence and ordinary trait solving.
///
/// Most importantly, trait solving during coherence must not be incomplete,
/// i.e. return `Err(NoSolution)` for goals for which a solution exists.
/// This means that we must not make any guesses or arbitrary choices.
Coherence,
}
trait CanonicalResponseExt {
fn has_no_inference_or_external_constraints(&self) -> bool;
}
@ -255,7 +264,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
return Err(NoSolution);
}
// FIXME(-Ztreat-solver=next): We should instead try to find a `Certainty::Yes` response with
// FIXME(-Ztrait-solver=next): We should instead try to find a `Certainty::Yes` response with
// a subset of the constraints that all the other responses have.
let one = candidates[0];
if candidates[1..].iter().all(|resp| resp == &one) {

View File

@ -34,7 +34,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
// projection cache in the solver.
if self.term_is_fully_unconstrained(goal) {
let candidates = self.assemble_and_evaluate_candidates(goal);
self.merge_candidates_and_discard_reservation_impls(candidates)
self.merge_candidates(candidates)
} else {
let predicate = goal.predicate;
let unconstrained_rhs = self.next_term_infer_of_kind(predicate.term);
@ -56,6 +56,10 @@ impl<'tcx> assembly::GoalKind<'tcx> for ProjectionPredicate<'tcx> {
self.self_ty()
}
fn trait_ref(self, tcx: TyCtxt<'tcx>) -> ty::TraitRef<'tcx> {
self.projection_ty.trait_ref(tcx)
}
fn with_self_ty(self, tcx: TyCtxt<'tcx>, self_ty: Ty<'tcx>) -> Self {
self.with_self_ty(tcx, self_ty)
}

View File

@ -1,8 +1,9 @@
mod cache;
mod overflow;
pub(super) use overflow::OverflowHandler;
use self::cache::ProvisionalEntry;
pub(super) use crate::solve::search_graph::overflow::OverflowHandler;
use cache::ProvisionalCache;
use overflow::OverflowData;
use rustc_index::vec::IndexVec;
@ -11,6 +12,8 @@ use rustc_middle::traits::solve::{CanonicalGoal, Certainty, MaybeCause, QueryRes
use rustc_middle::ty::TyCtxt;
use std::{collections::hash_map::Entry, mem};
use super::SolverMode;
rustc_index::newtype_index! {
pub struct StackDepth {}
}
@ -21,6 +24,7 @@ struct StackElem<'tcx> {
}
pub(super) struct SearchGraph<'tcx> {
mode: SolverMode,
/// The stack of goals currently being computed.
///
/// An element is *deeper* in the stack if its index is *lower*.
@ -30,14 +34,19 @@ pub(super) struct SearchGraph<'tcx> {
}
impl<'tcx> SearchGraph<'tcx> {
pub(super) fn new(tcx: TyCtxt<'tcx>) -> SearchGraph<'tcx> {
pub(super) fn new(tcx: TyCtxt<'tcx>, mode: SolverMode) -> SearchGraph<'tcx> {
Self {
mode,
stack: Default::default(),
overflow_data: OverflowData::new(tcx),
provisional_cache: ProvisionalCache::empty(),
}
}
pub(super) fn solver_mode(&self) -> SolverMode {
self.mode
}
pub(super) fn is_empty(&self) -> bool {
self.stack.is_empty() && self.provisional_cache.is_empty()
}

View File

@ -2,7 +2,7 @@
use std::iter;
use super::{assembly, EvalCtxt};
use super::{assembly, EvalCtxt, SolverMode};
use rustc_hir::def_id::DefId;
use rustc_hir::LangItem;
use rustc_infer::traits::query::NoSolution;
@ -20,6 +20,10 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
self.self_ty()
}
fn trait_ref(self, _: TyCtxt<'tcx>) -> ty::TraitRef<'tcx> {
self.trait_ref
}
fn with_self_ty(self, tcx: TyCtxt<'tcx>, self_ty: Ty<'tcx>) -> Self {
self.with_self_ty(tcx, self_ty)
}
@ -43,6 +47,22 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
return Err(NoSolution);
}
let impl_polarity = tcx.impl_polarity(impl_def_id);
// An upper bound of the certainty of this goal, used to lower the certainty
// of reservation impl to ambiguous during coherence.
let maximal_certainty = match impl_polarity {
ty::ImplPolarity::Positive | ty::ImplPolarity::Negative => {
match impl_polarity == goal.predicate.polarity {
true => Certainty::Yes,
false => return Err(NoSolution),
}
}
ty::ImplPolarity::Reservation => match ecx.solver_mode() {
SolverMode::Normal => return Err(NoSolution),
SolverMode::Coherence => Certainty::AMBIGUOUS,
},
};
ecx.probe(|ecx| {
let impl_substs = ecx.fresh_substs_for_item(impl_def_id);
let impl_trait_ref = impl_trait_ref.subst(tcx, impl_substs);
@ -55,7 +75,8 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
.into_iter()
.map(|pred| goal.with(tcx, pred));
ecx.add_goals(where_clause_bounds);
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
ecx.evaluate_added_goals_and_make_canonical_response(maximal_certainty)
})
}
@ -547,6 +568,6 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
goal: Goal<'tcx, TraitPredicate<'tcx>>,
) -> QueryResult<'tcx> {
let candidates = self.assemble_and_evaluate_candidates(goal);
self.merge_candidates_and_discard_reservation_impls(candidates)
self.merge_candidates(candidates)
}
}

View File

@ -4,7 +4,7 @@
pub mod auto_trait;
mod chalk_fulfill;
mod coherence;
pub(crate) mod coherence;
pub mod const_evaluatable;
mod engine;
pub mod error_reporting;

View File

@ -0,0 +1,44 @@
// This must fail coherence.
//
// Getting this to pass was fairly difficult, so here's an explanation
// of what's happening:
//
// Normalizing projections currently tries to replace them with inference variables
// while emitting a nested `Projection` obligation. This cannot be done if the projection
// has bound variables which is the case here.
//
// So the projections stay until after normalization. When unifying two projections we
// currently treat them as if they are injective, so we **incorrectly** unify their
// substs. This means that coherence for the two impls ends up unifying `?T` and `?U`
// as it tries to unify `<?T as WithAssoc1<'a>>::Assoc` with `<?U as WithAssoc1<'a>>::Assoc`.
//
// `impl1` therefore has the projection `<?T as WithAssoc2<'a>>::Assoc` and we have the
// assumption `?T: for<'a> WithAssoc2<'a, Assoc = i32>` in the `param_env`, so we normalize
// that to `i32`. We then try to unify `i32` from `impl1` with `u32` from `impl2` which fails,
// causing coherence to consider these two impls distinct.
// compile-flags: -Ztrait-solver=next
pub trait Trait<T> {}
pub trait WithAssoc1<'a> {
type Assoc;
}
pub trait WithAssoc2<'a> {
type Assoc;
}
// impl 1
impl<T, U> Trait<for<'a> fn(<T as WithAssoc1<'a>>::Assoc, <U as WithAssoc2<'a>>::Assoc)> for (T, U)
where
T: for<'a> WithAssoc1<'a> + for<'a> WithAssoc2<'a, Assoc = i32>,
U: for<'a> WithAssoc2<'a>,
{
}
// impl 2
impl<T, U> Trait<for<'a> fn(<U as WithAssoc1<'a>>::Assoc, u32)> for (T, U) where
U: for<'a> WithAssoc1<'a> //~^ ERROR conflicting implementations of trait
{
}
fn main() {}

View File

@ -0,0 +1,12 @@
error[E0119]: conflicting implementations of trait `Trait<for<'a> fn(<_ as WithAssoc1<'a>>::Assoc, <_ as WithAssoc2<'a>>::Assoc)>` for type `(_, _)`
--> $DIR/issue-102048.rs:39:1
|
LL | impl<T, U> Trait<for<'a> fn(<T as WithAssoc1<'a>>::Assoc, <U as WithAssoc2<'a>>::Assoc)> for (T, U)
| --------------------------------------------------------------------------------------------------- first implementation here
...
LL | impl<T, U> Trait<for<'a> fn(<U as WithAssoc1<'a>>::Assoc, u32)> for (T, U) where
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ conflicting implementation for `(_, _)`
error: aborting due to previous error
For more information about this error, try `rustc --explain E0119`.

View File

@ -0,0 +1,11 @@
error[E0119]: conflicting implementations of trait `OtherTrait` for type `()`
--> $DIR/coherence-conflict.rs:12:1
|
LL | impl OtherTrait for () {}
| ---------------------- first implementation here
LL | impl<T: MyTrait> OtherTrait for T {}
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 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 `OtherTrait` for type `()`
--> $DIR/coherence-conflict.rs:11:1
--> $DIR/coherence-conflict.rs:12:1
|
LL | impl OtherTrait for () {}
| ---------------------- first implementation here

View File

@ -1,5 +1,6 @@
// check that reservation impls are accounted for in negative reasoning.
// revisions: old next
//[next] compile-flags: -Ztrait-solver=next
#![feature(rustc_attrs)]
trait MyTrait {}

View File

@ -1,5 +1,5 @@
error[E0277]: the trait bound `(): MyTrait` is not satisfied
--> $DIR/no-use.rs:10:26
--> $DIR/no-use.rs:11:26
|
LL | <() as MyTrait>::foo(&());
| -------------------- ^^^ the trait `MyTrait` is not implemented for `()`

View File

@ -0,0 +1,13 @@
error[E0277]: the trait bound `(): MyTrait` is not satisfied
--> $DIR/no-use.rs:11:26
|
LL | <() as MyTrait>::foo(&());
| -------------------- ^^^ the trait `MyTrait` is not implemented for `()`
| |
| required by a bound introduced by this call
|
= help: the trait `MyTrait` is implemented for `()`
error: aborting due to previous error
For more information about this error, try `rustc --explain E0277`.

View File

@ -1,5 +1,6 @@
// check that reservation impls can't be used as normal impls in positive reasoning.
// revisions: old next
//[next] compile-flags: -Ztrait-solver=next
#![feature(rustc_attrs)]
trait MyTrait { fn foo(&self); }

View File

@ -30,6 +30,12 @@
//
// [ii]: https://smallcultfollowing.com/babysteps/blog/2016/09/24/intersection-impls/
// check that reservation impls can't be used as normal impls in positive reasoning.
// revisions: old next
//[next] compile-flags: -Ztrait-solver=next
#![feature(rustc_attrs, never_type)]
trait MyTrait {}

View File

@ -3,6 +3,9 @@
// rpass test for reservation impls. Not 100% required because `From` uses them,
// but still.
// revisions: old next
//[next] compile-flags: -Ztrait-solver=next
#![feature(rustc_attrs)]
use std::mem;