Rollup merge of #56214 - scalexm:unification, r=nikomatsakis
Implement chalk unification routines `ResolventOps` and `AggregateOps` are mostly straightforwardly translated from chalk. I had caught a few bugs already in my `chalk` branch and backported fixes to this branch, but there may be other ones left. EDIT: I hope there are none left now :) Fixes #54935.
This commit is contained in:
commit
a6c4771520
@ -11,30 +11,41 @@
|
||||
//! This code is kind of an alternate way of doing subtyping,
|
||||
//! supertyping, and type equating, distinct from the `combine.rs`
|
||||
//! code but very similar in its effect and design. Eventually the two
|
||||
//! ought to be merged. This code is intended for use in NLL.
|
||||
//! ought to be merged. This code is intended for use in NLL and chalk.
|
||||
//!
|
||||
//! Here are the key differences:
|
||||
//!
|
||||
//! - This code generally assumes that there are no unbound type
|
||||
//! inferences variables, because at NLL
|
||||
//! time types are fully inferred up-to regions.
|
||||
//! - Actually, to support user-given type annotations like
|
||||
//! `Vec<_>`, we do have some measure of support for type
|
||||
//! inference variables, but we impose some simplifying
|
||||
//! assumptions on them that would not be suitable for the infer
|
||||
//! code more generally. This could be fixed.
|
||||
//! - This code may choose to bypass some checks (e.g. the occurs check)
|
||||
//! in the case where we know that there are no unbound type inference
|
||||
//! variables. This is the case for NLL, because at NLL time types are fully
|
||||
//! inferred up-to regions.
|
||||
//! - This code uses "universes" to handle higher-ranked regions and
|
||||
//! not the leak-check. This is "more correct" than what rustc does
|
||||
//! and we are generally migrating in this direction, but NLL had to
|
||||
//! get there first.
|
||||
//!
|
||||
//! Also, this code assumes that there are no bound types at all, not even
|
||||
//! free ones. This is ok because:
|
||||
//! - we are not relating anything quantified over some type variable
|
||||
//! - we will have instantiated all the bound type vars already (the one
|
||||
//! thing we relate in chalk are basically domain goals and their
|
||||
//! constituents)
|
||||
|
||||
use crate::infer::InferCtxt;
|
||||
use crate::ty::fold::{TypeFoldable, TypeVisitor};
|
||||
use crate::ty::relate::{self, Relate, RelateResult, TypeRelation};
|
||||
use crate::ty::subst::Kind;
|
||||
use crate::ty::{self, Ty, TyCtxt};
|
||||
use crate::ty::error::TypeError;
|
||||
use crate::traits::DomainGoal;
|
||||
use rustc_data_structures::fx::FxHashMap;
|
||||
|
||||
#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
|
||||
pub enum NormalizationStrategy {
|
||||
Lazy,
|
||||
Eager,
|
||||
}
|
||||
|
||||
pub struct TypeRelating<'me, 'gcx: 'tcx, 'tcx: 'me, D>
|
||||
where
|
||||
D: TypeRelatingDelegate<'tcx>,
|
||||
@ -75,6 +86,10 @@ pub trait TypeRelatingDelegate<'tcx> {
|
||||
/// delegate.
|
||||
fn push_outlives(&mut self, sup: ty::Region<'tcx>, sub: ty::Region<'tcx>);
|
||||
|
||||
/// Push a domain goal that will need to be proved for the two types to
|
||||
/// be related. Used for lazy normalization.
|
||||
fn push_domain_goal(&mut self, domain_goal: DomainGoal<'tcx>);
|
||||
|
||||
/// Creates a new universe index. Used when instantiating placeholders.
|
||||
fn create_next_universe(&mut self) -> ty::UniverseIndex;
|
||||
|
||||
@ -105,6 +120,13 @@ pub trait TypeRelatingDelegate<'tcx> {
|
||||
/// relate `Foo<'?0>` with `Foo<'a>` (and probably add an outlives
|
||||
/// relation stating that `'?0: 'a`).
|
||||
fn generalize_existential(&mut self, universe: ty::UniverseIndex) -> ty::Region<'tcx>;
|
||||
|
||||
/// Define the normalization strategy to use, eager or lazy.
|
||||
fn normalization() -> NormalizationStrategy;
|
||||
|
||||
/// Enable some optimizations if we do not expect inference variables
|
||||
/// in the RHS of the relation.
|
||||
fn forbid_inference_vars() -> bool;
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
@ -242,15 +264,79 @@ fn push_outlives(&mut self, sup: ty::Region<'tcx>, sub: ty::Region<'tcx>) {
|
||||
self.delegate.push_outlives(sup, sub);
|
||||
}
|
||||
|
||||
/// When we encounter a canonical variable `var` in the output,
|
||||
/// equate it with `kind`. If the variable has been previously
|
||||
/// equated, then equate it again.
|
||||
fn relate_var(&mut self, var_ty: Ty<'tcx>, value_ty: Ty<'tcx>) -> RelateResult<'tcx, Ty<'tcx>> {
|
||||
debug!("equate_var(var_ty={:?}, value_ty={:?})", var_ty, value_ty);
|
||||
/// Relate a projection type and some value type lazily. This will always
|
||||
/// succeed, but we push an additional `ProjectionEq` goal depending
|
||||
/// on the value type:
|
||||
/// - if the value type is any type `T` which is not a projection, we push
|
||||
/// `ProjectionEq(projection = T)`.
|
||||
/// - if the value type is another projection `other_projection`, we create
|
||||
/// a new inference variable `?U` and push the two goals
|
||||
/// `ProjectionEq(projection = ?U)`, `ProjectionEq(other_projection = ?U)`.
|
||||
fn relate_projection_ty(
|
||||
&mut self,
|
||||
projection_ty: ty::ProjectionTy<'tcx>,
|
||||
value_ty: ty::Ty<'tcx>
|
||||
) -> Ty<'tcx> {
|
||||
use crate::infer::type_variable::TypeVariableOrigin;
|
||||
use crate::traits::WhereClause;
|
||||
use syntax_pos::DUMMY_SP;
|
||||
|
||||
let generalized_ty = self.generalize_value(value_ty);
|
||||
self.infcx
|
||||
.force_instantiate_unchecked(var_ty, generalized_ty);
|
||||
match value_ty.sty {
|
||||
ty::Projection(other_projection_ty) => {
|
||||
let var = self.infcx.next_ty_var(TypeVariableOrigin::MiscVariable(DUMMY_SP));
|
||||
self.relate_projection_ty(projection_ty, var);
|
||||
self.relate_projection_ty(other_projection_ty, var);
|
||||
var
|
||||
}
|
||||
|
||||
_ => {
|
||||
let projection = ty::ProjectionPredicate {
|
||||
projection_ty,
|
||||
ty: value_ty,
|
||||
};
|
||||
self.delegate.push_domain_goal(
|
||||
DomainGoal::Holds(WhereClause::ProjectionEq(projection))
|
||||
);
|
||||
value_ty
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// Relate a type inference variable with a value type.
|
||||
fn relate_ty_var(
|
||||
&mut self,
|
||||
vid: ty::TyVid,
|
||||
value_ty: Ty<'tcx>
|
||||
) -> RelateResult<'tcx, Ty<'tcx>> {
|
||||
debug!("relate_ty_var(vid={:?}, value_ty={:?})", vid, value_ty);
|
||||
|
||||
match value_ty.sty {
|
||||
ty::Infer(ty::TyVar(value_vid)) => {
|
||||
// Two type variables: just equate them.
|
||||
self.infcx.type_variables.borrow_mut().equate(vid, value_vid);
|
||||
return Ok(value_ty);
|
||||
}
|
||||
|
||||
ty::Projection(projection_ty)
|
||||
if D::normalization() == NormalizationStrategy::Lazy =>
|
||||
{
|
||||
return Ok(self.relate_projection_ty(projection_ty, self.infcx.tcx.mk_var(vid)));
|
||||
}
|
||||
|
||||
_ => (),
|
||||
}
|
||||
|
||||
let generalized_ty = self.generalize_value(value_ty, vid)?;
|
||||
debug!("relate_ty_var: generalized_ty = {:?}", generalized_ty);
|
||||
|
||||
if D::forbid_inference_vars() {
|
||||
// In NLL, we don't have type inference variables
|
||||
// floating around, so we can do this rather imprecise
|
||||
// variant of the occurs-check.
|
||||
assert!(!generalized_ty.has_infer_types());
|
||||
}
|
||||
|
||||
self.infcx.type_variables.borrow_mut().instantiate(vid, generalized_ty);
|
||||
|
||||
// The generalized values we extract from `canonical_var_values` have
|
||||
// been fully instantiated and hence the set of scopes we have
|
||||
@ -264,22 +350,27 @@ fn relate_var(&mut self, var_ty: Ty<'tcx>, value_ty: Ty<'tcx>) -> RelateResult<'
|
||||
// Restore the old scopes now.
|
||||
self.a_scopes = old_a_scopes;
|
||||
|
||||
debug!("equate_var: complete, result = {:?}", result);
|
||||
debug!("relate_ty_var: complete, result = {:?}", result);
|
||||
result
|
||||
}
|
||||
|
||||
fn generalize_value<T: Relate<'tcx>>(&mut self, value: T) -> T {
|
||||
TypeGeneralizer {
|
||||
tcx: self.infcx.tcx,
|
||||
fn generalize_value<T: Relate<'tcx>>(
|
||||
&mut self,
|
||||
value: T,
|
||||
for_vid: ty::TyVid
|
||||
) -> RelateResult<'tcx, T> {
|
||||
let universe = self.infcx.probe_ty_var(for_vid).unwrap_err();
|
||||
|
||||
let mut generalizer = TypeGeneralizer {
|
||||
infcx: self.infcx,
|
||||
delegate: &mut self.delegate,
|
||||
first_free_index: ty::INNERMOST,
|
||||
ambient_variance: self.ambient_variance,
|
||||
for_vid_sub_root: self.infcx.type_variables.borrow_mut().sub_root_var(for_vid),
|
||||
universe,
|
||||
};
|
||||
|
||||
// These always correspond to an `_` or `'_` written by
|
||||
// user, and those are always in the root universe.
|
||||
universe: ty::UniverseIndex::ROOT,
|
||||
}.relate(&value, &value)
|
||||
.unwrap()
|
||||
generalizer.relate(&value, &value)
|
||||
}
|
||||
}
|
||||
|
||||
@ -327,11 +418,35 @@ fn relate_with_variance<T: Relate<'tcx>>(
|
||||
Ok(r)
|
||||
}
|
||||
|
||||
fn tys(&mut self, a: Ty<'tcx>, b: Ty<'tcx>) -> RelateResult<'tcx, Ty<'tcx>> {
|
||||
fn tys(&mut self, a: Ty<'tcx>, mut b: Ty<'tcx>) -> RelateResult<'tcx, Ty<'tcx>> {
|
||||
let a = self.infcx.shallow_resolve(a);
|
||||
match a.sty {
|
||||
ty::Infer(ty::TyVar(_)) | ty::Infer(ty::IntVar(_)) | ty::Infer(ty::FloatVar(_)) => {
|
||||
self.relate_var(a.into(), b.into())
|
||||
|
||||
if !D::forbid_inference_vars() {
|
||||
b = self.infcx.shallow_resolve(b);
|
||||
}
|
||||
|
||||
match (&a.sty, &b.sty) {
|
||||
(_, &ty::Infer(ty::TyVar(vid))) => {
|
||||
if D::forbid_inference_vars() {
|
||||
// Forbid inference variables in the RHS.
|
||||
bug!("unexpected inference var {:?}", b)
|
||||
} else {
|
||||
self.relate_ty_var(vid, a)
|
||||
}
|
||||
}
|
||||
|
||||
(&ty::Infer(ty::TyVar(vid)), _) => self.relate_ty_var(vid, b),
|
||||
|
||||
(&ty::Projection(projection_ty), _)
|
||||
if D::normalization() == NormalizationStrategy::Lazy =>
|
||||
{
|
||||
Ok(self.relate_projection_ty(projection_ty, b))
|
||||
}
|
||||
|
||||
(_, &ty::Projection(projection_ty))
|
||||
if D::normalization() == NormalizationStrategy::Lazy =>
|
||||
{
|
||||
Ok(self.relate_projection_ty(projection_ty, a))
|
||||
}
|
||||
|
||||
_ => {
|
||||
@ -340,7 +455,8 @@ fn tys(&mut self, a: Ty<'tcx>, b: Ty<'tcx>) -> RelateResult<'tcx, Ty<'tcx>> {
|
||||
a, b, self.ambient_variance
|
||||
);
|
||||
|
||||
relate::super_relate_tys(self, a, b)
|
||||
// Will also handle unification of `IntVar` and `FloatVar`.
|
||||
self.infcx.super_combine_tys(self, a, b)
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -551,7 +667,7 @@ struct TypeGeneralizer<'me, 'gcx: 'tcx, 'tcx: 'me, D>
|
||||
where
|
||||
D: TypeRelatingDelegate<'tcx> + 'me,
|
||||
{
|
||||
tcx: TyCtxt<'me, 'gcx, 'tcx>,
|
||||
infcx: &'me InferCtxt<'me, 'gcx, 'tcx>,
|
||||
|
||||
delegate: &'me mut D,
|
||||
|
||||
@ -561,6 +677,14 @@ struct TypeGeneralizer<'me, 'gcx: 'tcx, 'tcx: 'me, D>
|
||||
|
||||
first_free_index: ty::DebruijnIndex,
|
||||
|
||||
/// The vid of the type variable that is in the process of being
|
||||
/// instantiated. If we find this within the value we are folding,
|
||||
/// that means we would have created a cyclic value.
|
||||
for_vid_sub_root: ty::TyVid,
|
||||
|
||||
/// The universe of the type variable that is in the process of being
|
||||
/// instantiated. If we find anything that this universe cannot name,
|
||||
/// we reject the relation.
|
||||
universe: ty::UniverseIndex,
|
||||
}
|
||||
|
||||
@ -569,7 +693,7 @@ impl<D> TypeRelation<'me, 'gcx, 'tcx> for TypeGeneralizer<'me, 'gcx, 'tcx, D>
|
||||
D: TypeRelatingDelegate<'tcx>,
|
||||
{
|
||||
fn tcx(&self) -> TyCtxt<'me, 'gcx, 'tcx> {
|
||||
self.tcx
|
||||
self.infcx.tcx
|
||||
}
|
||||
|
||||
fn tag(&self) -> &'static str {
|
||||
@ -609,17 +733,84 @@ fn relate_with_variance<T: Relate<'tcx>>(
|
||||
}
|
||||
|
||||
fn tys(&mut self, a: Ty<'tcx>, _: Ty<'tcx>) -> RelateResult<'tcx, Ty<'tcx>> {
|
||||
use crate::infer::type_variable::TypeVariableValue;
|
||||
|
||||
debug!("TypeGeneralizer::tys(a={:?})", a,);
|
||||
|
||||
match a.sty {
|
||||
ty::Infer(ty::TyVar(_)) | ty::Infer(ty::IntVar(_)) | ty::Infer(ty::FloatVar(_)) => {
|
||||
ty::Infer(ty::TyVar(_)) | ty::Infer(ty::IntVar(_)) | ty::Infer(ty::FloatVar(_))
|
||||
if D::forbid_inference_vars() =>
|
||||
{
|
||||
bug!(
|
||||
"unexpected inference variable encountered in NLL generalization: {:?}",
|
||||
a
|
||||
);
|
||||
}
|
||||
|
||||
_ => relate::super_relate_tys(self, a, a),
|
||||
ty::Infer(ty::TyVar(vid)) => {
|
||||
let mut variables = self.infcx.type_variables.borrow_mut();
|
||||
let vid = variables.root_var(vid);
|
||||
let sub_vid = variables.sub_root_var(vid);
|
||||
if sub_vid == self.for_vid_sub_root {
|
||||
// If sub-roots are equal, then `for_vid` and
|
||||
// `vid` are related via subtyping.
|
||||
debug!("TypeGeneralizer::tys: occurs check failed");
|
||||
return Err(TypeError::Mismatch);
|
||||
} else {
|
||||
match variables.probe(vid) {
|
||||
TypeVariableValue::Known { value: u } => {
|
||||
drop(variables);
|
||||
self.relate(&u, &u)
|
||||
}
|
||||
TypeVariableValue::Unknown { universe: _universe } => {
|
||||
if self.ambient_variance == ty::Bivariant {
|
||||
// FIXME: we may need a WF predicate (related to #54105).
|
||||
}
|
||||
|
||||
let origin = *variables.var_origin(vid);
|
||||
|
||||
// Replacing with a new variable in the universe `self.universe`,
|
||||
// it will be unified later with the original type variable in
|
||||
// the universe `_universe`.
|
||||
let new_var_id = variables.new_var(self.universe, false, origin);
|
||||
|
||||
let u = self.tcx().mk_var(new_var_id);
|
||||
debug!(
|
||||
"generalize: replacing original vid={:?} with new={:?}",
|
||||
vid,
|
||||
u
|
||||
);
|
||||
return Ok(u);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
ty::Infer(ty::IntVar(_)) |
|
||||
ty::Infer(ty::FloatVar(_)) => {
|
||||
// No matter what mode we are in,
|
||||
// integer/floating-point types must be equal to be
|
||||
// relatable.
|
||||
Ok(a)
|
||||
}
|
||||
|
||||
ty::Placeholder(placeholder) => {
|
||||
if self.universe.cannot_name(placeholder.universe) {
|
||||
debug!(
|
||||
"TypeGeneralizer::tys: root universe {:?} cannot name\
|
||||
placeholder in universe {:?}",
|
||||
self.universe,
|
||||
placeholder.universe
|
||||
);
|
||||
Err(TypeError::Mismatch)
|
||||
} else {
|
||||
Ok(a)
|
||||
}
|
||||
}
|
||||
|
||||
_ => {
|
||||
relate::super_relate_tys(self, a, a)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@ -673,64 +864,3 @@ fn binders<T>(
|
||||
Ok(ty::Binder::bind(result))
|
||||
}
|
||||
}
|
||||
|
||||
impl InferCtxt<'_, '_, 'tcx> {
|
||||
/// A hacky sort of method used by the NLL type-relating code:
|
||||
///
|
||||
/// - `var` must be some unbound type variable.
|
||||
/// - `value` must be a suitable type to use as its value.
|
||||
///
|
||||
/// `var` will then be equated with `value`. Note that this
|
||||
/// sidesteps a number of important checks, such as the "occurs
|
||||
/// check" that prevents cyclic types, so it is important not to
|
||||
/// use this method during regular type-check.
|
||||
fn force_instantiate_unchecked(&self, var: Ty<'tcx>, value: Ty<'tcx>) {
|
||||
match (&var.sty, &value.sty) {
|
||||
(&ty::Infer(ty::TyVar(vid)), _) => {
|
||||
let mut type_variables = self.type_variables.borrow_mut();
|
||||
|
||||
// In NLL, we don't have type inference variables
|
||||
// floating around, so we can do this rather imprecise
|
||||
// variant of the occurs-check.
|
||||
assert!(!value.has_infer_types());
|
||||
|
||||
type_variables.instantiate(vid, value);
|
||||
}
|
||||
|
||||
(&ty::Infer(ty::IntVar(vid)), &ty::Int(value)) => {
|
||||
let mut int_unification_table = self.int_unification_table.borrow_mut();
|
||||
int_unification_table
|
||||
.unify_var_value(vid, Some(ty::IntVarValue::IntType(value)))
|
||||
.unwrap_or_else(|_| {
|
||||
bug!("failed to unify int var `{:?}` with `{:?}`", vid, value);
|
||||
});
|
||||
}
|
||||
|
||||
(&ty::Infer(ty::IntVar(vid)), &ty::Uint(value)) => {
|
||||
let mut int_unification_table = self.int_unification_table.borrow_mut();
|
||||
int_unification_table
|
||||
.unify_var_value(vid, Some(ty::IntVarValue::UintType(value)))
|
||||
.unwrap_or_else(|_| {
|
||||
bug!("failed to unify int var `{:?}` with `{:?}`", vid, value);
|
||||
});
|
||||
}
|
||||
|
||||
(&ty::Infer(ty::FloatVar(vid)), &ty::Float(value)) => {
|
||||
let mut float_unification_table = self.float_unification_table.borrow_mut();
|
||||
float_unification_table
|
||||
.unify_var_value(vid, Some(ty::FloatVarValue(value)))
|
||||
.unwrap_or_else(|_| {
|
||||
bug!("failed to unify float var `{:?}` with `{:?}`", vid, value)
|
||||
});
|
||||
}
|
||||
|
||||
_ => {
|
||||
bug!(
|
||||
"force_instantiate_unchecked invoked with bad combination: var={:?} value={:?}",
|
||||
var,
|
||||
value,
|
||||
);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -680,24 +680,31 @@ pub fn anonymize_late_bound_regions<T>(self, sig: &Binder<T>) -> Binder<T>
|
||||
// vars. See comment on `shift_vars_through_binders` method in
|
||||
// `subst.rs` for more details.
|
||||
|
||||
#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
|
||||
enum Direction {
|
||||
In,
|
||||
Out,
|
||||
}
|
||||
|
||||
struct Shifter<'a, 'gcx: 'a+'tcx, 'tcx: 'a> {
|
||||
tcx: TyCtxt<'a, 'gcx, 'tcx>,
|
||||
|
||||
current_index: ty::DebruijnIndex,
|
||||
amount: u32,
|
||||
direction: Direction,
|
||||
}
|
||||
|
||||
impl Shifter<'a, 'gcx, 'tcx> {
|
||||
pub fn new(tcx: TyCtxt<'a, 'gcx, 'tcx>, amount: u32) -> Self {
|
||||
pub fn new(tcx: TyCtxt<'a, 'gcx, 'tcx>, amount: u32, direction: Direction) -> Self {
|
||||
Shifter {
|
||||
tcx,
|
||||
current_index: ty::INNERMOST,
|
||||
amount,
|
||||
direction,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<'a, 'gcx, 'tcx> TypeFolder<'gcx, 'tcx> for Shifter<'a, 'gcx, 'tcx> {
|
||||
impl TypeFolder<'gcx, 'tcx> for Shifter<'a, 'gcx, 'tcx> {
|
||||
fn tcx<'b>(&'b self) -> TyCtxt<'b, 'gcx, 'tcx> { self.tcx }
|
||||
|
||||
fn fold_binder<T: TypeFoldable<'tcx>>(&mut self, t: &ty::Binder<T>) -> ty::Binder<T> {
|
||||
@ -713,7 +720,14 @@ fn fold_region(&mut self, r: ty::Region<'tcx>) -> ty::Region<'tcx> {
|
||||
if self.amount == 0 || debruijn < self.current_index {
|
||||
r
|
||||
} else {
|
||||
let shifted = ty::ReLateBound(debruijn.shifted_in(self.amount), br);
|
||||
let debruijn = match self.direction {
|
||||
Direction::In => debruijn.shifted_in(self.amount),
|
||||
Direction::Out => {
|
||||
assert!(debruijn.as_u32() >= self.amount);
|
||||
debruijn.shifted_out(self.amount)
|
||||
}
|
||||
};
|
||||
let shifted = ty::ReLateBound(debruijn, br);
|
||||
self.tcx.mk_region(shifted)
|
||||
}
|
||||
}
|
||||
@ -727,8 +741,15 @@ fn fold_ty(&mut self, ty: ty::Ty<'tcx>) -> ty::Ty<'tcx> {
|
||||
if self.amount == 0 || debruijn < self.current_index {
|
||||
ty
|
||||
} else {
|
||||
let debruijn = match self.direction {
|
||||
Direction::In => debruijn.shifted_in(self.amount),
|
||||
Direction::Out => {
|
||||
assert!(debruijn.as_u32() >= self.amount);
|
||||
debruijn.shifted_out(self.amount)
|
||||
}
|
||||
};
|
||||
self.tcx.mk_ty(
|
||||
ty::Bound(debruijn.shifted_in(self.amount), bound_ty)
|
||||
ty::Bound(debruijn, bound_ty)
|
||||
)
|
||||
}
|
||||
}
|
||||
@ -761,7 +782,18 @@ pub fn shift_vars<'a, 'gcx, 'tcx, T>(
|
||||
debug!("shift_vars(value={:?}, amount={})",
|
||||
value, amount);
|
||||
|
||||
value.fold_with(&mut Shifter::new(tcx, amount))
|
||||
value.fold_with(&mut Shifter::new(tcx, amount, Direction::In))
|
||||
}
|
||||
|
||||
pub fn shift_out_vars<'a, 'gcx, 'tcx, T>(
|
||||
tcx: TyCtxt<'a, 'gcx, 'tcx>,
|
||||
value: &T,
|
||||
amount: u32
|
||||
) -> T where T: TypeFoldable<'tcx> {
|
||||
debug!("shift_out_vars(value={:?}, amount={})",
|
||||
value, amount);
|
||||
|
||||
value.fold_with(&mut Shifter::new(tcx, amount, Direction::Out))
|
||||
}
|
||||
|
||||
/// An "escaping var" is a bound var whose binder is not part of `t`. A bound var can be a
|
||||
|
@ -25,6 +25,7 @@
|
||||
use std::iter;
|
||||
use rustc_target::spec::abi;
|
||||
use hir as ast;
|
||||
use traits;
|
||||
|
||||
pub type RelateResult<'tcx, T> = Result<T, TypeError<'tcx>>;
|
||||
|
||||
@ -371,6 +372,10 @@ pub fn super_relate_tys<'a, 'gcx, 'tcx, R>(relation: &mut R,
|
||||
bug!("var types encountered in super_relate_tys")
|
||||
}
|
||||
|
||||
(ty::Bound(..), _) | (_, ty::Bound(..)) => {
|
||||
bug!("bound types encountered in super_relate_tys")
|
||||
}
|
||||
|
||||
(&ty::Error, _) | (_, &ty::Error) =>
|
||||
{
|
||||
Ok(tcx.types.err)
|
||||
@ -394,6 +399,10 @@ pub fn super_relate_tys<'a, 'gcx, 'tcx, R>(relation: &mut R,
|
||||
Ok(a)
|
||||
}
|
||||
|
||||
(ty::Placeholder(p1), ty::Placeholder(p2)) if p1 == p2 => {
|
||||
Ok(a)
|
||||
}
|
||||
|
||||
(&ty::Adt(a_def, a_substs), &ty::Adt(b_def, b_substs))
|
||||
if a_def == b_def =>
|
||||
{
|
||||
@ -556,8 +565,13 @@ pub fn super_relate_tys<'a, 'gcx, 'tcx, R>(relation: &mut R,
|
||||
Ok(tcx.mk_fn_ptr(fty))
|
||||
}
|
||||
|
||||
(&ty::Projection(ref a_data), &ty::Projection(ref b_data)) =>
|
||||
{
|
||||
(ty::UnnormalizedProjection(a_data), ty::UnnormalizedProjection(b_data)) => {
|
||||
let projection_ty = relation.relate(a_data, b_data)?;
|
||||
Ok(tcx.mk_ty(ty::UnnormalizedProjection(projection_ty)))
|
||||
}
|
||||
|
||||
// these two are already handled downstream in case of lazy normalization
|
||||
(ty::Projection(a_data), ty::Projection(b_data)) => {
|
||||
let projection_ty = relation.relate(a_data, b_data)?;
|
||||
Ok(tcx.mk_projection(projection_ty.item_def_id, projection_ty.substs))
|
||||
}
|
||||
@ -710,6 +724,283 @@ fn relate<'a, 'gcx, R>(
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> Relate<'tcx> for ty::TraitPredicate<'tcx> {
|
||||
fn relate<'a, 'gcx, R>(
|
||||
relation: &mut R,
|
||||
a: &ty::TraitPredicate<'tcx>,
|
||||
b: &ty::TraitPredicate<'tcx>
|
||||
) -> RelateResult<'tcx, ty::TraitPredicate<'tcx>>
|
||||
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
|
||||
{
|
||||
Ok(ty::TraitPredicate {
|
||||
trait_ref: relation.relate(&a.trait_ref, &b.trait_ref)?,
|
||||
})
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> Relate<'tcx> for ty::ProjectionPredicate<'tcx> {
|
||||
fn relate<'a, 'gcx, R>(
|
||||
relation: &mut R,
|
||||
a: &ty::ProjectionPredicate<'tcx>,
|
||||
b: &ty::ProjectionPredicate<'tcx>,
|
||||
) -> RelateResult<'tcx, ty::ProjectionPredicate<'tcx>>
|
||||
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
|
||||
{
|
||||
Ok(ty::ProjectionPredicate {
|
||||
projection_ty: relation.relate(&a.projection_ty, &b.projection_ty)?,
|
||||
ty: relation.relate(&a.ty, &b.ty)?,
|
||||
})
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> Relate<'tcx> for traits::WhereClause<'tcx> {
|
||||
fn relate<'a, 'gcx, R>(
|
||||
relation: &mut R,
|
||||
a: &traits::WhereClause<'tcx>,
|
||||
b: &traits::WhereClause<'tcx>
|
||||
) -> RelateResult<'tcx, traits::WhereClause<'tcx>>
|
||||
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
|
||||
{
|
||||
use traits::WhereClause::*;
|
||||
match (a, b) {
|
||||
(Implemented(a_pred), Implemented(b_pred)) => {
|
||||
Ok(Implemented(relation.relate(a_pred, b_pred)?))
|
||||
}
|
||||
|
||||
(ProjectionEq(a_pred), ProjectionEq(b_pred)) => {
|
||||
Ok(ProjectionEq(relation.relate(a_pred, b_pred)?))
|
||||
}
|
||||
|
||||
(RegionOutlives(a_pred), RegionOutlives(b_pred)) => {
|
||||
Ok(RegionOutlives(ty::OutlivesPredicate(
|
||||
relation.relate(&a_pred.0, &b_pred.0)?,
|
||||
relation.relate(&a_pred.1, &b_pred.1)?,
|
||||
)))
|
||||
}
|
||||
|
||||
(TypeOutlives(a_pred), TypeOutlives(b_pred)) => {
|
||||
Ok(TypeOutlives(ty::OutlivesPredicate(
|
||||
relation.relate(&a_pred.0, &b_pred.0)?,
|
||||
relation.relate(&a_pred.1, &b_pred.1)?,
|
||||
)))
|
||||
}
|
||||
|
||||
_ => Err(TypeError::Mismatch),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> Relate<'tcx> for traits::WellFormed<'tcx> {
|
||||
fn relate<'a, 'gcx, R>(
|
||||
relation: &mut R,
|
||||
a: &traits::WellFormed<'tcx>,
|
||||
b: &traits::WellFormed<'tcx>
|
||||
) -> RelateResult<'tcx, traits::WellFormed<'tcx>>
|
||||
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
|
||||
{
|
||||
use traits::WellFormed::*;
|
||||
match (a, b) {
|
||||
(Trait(a_pred), Trait(b_pred)) => Ok(Trait(relation.relate(a_pred, b_pred)?)),
|
||||
(Ty(a_ty), Ty(b_ty)) => Ok(Ty(relation.relate(a_ty, b_ty)?)),
|
||||
_ => Err(TypeError::Mismatch),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> Relate<'tcx> for traits::FromEnv<'tcx> {
|
||||
fn relate<'a, 'gcx, R>(
|
||||
relation: &mut R,
|
||||
a: &traits::FromEnv<'tcx>,
|
||||
b: &traits::FromEnv<'tcx>
|
||||
) -> RelateResult<'tcx, traits::FromEnv<'tcx>>
|
||||
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
|
||||
{
|
||||
use traits::FromEnv::*;
|
||||
match (a, b) {
|
||||
(Trait(a_pred), Trait(b_pred)) => Ok(Trait(relation.relate(a_pred, b_pred)?)),
|
||||
(Ty(a_ty), Ty(b_ty)) => Ok(Ty(relation.relate(a_ty, b_ty)?)),
|
||||
_ => Err(TypeError::Mismatch),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> Relate<'tcx> for traits::DomainGoal<'tcx> {
|
||||
fn relate<'a, 'gcx, R>(
|
||||
relation: &mut R,
|
||||
a: &traits::DomainGoal<'tcx>,
|
||||
b: &traits::DomainGoal<'tcx>
|
||||
) -> RelateResult<'tcx, traits::DomainGoal<'tcx>>
|
||||
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
|
||||
{
|
||||
use traits::DomainGoal::*;
|
||||
match (a, b) {
|
||||
(Holds(a_wc), Holds(b_wc)) => Ok(Holds(relation.relate(a_wc, b_wc)?)),
|
||||
(WellFormed(a_wf), WellFormed(b_wf)) => Ok(WellFormed(relation.relate(a_wf, b_wf)?)),
|
||||
(FromEnv(a_fe), FromEnv(b_fe)) => Ok(FromEnv(relation.relate(a_fe, b_fe)?)),
|
||||
|
||||
(Normalize(a_pred), Normalize(b_pred)) => {
|
||||
Ok(Normalize(relation.relate(a_pred, b_pred)?))
|
||||
}
|
||||
|
||||
_ => Err(TypeError::Mismatch),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> Relate<'tcx> for traits::Goal<'tcx> {
|
||||
fn relate<'a, 'gcx, R>(
|
||||
relation: &mut R,
|
||||
a: &traits::Goal<'tcx>,
|
||||
b: &traits::Goal<'tcx>
|
||||
) -> RelateResult<'tcx, traits::Goal<'tcx>>
|
||||
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
|
||||
{
|
||||
use traits::GoalKind::*;
|
||||
match (a, b) {
|
||||
(Implies(a_clauses, a_goal), Implies(b_clauses, b_goal)) => {
|
||||
let clauses = relation.relate(a_clauses, b_clauses)?;
|
||||
let goal = relation.relate(a_goal, b_goal)?;
|
||||
Ok(relation.tcx().mk_goal(Implies(clauses, goal)))
|
||||
}
|
||||
|
||||
(And(a_left, a_right), And(b_left, b_right)) => {
|
||||
let left = relation.relate(a_left, b_left)?;
|
||||
let right = relation.relate(a_right, b_right)?;
|
||||
Ok(relation.tcx().mk_goal(And(left, right)))
|
||||
}
|
||||
|
||||
(Not(a_goal), Not(b_goal)) => {
|
||||
let goal = relation.relate(a_goal, b_goal)?;
|
||||
Ok(relation.tcx().mk_goal(Not(goal)))
|
||||
}
|
||||
|
||||
(DomainGoal(a_goal), DomainGoal(b_goal)) => {
|
||||
let goal = relation.relate(a_goal, b_goal)?;
|
||||
Ok(relation.tcx().mk_goal(DomainGoal(goal)))
|
||||
}
|
||||
|
||||
(Quantified(a_qkind, a_goal), Quantified(b_qkind, b_goal))
|
||||
if a_qkind == b_qkind =>
|
||||
{
|
||||
let goal = relation.relate(a_goal, b_goal)?;
|
||||
Ok(relation.tcx().mk_goal(Quantified(*a_qkind, goal)))
|
||||
}
|
||||
|
||||
(CannotProve, CannotProve) => Ok(*a),
|
||||
|
||||
_ => Err(TypeError::Mismatch),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> Relate<'tcx> for traits::Goals<'tcx> {
|
||||
fn relate<'a, 'gcx, R>(
|
||||
relation: &mut R,
|
||||
a: &traits::Goals<'tcx>,
|
||||
b: &traits::Goals<'tcx>
|
||||
) -> RelateResult<'tcx, traits::Goals<'tcx>>
|
||||
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
|
||||
{
|
||||
if a.len() != b.len() {
|
||||
return Err(TypeError::Mismatch);
|
||||
}
|
||||
|
||||
let tcx = relation.tcx();
|
||||
let goals = a.iter().zip(b.iter()).map(|(a, b)| relation.relate(a, b));
|
||||
Ok(tcx.mk_goals(goals)?)
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> Relate<'tcx> for traits::Clause<'tcx> {
|
||||
fn relate<'a, 'gcx, R>(
|
||||
relation: &mut R,
|
||||
a: &traits::Clause<'tcx>,
|
||||
b: &traits::Clause<'tcx>
|
||||
) -> RelateResult<'tcx, traits::Clause<'tcx>>
|
||||
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
|
||||
{
|
||||
use traits::Clause::*;
|
||||
match (a, b) {
|
||||
(Implies(a_clause), Implies(b_clause)) => {
|
||||
let clause = relation.relate(a_clause, b_clause)?;
|
||||
Ok(Implies(clause))
|
||||
}
|
||||
|
||||
(ForAll(a_clause), ForAll(b_clause)) => {
|
||||
let clause = relation.relate(a_clause, b_clause)?;
|
||||
Ok(ForAll(clause))
|
||||
}
|
||||
|
||||
_ => Err(TypeError::Mismatch),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> Relate<'tcx> for traits::Clauses<'tcx> {
|
||||
fn relate<'a, 'gcx, R>(
|
||||
relation: &mut R,
|
||||
a: &traits::Clauses<'tcx>,
|
||||
b: &traits::Clauses<'tcx>
|
||||
) -> RelateResult<'tcx, traits::Clauses<'tcx>>
|
||||
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
|
||||
{
|
||||
if a.len() != b.len() {
|
||||
return Err(TypeError::Mismatch);
|
||||
}
|
||||
|
||||
let tcx = relation.tcx();
|
||||
let clauses = a.iter().zip(b.iter()).map(|(a, b)| relation.relate(a, b));
|
||||
Ok(tcx.mk_clauses(clauses)?)
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> Relate<'tcx> for traits::ProgramClause<'tcx> {
|
||||
fn relate<'a, 'gcx, R>(
|
||||
relation: &mut R,
|
||||
a: &traits::ProgramClause<'tcx>,
|
||||
b: &traits::ProgramClause<'tcx>
|
||||
) -> RelateResult<'tcx, traits::ProgramClause<'tcx>>
|
||||
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
|
||||
{
|
||||
Ok(traits::ProgramClause {
|
||||
goal: relation.relate(&a.goal, &b.goal)?,
|
||||
hypotheses: relation.relate(&a.hypotheses, &b.hypotheses)?,
|
||||
category: traits::ProgramClauseCategory::Other,
|
||||
})
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> Relate<'tcx> for traits::Environment<'tcx> {
|
||||
fn relate<'a, 'gcx, R>(
|
||||
relation: &mut R,
|
||||
a: &traits::Environment<'tcx>,
|
||||
b: &traits::Environment<'tcx>
|
||||
) -> RelateResult<'tcx, traits::Environment<'tcx>>
|
||||
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
|
||||
{
|
||||
Ok(traits::Environment {
|
||||
clauses: relation.relate(&a.clauses, &b.clauses)?,
|
||||
})
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx, G> Relate<'tcx> for traits::InEnvironment<'tcx, G>
|
||||
where G: Relate<'tcx>
|
||||
{
|
||||
fn relate<'a, 'gcx, R>(
|
||||
relation: &mut R,
|
||||
a: &traits::InEnvironment<'tcx, G>,
|
||||
b: &traits::InEnvironment<'tcx, G>
|
||||
) -> RelateResult<'tcx, traits::InEnvironment<'tcx, G>>
|
||||
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
|
||||
{
|
||||
Ok(traits::InEnvironment {
|
||||
environment: relation.relate(&a.environment, &b.environment)?,
|
||||
goal: relation.relate(&a.goal, &b.goal)?,
|
||||
})
|
||||
}
|
||||
}
|
||||
|
||||
///////////////////////////////////////////////////////////////////////////
|
||||
// Error handling
|
||||
|
||||
|
@ -10,10 +10,11 @@
|
||||
|
||||
use borrow_check::nll::constraints::OutlivesConstraint;
|
||||
use borrow_check::nll::type_check::{BorrowCheckContext, Locations};
|
||||
use rustc::infer::nll_relate::{TypeRelating, TypeRelatingDelegate};
|
||||
use rustc::infer::nll_relate::{TypeRelating, TypeRelatingDelegate, NormalizationStrategy};
|
||||
use rustc::infer::{InferCtxt, NLLRegionVariableOrigin};
|
||||
use rustc::mir::ConstraintCategory;
|
||||
use rustc::traits::query::Fallible;
|
||||
use rustc::traits::DomainGoal;
|
||||
use rustc::ty::relate::TypeRelation;
|
||||
use rustc::ty::{self, Ty};
|
||||
|
||||
@ -38,7 +39,7 @@ pub(super) fn relate_types<'tcx>(
|
||||
TypeRelating::new(
|
||||
infcx,
|
||||
NllTypeRelatingDelegate::new(infcx, borrowck_context, locations, category),
|
||||
v,
|
||||
v
|
||||
).relate(&a, &b)?;
|
||||
Ok(())
|
||||
}
|
||||
@ -115,4 +116,16 @@ fn push_outlives(&mut self, sup: ty::Region<'tcx>, sub: ty::Region<'tcx>) {
|
||||
});
|
||||
}
|
||||
}
|
||||
|
||||
fn push_domain_goal(&mut self, _: DomainGoal<'tcx>) {
|
||||
bug!("should never be invoked with eager normalization")
|
||||
}
|
||||
|
||||
fn normalization() -> NormalizationStrategy {
|
||||
NormalizationStrategy::Eager
|
||||
}
|
||||
|
||||
fn forbid_inference_vars() -> bool {
|
||||
true
|
||||
}
|
||||
}
|
||||
|
@ -9,13 +9,25 @@
|
||||
// except according to those terms.
|
||||
|
||||
mod program_clauses;
|
||||
mod resolvent_ops;
|
||||
mod unify;
|
||||
|
||||
use chalk_engine::fallible::Fallible as ChalkEngineFallible;
|
||||
use chalk_engine::{context, hh::HhGoal, DelayedLiteral, Literal, ExClause};
|
||||
use rustc::infer::canonical::{
|
||||
Canonical, CanonicalVarValues, OriginalQueryValues, QueryRegionConstraint, QueryResponse,
|
||||
use chalk_engine::fallible::{Fallible, NoSolution};
|
||||
use chalk_engine::{
|
||||
context,
|
||||
hh::HhGoal,
|
||||
DelayedLiteral,
|
||||
Literal,
|
||||
ExClause
|
||||
};
|
||||
use rustc::infer::{InferCtxt, LateBoundRegionConversionTime};
|
||||
use rustc::infer::canonical::{
|
||||
Canonical,
|
||||
CanonicalVarValues,
|
||||
OriginalQueryValues,
|
||||
QueryResponse,
|
||||
Certainty,
|
||||
};
|
||||
use rustc::infer::{InferCtxt, InferOk, LateBoundRegionConversionTime};
|
||||
use rustc::traits::{
|
||||
DomainGoal,
|
||||
ExClauseFold,
|
||||
@ -27,14 +39,15 @@
|
||||
Environment,
|
||||
InEnvironment,
|
||||
};
|
||||
use rustc::ty::{self, TyCtxt};
|
||||
use rustc::ty::fold::{TypeFoldable, TypeFolder, TypeVisitor};
|
||||
use rustc::ty::subst::{Kind, UnpackedKind};
|
||||
use rustc::ty::{self, TyCtxt};
|
||||
use syntax_pos::DUMMY_SP;
|
||||
|
||||
use std::fmt::{self, Debug};
|
||||
use std::marker::PhantomData;
|
||||
|
||||
use syntax_pos::DUMMY_SP;
|
||||
use self::unify::*;
|
||||
|
||||
#[derive(Copy, Clone, Debug)]
|
||||
crate struct ChalkArenas<'gcx> {
|
||||
@ -55,10 +68,12 @@
|
||||
#[derive(Copy, Clone, Debug)]
|
||||
crate struct UniverseMap;
|
||||
|
||||
crate type RegionConstraint<'tcx> = ty::OutlivesPredicate<Kind<'tcx>, ty::Region<'tcx>>;
|
||||
|
||||
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
|
||||
crate struct ConstrainedSubst<'tcx> {
|
||||
subst: CanonicalVarValues<'tcx>,
|
||||
constraints: Vec<QueryRegionConstraint<'tcx>>,
|
||||
constraints: Vec<RegionConstraint<'tcx>>,
|
||||
}
|
||||
|
||||
BraceStructTypeFoldableImpl! {
|
||||
@ -86,7 +101,7 @@ impl context::Context for ChalkArenas<'tcx> {
|
||||
|
||||
type GoalInEnvironment = InEnvironment<'tcx, Goal<'tcx>>;
|
||||
|
||||
type RegionConstraint = QueryRegionConstraint<'tcx>;
|
||||
type RegionConstraint = RegionConstraint<'tcx>;
|
||||
|
||||
type Substitution = CanonicalVarValues<'tcx>;
|
||||
|
||||
@ -104,7 +119,7 @@ impl context::Context for ChalkArenas<'tcx> {
|
||||
|
||||
type ProgramClauses = Vec<Clause<'tcx>>;
|
||||
|
||||
type UnificationResult = InferOk<'tcx, ()>;
|
||||
type UnificationResult = UnificationResult<'tcx>;
|
||||
|
||||
fn goal_in_environment(
|
||||
env: &Environment<'tcx>,
|
||||
@ -118,9 +133,34 @@ impl context::AggregateOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
|
||||
fn make_solution(
|
||||
&self,
|
||||
_root_goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
|
||||
_simplified_answers: impl context::AnswerStream<ChalkArenas<'gcx>>,
|
||||
mut simplified_answers: impl context::AnswerStream<ChalkArenas<'gcx>>,
|
||||
) -> Option<Canonical<'gcx, QueryResponse<'gcx, ()>>> {
|
||||
unimplemented!()
|
||||
use chalk_engine::SimplifiedAnswer;
|
||||
|
||||
if simplified_answers.peek_answer().is_none() {
|
||||
return None;
|
||||
}
|
||||
|
||||
let SimplifiedAnswer { subst, ambiguous } = simplified_answers
|
||||
.next_answer()
|
||||
.unwrap();
|
||||
|
||||
let ambiguous = simplified_answers.peek_answer().is_some() || ambiguous;
|
||||
|
||||
Some(subst.unchecked_map(|subst| {
|
||||
QueryResponse {
|
||||
var_values: subst.subst,
|
||||
region_constraints: subst.constraints
|
||||
.into_iter()
|
||||
.map(|c| ty::Binder::bind(c))
|
||||
.collect(),
|
||||
certainty: match ambiguous {
|
||||
true => Certainty::Ambiguous,
|
||||
false => Certainty::Proven,
|
||||
},
|
||||
value: (),
|
||||
}
|
||||
}))
|
||||
}
|
||||
}
|
||||
|
||||
@ -197,7 +237,7 @@ fn canonical(
|
||||
|
||||
fn is_trivial_substitution(
|
||||
u_canon: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
|
||||
canonical_subst: &Canonical<'tcx, ConstrainedSubst<'tcx>>,
|
||||
canonical_subst: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
|
||||
) -> bool {
|
||||
let subst = &canonical_subst.value.subst;
|
||||
assert_eq!(u_canon.variables.len(), subst.var_values.len());
|
||||
@ -282,30 +322,6 @@ fn add_clauses(
|
||||
}
|
||||
}
|
||||
|
||||
impl context::ResolventOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
|
||||
for ChalkInferenceContext<'cx, 'gcx, 'tcx>
|
||||
{
|
||||
fn resolvent_clause(
|
||||
&mut self,
|
||||
_environment: &Environment<'tcx>,
|
||||
_goal: &DomainGoal<'tcx>,
|
||||
_subst: &CanonicalVarValues<'tcx>,
|
||||
_clause: &Clause<'tcx>,
|
||||
) -> chalk_engine::fallible::Fallible<Canonical<'gcx, ChalkExClause<'gcx>>> {
|
||||
panic!()
|
||||
}
|
||||
|
||||
fn apply_answer_subst(
|
||||
&mut self,
|
||||
_ex_clause: ChalkExClause<'tcx>,
|
||||
_selected_goal: &InEnvironment<'tcx, Goal<'tcx>>,
|
||||
_answer_table_goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
|
||||
_canonical_answer_subst: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
|
||||
) -> chalk_engine::fallible::Fallible<ChalkExClause<'tcx>> {
|
||||
panic!()
|
||||
}
|
||||
}
|
||||
|
||||
impl context::TruncateOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
|
||||
for ChalkInferenceContext<'cx, 'gcx, 'tcx>
|
||||
{
|
||||
@ -376,7 +392,7 @@ fn canonicalize_ex_clause(
|
||||
fn canonicalize_constrained_subst(
|
||||
&mut self,
|
||||
subst: CanonicalVarValues<'tcx>,
|
||||
constraints: Vec<QueryRegionConstraint<'tcx>>,
|
||||
constraints: Vec<RegionConstraint<'tcx>>,
|
||||
) -> Canonical<'gcx, ConstrainedSubst<'gcx>> {
|
||||
self.infcx.canonicalize_response(&ConstrainedSubst { subst, constraints })
|
||||
}
|
||||
@ -400,11 +416,13 @@ fn invert_goal(
|
||||
|
||||
fn unify_parameters(
|
||||
&mut self,
|
||||
_environment: &Environment<'tcx>,
|
||||
_a: &Kind<'tcx>,
|
||||
_b: &Kind<'tcx>,
|
||||
) -> ChalkEngineFallible<InferOk<'tcx, ()>> {
|
||||
panic!()
|
||||
environment: &Environment<'tcx>,
|
||||
a: &Kind<'tcx>,
|
||||
b: &Kind<'tcx>,
|
||||
) -> Fallible<UnificationResult<'tcx>> {
|
||||
self.infcx.commit_if_ok(|_| {
|
||||
unify(self.infcx, *environment, a, b).map_err(|_| NoSolution)
|
||||
})
|
||||
}
|
||||
|
||||
fn sink_answer_subset(
|
||||
@ -421,11 +439,22 @@ fn lift_delayed_literal(
|
||||
panic!("lift")
|
||||
}
|
||||
|
||||
fn into_ex_clause(&mut self, _result: InferOk<'tcx, ()>, _ex_clause: &mut ChalkExClause<'tcx>) {
|
||||
panic!("TBD")
|
||||
fn into_ex_clause(
|
||||
&mut self,
|
||||
result: UnificationResult<'tcx>,
|
||||
ex_clause: &mut ChalkExClause<'tcx>
|
||||
) {
|
||||
into_ex_clause(result, ex_clause);
|
||||
}
|
||||
}
|
||||
|
||||
crate fn into_ex_clause(result: UnificationResult<'tcx>, ex_clause: &mut ChalkExClause<'tcx>) {
|
||||
ex_clause.subgoals.extend(
|
||||
result.goals.into_iter().map(Literal::Positive)
|
||||
);
|
||||
ex_clause.constraints.extend(result.constraints);
|
||||
}
|
||||
|
||||
type ChalkHhGoal<'tcx> = HhGoal<ChalkArenas<'tcx>>;
|
||||
|
||||
type ChalkExClause<'tcx> = ExClause<ChalkArenas<'tcx>>;
|
||||
|
241
src/librustc_traits/chalk_context/resolvent_ops.rs
Normal file
241
src/librustc_traits/chalk_context/resolvent_ops.rs
Normal file
@ -0,0 +1,241 @@
|
||||
use chalk_engine::fallible::{Fallible, NoSolution};
|
||||
use chalk_engine::{
|
||||
context,
|
||||
Literal,
|
||||
ExClause
|
||||
};
|
||||
use rustc::infer::{InferCtxt, LateBoundRegionConversionTime};
|
||||
use rustc::infer::canonical::{Canonical, CanonicalVarValues};
|
||||
use rustc::traits::{
|
||||
DomainGoal,
|
||||
Goal,
|
||||
GoalKind,
|
||||
Clause,
|
||||
ProgramClause,
|
||||
Environment,
|
||||
InEnvironment,
|
||||
};
|
||||
use rustc::ty::{self, Ty};
|
||||
use rustc::ty::subst::Kind;
|
||||
use rustc::ty::relate::{Relate, RelateResult, TypeRelation};
|
||||
use syntax_pos::DUMMY_SP;
|
||||
|
||||
use super::{ChalkInferenceContext, ChalkArenas, ChalkExClause, ConstrainedSubst};
|
||||
use super::unify::*;
|
||||
|
||||
impl context::ResolventOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
|
||||
for ChalkInferenceContext<'cx, 'gcx, 'tcx>
|
||||
{
|
||||
fn resolvent_clause(
|
||||
&mut self,
|
||||
environment: &Environment<'tcx>,
|
||||
goal: &DomainGoal<'tcx>,
|
||||
subst: &CanonicalVarValues<'tcx>,
|
||||
clause: &Clause<'tcx>,
|
||||
) -> Fallible<Canonical<'gcx, ChalkExClause<'gcx>>> {
|
||||
use chalk_engine::context::UnificationOps;
|
||||
|
||||
self.infcx.probe(|_| {
|
||||
let ProgramClause {
|
||||
goal: consequence,
|
||||
hypotheses,
|
||||
..
|
||||
} = match clause {
|
||||
Clause::Implies(program_clause) => *program_clause,
|
||||
Clause::ForAll(program_clause) => self.infcx.replace_bound_vars_with_fresh_vars(
|
||||
DUMMY_SP,
|
||||
LateBoundRegionConversionTime::HigherRankedType,
|
||||
program_clause
|
||||
).0,
|
||||
};
|
||||
|
||||
let result = unify(self.infcx, *environment, goal, &consequence)
|
||||
.map_err(|_| NoSolution)?;
|
||||
|
||||
let mut ex_clause = ExClause {
|
||||
subst: subst.clone(),
|
||||
delayed_literals: vec![],
|
||||
constraints: vec![],
|
||||
subgoals: vec![],
|
||||
};
|
||||
|
||||
self.into_ex_clause(result, &mut ex_clause);
|
||||
|
||||
ex_clause.subgoals.extend(
|
||||
hypotheses.iter().map(|g| match g {
|
||||
GoalKind::Not(g) => Literal::Negative(environment.with(*g)),
|
||||
g => Literal::Positive(environment.with(*g)),
|
||||
})
|
||||
);
|
||||
|
||||
let canonical_ex_clause = self.canonicalize_ex_clause(&ex_clause);
|
||||
Ok(canonical_ex_clause)
|
||||
})
|
||||
}
|
||||
|
||||
fn apply_answer_subst(
|
||||
&mut self,
|
||||
ex_clause: ChalkExClause<'tcx>,
|
||||
selected_goal: &InEnvironment<'tcx, Goal<'tcx>>,
|
||||
answer_table_goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
|
||||
canonical_answer_subst: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
|
||||
) -> Fallible<ChalkExClause<'tcx>> {
|
||||
let (answer_subst, _) = self.infcx.instantiate_canonical_with_fresh_inference_vars(
|
||||
DUMMY_SP,
|
||||
canonical_answer_subst
|
||||
);
|
||||
|
||||
let mut substitutor = AnswerSubstitutor {
|
||||
infcx: self.infcx,
|
||||
environment: selected_goal.environment,
|
||||
answer_subst: answer_subst.subst,
|
||||
binder_index: ty::INNERMOST,
|
||||
ex_clause,
|
||||
};
|
||||
|
||||
substitutor.relate(&answer_table_goal.value, &selected_goal)
|
||||
.map_err(|_| NoSolution)?;
|
||||
|
||||
let mut ex_clause = substitutor.ex_clause;
|
||||
ex_clause.constraints.extend(answer_subst.constraints);
|
||||
Ok(ex_clause)
|
||||
}
|
||||
}
|
||||
|
||||
struct AnswerSubstitutor<'cx, 'gcx: 'tcx, 'tcx: 'cx> {
|
||||
infcx: &'cx InferCtxt<'cx, 'gcx, 'tcx>,
|
||||
environment: Environment<'tcx>,
|
||||
answer_subst: CanonicalVarValues<'tcx>,
|
||||
binder_index: ty::DebruijnIndex,
|
||||
ex_clause: ChalkExClause<'tcx>,
|
||||
}
|
||||
|
||||
impl AnswerSubstitutor<'cx, 'gcx, 'tcx> {
|
||||
fn unify_free_answer_var(
|
||||
&mut self,
|
||||
answer_var: ty::BoundVar,
|
||||
pending: Kind<'tcx>
|
||||
) -> RelateResult<'tcx, ()> {
|
||||
let answer_param = &self.answer_subst.var_values[answer_var];
|
||||
let pending = &ty::fold::shift_out_vars(
|
||||
self.infcx.tcx,
|
||||
&pending,
|
||||
self.binder_index.as_u32()
|
||||
);
|
||||
|
||||
super::into_ex_clause(
|
||||
unify(self.infcx, self.environment, answer_param, pending)?,
|
||||
&mut self.ex_clause
|
||||
);
|
||||
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
impl TypeRelation<'cx, 'gcx, 'tcx> for AnswerSubstitutor<'cx, 'gcx, 'tcx> {
|
||||
fn tcx(&self) -> ty::TyCtxt<'cx, 'gcx, 'tcx> {
|
||||
self.infcx.tcx
|
||||
}
|
||||
|
||||
fn tag(&self) -> &'static str {
|
||||
"chalk_context::answer_substitutor"
|
||||
}
|
||||
|
||||
fn a_is_expected(&self) -> bool {
|
||||
true
|
||||
}
|
||||
|
||||
fn relate_with_variance<T: Relate<'tcx>>(
|
||||
&mut self,
|
||||
_variance: ty::Variance,
|
||||
a: &T,
|
||||
b: &T,
|
||||
) -> RelateResult<'tcx, T> {
|
||||
// We don't care about variance.
|
||||
self.relate(a, b)
|
||||
}
|
||||
|
||||
fn binders<T: Relate<'tcx>>(
|
||||
&mut self,
|
||||
a: &ty::Binder<T>,
|
||||
b: &ty::Binder<T>,
|
||||
) -> RelateResult<'tcx, ty::Binder<T>> {
|
||||
self.binder_index.shift_in(1);
|
||||
let result = self.relate(a.skip_binder(), b.skip_binder())?;
|
||||
self.binder_index.shift_out(1);
|
||||
Ok(ty::Binder::bind(result))
|
||||
}
|
||||
|
||||
fn tys(&mut self, a: Ty<'tcx>, b: Ty<'tcx>) -> RelateResult<'tcx, Ty<'tcx>> {
|
||||
let b = self.infcx.shallow_resolve(b);
|
||||
|
||||
if let &ty::Bound(debruijn, bound_ty) = &a.sty {
|
||||
// Free bound var
|
||||
if debruijn == self.binder_index {
|
||||
self.unify_free_answer_var(bound_ty.var, b.into())?;
|
||||
return Ok(b);
|
||||
}
|
||||
}
|
||||
|
||||
match (&a.sty, &b.sty) {
|
||||
(&ty::Bound(a_debruijn, a_bound), &ty::Bound(b_debruijn, b_bound)) => {
|
||||
assert_eq!(a_debruijn, b_debruijn);
|
||||
assert_eq!(a_bound.var, b_bound.var);
|
||||
Ok(a)
|
||||
}
|
||||
|
||||
// Those should have been canonicalized away.
|
||||
(ty::Placeholder(..), _) => {
|
||||
bug!("unexpected placeholder ty in `AnswerSubstitutor`: {:?} ", a);
|
||||
}
|
||||
|
||||
// Everything else should just be a perfect match as well,
|
||||
// and we forbid inference variables.
|
||||
_ => match ty::relate::super_relate_tys(self, a, b) {
|
||||
Ok(ty) => Ok(ty),
|
||||
Err(err) => bug!("type mismatch in `AnswerSubstitutor`: {}", err),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn regions(
|
||||
&mut self,
|
||||
a: ty::Region<'tcx>,
|
||||
b: ty::Region<'tcx>,
|
||||
) -> RelateResult<'tcx, ty::Region<'tcx>> {
|
||||
let b = match b {
|
||||
&ty::ReVar(vid) => self.infcx
|
||||
.borrow_region_constraints()
|
||||
.opportunistic_resolve_var(self.infcx.tcx, vid),
|
||||
|
||||
other => other,
|
||||
};
|
||||
|
||||
if let &ty::ReLateBound(debruijn, bound) = a {
|
||||
// Free bound region
|
||||
if debruijn == self.binder_index {
|
||||
self.unify_free_answer_var(bound.assert_bound_var(), b.into())?;
|
||||
return Ok(b);
|
||||
}
|
||||
}
|
||||
|
||||
match (a, b) {
|
||||
(&ty::ReLateBound(a_debruijn, a_bound), &ty::ReLateBound(b_debruijn, b_bound)) => {
|
||||
assert_eq!(a_debruijn, b_debruijn);
|
||||
assert_eq!(a_bound.assert_bound_var(), b_bound.assert_bound_var());
|
||||
}
|
||||
|
||||
(ty::ReStatic, ty::ReStatic) |
|
||||
(ty::ReErased, ty::ReErased) |
|
||||
(ty::ReEmpty, ty::ReEmpty) => (),
|
||||
|
||||
(&ty::ReFree(a_free), &ty::ReFree(b_free)) => {
|
||||
assert_eq!(a_free, b_free);
|
||||
}
|
||||
|
||||
_ => bug!("unexpected regions in `AnswerSubstitutor`: {:?}, {:?}", a, b),
|
||||
}
|
||||
|
||||
Ok(a)
|
||||
}
|
||||
}
|
98
src/librustc_traits/chalk_context/unify.rs
Normal file
98
src/librustc_traits/chalk_context/unify.rs
Normal file
@ -0,0 +1,98 @@
|
||||
use rustc::infer::nll_relate::{TypeRelating, TypeRelatingDelegate, NormalizationStrategy};
|
||||
use rustc::infer::{InferCtxt, RegionVariableOrigin};
|
||||
use rustc::traits::{DomainGoal, Goal, Environment, InEnvironment};
|
||||
use rustc::ty::relate::{Relate, TypeRelation, RelateResult};
|
||||
use rustc::ty;
|
||||
use syntax_pos::DUMMY_SP;
|
||||
|
||||
crate struct UnificationResult<'tcx> {
|
||||
crate goals: Vec<InEnvironment<'tcx, Goal<'tcx>>>,
|
||||
crate constraints: Vec<super::RegionConstraint<'tcx>>,
|
||||
}
|
||||
|
||||
crate fn unify<'me, 'gcx, 'tcx, T: Relate<'tcx>>(
|
||||
infcx: &'me InferCtxt<'me, 'gcx, 'tcx>,
|
||||
environment: Environment<'tcx>,
|
||||
a: &T,
|
||||
b: &T
|
||||
) -> RelateResult<'tcx, UnificationResult<'tcx>> {
|
||||
let mut delegate = ChalkTypeRelatingDelegate::new(
|
||||
infcx,
|
||||
environment
|
||||
);
|
||||
|
||||
TypeRelating::new(
|
||||
infcx,
|
||||
&mut delegate,
|
||||
ty::Variance::Invariant
|
||||
).relate(a, b)?;
|
||||
|
||||
Ok(UnificationResult {
|
||||
goals: delegate.goals,
|
||||
constraints: delegate.constraints,
|
||||
})
|
||||
}
|
||||
|
||||
struct ChalkTypeRelatingDelegate<'me, 'gcx: 'tcx, 'tcx: 'me> {
|
||||
infcx: &'me InferCtxt<'me, 'gcx, 'tcx>,
|
||||
environment: Environment<'tcx>,
|
||||
goals: Vec<InEnvironment<'tcx, Goal<'tcx>>>,
|
||||
constraints: Vec<super::RegionConstraint<'tcx>>,
|
||||
}
|
||||
|
||||
impl ChalkTypeRelatingDelegate<'me, 'gcx, 'tcx> {
|
||||
fn new(
|
||||
infcx: &'me InferCtxt<'me, 'gcx, 'tcx>,
|
||||
environment: Environment<'tcx>,
|
||||
) -> Self {
|
||||
Self {
|
||||
infcx,
|
||||
environment,
|
||||
goals: Vec::new(),
|
||||
constraints: Vec::new(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl TypeRelatingDelegate<'tcx> for &mut ChalkTypeRelatingDelegate<'_, '_, 'tcx> {
|
||||
fn create_next_universe(&mut self) -> ty::UniverseIndex {
|
||||
self.infcx.create_next_universe()
|
||||
}
|
||||
|
||||
fn next_existential_region_var(&mut self) -> ty::Region<'tcx> {
|
||||
self.infcx.next_region_var(RegionVariableOrigin::MiscVariable(DUMMY_SP))
|
||||
}
|
||||
|
||||
fn next_placeholder_region(
|
||||
&mut self,
|
||||
placeholder: ty::PlaceholderRegion
|
||||
) -> ty::Region<'tcx> {
|
||||
self.infcx.tcx.mk_region(ty::RePlaceholder(placeholder))
|
||||
}
|
||||
|
||||
fn generalize_existential(&mut self, universe: ty::UniverseIndex) -> ty::Region<'tcx> {
|
||||
self.infcx.next_region_var_in_universe(
|
||||
RegionVariableOrigin::MiscVariable(DUMMY_SP),
|
||||
universe
|
||||
)
|
||||
}
|
||||
|
||||
fn push_outlives(&mut self, sup: ty::Region<'tcx>, sub: ty::Region<'tcx>) {
|
||||
self.constraints.push(ty::OutlivesPredicate(sup.into(), sub));
|
||||
}
|
||||
|
||||
fn push_domain_goal(&mut self, domain_goal: DomainGoal<'tcx>) {
|
||||
let goal = self.environment.with(
|
||||
self.infcx.tcx.mk_goal(domain_goal.into_goal())
|
||||
);
|
||||
self.goals.push(goal);
|
||||
}
|
||||
|
||||
fn normalization() -> NormalizationStrategy {
|
||||
NormalizationStrategy::Lazy
|
||||
}
|
||||
|
||||
fn forbid_inference_vars() -> bool {
|
||||
false
|
||||
}
|
||||
}
|
Loading…
Reference in New Issue
Block a user