1
Fork 0

Remove AliasRelationDirection::Supertype

This commit is contained in:
Michael Goulet 2023-03-22 16:58:51 +00:00
parent f6fd754680
commit 244cdaa457
5 changed files with 98 additions and 90 deletions

View file

@ -128,7 +128,7 @@ impl<'tcx> InferCtxt<'tcx> {
(_, ty::Alias(AliasKind::Projection, _)) | (ty::Alias(AliasKind::Projection, _), _) (_, ty::Alias(AliasKind::Projection, _)) | (ty::Alias(AliasKind::Projection, _), _)
if self.tcx.trait_solver_next() => if self.tcx.trait_solver_next() =>
{ {
relation.register_type_equate_obligation(a, b); relation.register_type_relate_obligation(a, b);
Ok(a) Ok(a)
} }
@ -848,10 +848,9 @@ pub trait ObligationEmittingRelation<'tcx>: TypeRelation<'tcx> {
})]); })]);
} }
/// Register an obligation that both types must be equal to each other. /// Register an obligation that both types must be related to each other according to
/// /// the [`ty::AliasRelationDirection`] given by [`ObligationEmittingRelation::alias_relate_direction`]
/// If they aren't equal then the relation doesn't hold. fn register_type_relate_obligation(&mut self, a: Ty<'tcx>, b: Ty<'tcx>) {
fn register_type_equate_obligation(&mut self, a: Ty<'tcx>, b: Ty<'tcx>) {
self.register_predicates([ty::Binder::dummy(ty::PredicateKind::AliasRelate( self.register_predicates([ty::Binder::dummy(ty::PredicateKind::AliasRelate(
a.into(), a.into(),
b.into(), b.into(),
@ -859,7 +858,8 @@ pub trait ObligationEmittingRelation<'tcx>: TypeRelation<'tcx> {
))]); ))]);
} }
/// Relation direction emitted for `AliasRelate` predicates /// Relation direction emitted for `AliasRelate` predicates, corresponding to the direction
/// of the relation.
fn alias_relate_direction(&self) -> ty::AliasRelationDirection; fn alias_relate_direction(&self) -> ty::AliasRelationDirection;
} }

View file

@ -779,13 +779,31 @@ where
} }
fn alias_relate_direction(&self) -> ty::AliasRelationDirection { fn alias_relate_direction(&self) -> ty::AliasRelationDirection {
match self.ambient_variance { unreachable!("manually overridden to handle ty::Variance::Contravariant ambient variance")
ty::Variance::Covariant => ty::AliasRelationDirection::Subtype, }
ty::Variance::Contravariant => ty::AliasRelationDirection::Supertype,
ty::Variance::Invariant => ty::AliasRelationDirection::Equate, fn register_type_relate_obligation(&mut self, a: Ty<'tcx>, b: Ty<'tcx>) {
// FIXME(deferred_projection_equality): Implement this when we trigger it self.register_predicates([ty::Binder::dummy(match self.ambient_variance {
ty::Variance::Covariant => ty::PredicateKind::AliasRelate(
a.into(),
b.into(),
ty::AliasRelationDirection::Subtype,
),
// a :> b is b <: a
ty::Variance::Contravariant => ty::PredicateKind::AliasRelate(
b.into(),
a.into(),
ty::AliasRelationDirection::Subtype,
),
ty::Variance::Invariant => ty::PredicateKind::AliasRelate(
a.into(),
b.into(),
ty::AliasRelationDirection::Equate,
),
// FIXME(deferred_projection_equality): Implement this when we trigger it.
// Probably just need to do nothing here.
ty::Variance::Bivariant => unreachable!(), ty::Variance::Bivariant => unreachable!(),
} })]);
} }
} }

View file

@ -648,17 +648,6 @@ pub enum PredicateKind<'tcx> {
pub enum AliasRelationDirection { pub enum AliasRelationDirection {
Equate, Equate,
Subtype, Subtype,
Supertype,
}
impl AliasRelationDirection {
pub fn invert(self) -> Self {
match self {
AliasRelationDirection::Equate => AliasRelationDirection::Equate,
AliasRelationDirection::Subtype => AliasRelationDirection::Supertype,
AliasRelationDirection::Supertype => AliasRelationDirection::Subtype,
}
}
} }
impl std::fmt::Display for AliasRelationDirection { impl std::fmt::Display for AliasRelationDirection {
@ -666,7 +655,6 @@ impl std::fmt::Display for AliasRelationDirection {
match self { match self {
AliasRelationDirection::Equate => write!(f, " == "), AliasRelationDirection::Equate => write!(f, " == "),
AliasRelationDirection::Subtype => write!(f, " <: "), AliasRelationDirection::Subtype => write!(f, " <: "),
AliasRelationDirection::Supertype => write!(f, " :> "),
} }
} }
} }

View file

@ -459,6 +459,25 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
}) })
} }
#[instrument(level = "debug", skip(self, param_env), ret)]
pub(super) fn sub<T: ToTrace<'tcx>>(
&mut self,
param_env: ty::ParamEnv<'tcx>,
sub: T,
sup: T,
) -> Result<(), NoSolution> {
self.infcx
.at(&ObligationCause::dummy(), param_env)
.sub(DefineOpaqueTypes::No, sub, sup)
.map(|InferOk { value: (), obligations }| {
self.add_goals(obligations.into_iter().map(|o| o.into()));
})
.map_err(|e| {
debug!(?e, "failed to subtype");
NoSolution
})
}
/// Equates two values returning the nested goals without adding them /// Equates two values returning the nested goals without adding them
/// to the nested goals of the `EvalCtxt`. /// to the nested goals of the `EvalCtxt`.
/// ///

View file

@ -17,7 +17,6 @@
use rustc_hir::def_id::DefId; use rustc_hir::def_id::DefId;
use rustc_infer::infer::canonical::{Canonical, CanonicalVarValues}; use rustc_infer::infer::canonical::{Canonical, CanonicalVarValues};
use rustc_infer::infer::{DefineOpaqueTypes, InferOk};
use rustc_infer::traits::query::NoSolution; use rustc_infer::traits::query::NoSolution;
use rustc_middle::traits::solve::{ use rustc_middle::traits::solve::{
CanonicalGoal, CanonicalResponse, Certainty, ExternalConstraints, ExternalConstraintsData, CanonicalGoal, CanonicalResponse, Certainty, ExternalConstraints, ExternalConstraintsData,
@ -101,11 +100,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
// That won't actually reflect in the query response, so it seems moot. // That won't actually reflect in the query response, so it seems moot.
self.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS) self.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
} else { } else {
let InferOk { value: (), obligations } = self self.sub(goal.param_env, goal.predicate.a, goal.predicate.b)?;
.infcx
.at(&ObligationCause::dummy(), goal.param_env)
.sub(DefineOpaqueTypes::No, goal.predicate.a, goal.predicate.b)?;
self.add_goals(obligations.into_iter().map(|pred| pred.into()));
self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes) self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
} }
} }
@ -161,44 +156,41 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
goal: Goal<'tcx, (ty::Term<'tcx>, ty::Term<'tcx>, ty::AliasRelationDirection)>, goal: Goal<'tcx, (ty::Term<'tcx>, ty::Term<'tcx>, ty::AliasRelationDirection)>,
) -> QueryResult<'tcx> { ) -> QueryResult<'tcx> {
let tcx = self.tcx(); let tcx = self.tcx();
// We may need to invert the alias relation direction if dealing an alias on the RHS.
enum Invert {
No,
Yes,
}
let evaluate_normalizes_to =
|ecx: &mut EvalCtxt<'_, 'tcx>, alias, other, direction, invert| {
debug!("evaluate_normalizes_to(alias={:?}, other={:?})", alias, other);
let result = ecx.probe(|ecx| {
let other = match direction {
// This is purely an optimization.
ty::AliasRelationDirection::Equate => other,
let evaluate_normalizes_to = |ecx: &mut EvalCtxt<'_, 'tcx>, alias, other, direction| { ty::AliasRelationDirection::Subtype => {
debug!("evaluate_normalizes_to(alias={:?}, other={:?})", alias, other); let fresh = ecx.next_term_infer_of_kind(other);
let result = ecx.probe(|ecx| { let (sub, sup) = match invert {
let other = match direction { Invert::No => (fresh, other),
// This is purely an optimization. Invert::Yes => (other, fresh),
ty::AliasRelationDirection::Equate => other, };
ecx.sub(goal.param_env, sub, sup)?;
ty::AliasRelationDirection::Subtype | ty::AliasRelationDirection::Supertype => { fresh
let fresh = ecx.next_term_infer_of_kind(other); }
let (sub, sup) = if direction == ty::AliasRelationDirection::Subtype { };
(fresh, other) ecx.add_goal(goal.with(
} else { tcx,
(other, fresh) ty::Binder::dummy(ty::ProjectionPredicate {
}; projection_ty: alias,
ecx.add_goals( term: other,
ecx.infcx }),
.at(&ObligationCause::dummy(), goal.param_env) ));
.sub(DefineOpaqueTypes::No, sub, sup)? ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
.into_obligations() });
.into_iter() debug!("evaluate_normalizes_to({alias}, {other}, {direction:?}) -> {result:?}");
.map(|o| o.into()), result
); };
fresh
}
};
ecx.add_goal(goal.with(
tcx,
ty::Binder::dummy(ty::ProjectionPredicate {
projection_ty: alias,
term: other,
}),
));
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
});
debug!("evaluate_normalizes_to({alias}, {other}, {direction:?}) -> {result:?}");
result
};
let (lhs, rhs, direction) = goal.predicate; let (lhs, rhs, direction) = goal.predicate;
@ -212,11 +204,13 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
(None, None) => bug!("`AliasRelate` goal without an alias on either lhs or rhs"), (None, None) => bug!("`AliasRelate` goal without an alias on either lhs or rhs"),
// RHS is not a projection, only way this is true is if LHS normalizes-to RHS // 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), (Some(alias_lhs), None) => {
evaluate_normalizes_to(self, alias_lhs, rhs, direction, Invert::No)
}
// LHS is not a projection, only way this is true is if RHS normalizes-to LHS // LHS is not a projection, only way this is true is if RHS normalizes-to LHS
(None, Some(alias_rhs)) => { (None, Some(alias_rhs)) => {
evaluate_normalizes_to(self, alias_rhs, lhs, direction.invert()) evaluate_normalizes_to(self, alias_rhs, lhs, direction, Invert::Yes)
} }
(Some(alias_lhs), Some(alias_rhs)) => { (Some(alias_lhs), Some(alias_rhs)) => {
@ -224,34 +218,23 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
let candidates = vec![ let candidates = vec![
// LHS normalizes-to RHS // LHS normalizes-to RHS
evaluate_normalizes_to(self, alias_lhs, rhs, direction), evaluate_normalizes_to(self, alias_lhs, rhs, direction, Invert::No),
// RHS normalizes-to RHS // RHS normalizes-to RHS
evaluate_normalizes_to(self, alias_rhs, lhs, direction.invert()), evaluate_normalizes_to(self, alias_rhs, lhs, direction, Invert::Yes),
// Relate via substs // Relate via substs
self.probe(|ecx| { self.probe(|ecx| {
debug!( debug!(
"compute_alias_relate_goal: alias defids are equal, equating substs" "compute_alias_relate_goal: alias defids are equal, equating substs"
); );
ecx.add_goals( match direction {
match direction { ty::AliasRelationDirection::Equate => {
ty::AliasRelationDirection::Equate => ecx ecx.eq(goal.param_env, alias_lhs, alias_rhs)?;
.infcx }
.at(&ObligationCause::dummy(), goal.param_env) ty::AliasRelationDirection::Subtype => {
.eq(DefineOpaqueTypes::No, alias_lhs, alias_rhs), ecx.sub(goal.param_env, 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) ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
}), }),