add unused NormalizesTo predicate

This commit is contained in:
lcnr 2023-12-07 17:52:51 +01:00
parent 40aa9f4fd9
commit 3978f545ba
18 changed files with 128 additions and 64 deletions

View file

@ -657,19 +657,11 @@ pub(in super::super) fn obligations_for_self_ty<'b>(
| ty::PredicateKind::Clause(ty::ClauseKind::TypeOutlives(..))
| ty::PredicateKind::Clause(ty::ClauseKind::WellFormed(..))
| ty::PredicateKind::ObjectSafe(..)
| ty::PredicateKind::NormalizesTo(..)
| ty::PredicateKind::AliasRelate(..)
| ty::PredicateKind::Clause(ty::ClauseKind::ConstEvaluatable(..))
| ty::PredicateKind::ConstEquate(..)
// N.B., this predicate is created by breaking down a
// `ClosureType: FnFoo()` predicate, where
// `ClosureType` represents some `Closure`. It can't
// possibly be referring to the current closure,
// because we haven't produced the `Closure` for
// this closure yet; this is exactly why the other
// code is looking for a self type of an unresolved
// inference variable.
| ty::PredicateKind::Ambiguous
=> None,
| ty::PredicateKind::Ambiguous => None,
},
)
}

View file

@ -261,9 +261,14 @@ pub fn filter_only_self_that_defines(mut self, assoc_ty: Ident) -> Self {
fn elaborate(&mut self, elaboratable: &O) {
let tcx = self.visited.tcx;
let bound_predicate = elaboratable.predicate().kind();
match bound_predicate.skip_binder() {
ty::PredicateKind::Clause(ty::ClauseKind::Trait(data)) => {
// We only elaborate clauses.
let Some(clause) = elaboratable.predicate().as_clause() else {
return;
};
let bound_clause = clause.kind();
match bound_clause.skip_binder() {
ty::ClauseKind::Trait(data) => {
// Negative trait bounds do not imply any supertrait bounds
if data.polarity == ty::ImplPolarity::Negative {
return;
@ -280,49 +285,16 @@ fn elaborate(&mut self, elaboratable: &O) {
let obligations =
predicates.predicates.iter().enumerate().map(|(index, &(clause, span))| {
elaboratable.child_with_derived_cause(
clause.subst_supertrait(tcx, &bound_predicate.rebind(data.trait_ref)),
clause.subst_supertrait(tcx, &bound_clause.rebind(data.trait_ref)),
span,
bound_predicate.rebind(data),
bound_clause.rebind(data),
index,
)
});
debug!(?data, ?obligations, "super_predicates");
self.extend_deduped(obligations);
}
ty::PredicateKind::Clause(ty::ClauseKind::WellFormed(..)) => {
// Currently, we do not elaborate WF predicates,
// although we easily could.
}
ty::PredicateKind::ObjectSafe(..) => {
// Currently, we do not elaborate object-safe
// predicates.
}
ty::PredicateKind::Subtype(..) => {
// Currently, we do not "elaborate" predicates like `X <: Y`,
// though conceivably we might.
}
ty::PredicateKind::Coerce(..) => {
// Currently, we do not "elaborate" predicates like `X -> Y`,
// though conceivably we might.
}
ty::PredicateKind::Clause(ty::ClauseKind::Projection(..)) => {
// Nothing to elaborate in a projection predicate.
}
ty::PredicateKind::Clause(ty::ClauseKind::ConstEvaluatable(..)) => {
// Currently, we do not elaborate const-evaluatable
// predicates.
}
ty::PredicateKind::ConstEquate(..) => {
// Currently, we do not elaborate const-equate
// predicates.
}
ty::PredicateKind::Clause(ty::ClauseKind::RegionOutlives(..)) => {
// Nothing to elaborate from `'a: 'b`.
}
ty::PredicateKind::Clause(ty::ClauseKind::TypeOutlives(ty::OutlivesPredicate(
ty_max,
r_min,
))) => {
ty::ClauseKind::TypeOutlives(ty::OutlivesPredicate(ty_max, r_min)) => {
// We know that `T: 'a` for some type `T`. We can
// often elaborate this. For example, if we know that
// `[U]: 'a`, that implies that `U: 'a`. Similarly, if
@ -385,15 +357,25 @@ fn elaborate(&mut self, elaboratable: &O) {
}
})
.map(|clause| {
elaboratable.child(bound_predicate.rebind(clause).to_predicate(tcx))
elaboratable.child(bound_clause.rebind(clause).to_predicate(tcx))
}),
);
}
ty::PredicateKind::Ambiguous => {}
ty::PredicateKind::AliasRelate(..) => {
// No
ty::ClauseKind::RegionOutlives(..) => {
// Nothing to elaborate from `'a: 'b`.
}
ty::PredicateKind::Clause(ty::ClauseKind::ConstArgHasType(..)) => {
ty::ClauseKind::WellFormed(..) => {
// Currently, we do not elaborate WF predicates,
// although we easily could.
}
ty::ClauseKind::Projection(..) => {
// Nothing to elaborate in a projection predicate.
}
ty::ClauseKind::ConstEvaluatable(..) => {
// Currently, we do not elaborate const-evaluatable
// predicates.
}
ty::ClauseKind::ConstArgHasType(..) => {
// Nothing to elaborate
}
}

View file

@ -121,6 +121,7 @@ impl<'tcx> Interner for TyCtxt<'tcx> {
type RegionOutlivesPredicate = ty::RegionOutlivesPredicate<'tcx>;
type TypeOutlivesPredicate = ty::TypeOutlivesPredicate<'tcx>;
type ProjectionPredicate = ty::ProjectionPredicate<'tcx>;
type NormalizesTo = ty::NormalizesTo<'tcx>;
type SubtypePredicate = ty::SubtypePredicate<'tcx>;
type CoercePredicate = ty::CoercePredicate<'tcx>;
type ClosureKind = ty::ClosureKind;

View file

@ -272,6 +272,10 @@ fn add_predicate_atom(&mut self, atom: ty::PredicateKind<'_>) {
self.add_const(found);
}
ty::PredicateKind::Ambiguous => {}
ty::PredicateKind::NormalizesTo(ty::NormalizesTo { alias, term }) => {
self.add_alias_ty(alias);
self.add_term(term);
}
ty::PredicateKind::AliasRelate(t1, t2, _) => {
self.add_term(t1);
self.add_term(t2);

View file

@ -553,6 +553,10 @@ pub fn is_coinductive(self, tcx: TyCtxt<'tcx>) -> bool {
pub fn allow_normalization(self) -> bool {
match self.kind().skip_binder() {
PredicateKind::Clause(ClauseKind::WellFormed(_)) => false,
// `NormalizesTo` is only used in the new solver, so this shouldn't
// matter. Normalizing `term` would be 'wrong' however, as it changes whether
// `normalizes-to(<T as Trait>::Assoc, <T as Trait>::Assoc)` holds.
PredicateKind::NormalizesTo(..) => false,
PredicateKind::Clause(ClauseKind::Trait(_))
| PredicateKind::Clause(ClauseKind::RegionOutlives(_))
| PredicateKind::Clause(ClauseKind::TypeOutlives(_))
@ -1093,6 +1097,33 @@ pub fn projection_def_id(&self) -> DefId {
}
}
/// Used by the new solver. Unlike a `ProjectionPredicate` this can only be
/// proven by actually normalizing `alias`.
#[derive(Copy, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)]
#[derive(HashStable, TypeFoldable, TypeVisitable, Lift)]
pub struct NormalizesTo<'tcx> {
pub alias: AliasTy<'tcx>,
pub term: Term<'tcx>,
}
impl<'tcx> NormalizesTo<'tcx> {
pub fn self_ty(self) -> Ty<'tcx> {
self.alias.self_ty()
}
pub fn with_self_ty(self, tcx: TyCtxt<'tcx>, self_ty: Ty<'tcx>) -> NormalizesTo<'tcx> {
Self { alias: self.alias.with_self_ty(tcx, self_ty), ..self }
}
pub fn trait_def_id(self, tcx: TyCtxt<'tcx>) -> DefId {
self.alias.trait_def_id(tcx)
}
pub fn def_id(self) -> DefId {
self.alias.def_id
}
}
pub trait ToPolyTraitRef<'tcx> {
fn to_poly_trait_ref(&self) -> PolyTraitRef<'tcx>;
}
@ -1274,6 +1305,12 @@ fn to_predicate(self, tcx: TyCtxt<'tcx>) -> Clause<'tcx> {
}
}
impl<'tcx> ToPredicate<'tcx> for NormalizesTo<'tcx> {
fn to_predicate(self, tcx: TyCtxt<'tcx>) -> Predicate<'tcx> {
PredicateKind::NormalizesTo(self).to_predicate(tcx)
}
}
impl<'tcx> Predicate<'tcx> {
pub fn to_opt_poly_trait_pred(self) -> Option<PolyTraitPredicate<'tcx>> {
let predicate = self.kind();
@ -1281,6 +1318,7 @@ pub fn to_opt_poly_trait_pred(self) -> Option<PolyTraitPredicate<'tcx>> {
PredicateKind::Clause(ClauseKind::Trait(t)) => Some(predicate.rebind(t)),
PredicateKind::Clause(ClauseKind::Projection(..))
| PredicateKind::Clause(ClauseKind::ConstArgHasType(..))
| PredicateKind::NormalizesTo(..)
| PredicateKind::AliasRelate(..)
| PredicateKind::Subtype(..)
| PredicateKind::Coerce(..)
@ -1300,6 +1338,7 @@ pub fn to_opt_poly_projection_pred(self) -> Option<PolyProjectionPredicate<'tcx>
PredicateKind::Clause(ClauseKind::Projection(t)) => Some(predicate.rebind(t)),
PredicateKind::Clause(ClauseKind::Trait(..))
| PredicateKind::Clause(ClauseKind::ConstArgHasType(..))
| PredicateKind::NormalizesTo(..)
| PredicateKind::AliasRelate(..)
| PredicateKind::Subtype(..)
| PredicateKind::Coerce(..)

View file

@ -2814,6 +2814,7 @@ macro_rules! define_print_and_forward_display {
p!("the constant `", print(c1), "` equals `", print(c2), "`")
}
ty::PredicateKind::Ambiguous => p!("ambiguous"),
ty::PredicateKind::NormalizesTo(data) => p!(print(data.alias), " normalizes-to ", print(data.term)),
ty::PredicateKind::AliasRelate(t1, t2, dir) => p!(print(t1), write(" {} ", dir), print(t2)),
}
}

View file

@ -173,6 +173,12 @@ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
}
}
impl<'tcx> fmt::Debug for ty::NormalizesTo<'tcx> {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
write!(f, "NormalizesTo({:?}, {:?})", self.alias, self.term)
}
}
impl<'tcx> fmt::Debug for ty::Predicate<'tcx> {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
write!(f, "{:?}", self.kind())

View file

@ -601,6 +601,7 @@ fn stable(&self, tables: &mut Tables<'tcx>) -> Self::T {
stable_mir::ty::PredicateKind::ConstEquate(a.stable(tables), b.stable(tables))
}
PredicateKind::Ambiguous => stable_mir::ty::PredicateKind::Ambiguous,
PredicateKind::NormalizesTo(_pred) => unimplemented!(),
PredicateKind::AliasRelate(a, b, alias_relation_direction) => {
stable_mir::ty::PredicateKind::AliasRelate(
a.unpack().stable(tables),

View file

@ -423,6 +423,7 @@ fn compute_goal(&mut self, goal: Goal<'tcx, ty::Predicate<'tcx>>) -> QueryResult
ty::PredicateKind::ConstEquate(_, _) => {
bug!("ConstEquate should not be emitted when `-Ztrait-solver=next` is active")
}
ty::PredicateKind::NormalizesTo(_) => unimplemented!(),
ty::PredicateKind::AliasRelate(lhs, rhs, direction) => self
.compute_alias_relate_goal(Goal {
param_env,

View file

@ -108,6 +108,11 @@ fn select_where_possible(&mut self, infcx: &InferCtxt<'tcx>) -> Vec<FulfillmentE
MismatchedProjectionTypes { err: TypeError::Mismatch },
)
}
ty::PredicateKind::NormalizesTo(..) => {
FulfillmentErrorCode::CodeProjectionError(
MismatchedProjectionTypes { err: TypeError::Mismatch },
)
}
ty::PredicateKind::AliasRelate(_, _, _) => {
FulfillmentErrorCode::CodeProjectionError(
MismatchedProjectionTypes { err: TypeError::Mismatch },

View file

@ -820,6 +820,7 @@ fn evaluate_nested_obligations(
// the `ParamEnv`.
ty::PredicateKind::Clause(ty::ClauseKind::WellFormed(..))
| ty::PredicateKind::Clause(ty::ClauseKind::ConstArgHasType(..))
| ty::PredicateKind::NormalizesTo(..)
| ty::PredicateKind::AliasRelate(..)
| ty::PredicateKind::ObjectSafe(..)
| ty::PredicateKind::Subtype(..)

View file

@ -854,6 +854,11 @@ fn report_selection_error(
ty::PredicateKind::Ambiguous => span_bug!(span, "ambiguous"),
ty::PredicateKind::NormalizesTo(..) => span_bug!(
span,
"NormalizesTo predicate should never be the predicate cause of a SelectionError"
),
ty::PredicateKind::AliasRelate(..) => span_bug!(
span,
"AliasRelate predicate should never be the predicate cause of a SelectionError"

View file

@ -360,8 +360,11 @@ fn process_obligation(
ProcessResult::Changed(mk_pending(vec![obligation.with(infcx.tcx, pred)]))
}
ty::PredicateKind::Ambiguous => ProcessResult::Unchanged,
ty::PredicateKind::NormalizesTo(..) => {
bug!("NormalizesTo is only used by the new solver")
}
ty::PredicateKind::AliasRelate(..) => {
bug!("AliasRelate is only used for new solver")
bug!("AliasRelate is only used by the new solver")
}
},
Some(pred) => match pred {
@ -412,8 +415,11 @@ fn process_obligation(
}
ty::PredicateKind::Ambiguous => ProcessResult::Unchanged,
ty::PredicateKind::NormalizesTo(..) => {
bug!("NormalizesTo is only used by the new solver")
}
ty::PredicateKind::AliasRelate(..) => {
bug!("AliasRelate is only used for new solver")
bug!("AliasRelate is only used by the new solver")
}
// General case overflow check. Allow `process_trait_obligation`

View file

@ -123,9 +123,9 @@ pub fn compute_implied_outlives_bounds_inner<'tcx>(
Some(pred) => pred,
};
match pred {
ty::PredicateKind::Clause(ty::ClauseKind::Trait(..))
// FIXME(const_generics): Make sure that `<'a, 'b, const N: &'a &'b u32>` is sound
// if we ever support that
ty::PredicateKind::Clause(ty::ClauseKind::Trait(..))
| ty::PredicateKind::Clause(ty::ClauseKind::ConstArgHasType(..))
| ty::PredicateKind::Subtype(..)
| ty::PredicateKind::Coerce(..)
@ -134,8 +134,8 @@ pub fn compute_implied_outlives_bounds_inner<'tcx>(
| ty::PredicateKind::Clause(ty::ClauseKind::ConstEvaluatable(..))
| ty::PredicateKind::ConstEquate(..)
| ty::PredicateKind::Ambiguous
| ty::PredicateKind::AliasRelate(..)
=> {}
| ty::PredicateKind::NormalizesTo(..)
| ty::PredicateKind::AliasRelate(..) => {}
// We need to search through *all* WellFormed predicates
ty::PredicateKind::Clause(ty::ClauseKind::WellFormed(arg)) => {
@ -143,10 +143,9 @@ pub fn compute_implied_outlives_bounds_inner<'tcx>(
}
// We need to register region relationships
ty::PredicateKind::Clause(ty::ClauseKind::RegionOutlives(ty::OutlivesPredicate(
r_a,
r_b,
))) => outlives_bounds.push(ty::OutlivesPredicate(r_a.into(), r_b)),
ty::PredicateKind::Clause(ty::ClauseKind::RegionOutlives(
ty::OutlivesPredicate(r_a, r_b),
)) => outlives_bounds.push(ty::OutlivesPredicate(r_a.into(), r_b)),
ty::PredicateKind::Clause(ty::ClauseKind::TypeOutlives(ty::OutlivesPredicate(
ty_a,

View file

@ -990,8 +990,11 @@ fn evaluate_predicate_recursively<'o>(
}
}
}
ty::PredicateKind::NormalizesTo(..) => {
bug!("NormalizesTo is only used by the new solver")
}
ty::PredicateKind::AliasRelate(..) => {
bug!("AliasRelate is only used for new solver")
bug!("AliasRelate is only used by the new solver")
}
ty::PredicateKind::Ambiguous => Ok(EvaluatedToAmbig),
ty::PredicateKind::Clause(ty::ClauseKind::ConstArgHasType(ct, ty)) => {

View file

@ -55,6 +55,7 @@ fn not_outlives_predicate(p: ty::Predicate<'_>) -> bool {
ty::PredicateKind::Clause(ty::ClauseKind::Trait(..))
| ty::PredicateKind::Clause(ty::ClauseKind::Projection(..))
| ty::PredicateKind::Clause(ty::ClauseKind::ConstArgHasType(..))
| ty::PredicateKind::NormalizesTo(..)
| ty::PredicateKind::AliasRelate(..)
| ty::PredicateKind::Clause(ty::ClauseKind::WellFormed(..))
| ty::PredicateKind::ObjectSafe(..)

View file

@ -57,6 +57,7 @@ pub trait Interner: Sized {
type RegionOutlivesPredicate: Clone + Debug + Hash + Eq;
type TypeOutlivesPredicate: Clone + Debug + Hash + Eq;
type ProjectionPredicate: Clone + Debug + Hash + Eq;
type NormalizesTo: Clone + Debug + Hash + Eq;
type SubtypePredicate: Clone + Debug + Hash + Eq;
type CoercePredicate: Clone + Debug + Hash + Eq;
type ClosureKind: Clone + Debug + Hash + Eq;

View file

@ -153,6 +153,15 @@ pub enum PredicateKind<I: Interner> {
/// Used for coherence to mark opaque types as possibly equal to each other but ambiguous.
Ambiguous,
/// The alias normalizes to `term`. Unlike `Projection`, this always fails if the alias
/// cannot be normalized in the current context.
///
/// `Projection(<T as Trait>::Assoc, ?x)` results in `?x == <T as Trait>::Assoc` while
/// `NormalizesTo(<T as Trait>::Assoc, ?x)` results in `NoSolution`.
///
/// Only used in the new solver.
NormalizesTo(I::NormalizesTo),
/// Separate from `ClauseKind::Projection` which is used for normalization in new solver.
/// This predicate requires two terms to be equal to eachother.
///
@ -160,6 +169,7 @@ pub enum PredicateKind<I: Interner> {
AliasRelate(I::Term, I::Term, AliasRelationDirection),
}
/// FIXME: This impl sh
impl<I: Interner> Copy for PredicateKind<I>
where
I::DefId: Copy,
@ -168,6 +178,7 @@ impl<I: Interner> Copy for PredicateKind<I>
I::Term: Copy,
I::CoercePredicate: Copy,
I::SubtypePredicate: Copy,
I::NormalizesTo: Copy,
ClauseKind<I>: Copy,
{
}
@ -198,6 +209,7 @@ impl<I: Interner> TypeFoldable<I> for PredicateKind<I>
I::Term: TypeFoldable<I>,
I::CoercePredicate: TypeFoldable<I>,
I::SubtypePredicate: TypeFoldable<I>,
I::NormalizesTo: TypeFoldable<I>,
ClauseKind<I>: TypeFoldable<I>,
{
fn try_fold_with<F: FallibleTypeFolder<I>>(self, folder: &mut F) -> Result<Self, F::Error> {
@ -210,6 +222,7 @@ fn try_fold_with<F: FallibleTypeFolder<I>>(self, folder: &mut F) -> Result<Self,
PredicateKind::ConstEquate(a.try_fold_with(folder)?, b.try_fold_with(folder)?)
}
PredicateKind::Ambiguous => PredicateKind::Ambiguous,
PredicateKind::NormalizesTo(p) => PredicateKind::NormalizesTo(p.try_fold_with(folder)?),
PredicateKind::AliasRelate(a, b, d) => PredicateKind::AliasRelate(
a.try_fold_with(folder)?,
b.try_fold_with(folder)?,
@ -227,6 +240,7 @@ impl<I: Interner> TypeVisitable<I> for PredicateKind<I>
I::Term: TypeVisitable<I>,
I::CoercePredicate: TypeVisitable<I>,
I::SubtypePredicate: TypeVisitable<I>,
I::NormalizesTo: TypeVisitable<I>,
ClauseKind<I>: TypeVisitable<I>,
{
fn visit_with<V: TypeVisitor<I>>(&self, visitor: &mut V) -> ControlFlow<V::BreakTy> {
@ -240,6 +254,7 @@ fn visit_with<V: TypeVisitor<I>>(&self, visitor: &mut V) -> ControlFlow<V::Break
b.visit_with(visitor)
}
PredicateKind::Ambiguous => ControlFlow::Continue(()),
PredicateKind::NormalizesTo(p) => p.visit_with(visitor),
PredicateKind::AliasRelate(a, b, d) => {
a.visit_with(visitor)?;
b.visit_with(visitor)?;
@ -294,6 +309,7 @@ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
}
PredicateKind::ConstEquate(c1, c2) => write!(f, "ConstEquate({c1:?}, {c2:?})"),
PredicateKind::Ambiguous => write!(f, "Ambiguous"),
PredicateKind::NormalizesTo(p) => p.fmt(f),
PredicateKind::AliasRelate(t1, t2, dir) => {
write!(f, "AliasRelate({t1:?}, {dir:?}, {t2:?})")
}