Skip to content

Commit

Permalink
Fix coinductive coherence overlap checks
Browse files Browse the repository at this point in the history
  • Loading branch information
spastorino committed Mar 28, 2023
1 parent 408c732 commit 45ac61a
Show file tree
Hide file tree
Showing 5 changed files with 90 additions and 1 deletion.
42 changes: 42 additions & 0 deletions compiler/rustc_trait_selection/src/traits/coherence.rs
Original file line number Diff line number Diff line change
Expand Up @@ -120,6 +120,48 @@ pub fn overlapping_impls(
Some(overlap(selcx, skip_leak_check, impl1_def_id, impl2_def_id, overlap_mode).unwrap())
}

/// Given an impl_def_id that "positively" implement a trait, check if the "negative" holds.
pub fn negative_impl_holds(tcx: TyCtxt<'_>, impl_def_id: DefId, overlap_mode: OverlapMode) -> bool {
debug!("negative_impl_holds(impl1_header={:?}, overlap_mode={:?})", impl_def_id, overlap_mode);
// `for<T> (Vec<u32>, T): Trait`
let header = tcx.impl_trait_ref(impl_def_id).unwrap();

let infcx = tcx
.infer_ctxt()
.with_opaque_type_inference(DefiningAnchor::Bubble)
.intercrate(true)
.build();

// `[?t]`
let infer_substs = infcx.fresh_substs_for_item(DUMMY_SP, impl_def_id);

// `(Vec<u32>, ?t): Trait`
let trait_ref = header.subst(tcx, infer_substs);

// `(Vec<u32>, ?t): !Trait`
let trait_pred = tcx.mk_predicate(ty::Binder::dummy(ty::PredicateKind::Clause(
ty::Clause::Trait(ty::TraitPredicate {
trait_ref,
constness: ty::BoundConstness::NotConst,
polarity: ty::ImplPolarity::Negative,
}),
)));

// Ideally we would use param_env(impl_def_id) but that's unsound today.
let param_env = ty::ParamEnv::empty();

let selcx = &mut SelectionContext::new(&infcx);
selcx
.evaluate_root_obligation(&Obligation::new(
tcx,
ObligationCause::dummy(),
param_env,
trait_pred,
))
.expect("Overflow should be caught earlier in standard query mode")
.must_apply_modulo_regions()
}

fn with_fresh_ty_vars<'cx, 'tcx>(
selcx: &mut SelectionContext<'cx, 'tcx>,
param_env: ty::ParamEnv<'tcx>,
Expand Down
4 changes: 3 additions & 1 deletion compiler/rustc_trait_selection/src/traits/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,9 @@ pub use self::ImplSource::*;
pub use self::ObligationCauseCode::*;
pub use self::SelectionError::*;

pub use self::coherence::{add_placeholder_note, orphan_check, overlapping_impls};
pub use self::coherence::{
add_placeholder_note, negative_impl_holds, orphan_check, overlapping_impls,
};
pub use self::coherence::{OrphanCheckErr, OverlapResult};
pub use self::engine::{ObligationCtxt, TraitEngineExt};
pub use self::fulfill::{FulfillmentContext, PendingPredicateObligation};
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -226,6 +226,22 @@ fn overlap_check_considering_specialization<'tcx>(
return Ok(OverlapResult::SpecializeAll(replace_children));
}

if overlap_mode.use_negative_impl()
&& tcx.impl_polarity(impl_def_id) == ty::ImplPolarity::Positive
&& traits::negative_impl_holds(tcx, impl_def_id, overlap_mode)
{
let trait_ref = tcx.impl_trait_ref(impl_def_id).unwrap().skip_binder();
let self_ty = trait_ref.self_ty();

return Err(OverlapError {
with_impl: impl_def_id,
trait_ref,
self_ty: self_ty.has_concrete_skeleton().then_some(self_ty),
intercrate_ambiguity_causes: Default::default(),
involves_placeholder: false,
});
}

Ok(OverlapResult::NoOverlap(last_lint))
}

Expand Down
17 changes: 17 additions & 0 deletions tests/ui/coherence/coherence-overlap-negative-cycles.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
#![feature(trivial_bounds)]
#![feature(negative_impls)]
#![feature(rustc_attrs)]
#![feature(with_negative_coherence)]
#![allow(trivial_bounds)]

#[rustc_strict_coherence]
trait MyTrait {}

struct Foo {}

impl !MyTrait for Foo {}

impl MyTrait for Foo where Foo: MyTrait {}
//~^ ERROR: conflicting implementations of trait `MyTrait`

fn main() {}
12 changes: 12 additions & 0 deletions tests/ui/coherence/coherence-overlap-negative-cycles.stderr
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
error[E0119]: conflicting implementations of trait `MyTrait` for type `Foo`
--> $DIR/coherence-overlap-negative-cycles.rs:14:1
|
LL | impl MyTrait for Foo where Foo: MyTrait {}
| ^^^^^^^^^^^^^^^^^^^^
| |
| first implementation here
| conflicting implementation for `Foo`

error: aborting due to previous error

For more information about this error, try `rustc --explain E0119`.

0 comments on commit 45ac61a

Please sign in to comment.