Skip to content

Commit

Permalink
Auto merge of rust-lang#98542 - jackh726:coinductive-wf, r=oli-obk
Browse files Browse the repository at this point in the history
Make empty bounds lower to `WellFormed` and make `WellFormed` coinductive

r? rust-lang/types
  • Loading branch information
bors committed Jun 29, 2022
2 parents 126e3df + bd298ad commit 116edb6
Show file tree
Hide file tree
Showing 8 changed files with 130 additions and 26 deletions.
1 change: 1 addition & 0 deletions compiler/rustc_privacy/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -154,6 +154,7 @@ where
}
ControlFlow::CONTINUE
}
ty::PredicateKind::WellFormed(arg) => arg.visit_with(self),
_ => bug!("unexpected predicate: {:?}", predicate),
}
}
Expand Down
115 changes: 100 additions & 15 deletions compiler/rustc_trait_selection/src/traits/select/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -488,20 +488,93 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
}
}

ty::PredicateKind::WellFormed(arg) => match wf::obligations(
self.infcx,
obligation.param_env,
obligation.cause.body_id,
obligation.recursion_depth + 1,
arg,
obligation.cause.span,
) {
Some(mut obligations) => {
self.add_depth(obligations.iter_mut(), obligation.recursion_depth);
self.evaluate_predicates_recursively(previous_stack, obligations)
ty::PredicateKind::WellFormed(arg) => {
// So, there is a bit going on here. First, `WellFormed` predicates
// are coinductive, like trait predicates with auto traits.
// This means that we need to detect if we have recursively
// evaluated `WellFormed(X)`. Otherwise, we would run into
// a "natural" overflow error.
//
// Now, the next question is whether we need to do anything
// special with caching. Considering the following tree:
// - `WF(Foo<T>)`
// - `Bar<T>: Send`
// - `WF(Foo<T>)`
// - `Foo<T>: Trait`
// In this case, the innermost `WF(Foo<T>)` should return
// `EvaluatedToOk`, since it's coinductive. Then if
// `Bar<T>: Send` is resolved to `EvaluatedToOk`, it can be
// inserted into a cache (because without thinking about `WF`
// goals, it isn't in a cycle). If `Foo<T>: Trait` later doesn't
// hold, then `Bar<T>: Send` shouldn't hold. Therefore, we
// *do* need to keep track of coinductive cycles.

let cache = previous_stack.cache;
let dfn = cache.next_dfn();

for stack_arg in previous_stack.cache.wf_args.borrow().iter().rev() {
if stack_arg.0 != arg {
continue;
}
debug!("WellFormed({:?}) on stack", arg);
if let Some(stack) = previous_stack.head {
// Okay, let's imagine we have two different stacks:
// `T: NonAutoTrait -> WF(T) -> T: NonAutoTrait`
// `WF(T) -> T: NonAutoTrait -> WF(T)`
// Because of this, we need to check that all
// predicates between the WF goals are coinductive.
// Otherwise, we can say that `T: NonAutoTrait` is
// true.
// Let's imagine we have a predicate stack like
// `Foo: Bar -> WF(T) -> T: NonAutoTrait -> T: Auto
// depth ^1 ^2 ^3
// and the current predicate is `WF(T)`. `wf_args`
// would contain `(T, 1)`. We want to check all
// trait predicates greater than `1`. The previous
// stack would be `T: Auto`.
let cycle = stack.iter().take_while(|s| s.depth > stack_arg.1);
let tcx = self.tcx();
let cycle =
cycle.map(|stack| stack.obligation.predicate.to_predicate(tcx));
if self.coinductive_match(cycle) {
stack.update_reached_depth(stack_arg.1);
return Ok(EvaluatedToOk);
} else {
return Ok(EvaluatedToRecur);
}
}
return Ok(EvaluatedToOk);
}
None => Ok(EvaluatedToAmbig),
},

match wf::obligations(
self.infcx,
obligation.param_env,
obligation.cause.body_id,
obligation.recursion_depth + 1,
arg,
obligation.cause.span,
) {
Some(mut obligations) => {
self.add_depth(obligations.iter_mut(), obligation.recursion_depth);

cache.wf_args.borrow_mut().push((arg, previous_stack.depth()));
let result =
self.evaluate_predicates_recursively(previous_stack, obligations);
cache.wf_args.borrow_mut().pop();

let result = result?;

if !result.must_apply_modulo_regions() {
cache.on_failure(dfn);
}

cache.on_completion(dfn);

Ok(result)
}
None => Ok(EvaluatedToAmbig),
}
}

ty::PredicateKind::TypeOutlives(pred) => {
// A global type with no late-bound regions can only
Expand Down Expand Up @@ -718,6 +791,8 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {

debug!(?fresh_trait_pred);

// If a trait predicate is in the (local or global) evaluation cache,
// then we know it holds without cycles.
if let Some(result) = self.check_evaluation_cache(param_env, fresh_trait_pred) {
debug!(?result, "CACHE HIT");
return Ok(result);
Expand Down Expand Up @@ -921,7 +996,7 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
/// - it also appears in the backtrace at some position `X`,
/// - all the predicates at positions `X..` between `X` and the top are
/// also defaulted traits.
pub fn coinductive_match<I>(&mut self, mut cycle: I) -> bool
pub(crate) fn coinductive_match<I>(&mut self, mut cycle: I) -> bool
where
I: Iterator<Item = ty::Predicate<'tcx>>,
{
Expand All @@ -931,6 +1006,7 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
fn coinductive_predicate(&self, predicate: ty::Predicate<'tcx>) -> bool {
let result = match predicate.kind().skip_binder() {
ty::PredicateKind::Trait(ref data) => self.tcx().trait_is_auto(data.def_id()),
ty::PredicateKind::WellFormed(_) => true,
_ => false,
};
debug!(?predicate, ?result, "coinductive_predicate");
Expand Down Expand Up @@ -2410,6 +2486,15 @@ struct ProvisionalEvaluationCache<'tcx> {
/// all cache values whose DFN is >= 4 -- in this case, that
/// means the cached value for `F`.
map: RefCell<FxHashMap<ty::PolyTraitPredicate<'tcx>, ProvisionalEvaluation>>,

/// The stack of args that we assume to be true because a `WF(arg)` predicate
/// is on the stack above (and because of wellformedness is coinductive).
/// In an "ideal" world, this would share a stack with trait predicates in
/// `TraitObligationStack`. However, trait predicates are *much* hotter than
/// `WellFormed` predicates, and it's very likely that the additional matches
/// will have a perf effect. The value here is the well-formed `GenericArg`
/// and the depth of the trait predicate *above* that well-formed predicate.
wf_args: RefCell<Vec<(ty::GenericArg<'tcx>, usize)>>,
}

/// A cache value for the provisional cache: contains the depth-first
Expand All @@ -2423,7 +2508,7 @@ struct ProvisionalEvaluation {

impl<'tcx> Default for ProvisionalEvaluationCache<'tcx> {
fn default() -> Self {
Self { dfn: Cell::new(0), map: Default::default() }
Self { dfn: Cell::new(0), map: Default::default(), wf_args: Default::default() }
}
}

Expand Down
12 changes: 10 additions & 2 deletions compiler/rustc_traits/src/chalk/lowering.rs
Original file line number Diff line number Diff line change
Expand Up @@ -106,8 +106,16 @@ impl<'tcx> LowerInto<'tcx, chalk_ir::InEnvironment<chalk_ir::Goal<RustInterner<'
ty::PredicateKind::Projection(predicate) => chalk_ir::DomainGoal::Holds(
chalk_ir::WhereClause::AliasEq(predicate.lower_into(interner)),
),
ty::PredicateKind::WellFormed(..)
| ty::PredicateKind::ObjectSafe(..)
ty::PredicateKind::WellFormed(arg) => match arg.unpack() {
ty::GenericArgKind::Type(ty) => chalk_ir::DomainGoal::WellFormed(
chalk_ir::WellFormed::Ty(ty.lower_into(interner)),
),
// FIXME(chalk): we need to change `WellFormed` in Chalk to take a `GenericArg`
_ => chalk_ir::DomainGoal::WellFormed(chalk_ir::WellFormed::Ty(
interner.tcx.types.unit.lower_into(interner),
)),
},
ty::PredicateKind::ObjectSafe(..)
| ty::PredicateKind::ClosureKind(..)
| ty::PredicateKind::Subtype(..)
| ty::PredicateKind::Coerce(..)
Expand Down
11 changes: 8 additions & 3 deletions compiler/rustc_traits/src/implied_outlives_bounds.rs
Original file line number Diff line number Diff line change
Expand Up @@ -44,16 +44,21 @@ fn compute_implied_outlives_bounds<'tcx>(

// Sometimes when we ask what it takes for T: WF, we get back that
// U: WF is required; in that case, we push U onto this stack and
// process it next. Currently (at least) these resulting
// predicates are always guaranteed to be a subset of the original
// type, so we need not fear non-termination.
// process it next. Because the resulting predicates aren't always
// guaranteed to be a subset of the original type, so we need to store the
// WF args we've computed in a set.
let mut checked_wf_args = rustc_data_structures::stable_set::FxHashSet::default();
let mut wf_args = vec![ty.into()];

let mut implied_bounds = vec![];

let mut fulfill_cx = FulfillmentContext::new();

while let Some(arg) = wf_args.pop() {
if !checked_wf_args.insert(arg) {
continue;
}

// Compute the obligations for `arg` to be well-formed. If `arg` is
// an unresolved inference variable, just substituted an empty set
// -- because the return type here is going to be things we *add*
Expand Down
3 changes: 3 additions & 0 deletions compiler/rustc_typeck/src/check/dropck.rs
Original file line number Diff line number Diff line change
Expand Up @@ -206,6 +206,9 @@ fn ensure_drop_predicates_are_implied_by_item_defn<'tcx>(
relator.relate(predicate.rebind(ty_a), p.rebind(ty_b)).is_ok()
&& relator.relate(predicate.rebind(lt_a), p.rebind(lt_b)).is_ok()
}
(ty::PredicateKind::WellFormed(arg_a), ty::PredicateKind::WellFormed(arg_b)) => {
relator.relate(predicate.rebind(arg_a), p.rebind(arg_b)).is_ok()
}
_ => predicate == p,
}
};
Expand Down
6 changes: 6 additions & 0 deletions compiler/rustc_typeck/src/check/wfcheck.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1807,6 +1807,12 @@ fn check_false_global_bounds(fcx: &FnCtxt<'_, '_>, mut span: Span, id: hir::HirI
let implied_obligations = traits::elaborate_predicates_with_span(fcx.tcx, predicates_with_span);

for obligation in implied_obligations {
// We lower empty bounds like `Vec<dyn Copy>:` as
// `WellFormed(Vec<dyn Copy>)`, which will later get checked by
// regular WF checking
if let ty::PredicateKind::WellFormed(..) = obligation.predicate.kind().skip_binder() {
continue;
}
let pred = obligation.predicate;
// Match the existing behavior.
if pred.is_global() && !pred.has_late_bound_regions() {
Expand Down
6 changes: 1 addition & 5 deletions compiler/rustc_typeck/src/collect.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2264,12 +2264,8 @@ fn gather_explicit_predicates_of(tcx: TyCtxt<'_>, def_id: DefId) -> ty::GenericP
// compiler/tooling bugs from not handling WF predicates.
} else {
let span = bound_pred.bounded_ty.span;
let re_root_empty = tcx.lifetimes.re_root_empty;
let predicate = ty::Binder::bind_with_vars(
ty::PredicateKind::TypeOutlives(ty::OutlivesPredicate(
ty,
re_root_empty,
)),
ty::PredicateKind::WellFormed(ty.into()),
bound_vars,
);
predicates.insert((predicate.to_predicate(tcx), span));
Expand Down
2 changes: 1 addition & 1 deletion src/librustdoc/clean/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -293,10 +293,10 @@ impl<'tcx> Clean<'tcx, Option<WherePredicate>> for ty::Predicate<'tcx> {
ty::PredicateKind::TypeOutlives(pred) => pred.clean(cx),
ty::PredicateKind::Projection(pred) => Some(pred.clean(cx)),
ty::PredicateKind::ConstEvaluatable(..) => None,
ty::PredicateKind::WellFormed(..) => None,

ty::PredicateKind::Subtype(..)
| ty::PredicateKind::Coerce(..)
| ty::PredicateKind::WellFormed(..)
| ty::PredicateKind::ObjectSafe(..)
| ty::PredicateKind::ClosureKind(..)
| ty::PredicateKind::ConstEquate(..)
Expand Down

0 comments on commit 116edb6

Please sign in to comment.