nits
This commit is contained in:
parent
e1edefc137
commit
0626f2e7d0
@ -9,7 +9,6 @@
|
|||||||
use crate::solve::inspect;
|
use crate::solve::inspect;
|
||||||
use crate::solve::inspect::{InspectGoal, ProofTreeInferCtxtExt, ProofTreeVisitor};
|
use crate::solve::inspect::{InspectGoal, ProofTreeInferCtxtExt, ProofTreeVisitor};
|
||||||
use crate::traits::engine::TraitEngineExt;
|
use crate::traits::engine::TraitEngineExt;
|
||||||
use crate::traits::outlives_bounds::InferCtxtExt as _;
|
|
||||||
use crate::traits::query::evaluate_obligation::InferCtxtExt;
|
use crate::traits::query::evaluate_obligation::InferCtxtExt;
|
||||||
use crate::traits::select::{IntercrateAmbiguityCause, TreatInductiveCycleAs};
|
use crate::traits::select::{IntercrateAmbiguityCause, TreatInductiveCycleAs};
|
||||||
use crate::traits::structural_normalize::StructurallyNormalizeExt;
|
use crate::traits::structural_normalize::StructurallyNormalizeExt;
|
||||||
@ -21,7 +20,7 @@
|
|||||||
};
|
};
|
||||||
use rustc_data_structures::fx::FxIndexSet;
|
use rustc_data_structures::fx::FxIndexSet;
|
||||||
use rustc_errors::Diagnostic;
|
use rustc_errors::Diagnostic;
|
||||||
use rustc_hir::def_id::{DefId, CRATE_DEF_ID, LOCAL_CRATE};
|
use rustc_hir::def_id::{DefId, LOCAL_CRATE};
|
||||||
use rustc_infer::infer::{DefineOpaqueTypes, InferCtxt, TyCtxtInferExt};
|
use rustc_infer::infer::{DefineOpaqueTypes, InferCtxt, TyCtxtInferExt};
|
||||||
use rustc_infer::traits::{util, TraitEngine};
|
use rustc_infer::traits::{util, TraitEngine};
|
||||||
use rustc_middle::traits::query::NoSolution;
|
use rustc_middle::traits::query::NoSolution;
|
||||||
@ -36,7 +35,6 @@
|
|||||||
use rustc_span::symbol::sym;
|
use rustc_span::symbol::sym;
|
||||||
use rustc_span::DUMMY_SP;
|
use rustc_span::DUMMY_SP;
|
||||||
use std::fmt::Debug;
|
use std::fmt::Debug;
|
||||||
use std::iter;
|
|
||||||
use std::ops::ControlFlow;
|
use std::ops::ControlFlow;
|
||||||
|
|
||||||
/// Whether we do the orphan check relative to this crate or
|
/// Whether we do the orphan check relative to this crate or
|
||||||
@ -417,41 +415,8 @@ fn impl_intersection_has_negative_obligation(
|
|||||||
|
|
||||||
plug_infer_with_placeholders(infcx, universe, (impl1_header.impl_args, impl2_header.impl_args));
|
plug_infer_with_placeholders(infcx, universe, (impl1_header.impl_args, impl2_header.impl_args));
|
||||||
|
|
||||||
for (predicate, _) in util::elaborate(
|
util::elaborate(tcx, tcx.predicates_of(impl2_def_id).instantiate(tcx, impl2_header.impl_args))
|
||||||
tcx,
|
.any(|(clause, _)| try_prove_negated_where_clause(infcx, clause, param_env))
|
||||||
tcx.predicates_of(impl2_def_id).instantiate(tcx, impl2_header.impl_args),
|
|
||||||
) {
|
|
||||||
let Some(negative_predicate) = predicate.as_predicate().flip_polarity(tcx) else {
|
|
||||||
continue;
|
|
||||||
};
|
|
||||||
|
|
||||||
let ref infcx = infcx.fork();
|
|
||||||
let ocx = ObligationCtxt::new(infcx);
|
|
||||||
|
|
||||||
ocx.register_obligation(Obligation::new(
|
|
||||||
tcx,
|
|
||||||
ObligationCause::dummy(),
|
|
||||||
param_env,
|
|
||||||
negative_predicate,
|
|
||||||
));
|
|
||||||
if !ocx.select_all_or_error().is_empty() {
|
|
||||||
continue;
|
|
||||||
}
|
|
||||||
|
|
||||||
// FIXME: We could use the assumed_wf_types from both impls, I think,
|
|
||||||
// if that wasn't implemented just for LocalDefId, and we'd need to do
|
|
||||||
//the normalization ourselves since this is totally fallible...
|
|
||||||
let outlives_env = OutlivesEnvironment::new(param_env);
|
|
||||||
|
|
||||||
let errors = infcx.resolve_regions(&outlives_env);
|
|
||||||
if !errors.is_empty() {
|
|
||||||
continue;
|
|
||||||
}
|
|
||||||
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
|
|
||||||
false
|
|
||||||
}
|
}
|
||||||
|
|
||||||
fn plug_infer_with_placeholders<'tcx>(
|
fn plug_infer_with_placeholders<'tcx>(
|
||||||
@ -566,60 +531,47 @@ fn visit_region(&mut self, r: ty::Region<'tcx>) -> ControlFlow<Self::BreakTy> {
|
|||||||
});
|
});
|
||||||
}
|
}
|
||||||
|
|
||||||
/// Try to prove that a negative impl exist for the obligation or its supertraits.
|
fn try_prove_negated_where_clause<'tcx>(
|
||||||
///
|
root_infcx: &InferCtxt<'tcx>,
|
||||||
/// If such a negative impl exists, then the obligation definitely must not hold
|
clause: ty::Clause<'tcx>,
|
||||||
/// due to coherence, even if it's not necessarily "knowable" in this crate. Any
|
param_env: ty::ParamEnv<'tcx>,
|
||||||
/// valid impl downstream would not be able to exist due to the overlapping
|
|
||||||
/// negative impl.
|
|
||||||
#[instrument(level = "debug", skip(infcx))]
|
|
||||||
fn negative_impl_exists<'tcx>(
|
|
||||||
infcx: &InferCtxt<'tcx>,
|
|
||||||
o: &PredicateObligation<'tcx>,
|
|
||||||
body_def_id: DefId,
|
|
||||||
) -> bool {
|
) -> bool {
|
||||||
// Try to prove a negative obligation exists for super predicates
|
let Some(negative_predicate) = clause.as_predicate().flip_polarity(root_infcx.tcx) else {
|
||||||
for pred in util::elaborate(infcx.tcx, iter::once(o.predicate)) {
|
|
||||||
if prove_negated_obligation(infcx.fork(), &o.with(infcx.tcx, pred), body_def_id) {
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
false
|
|
||||||
}
|
|
||||||
|
|
||||||
#[instrument(level = "debug", skip(infcx))]
|
|
||||||
fn prove_negated_obligation<'tcx>(
|
|
||||||
infcx: InferCtxt<'tcx>,
|
|
||||||
o: &PredicateObligation<'tcx>,
|
|
||||||
body_def_id: DefId,
|
|
||||||
) -> bool {
|
|
||||||
let tcx = infcx.tcx;
|
|
||||||
|
|
||||||
let Some(o) = o.flip_polarity(tcx) else {
|
|
||||||
return false;
|
return false;
|
||||||
};
|
};
|
||||||
|
|
||||||
let param_env = o.param_env;
|
// FIXME(with_negative_coherence): the infcx has region contraints from equating
|
||||||
let ocx = ObligationCtxt::new(&infcx);
|
// the impl headers as requirements. Given that the only region constraints we
|
||||||
ocx.register_obligation(o);
|
// get are involving inference regions in the root, it shouldn't matter, but
|
||||||
let errors = ocx.select_all_or_error();
|
// still sus.
|
||||||
|
//
|
||||||
|
// We probably should just throw away the region obligations registered up until
|
||||||
|
// now, or ideally use them as assumptions when proving the region obligations
|
||||||
|
// that we get from proving the negative predicate below.
|
||||||
|
let ref infcx = root_infcx.fork();
|
||||||
|
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() {
|
||||||
|
return false;
|
||||||
|
}
|
||||||
|
|
||||||
|
// FIXME: We could use the assumed_wf_types from both impls, I think,
|
||||||
|
// if that wasn't implemented just for LocalDefId, and we'd need to do
|
||||||
|
// the normalization ourselves since this is totally fallible...
|
||||||
|
let outlives_env = OutlivesEnvironment::new(param_env);
|
||||||
|
|
||||||
|
let errors = infcx.resolve_regions(&outlives_env);
|
||||||
if !errors.is_empty() {
|
if !errors.is_empty() {
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
let body_def_id = body_def_id.as_local().unwrap_or(CRATE_DEF_ID);
|
true
|
||||||
|
|
||||||
let ocx = ObligationCtxt::new(&infcx);
|
|
||||||
let Ok(wf_tys) = ocx.assumed_wf_types(param_env, body_def_id) else {
|
|
||||||
return false;
|
|
||||||
};
|
|
||||||
|
|
||||||
let outlives_env = OutlivesEnvironment::with_bounds(
|
|
||||||
param_env,
|
|
||||||
infcx.implied_bounds_tys(param_env, body_def_id, wf_tys),
|
|
||||||
);
|
|
||||||
infcx.resolve_regions(&outlives_env).is_empty()
|
|
||||||
}
|
}
|
||||||
|
|
||||||
/// Returns whether all impls which would apply to the `trait_ref`
|
/// Returns whether all impls which would apply to the `trait_ref`
|
||||||
|
@ -40,7 +40,7 @@ fn new(infcx: &InferCtxt<'tcx>) -> Box<Self> {
|
|||||||
(TraitSolver::Classic | TraitSolver::Next | TraitSolver::NextCoherence, true) => {
|
(TraitSolver::Classic | TraitSolver::Next | TraitSolver::NextCoherence, true) => {
|
||||||
Box::new(NextFulfillmentCtxt::new(infcx))
|
Box::new(NextFulfillmentCtxt::new(infcx))
|
||||||
}
|
}
|
||||||
_ => bug!(
|
(TraitSolver::Next, false) => bug!(
|
||||||
"incompatible combination of -Ztrait-solver flag ({:?}) and InferCtxt::next_trait_solver ({:?})",
|
"incompatible combination of -Ztrait-solver flag ({:?}) and InferCtxt::next_trait_solver ({:?})",
|
||||||
infcx.tcx.sess.opts.unstable_opts.trait_solver,
|
infcx.tcx.sess.opts.unstable_opts.trait_solver,
|
||||||
infcx.next_trait_solver()
|
infcx.next_trait_solver()
|
||||||
|
@ -1,5 +1,11 @@
|
|||||||
// known-bug: unknown
|
// known-bug: unknown
|
||||||
|
|
||||||
|
// This fails because we currently perform negative coherence in coherence mode.
|
||||||
|
// This means that when looking for a negative predicate, we also assemble a
|
||||||
|
// coherence-unknowable predicate. Since confirming the negative impl has region
|
||||||
|
// obligations, we don't prefer the impl over the unknowable predicate
|
||||||
|
// unconditionally and instead flounder.
|
||||||
|
|
||||||
#![feature(negative_impls)]
|
#![feature(negative_impls)]
|
||||||
#![feature(rustc_attrs)]
|
#![feature(rustc_attrs)]
|
||||||
#![feature(with_negative_coherence)]
|
#![feature(with_negative_coherence)]
|
||||||
|
@ -1,6 +1,12 @@
|
|||||||
// revisions: any_lt static_lt
|
// revisions: any_lt static_lt
|
||||||
//[static_lt] known-bug: unknown
|
//[static_lt] known-bug: unknown
|
||||||
|
|
||||||
|
// This fails because we currently perform negative coherence in coherence mode.
|
||||||
|
// This means that when looking for a negative predicate, we also assemble a
|
||||||
|
// coherence-unknowable predicate. Since confirming the negative impl has region
|
||||||
|
// obligations, we don't prefer the impl over the unknowable predicate
|
||||||
|
// unconditionally and instead flounder.
|
||||||
|
|
||||||
#![feature(negative_impls)]
|
#![feature(negative_impls)]
|
||||||
#![feature(with_negative_coherence)]
|
#![feature(with_negative_coherence)]
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user