diff --git a/src/fold.rs b/src/fold.rs index 1fa900e7041..6e4a91fbf67 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 bb523f99690..b5086da1719 100644 --- a/src/ir.rs +++ b/src/ir.rs @@ -688,7 +688,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 e7fd29b18a6..981bd0f4b98 100644 --- a/src/rules.rs +++ b/src/rules.rs @@ -496,11 +496,12 @@ impl ir::AssociatedTyDatum { // FromEnv(WC) :- FromEnv((Foo::Assoc)). // } 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() })); @@ -539,55 +540,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 three 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()); - - // The second: - // - // forall { - // ProjectionEq(::Assoc = U) :- FromEnv(T: Foo) - // } - clauses.push(ir::Binders { - binders: binders.clone(), - value: ir::ProgramClauseImplication { - consequence: projection_eq.clone().cast(), - conditions: vec![ir::DomainGoal::FromEnv(projection_wc).cast()], - }, - }.cast()); - // And the third: // // forall { diff --git a/src/rules/wf.rs b/src/rules/wf.rs index 06a66fe3a01..55f3cedec5a 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; @@ -207,13 +209,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 { ... } // @@ -221,24 +221,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 @@ -257,49 +241,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 = @@ -316,7 +299,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()); @@ -335,12 +317,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`" - } - } -}