Skip to content

Commit

Permalink
Rollup merge of rust-lang#93175 - spastorino:negative-traits-coherenc…
Browse files Browse the repository at this point in the history
…e-new, r=nikomatsakis

Implement stable overlap check considering negative traits

This PR implement the new disjointness rules for overlap check described in https://rust-lang.github.io/negative-impls-initiative/explainer/coherence-check.html#new-disjointness-rules

r? `@nikomatsakis`
  • Loading branch information
matthiaskrgr authored Jan 25, 2022
2 parents fa16356 + 8189bac commit e4de1b5
Show file tree
Hide file tree
Showing 5 changed files with 229 additions and 61 deletions.
1 change: 1 addition & 0 deletions compiler/rustc_feature/src/builtin_attrs.rs
Original file line number Diff line number Diff line change
Expand Up @@ -697,6 +697,7 @@ pub const BUILTIN_ATTRIBUTES: &[BuiltinAttribute] = &[
rustc_attr!(TEST, rustc_capture_analysis, Normal, template!(Word), WarnFollowing),
rustc_attr!(TEST, rustc_insignificant_dtor, Normal, template!(Word), WarnFollowing),
rustc_attr!(TEST, rustc_strict_coherence, Normal, template!(Word), WarnFollowing),
rustc_attr!(TEST, rustc_with_negative_coherence, Normal, template!(Word), WarnFollowing),
rustc_attr!(TEST, rustc_variance, Normal, template!(Word), WarnFollowing),
rustc_attr!(TEST, rustc_layout, Normal, template!(List: "field1, field2, ..."), WarnFollowing),
rustc_attr!(TEST, rustc_regions, Normal, template!(Word), WarnFollowing),
Expand Down
1 change: 1 addition & 0 deletions compiler/rustc_span/src/symbol.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1204,6 +1204,7 @@ symbols! {
rustc_trivial_field_reads,
rustc_unsafe_specialization_marker,
rustc_variance,
rustc_with_negative_coherence,
rustdoc,
rustdoc_internals,
rustfmt,
Expand Down
262 changes: 201 additions & 61 deletions compiler/rustc_trait_selection/src/traits/coherence.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,11 @@
use crate::infer::{CombinedSnapshot, InferOk, TyCtxtInferExt};
use crate::traits::query::evaluate_obligation::InferCtxtExt;
use crate::traits::select::IntercrateAmbiguityCause;
use crate::traits::util::impl_trait_ref_and_oblig;
use crate::traits::SkipLeakCheck;
use crate::traits::{
self, Normalized, Obligation, ObligationCause, PredicateObligation, SelectionContext,
self, FulfillmentContext, Normalized, Obligation, ObligationCause, PredicateObligation,
PredicateObligations, SelectionContext,
};
use rustc_hir::def_id::{DefId, LOCAL_CRATE};
use rustc_middle::ty::fast_reject::{self, SimplifyParams, StripReferences};
Expand Down Expand Up @@ -135,45 +137,83 @@ fn with_fresh_ty_vars<'cx, 'tcx>(
header
}

/// What kind of overlap check are we doing -- this exists just for testing and feature-gating
/// purposes.
#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
enum OverlapMode {
/// The 1.0 rules (either types fail to unify, or where clauses are not implemented for crate-local types)
Stable,
/// Feature-gated test: Stable, *or* there is an explicit negative impl that rules out one of the where-clauses.
WithNegative,
/// Just check for negative impls, not for "where clause not implemented": used for testing.
Strict,
}

impl OverlapMode {
fn use_negative_impl(&self) -> bool {
*self == OverlapMode::Strict || *self == OverlapMode::WithNegative
}

fn use_implicit_negative(&self) -> bool {
*self == OverlapMode::Stable || *self == OverlapMode::WithNegative
}
}

fn overlap_mode<'tcx>(tcx: TyCtxt<'tcx>, impl1_def_id: DefId, impl2_def_id: DefId) -> OverlapMode {
if tcx.has_attr(impl1_def_id, sym::rustc_strict_coherence)
!= tcx.has_attr(impl2_def_id, sym::rustc_strict_coherence)
{
bug!("Use strict coherence on both impls",);
}

if tcx.has_attr(impl1_def_id, sym::rustc_with_negative_coherence)
!= tcx.has_attr(impl2_def_id, sym::rustc_with_negative_coherence)
{
bug!("Use with negative coherence on both impls",);
}

if tcx.has_attr(impl1_def_id, sym::rustc_strict_coherence) {
OverlapMode::Strict
} else if tcx.has_attr(impl1_def_id, sym::rustc_with_negative_coherence) {
OverlapMode::WithNegative
} else {
OverlapMode::Stable
}
}

/// Can both impl `a` and impl `b` be satisfied by a common type (including
/// where-clauses)? If so, returns an `ImplHeader` that unifies the two impls.
fn overlap<'cx, 'tcx>(
selcx: &mut SelectionContext<'cx, 'tcx>,
skip_leak_check: SkipLeakCheck,
a_def_id: DefId,
b_def_id: DefId,
impl1_def_id: DefId,
impl2_def_id: DefId,
) -> Option<OverlapResult<'tcx>> {
debug!("overlap(a_def_id={:?}, b_def_id={:?})", a_def_id, b_def_id);
debug!("overlap(impl1_def_id={:?}, impl2_def_id={:?})", impl1_def_id, impl2_def_id);

selcx.infcx().probe_maybe_skip_leak_check(skip_leak_check.is_yes(), |snapshot| {
overlap_within_probe(selcx, skip_leak_check, a_def_id, b_def_id, snapshot)
overlap_within_probe(selcx, skip_leak_check, impl1_def_id, impl2_def_id, snapshot)
})
}

fn overlap_within_probe<'cx, 'tcx>(
selcx: &mut SelectionContext<'cx, 'tcx>,
skip_leak_check: SkipLeakCheck,
a_def_id: DefId,
b_def_id: DefId,
impl1_def_id: DefId,
impl2_def_id: DefId,
snapshot: &CombinedSnapshot<'_, 'tcx>,
) -> Option<OverlapResult<'tcx>> {
fn loose_check<'cx, 'tcx>(
selcx: &mut SelectionContext<'cx, 'tcx>,
o: &PredicateObligation<'tcx>,
) -> bool {
!selcx.predicate_may_hold_fatal(o)
}
let infcx = selcx.infcx();
let tcx = infcx.tcx;

fn strict_check<'cx, 'tcx>(
selcx: &SelectionContext<'cx, 'tcx>,
o: &PredicateObligation<'tcx>,
) -> bool {
let infcx = selcx.infcx();
let tcx = infcx.tcx;
o.flip_polarity(tcx)
.as_ref()
.map(|o| selcx.infcx().predicate_must_hold_modulo_regions(o))
.unwrap_or(false)
let overlap_mode = overlap_mode(tcx, impl1_def_id, impl2_def_id);

if overlap_mode.use_negative_impl() {
if negative_impl(selcx, impl1_def_id, impl2_def_id)
|| negative_impl(selcx, impl2_def_id, impl1_def_id)
{
return None;
}
}

// For the purposes of this check, we don't bring any placeholder
Expand All @@ -182,26 +222,61 @@ fn overlap_within_probe<'cx, 'tcx>(
// empty environment.
let param_env = ty::ParamEnv::empty();

let a_impl_header = with_fresh_ty_vars(selcx, param_env, a_def_id);
let b_impl_header = with_fresh_ty_vars(selcx, param_env, b_def_id);
let impl1_header = with_fresh_ty_vars(selcx, param_env, impl1_def_id);
let impl2_header = with_fresh_ty_vars(selcx, param_env, impl2_def_id);

debug!("overlap: a_impl_header={:?}", a_impl_header);
debug!("overlap: b_impl_header={:?}", b_impl_header);
debug!("overlap: impl1_header={:?}", impl1_header);
debug!("overlap: impl2_header={:?}", impl2_header);

// Do `a` and `b` unify? If not, no overlap.
let obligations = match selcx
.infcx()
.at(&ObligationCause::dummy(), param_env)
.eq_impl_headers(&a_impl_header, &b_impl_header)
{
Ok(InferOk { obligations, value: () }) => obligations,
Err(_) => {
let obligations = equate_impl_headers(selcx, &impl1_header, &impl2_header)?;
debug!("overlap: unification check succeeded");

if overlap_mode.use_implicit_negative() {
if implicit_negative(selcx, param_env, &impl1_header, impl2_header, obligations) {
return None;
}
};
}

debug!("overlap: unification check succeeded");
if !skip_leak_check.is_yes() {
if infcx.leak_check(true, snapshot).is_err() {
debug!("overlap: leak check failed");
return None;
}
}

let intercrate_ambiguity_causes = selcx.take_intercrate_ambiguity_causes();
debug!("overlap: intercrate_ambiguity_causes={:#?}", intercrate_ambiguity_causes);

let involves_placeholder =
matches!(selcx.infcx().region_constraints_added_in_snapshot(snapshot), Some(true));

let impl_header = selcx.infcx().resolve_vars_if_possible(impl1_header);
Some(OverlapResult { impl_header, intercrate_ambiguity_causes, involves_placeholder })
}

fn equate_impl_headers<'cx, 'tcx>(
selcx: &mut SelectionContext<'cx, 'tcx>,
impl1_header: &ty::ImplHeader<'tcx>,
impl2_header: &ty::ImplHeader<'tcx>,
) -> Option<PredicateObligations<'tcx>> {
// Do `a` and `b` unify? If not, no overlap.
selcx
.infcx()
.at(&ObligationCause::dummy(), ty::ParamEnv::empty())
.eq_impl_headers(impl1_header, impl2_header)
.map(|infer_ok| infer_ok.obligations)
.ok()
}

/// Given impl1 and impl2 check if both impls can be satisfied by a common type (including
/// where-clauses) If so, return false, otherwise return true, they are disjoint.
fn implicit_negative<'cx, 'tcx>(
selcx: &mut SelectionContext<'cx, 'tcx>,
param_env: ty::ParamEnv<'tcx>,
impl1_header: &ty::ImplHeader<'tcx>,
impl2_header: ty::ImplHeader<'tcx>,
obligations: PredicateObligations<'tcx>,
) -> bool {
// There's no overlap if obligations are unsatisfiable or if the obligation negated is
// satisfied.
//
Expand All @@ -225,11 +300,11 @@ fn overlap_within_probe<'cx, 'tcx>(
// at some point an impl for `&'?a str: Error` could be added.
let infcx = selcx.infcx();
let tcx = infcx.tcx;
let opt_failing_obligation = a_impl_header
let opt_failing_obligation = impl1_header
.predicates
.iter()
.copied()
.chain(b_impl_header.predicates)
.chain(impl2_header.predicates)
.map(|p| infcx.resolve_vars_if_possible(p))
.map(|p| Obligation {
cause: ObligationCause::dummy(),
Expand All @@ -239,40 +314,105 @@ fn overlap_within_probe<'cx, 'tcx>(
})
.chain(obligations)
.find(|o| {
// if both impl headers are set to strict coherence it means that this will be accepted
// only if it's stated that T: !Trait. So only prove that the negated obligation holds.
if tcx.has_attr(a_def_id, sym::rustc_strict_coherence)
&& tcx.has_attr(b_def_id, sym::rustc_strict_coherence)
{
strict_check(selcx, o)
} else {
loose_check(selcx, o) || tcx.features().negative_impls && strict_check(selcx, o)
}
loose_check(selcx, o) || tcx.features().negative_impls && negative_impl_exists(selcx, o)
});
// FIXME: the call to `selcx.predicate_may_hold_fatal` above should be ported
// to the canonical trait query form, `infcx.predicate_may_hold`, once
// the new system supports intercrate mode (which coherence needs).

if let Some(failing_obligation) = opt_failing_obligation {
debug!("overlap: obligation unsatisfiable {:?}", failing_obligation);
return None;
true
} else {
false
}
}

if !skip_leak_check.is_yes() {
if infcx.leak_check(true, snapshot).is_err() {
debug!("overlap: leak check failed");
return None;
}
}
/// Given impl1 and impl2 check if both impls are never satisfied by a common type (including
/// where-clauses) If so, return true, they are disjoint and false otherwise.
fn negative_impl<'cx, 'tcx>(
selcx: &mut SelectionContext<'cx, 'tcx>,
impl1_def_id: DefId,
impl2_def_id: DefId,
) -> bool {
let tcx = selcx.infcx().tcx;

let impl_header = selcx.infcx().resolve_vars_if_possible(a_impl_header);
let intercrate_ambiguity_causes = selcx.take_intercrate_ambiguity_causes();
debug!("overlap: intercrate_ambiguity_causes={:#?}", intercrate_ambiguity_causes);
// create a parameter environment corresponding to a (placeholder) instantiation of impl1
let impl1_env = tcx.param_env(impl1_def_id);
let impl1_trait_ref = tcx.impl_trait_ref(impl1_def_id).unwrap();

let involves_placeholder =
matches!(selcx.infcx().region_constraints_added_in_snapshot(snapshot), Some(true));
// Create an infcx, taking the predicates of impl1 as assumptions:
tcx.infer_ctxt().enter(|infcx| {
// Normalize the trait reference. The WF rules ought to ensure
// that this always succeeds.
let impl1_trait_ref = match traits::fully_normalize(
&infcx,
FulfillmentContext::new(),
ObligationCause::dummy(),
impl1_env,
impl1_trait_ref,
) {
Ok(impl1_trait_ref) => impl1_trait_ref,
Err(err) => {
bug!("failed to fully normalize {:?}: {:?}", impl1_trait_ref, err);
}
};

// Attempt to prove that impl2 applies, given all of the above.
let selcx = &mut SelectionContext::new(&infcx);
let impl2_substs = infcx.fresh_substs_for_item(DUMMY_SP, impl2_def_id);
let (impl2_trait_ref, obligations) =
impl_trait_ref_and_oblig(selcx, impl1_env, impl2_def_id, impl2_substs);

// do the impls unify? If not, not disjoint.
let more_obligations = match infcx
.at(&ObligationCause::dummy(), impl1_env)
.eq(impl1_trait_ref, impl2_trait_ref)
{
Ok(InferOk { obligations, .. }) => obligations,
Err(_) => {
debug!(
"explicit_disjoint: {:?} does not unify with {:?}",
impl1_trait_ref, impl2_trait_ref
);
return false;
}
};

Some(OverlapResult { impl_header, intercrate_ambiguity_causes, involves_placeholder })
let opt_failing_obligation = obligations
.into_iter()
.chain(more_obligations)
.find(|o| negative_impl_exists(selcx, o));

if let Some(failing_obligation) = opt_failing_obligation {
debug!("overlap: obligation unsatisfiable {:?}", failing_obligation);
true
} else {
false
}
})
}

fn loose_check<'cx, 'tcx>(
selcx: &mut SelectionContext<'cx, 'tcx>,
o: &PredicateObligation<'tcx>,
) -> bool {
!selcx.predicate_may_hold_fatal(o)
}

fn negative_impl_exists<'cx, 'tcx>(
selcx: &SelectionContext<'cx, 'tcx>,
o: &PredicateObligation<'tcx>,
) -> bool {
let infcx = selcx.infcx();
let tcx = infcx.tcx;
o.flip_polarity(tcx)
.as_ref()
.map(|o| {
// FIXME This isn't quite correct, regions should be included
selcx.infcx().predicate_must_hold_modulo_regions(o)
})
.unwrap_or(false)
}

pub fn trait_ref_is_knowable<'tcx>(
Expand Down
8 changes: 8 additions & 0 deletions src/test/ui/coherence/auxiliary/option_future.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
#![crate_type = "lib"]
#![feature(negative_impls)]
#![feature(rustc_attrs)]

pub trait Future {}

#[rustc_with_negative_coherence]
impl<E> !Future for Option<E> where E: Sized {}
18 changes: 18 additions & 0 deletions src/test/ui/coherence/coherence-overlap-negative-trait2.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
// check-pass
// aux-build:option_future.rs
//
// Check that if we promise to not impl what would overlap it doesn't actually overlap

#![feature(rustc_attrs)]

extern crate option_future as lib;
use lib::Future;

trait Termination {}

#[rustc_with_negative_coherence]
impl<E> Termination for Option<E> where E: Sized {}
#[rustc_with_negative_coherence]
impl<F> Termination for F where F: Future + Sized {}

fn main() {}

0 comments on commit e4de1b5

Please sign in to comment.