Skip to content

Commit

Permalink
Prove obligations to termination instead of ignoring ambiguities.
Browse files Browse the repository at this point in the history
Sometimes an obligation depends on a later one, so we can't just process them in order like it was done previously.

This is not a problem in our test suite, but there may be ICEs out there and it will definitely be a problem with lazy TAIT.
  • Loading branch information
oli-obk committed Dec 16, 2021
1 parent 5c46002 commit bdeeb07
Showing 1 changed file with 42 additions and 19 deletions.
61 changes: 42 additions & 19 deletions compiler/rustc_trait_selection/src/traits/query/type_op/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,9 @@ use crate::infer::canonical::{
use crate::infer::{InferCtxt, InferOk};
use crate::traits::query::Fallible;
use crate::traits::ObligationCause;
use rustc_infer::infer::canonical::Canonical;
use rustc_infer::infer::canonical::{Canonical, Certainty};
use rustc_infer::traits::query::NoSolution;
use rustc_infer::traits::PredicateObligations;
use rustc_middle::ty::fold::TypeFoldable;
use rustc_middle::ty::{ParamEnvAnd, TyCtxt};
use std::fmt;
Expand All @@ -17,7 +19,6 @@ pub mod implied_outlives_bounds;
pub mod normalize;
pub mod outlives;
pub mod prove_predicate;
use self::prove_predicate::ProvePredicate;
pub mod subtype;

pub use rustc_middle::traits::query::type_op::*;
Expand Down Expand Up @@ -80,9 +81,14 @@ pub trait QueryTypeOp<'tcx>: fmt::Debug + Copy + TypeFoldable<'tcx> + 'tcx {
query_key: ParamEnvAnd<'tcx, Self>,
infcx: &InferCtxt<'_, 'tcx>,
output_query_region_constraints: &mut QueryRegionConstraints<'tcx>,
) -> Fallible<(Self::QueryResponse, Option<Canonical<'tcx, ParamEnvAnd<'tcx, Self>>>)> {
) -> Fallible<(
Self::QueryResponse,
Option<Canonical<'tcx, ParamEnvAnd<'tcx, Self>>>,
PredicateObligations<'tcx>,
Certainty,
)> {
if let Some(result) = QueryTypeOp::try_fast_path(infcx.tcx, &query_key) {
return Ok((result, None));
return Ok((result, None, vec![], Certainty::Proven));
}

// FIXME(#33684) -- We need to use
Expand All @@ -104,20 +110,7 @@ pub trait QueryTypeOp<'tcx>: fmt::Debug + Copy + TypeFoldable<'tcx> + 'tcx {
output_query_region_constraints,
)?;

// Typically, instantiating NLL query results does not
// create obligations. However, in some cases there
// are unresolved type variables, and unify them *can*
// create obligations. In that case, we have to go
// fulfill them. We do this via a (recursive) query.
for obligation in obligations {
let ((), _) = ProvePredicate::fully_perform_into(
obligation.param_env.and(ProvePredicate::new(obligation.predicate)),
infcx,
output_query_region_constraints,
)?;
}

Ok((value, Some(canonical_self)))
Ok((value, Some(canonical_self), obligations, canonical_result.value.certainty))
}
}

Expand All @@ -129,9 +122,39 @@ where

fn fully_perform(self, infcx: &InferCtxt<'_, 'tcx>) -> Fallible<TypeOpOutput<'tcx, Self>> {
let mut region_constraints = QueryRegionConstraints::default();
let (output, canonicalized_query) =
let (output, canonicalized_query, mut obligations, _) =
Q::fully_perform_into(self, infcx, &mut region_constraints)?;

// Typically, instantiating NLL query results does not
// create obligations. However, in some cases there
// are unresolved type variables, and unify them *can*
// create obligations. In that case, we have to go
// fulfill them. We do this via a (recursive) query.
while !obligations.is_empty() {
trace!("{:#?}", obligations);
let mut progress = false;
for obligation in std::mem::take(&mut obligations) {
let obligation = infcx.resolve_vars_if_possible(obligation);
match ProvePredicate::fully_perform_into(
obligation.param_env.and(ProvePredicate::new(obligation.predicate)),
infcx,
&mut region_constraints,
) {
Ok(((), _, new, certainty)) => {
obligations.extend(new);
progress = true;
if let Certainty::Ambiguous = certainty {
obligations.push(obligation);
}
}
Err(_) => obligations.push(obligation),
}
}
if !progress {
return Err(NoSolution);
}
}

// Promote the final query-region-constraints into a
// (optional) ref-counted vector:
let region_constraints =
Expand Down

0 comments on commit bdeeb07

Please sign in to comment.