From cdeb4a64422f5d0ecf11254108db3281c9cc6ffd Mon Sep 17 00:00:00 2001 From: scalexm Date: Sun, 3 Jun 2018 16:36:26 +0200 Subject: [PATCH 1/2] Add support for quantified bounds on GATs --- chalk-parse/src/ast.rs | 8 ++++++- chalk-parse/src/parser.lalrpop | 14 +++++++++++- src/ir.rs | 26 ++++++++++++++++----- src/ir/lowering.rs | 34 ++++++++++++++++----------- src/ir/lowering/test.rs | 28 +++++++++++++++++++++++ src/rules.rs | 8 ++++--- src/rules/wf.rs | 8 ++++--- src/rules/wf/test.rs | 42 ++++++++++++++++++++++++++++++++++ src/solve/test.rs | 24 +++++++++++++++++++ 9 files changed, 165 insertions(+), 27 deletions(-) diff --git a/chalk-parse/src/ast.rs b/chalk-parse/src/ast.rs index 2712c82f7c2..e08e5a0d267 100644 --- a/chalk-parse/src/ast.rs +++ b/chalk-parse/src/ast.rs @@ -62,7 +62,7 @@ pub struct TraitFlags { pub struct AssocTyDefn { pub name: Identifier, pub parameter_kinds: Vec, - pub bounds: Vec, + pub bounds: Vec, pub where_clauses: Vec, } @@ -85,6 +85,12 @@ pub enum InlineBound { ProjectionEqBound(ProjectionEqBound), } +#[derive(Clone, PartialEq, Eq, Debug)] +pub struct QuantifiedInlineBound { + pub parameter_kinds: Vec, + pub bound: InlineBound, +} + #[derive(Clone, PartialEq, Eq, Debug)] /// Represents a trait bound on e.g. a type or type parameter. /// Does not know anything about what it's binding. diff --git a/chalk-parse/src/parser.lalrpop b/chalk-parse/src/parser.lalrpop index d739c10f32c..b1c42e95bb4 100644 --- a/chalk-parse/src/parser.lalrpop +++ b/chalk-parse/src/parser.lalrpop @@ -74,7 +74,7 @@ TraitDefn: TraitDefn = { }; AssocTyDefn: AssocTyDefn = { - "type" > >)?> + "type" > >)?> ";" => { AssocTyDefn { @@ -114,6 +114,18 @@ ProjectionEqBound: ProjectionEqBound = { } }; +QuantifiedInlineBound: QuantifiedInlineBound = { + => QuantifiedInlineBound { + parameter_kinds: vec![], + bound: b, + }, + + "forall" "<" > ">" => QuantifiedInlineBound { + parameter_kinds: pk, + bound: b, + }, +}; + Impl: Impl = { "impl" > > "for" "{" "}" => diff --git a/src/ir.rs b/src/ir.rs index 037fd870ba8..f85f43889a8 100644 --- a/src/ir.rs +++ b/src/ir.rs @@ -275,12 +275,14 @@ pub enum InlineBound { ProjectionEqBound(ProjectionEqBound), } +pub type QuantifiedInlineBound = Binders; + impl InlineBound { /// Applies the `InlineBound` to `self_ty` and lowers to a [`DomainGoal`]. /// /// Because an `InlineBound` does not know anything about what it's binding, /// you must provide that type as `self_ty`. - crate fn into_where_clauses(&self, self_ty: Ty) -> Vec { + fn into_where_clauses(&self, self_ty: Ty) -> Vec { match self { InlineBound::TraitBound(b) => b.into_where_clauses(self_ty), InlineBound::ProjectionEqBound(b) => b.into_where_clauses(self_ty), @@ -288,6 +290,19 @@ impl InlineBound { } } +impl QuantifiedInlineBound { + crate fn into_where_clauses(&self, self_ty: Ty) -> Vec { + let self_ty = self_ty.up_shift(self.binders.len()); + self.value.into_where_clauses(self_ty).into_iter().map(|wc| { + Binders { + binders: self.binders.clone(), + value: wc, + } + }).collect() + } +} + + /// Represents a trait bound on e.g. a type or type parameter. /// Does not know anything about what it's binding. #[derive(Clone, Debug, PartialEq, Eq, Hash)] @@ -297,7 +312,7 @@ pub struct TraitBound { } impl TraitBound { - crate fn into_where_clauses(&self, self_ty: Ty) -> Vec { + fn into_where_clauses(&self, self_ty: Ty) -> Vec { let trait_ref = self.as_trait_ref(self_ty); vec![WhereClause::Implemented(trait_ref)] } @@ -310,7 +325,6 @@ impl TraitBound { } } } - /// Represents a projection equality bound on e.g. a type or type parameter. /// Does not know anything about what it's binding. #[derive(Clone, Debug, PartialEq, Eq, Hash)] @@ -323,7 +337,7 @@ pub struct ProjectionEqBound { } impl ProjectionEqBound { - crate fn into_where_clauses(&self, self_ty: Ty) -> Vec { + fn into_where_clauses(&self, self_ty: Ty) -> Vec { let trait_ref = self.trait_bound.as_trait_ref(self_ty); let mut parameters = self.parameters.clone(); @@ -361,7 +375,7 @@ pub struct AssociatedTyDatum { /// /// These must be proven by the implementer, for all possible parameters that /// would result in a well-formed projection. - crate bounds: Vec, + crate bounds: Vec, /// Where clauses that must hold for the projection to be well-formed. crate where_clauses: Vec, @@ -373,7 +387,7 @@ impl AssociatedTyDatum { /// ```notrust /// Implemented(::Item: Sized) /// ``` - crate fn bounds_on_self(&self) -> Vec { + crate fn bounds_on_self(&self) -> Vec { let parameters = self.parameter_kinds .anonymize() .iter() diff --git a/src/ir/lowering.rs b/src/ir/lowering.rs index cfaee6c07f7..4be11945ceb 100644 --- a/src/ir/lowering.rs +++ b/src/ir/lowering.rs @@ -414,17 +414,11 @@ impl LowerWhereClauses for Impl { } } -trait LowerWhereClauseVec { - fn lower(&self, env: &Env) -> Result>; +trait LowerWhereClauseVec { + fn lower(&self, env: &Env) -> Result>; } -impl LowerWhereClauseVec for [WhereClause] { - fn lower(&self, env: &Env) -> Result> { - self.iter().flat_map(|wc| wc.lower(env).apply_result()).collect() - } -} - -impl LowerWhereClauseVec for [QuantifiedWhereClause] { +impl LowerWhereClauseVec for [QuantifiedWhereClause] { fn lower(&self, env: &Env) -> Result> { self.iter() .flat_map(|wc| match wc.lower(env) { @@ -723,12 +717,26 @@ impl LowerInlineBound for InlineBound { } } -trait LowerInlineBounds { - fn lower(&self, env: &Env) -> Result>; +trait LowerQuantifiedInlineBound { + fn lower(&self, env: &Env) -> Result; +} + +impl LowerQuantifiedInlineBound for QuantifiedInlineBound { + fn lower(&self, env: &Env) -> Result { + let parameter_kinds = self.parameter_kinds.iter().map(|pk| pk.lower()); + let binders = env.in_binders(parameter_kinds, |env| { + Ok(self.bound.lower(env)?) + })?; + Ok(binders) + } +} + +trait LowerQuantifiedInlineBoundVec { + fn lower(&self, env: &Env) -> Result>; } -impl LowerInlineBounds for Vec { - fn lower(&self, env: &Env) -> Result> { +impl LowerQuantifiedInlineBoundVec for [QuantifiedInlineBound] { + fn lower(&self, env: &Env) -> Result> { self.iter() .map(|b| b.lower(env)) .collect() diff --git a/src/ir/lowering/test.rs b/src/ir/lowering/test.rs index c7b94e38aa6..c7ea694848b 100644 --- a/src/ir/lowering/test.rs +++ b/src/ir/lowering/test.rs @@ -354,6 +354,21 @@ fn gat_parse() { } } +#[test] +fn gat_higher_ranked_bound() { + lowering_success! { + program { + trait Fn {} + trait Ref<'a, T> {} + trait Sized {} + + trait Foo { + type Item: forall<'a> Fn> + Sized; + } + } + } +} + #[test] fn duplicate_parameters() { lowering_error! { @@ -388,6 +403,19 @@ fn duplicate_parameters() { "duplicate or shadowed parameters" } } + + lowering_error! { + program { + trait Fn {} + trait Ref<'a, T> {} + + trait Foo<'a> { + type Item: forall<'a> Fn>; + } + } error_msg { + "duplicate parameters" + } + } } #[test] diff --git a/src/rules.rs b/src/rules.rs index 69303cdc771..9b867115035 100644 --- a/src/rules.rs +++ b/src/rules.rs @@ -717,12 +717,14 @@ impl AssociatedTyDatum { // FromEnv(::Assoc: Bounds) :- FromEnv(Self: Foo) // } clauses.extend(self.bounds_on_self().into_iter().map(|bound| { + // Same as above in case of higher-ranked inline bounds. + let shift = bound.binders.len(); Binders { - binders: binders.clone(), + binders: bound.binders.iter().chain(binders.iter()).cloned().collect(), value: ProgramClauseImplication { - consequence: bound.into_from_env_goal(), + consequence: bound.value.clone().into_from_env_goal(), conditions: vec![ - FromEnv::Trait(trait_ref.clone()).cast() + FromEnv::Trait(trait_ref.clone()).up_shift(shift).cast() ], } }.cast() diff --git a/src/rules/wf.rs b/src/rules/wf.rs index a0c0f11e34b..9bf0c04887a 100644 --- a/src/rules/wf.rs +++ b/src/rules/wf.rs @@ -216,7 +216,8 @@ impl WfSolver { let wf_goals = input_types.into_iter() - .map(|ty| DomainGoal::WellFormed(WellFormed::Ty(ty))); + .map(|ty| DomainGoal::WellFormed(WellFormed::Ty(ty))) + .casted(); let trait_ref = trait_ref.up_shift(assoc_ty.value.binders.len()); @@ -233,9 +234,10 @@ impl WfSolver { bounds.iter() .map(|b| Subst::apply(&all_parameters, b)) .flat_map(|b| b.into_where_clauses(assoc_ty.value.value.ty.clone())) - .map(|g| g.into_well_formed_goal()); + .map(|wc| wc.map(|bound| bound.into_well_formed_goal())) + .casted(); - let goals = wf_goals.chain(bound_goals).casted(); + let goals = wf_goals.chain(bound_goals); let goal = match goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))) { Some(goal) => goal, None => return None, diff --git a/src/rules/wf/test.rs b/src/rules/wf/test.rs index 3e1a3a6317d..0559873914c 100644 --- a/src/rules/wf/test.rs +++ b/src/rules/wf/test.rs @@ -519,3 +519,45 @@ fn higher_ranked_cyclic_requirements() { } } } + +#[test] +fn higher_ranked_inline_bound_on_gat() { + lowering_success! { + program { + trait Fn { } + struct Ref<'a, T> { } + struct i32 {} + + struct fn { } + + impl<'a, T> Fn> for for<'b> fn> { } + + trait Bar { + type Item: forall<'a> Fn>; + } + + impl Bar for i32 { + type Item = for<'a> fn>; + } + } + } + + lowering_error! { + program { + trait Fn { } + struct i32 {} + + struct fn { } + + trait Bar { + type Item: forall Fn; + } + + impl Bar for i32 { + type Item = fn; + } + } error_msg { + "trait impl for \"Bar\" does not meet well-formedness requirements" + } + } +} diff --git a/src/solve/test.rs b/src/solve/test.rs index f6d58f8aac4..a06271205d9 100644 --- a/src/solve/test.rs +++ b/src/solve/test.rs @@ -798,6 +798,30 @@ fn gat_implied_bounds() { "No possible solution" } } + + test! { + program { + trait Fn { } + struct Ref<'a, T> { } + trait Sized { } + + trait Foo { + type Item: forall<'a> Fn> + Sized; + } + } + + goal { + forall { + if (Type: Foo) { + forall<'a, T> { + ::Item: Fn> + } + } + } + } yields { + "Unique" + } + } } #[test] From ddaafd3397ce8988f0ea9e3c6220c8ebb7191fdc Mon Sep 17 00:00:00 2001 From: scalexm Date: Sun, 10 Jun 2018 15:05:56 +0200 Subject: [PATCH 2/2] Fix test --- src/ir/lowering/test.rs | 2 +- src/rules/wf/test.rs | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ir/lowering/test.rs b/src/ir/lowering/test.rs index c7ea694848b..10d4acd84ea 100644 --- a/src/ir/lowering/test.rs +++ b/src/ir/lowering/test.rs @@ -413,7 +413,7 @@ fn duplicate_parameters() { type Item: forall<'a> Fn>; } } error_msg { - "duplicate parameters" + "duplicate or shadowed parameters" } } } diff --git a/src/rules/wf/test.rs b/src/rules/wf/test.rs index 0559873914c..0a5e62fa45b 100644 --- a/src/rules/wf/test.rs +++ b/src/rules/wf/test.rs @@ -549,6 +549,8 @@ fn higher_ranked_inline_bound_on_gat() { struct fn { } + impl Fn for fn { } + trait Bar { type Item: forall Fn; }