bjoernager/rust
bjoernager/rust
1
Fork 0
Code Issues Pull requests Activity

Make infer higher ranked equate use bidirectional subtyping in invariant context

Browse source
This commit is contained in:
Santiago Pastorino 2023-11-27 22:36:39 -03:00
parent 384d26fc7e
commit 23ae3dbb31
No known key found for this signature in database
GPG key ID: 8131A24E0C79EFAF
15 changed files with 153 additions and 47 deletions
Download patch file Download diff file Expand all files Collapse all files

27
compiler/rustc_infer/src/infer/relate/equate.rs
View file

@ -1,5 +1,6 @@
use super::combine::{CombineFields, ObligationEmittingRelation};
use super::StructurallyRelateAliases;
use crate::infer::BoundRegionConversionTime::HigherRankedType;
use crate::infer::{DefineOpaqueTypes, SubregionOrigin};
use crate::traits::PredicateObligations;
@ -168,8 +169,30 @@ impl<'tcx> TypeRelation<'tcx> for Equate<'_, '_, 'tcx> {
}
if a.skip_binder().has_escaping_bound_vars() || b.skip_binder().has_escaping_bound_vars() {
self.fields.higher_ranked_sub(a, b, self.a_is_expected)?;
self.fields.higher_ranked_sub(b, a, self.a_is_expected)?;
// 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`.
let span = self.fields.trace.cause.span;
let infcx = self.fields.infcx;
// Check if `exists<..> A == for<..> B`
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)
})?;
} else {
// Fast path for the common case.
self.relate(a.skip_binder(), b.skip_binder())?;