From 520c416dc62aa2214f3f2cd0d253c5cacece1553 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Sun, 13 May 2018 20:54:07 -0500 Subject: [PATCH 01/10] Add `Self: Foo` to lowered ProjectionEq where clauses --- src/ir/lowering.rs | 45 +++++++++++++++++++++++------------------ src/ir/lowering/test.rs | 9 ++++++++- 2 files changed, 33 insertions(+), 21 deletions(-) diff --git a/src/ir/lowering.rs b/src/ir/lowering.rs index 252468528da..7c0ba4c7d64 100644 --- a/src/ir/lowering.rs +++ b/src/ir/lowering.rs @@ -441,32 +441,37 @@ trait LowerWhereClause { /// type in Rust and well-formedness checks. impl LowerWhereClause for WhereClause { fn lower(&self, env: &Env) -> Result> { - let goal = match self { + let goals = match self { WhereClause::Implemented { trait_ref } => { - ir::DomainGoal::Holds(ir::WhereClauseAtom::Implemented(trait_ref.lower(env)?)) + vec![ir::DomainGoal::Holds(ir::WhereClauseAtom::Implemented(trait_ref.lower(env)?))] } WhereClause::ProjectionEq { projection, ty, - } => ir::DomainGoal::Holds(ir::WhereClauseAtom::ProjectionEq(ir::ProjectionEq { - projection: projection.lower(env)?, - ty: ty.lower(env)?, - })), + } => vec![ + ir::DomainGoal::Holds(ir::WhereClauseAtom::ProjectionEq(ir::ProjectionEq { + projection: projection.lower(env)?, + ty: ty.lower(env)?, + })), + ir::DomainGoal::Holds(ir::WhereClauseAtom::Implemented( + projection.trait_ref.lower(env)? + )), + ], WhereClause::Normalize { projection, ty, - } => ir::DomainGoal::Normalize(ir::Normalize { + } => vec![ir::DomainGoal::Normalize(ir::Normalize { projection: projection.lower(env)?, ty: ty.lower(env)?, - }), - WhereClause::TyWellFormed { ty } => ir::DomainGoal::WellFormedTy(ty.lower(env)?), - WhereClause::TraitRefWellFormed { trait_ref } => { + })], + WhereClause::TyWellFormed { ty } => vec![ir::DomainGoal::WellFormedTy(ty.lower(env)?)], + WhereClause::TraitRefWellFormed { trait_ref } => vec![ ir::DomainGoal::WellFormed(ir::WhereClauseAtom::Implemented(trait_ref.lower(env)?)) - } - WhereClause::TyFromEnv { ty } => ir::DomainGoal::FromEnvTy(ty.lower(env)?), - WhereClause::TraitRefFromEnv { trait_ref } => { + ], + WhereClause::TyFromEnv { ty } => vec![ir::DomainGoal::FromEnvTy(ty.lower(env)?)], + WhereClause::TraitRefFromEnv { trait_ref } => vec![ ir::DomainGoal::FromEnv(ir::WhereClauseAtom::Implemented(trait_ref.lower(env)?)) - } + ], WhereClause::UnifyTys { .. } | WhereClause::UnifyLifetimes { .. } => { bail!("this form of where-clause not allowed here") } @@ -480,19 +485,19 @@ impl LowerWhereClause for WhereClause { bail!(ErrorKind::NotTrait(trait_name)); } - ir::DomainGoal::InScope(id) + vec![ir::DomainGoal::InScope(id)] } - WhereClause::Derefs { source, target } => { + WhereClause::Derefs { source, target } => vec![ ir::DomainGoal::Derefs(ir::Derefs { source: source.lower(env)?, target: target.lower(env)? }) - } - WhereClause::TyIsLocal { ty } => { + ], + WhereClause::TyIsLocal { ty } => vec![ ir::DomainGoal::IsLocalTy(ty.lower(env)?) - } + ], }; - Ok(vec![goal]) + Ok(goals) } } diff --git a/src/ir/lowering/test.rs b/src/ir/lowering/test.rs index f97a10e27bd..5831923e6b8 100644 --- a/src/ir/lowering/test.rs +++ b/src/ir/lowering/test.rs @@ -228,7 +228,14 @@ fn atc_accounting() { println!("{}", goal_text); assert_eq!( goal_text, - "ForAll { ForAll { ForAll { ProjectionEq(::Iter<'?1> = ?0) } } }" + "ForAll { \ + ForAll { \ + ForAll { \ + (ProjectionEq(::Iter<'?1> = ?0), \ + Implemented(?2: Iterable)) \ + } \ + } \ + }" ); }); } From 3408f36f0be1440e8a2c023ef9b22d3ea3c21271 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Sun, 13 May 2018 18:07:14 -0500 Subject: [PATCH 02/10] Write tests for GATs --- src/ir/lowering/test.rs | 1 + src/rules/wf/test.rs | 122 ++++++++++++++- src/solve/test.rs | 324 +++++++++++++++++++++++++++++++++++++--- src/test_util.rs | 12 +- 4 files changed, 433 insertions(+), 26 deletions(-) diff --git a/src/ir/lowering/test.rs b/src/ir/lowering/test.rs index 5831923e6b8..3962201c4ba 100644 --- a/src/ir/lowering/test.rs +++ b/src/ir/lowering/test.rs @@ -315,6 +315,7 @@ fn gat_parse() { lowering_success! { program { trait Sized {} + trait Clone {} trait Foo { type Item<'a, T>: Sized + Clone where Self: Sized; diff --git a/src/rules/wf/test.rs b/src/rules/wf/test.rs index e190caae516..6f51b17a4c1 100644 --- a/src/rules/wf/test.rs +++ b/src/rules/wf/test.rs @@ -217,7 +217,7 @@ fn projection_type_in_header() { // Projection types in an impl header are not assumed to be well-formed, // an explicit where clause is needed (see below). - impl Bar for ::Value { } + impl Bar for T where ::Value: Bar { } } error_msg { "trait impl for \"Bar\" does not meet well-formedness requirements" } @@ -231,7 +231,125 @@ fn projection_type_in_header() { trait Bar { } - impl Bar for ::Value where T: Foo { } + impl Bar for T where T: Foo, ::Value: Bar { } + } + } +} + +#[test] +fn bound_in_header_from_env() { + lowering_success! { + program { + trait Foo { } + + trait Bar { + type Item: Foo; + } + + struct Stuff { } + + impl Bar for Stuff where T: Foo { + // Should have FromEnv(T: Foo) here. + type Item = T; + } + } + } + + lowering_error! { + program { + trait Foo { } + trait Baz { } + + trait Bar { + type Item: Baz; + } + + struct Stuff { } + + impl Bar for Stuff where T: Foo { + // No T: Baz here. + type Item = T; + } + } error_msg { + "trait impl for \"Bar\" does not meet well-formedness requirements" + } + } +} + +#[test] +fn generic_projection_where_clause() { + lowering_success! { + program { + trait PointerFamily { type Pointer; } + + struct Cow { } + struct CowFamily { } + impl PointerFamily for CowFamily { type Pointer = Cow; } + + struct String { } + struct Foo

where P: PointerFamily { + bar:

::Pointer + } + } + } + + lowering_error! { + program { + trait Copy { } + trait PointerFamily { type Pointer where T: Copy; } + + struct Cow { } + struct CowFamily { } + impl PointerFamily for CowFamily { type Pointer = Cow; } + + struct String { } + struct Foo

where P: PointerFamily { + // No impl Copy for String, so this will fail. + bar:

::Pointer + } + } error_msg { + "type declaration \"Foo\" does not meet well-formedness requirements" + } + } +} + +#[test] +fn generic_projection_bound() { + lowering_success! { + program { + trait Clone { } + trait PointerFamily { type Pointer: Clone where T: Clone; } + + struct Cow { } + impl Clone for Cow where T: Clone { } + + struct CowFamily { } + + // impl is WF due because of: + // - `where T: Clone` clause on PointerFamily::Pointer + // - impl Clone for Cow where T: Clone + impl PointerFamily for CowFamily { type Pointer = Cow; } + + struct String { } + impl Clone for String { } + struct Foo

where P: PointerFamily { + bar:

::Pointer + } + } + } + + lowering_error! { + program { + trait Clone { } + trait PointerFamily { type Pointer: Clone where T: Clone; } + + struct Cow { } + struct CowFamily { } + + // No impl Clone for Cow, so this will fail. + impl PointerFamily for CowFamily { type Pointer = Cow; } + } error_msg { + "trait impl for \"PointerFamily\" does not meet well-formedness requirements" } } } diff --git a/src/solve/test.rs b/src/solve/test.rs index 176f0b098eb..86aaf5c2008 100644 --- a/src/solve/test.rs +++ b/src/solve/test.rs @@ -546,6 +546,129 @@ fn normalize_basic() { } } +#[test] +fn normalize_gat1() { + test! { + program { + struct Vec { } + + trait Iterable { + type Iter<'a>; + } + + impl Iterable for Vec { + type Iter<'a> = Iter<'a, T>; + } + + trait Iterator { + type Item; + } + + struct Iter<'a, T> { } + struct Ref<'a, T> { } + + impl<'a, T> Iterator for Iter<'a, T> { + type Item = Ref<'a, T>; + } + } + + goal { + forall { + forall<'a> { + exists { + Normalize( as Iterable>::Iter<'a> -> U) + } + } + } + } yields { + "Unique; substitution [?0 := Iter<'!2, !1>], lifetime constraints []" + } + } +} + +#[test] +fn normalize_gat2() { + test! { + program { + trait StreamingIterator { type Item<'a>; } + struct Span<'a, T> { } + struct StreamIterMut { } + struct u32 { } + impl StreamingIterator for StreamIterMut { + type Item<'a> = Span<'a, T>; + } + } + + goal { + forall<'a, T> { + exists { + Normalize( as StreamingIterator>::Item<'a> -> U) + } + } + } yields { + "Unique; substitution [?0 := Span<'!1, !2>], lifetime constraints []" + } + + goal { + forall<'a, T> { + as StreamingIterator>::Item<'a> = Span<'a, T> + } + } yields { + "Unique; substitution [], lifetime constraints []" + } + + goal { + forall<'a, T, U> { + if (T: StreamingIterator = Span<'a, U>>) { + >::Item<'a> = Span<'a, U> + } + } + } yields { + "Unique; substitution [], lifetime constraints []" + } + } +} + +#[test] +fn normalize_gat_with_where_clause() { + test! { + program { + trait Sized { } + trait Foo { + type Item where T: Sized; + } + + struct Value { } + struct Sometype { } + impl Foo for Sometype { + type Item = Value; + } + } + + goal { + forall { + exists { + Normalize(::Item -> U) + } + } + } yields { + "No possible solution" + } + + goal { + forall { + exists { + if (T: Sized) { + Normalize(::Item -> U) + } + } + } + } yields { + "Unique; substitution [?0 := Value]" + } + } +} + #[test] fn normalize_implied_bound() { test! { @@ -567,6 +690,46 @@ fn normalize_implied_bound() { } } +#[test] +fn normalize_implied_bound_gat() { + test! { + program { + trait Clone { } + trait Foo { type Item: Clone; } + struct u32 { } + } + + goal { + forall { + if (T: Foo = V>) { + V: Clone + } + } + } yields { + "Unique; substitution []" + } + } + + test! { + program { + trait Clone { } + trait Foo { type Item; } + struct u32 { } + } + + goal { + forall { + if (T: Foo = V>) { + // Without the bound Item: Clone, there is no way to infer this. + V: Clone + } + } + } yields { + "No possible solution" + } + } +} + /// Demonstrates that, given the expected value of the associated /// type, we can use that to narrow down the relevant impls. #[test] @@ -590,6 +753,31 @@ fn normalize_rev_infer() { } } +/// Demonstrates that, given the expected value of the associated +/// type, we can use that to narrow down the relevant impls. +#[test] +fn normalize_rev_infer_gat() { + test! { + program { + trait Combine { type Item; } + struct u32 { } + struct i32 { } + struct Either { } + impl Combine for u32 { type Item = Either; } + impl Combine for i32 { type Item = Either; } + } + + goal { + exists { + T: Combine = Either> + } + } yields { + // T is ?1 and U is ?0, so this is surprising, but correct! (See #126.) + "Unique; substitution [?0 := i32, ?1 := u32]" + } + } +} + /// Demonstrates that, given the expected value of the associated /// type, we can use that to narrow down the relevant impls. #[test] @@ -689,42 +877,58 @@ fn forall_projection() { } } +/// Demonstrates that, given the expected value of the associated +/// type, we can use that to narrow down the relevant impls. #[test] -fn atc1() { +fn forall_projection_gat() { test! { program { - struct Vec { } + trait Eq { } + impl Eq for T { } - trait Iterable { - type Iter<'a>; - } + trait Sized { } - impl Iterable for Vec { - type Iter<'a> = Iter<'a, T>; - } + trait DropOuter<'a> { type Item where U: Sized; } + impl<'a, T> DropOuter<'a> for T { type Item = T; } - trait Iterator { - type Item; + struct Unit { } + struct Ref<'a, T> { } + } + + goal { + forall { + for<'a> >::Item: Eq } + } yields { + "No possible solution" + } - struct Iter<'a, T> { } - struct Ref<'a, T> { } + goal { + forall { + if (T: Sized) { + for<'a> >::Item: Eq + } + } + } yields { + "Unique; substitution [], lifetime constraints []" + } - impl<'a, T> Iterator for Iter<'a, T> { - type Item = Ref<'a, T>; + goal { + forall<'a, T> { + WellFormed(>::Item) } + } yields { + "No possible solution" } goal { forall { - forall<'a> { - exists { - Normalize( as Iterable>::Iter<'a> -> U) - } + if (T: Sized) { + WellFormed(for<'a> >::Item: Eq) } } } yields { - "Unique; substitution [?0 := Iter<'!2, !1>], lifetime constraints []" + "Unique; substitution [], lifetime constraints []" } } } @@ -1020,6 +1224,34 @@ fn mixed_indices_normalize_application() { } } +#[test] +fn mixed_indices_normalize_gat_application() { + test! { + program { + struct Either { } + struct Ref<'a, T> { } + trait Foo { + type T; + } + + impl Foo for Ref<'a, U> { + type T = Either; + } + } + + goal { + exists { + Normalize( as Foo>::T -> Either) + } + } yields { + // Our GAT parameter is mapped to ?0; all others appear left to right + // in our Normalize(...) goal. + "Unique; for { \ + substitution [?0 := ?0, ?1 := '?1, ?2 := ?2, ?3 := ?0, ?4 := ?2], " + } + } +} + #[test] // Test that we properly detect failure even if there are applicable impls at // the top level, if we can't find anything to fill in those impls with @@ -1766,7 +1998,7 @@ fn unselected_projection() { } #[test] -fn unselected_projection_with_atc() { +fn unselected_projection_with_gat() { test! { program { trait Foo { @@ -1780,6 +2012,7 @@ fn unselected_projection_with_atc() { type Item<'a> = Ref<'a, i32>; } } + goal { forall<'a> { if (InScope(Foo)) { @@ -1789,6 +2022,16 @@ fn unselected_projection_with_atc() { } yields { "Unique" } + + goal { + forall<'a> { + if (InScope(Foo)) { + WellFormed(i32::Item<'a>) + } + } + } yields { + "Unique" + } } } @@ -1877,6 +2120,47 @@ fn projection_from_env() { } } +#[test] +fn gat_unify_with_implied_wc() { + test! { + program { + struct Slice { } + + trait Cast { } + trait CastingIter { + type Item: Cast where T: Cast; + } + + impl CastingIter for Slice { + type Item = Castable; + } + + struct Castable { } + impl Cast for Castable { } + } + + goal { + forall { + if ( + FromEnv( as CastingIter>::Item) + ) { + T: Cast + } + } + } yields { + "Unique" + } + + goal { + forall { + T: Cast + } + } yields { + "No possible solution" + } + } +} + // This variant of the above test used to be achingly slow on SLG // solvers, before the "trivial answer" green cut was introduced. // diff --git a/src/test_util.rs b/src/test_util.rs index 89662355c57..0a1921b8db2 100644 --- a/src/test_util.rs +++ b/src/test_util.rs @@ -22,11 +22,15 @@ macro_rules! lowering_success { let program_text = stringify!($program); assert!(program_text.starts_with("{")); assert!(program_text.ends_with("}")); + let result = parse_and_lower_program( + &program_text[1..program_text.len()-1], + $crate::solve::SolverChoice::slg() + ); + if let Err(ref e) = result { + println!("lowering error: {}", e); + } assert!( - parse_and_lower_program( - &program_text[1..program_text.len()-1], - $crate::solve::SolverChoice::slg() - ).is_ok() + result.is_ok() ); } } From c29c033bd74b147d563823e41befce2a46d2d714 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Sun, 13 May 2018 23:14:15 -0500 Subject: [PATCH 03/10] Add GAT rules that don't involve bounds --- src/rules.rs | 101 ++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 72 insertions(+), 29 deletions(-) diff --git a/src/rules.rs b/src/rules.rs index 81afe607d50..e8e08345928 100644 --- a/src/rules.rs +++ b/src/rules.rs @@ -1,6 +1,7 @@ use cast::{Cast, Caster}; use fold::shift::Shift; use ir::{self, ToParameter}; +use std::iter; mod default; mod wf; @@ -181,12 +182,14 @@ impl ir::AssociatedTyValue { program: &ir::Program, impl_datum: &ir::ImplDatum, ) -> Vec { + let associated_ty = &program.associated_ty_data[&self.associated_ty_id]; + // Begin with the innermost parameters (`'a`) and then add those from impl (`T`). let all_binders: Vec<_> = self.value .binders .iter() + .chain(impl_datum.binders.binders.iter()) .cloned() - .chain(impl_datum.binders.binders.iter().cloned()) .collect(); // Assemble the full list of conditions for projection to be valid. @@ -200,7 +203,9 @@ impl ir::AssociatedTyValue { .trait_ref .trait_ref() .up_shift(self.value.len()); - let conditions: Vec = vec![impl_trait_ref.clone().cast()]; + let conditions: Vec = + iter::once(impl_trait_ref.clone().cast()) + .chain(associated_ty.where_clauses.iter().cloned().casted()).collect(); // Bound parameters + `Self` type of the trait-ref let parameters: Vec<_> = { @@ -233,14 +238,12 @@ impl ir::AssociatedTyValue { binders: all_binders.clone(), value: ir::ProgramClauseImplication { consequence: normalize_goal.clone(), - conditions: conditions.clone(), + conditions: conditions, }, }.cast(); let unselected_projection = ir::UnselectedProjectionTy { - type_name: program.associated_ty_data[&self.associated_ty_id] - .name - .clone(), + type_name: associated_ty.name.clone(), parameters: parameters, }; @@ -410,23 +413,22 @@ impl ir::AssociatedTyDatum { // equality" rules. There are always two; one for a successful normalization, // and one for the "fallback" notion of equality. // - // Given: + // Given: (here, `'a` and `T` represent zero or more parameters) // // trait Foo { - // type Assoc; + // type Assoc<'a, T>: Bounds where WC; // } // // we generate the 'fallback' rule: // - // forall { - // ProjectionEq(::Assoc = (Foo::Assoc)) :- - // T: Foo + // forall { + // ProjectionEq(::Assoc<'a, T> = (Foo::Assoc<'a, T>)). // } // // and // - // forall { - // ProjectionEq(::Assoc = U) :- + // forall { + // ProjectionEq(::Assoc<'a, T> = U) :- // Normalize(::Assoc -> U) // } // @@ -473,37 +475,76 @@ impl ir::AssociatedTyDatum { }; let app_ty = ir::Ty::Apply(app); + let projection_eq = ir::ProjectionEq { + projection: projection.clone(), + ty: app_ty.clone(), + }; + let mut clauses = vec![]; - // forall { - // ProjectionEq(::Assoc = (Foo::Assoc)) :- - // T: Foo + // Fallback rule. The solver uses this to move between the projection + // and skolemized type. + // + // forall { + // ProjectionEq(::Assoc = (Foo::Assoc)). // } clauses.push(ir::Binders { binders: binders.clone(), value: ir::ProgramClauseImplication { - consequence: ir::ProjectionEq { - projection: projection.clone(), - ty: app_ty.clone(), - }.cast(), - conditions: vec![trait_ref.clone().cast()], + consequence: projection_eq.clone().cast(), + conditions: vec![], }, }.cast()); - // The above application type is always well-formed, and `::Assoc` will - // unify with `(Foo::Assoc)` only if `T: Foo`, because of the above rule, so we have: + // Well-formedness of projection type. // - // forall { - // WellFormed((Foo::Assoc)). + // forall { + // WellFormed((Foo::Assoc)) :- Self: Foo, WC. // } clauses.push(ir::Binders { binders: binders.clone(), value: ir::ProgramClauseImplication { - consequence: ir::DomainGoal::WellFormedTy(app_ty).cast(), - conditions: vec![], + consequence: ir::DomainGoal::WellFormedTy(app_ty.clone()).cast(), + conditions: iter::once(trait_ref.clone().cast()) + .chain(self.where_clauses.iter().cloned().casted()) + .collect(), }, }.cast()); + // Assuming well-formedness of projection type means we can assume + // the trait ref as well. + // + // Currently we do not use this rule in chalk (it's used in fn bodies), + // but it's here for completeness. + // + // forall { + // FromEnv(Self: Foo) :- FromEnv((Foo::Assoc)). + // } + clauses.push(ir::Binders { + binders: binders.clone(), + value: ir::ProgramClauseImplication { + consequence: ir::DomainGoal::FromEnv(trait_ref.clone().cast()), + conditions: vec![ir::DomainGoal::FromEnvTy(app_ty.clone()).cast()], + } + }.cast()); + + // Reverse rule for where clauses. + // + // forall { + // FromEnv(WC) :- FromEnv((Foo::Assoc)). + // } + // + // This is really a family of clauses, one for each where clause. + clauses.extend(self.where_clauses.iter().map(|wc| { + ir::Binders { + binders: binders.iter().chain(wc.binders.iter()).cloned().collect(), + value: ir::ProgramClauseImplication { + consequence: wc.value.clone().into_from_env_goal(), + conditions: vec![ir::DomainGoal::FromEnvTy(app_ty.clone()).cast()], + } + }.cast() + })); + // add new type parameter U let mut binders = binders; binders.push(ir::ParameterKind::Ty(())); @@ -515,9 +556,11 @@ impl ir::AssociatedTyDatum { // `ProjectionEq(::Assoc = U)` let projection_eq = ir::ProjectionEq { projection: projection.clone(), ty }; - // forall { + // Projection equality rule from above. + // + // forall { // ProjectionEq(::Assoc = U) :- - // Normalize(::Assoc -> U) + // Normalize(::Assoc -> U). // } clauses.push(ir::Binders { binders: binders.clone(), From d109ff082e2f208cb0186fa9a22191623c9d83b1 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Sat, 19 May 2018 22:15:44 -0500 Subject: [PATCH 04/10] Add and lower to ir::InlineBounds --- src/ir.rs | 32 +++++++++++++- src/ir/lowering.rs | 102 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 133 insertions(+), 1 deletion(-) diff --git a/src/ir.rs b/src/ir.rs index e65eb60e9b5..3d07345cbd5 100644 --- a/src/ir.rs +++ b/src/ir.rs @@ -258,6 +258,32 @@ pub struct TraitFlags { pub deref: bool, } +/// An inline bound, e.g. `: Foo` in `impl> SomeType`. +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub enum InlineBound { + TraitBound(TraitBound), + ProjectionEqBound(ProjectionEqBound), +} + +/// 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)] +pub struct TraitBound { + crate trait_id: ItemId, + crate args_no_self: Vec, +} + +/// 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)] +pub struct ProjectionEqBound { + crate trait_bound: TraitBound, + crate associated_ty_id: ItemId, + /// Does not include trait parameters. + crate parameters: Vec, + crate value: Ty, +} + #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub struct AssociatedTyDatum { /// The trait this associated type is defined in. @@ -273,7 +299,11 @@ pub struct AssociatedTyDatum { /// but possibly including more. crate parameter_kinds: Vec>, - // FIXME: inline bounds on the associated ty need to be implemented + /// Bounds on the associated type itself. + /// + /// These must be proven by the implementer, for all possible parameters that + /// would result in a well-formed projection. + crate bounds: Vec, /// Where clauses that must hold for the projection be well-formed. crate where_clauses: Vec, diff --git a/src/ir/lowering.rs b/src/ir/lowering.rs index 7c0ba4c7d64..77460ebc4c4 100644 --- a/src/ir/lowering.rs +++ b/src/ir/lowering.rs @@ -191,6 +191,7 @@ impl LowerProgram for Program { id: info.id, name: defn.name.str, parameter_kinds: parameter_kinds, + bounds: defn.bounds.lower(&env)?, where_clauses: defn.where_clauses.lower(&env)?, }, ); @@ -638,6 +639,107 @@ impl LowerTraitRef for TraitRef { } } +trait LowerTraitBound { + fn lower_trait_bound(&self, env: &Env) -> Result; +} + +impl LowerTraitBound for TraitBound { + fn lower_trait_bound(&self, env: &Env) -> Result { + let id = match env.lookup(self.trait_name)? { + NameLookup::Type(id) => id, + NameLookup::Parameter(_) => bail!(ErrorKind::NotTrait(self.trait_name)), + }; + + let k = env.type_kind(id); + if k.sort != ir::TypeSort::Trait { + bail!(ErrorKind::NotTrait(self.trait_name)); + } + + let parameters = self.args_no_self + .iter() + .map(|a| Ok(a.lower(env)?)) + .collect::>>()?; + + if parameters.len() != k.binders.len() { + bail!( + "wrong number of parameters, expected `{:?}`, got `{:?}`", + k.binders.len(), + parameters.len() + ) + } + + for (binder, param) in k.binders.binders.iter().zip(parameters.iter()) { + check_type_kinds("incorrect kind for trait parameter", binder, param)?; + } + + Ok(ir::TraitBound { + trait_id: id, + args_no_self: parameters, + }) + } +} + +trait LowerInlineBound { + fn lower(&self, env: &Env) -> Result; +} + +impl LowerInlineBound for TraitBound { + fn lower(&self, env: &Env) -> Result { + Ok(ir::InlineBound::TraitBound(self.lower_trait_bound(&env)?)) + } +} + +impl LowerInlineBound for ProjectionEqBound { + fn lower(&self, env: &Env) -> Result { + let trait_bound = self.trait_bound.lower_trait_bound(env)?; + let info = match env.associated_ty_infos.get(&(trait_bound.trait_id, self.name.str)) { + Some(info) => info, + None => bail!("no associated type `{}` defined in trait", self.name.str), + }; + let args: Vec<_> = try!(self.args.iter().map(|a| a.lower(env)).collect()); + + if args.len() != info.addl_parameter_kinds.len() { + bail!( + "wrong number of parameters for associated type (expected {}, got {})", + info.addl_parameter_kinds.len(), + args.len() + ) + } + + for (param, arg) in info.addl_parameter_kinds.iter().zip(args.iter()) { + check_type_kinds("incorrect kind for associated type parameter", param, arg)?; + } + + Ok(ir::InlineBound::ProjectionEqBound(ir::ProjectionEqBound { + trait_bound, + associated_ty_id: info.id, + parameters: args, + value: self.value.lower(env)?, + })) + } +} + +impl LowerInlineBound for InlineBound { + fn lower(&self, env: &Env) -> Result { + match self { + InlineBound::TraitBound(b) => b.lower(&env), + InlineBound::ProjectionEqBound(b) => b.lower(&env), + } + } +} + +trait LowerInlineBounds { + fn lower(&self, env: &Env) -> Result>; +} + +impl LowerInlineBounds for Vec { + fn lower(&self, env: &Env) -> Result> { + self.iter() + .map(|b| b.lower(env)) + .collect() + } +} + trait LowerPolarizedTraitRef { fn lower(&self, env: &Env) -> Result; } From 446df305703608b99b840d0b3878781a4938c771 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Tue, 15 May 2018 23:12:26 -0500 Subject: [PATCH 05/10] Lower bounds on associated types Adds reverse rule and WF rules for associated type bounds. The WF rules aren't quite right, but they'll be fixed in a later commit. --- chalk-parse/src/ast.rs | 2 +- chalk-parse/src/parser.lalrpop | 2 +- src/ir.rs | 70 ++++++++++++++++++++++++++++++++++ src/rules.rs | 66 +++++++++----------------------- src/rules/wf.rs | 51 +++++++++++++++++++++---- 5 files changed, 132 insertions(+), 59 deletions(-) diff --git a/chalk-parse/src/ast.rs b/chalk-parse/src/ast.rs index ae46209564a..5318f9da8f6 100644 --- a/chalk-parse/src/ast.rs +++ b/chalk-parse/src/ast.rs @@ -86,7 +86,7 @@ pub struct TraitBound { pub struct ProjectionEqBound { pub trait_bound: TraitBound, pub name: Identifier, - pub parameters: Vec, + pub args: Vec, pub value: Ty, } diff --git a/chalk-parse/src/parser.lalrpop b/chalk-parse/src/parser.lalrpop index d18516ec134..21881e1f026 100644 --- a/chalk-parse/src/parser.lalrpop +++ b/chalk-parse/src/parser.lalrpop @@ -107,7 +107,7 @@ ProjectionEqBound: ProjectionEqBound = { args_no_self: a.unwrap_or(vec![]), }, name, - parameters: a2, + args: a2, value: ty, } }; diff --git a/src/ir.rs b/src/ir.rs index 3d07345cbd5..ca0f7f500e9 100644 --- a/src/ir.rs +++ b/src/ir.rs @@ -5,6 +5,7 @@ use fold::shift::Shift; use lalrpop_intern::InternedString; use std::collections::{BTreeMap, BTreeSet}; use std::sync::Arc; +use std::iter; #[macro_use] mod macros; @@ -265,6 +266,19 @@ pub enum InlineBound { ProjectionEqBound(ProjectionEqBound), } +impl InlineBound { + /// Applies the `InlineBound` to `self_ty` and lowers to a [`DomainGoal`]. + /// + /// Because an `InlineBound` not know anything about what it's binding, you + /// must provide that type as `self_ty`. + pub fn lower_with_self(&self, self_ty: Ty) -> Vec { + match self { + InlineBound::TraitBound(b) => b.lower_with_self(self_ty), + InlineBound::ProjectionEqBound(b) => b.lower_with_self(self_ty), + } + } +} + /// 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)] @@ -273,6 +287,21 @@ pub struct TraitBound { crate args_no_self: Vec, } +impl TraitBound { + pub fn lower_with_self(&self, self_ty: Ty) -> Vec { + let trait_ref = self.as_trait_ref(self_ty); + vec![DomainGoal::Holds(WhereClauseAtom::Implemented(trait_ref))] + } + + fn as_trait_ref(&self, self_ty: Ty) -> TraitRef { + let self_ty = ParameterKind::Ty(self_ty); + TraitRef { + trait_id: self.trait_id, + parameters: iter::once(self_ty).chain(self.args_no_self.iter().cloned()).collect(), + } + } +} + /// 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)] @@ -284,6 +313,26 @@ pub struct ProjectionEqBound { crate value: Ty, } +impl ProjectionEqBound { + pub fn lower_with_self(&self, self_ty: Ty) -> Vec { + let trait_ref = self.trait_bound.as_trait_ref(self_ty); + + let mut parameters = self.parameters.clone(); + parameters.extend(trait_ref.parameters.clone()); + + vec![ + DomainGoal::Holds(WhereClauseAtom::Implemented(trait_ref)), + DomainGoal::Holds(WhereClauseAtom::ProjectionEq(ProjectionEq { + projection: ProjectionTy { + associated_ty_id: self.associated_ty_id, + parameters: parameters, + }, + ty: self.value.clone(), + })) + ] + } +} + #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub struct AssociatedTyDatum { /// The trait this associated type is defined in. @@ -309,6 +358,27 @@ pub struct AssociatedTyDatum { crate where_clauses: Vec, } +impl AssociatedTyDatum { + /// Returns the associated ty's bounds applied to the projection type, e.g.: + /// + /// ```notrust + /// Implemented(::Item: Sized) + /// ``` + pub fn bounds_on_self(&self) -> Vec { + let parameters = self.parameter_kinds + .anonymize() + .iter() + .zip(0..) + .map(|p| p.to_parameter()) + .collect(); + let self_ty = Ty::Projection(ProjectionTy { + associated_ty_id: self.id, + parameters + }); + self.bounds.iter().flat_map(|b| b.lower_with_self(self_ty.clone())).collect() + } +} + #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub struct AssociatedTyValue { crate associated_ty_id: ItemId, diff --git a/src/rules.rs b/src/rules.rs index e8e08345928..7da0efd55ab 100644 --- a/src/rules.rs +++ b/src/rules.rs @@ -545,6 +545,23 @@ impl ir::AssociatedTyDatum { }.cast() })); + // Reverse rule for implied bounds. + // + // forall { + // FromEnv(::Assoc: Bounds) :- FromEnv(Self: Foo) + // } + clauses.extend(self.bounds_on_self().into_iter().map(|bound| { + ir::Binders { + binders: binders.clone(), + value: ir::ProgramClauseImplication { + consequence: bound.into_from_env_goal(), + conditions: vec![ + ir::DomainGoal::FromEnv(trait_ref.clone().cast()).cast() + ], + } + }.cast() + })); + // add new type parameter U let mut binders = binders; binders.push(ir::ParameterKind::Ty(())); @@ -570,55 +587,6 @@ impl ir::AssociatedTyDatum { }, }.cast()); - - let projection_wc = ir::WhereClauseAtom::ProjectionEq(projection_eq.clone()); - let trait_ref_wc = ir::WhereClauseAtom::Implemented(trait_ref.clone()); - - // We generate a proxy rule for the well-formedness of `T: Foo` which really - // means two things: `T: Foo` and `Normalize(::Assoc -> U)`. So we have the - // following rule: - // - // forall { - // WellFormed(T: Foo) :- - // WellFormed(T: Foo), ProjectionEq(::Assoc = U) - // } - clauses.push(ir::Binders { - binders: binders.clone(), - value: ir::ProgramClauseImplication { - consequence: ir::DomainGoal::WellFormed(projection_wc.clone()), - conditions: vec![ - ir::DomainGoal::WellFormed(trait_ref_wc.clone()).cast(), - projection_eq.clone().cast() - ], - } - }.cast()); - - // We also have two proxy reverse rules, the first one being: - // - // forall { - // FromEnv(T: Foo) :- FromEnv(T: Foo) - // } - clauses.push(ir::Binders { - binders: binders.clone(), - value: ir::ProgramClauseImplication { - consequence: ir::DomainGoal::FromEnv(trait_ref_wc).cast(), - conditions: vec![ir::DomainGoal::FromEnv(projection_wc.clone()).cast()], - }, - }.cast()); - - // And the other one being: - // - // forall { - // ProjectionEq(::Assoc = U) :- FromEnv(T: Foo) - // } - clauses.push(ir::Binders { - binders, - value: ir::ProgramClauseImplication { - consequence: projection_eq.clone().cast(), - conditions: vec![ir::DomainGoal::FromEnv(projection_wc).cast()], - }, - }.cast()); - clauses } } diff --git a/src/rules/wf.rs b/src/rules/wf.rs index b48851bb2ec..8266c2c4c9b 100644 --- a/src/rules/wf.rs +++ b/src/rules/wf.rs @@ -256,17 +256,52 @@ impl WfSolver { // ``` // we would issue the following subgoal: `forall<'a> { WellFormed(Box<&'a T>) }`. let compute_assoc_ty_goal = |assoc_ty: &AssociatedTyValue| { + let assoc_ty_datum = &self.env.associated_ty_data[&assoc_ty.associated_ty_id]; + let bounds = &assoc_ty_datum.bounds; + + let trait_datum = &self.env.trait_data[&assoc_ty_datum.trait_id]; + let mut input_types = Vec::new(); assoc_ty.value.value.ty.fold(&mut input_types); - if input_types.is_empty() { - return None; - } - - let goals = input_types.into_iter().map(|ty| DomainGoal::WellFormedTy(ty).cast()); - let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))) - .expect("at least one goal"); - Some(goal.quantify(QuantifierKind::ForAll, assoc_ty.value.binders.clone())) + let goals = input_types.into_iter() + .map(|ty| DomainGoal::WellFormedTy(ty).cast()); + //.chain(bounds.iter() + // .flat_map(|b| b.clone() + // .lower_with_self(assoc_ty.value.value.ty.clone())) + // .map(|g| g.into_well_formed_goal().cast())); + let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))); + //.expect("at least one goal"); + let goal = goal //Goal::Implies(hypotheses, Box::new(goal)) + .map(|goal| goal.quantify(QuantifierKind::ForAll, assoc_ty.value.binders.clone()));//binders); + + // FIXME this is wrong (and test)! + let mut bound_binders = assoc_ty.value.binders.clone(); + bound_binders.extend(trait_datum.binders.binders.iter()); + + let hypotheses = + assoc_ty_datum.where_clauses + .iter() + .chain(impl_datum.binders.value.where_clauses.iter()) // FIXME binders (and test)! + .cloned() + .map(|wc| wc.map(|bound| bound.into_from_env_goal())) + .casted() + .collect(); + let bound_goal = bounds.iter() + .flat_map(|b| b.clone() + .lower_with_self(assoc_ty.value.value.ty.clone())) + .map(|g| g.into_well_formed_goal().cast()) + .fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))); + let bound_goal = bound_goal.map(|g| { + Goal::Implies(hypotheses, Box::new(g)).quantify(QuantifierKind::ForAll, bound_binders) + }); + + let goal = goal.into_iter() + .chain(bound_goal.into_iter()) + .fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))); + println!("{:?}", goal); + + goal }; let assoc_ty_goals = From 9e52a13c6d24082b158e3bf21e56e8363f4f52e0 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Sun, 20 May 2018 09:39:58 -0500 Subject: [PATCH 06/10] Add test mixed_indices_check_projection_bounds --- src/rules/wf/test.rs | 84 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 84 insertions(+) diff --git a/src/rules/wf/test.rs b/src/rules/wf/test.rs index 6f51b17a4c1..c5df79b0721 100644 --- a/src/rules/wf/test.rs +++ b/src/rules/wf/test.rs @@ -276,6 +276,90 @@ fn bound_in_header_from_env() { } } +#[test] +fn mixed_indices_check_projection_bounds() { + lowering_success! { + program { + trait Foo { } + + trait Bar { + type Item: Foo; + } + + struct Stuff { } + + impl Bar for Stuff where U: Foo { + type Item = U; + } + } + } + + lowering_error! { + program { + trait Foo { } + trait Baz { } + + trait Bar { + type Item: Baz; + } + + struct Stuff { } + + impl Bar for Stuff where U: Foo { + type Item = U; + } + } error_msg { + "trait impl for \"Bar\" does not meet well-formedness requirements" + } + } +} + +#[test] +fn mixed_indices_check_generic_projection_bounds() { + lowering_success! { + program { + struct Stuff { } + + trait Foo { } + + // A type that impls Foo as long as U: Foo. + struct Fooey { } + impl Foo for Fooey where U: Foo { } + + trait Bar { + type Item: Foo where V: Foo; + } + + impl Bar for Stuff where U: Foo { + type Item = Fooey; + } + } + } + + lowering_error! { + program { + struct Stuff { } + + trait Foo { } + trait Baz { } + + // A type that impls Foo as long as U: Foo. + struct Fooey { } + impl Foo for Fooey where U: Foo { } + + trait Bar { + type Item: Baz where V: Foo; + } + + impl Bar for Stuff where U: Foo { + type Item = Fooey; + } + } error_msg { + "trait impl for \"Bar\" does not meet well-formedness requirements" + } + } +} + #[test] fn generic_projection_where_clause() { lowering_success! { From b5d9422eecbbf644d2821adcfc97d8dfad9771e8 Mon Sep 17 00:00:00 2001 From: scalexm Date: Mon, 21 May 2018 23:33:20 +0200 Subject: [PATCH 07/10] Correctly instantiate where clauses / bounds on GATs in `wf.rs` --- src/fold.rs | 13 ++++++ src/ir.rs | 4 +- src/ir/lowering/test.rs | 28 ++++++++++++ src/rules.rs | 5 ++- src/rules/wf.rs | 98 +++++++++++++++++------------------------ src/rules/wf/test.rs | 46 ++++++++----------- 6 files changed, 106 insertions(+), 88 deletions(-) diff --git a/src/fold.rs b/src/fold.rs index bcd60778ed2..f0bbd17df2a 100644 --- a/src/fold.rs +++ b/src/fold.rs @@ -431,6 +431,7 @@ enum_fold!(Constraint[] { LifetimeEq(a, b) }); enum_fold!(Goal[] { Quantified(qkind, subgoal), Implies(wc, subgoal), And(g1, g2), Not(g), Leaf(wc), CannotProve(a) }); enum_fold!(ProgramClause[] { Implies(a), ForAll(a) }); +enum_fold!(InlineBound[] { TraitBound(a), ProjectionEqBound(a) }); macro_rules! struct_fold { ($s:ident $([$($tt_args:tt)*])? { $($name:ident),* $(,)* } $($w:tt)*) => { @@ -582,4 +583,16 @@ struct_fold!(ConstrainedSubst { constraints, }); +struct_fold!(TraitBound { + trait_id, + args_no_self, +}); + +struct_fold!(ProjectionEqBound { + trait_bound, + associated_ty_id, + parameters, + value, +}); + // struct_fold!(ApplicationTy { name, parameters }); -- intentionally omitted, folded through Ty diff --git a/src/ir.rs b/src/ir.rs index ca0f7f500e9..0ea811ad6ff 100644 --- a/src/ir.rs +++ b/src/ir.rs @@ -693,7 +693,9 @@ impl DomainGoal { /// Same as `into_well_formed_goal` but with the `FromEnv` predicate instead of `WellFormed`. crate fn into_from_env_goal(self) -> DomainGoal { match self { - DomainGoal::Holds(wca) => DomainGoal::FromEnv(wca), + DomainGoal::Holds(wca @ WhereClauseAtom::Implemented(..)) => { + DomainGoal::FromEnv(wca) + } goal => goal, } } diff --git a/src/ir/lowering/test.rs b/src/ir/lowering/test.rs index 3962201c4ba..752485c9470 100644 --- a/src/ir/lowering/test.rs +++ b/src/ir/lowering/test.rs @@ -378,3 +378,31 @@ fn duplicate_parameters() { } } } + +#[test] +fn external_items() { + lowering_success! { + program { + extern trait Send { } + extern struct Vec { } + } + } +} + +#[test] +fn deref_trait() { + lowering_success! { + program { + #[lang_deref] trait Deref { type Target; } + } + } + + lowering_error! { + program { + #[lang_deref] trait Deref { } + #[lang_deref] trait DerefDupe { } + } error_msg { + "Duplicate lang item `DerefTrait`" + } + } +} diff --git a/src/rules.rs b/src/rules.rs index 7da0efd55ab..f8f3df45820 100644 --- a/src/rules.rs +++ b/src/rules.rs @@ -536,11 +536,12 @@ impl ir::AssociatedTyDatum { // // This is really a family of clauses, one for each where clause. clauses.extend(self.where_clauses.iter().map(|wc| { + let shift = wc.binders.len(); ir::Binders { - binders: binders.iter().chain(wc.binders.iter()).cloned().collect(), + binders: wc.binders.iter().chain(binders.iter()).cloned().collect(), value: ir::ProgramClauseImplication { consequence: wc.value.clone().into_from_env_goal(), - conditions: vec![ir::DomainGoal::FromEnvTy(app_ty.clone()).cast()], + conditions: vec![ir::DomainGoal::FromEnvTy(app_ty.clone()).up_shift(shift).cast()], } }.cast() })); diff --git a/src/rules/wf.rs b/src/rules/wf.rs index 8266c2c4c9b..1215aa08fab 100644 --- a/src/rules/wf.rs +++ b/src/rules/wf.rs @@ -5,6 +5,8 @@ use errors::*; use cast::*; use solve::SolverChoice; use itertools::Itertools; +use fold::*; +use fold::shift::Shift; mod test; @@ -209,13 +211,11 @@ impl WfSolver { let mut input_types = Vec::new(); impl_datum.binders.value.where_clauses.fold(&mut input_types); - // We partition the input types of the type on which we implement the trait in two categories: - // * projection types, e.g. `::Item`: we will have to prove that these types - // are well-formed, e.g. that we can show that `T: Iterator` holds - // * any other types, e.g. `HashSet`: we will *assume* that these types are well-formed, e.g. - // we will be able to derive that `K: Hash` holds without writing any where clause. + // We retrieve all the input types of the type on which we implement the trait: we will + // *assume* that these types are well-formed, e.g. we will be able to derive that + // `K: Hash` holds without writing any where clause. // - // Examples: + // Example: // ``` // struct HashSet where K: Hash { ... } // @@ -223,24 +223,8 @@ impl WfSolver { // // Inside here, we can rely on the fact that `K: Hash` holds // } // ``` - // - // ``` - // impl Foo for ::Item { - // // The impl is not well-formed, as an exception we do not assume that - // // `::Item` is well-formed and instead want to prove it. - // } - // ``` - // - // ``` - // impl Foo for ::Item where T: Iterator { - // // Now ok. - // } - // ``` let mut header_input_types = Vec::new(); trait_ref.fold(&mut header_input_types); - let (header_projection_types, header_other_types): (Vec<_>, Vec<_>) = - header_input_types.into_iter() - .partition(|ty| ty.is_projection()); // Associated type values are special because they can be parametric (independently of // the impl), so we issue a special goal which is quantified using the binders of the @@ -259,49 +243,48 @@ impl WfSolver { let assoc_ty_datum = &self.env.associated_ty_data[&assoc_ty.associated_ty_id]; let bounds = &assoc_ty_datum.bounds; - let trait_datum = &self.env.trait_data[&assoc_ty_datum.trait_id]; - let mut input_types = Vec::new(); assoc_ty.value.value.ty.fold(&mut input_types); - let goals = input_types.into_iter() - .map(|ty| DomainGoal::WellFormedTy(ty).cast()); - //.chain(bounds.iter() - // .flat_map(|b| b.clone() - // .lower_with_self(assoc_ty.value.value.ty.clone())) - // .map(|g| g.into_well_formed_goal().cast())); - let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))); - //.expect("at least one goal"); - let goal = goal //Goal::Implies(hypotheses, Box::new(goal)) - .map(|goal| goal.quantify(QuantifierKind::ForAll, assoc_ty.value.binders.clone()));//binders); - - // FIXME this is wrong (and test)! - let mut bound_binders = assoc_ty.value.binders.clone(); - bound_binders.extend(trait_datum.binders.binders.iter()); + let wf_goals = + input_types.into_iter() + .map(|ty| DomainGoal::WellFormedTy(ty)); + + let trait_ref = trait_ref.up_shift(assoc_ty.value.binders.len()); + + let all_parameters: Vec<_> = + assoc_ty.value.binders.iter() + .zip(0..) + .map(|p| p.to_parameter()) + .chain(trait_ref.parameters.iter().cloned()) + .collect(); + + let bound_goals = + bounds.iter() + .map(|b| Subst::apply(&all_parameters, b)) + .flat_map(|b| b.lower_with_self(assoc_ty.value.value.ty.clone())) + .map(|g| g.into_well_formed_goal()); + + let goals = wf_goals.chain(bound_goals).casted(); + let goal = match goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))) { + Some(goal) => goal, + None => return None, + }; let hypotheses = assoc_ty_datum.where_clauses .iter() - .chain(impl_datum.binders.value.where_clauses.iter()) // FIXME binders (and test)! - .cloned() + .map(|wc| Subst::apply(&all_parameters, wc)) .map(|wc| wc.map(|bound| bound.into_from_env_goal())) .casted() .collect(); - let bound_goal = bounds.iter() - .flat_map(|b| b.clone() - .lower_with_self(assoc_ty.value.value.ty.clone())) - .map(|g| g.into_well_formed_goal().cast()) - .fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))); - let bound_goal = bound_goal.map(|g| { - Goal::Implies(hypotheses, Box::new(g)).quantify(QuantifierKind::ForAll, bound_binders) - }); - - let goal = goal.into_iter() - .chain(bound_goal.into_iter()) - .fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))); - println!("{:?}", goal); - - goal + + let goal = Goal::Implies( + hypotheses, + Box::new(goal) + ); + + Some(goal.quantify(QuantifierKind::ForAll, assoc_ty.value.binders.clone())) }; let assoc_ty_goals = @@ -318,7 +301,6 @@ impl WfSolver { ); let goals = input_types.into_iter() - .chain(header_projection_types.into_iter()) .map(|ty| DomainGoal::WellFormedTy(ty).cast()) .chain(assoc_ty_goals) .chain(Some(trait_ref_wf).cast()); @@ -337,12 +319,14 @@ impl WfSolver { .cloned() .map(|wc| wc.map(|bound| bound.into_from_env_goal())) .casted() - .chain(header_other_types.into_iter().map(|ty| DomainGoal::FromEnvTy(ty).cast())) + .chain(header_input_types.into_iter().map(|ty| DomainGoal::FromEnvTy(ty).cast())) .collect(); let goal = Goal::Implies(hypotheses, Box::new(goal)) .quantify(QuantifierKind::ForAll, impl_datum.binders.binders.clone()); + println!("{:?}", goal); + match self.solver_choice.solve_root_goal(&self.env, &goal.into_closed_goal()).unwrap() { Some(sol) => sol.is_unique(), None => false, diff --git a/src/rules/wf/test.rs b/src/rules/wf/test.rs index c5df79b0721..befb4214e89 100644 --- a/src/rules/wf/test.rs +++ b/src/rules/wf/test.rs @@ -438,16 +438,6 @@ fn generic_projection_bound() { } } -#[test] -fn external_items() { - lowering_success! { - program { - extern trait Send { } - extern struct Vec { } - } - } -} - #[test] fn higher_ranked_trait_bounds() { lowering_error! { @@ -474,6 +464,24 @@ fn higher_ranked_trait_bounds() { } } +#[test] +fn higher_ranked_trait_bound_on_gat() { + lowering_success! { + program { + trait Foo<'a> { } + struct i32 { } + + trait Bar<'a> { + type Item: Foo<'a> where forall<'b> V: Foo<'b>; + } + + impl<'a> Bar<'a> for i32 { + type Item = V; + } + } + } +} + // See `cyclic_traits`, this is essentially the same but with higher-ranked co-inductive WF goals. #[test] fn higher_ranked_cyclic_requirements() { @@ -511,21 +519,3 @@ fn higher_ranked_cyclic_requirements() { } } } - -#[test] -fn deref_trait() { - lowering_success! { - program { - #[lang_deref] trait Deref { type Target; } - } - } - - lowering_error! { - program { - #[lang_deref] trait Deref { } - #[lang_deref] trait DerefDupe { } - } error_msg { - "Duplicate lang item `DerefTrait`" - } - } -} From fcd7fe2eca12d2cae8bf8dcaccfab009af05c626 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Tue, 22 May 2018 23:48:54 -0500 Subject: [PATCH 08/10] Add failing tests for where clauses --- src/rules/wf.rs | 2 +- src/solve/test.rs | 70 +++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 71 insertions(+), 1 deletion(-) diff --git a/src/rules/wf.rs b/src/rules/wf.rs index 1215aa08fab..397084cef4d 100644 --- a/src/rules/wf.rs +++ b/src/rules/wf.rs @@ -325,7 +325,7 @@ impl WfSolver { let goal = Goal::Implies(hypotheses, Box::new(goal)) .quantify(QuantifierKind::ForAll, impl_datum.binders.binders.clone()); - println!("{:?}", goal); + debug!("WF trait goal: {:?}", goal); match self.solver_choice.solve_root_goal(&self.env, &goal.into_closed_goal()).unwrap() { Some(sol) => sol.is_unique(), diff --git a/src/solve/test.rs b/src/solve/test.rs index 86aaf5c2008..5605949be13 100644 --- a/src/solve/test.rs +++ b/src/solve/test.rs @@ -669,6 +669,76 @@ fn normalize_gat_with_where_clause() { } } +#[test] +fn normalize_gat_with_where_clause2() { + test! { + program { + trait Bar { } + trait Foo { + type Item where U: Bar; + } + + struct i32 { } + impl Foo for i32 { + type Item = U; + } + } + + goal { + forall { + exists { + Normalize(>::Item -> V) + } + } + } yields { + "No possible solution" + } + + goal { + forall { + exists { + if (U: Bar) { + Normalize(>::Item -> V) + } + } + } + } yields { + "Unique; substitution [?0 := !2]" + } + } +} + +#[test] +fn normalize_gat_with_higher_ranked_trait_bound() { + test! { + program { + trait Foo<'a, T> { } + struct i32 { } + + trait Bar<'a, T> { + type Item: Foo<'a, T> where forall<'b> V: Foo<'b, T>; + } + + impl<'a, T> Foo<'a, T> for i32 { } + impl<'a, T> Bar<'a, T> for i32 { + type Item = i32; + } + } + + goal { + forall<'a, T, V> { + if (forall<'b> { V: Foo<'b, T> }) { + exists { + Normalize(>::Item -> U) + } + } + } + } yields { + "Unique; substitution [?0 := i32], lifetime constraints []" + } + } +} + #[test] fn normalize_implied_bound() { test! { From dc524ebfc02f17e905ed9551a5c36c23ac613f77 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Wed, 23 May 2018 14:14:39 -0500 Subject: [PATCH 09/10] Correctly instantiate where clauses on GAT impl values --- src/rules.rs | 32 ++++++++++++++++++++++++-------- 1 file changed, 24 insertions(+), 8 deletions(-) diff --git a/src/rules.rs b/src/rules.rs index f8f3df45820..6ff38f329a0 100644 --- a/src/rules.rs +++ b/src/rules.rs @@ -1,5 +1,6 @@ use cast::{Cast, Caster}; use fold::shift::Shift; +use fold::Subst; use ir::{self, ToParameter}; use std::iter; @@ -192,20 +193,35 @@ impl ir::AssociatedTyValue { .cloned() .collect(); + let impl_trait_ref = impl_datum.binders + .value + .trait_ref + .trait_ref() + .up_shift(self.value.len()); + + let all_parameters: Vec<_> = + self.value.binders + .iter() + .zip(0..) + .map(|p| p.to_parameter()) + .chain(impl_trait_ref.parameters.iter().cloned()) + .collect(); + // Assemble the full list of conditions for projection to be valid. // This comes in two parts, marked as (1) and (2) in example above: // // 1. require that the trait is implemented // 2. any where-clauses from the `type` declaration in the impl - let impl_trait_ref = impl_datum - .binders - .value - .trait_ref - .trait_ref() - .up_shift(self.value.len()); + let where_clauses = + associated_ty.where_clauses + .iter() + .map(|wc| Subst::apply(&all_parameters, wc)) + .casted(); + let conditions: Vec = - iter::once(impl_trait_ref.clone().cast()) - .chain(associated_ty.where_clauses.iter().cloned().casted()).collect(); + where_clauses + .chain(Some(impl_trait_ref.clone().cast())) + .collect(); // Bound parameters + `Self` type of the trait-ref let parameters: Vec<_> = { From a9ebee0ca257d17610a2c0426ab51e73f787cdc5 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Thu, 24 May 2018 14:55:25 -0500 Subject: [PATCH 10/10] Add test implied_from_env and clean up --- src/ir.rs | 14 +++++++------- src/rules.rs | 7 ++----- src/rules/wf.rs | 8 ++++++-- src/solve/test.rs | 34 ++++++++++++++++++++++++++++++++-- 4 files changed, 47 insertions(+), 16 deletions(-) diff --git a/src/ir.rs b/src/ir.rs index 0ea811ad6ff..a0a2cf3ab39 100644 --- a/src/ir.rs +++ b/src/ir.rs @@ -269,9 +269,9 @@ pub enum InlineBound { impl InlineBound { /// Applies the `InlineBound` to `self_ty` and lowers to a [`DomainGoal`]. /// - /// Because an `InlineBound` not know anything about what it's binding, you - /// must provide that type as `self_ty`. - pub fn lower_with_self(&self, self_ty: Ty) -> Vec { + /// Because an `InlineBound` does not know anything about what it's binding, + /// you must provide that type as `self_ty`. + crate fn lower_with_self(&self, self_ty: Ty) -> Vec { match self { InlineBound::TraitBound(b) => b.lower_with_self(self_ty), InlineBound::ProjectionEqBound(b) => b.lower_with_self(self_ty), @@ -288,7 +288,7 @@ pub struct TraitBound { } impl TraitBound { - pub fn lower_with_self(&self, self_ty: Ty) -> Vec { + crate fn lower_with_self(&self, self_ty: Ty) -> Vec { let trait_ref = self.as_trait_ref(self_ty); vec![DomainGoal::Holds(WhereClauseAtom::Implemented(trait_ref))] } @@ -314,7 +314,7 @@ pub struct ProjectionEqBound { } impl ProjectionEqBound { - pub fn lower_with_self(&self, self_ty: Ty) -> Vec { + crate fn lower_with_self(&self, self_ty: Ty) -> Vec { let trait_ref = self.trait_bound.as_trait_ref(self_ty); let mut parameters = self.parameters.clone(); @@ -354,7 +354,7 @@ pub struct AssociatedTyDatum { /// would result in a well-formed projection. crate bounds: Vec, - /// Where clauses that must hold for the projection be well-formed. + /// Where clauses that must hold for the projection to be well-formed. crate where_clauses: Vec, } @@ -364,7 +364,7 @@ impl AssociatedTyDatum { /// ```notrust /// Implemented(::Item: Sized) /// ``` - pub fn bounds_on_self(&self) -> Vec { + crate fn bounds_on_self(&self) -> Vec { let parameters = self.parameter_kinds .anonymize() .iter() diff --git a/src/rules.rs b/src/rules.rs index 6ff38f329a0..4622dd30670 100644 --- a/src/rules.rs +++ b/src/rules.rs @@ -237,7 +237,7 @@ impl ir::AssociatedTyValue { let projection = ir::ProjectionTy { associated_ty_id: self.associated_ty_id, - // Add the remaining parameters of the trait-ref if any + // Add the remaining parameters of the trait-ref, if any parameters: parameters.iter() .chain(&impl_trait_ref.parameters[1..]) .cloned() @@ -528,10 +528,7 @@ impl ir::AssociatedTyDatum { }.cast()); // Assuming well-formedness of projection type means we can assume - // the trait ref as well. - // - // Currently we do not use this rule in chalk (it's used in fn bodies), - // but it's here for completeness. + // the trait ref as well. Mostly used in function bodies. // // forall { // FromEnv(Self: Foo) :- FromEnv((Foo::Assoc)). diff --git a/src/rules/wf.rs b/src/rules/wf.rs index 397084cef4d..ddf4a83805a 100644 --- a/src/rules/wf.rs +++ b/src/rules/wf.rs @@ -258,7 +258,9 @@ impl WfSolver { .map(|p| p.to_parameter()) .chain(trait_ref.parameters.iter().cloned()) .collect(); - + + // Add bounds from the trait. Because they are defined on the trait, + // their parameters must be substituted with those of the impl. let bound_goals = bounds.iter() .map(|b| Subst::apply(&all_parameters, b)) @@ -271,6 +273,8 @@ impl WfSolver { None => return None, }; + // Add where clauses from the associated ty definition. We must + // substitute parameters here, like we did with the bounds above. let hypotheses = assoc_ty_datum.where_clauses .iter() @@ -278,7 +282,7 @@ impl WfSolver { .map(|wc| wc.map(|bound| bound.into_from_env_goal())) .casted() .collect(); - + let goal = Goal::Implies( hypotheses, Box::new(goal) diff --git a/src/solve/test.rs b/src/solve/test.rs index 5605949be13..bc75818f98f 100644 --- a/src/solve/test.rs +++ b/src/solve/test.rs @@ -740,7 +740,7 @@ fn normalize_gat_with_higher_ranked_trait_bound() { } #[test] -fn normalize_implied_bound() { +fn implied_bounds() { test! { program { trait Clone { } @@ -761,7 +761,7 @@ fn normalize_implied_bound() { } #[test] -fn normalize_implied_bound_gat() { +fn gat_implied_bounds() { test! { program { trait Clone { } @@ -800,6 +800,36 @@ fn normalize_implied_bound_gat() { } } +#[test] +fn implied_from_env() { + test! { + program { + trait Clone { } + trait Foo { type Item; } + } + + goal { + forall { + if (FromEnv(>::Item)) { + FromEnv(T: Foo) + } + } + } yields { + "Unique" + } + + goal { + forall { + if (FromEnv(>::Item)) { + FromEnv(T: Clone) + } + } + } yields { + "No possible solution" + } + } +} + /// Demonstrates that, given the expected value of the associated /// type, we can use that to narrow down the relevant impls. #[test]