Include relation direction in AliasEq predicate

This commit is contained in:
Michael Goulet 2023-03-21 21:50:16 +00:00
parent 439292bc79
commit 5dc3fd7c05
16 changed files with 173 additions and 34 deletions

View file

@ -223,8 +223,8 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
ty::PredicateKind::TypeWellFormedFromEnv(..) => {
bug!("TypeWellFormedFromEnv is only used for Chalk")
}
ty::PredicateKind::AliasEq(lhs, rhs) => {
self.compute_alias_eq_goal(Goal { param_env, predicate: (lhs, rhs) })
ty::PredicateKind::AliasEq(lhs, rhs, direction) => {
self.compute_alias_eq_goal(Goal { param_env, predicate: (lhs, rhs, direction) })
}
}
} else {

View file

@ -73,7 +73,7 @@ impl<'tcx> TraitEngine<'tcx> for FulfillmentCtxt<'tcx> {
MismatchedProjectionTypes { err: TypeError::Mismatch },
)
}
ty::PredicateKind::AliasEq(_, _) => {
ty::PredicateKind::AliasEq(_, _, _) => {
FulfillmentErrorCode::CodeProjectionError(
MismatchedProjectionTypes { err: TypeError::Mismatch },
)

View file

@ -158,13 +158,35 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
#[instrument(level = "debug", skip(self), ret)]
fn compute_alias_eq_goal(
&mut self,
goal: Goal<'tcx, (ty::Term<'tcx>, ty::Term<'tcx>)>,
goal: Goal<'tcx, (ty::Term<'tcx>, ty::Term<'tcx>, ty::AliasRelationDirection)>,
) -> QueryResult<'tcx> {
let tcx = self.tcx();
let evaluate_normalizes_to = |ecx: &mut EvalCtxt<'_, 'tcx>, alias, other| {
let evaluate_normalizes_to = |ecx: &mut EvalCtxt<'_, 'tcx>, alias, other, direction| {
debug!("evaluate_normalizes_to(alias={:?}, other={:?})", alias, other);
let r = ecx.probe(|ecx| {
let result = ecx.probe(|ecx| {
let other = match direction {
// This is purely an optimization.
ty::AliasRelationDirection::Equate => other,
ty::AliasRelationDirection::Subtype | ty::AliasRelationDirection::Supertype => {
let fresh = ecx.next_term_infer_of_kind(other);
let (sub, sup) = if direction == ty::AliasRelationDirection::Subtype {
(fresh, other)
} else {
(other, fresh)
};
ecx.add_goals(
ecx.infcx
.at(&ObligationCause::dummy(), goal.param_env)
.sub(DefineOpaqueTypes::No, sub, sup)?
.into_obligations()
.into_iter()
.map(|o| o.into()),
);
fresh
}
};
ecx.add_goal(goal.with(
tcx,
ty::Binder::dummy(ty::ProjectionPredicate {
@ -174,37 +196,64 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
));
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
});
debug!("evaluate_normalizes_to(..) -> {:?}", r);
r
debug!("evaluate_normalizes_to({alias}, {other}, {direction:?}) -> {result:?}");
result
};
if goal.predicate.0.is_infer() || goal.predicate.1.is_infer() {
let (lhs, rhs, direction) = goal.predicate;
if lhs.is_infer() || rhs.is_infer() {
bug!(
"`AliasEq` goal with an infer var on lhs or rhs which should have been instantiated"
);
}
match (
goal.predicate.0.to_alias_term_no_opaque(tcx),
goal.predicate.1.to_alias_term_no_opaque(tcx),
) {
match (lhs.to_projection_term(tcx), rhs.to_projection_term(tcx)) {
(None, None) => bug!("`AliasEq` goal without an alias on either lhs or rhs"),
(Some(alias), None) => evaluate_normalizes_to(self, alias, goal.predicate.1),
(None, Some(alias)) => evaluate_normalizes_to(self, alias, goal.predicate.0),
// RHS is not a projection, only way this is true is if LHS normalizes-to RHS
(Some(alias_lhs), None) => evaluate_normalizes_to(self, alias_lhs, rhs, direction),
// LHS is not a projection, only way this is true is if RHS normalizes-to LHS
(None, Some(alias_rhs)) => {
evaluate_normalizes_to(self, alias_rhs, lhs, direction.invert())
}
(Some(alias_lhs), Some(alias_rhs)) => {
debug!("compute_alias_eq_goal: both sides are aliases");
let mut candidates = Vec::with_capacity(3);
let candidates = vec![
// LHS normalizes-to RHS
evaluate_normalizes_to(self, alias_lhs, rhs, direction),
// RHS normalizes-to RHS
evaluate_normalizes_to(self, alias_rhs, lhs, direction.invert()),
// Relate via substs
self.probe(|ecx| {
debug!("compute_alias_eq_goal: alias defids are equal, equating substs");
// Evaluate all 3 potential candidates for the alias' being equal
candidates.push(evaluate_normalizes_to(self, alias_lhs, goal.predicate.1));
candidates.push(evaluate_normalizes_to(self, alias_rhs, goal.predicate.0));
candidates.push(self.probe(|ecx| {
debug!("compute_alias_eq_goal: alias defids are equal, equating substs");
ecx.eq(goal.param_env, alias_lhs, alias_rhs)?;
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
}));
ecx.add_goals(
match direction {
ty::AliasRelationDirection::Equate => ecx
.infcx
.at(&ObligationCause::dummy(), goal.param_env)
.eq(DefineOpaqueTypes::No, alias_lhs, alias_rhs),
ty::AliasRelationDirection::Subtype => ecx
.infcx
.at(&ObligationCause::dummy(), goal.param_env)
.sub(DefineOpaqueTypes::No, alias_lhs, alias_rhs),
ty::AliasRelationDirection::Supertype => ecx
.infcx
.at(&ObligationCause::dummy(), goal.param_env)
.sup(DefineOpaqueTypes::No, alias_lhs, alias_rhs),
}?
.into_obligations()
.into_iter()
.map(|o| o.into()),
);
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
}),
];
debug!(?candidates);
self.try_merge_responses(candidates.into_iter())

View file

@ -92,6 +92,11 @@ impl<'a, 'tcx> TypeRelation<'tcx> for CollectAllMismatches<'a, 'tcx> {
}
impl<'tcx> ObligationEmittingRelation<'tcx> for CollectAllMismatches<'_, 'tcx> {
fn alias_relate_direction(&self) -> ty::AliasRelationDirection {
// FIXME(deferred_projection_equality): We really should get rid of this relation.
ty::AliasRelationDirection::Equate
}
fn register_obligations(&mut self, _obligations: PredicateObligations<'tcx>) {
// FIXME(deferred_projection_equality)
}