Skip to content

Commit

Permalink
Rollup merge of #109447 - lcnr:coherence, r=compiler-errors
Browse files Browse the repository at this point in the history
new solver cleanup + implement coherence

the cleanup:
- change `Certainty::unify_and` to consider ambig + overflow to be ambig
- rename `trait_candidate_should_be_dropped_in_favor_of` to `candidate_should_be_dropped_in_favor_of`
- remove outdated fixme

For coherence I mostly just add an ambiguous candidate if the current trait ref is unknowable. I am doing the same for reservation impl where I also just add an ambiguous candidate.
  • Loading branch information
matthiaskrgr committed Mar 22, 2023
2 parents b22db3f + f86b035 commit 28b9354
Show file tree
Hide file tree
Showing 20 changed files with 226 additions and 62 deletions.
4 changes: 2 additions & 2 deletions compiler/rustc_infer/src/infer/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -585,8 +585,8 @@ impl<'tcx> InferCtxtBuilder<'tcx> {
self
}

pub fn intercrate(mut self) -> Self {
self.intercrate = true;
pub fn intercrate(mut self, intercrate: bool) -> Self {
self.intercrate = intercrate;
self
}

Expand Down
13 changes: 6 additions & 7 deletions compiler/rustc_middle/src/traits/solve.rs
Original file line number Diff line number Diff line change
Expand Up @@ -63,15 +63,14 @@ 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::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::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)
}
}
}
}
Expand Down
69 changes: 40 additions & 29 deletions compiler/rustc_trait_selection/src/solve/assembly.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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>,
Expand Down Expand Up @@ -468,25 +472,49 @@ 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),
_ => {}
}

if candidates.len() > 1 {
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;
Expand All @@ -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>,
Expand All @@ -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
}
}
19 changes: 16 additions & 3 deletions compiler/rustc_trait_selection/src/solve/eval_ctxt.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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> {
Expand Down Expand Up @@ -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,
Expand All @@ -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
Expand All @@ -120,8 +127,14 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
//
// The actual solver logic happens in `ecx.compute_goal`.
search_graph.with_new_goal(tcx, canonical_goal, |search_graph| {
let (ref infcx, goal, var_values) =
tcx.infer_ctxt().build_with_canonical(DUMMY_SP, &canonical_goal);
let intercrate = match search_graph.solver_mode() {
SolverMode::Normal => false,
SolverMode::Coherence => true,
};
let (ref infcx, goal, var_values) = tcx
.infer_ctxt()
.intercrate(intercrate)
.build_with_canonical(DUMMY_SP, &canonical_goal);
let mut ecx = EvalCtxt {
infcx,
var_values,
Expand Down
19 changes: 14 additions & 5 deletions compiler/rustc_trait_selection/src/solve/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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;
}
Expand Down Expand Up @@ -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) {
Expand Down
6 changes: 5 additions & 1 deletion compiler/rustc_trait_selection/src/solve/project_goals.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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)
}
Expand Down
16 changes: 13 additions & 3 deletions compiler/rustc_trait_selection/src/solve/search_graph/mod.rs
Original file line number Diff line number Diff line change
@@ -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;
Expand All @@ -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 {}
}
Expand All @@ -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*.
Expand All @@ -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()
}
Expand Down Expand Up @@ -245,7 +254,8 @@ impl<'tcx> SearchGraph<'tcx> {
// dependencies, our non-root goal may no longer appear as child of the root goal.
//
// See https://github.com/rust-lang/rust/pull/108071 for some additional context.
let should_cache_globally = !self.overflow_data.did_overflow() || self.stack.is_empty();
let should_cache_globally = matches!(self.solver_mode(), SolverMode::Normal)
&& (!self.overflow_data.did_overflow() || self.stack.is_empty());
if should_cache_globally {
tcx.new_solver_evaluation_cache.insert(
current_goal.goal,
Expand Down
27 changes: 24 additions & 3 deletions compiler/rustc_trait_selection/src/solve/trait_goals.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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)
}
Expand All @@ -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);
Expand All @@ -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)
})
}

Expand Down Expand Up @@ -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)
}
}
Loading

0 comments on commit 28b9354

Please sign in to comment.