prioritize param-env candidates
This commit is contained in:
parent
749b487be4
commit
2b0f5721c1
8 changed files with 150 additions and 87 deletions
|
@ -4,8 +4,8 @@ use super::search_graph::OverflowHandler;
|
|||
#[cfg(doc)]
|
||||
use super::trait_goals::structural_traits::*;
|
||||
use super::{EvalCtxt, SolverMode};
|
||||
use crate::solve::CanonicalResponseExt;
|
||||
use crate::traits::coherence;
|
||||
use itertools::Itertools;
|
||||
use rustc_data_structures::fx::FxIndexSet;
|
||||
use rustc_hir::def_id::DefId;
|
||||
use rustc_infer::traits::query::NoSolution;
|
||||
|
@ -547,61 +547,41 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
|
|||
}
|
||||
}
|
||||
|
||||
/// If there are multiple ways to prove a trait or projection goal, we have
|
||||
/// to somehow try to merge the candidates into one. If that fails, we return
|
||||
/// ambiguity.
|
||||
#[instrument(level = "debug", skip(self), ret)]
|
||||
pub(super) fn merge_candidates(
|
||||
&mut self,
|
||||
mut candidates: Vec<Candidate<'tcx>>,
|
||||
) -> QueryResult<'tcx> {
|
||||
match candidates.len() {
|
||||
0 => return Err(NoSolution),
|
||||
1 => return Ok(candidates.pop().unwrap().result),
|
||||
_ => {}
|
||||
// First try merging all candidates. This is complete and fully sound.
|
||||
let responses = candidates.iter().map(|c| c.result).collect::<Vec<_>>();
|
||||
if let Some(result) = self.try_merge_responses(&responses) {
|
||||
return Ok(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.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;
|
||||
// We then check whether we should prioritize `ParamEnv` candidates.
|
||||
//
|
||||
// Doing so is incomplete and would therefore be unsound during coherence.
|
||||
match self.solver_mode() {
|
||||
SolverMode::Coherence => (),
|
||||
// Prioritize `ParamEnv` candidates only if they do not guide inference.
|
||||
//
|
||||
// This is still incomplete as we may add incorrect region bounds.
|
||||
SolverMode::Normal => {
|
||||
let param_env_responses = candidates
|
||||
.iter()
|
||||
.filter(|c| matches!(c.source, CandidateSource::ParamEnv(_)))
|
||||
.map(|c| c.result)
|
||||
.collect::<Vec<_>>();
|
||||
if let Some(result) = self.try_merge_responses(¶m_env_responses) {
|
||||
if result.has_only_region_constraints() {
|
||||
return Ok(result);
|
||||
}
|
||||
}
|
||||
|
||||
debug!(candidate = ?candidates[i], "Retaining candidate #{}/{}", i, candidates.len());
|
||||
i += 1;
|
||||
}
|
||||
|
||||
// If there are *STILL* multiple candidates that have *different* response
|
||||
// results, give up and report ambiguity.
|
||||
if candidates.len() > 1 && !candidates.iter().map(|cand| cand.result).all_equal() {
|
||||
let certainty = if candidates.iter().all(|x| {
|
||||
matches!(x.result.value.certainty, Certainty::Maybe(MaybeCause::Overflow))
|
||||
}) {
|
||||
Certainty::Maybe(MaybeCause::Overflow)
|
||||
} else {
|
||||
Certainty::AMBIGUOUS
|
||||
};
|
||||
return self.evaluate_added_goals_and_make_canonical_response(certainty);
|
||||
}
|
||||
}
|
||||
|
||||
Ok(candidates.pop().unwrap().result)
|
||||
}
|
||||
|
||||
fn candidate_should_be_dropped_in_favor_of(
|
||||
&self,
|
||||
candidate: &Candidate<'tcx>,
|
||||
other: &Candidate<'tcx>,
|
||||
) -> bool {
|
||||
// FIXME: implement this
|
||||
match (candidate.source, other.source) {
|
||||
(CandidateSource::Impl(_), _)
|
||||
| (CandidateSource::ParamEnv(_), _)
|
||||
| (CandidateSource::AliasBound, _)
|
||||
| (CandidateSource::BuiltinImpl, _) => false,
|
||||
}
|
||||
self.flounder(&responses)
|
||||
}
|
||||
}
|
||||
|
|
|
@ -46,6 +46,8 @@ enum SolverMode {
|
|||
|
||||
trait CanonicalResponseExt {
|
||||
fn has_no_inference_or_external_constraints(&self) -> bool;
|
||||
|
||||
fn has_only_region_constraints(&self) -> bool;
|
||||
}
|
||||
|
||||
impl<'tcx> CanonicalResponseExt for Canonical<'tcx, Response<'tcx>> {
|
||||
|
@ -54,6 +56,11 @@ impl<'tcx> CanonicalResponseExt for Canonical<'tcx, Response<'tcx>> {
|
|||
&& self.value.var_values.is_identity()
|
||||
&& self.value.external_constraints.opaque_types.is_empty()
|
||||
}
|
||||
|
||||
fn has_only_region_constraints(&self) -> bool {
|
||||
self.value.var_values.is_identity_modulo_regions()
|
||||
&& self.value.external_constraints.opaque_types.is_empty()
|
||||
}
|
||||
}
|
||||
|
||||
impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
|
||||
|
@ -221,12 +228,17 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
|
|||
(Some(alias_lhs), Some(alias_rhs)) => {
|
||||
debug!("both sides are aliases");
|
||||
|
||||
let candidates = vec![
|
||||
// LHS normalizes-to RHS
|
||||
evaluate_normalizes_to(self, alias_lhs, rhs, direction, Invert::No),
|
||||
// RHS normalizes-to RHS
|
||||
evaluate_normalizes_to(self, alias_rhs, lhs, direction, Invert::Yes),
|
||||
// Relate via substs
|
||||
let mut candidates = Vec::new();
|
||||
// LHS normalizes-to RHS
|
||||
candidates.extend(
|
||||
evaluate_normalizes_to(self, alias_lhs, rhs, direction, Invert::No).ok(),
|
||||
);
|
||||
// RHS normalizes-to RHS
|
||||
candidates.extend(
|
||||
evaluate_normalizes_to(self, alias_rhs, lhs, direction, Invert::Yes).ok(),
|
||||
);
|
||||
// Relate via substs
|
||||
candidates.extend(
|
||||
self.probe(|ecx| {
|
||||
let span = tracing::span!(
|
||||
tracing::Level::DEBUG,
|
||||
|
@ -247,11 +259,16 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
|
|||
}
|
||||
|
||||
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
|
||||
}),
|
||||
];
|
||||
})
|
||||
.ok(),
|
||||
);
|
||||
debug!(?candidates);
|
||||
|
||||
self.try_merge_responses(candidates.into_iter())
|
||||
if let Some(merged) = self.try_merge_responses(&candidates) {
|
||||
Ok(merged)
|
||||
} else {
|
||||
self.flounder(&candidates)
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -289,43 +306,51 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
|
|||
debug!("added_goals={:?}", &self.nested_goals.goals[current_len..]);
|
||||
}
|
||||
|
||||
#[instrument(level = "debug", skip(self, responses))]
|
||||
/// Try to merge multiple possible ways to prove a goal, if that is not possible returns `None`.
|
||||
///
|
||||
/// In this case we tend to flounder and return ambiguity by calling `[EvalCtxt::flounder]`.
|
||||
#[instrument(level = "debug", skip(self), ret)]
|
||||
fn try_merge_responses(
|
||||
&mut self,
|
||||
responses: impl Iterator<Item = QueryResult<'tcx>>,
|
||||
) -> QueryResult<'tcx> {
|
||||
let candidates = responses.into_iter().flatten().collect::<Box<[_]>>();
|
||||
|
||||
if candidates.is_empty() {
|
||||
return Err(NoSolution);
|
||||
responses: &[CanonicalResponse<'tcx>],
|
||||
) -> Option<CanonicalResponse<'tcx>> {
|
||||
if responses.is_empty() {
|
||||
return None;
|
||||
}
|
||||
|
||||
// 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) {
|
||||
return Ok(one);
|
||||
let one = responses[0];
|
||||
if responses[1..].iter().all(|&resp| resp == one) {
|
||||
return Some(one);
|
||||
}
|
||||
|
||||
if let Some(response) = candidates.iter().find(|response| {
|
||||
response.value.certainty == Certainty::Yes
|
||||
&& response.has_no_inference_or_external_constraints()
|
||||
}) {
|
||||
return Ok(*response);
|
||||
}
|
||||
responses
|
||||
.iter()
|
||||
.find(|response| {
|
||||
response.value.certainty == Certainty::Yes
|
||||
&& response.has_no_inference_or_external_constraints()
|
||||
})
|
||||
.copied()
|
||||
}
|
||||
|
||||
let certainty = candidates.iter().fold(Certainty::AMBIGUOUS, |certainty, response| {
|
||||
/// If we fail to merge responses we flounder and return overflow or ambiguity.
|
||||
#[instrument(level = "debug", skip(self), ret)]
|
||||
fn flounder(&mut self, responses: &[CanonicalResponse<'tcx>]) -> QueryResult<'tcx> {
|
||||
if responses.is_empty() {
|
||||
return Err(NoSolution);
|
||||
}
|
||||
let certainty = responses.iter().fold(Certainty::AMBIGUOUS, |certainty, response| {
|
||||
certainty.unify_and(response.value.certainty)
|
||||
});
|
||||
// FIXME(-Ztrait-solver=next): We should take the intersection of the constraints on all the
|
||||
// responses and use that for the constraints of this ambiguous response.
|
||||
debug!(">1 response, bailing with {certainty:?}");
|
||||
let response = self.evaluate_added_goals_and_make_canonical_response(certainty);
|
||||
if let Ok(response) = &response {
|
||||
assert!(response.has_no_inference_or_external_constraints());
|
||||
}
|
||||
|
||||
response
|
||||
let response = self.evaluate_added_goals_and_make_canonical_response(certainty);
|
||||
if let Ok(response) = response {
|
||||
assert!(response.has_no_inference_or_external_constraints());
|
||||
Ok(response)
|
||||
} else {
|
||||
bug!("failed to make floundered response: {responses:?}");
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue