Rebase fallout from TypeRelating::binders, inline higher_ranked_sub
This commit is contained in:
parent
b1536568db
commit
5072b659ff
@ -1,70 +1,11 @@
|
||||
//! Helper routines for higher-ranked things. See the `doc` module at
|
||||
//! the end of the file for details.
|
||||
|
||||
use super::combine::CombineFields;
|
||||
use crate::infer::CombinedSnapshot;
|
||||
use crate::infer::{HigherRankedType, InferCtxt};
|
||||
use crate::infer::InferCtxt;
|
||||
use rustc_middle::ty::fold::FnMutDelegate;
|
||||
use rustc_middle::ty::relate::{Relate, RelateResult, TypeRelation};
|
||||
use rustc_middle::ty::{self, Binder, Ty, TyCtxt, TypeFoldable};
|
||||
|
||||
impl<'a, 'tcx> CombineFields<'a, 'tcx> {
|
||||
/// Checks whether `for<..> sub <: for<..> sup` holds.
|
||||
///
|
||||
/// For this to hold, **all** instantiations of the super type
|
||||
/// have to be a super type of **at least one** instantiation of
|
||||
/// the subtype.
|
||||
///
|
||||
/// This is implemented by first entering a new universe.
|
||||
/// We then replace all bound variables in `sup` with placeholders,
|
||||
/// and all bound variables in `sub` with inference vars.
|
||||
/// We can then just relate the two resulting types as normal.
|
||||
///
|
||||
/// Note: this is a subtle algorithm. For a full explanation, please see
|
||||
/// the [rustc dev guide][rd]
|
||||
///
|
||||
/// [rd]: https://rustc-dev-guide.rust-lang.org/borrow_check/region_inference/placeholders_and_universes.html
|
||||
#[instrument(skip(self), level = "debug")]
|
||||
pub fn higher_ranked_sub<T>(
|
||||
&mut self,
|
||||
sub: Binder<'tcx, T>,
|
||||
sup: Binder<'tcx, T>,
|
||||
sub_is_expected: bool,
|
||||
) -> RelateResult<'tcx, ()>
|
||||
where
|
||||
T: Relate<'tcx>,
|
||||
{
|
||||
let span = self.trace.cause.span;
|
||||
// First, we instantiate each bound region in the supertype with a
|
||||
// fresh placeholder region. Note that this automatically creates
|
||||
// a new universe if needed.
|
||||
self.infcx.enter_forall(sup, |sup_prime| {
|
||||
// Next, we instantiate each bound region in the subtype
|
||||
// with a fresh region variable. These region variables --
|
||||
// but no other preexisting region variables -- can name
|
||||
// the placeholders.
|
||||
let sub_prime =
|
||||
self.infcx.instantiate_binder_with_fresh_vars(span, HigherRankedType, sub);
|
||||
debug!("a_prime={:?}", sub_prime);
|
||||
debug!("b_prime={:?}", sup_prime);
|
||||
|
||||
// Compare types now that bound regions have been replaced.
|
||||
// Reorder the inputs so that the expected is passed first.
|
||||
let result = if sub_is_expected {
|
||||
self.sub().relate(sub_prime, sup_prime)
|
||||
} else {
|
||||
self.sup().relate(sup_prime, sub_prime)
|
||||
};
|
||||
|
||||
if result.is_ok() {
|
||||
debug!("OK result={result:?}");
|
||||
}
|
||||
// NOTE: returning the result here would be dangerous as it contains
|
||||
// placeholders which **must not** be named afterwards.
|
||||
result.map(|_| ())
|
||||
})
|
||||
}
|
||||
}
|
||||
use rustc_middle::ty::relate::RelateResult;
|
||||
use rustc_middle::ty::{self, Ty, TyCtxt, TypeFoldable};
|
||||
|
||||
impl<'tcx> InferCtxt<'tcx> {
|
||||
/// Replaces all bound variables (lifetimes, types, and constants) bound by
|
||||
|
@ -1,4 +1,5 @@
|
||||
use super::combine::CombineFields;
|
||||
use crate::infer::BoundRegionConversionTime::HigherRankedType;
|
||||
use crate::infer::{
|
||||
DefineOpaqueTypes, ObligationEmittingRelation, StructurallyRelateAliases, SubregionOrigin,
|
||||
};
|
||||
@ -214,16 +215,59 @@ impl<'tcx> TypeRelation<'tcx> for TypeRelating<'_, '_, 'tcx> {
|
||||
{
|
||||
self.relate(a, b)?;
|
||||
} else {
|
||||
let span = self.fields.trace.cause.span;
|
||||
let infcx = self.fields.infcx;
|
||||
|
||||
match self.ambient_variance {
|
||||
// Checks whether `for<..> sub <: for<..> sup` holds.
|
||||
//
|
||||
// For this to hold, **all** instantiations of the super type
|
||||
// have to be a super type of **at least one** instantiation of
|
||||
// the subtype.
|
||||
//
|
||||
// This is implemented by first entering a new universe.
|
||||
// We then replace all bound variables in `sup` with placeholders,
|
||||
// and all bound variables in `sub` with inference vars.
|
||||
// We can then just relate the two resulting types as normal.
|
||||
//
|
||||
// Note: this is a subtle algorithm. For a full explanation, please see
|
||||
// the [rustc dev guide][rd]
|
||||
//
|
||||
// [rd]: https://rustc-dev-guide.rust-lang.org/borrow_check/region_inference/placeholders_and_universes.html
|
||||
ty::Covariant => {
|
||||
self.fields.higher_ranked_sub(a, b, true)?;
|
||||
infcx.enter_forall(b, |b| {
|
||||
let a = infcx.instantiate_binder_with_fresh_vars(span, HigherRankedType, a);
|
||||
self.relate(a, b)
|
||||
})?;
|
||||
}
|
||||
ty::Contravariant => {
|
||||
self.fields.higher_ranked_sub(b, a, false)?;
|
||||
infcx.enter_forall(a, |a| {
|
||||
let b = infcx.instantiate_binder_with_fresh_vars(span, HigherRankedType, b);
|
||||
self.relate(a, b)
|
||||
})?;
|
||||
}
|
||||
|
||||
// When **equating** binders, we check that there is a 1-to-1
|
||||
// correspondence between the bound vars in both types.
|
||||
//
|
||||
// We do so by separately instantiating one of the binders with
|
||||
// placeholders and the other with inference variables and then
|
||||
// equating the instantiated types.
|
||||
//
|
||||
// We want `for<..> A == for<..> B` -- therefore we want
|
||||
// `exists<..> A == for<..> B` and `exists<..> B == for<..> A`.
|
||||
// Check if `exists<..> A == for<..> B`
|
||||
ty::Invariant => {
|
||||
self.fields.higher_ranked_sub(a, b, true)?;
|
||||
self.fields.higher_ranked_sub(b, a, false)?;
|
||||
infcx.enter_forall(b, |b| {
|
||||
let a = infcx.instantiate_binder_with_fresh_vars(span, HigherRankedType, a);
|
||||
self.relate(a, b)
|
||||
})?;
|
||||
|
||||
// Check if `exists<..> B == for<..> A`.
|
||||
infcx.enter_forall(a, |a| {
|
||||
let b = infcx.instantiate_binder_with_fresh_vars(span, HigherRankedType, b);
|
||||
self.relate(a, b)
|
||||
})?;
|
||||
}
|
||||
ty::Bivariant => {
|
||||
unreachable!("Expected bivariance to be handled in relate_with_variance")
|
||||
|
Loading…
x
Reference in New Issue
Block a user