Skip to content

Commit 0626f2e

Browse files
nits
1 parent e1edefc commit 0626f2e

File tree

4 files changed

+47
-83
lines changed

4 files changed

+47
-83
lines changed

compiler/rustc_trait_selection/src/traits/coherence.rs

+34-82
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@ use crate::infer::InferOk;
99
use crate::solve::inspect;
1010
use crate::solve::inspect::{InspectGoal, ProofTreeInferCtxtExt, ProofTreeVisitor};
1111
use crate::traits::engine::TraitEngineExt;
12-
use crate::traits::outlives_bounds::InferCtxtExt as _;
1312
use crate::traits::query::evaluate_obligation::InferCtxtExt;
1413
use crate::traits::select::{IntercrateAmbiguityCause, TreatInductiveCycleAs};
1514
use crate::traits::structural_normalize::StructurallyNormalizeExt;
@@ -21,7 +20,7 @@ use crate::traits::{
2120
};
2221
use rustc_data_structures::fx::FxIndexSet;
2322
use rustc_errors::Diagnostic;
24-
use rustc_hir::def_id::{DefId, CRATE_DEF_ID, LOCAL_CRATE};
23+
use rustc_hir::def_id::{DefId, LOCAL_CRATE};
2524
use rustc_infer::infer::{DefineOpaqueTypes, InferCtxt, TyCtxtInferExt};
2625
use rustc_infer::traits::{util, TraitEngine};
2726
use rustc_middle::traits::query::NoSolution;
@@ -36,7 +35,6 @@ use rustc_session::lint::builtin::COINDUCTIVE_OVERLAP_IN_COHERENCE;
3635
use rustc_span::symbol::sym;
3736
use rustc_span::DUMMY_SP;
3837
use std::fmt::Debug;
39-
use std::iter;
4038
use std::ops::ControlFlow;
4139

4240
/// Whether we do the orphan check relative to this crate or
@@ -417,41 +415,8 @@ fn impl_intersection_has_negative_obligation(
417415

418416
plug_infer_with_placeholders(infcx, universe, (impl1_header.impl_args, impl2_header.impl_args));
419417

420-
for (predicate, _) in util::elaborate(
421-
tcx,
422-
tcx.predicates_of(impl2_def_id).instantiate(tcx, impl2_header.impl_args),
423-
) {
424-
let Some(negative_predicate) = predicate.as_predicate().flip_polarity(tcx) else {
425-
continue;
426-
};
427-
428-
let ref infcx = infcx.fork();
429-
let ocx = ObligationCtxt::new(infcx);
430-
431-
ocx.register_obligation(Obligation::new(
432-
tcx,
433-
ObligationCause::dummy(),
434-
param_env,
435-
negative_predicate,
436-
));
437-
if !ocx.select_all_or_error().is_empty() {
438-
continue;
439-
}
440-
441-
// FIXME: We could use the assumed_wf_types from both impls, I think,
442-
// if that wasn't implemented just for LocalDefId, and we'd need to do
443-
//the normalization ourselves since this is totally fallible...
444-
let outlives_env = OutlivesEnvironment::new(param_env);
445-
446-
let errors = infcx.resolve_regions(&outlives_env);
447-
if !errors.is_empty() {
448-
continue;
449-
}
450-
451-
return true;
452-
}
453-
454-
false
418+
util::elaborate(tcx, tcx.predicates_of(impl2_def_id).instantiate(tcx, impl2_header.impl_args))
419+
.any(|(clause, _)| try_prove_negated_where_clause(infcx, clause, param_env))
455420
}
456421

457422
fn plug_infer_with_placeholders<'tcx>(
@@ -566,60 +531,47 @@ fn plug_infer_with_placeholders<'tcx>(
566531
});
567532
}
568533

569-
/// Try to prove that a negative impl exist for the obligation or its supertraits.
570-
///
571-
/// If such a negative impl exists, then the obligation definitely must not hold
572-
/// due to coherence, even if it's not necessarily "knowable" in this crate. Any
573-
/// valid impl downstream would not be able to exist due to the overlapping
574-
/// negative impl.
575-
#[instrument(level = "debug", skip(infcx))]
576-
fn negative_impl_exists<'tcx>(
577-
infcx: &InferCtxt<'tcx>,
578-
o: &PredicateObligation<'tcx>,
579-
body_def_id: DefId,
580-
) -> bool {
581-
// Try to prove a negative obligation exists for super predicates
582-
for pred in util::elaborate(infcx.tcx, iter::once(o.predicate)) {
583-
if prove_negated_obligation(infcx.fork(), &o.with(infcx.tcx, pred), body_def_id) {
584-
return true;
585-
}
586-
}
587-
588-
false
589-
}
590-
591-
#[instrument(level = "debug", skip(infcx))]
592-
fn prove_negated_obligation<'tcx>(
593-
infcx: InferCtxt<'tcx>,
594-
o: &PredicateObligation<'tcx>,
595-
body_def_id: DefId,
534+
fn try_prove_negated_where_clause<'tcx>(
535+
root_infcx: &InferCtxt<'tcx>,
536+
clause: ty::Clause<'tcx>,
537+
param_env: ty::ParamEnv<'tcx>,
596538
) -> bool {
597-
let tcx = infcx.tcx;
598-
599-
let Some(o) = o.flip_polarity(tcx) else {
539+
let Some(negative_predicate) = clause.as_predicate().flip_polarity(root_infcx.tcx) else {
600540
return false;
601541
};
602542

603-
let param_env = o.param_env;
604-
let ocx = ObligationCtxt::new(&infcx);
605-
ocx.register_obligation(o);
606-
let errors = ocx.select_all_or_error();
607-
if !errors.is_empty() {
543+
// FIXME(with_negative_coherence): the infcx has region contraints from equating
544+
// the impl headers as requirements. Given that the only region constraints we
545+
// get are involving inference regions in the root, it shouldn't matter, but
546+
// still sus.
547+
//
548+
// We probably should just throw away the region obligations registered up until
549+
// now, or ideally use them as assumptions when proving the region obligations
550+
// that we get from proving the negative predicate below.
551+
let ref infcx = root_infcx.fork();
552+
let ocx = ObligationCtxt::new(infcx);
553+
554+
ocx.register_obligation(Obligation::new(
555+
infcx.tcx,
556+
ObligationCause::dummy(),
557+
param_env,
558+
negative_predicate,
559+
));
560+
if !ocx.select_all_or_error().is_empty() {
608561
return false;
609562
}
610563

611-
let body_def_id = body_def_id.as_local().unwrap_or(CRATE_DEF_ID);
564+
// FIXME: We could use the assumed_wf_types from both impls, I think,
565+
// if that wasn't implemented just for LocalDefId, and we'd need to do
566+
// the normalization ourselves since this is totally fallible...
567+
let outlives_env = OutlivesEnvironment::new(param_env);
612568

613-
let ocx = ObligationCtxt::new(&infcx);
614-
let Ok(wf_tys) = ocx.assumed_wf_types(param_env, body_def_id) else {
569+
let errors = infcx.resolve_regions(&outlives_env);
570+
if !errors.is_empty() {
615571
return false;
616-
};
572+
}
617573

618-
let outlives_env = OutlivesEnvironment::with_bounds(
619-
param_env,
620-
infcx.implied_bounds_tys(param_env, body_def_id, wf_tys),
621-
);
622-
infcx.resolve_regions(&outlives_env).is_empty()
574+
true
623575
}
624576

625577
/// Returns whether all impls which would apply to the `trait_ref`

compiler/rustc_trait_selection/src/traits/engine.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ impl<'tcx> TraitEngineExt<'tcx> for dyn TraitEngine<'tcx> {
4040
(TraitSolver::Classic | TraitSolver::Next | TraitSolver::NextCoherence, true) => {
4141
Box::new(NextFulfillmentCtxt::new(infcx))
4242
}
43-
_ => bug!(
43+
(TraitSolver::Next, false) => bug!(
4444
"incompatible combination of -Ztrait-solver flag ({:?}) and InferCtxt::next_trait_solver ({:?})",
4545
infcx.tcx.sess.opts.unstable_opts.trait_solver,
4646
infcx.next_trait_solver()

tests/ui/coherence/coherence-overlap-with-regions.rs

+6
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,11 @@
11
// known-bug: unknown
22

3+
// This fails because we currently perform negative coherence in coherence mode.
4+
// This means that when looking for a negative predicate, we also assemble a
5+
// coherence-unknowable predicate. Since confirming the negative impl has region
6+
// obligations, we don't prefer the impl over the unknowable predicate
7+
// unconditionally and instead flounder.
8+
39
#![feature(negative_impls)]
410
#![feature(rustc_attrs)]
511
#![feature(with_negative_coherence)]

tests/ui/coherence/negative-coherence-considering-regions.rs

+6
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,12 @@
11
// revisions: any_lt static_lt
22
//[static_lt] known-bug: unknown
33

4+
// This fails because we currently perform negative coherence in coherence mode.
5+
// This means that when looking for a negative predicate, we also assemble a
6+
// coherence-unknowable predicate. Since confirming the negative impl has region
7+
// obligations, we don't prefer the impl over the unknowable predicate
8+
// unconditionally and instead flounder.
9+
410
#![feature(negative_impls)]
511
#![feature(with_negative_coherence)]
612

0 commit comments

Comments
 (0)