Add consider_implied_clause
This commit is contained in:
parent
82b52056fe
commit
6402c98621
3 changed files with 97 additions and 102 deletions
|
@ -90,30 +90,22 @@ pub(super) trait GoalKind<'tcx>: TypeFoldable<'tcx> + Copy + Eq {
|
||||||
|
|
||||||
fn trait_def_id(self, tcx: TyCtxt<'tcx>) -> DefId;
|
fn trait_def_id(self, tcx: TyCtxt<'tcx>) -> DefId;
|
||||||
|
|
||||||
|
// Consider a clause, which consists of a "assumption" and some "requirements",
|
||||||
|
// to satisfy a goal. If the requirements hold, then attempt to satisfy our
|
||||||
|
// goal by equating it with the assumption.
|
||||||
|
fn consider_implied_clause(
|
||||||
|
ecx: &mut EvalCtxt<'_, 'tcx>,
|
||||||
|
goal: Goal<'tcx, Self>,
|
||||||
|
assumption: ty::Predicate<'tcx>,
|
||||||
|
requirements: impl IntoIterator<Item = Goal<'tcx, ty::Predicate<'tcx>>>,
|
||||||
|
) -> QueryResult<'tcx>;
|
||||||
|
|
||||||
fn consider_impl_candidate(
|
fn consider_impl_candidate(
|
||||||
ecx: &mut EvalCtxt<'_, 'tcx>,
|
ecx: &mut EvalCtxt<'_, 'tcx>,
|
||||||
goal: Goal<'tcx, Self>,
|
goal: Goal<'tcx, Self>,
|
||||||
impl_def_id: DefId,
|
impl_def_id: DefId,
|
||||||
) -> QueryResult<'tcx>;
|
) -> QueryResult<'tcx>;
|
||||||
|
|
||||||
// Consider a predicate we know holds (`assumption`) against a goal we're trying to prove.
|
|
||||||
fn consider_assumption(
|
|
||||||
ecx: &mut EvalCtxt<'_, 'tcx>,
|
|
||||||
goal: Goal<'tcx, Self>,
|
|
||||||
assumption: ty::Predicate<'tcx>,
|
|
||||||
) -> QueryResult<'tcx> {
|
|
||||||
Self::consider_assumption_with_certainty(ecx, goal, assumption, Certainty::Yes)
|
|
||||||
}
|
|
||||||
|
|
||||||
// Consider a predicate we know holds (`assumption`) against a goal, unifying with
|
|
||||||
// the `assumption_certainty` if it satisfies the goal.
|
|
||||||
fn consider_assumption_with_certainty(
|
|
||||||
ecx: &mut EvalCtxt<'_, 'tcx>,
|
|
||||||
goal: Goal<'tcx, Self>,
|
|
||||||
assumption: ty::Predicate<'tcx>,
|
|
||||||
assumption_certainty: Certainty,
|
|
||||||
) -> QueryResult<'tcx>;
|
|
||||||
|
|
||||||
// A type implements an `auto trait` if its components do as well. These components
|
// A type implements an `auto trait` if its components do as well. These components
|
||||||
// are given by built-in rules from [`instantiate_constituent_tys_for_auto_trait`].
|
// are given by built-in rules from [`instantiate_constituent_tys_for_auto_trait`].
|
||||||
fn consider_auto_trait_candidate(
|
fn consider_auto_trait_candidate(
|
||||||
|
@ -367,7 +359,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
|
||||||
candidates: &mut Vec<Candidate<'tcx>>,
|
candidates: &mut Vec<Candidate<'tcx>>,
|
||||||
) {
|
) {
|
||||||
for (i, assumption) in goal.param_env.caller_bounds().iter().enumerate() {
|
for (i, assumption) in goal.param_env.caller_bounds().iter().enumerate() {
|
||||||
match G::consider_assumption(self, goal, assumption) {
|
match G::consider_implied_clause(self, goal, assumption, []) {
|
||||||
Ok(result) => {
|
Ok(result) => {
|
||||||
candidates.push(Candidate { source: CandidateSource::ParamEnv(i), result })
|
candidates.push(Candidate { source: CandidateSource::ParamEnv(i), result })
|
||||||
}
|
}
|
||||||
|
@ -414,7 +406,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
|
||||||
|
|
||||||
for assumption in self.tcx().item_bounds(alias_ty.def_id).subst(self.tcx(), alias_ty.substs)
|
for assumption in self.tcx().item_bounds(alias_ty.def_id).subst(self.tcx(), alias_ty.substs)
|
||||||
{
|
{
|
||||||
match G::consider_assumption(self, goal, assumption) {
|
match G::consider_implied_clause(self, goal, assumption, []) {
|
||||||
Ok(result) => {
|
Ok(result) => {
|
||||||
candidates.push(Candidate { source: CandidateSource::AliasBound, result })
|
candidates.push(Candidate { source: CandidateSource::AliasBound, result })
|
||||||
}
|
}
|
||||||
|
@ -464,7 +456,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
|
||||||
for assumption in
|
for assumption in
|
||||||
elaborate_predicates(tcx, bounds.iter().map(|bound| bound.with_self_ty(tcx, self_ty)))
|
elaborate_predicates(tcx, bounds.iter().map(|bound| bound.with_self_ty(tcx, self_ty)))
|
||||||
{
|
{
|
||||||
match G::consider_assumption(self, goal, assumption.predicate) {
|
match G::consider_implied_clause(self, goal, assumption.predicate, []) {
|
||||||
Ok(result) => {
|
Ok(result) => {
|
||||||
candidates.push(Candidate { source: CandidateSource::BuiltinImpl, result })
|
candidates.push(Candidate { source: CandidateSource::BuiltinImpl, result })
|
||||||
}
|
}
|
||||||
|
|
|
@ -168,6 +168,37 @@ impl<'tcx> assembly::GoalKind<'tcx> for ProjectionPredicate<'tcx> {
|
||||||
self.trait_def_id(tcx)
|
self.trait_def_id(tcx)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
fn consider_implied_clause(
|
||||||
|
ecx: &mut EvalCtxt<'_, 'tcx>,
|
||||||
|
goal: Goal<'tcx, Self>,
|
||||||
|
assumption: ty::Predicate<'tcx>,
|
||||||
|
requirements: impl IntoIterator<Item = Goal<'tcx, ty::Predicate<'tcx>>>,
|
||||||
|
) -> QueryResult<'tcx> {
|
||||||
|
if let Some(poly_projection_pred) = assumption.to_opt_poly_projection_pred()
|
||||||
|
&& poly_projection_pred.projection_def_id() == goal.predicate.def_id()
|
||||||
|
{
|
||||||
|
ecx.infcx.probe(|_| {
|
||||||
|
let assumption_projection_pred =
|
||||||
|
ecx.infcx.instantiate_binder_with_infer(poly_projection_pred);
|
||||||
|
let mut nested_goals = ecx.infcx.eq(
|
||||||
|
goal.param_env,
|
||||||
|
goal.predicate.projection_ty,
|
||||||
|
assumption_projection_pred.projection_ty,
|
||||||
|
)?;
|
||||||
|
nested_goals.extend(requirements);
|
||||||
|
let subst_certainty = ecx.evaluate_all(nested_goals)?;
|
||||||
|
|
||||||
|
ecx.eq_term_and_make_canonical_response(
|
||||||
|
goal,
|
||||||
|
subst_certainty,
|
||||||
|
assumption_projection_pred.term,
|
||||||
|
)
|
||||||
|
})
|
||||||
|
} else {
|
||||||
|
Err(NoSolution)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
fn consider_impl_candidate(
|
fn consider_impl_candidate(
|
||||||
ecx: &mut EvalCtxt<'_, 'tcx>,
|
ecx: &mut EvalCtxt<'_, 'tcx>,
|
||||||
goal: Goal<'tcx, ProjectionPredicate<'tcx>>,
|
goal: Goal<'tcx, ProjectionPredicate<'tcx>>,
|
||||||
|
@ -260,36 +291,6 @@ impl<'tcx> assembly::GoalKind<'tcx> for ProjectionPredicate<'tcx> {
|
||||||
})
|
})
|
||||||
}
|
}
|
||||||
|
|
||||||
fn consider_assumption_with_certainty(
|
|
||||||
ecx: &mut EvalCtxt<'_, 'tcx>,
|
|
||||||
goal: Goal<'tcx, Self>,
|
|
||||||
assumption: ty::Predicate<'tcx>,
|
|
||||||
assumption_certainty: Certainty,
|
|
||||||
) -> QueryResult<'tcx> {
|
|
||||||
if let Some(poly_projection_pred) = assumption.to_opt_poly_projection_pred()
|
|
||||||
&& poly_projection_pred.projection_def_id() == goal.predicate.def_id()
|
|
||||||
{
|
|
||||||
ecx.infcx.probe(|_| {
|
|
||||||
let assumption_projection_pred =
|
|
||||||
ecx.infcx.instantiate_binder_with_infer(poly_projection_pred);
|
|
||||||
let nested_goals = ecx.infcx.eq(
|
|
||||||
goal.param_env,
|
|
||||||
goal.predicate.projection_ty,
|
|
||||||
assumption_projection_pred.projection_ty,
|
|
||||||
)?;
|
|
||||||
let subst_certainty = ecx.evaluate_all(nested_goals)?;
|
|
||||||
|
|
||||||
ecx.eq_term_and_make_canonical_response(
|
|
||||||
goal,
|
|
||||||
subst_certainty.unify_and(assumption_certainty),
|
|
||||||
assumption_projection_pred.term,
|
|
||||||
)
|
|
||||||
})
|
|
||||||
} else {
|
|
||||||
Err(NoSolution)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
fn consider_auto_trait_candidate(
|
fn consider_auto_trait_candidate(
|
||||||
_ecx: &mut EvalCtxt<'_, 'tcx>,
|
_ecx: &mut EvalCtxt<'_, 'tcx>,
|
||||||
goal: Goal<'tcx, Self>,
|
goal: Goal<'tcx, Self>,
|
||||||
|
@ -331,31 +332,27 @@ impl<'tcx> assembly::GoalKind<'tcx> for ProjectionPredicate<'tcx> {
|
||||||
goal_kind: ty::ClosureKind,
|
goal_kind: ty::ClosureKind,
|
||||||
) -> QueryResult<'tcx> {
|
) -> QueryResult<'tcx> {
|
||||||
let tcx = ecx.tcx();
|
let tcx = ecx.tcx();
|
||||||
if let Some(tupled_inputs_and_output) =
|
let Some(tupled_inputs_and_output) =
|
||||||
structural_traits::extract_tupled_inputs_and_output_from_callable(
|
structural_traits::extract_tupled_inputs_and_output_from_callable(
|
||||||
tcx,
|
tcx,
|
||||||
goal.predicate.self_ty(),
|
goal.predicate.self_ty(),
|
||||||
goal_kind,
|
goal_kind,
|
||||||
)?
|
)? else {
|
||||||
{
|
return ecx.make_canonical_response(Certainty::AMBIGUOUS);
|
||||||
// A built-in `Fn` trait needs to check that its output is `Sized`
|
};
|
||||||
// (FIXME: technically we only need to check this if the type is a fn ptr...)
|
let output_is_sized_pred = tupled_inputs_and_output
|
||||||
let output_is_sized_pred = tupled_inputs_and_output
|
.map_bound(|(_, output)| tcx.at(DUMMY_SP).mk_trait_ref(LangItem::Sized, [output]));
|
||||||
.map_bound(|(_, output)| tcx.at(DUMMY_SP).mk_trait_ref(LangItem::Sized, [output]));
|
|
||||||
let (_, output_is_sized_certainty) =
|
|
||||||
ecx.evaluate_goal(goal.with(tcx, output_is_sized_pred))?;
|
|
||||||
|
|
||||||
let pred = tupled_inputs_and_output
|
let pred = tupled_inputs_and_output
|
||||||
.map_bound(|(inputs, output)| ty::ProjectionPredicate {
|
.map_bound(|(inputs, output)| ty::ProjectionPredicate {
|
||||||
projection_ty: tcx
|
projection_ty: tcx
|
||||||
.mk_alias_ty(goal.predicate.def_id(), [goal.predicate.self_ty(), inputs]),
|
.mk_alias_ty(goal.predicate.def_id(), [goal.predicate.self_ty(), inputs]),
|
||||||
term: output.into(),
|
term: output.into(),
|
||||||
})
|
})
|
||||||
.to_predicate(tcx);
|
.to_predicate(tcx);
|
||||||
Self::consider_assumption_with_certainty(ecx, goal, pred, output_is_sized_certainty)
|
// A built-in `Fn` impl only holds if the output is sized.
|
||||||
} else {
|
// (FIXME: technically we only need to check this if the type is a fn ptr...)
|
||||||
ecx.make_canonical_response(Certainty::AMBIGUOUS)
|
Self::consider_implied_clause(ecx, goal, pred, [goal.with(tcx, output_is_sized_pred)])
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
fn consider_builtin_tuple_candidate(
|
fn consider_builtin_tuple_candidate(
|
||||||
|
@ -474,7 +471,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for ProjectionPredicate<'tcx> {
|
||||||
|
|
||||||
let term = substs.as_generator().return_ty().into();
|
let term = substs.as_generator().return_ty().into();
|
||||||
|
|
||||||
Self::consider_assumption(
|
Self::consider_implied_clause(
|
||||||
ecx,
|
ecx,
|
||||||
goal,
|
goal,
|
||||||
ty::Binder::dummy(ty::ProjectionPredicate {
|
ty::Binder::dummy(ty::ProjectionPredicate {
|
||||||
|
@ -482,6 +479,9 @@ impl<'tcx> assembly::GoalKind<'tcx> for ProjectionPredicate<'tcx> {
|
||||||
term,
|
term,
|
||||||
})
|
})
|
||||||
.to_predicate(tcx),
|
.to_predicate(tcx),
|
||||||
|
// Technically, we need to check that the future type is Sized,
|
||||||
|
// but that's already proven by the generator being WF.
|
||||||
|
[],
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -511,7 +511,7 @@ impl<'tcx> assembly::GoalKind<'tcx> for ProjectionPredicate<'tcx> {
|
||||||
bug!("unexpected associated item `<{self_ty} as Generator>::{name}`")
|
bug!("unexpected associated item `<{self_ty} as Generator>::{name}`")
|
||||||
};
|
};
|
||||||
|
|
||||||
Self::consider_assumption(
|
Self::consider_implied_clause(
|
||||||
ecx,
|
ecx,
|
||||||
goal,
|
goal,
|
||||||
ty::Binder::dummy(ty::ProjectionPredicate {
|
ty::Binder::dummy(ty::ProjectionPredicate {
|
||||||
|
@ -521,6 +521,9 @@ impl<'tcx> assembly::GoalKind<'tcx> for ProjectionPredicate<'tcx> {
|
||||||
term,
|
term,
|
||||||
})
|
})
|
||||||
.to_predicate(tcx),
|
.to_predicate(tcx),
|
||||||
|
// Technically, we need to check that the future type is Sized,
|
||||||
|
// but that's already proven by the generator being WF.
|
||||||
|
[],
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -62,11 +62,11 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
|
||||||
})
|
})
|
||||||
}
|
}
|
||||||
|
|
||||||
fn consider_assumption_with_certainty(
|
fn consider_implied_clause(
|
||||||
ecx: &mut EvalCtxt<'_, 'tcx>,
|
ecx: &mut EvalCtxt<'_, 'tcx>,
|
||||||
goal: Goal<'tcx, Self>,
|
goal: Goal<'tcx, Self>,
|
||||||
assumption: ty::Predicate<'tcx>,
|
assumption: ty::Predicate<'tcx>,
|
||||||
assumption_certainty: Certainty,
|
requirements: impl IntoIterator<Item = Goal<'tcx, ty::Predicate<'tcx>>>,
|
||||||
) -> QueryResult<'tcx> {
|
) -> QueryResult<'tcx> {
|
||||||
if let Some(poly_trait_pred) = assumption.to_opt_poly_trait_pred()
|
if let Some(poly_trait_pred) = assumption.to_opt_poly_trait_pred()
|
||||||
&& poly_trait_pred.def_id() == goal.predicate.def_id()
|
&& poly_trait_pred.def_id() == goal.predicate.def_id()
|
||||||
|
@ -75,14 +75,13 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
|
||||||
ecx.infcx.probe(|_| {
|
ecx.infcx.probe(|_| {
|
||||||
let assumption_trait_pred =
|
let assumption_trait_pred =
|
||||||
ecx.infcx.instantiate_binder_with_infer(poly_trait_pred);
|
ecx.infcx.instantiate_binder_with_infer(poly_trait_pred);
|
||||||
let nested_goals = ecx.infcx.eq(
|
let mut nested_goals = ecx.infcx.eq(
|
||||||
goal.param_env,
|
goal.param_env,
|
||||||
goal.predicate.trait_ref,
|
goal.predicate.trait_ref,
|
||||||
assumption_trait_pred.trait_ref,
|
assumption_trait_pred.trait_ref,
|
||||||
)?;
|
)?;
|
||||||
ecx.evaluate_all(nested_goals).and_then(|certainty| {
|
nested_goals.extend(requirements);
|
||||||
ecx.make_canonical_response(certainty.unify_and(assumption_certainty))
|
ecx.evaluate_all_and_make_canonical_response(nested_goals)
|
||||||
})
|
|
||||||
})
|
})
|
||||||
} else {
|
} else {
|
||||||
Err(NoSolution)
|
Err(NoSolution)
|
||||||
|
@ -178,29 +177,25 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
|
||||||
goal_kind: ty::ClosureKind,
|
goal_kind: ty::ClosureKind,
|
||||||
) -> QueryResult<'tcx> {
|
) -> QueryResult<'tcx> {
|
||||||
let tcx = ecx.tcx();
|
let tcx = ecx.tcx();
|
||||||
if let Some(tupled_inputs_and_output) =
|
let Some(tupled_inputs_and_output) =
|
||||||
structural_traits::extract_tupled_inputs_and_output_from_callable(
|
structural_traits::extract_tupled_inputs_and_output_from_callable(
|
||||||
tcx,
|
tcx,
|
||||||
goal.predicate.self_ty(),
|
goal.predicate.self_ty(),
|
||||||
goal_kind,
|
goal_kind,
|
||||||
)?
|
)? else {
|
||||||
{
|
return ecx.make_canonical_response(Certainty::AMBIGUOUS);
|
||||||
// A built-in `Fn` trait needs to check that its output is `Sized`
|
};
|
||||||
// (FIXME: technically we only need to check this if the type is a fn ptr...)
|
let output_is_sized_pred = tupled_inputs_and_output
|
||||||
let output_is_sized_pred = tupled_inputs_and_output
|
.map_bound(|(_, output)| tcx.at(DUMMY_SP).mk_trait_ref(LangItem::Sized, [output]));
|
||||||
.map_bound(|(_, output)| tcx.at(DUMMY_SP).mk_trait_ref(LangItem::Sized, [output]));
|
|
||||||
let (_, output_is_sized_certainty) =
|
|
||||||
ecx.evaluate_goal(goal.with(tcx, output_is_sized_pred))?;
|
|
||||||
|
|
||||||
let pred = tupled_inputs_and_output
|
let pred = tupled_inputs_and_output
|
||||||
.map_bound(|(inputs, _)| {
|
.map_bound(|(inputs, _)| {
|
||||||
tcx.mk_trait_ref(goal.predicate.def_id(), [goal.predicate.self_ty(), inputs])
|
tcx.mk_trait_ref(goal.predicate.def_id(), [goal.predicate.self_ty(), inputs])
|
||||||
})
|
})
|
||||||
.to_predicate(tcx);
|
.to_predicate(tcx);
|
||||||
Self::consider_assumption_with_certainty(ecx, goal, pred, output_is_sized_certainty)
|
// A built-in `Fn` impl only holds if the output is sized.
|
||||||
} else {
|
// (FIXME: technically we only need to check this if the type is a fn ptr...)
|
||||||
ecx.make_canonical_response(Certainty::AMBIGUOUS)
|
Self::consider_implied_clause(ecx, goal, pred, [goal.with(tcx, output_is_sized_pred)])
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
fn consider_builtin_tuple_candidate(
|
fn consider_builtin_tuple_candidate(
|
||||||
|
@ -236,6 +231,8 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
|
||||||
}
|
}
|
||||||
|
|
||||||
// Async generator unconditionally implement `Future`
|
// Async generator unconditionally implement `Future`
|
||||||
|
// Technically, we need to check that the future output type is Sized,
|
||||||
|
// but that's already proven by the generator being WF.
|
||||||
ecx.make_canonical_response(Certainty::Yes)
|
ecx.make_canonical_response(Certainty::Yes)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -255,13 +252,16 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
|
||||||
}
|
}
|
||||||
|
|
||||||
let generator = substs.as_generator();
|
let generator = substs.as_generator();
|
||||||
Self::consider_assumption(
|
Self::consider_implied_clause(
|
||||||
ecx,
|
ecx,
|
||||||
goal,
|
goal,
|
||||||
ty::Binder::dummy(
|
ty::Binder::dummy(
|
||||||
tcx.mk_trait_ref(goal.predicate.def_id(), [self_ty, generator.resume_ty()]),
|
tcx.mk_trait_ref(goal.predicate.def_id(), [self_ty, generator.resume_ty()]),
|
||||||
)
|
)
|
||||||
.to_predicate(tcx),
|
.to_predicate(tcx),
|
||||||
|
// Technically, we need to check that the generator types are Sized,
|
||||||
|
// but that's already proven by the generator being WF.
|
||||||
|
[],
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue