implement consider_assumption

This commit is contained in:
Michael Goulet 2023-01-17 19:50:50 +00:00
parent b84b1da2db
commit f99b273d57
3 changed files with 70 additions and 10 deletions

View File

@ -25,6 +25,13 @@ pub(super) trait InferCtxtExt<'tcx> {
lhs: T,
rhs: T,
) -> Result<Vec<Goal<'tcx, ty::Predicate<'tcx>>>, NoSolution>;
fn sup<T: ToTrace<'tcx>>(
&self,
param_env: ty::ParamEnv<'tcx>,
lhs: T,
rhs: T,
) -> Result<Vec<Goal<'tcx, ty::Predicate<'tcx>>>, NoSolution>;
}
impl<'tcx> InferCtxtExt<'tcx> for InferCtxt<'tcx> {
@ -59,4 +66,23 @@ impl<'tcx> InferCtxtExt<'tcx> for InferCtxt<'tcx> {
NoSolution
})
}
#[instrument(level = "debug", skip(self, param_env), ret)]
fn sup<T: ToTrace<'tcx>>(
&self,
param_env: ty::ParamEnv<'tcx>,
lhs: T,
rhs: T,
) -> Result<Vec<Goal<'tcx, ty::Predicate<'tcx>>>, NoSolution> {
self.at(&ObligationCause::dummy(), param_env)
.define_opaque_types(false)
.sup(lhs, rhs)
.map(|InferOk { value: (), obligations }| {
obligations.into_iter().map(|o| o.into()).collect()
})
.map_err(|e| {
debug!(?e, "failed to sup");
NoSolution
})
}
}

View File

@ -6,7 +6,7 @@ use super::{Certainty, EvalCtxt, Goal, MaybeCause, QueryResult};
use rustc_errors::ErrorGuaranteed;
use rustc_hir::def::DefKind;
use rustc_hir::def_id::DefId;
use rustc_infer::infer::InferCtxt;
use rustc_infer::infer::{InferCtxt, LateBoundRegionConversionTime};
use rustc_infer::traits::query::NoSolution;
use rustc_infer::traits::specialization_graph::LeafDef;
use rustc_infer::traits::Reveal;
@ -298,12 +298,37 @@ impl<'tcx> assembly::GoalKind<'tcx> for ProjectionPredicate<'tcx> {
}
fn consider_assumption(
_ecx: &mut EvalCtxt<'_, 'tcx>,
_goal: Goal<'tcx, Self>,
ecx: &mut EvalCtxt<'_, 'tcx>,
goal: Goal<'tcx, Self>,
assumption: ty::Predicate<'tcx>,
) -> QueryResult<'tcx> {
if let Some(_poly_projection_pred) = assumption.to_opt_poly_projection_pred() {
unimplemented!()
if let Some(poly_projection_pred) = assumption.to_opt_poly_projection_pred() {
ecx.infcx.probe(|_| {
let assumption_projection_pred = ecx.infcx.replace_bound_vars_with_fresh_vars(
DUMMY_SP,
LateBoundRegionConversionTime::HigherRankedType,
poly_projection_pred,
);
let nested_goals = ecx.infcx.sup(
goal.param_env,
goal.predicate.projection_ty,
assumption_projection_pred.projection_ty,
)?;
let subst_certainty = ecx.evaluate_all(nested_goals)?;
// The term of our goal should be fully unconstrained, so this should never fail.
//
// It can however be ambiguous when the resolved type is a projection.
let nested_goals = ecx
.infcx
.eq(goal.param_env, goal.predicate.term, assumption_projection_pred.term)
.expect("failed to unify with unconstrained term");
let rhs_certainty = ecx
.evaluate_all(nested_goals)
.expect("failed to unify with unconstrained term");
ecx.make_canonical_response(subst_certainty.unify_and(rhs_certainty))
})
} else {
Err(NoSolution)
}

View File

@ -6,10 +6,11 @@ use super::assembly::{self, Candidate, CandidateSource};
use super::infcx_ext::InferCtxtExt;
use super::{EvalCtxt, Goal, QueryResult};
use rustc_hir::def_id::DefId;
use rustc_infer::infer::LateBoundRegionConversionTime;
use rustc_infer::traits::query::NoSolution;
use rustc_middle::ty::fast_reject::{DeepRejectCtxt, TreatParams};
use rustc_middle::ty::TraitPredicate;
use rustc_middle::ty::{self, Ty, TyCtxt};
use rustc_middle::ty::{ToPolyTraitRef, TraitPredicate};
use rustc_span::DUMMY_SP;
impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
@ -65,12 +66,20 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
}
fn consider_assumption(
_ecx: &mut EvalCtxt<'_, 'tcx>,
_goal: Goal<'tcx, Self>,
ecx: &mut EvalCtxt<'_, 'tcx>,
goal: Goal<'tcx, Self>,
assumption: ty::Predicate<'tcx>,
) -> QueryResult<'tcx> {
if let Some(_poly_trait_pred) = assumption.to_opt_poly_trait_pred() {
unimplemented!()
if let Some(poly_trait_pred) = assumption.to_opt_poly_trait_pred() {
// FIXME: Constness and polarity
ecx.infcx.probe(|_| {
let nested_goals = ecx.infcx.sup(
goal.param_env,
ty::Binder::dummy(goal.predicate.trait_ref),
poly_trait_pred.to_poly_trait_ref(),
)?;
ecx.evaluate_all_and_make_canonical_response(nested_goals)
})
} else {
Err(NoSolution)
}