1
Fork 0

Make empty bounds lower to WellFormed and make WellFormed coinductive

This commit is contained in:
Jack Huey 2022-06-26 11:08:58 -04:00
parent 8e430bfa9a
commit e16dbb5076
8 changed files with 100 additions and 26 deletions

View file

@ -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(..)

View file

@ -44,9 +44,10 @@ 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![];
@ -54,6 +55,10 @@ fn compute_implied_outlives_bounds<'tcx>(
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*