do not attempt to prove unknowable goals

This commit is contained in:
lcnr 2024-09-02 14:50:50 +00:00
parent 6199b69c53
commit 6188aae369
5 changed files with 100 additions and 108 deletions

View File

@ -304,6 +304,11 @@ where
let mut candidates = vec![];
if self.solver_mode() == SolverMode::Coherence {
if let Ok(candidate) = self.consider_coherence_unknowable_candidate(goal) {
return vec![candidate];
}
}
self.assemble_impl_candidates(goal, &mut candidates);
self.assemble_builtin_impl_candidates(goal, &mut candidates);
@ -314,11 +319,8 @@ where
self.assemble_param_env_candidates(goal, &mut candidates);
match self.solver_mode() {
SolverMode::Normal => self.discard_impls_shadowed_by_env(goal, &mut candidates),
SolverMode::Coherence => {
self.assemble_coherence_unknowable_candidates(goal, &mut candidates)
}
if self.solver_mode() == SolverMode::Normal {
self.discard_impls_shadowed_by_env(goal, &mut candidates);
}
candidates
@ -682,38 +684,34 @@ where
/// also consider impls which may get added in a downstream or sibling crate
/// or which an upstream impl may add in a minor release.
///
/// To do so we add an ambiguous candidate in case such an unknown impl could
/// apply to the current goal.
/// To do so we return a single ambiguous candidate in case such an unknown
/// impl could apply to the current goal.
#[instrument(level = "trace", skip_all)]
fn assemble_coherence_unknowable_candidates<G: GoalKind<D>>(
fn consider_coherence_unknowable_candidate<G: GoalKind<D>>(
&mut self,
goal: Goal<I, G>,
candidates: &mut Vec<Candidate<I>>,
) {
let cx = self.cx();
candidates.extend(self.probe_trait_candidate(CandidateSource::CoherenceUnknowable).enter(
|ecx| {
let trait_ref = goal.predicate.trait_ref(cx);
if ecx.trait_ref_is_knowable(goal.param_env, trait_ref)? {
Err(NoSolution)
} else {
// While the trait bound itself may be unknowable, we may be able to
// prove that a super trait is not implemented. For this, we recursively
// prove the super trait bounds of the current goal.
//
// We skip the goal itself as that one would cycle.
let predicate: I::Predicate = trait_ref.upcast(cx);
ecx.add_goals(
GoalSource::Misc,
elaborate::elaborate(cx, [predicate])
.skip(1)
.map(|predicate| goal.with(cx, predicate)),
);
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
}
},
))
) -> Result<Candidate<I>, NoSolution> {
self.probe_trait_candidate(CandidateSource::CoherenceUnknowable).enter(|ecx| {
let cx = ecx.cx();
let trait_ref = goal.predicate.trait_ref(cx);
if ecx.trait_ref_is_knowable(goal.param_env, trait_ref)? {
Err(NoSolution)
} else {
// While the trait bound itself may be unknowable, we may be able to
// prove that a super trait is not implemented. For this, we recursively
// prove the super trait bounds of the current goal.
//
// We skip the goal itself as that one would cycle.
let predicate: I::Predicate = trait_ref.upcast(cx);
ecx.add_goals(
GoalSource::Misc,
elaborate::elaborate(cx, [predicate])
.skip(1)
.map(|predicate| goal.with(cx, predicate)),
);
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
}
})
}
/// If there's a where-bound for the current goal, do not use any impl candidates

View File

@ -29,6 +29,7 @@ use crate::infer::outlives::env::OutlivesEnvironment;
use crate::infer::InferOk;
use crate::solve::inspect::{InspectGoal, ProofTreeInferCtxtExt, ProofTreeVisitor};
use crate::solve::{deeply_normalize_for_diagnostics, inspect};
use crate::traits::query::evaluate_obligation::InferCtxtExt;
use crate::traits::select::IntercrateAmbiguityCause;
use crate::traits::{
util, FulfillmentErrorCode, NormalizeExt, Obligation, ObligationCause, PredicateObligation,
@ -624,14 +625,13 @@ impl<'a, 'tcx> ProofTreeVisitor<'tcx> for AmbiguityCausesVisitor<'a, 'tcx> {
// at ambiguous goals, as for others the coherence unknowable candidate
// was irrelevant.
match goal.result() {
Ok(Certainty::Maybe(_)) => {}
Ok(Certainty::Yes) | Err(NoSolution) => return,
Ok(Certainty::Maybe(_)) => {}
}
let Goal { param_env, predicate } = goal.goal();
// For bound predicates we simply call `infcx.enter_forall`
// and then prove the resulting predicate as a nested goal.
let Goal { param_env, predicate } = goal.goal();
let trait_ref = match predicate.kind().no_bound_vars() {
Some(ty::PredicateKind::Clause(ty::ClauseKind::Trait(tr))) => tr.trait_ref,
Some(ty::PredicateKind::Clause(ty::ClauseKind::Projection(proj)))
@ -645,7 +645,11 @@ impl<'a, 'tcx> ProofTreeVisitor<'tcx> for AmbiguityCausesVisitor<'a, 'tcx> {
_ => return,
};
// Add ambiguity causes for reservation impls.
if trait_ref.references_error() {
return;
}
let mut candidates = goal.candidates();
for cand in goal.candidates() {
if let inspect::ProbeKind::TraitCandidate {
source: CandidateSource::Impl(def_id),
@ -664,78 +668,68 @@ impl<'a, 'tcx> ProofTreeVisitor<'tcx> for AmbiguityCausesVisitor<'a, 'tcx> {
}
}
// Add ambiguity causes for unknowable goals.
let mut ambiguity_cause = None;
for cand in goal.candidates() {
if let inspect::ProbeKind::TraitCandidate {
source: CandidateSource::CoherenceUnknowable,
result: Ok(_),
} = cand.kind()
{
let lazily_normalize_ty = |mut ty: Ty<'tcx>| {
if matches!(ty.kind(), ty::Alias(..)) {
let ocx = ObligationCtxt::new(infcx);
ty = ocx
.structurally_normalize(&ObligationCause::dummy(), param_env, ty)
.map_err(|_| ())?;
if !ocx.select_where_possible().is_empty() {
return Err(());
}
}
Ok(ty)
};
// We also look for unknowable candidates. In case a goal is unknowable, there's
// always exactly 1 candidate.
let Some(cand) = candidates.pop() else {
return;
};
infcx.probe(|_| {
match trait_ref_is_knowable(infcx, trait_ref, lazily_normalize_ty) {
Err(()) => {}
Ok(Ok(())) => warn!("expected an unknowable trait ref: {trait_ref:?}"),
Ok(Err(conflict)) => {
if !trait_ref.references_error() {
// Normalize the trait ref for diagnostics, ignoring any errors if this fails.
let trait_ref =
deeply_normalize_for_diagnostics(infcx, param_env, trait_ref);
let inspect::ProbeKind::TraitCandidate {
source: CandidateSource::CoherenceUnknowable,
result: Ok(_),
} = cand.kind()
else {
return;
};
let self_ty = trait_ref.self_ty();
let self_ty = self_ty.has_concrete_skeleton().then(|| self_ty);
ambiguity_cause = Some(match conflict {
Conflict::Upstream => {
IntercrateAmbiguityCause::UpstreamCrateUpdate {
trait_ref,
self_ty,
}
}
Conflict::Downstream => {
IntercrateAmbiguityCause::DownstreamCrate {
trait_ref,
self_ty,
}
}
});
}
}
}
})
} else {
match cand.result() {
// We only add an ambiguity cause if the goal would otherwise
// result in an error.
//
// FIXME: While this matches the behavior of the
// old solver, it is not the only way in which the unknowable
// candidates *weaken* coherence, they can also force otherwise
// successful normalization to be ambiguous.
Ok(Certainty::Maybe(_) | Certainty::Yes) => {
ambiguity_cause = None;
break;
}
Err(NoSolution) => continue,
let lazily_normalize_ty = |mut ty: Ty<'tcx>| {
if matches!(ty.kind(), ty::Alias(..)) {
let ocx = ObligationCtxt::new(infcx);
ty = ocx
.structurally_normalize(&ObligationCause::dummy(), param_env, ty)
.map_err(|_| ())?;
if !ocx.select_where_possible().is_empty() {
return Err(());
}
}
}
Ok(ty)
};
if let Some(ambiguity_cause) = ambiguity_cause {
self.causes.insert(ambiguity_cause);
}
infcx.probe(|_| {
let conflict = match trait_ref_is_knowable(infcx, trait_ref, lazily_normalize_ty) {
Err(()) => return,
Ok(Ok(())) => {
warn!("expected an unknowable trait ref: {trait_ref:?}");
return;
}
Ok(Err(conflict)) => conflict,
};
// It is only relevant that a goal is unknowable if it would have otherwise
// failed.
let non_intercrate_infcx = infcx.fork_with_intercrate(false);
if non_intercrate_infcx.predicate_may_hold(&Obligation::new(
infcx.tcx,
ObligationCause::dummy(),
param_env,
predicate,
)) {
return;
}
// Normalize the trait ref for diagnostics, ignoring any errors if this fails.
let trait_ref = deeply_normalize_for_diagnostics(infcx, param_env, trait_ref);
let self_ty = trait_ref.self_ty();
let self_ty = self_ty.has_concrete_skeleton().then(|| self_ty);
self.causes.insert(match conflict {
Conflict::Upstream => {
IntercrateAmbiguityCause::UpstreamCrateUpdate { trait_ref, self_ty }
}
Conflict::Downstream => {
IntercrateAmbiguityCause::DownstreamCrate { trait_ref, self_ty }
}
});
});
}
}

View File

@ -58,7 +58,7 @@ pub enum Reveal {
All,
}
#[derive(Debug, Clone, Copy)]
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum SolverMode {
/// Ordinary trait solving, using everywhere except for coherence.
Normal,

View File

@ -7,7 +7,7 @@ LL |
LL | impl<S: Iterator> MyTrait<S> for (Box<<(MyType,) as Mirror>::Assoc>, S::Item) {}
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ conflicting implementation for `(Box<(MyType,)>, <_ as Iterator>::Item)`
|
= note: upstream crates may add a new impl of trait `std::clone::Clone` for type `(MyType,)` in future versions
= note: upstream crates may add a new impl of trait `std::clone::Clone` for type `std::boxed::Box<(MyType,)>` in future versions
= note: upstream crates may add a new impl of trait `std::marker::Copy` for type `std::boxed::Box<(MyType,)>` in future versions
error: aborting due to 1 previous error

View File

@ -18,6 +18,6 @@ impl<S: Iterator> MyTrait<S> for (Box<<(MyType,) as Mirror>::Assoc>, S::Item) {}
//~^ ERROR conflicting implementations of trait `MyTrait<_>` for type `(Box<(MyType,)>,
//~| NOTE conflicting implementation for `(Box<(MyType,)>,
//~| NOTE upstream crates may add a new impl of trait `std::marker::Copy` for type `std::boxed::Box<(MyType,)>` in future versions
//[next]~| NOTE upstream crates may add a new impl of trait `std::clone::Clone` for type `(MyType,)` in future versions
//[next]~| NOTE upstream crates may add a new impl of trait `std::clone::Clone` for type `std::boxed::Box<(MyType,)>` in future versions
fn main() {}