From 3b2cfc510b523f62b66c7106f04153f7625c8936 Mon Sep 17 00:00:00 2001 From: scalexm Date: Tue, 6 Nov 2018 20:55:50 +0100 Subject: [PATCH 1/5] Handle inference variables in `nll_relate` and use it for chalk --- src/librustc/infer/nll_relate/mod.rs | 327 +++++++++++++----- src/librustc/ty/relate.rs | 17 +- .../borrow_check/nll/type_check/relate_tys.rs | 17 +- src/librustc_traits/chalk_context/mod.rs | 51 ++- src/librustc_traits/chalk_context/unify.rs | 98 ++++++ 5 files changed, 393 insertions(+), 117 deletions(-) create mode 100644 src/librustc_traits/chalk_context/unify.rs diff --git a/src/librustc/infer/nll_relate/mod.rs b/src/librustc/infer/nll_relate/mod.rs index 9bdbf77fee0a9..ff79c38680f25 100644 --- a/src/librustc/infer/nll_relate/mod.rs +++ b/src/librustc/infer/nll_relate/mod.rs @@ -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 case 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 type vars 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 @@ where 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 are pushing 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; + + 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()); + } - let generalized_ty = self.generalize_value(value_ty); - self.infcx - .force_instantiate_unchecked(var_ty, generalized_ty); + 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 @@ where // 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>(&mut self, value: T) -> T { - TypeGeneralizer { - tcx: self.infcx.tcx, + fn generalize_value>( + &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 @@ where 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 @@ where 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 @@ where 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 @@ where D: TypeRelatingDelegate<'tcx>, { fn tcx(&self) -> TyCtxt<'me, 'gcx, 'tcx> { - self.tcx + self.infcx.tcx } fn tag(&self) -> &'static str { @@ -609,17 +733,89 @@ where } 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 } => { + if self.universe.cannot_name(universe) { + debug!( + "TypeGeneralizer::tys: root universe {:?} cannot name\ + variable in universe {:?}", + self.universe, + universe + ); + return Err(TypeError::Mismatch); + } + + if self.ambient_variance == ty::Bivariant { + // FIXME: we may need a WF predicate (related to #54105). + } + + let origin = *variables.var_origin(vid); + 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 +869,3 @@ where 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, - ); - } - } - } -} diff --git a/src/librustc/ty/relate.rs b/src/librustc/ty/relate.rs index 082c1bd5fea44..60ad7413cc7ff 100644 --- a/src/librustc/ty/relate.rs +++ b/src/librustc/ty/relate.rs @@ -371,6 +371,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 +398,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 +564,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)) } diff --git a/src/librustc_mir/borrow_check/nll/type_check/relate_tys.rs b/src/librustc_mir/borrow_check/nll/type_check/relate_tys.rs index cf4f913080783..9924b03387132 100644 --- a/src/librustc_mir/borrow_check/nll/type_check/relate_tys.rs +++ b/src/librustc_mir/borrow_check/nll/type_check/relate_tys.rs @@ -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 @@ impl TypeRelatingDelegate<'tcx> for NllTypeRelatingDelegate<'_, '_, '_, 'tcx> { }); } } + + fn push_domain_goal(&mut self, _: DomainGoal<'tcx>) { + // No-op + } + + fn normalization() -> NormalizationStrategy { + NormalizationStrategy::Eager + } + + fn forbid_inference_vars() -> bool { + true + } } diff --git a/src/librustc_traits/chalk_context/mod.rs b/src/librustc_traits/chalk_context/mod.rs index 25a6af284b572..e4d93374faa46 100644 --- a/src/librustc_traits/chalk_context/mod.rs +++ b/src/librustc_traits/chalk_context/mod.rs @@ -9,13 +9,14 @@ // except according to those terms. mod program_clauses; +mod unify; -use chalk_engine::fallible::Fallible as ChalkEngineFallible; +use chalk_engine::fallible::{Fallible, NoSolution}; use chalk_engine::{context, hh::HhGoal, DelayedLiteral, Literal, ExClause}; use rustc::infer::canonical::{ - Canonical, CanonicalVarValues, OriginalQueryValues, QueryRegionConstraint, QueryResponse, + Canonical, CanonicalVarValues, OriginalQueryValues, QueryResponse, }; -use rustc::infer::{InferCtxt, InferOk, LateBoundRegionConversionTime}; +use rustc::infer::{InferCtxt, LateBoundRegionConversionTime}; use rustc::traits::{ DomainGoal, ExClauseFold, @@ -30,11 +31,12 @@ use rustc::traits::{ 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 +57,12 @@ crate struct ChalkInferenceContext<'cx, 'gcx: 'tcx, 'tcx: 'cx> { #[derive(Copy, Clone, Debug)] crate struct UniverseMap; +crate type RegionConstraint<'tcx> = ty::OutlivesPredicate, ty::Region<'tcx>>; + #[derive(Clone, Debug, PartialEq, Eq, Hash)] crate struct ConstrainedSubst<'tcx> { subst: CanonicalVarValues<'tcx>, - constraints: Vec>, + constraints: Vec>, } BraceStructTypeFoldableImpl! { @@ -86,7 +90,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 +108,7 @@ impl context::Context for ChalkArenas<'tcx> { type ProgramClauses = Vec>; - type UnificationResult = InferOk<'tcx, ()>; + type UnificationResult = UnificationResult<'tcx>; fn goal_in_environment( env: &Environment<'tcx>, @@ -291,7 +295,7 @@ impl context::ResolventOps, ChalkArenas<'tcx>> _goal: &DomainGoal<'tcx>, _subst: &CanonicalVarValues<'tcx>, _clause: &Clause<'tcx>, - ) -> chalk_engine::fallible::Fallible>> { + ) -> Fallible>> { panic!() } @@ -301,7 +305,7 @@ impl context::ResolventOps, ChalkArenas<'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> { + ) -> Fallible> { panic!() } } @@ -376,7 +380,7 @@ impl context::UnificationOps, ChalkArenas<'tcx>> fn canonicalize_constrained_subst( &mut self, subst: CanonicalVarValues<'tcx>, - constraints: Vec>, + constraints: Vec>, ) -> Canonical<'gcx, ConstrainedSubst<'gcx>> { self.infcx.canonicalize_response(&ConstrainedSubst { subst, constraints }) } @@ -400,11 +404,13 @@ impl context::UnificationOps, ChalkArenas<'tcx>> fn unify_parameters( &mut self, - _environment: &Environment<'tcx>, - _a: &Kind<'tcx>, - _b: &Kind<'tcx>, - ) -> ChalkEngineFallible> { - panic!() + environment: &Environment<'tcx>, + a: &Kind<'tcx>, + b: &Kind<'tcx>, + ) -> Fallible> { + self.infcx.commit_if_ok(|_| { + unify(self.infcx, *environment, a, b).map_err(|_| NoSolution) + }) } fn sink_answer_subset( @@ -421,11 +427,22 @@ impl context::UnificationOps, ChalkArenas<'tcx>> 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>; type ChalkExClause<'tcx> = ExClause>; diff --git a/src/librustc_traits/chalk_context/unify.rs b/src/librustc_traits/chalk_context/unify.rs new file mode 100644 index 0000000000000..3a9c3918d137e --- /dev/null +++ b/src/librustc_traits/chalk_context/unify.rs @@ -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>>, + crate constraints: Vec>, +} + +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>>, + constraints: Vec>, +} + +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 + } +} From 0169dc3f36aec63e5926f2d69e788a396fd10f82 Mon Sep 17 00:00:00 2001 From: scalexm Date: Fri, 9 Nov 2018 14:49:37 +0100 Subject: [PATCH 2/5] Implement `ResolventOps` --- src/librustc/ty/fold.rs | 44 ++- src/librustc/ty/relate.rs | 278 ++++++++++++++++++ src/librustc_traits/chalk_context/mod.rs | 44 +-- .../chalk_context/resolvent_ops.rs | 241 +++++++++++++++ 4 files changed, 572 insertions(+), 35 deletions(-) create mode 100644 src/librustc_traits/chalk_context/resolvent_ops.rs diff --git a/src/librustc/ty/fold.rs b/src/librustc/ty/fold.rs index 6f0e8d4f02680..5b9193ad74ac3 100644 --- a/src/librustc/ty/fold.rs +++ b/src/librustc/ty/fold.rs @@ -679,24 +679,31 @@ impl<'a, 'gcx, 'tcx> TyCtxt<'a, 'gcx, 'tcx> { // 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>(&mut self, t: &ty::Binder) -> ty::Binder { @@ -712,7 +719,14 @@ impl<'a, 'gcx, 'tcx> TypeFolder<'gcx, 'tcx> for Shifter<'a, 'gcx, '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) } } @@ -726,8 +740,15 @@ impl<'a, 'gcx, 'tcx> TypeFolder<'gcx, 'tcx> for Shifter<'a, 'gcx, '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) ) } } @@ -760,7 +781,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 diff --git a/src/librustc/ty/relate.rs b/src/librustc/ty/relate.rs index 60ad7413cc7ff..1b64a686794c0 100644 --- a/src/librustc/ty/relate.rs +++ b/src/librustc/ty/relate.rs @@ -25,6 +25,7 @@ use std::rc::Rc; use std::iter; use rustc_target::spec::abi; use hir as ast; +use traits; pub type RelateResult<'tcx, T> = Result>; @@ -723,6 +724,283 @@ impl<'tcx> Relate<'tcx> for Kind<'tcx> { } } +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 diff --git a/src/librustc_traits/chalk_context/mod.rs b/src/librustc_traits/chalk_context/mod.rs index e4d93374faa46..bc3f2fd951b93 100644 --- a/src/librustc_traits/chalk_context/mod.rs +++ b/src/librustc_traits/chalk_context/mod.rs @@ -9,14 +9,24 @@ // except according to those terms. mod program_clauses; +mod resolvent_ops; mod unify; use chalk_engine::fallible::{Fallible, NoSolution}; -use chalk_engine::{context, hh::HhGoal, DelayedLiteral, Literal, ExClause}; -use rustc::infer::canonical::{ - Canonical, CanonicalVarValues, OriginalQueryValues, QueryResponse, +use chalk_engine::{ + context, + hh::HhGoal, + DelayedLiteral, + Literal, + ExClause }; use rustc::infer::{InferCtxt, LateBoundRegionConversionTime}; +use rustc::infer::canonical::{ + Canonical, + CanonicalVarValues, + OriginalQueryValues, + QueryResponse, +}; use rustc::traits::{ DomainGoal, ExClauseFold, @@ -28,9 +38,9 @@ use rustc::traits::{ 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}; @@ -201,7 +211,7 @@ impl context::ContextOps> for ChalkContext<'cx, 'gcx> { 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()); @@ -286,30 +296,6 @@ impl context::InferenceTable, ChalkArenas<'tcx>> } } -impl context::ResolventOps, 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>> { - 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>>, - ) -> Fallible> { - panic!() - } -} - impl context::TruncateOps, ChalkArenas<'tcx>> for ChalkInferenceContext<'cx, 'gcx, 'tcx> { diff --git a/src/librustc_traits/chalk_context/resolvent_ops.rs b/src/librustc_traits/chalk_context/resolvent_ops.rs new file mode 100644 index 0000000000000..df6458a766d4e --- /dev/null +++ b/src/librustc_traits/chalk_context/resolvent_ops.rs @@ -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<'tcx>> + for ChalkInferenceContext<'cx, 'gcx, 'tcx> +{ + fn resolvent_clause( + &mut self, + environment: &Environment<'tcx>, + goal: &DomainGoal<'tcx>, + subst: &CanonicalVarValues<'tcx>, + clause: &Clause<'tcx>, + ) -> Fallible>> { + 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> { + 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>( + &mut self, + _variance: ty::Variance, + a: &T, + b: &T, + ) -> RelateResult<'tcx, T> { + // We don't care about variance. + self.relate(a, b) + } + + fn binders>( + &mut self, + a: &ty::Binder, + b: &ty::Binder, + ) -> RelateResult<'tcx, ty::Binder> { + 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) + } +} From b2b82f790b0342fa7eb4e3b81bf1ae00681b4543 Mon Sep 17 00:00:00 2001 From: scalexm Date: Thu, 15 Nov 2018 20:05:36 +0100 Subject: [PATCH 3/5] Implement `AggregateOps` `make_solution` does not return any guidance for now --- src/librustc_traits/chalk_context/mod.rs | 30 ++++++++++++++++++++++-- 1 file changed, 28 insertions(+), 2 deletions(-) diff --git a/src/librustc_traits/chalk_context/mod.rs b/src/librustc_traits/chalk_context/mod.rs index bc3f2fd951b93..58a8d2abd9962 100644 --- a/src/librustc_traits/chalk_context/mod.rs +++ b/src/librustc_traits/chalk_context/mod.rs @@ -26,6 +26,7 @@ use rustc::infer::canonical::{ CanonicalVarValues, OriginalQueryValues, QueryResponse, + Certainty, }; use rustc::traits::{ DomainGoal, @@ -132,9 +133,34 @@ impl context::AggregateOps> for ChalkContext<'cx, 'gcx> { fn make_solution( &self, _root_goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>, - _simplified_answers: impl context::AnswerStream>, + mut simplified_answers: impl context::AnswerStream>, ) -> Option>> { - 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: (), + } + })) } } From c805e817a93a641ef92e58900bc5b0876bbf51f1 Mon Sep 17 00:00:00 2001 From: scalexm Date: Thu, 29 Nov 2018 20:29:50 +0100 Subject: [PATCH 4/5] Fix doc comments --- src/librustc/infer/nll_relate/mod.rs | 10 +++++----- .../borrow_check/nll/type_check/relate_tys.rs | 2 +- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/librustc/infer/nll_relate/mod.rs b/src/librustc/infer/nll_relate/mod.rs index ff79c38680f25..ce5aee81ef9d7 100644 --- a/src/librustc/infer/nll_relate/mod.rs +++ b/src/librustc/infer/nll_relate/mod.rs @@ -16,15 +16,15 @@ //! Here are the key differences: //! //! - This code may choose to bypass some checks (e.g. the occurs check) -//! in case 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. +//! 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 type vars at all, not even +//! 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 @@ -265,7 +265,7 @@ where } /// Relate a projection type and some value type lazily. This will always - /// succeed, but we are pushing an additional `ProjectionEq` goal depending + /// 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)`. diff --git a/src/librustc_mir/borrow_check/nll/type_check/relate_tys.rs b/src/librustc_mir/borrow_check/nll/type_check/relate_tys.rs index 9924b03387132..225e2841fb0ac 100644 --- a/src/librustc_mir/borrow_check/nll/type_check/relate_tys.rs +++ b/src/librustc_mir/borrow_check/nll/type_check/relate_tys.rs @@ -118,7 +118,7 @@ impl TypeRelatingDelegate<'tcx> for NllTypeRelatingDelegate<'_, '_, '_, 'tcx> { } fn push_domain_goal(&mut self, _: DomainGoal<'tcx>) { - // No-op + bug!("should never be invoked with eager normalization") } fn normalization() -> NormalizationStrategy { From 1fce415649784ecaf3bcb3a6916e10284c0affec Mon Sep 17 00:00:00 2001 From: scalexm Date: Thu, 29 Nov 2018 20:50:16 +0100 Subject: [PATCH 5/5] Correctly generalize inference variables in `nll_relate` --- src/librustc/infer/nll_relate/mod.rs | 17 ++++++----------- 1 file changed, 6 insertions(+), 11 deletions(-) diff --git a/src/librustc/infer/nll_relate/mod.rs b/src/librustc/infer/nll_relate/mod.rs index ce5aee81ef9d7..972ba16f7e2c7 100644 --- a/src/librustc/infer/nll_relate/mod.rs +++ b/src/librustc/infer/nll_relate/mod.rs @@ -762,23 +762,18 @@ where drop(variables); self.relate(&u, &u) } - TypeVariableValue::Unknown { universe } => { - if self.universe.cannot_name(universe) { - debug!( - "TypeGeneralizer::tys: root universe {:?} cannot name\ - variable in universe {:?}", - self.universe, - universe - ); - return Err(TypeError::Mismatch); - } - + 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={:?}",