From a4ddd09d4d3f73250e5ccf5ada56a8655ed9f55f Mon Sep 17 00:00:00 2001 From: scalexm Date: Thu, 25 Jan 2018 12:11:54 +0100 Subject: [PATCH 01/10] Add implied bounds and WF requirements --- chalk-parse/src/ast.rs | 7 +- chalk-parse/src/parser.lalrpop | 15 +-- src/cast.rs | 19 +++ src/errors.rs | 10 ++ src/fold/mod.rs | 5 +- src/ir/debug.rs | 13 ++ src/ir/mod.rs | 46 +++---- src/lower/default.rs | 2 +- src/lower/mod.rs | 199 ++++++++++++++++-------------- src/lower/test.rs | 2 +- src/lower/wf.rs | 209 ++++++++++++++++++++++++++++++++ src/solve/test/mod.rs | 213 --------------------------------- src/zip.rs | 4 +- 13 files changed, 403 insertions(+), 341 deletions(-) create mode 100644 src/lower/wf.rs diff --git a/chalk-parse/src/ast.rs b/chalk-parse/src/ast.rs index 667f6d0529b..3ed832184a9 100644 --- a/chalk-parse/src/ast.rs +++ b/chalk-parse/src/ast.rs @@ -181,6 +181,8 @@ pub enum WhereClause { ProjectionEq { projection: ProjectionTy, ty: Ty }, TyWellFormed { ty: Ty }, TraitRefWellFormed { trait_ref: TraitRef }, + TyFromEnv { ty: Ty }, + TraitRefFromEnv { trait_ref: TraitRef }, UnifyTys { a: Ty, b: Ty }, UnifyLifetimes { a: Lifetime, b: Lifetime }, TraitInScope { trait_name: Identifier }, @@ -202,10 +204,7 @@ pub struct Clause { pub enum Goal { ForAll(Vec, Box), Exists(Vec, Box), - - // The `bool` flag indicates whether we should elaborate where clauses or not - Implies(Vec, Box, bool), - + Implies(Vec, Box), And(Box, Box), Not(Box), diff --git a/chalk-parse/src/parser.lalrpop b/chalk-parse/src/parser.lalrpop index 8343025b9c4..c9428f6a80c 100644 --- a/chalk-parse/src/parser.lalrpop +++ b/chalk-parse/src/parser.lalrpop @@ -29,17 +29,12 @@ pub Goal: Box = { Goal1: Box = { "forall" "<" > ">" "{" "}" => Box::new(Goal::ForAll(p, g)), "exists" "<" > ">" "{" "}" => Box::new(Goal::Exists(p, g)), - "(" > ")" "{" "}" => Box::new(Goal::Implies(w, g, i)), + "if" "(" > ")" "{" "}" => Box::new(Goal::Implies(w, g)), "not" "{" "}" => Box::new(Goal::Not(g)), => Box::new(Goal::Leaf(w)), "(" ")", }; -IfKeyword: bool = { - "if" => true, - "if_raw" => false, -}; - StructDefn: StructDefn = { "struct" > "{" "}" => StructDefn { name: n, @@ -187,9 +182,11 @@ WhereClause: WhereClause = { "WellFormed" "(" ")" => WhereClause::TyWellFormed { ty: t }, - "WellFormed" "(" > ")" => WhereClause::TraitRefWellFormed { - trait_ref: t - }, + "WellFormed" "(" > ")" => WhereClause::TraitRefWellFormed { trait_ref: t }, + + "FromEnv" "(" ")" => WhereClause::TyFromEnv { ty: t }, + + "FromEnv" "(" > ")" => WhereClause::TraitRefFromEnv { trait_ref: t }, "=" => WhereClause::UnifyTys { a, b }, diff --git a/src/cast.rs b/src/cast.rs index a5ff5a2adbe..ed8011de5ac 100644 --- a/src/cast.rs +++ b/src/cast.rs @@ -111,6 +111,18 @@ impl Cast for WellFormed { } } +impl Cast for FromEnv { + fn cast(self) -> DomainGoal { + DomainGoal::FromEnv(self) + } +} + +impl Cast for FromEnv { + fn cast(self) -> LeafGoal { + LeafGoal::DomainGoal(self.cast()) + } +} + impl Cast for WellFormed { fn cast(self) -> Goal { let wcg: LeafGoal = self.cast(); @@ -118,6 +130,13 @@ impl Cast for WellFormed { } } +impl Cast for FromEnv { + fn cast(self) -> Goal { + let wcg: LeafGoal = self.cast(); + wcg.cast() + } +} + impl Cast for Normalize { fn cast(self) -> Goal { let wcg: LeafGoal = self.cast(); diff --git a/src/errors.rs b/src/errors.rs index bdf8c19456f..38ad9b2f8ef 100644 --- a/src/errors.rs +++ b/src/errors.rs @@ -34,6 +34,16 @@ error_chain! { display("overlapping impls of trait {:?}", trait_id) } + IllFormedTypeDecl(ty_id: ir::Identifier) { + description("ill-formed type declaration") + display("type declaration {:?} does not meet well-formedness requirements", ty_id) + } + + IllFormedTraitImpl(trait_id: ir::Identifier) { + description("ill-formed trait impl") + display("trait impl for {:?} does not meet well-formedness requirements", trait_id) + } + CouldNotMatch { description("could not match") display("could not match") diff --git a/src/fold/mod.rs b/src/fold/mod.rs index 69766b34ce4..3afc6e14ec8 100644 --- a/src/fold/mod.rs +++ b/src/fold/mod.rs @@ -404,8 +404,9 @@ macro_rules! enum_fold { enum_fold!(PolarizedTraitRef[] { Positive(a), Negative(a) }); enum_fold!(ParameterKind[T,L] { Ty(a), Lifetime(a) } where T: Fold, L: Fold); -enum_fold!(DomainGoal[] { Implemented(a), ProjectionEq(a), Normalize(a), UnselectedNormalize(a), WellFormed(a), InScope(a) }); -enum_fold!(WellFormed[] { Ty(a), TraitRef(a) }); +enum_fold!(DomainGoal[] { Implemented(a), ProjectionEq(a), Normalize(a), UnselectedNormalize(a), WellFormed(a), FromEnv(a), InScope(a) }); +enum_fold!(WellFormed[] { Ty(a), TraitRef(a), Normalize(a) }); +enum_fold!(FromEnv[] { Ty(a), TraitRef(a), Normalize(a) }); enum_fold!(LeafGoal[] { EqGoal(a), DomainGoal(a) }); enum_fold!(Constraint[] { LifetimeEq(a, b) }); enum_fold!(Goal[] { Quantified(qkind, subgoal), Implies(wc, subgoal), And(g1, g2), Not(g), Leaf(wc), diff --git a/src/ir/debug.rs b/src/ir/debug.rs index 163a0c44c81..b4941e9e0e4 100644 --- a/src/ir/debug.rs +++ b/src/ir/debug.rs @@ -182,6 +182,7 @@ impl Debug for DomainGoal { Angle(&n.parameters[1..]) ), DomainGoal::WellFormed(ref n) => write!(fmt, "{:?}", n), + DomainGoal::FromEnv(ref n) => write!(fmt, "{:?}", n), DomainGoal::InScope(ref n) => write!(fmt, "InScope({:?})", n), } } @@ -201,11 +202,23 @@ impl Debug for WellFormed { let value: &Debug = match *self { WellFormed::Ty(ref t) => t, WellFormed::TraitRef(ref t) => t, + WellFormed::Normalize(ref t) => t, }; write!(fmt, "WellFormed({:?})", value) } } +impl Debug for FromEnv { + fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> { + let value: &Debug = match *self { + FromEnv::Ty(ref t) => t, + FromEnv::TraitRef(ref t) => t, + FromEnv::Normalize(ref t) => t, + }; + write!(fmt, "FromEnv({:?})", value) + } +} + impl Debug for EqGoal { fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> { write!(fmt, "({:?} = {:?})", self.a, self.b) diff --git a/src/ir/mod.rs b/src/ir/mod.rs index 0f5e56548de..51448774445 100644 --- a/src/ir/mod.rs +++ b/src/ir/mod.rs @@ -1,4 +1,3 @@ -use cast::Cast; use chalk_parse::ast; use fallible::*; use fold::{DefaultTypeFolder, ExistentialFolder, Fold, IdentityUniversalFolder}; @@ -444,6 +443,7 @@ pub enum DomainGoal { Normalize(Normalize), UnselectedNormalize(UnselectedNormalize), WellFormed(WellFormed), + FromEnv(FromEnv), InScope(ItemId), } @@ -462,27 +462,20 @@ impl DomainGoal { } } - /// A clause of the form (T: Foo) expands to (T: Foo), WF(T: Foo). - /// A clause of the form (T: Foo) expands to (T: Foo), T: Foo, WF(T: Foo). - crate fn expanded(self, program: &Program) -> impl Iterator { - let mut expanded = vec![]; + crate fn into_well_formed_clause(self) -> DomainGoal { match self { - DomainGoal::Implemented(ref trait_ref) => { - expanded.push(WellFormed::TraitRef(trait_ref.clone()).cast()) - } - DomainGoal::ProjectionEq(ProjectionEq { ref projection, .. }) => { - let (associated_ty_data, trait_params, _) = program.split_projection(&projection); - let trait_ref = TraitRef { - trait_id: associated_ty_data.trait_id, - parameters: trait_params.to_owned(), - }; - expanded.push(WellFormed::TraitRef(trait_ref.clone()).cast()); - expanded.push(trait_ref.cast()); - } - _ => (), - }; - expanded.push(self.cast()); - expanded.into_iter() + DomainGoal::Implemented(tr) => DomainGoal::WellFormed(WellFormed::TraitRef(tr)), + DomainGoal::Normalize(n) => DomainGoal::WellFormed(WellFormed::Normalize(n)), + goal => goal, + } + } + + crate fn into_from_env_clause(self) -> DomainGoal { + match self { + DomainGoal::Implemented(tr) => DomainGoal::FromEnv(FromEnv::TraitRef(tr)), + DomainGoal::Normalize(n) => DomainGoal::FromEnv(FromEnv::Normalize(n)), + goal => goal, + } } } @@ -505,6 +498,14 @@ pub struct EqGoal { pub enum WellFormed { Ty(Ty), TraitRef(TraitRef), + Normalize(Normalize), +} + +#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)] +pub enum FromEnv { + Ty(Ty), + TraitRef(TraitRef), + Normalize(Normalize), } /// Proves that the given projection **normalizes** to the given @@ -717,6 +718,9 @@ impl UCanonical> { let trait_datum = &program.trait_data[&tr.trait_id]; trait_datum.binders.value.flags.auto } + Goal::Leaf(LeafGoal::DomainGoal(DomainGoal::WellFormed(WellFormed::TraitRef(_)))) => { + true + } _ => false, } } diff --git a/src/lower/default.rs b/src/lower/default.rs index 3af1a0698f9..ecdfed9753c 100644 --- a/src/lower/default.rs +++ b/src/lower/default.rs @@ -3,7 +3,7 @@ use solve::infer::InferenceTable; use cast::Cast; impl Program { - pub(super) fn add_default_impls(&mut self) { + pub fn add_default_impls(&mut self) { // For each auto trait `MyAutoTrait` and for each struct/type `MyStruct` for auto_trait in self.trait_data .values() diff --git a/src/lower/mod.rs b/src/lower/mod.rs index 4d70b3be5bf..70068578615 100644 --- a/src/lower/mod.rs +++ b/src/lower/mod.rs @@ -11,6 +11,7 @@ use solve::SolverChoice; mod test; mod default; +mod wf; type TypeIds = BTreeMap; type TypeKinds = BTreeMap; @@ -119,6 +120,7 @@ impl LowerProgram for Program { fn lower(&self, solver_choice: SolverChoice) -> Result { let mut program = self.lower_without_coherence()?; program.record_specialization_priorities(solver_choice)?; + program.verify_well_formedness(solver_choice)?; Ok(program) } @@ -445,6 +447,10 @@ impl LowerWhereClause for WhereClause { WhereClause::TraitRefWellFormed { ref trait_ref } => { ir::WellFormed::TraitRef(trait_ref.lower(env)?).cast() } + WhereClause::TyFromEnv { ref ty } => ir::FromEnv::Ty(ty.lower(env)?).cast(), + WhereClause::TraitRefFromEnv { ref trait_ref } => { + ir::FromEnv::TraitRef(trait_ref.lower(env)?).cast() + } WhereClause::UnifyTys { .. } | WhereClause::UnifyLifetimes { .. } => { bail!("this form of where-clause not allowed here") } @@ -481,6 +487,10 @@ impl LowerWhereClause for WhereClause { WhereClause::TraitRefWellFormed { ref trait_ref } => { ir::WellFormed::TraitRef(trait_ref.lower(env)?).cast() } + WhereClause::TyFromEnv { ref ty } => ir::FromEnv::Ty(ty.lower(env)?).cast(), + WhereClause::TraitRefFromEnv { ref trait_ref } => { + ir::FromEnv::TraitRef(trait_ref.lower(env)?).cast() + } WhereClause::UnifyTys { ref a, ref b } => ir::EqGoal { a: ir::ParameterKind::Ty(a.lower(env)?), b: ir::ParameterKind::Ty(b.lower(env)?), @@ -925,19 +935,8 @@ impl<'k> LowerGoal> for Goal { Goal::Exists(ref ids, ref g) => { g.lower_quantified(env, ir::QuantifierKind::Exists, ids) } - Goal::Implies(ref wc, ref g, elaborate) => { - let mut where_clauses = wc.lower(env)?; - if elaborate { - where_clauses = ir::tls::with_current_program(|program| { - let program = program.expect("cannot elaborate without a program"); - where_clauses - .into_iter() - .flat_map(|wc| wc.expanded(program)) - .casted() - .collect() - }); - } - Ok(Box::new(ir::Goal::Implies(where_clauses, g.lower(env)?))) + Goal::Implies(ref wc, ref g) => { + Ok(Box::new(ir::Goal::Implies(wc.lower(env)?, g.lower(env)?))) } Goal::And(ref g1, ref g2) => { Ok(Box::new(ir::Goal::And(g1.lower(env)?, g2.lower(env)?))) @@ -987,12 +986,12 @@ impl ir::Program { program_clauses.extend( self.struct_data .values() - .flat_map(|d| d.to_program_clauses(self)), + .flat_map(|d| d.to_program_clauses()), ); program_clauses.extend( self.trait_data .values() - .flat_map(|d| d.to_program_clauses(self)), + .flat_map(|d| d.to_program_clauses()), ); program_clauses.extend( self.associated_ty_data @@ -1005,7 +1004,7 @@ impl ir::Program { // If we encounter a negative impl, do not generate any rule. Negative impls // are currently just there to deactivate default impls for auto traits. if datum.binders.value.trait_ref.is_positive() { - program_clauses.push(datum.to_program_clause(self)); + program_clauses.push(datum.to_program_clause()); program_clauses.extend( datum .binders @@ -1032,9 +1031,9 @@ impl ir::ImplDatum { /// Given `impl Clone for Vec`, generate: /// /// ```notrust - /// forall { (Vec: Clone) :- (T: Clone), WF(T: Clone) } + /// forall { (Vec: Clone) :- (T: Clone) } /// ``` - fn to_program_clause(&self, program: &ir::Program) -> ir::ProgramClause { + fn to_program_clause(&self) -> ir::ProgramClause { ir::ProgramClause { implication: self.binders.map_ref(|bound| { ir::ProgramClauseImplication { @@ -1043,7 +1042,6 @@ impl ir::ImplDatum { .where_clauses .iter() .cloned() - .flat_map(|wc| wc.expanded(program)) .casted() .collect(), } @@ -1072,8 +1070,8 @@ impl ir::DefaultImplDatum { /// ```notrust /// forall { /// (MyList: Send) :- - /// (T: Send), WF(T: Send), - /// (Box>>: Send), WF(Box>>: Send) + /// (T: Send), + /// (Box>>: Send) /// } /// ``` fn to_program_clause(&self) -> ir::ProgramClause { @@ -1242,14 +1240,15 @@ impl Anonymize for [ir::ParameterKind] { } impl ir::StructDatum { - fn to_program_clauses(&self, program: &ir::Program) -> Vec { + fn to_program_clauses(&self) -> Vec { // Given: // // struct Foo { } // // we generate the following clause: // - // for WF(Foo) :- WF(?T), (?T: Eq), WF(?T: Eq). + // for WF(Foo) :- (?T: Eq). + // for FromEnv(?T: Eq) :- FromEnv(Foo). let wf = ir::ProgramClause { implication: self.binders.map_ref(|bound_datum| { @@ -1257,34 +1256,42 @@ impl ir::StructDatum { consequence: ir::WellFormed::Ty(bound_datum.self_ty.clone().cast()).cast(), conditions: { - let tys = bound_datum - .self_ty - .parameters - .iter() - .filter_map(|pk| pk.as_ref().ty()) - .cloned() - .map(|ty| ir::WellFormed::Ty(ty)) - .casted(); - - let where_clauses = bound_datum - .where_clauses - .iter() - .cloned() - .flat_map(|wc| wc.expanded(program)) - .casted(); - - tys.chain(where_clauses).collect() + bound_datum.where_clauses + .iter() + .cloned() + .casted() + .collect() }, } }), }; - vec![wf] + let mut clauses = vec![wf]; + let condition = ir::FromEnv::Ty(self.binders.value.self_ty.clone().cast()); + + for wc in self.binders + .value + .where_clauses + .iter() + .cloned() + .map(|wc| wc.into_from_env_clause()) + { + clauses.push(ir::ProgramClause { + implication: self.binders.map_ref(|_| { + ir::ProgramClauseImplication { + consequence: wc.cast(), + conditions: vec![condition.clone().cast()], + } + }) + }); + } + + clauses } } impl ir::TraitDatum { - fn to_program_clauses(&self, program: &ir::Program) -> Vec { + fn to_program_clauses(&self) -> Vec { // Given: // // trait Ord where Self: Eq { ... } @@ -1292,53 +1299,46 @@ impl ir::TraitDatum { // we generate the following clauses: // // for WF(?Self: Ord) :- - // // types are well-formed: - // WF(?Self), - // WF(?T), - // // where clauses declared on the trait are met: - // (?Self: Eq), WF(?Self: Eq) + // (?Self: Ord), WF(?Self: Eq) // - // for (?Self: Eq) :- WF(?Self: Ord) - // for WF(?Self: Ord) :- WF(?Self: Ord) - - let where_clauses = self.binders - .value - .where_clauses - .iter() - .cloned() - .flat_map(|wc| wc.expanded(program)) - .collect::>(); + // for (?Self: Ord) :- FromEnv(?Self: Ord) + // for FromEnv(?Self: Ord) :- FromEnv(?Self: Ord) - let wf = ir::WellFormed::TraitRef(self.binders.value.trait_ref.clone()); + let trait_ref = self.binders.value.trait_ref.clone(); - let clauses = ir::ProgramClause { + let wf = ir::ProgramClause { implication: self.binders.map_ref(|bound| { ir::ProgramClauseImplication { - consequence: wf.clone().cast(), + consequence: ir::WellFormed::TraitRef(trait_ref.clone()).cast(), conditions: { - let tys = bound - .trait_ref - .parameters - .iter() - .filter_map(|pk| pk.as_ref().ty()) - .cloned() - .map(|ty| ir::WellFormed::Ty(ty)) - .casted(); - - tys.chain(where_clauses.iter().cloned().casted()).collect() + bound.where_clauses + .iter() + .cloned() + .map(|wc| wc.into_well_formed_clause().cast()) + .chain(Some(ir::DomainGoal::Implemented(trait_ref.clone()).cast())) + .collect() }, } }), }; - let mut clauses = vec![clauses]; - for wc in where_clauses { + let mut clauses = vec![wf]; + let condition = ir::FromEnv::TraitRef(trait_ref.clone()); + + for wc in self.binders + .value + .where_clauses + .iter() + .cloned() + .map(|wc| wc.into_from_env_clause().cast()) + .chain(Some(ir::DomainGoal::Implemented(trait_ref).cast())) + { clauses.push(ir::ProgramClause { implication: self.binders.map_ref(|_| { ir::ProgramClauseImplication { consequence: wc, - conditions: vec![wf.clone().cast()], + conditions: vec![condition.clone().cast()], } }), }); @@ -1429,42 +1429,63 @@ impl ir::AssociatedTyDatum { ty: app_ty, }.cast(), conditions: vec![ - trait_ref.cast(), + trait_ref.clone().cast(), ], }, }, } }; + // add new type parameter U + let mut binders = binders; + binders.push(ir::ParameterKind::Ty(())); + let ty = ir::Ty::Var(binders.len() - 1); + + // `Normalize(::Assoc -> U)` + let normalize = ir::Normalize { projection: projection.clone(), ty: ty.clone() }; + // forall { // ProjectionEq(::Assoc = U) :- // Normalize(::Assoc -> U) // } - let normalize_clause = { - // add new type parameter U - let mut binders = binders.clone(); - binders.push(ir::ParameterKind::Ty(())); - let ty = ir::Ty::Var(binders.len() - 1); - + let normalize_clause = ir::ProgramClause { implication: ir::Binders { - binders, + binders: binders.clone(), value: ir::ProgramClauseImplication { consequence: ir::ProjectionEq { projection: projection.clone(), - ty: ty.clone(), + ty, }.cast(), - conditions: vec![ - ir::Normalize { - projection: projection.clone(), - ty, - }.cast() - ], + conditions: vec![normalize.clone().cast()], }, }, + }; + + + let well_formed_clause = ir::ProgramClause { + implication: ir::Binders { + binders: binders.clone(), + value: ir::ProgramClauseImplication { + consequence: ir::WellFormed::Normalize(normalize.clone()).cast(), + conditions: vec![ + normalize.clone().cast(), + ir::WellFormed::TraitRef(trait_ref.clone()).cast() + ], + } + } + }; + + let from_env_clause = ir::ProgramClause { + implication: ir::Binders { + binders, + value: ir::ProgramClauseImplication { + consequence: ir::FromEnv::TraitRef(trait_ref).cast(), + conditions: vec![ir::FromEnv::Normalize(normalize).cast()], + }, } }; - vec![fallback_clause, normalize_clause] + vec![fallback_clause, normalize_clause, well_formed_clause, from_env_clause] } } diff --git a/src/lower/test.rs b/src/lower/test.rs index 5d679b02ecf..3e7a0e2a8ce 100755 --- a/src/lower/test.rs +++ b/src/lower/test.rs @@ -32,7 +32,7 @@ macro_rules! lowering_error { fn parse_and_lower(text: &str) -> Result { - chalk_parse::parse_program(text)?.lower(SolverChoice::default()) + chalk_parse::parse_program(text)?.lower(SolverChoice::on_demand_slg()) } fn parse_and_lower_goal(program: &Program, text: &str) -> Result> { diff --git a/src/lower/wf.rs b/src/lower/wf.rs new file mode 100644 index 00000000000..6dc1a239904 --- /dev/null +++ b/src/lower/wf.rs @@ -0,0 +1,209 @@ +use std::sync::Arc; + +use ir::*; +use errors::*; +use cast::Cast; +use solve::SolverChoice; +use itertools::Itertools; + +struct WfSolver { + env: Arc, + solver_choice: SolverChoice, +} + +impl Program { + pub fn verify_well_formedness(&self, solver_choice: SolverChoice) -> Result<()> { + set_current_program(&Arc::new(self.clone()), || self.solve_wf_requirements(solver_choice)) + } + + fn solve_wf_requirements(&self, solver_choice: SolverChoice) -> Result<()> { + let solver = WfSolver { + env: Arc::new(self.environment()), + solver_choice, + }; + + for (id, struct_datum) in &self.struct_data { + if !solver.verify_struct_decl(struct_datum) { + let name = self.type_kinds.get(id).unwrap().name; + return Err(Error::from_kind(ErrorKind::IllFormedTypeDecl(name))); + } + } + + for impl_datum in self.impl_data.values() { + if !solver.verify_trait_impl(impl_datum) { + let trait_ref = impl_datum.binders.value.trait_ref.trait_ref(); + let name = self.type_kinds.get(&trait_ref.trait_id).unwrap().name; + return Err(Error::from_kind(ErrorKind::IllFormedTraitImpl(name))); + } + } + + Ok(()) + } +} + +trait FoldInputTypes { + fn fold(&self, accumulator: &mut Vec); +} + +impl FoldInputTypes for Vec { + fn fold(&self, accumulator: &mut Vec) { + for f in self { + f.fold(accumulator); + } + } +} + +impl FoldInputTypes for Parameter { + fn fold(&self, accumulator: &mut Vec) { + match *self { + ParameterKind::Ty(ref ty) => ty.fold(accumulator), + _ => (), + } + } +} + +impl FoldInputTypes for Ty { + fn fold(&self, accumulator: &mut Vec) { + match *self { + Ty::Apply(ref app) => { + accumulator.push(self.clone()); + app.parameters.fold(accumulator); + } + Ty::Projection(ref proj) => { + accumulator.push(self.clone()); + proj.parameters.fold(accumulator); + } + Ty::UnselectedProjection(ref proj) => { + accumulator.push(self.clone()); + proj.parameters.fold(accumulator); + } + _ => (), + } + } +} + +impl FoldInputTypes for TraitRef { + fn fold(&self, accumulator: &mut Vec) { + self.parameters.fold(accumulator); + } +} + +impl FoldInputTypes for Normalize { + fn fold(&self, accumulator: &mut Vec) { + self.projection.parameters.fold(accumulator); + self.ty.fold(accumulator); + } +} + +impl FoldInputTypes for UnselectedNormalize { + fn fold(&self, accumulator: &mut Vec) { + self.projection.parameters.fold(accumulator); + self.ty.fold(accumulator); + } +} + +impl FoldInputTypes for DomainGoal { + fn fold(&self, accumulator: &mut Vec) { + match *self { + DomainGoal::Implemented(ref tr) => tr.fold(accumulator), + DomainGoal::Normalize(ref n) => n.fold(accumulator), + DomainGoal::UnselectedNormalize(ref n) => n.fold(accumulator), + _ => (), + } + } +} + +impl WfSolver { + fn verify_struct_decl(&self, struct_datum: &StructDatum) -> bool { + let mut input_types = Vec::new(); + struct_datum.binders.value.fields.fold(&mut input_types); + struct_datum.binders.value.where_clauses.fold(&mut input_types); + + if input_types.is_empty() { + return true; + } + + let goals = input_types.into_iter().map(|ty| WellFormed::Ty(ty).cast()); + + let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))) + .expect("at least one goal"); + + let hypotheses = + struct_datum.binders + .value + .where_clauses + .iter() + .cloned() + .map(|wc| wc.into_from_env_clause()) + .collect(); + + let goal = Goal::Implies(hypotheses, Box::new(goal)) + .quantify(QuantifierKind::ForAll, struct_datum.binders.binders.clone()); + + match self.solver_choice.solve_root_goal(&self.env, &goal.into_closed_goal()).unwrap() { + Some(sol) => sol.is_unique(), + None => false, + } + } + + fn verify_trait_impl(&self, impl_datum: &ImplDatum) -> bool { + let trait_ref = match impl_datum.binders.value.trait_ref { + PolarizedTraitRef::Positive(ref trait_ref) => trait_ref, + _ => return true + }; + + let mut input_types = Vec::new(); + impl_datum.binders.value.where_clauses.fold(&mut input_types); + + let compute_assoc_ty_goal = |assoc_ty: &AssociatedTyValue| { + 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| WellFormed::Ty(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 assoc_ty_goals = + impl_datum.binders + .value + .associated_ty_values + .iter() + .filter_map(compute_assoc_ty_goal); + + let goals = + input_types.into_iter() + .map(|ty| WellFormed::Ty(ty).cast()) + .chain(assoc_ty_goals) + .chain(Some(WellFormed::TraitRef(trait_ref.clone())).cast()); + + let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))) + .expect("at least one goal"); + + let mut input_types = Vec::new(); + trait_ref.fold(&mut input_types); + + let hypotheses = + impl_datum.binders + .value + .where_clauses + .iter() + .cloned() + .map(|wc| wc.into_from_env_clause()) + .chain(input_types.into_iter().map(|ty| FromEnv::Ty(ty).cast())) + .collect(); + + let goal = Goal::Implies(hypotheses, Box::new(goal)) + .quantify(QuantifierKind::ForAll, impl_datum.binders.binders.clone()); + + 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/solve/test/mod.rs b/src/solve/test/mod.rs index cfb08c6ccb0..7a31a1c3d2d 100644 --- a/src/solve/test/mod.rs +++ b/src/solve/test/mod.rs @@ -287,18 +287,6 @@ fn prove_forall() { } yields { "Unique; substitution [], lifetime constraints []" } - - // This fails because we used `if_raw`, and hence we do not - // know that `WF(T: Clone)` holds. - goal { - forall { - if_raw (T: Clone) { - Vec: Clone - } - } - } yields { - "No possible solution" - } } } @@ -689,97 +677,6 @@ fn forall_projection() { } } -#[test] -fn elaborate_eq() { - test! { - program { - trait PartialEq { } - trait Eq where Self: PartialEq { } - } - - goal { - forall { - if (T: Eq) { - T: PartialEq - } - } - } yields { - "Unique; substitution [], lifetime constraints []" - } - } -} - -#[test] -fn elaborate_transitive() { - test! { - program { - trait PartialEq { } - trait Eq where Self: PartialEq { } - trait StrictEq where Self: Eq { } - } - - goal { - forall { - if (T: StrictEq) { - T: PartialEq - } - } - } yields { - "Unique; substitution [], lifetime constraints []" - } - } -} - -#[test] -#[ignore] -fn elaborate_normalize() { - test! { - program { - trait Eq { } - struct i32 { } - - trait Item where ::Out: Eq { - type Out; - } - - impl Eq for i32 { } - impl Item for i32 { - type Out = i32; - } - } - - goal { - forall { - if (T: Item) { - U: Eq - } - } - } yields { - "Unique; substitution [], lifetime constraints []" - } - - goal { - forall { - if (T: Item) { - T: Item - } - } - } yields { - "Unique" - } - - goal { - forall { - if (T: Item) { - T: Item - } - } - } yields { - "Unique" - } - } -} - #[test] fn atc1() { test! { @@ -887,116 +784,6 @@ fn generic_trait() { } } -#[test] -fn trait_wf() { - test! { - program { - struct Vec where T: Sized { } - struct Slice where T: Sized { } - struct Int { } - - trait Sized { } - trait Eq { } - trait Ord where Self: Eq { } - - impl Sized for Vec where T: Sized { } - impl Sized for Int { } - - impl Eq for Int { } - impl Eq> for Vec where T: Eq { } - - impl Ord for Int { } - impl Ord> for Vec where T: Ord { } - - impl Ord> for Slice { } - } - - goal { - WellFormed(Slice) - } yields { - "Unique; substitution [], lifetime constraints []" - } - - goal { - Slice: Sized - } yields { - "No possible solution" - } - - goal { - WellFormed(Slice: Sized) - } yields { - "Unique; substitution [], lifetime constraints []" - } - - goal { - WellFormed(Slice: Eq>) - } yields { - "Unique; substitution [], lifetime constraints []" - } - - goal { - Slice: Ord> - } yields { - "Unique" - } - - goal { - Slice: Eq> - } yields { - "No possible solution" - } - - // not WF because previous equation doesn't hold, despite Slice having an impl for Ord - goal { - WellFormed(Slice: Ord>) - } yields { - "No possible solution" - } - - goal { - Vec: Eq> - } yields { - "Unique; substitution [], lifetime constraints []" - } - - // WF because previous equation does hold - goal { - WellFormed(Vec: Ord>) - } yields { - "Unique; substitution [], lifetime constraints []" - } - } -} - -#[test] -fn normalize_fallback_option() { - test! { - program { - trait Iterator { type Item; } - struct Foo { } - struct Vec { } - impl Iterator for Vec { type Item = T; } - } - - goal { - forall { - if (T: Iterator) { - exists { - exists { - // Here, `U` could be `T` or it could be - // `Vec`. - U: Iterator - } - } - } - } - } yields { - "Ambiguous" - } - } -} - #[test] fn normalize_under_binder() { test! { diff --git a/src/zip.rs b/src/zip.rs index d0d90ceb307..af14b21e3d2 100644 --- a/src/zip.rs +++ b/src/zip.rs @@ -220,10 +220,12 @@ enum_zip!(DomainGoal { ProjectionEq, UnselectedNormalize, WellFormed, + FromEnv, InScope, }); enum_zip!(LeafGoal { DomainGoal, EqGoal }); -enum_zip!(WellFormed { Ty, TraitRef }); +enum_zip!(WellFormed { Ty, TraitRef, Normalize }); +enum_zip!(FromEnv { Ty, TraitRef, Normalize }); // Annoyingly, Goal cannot use `enum_zip` because some variants have // two parameters, and I'm too lazy to make the macro account for the From 9d4f4cb159ff0cd84f525da9ba9c123e430f7e20 Mon Sep 17 00:00:00 2001 From: scalexm Date: Mon, 5 Feb 2018 13:01:37 +0100 Subject: [PATCH 02/10] Add tests --- src/lower/test.rs | 152 ++++++++++++++++++++++++++++++++++++++++ src/solve/test/bench.rs | 6 +- src/solve/test/mod.rs | 12 +++- 3 files changed, 166 insertions(+), 4 deletions(-) diff --git a/src/lower/test.rs b/src/lower/test.rs index 3e7a0e2a8ce..5318177d81f 100755 --- a/src/lower/test.rs +++ b/src/lower/test.rs @@ -542,3 +542,155 @@ fn overlapping_negative_impls() { } } } + +#[test] +fn well_formed_trait_decl() { + lowering_success! { + program { + trait Clone { } + trait Copy where Self: Clone { } + + struct i32 { } + + impl Clone for i32 { } + impl Copy for i32 { } + } + } +} + +#[test] +fn ill_formed_trait_decl() { + lowering_error! { + program { + trait Clone { } + trait Copy where Self: Clone { } + + struct i32 { } + + impl Copy for i32 { } + } error_msg { + "trait impl for \"Copy\" does not meet well-formedness requirements" + } + } +} + +#[test] +fn cyclic_traits() { + lowering_success! { + program { + trait A where Self: B { } + trait B where Self: A { } + + impl B for T { } + impl A for T { } + } + } +} + +#[test] +fn cyclic_traits_error() { + lowering_error! { + program { + trait Copy { } + + trait A where Self: B, Self: Copy {} + trait B where Self: A { } + + impl B for T {} + impl A for T where T: B {} + } error_msg { + "trait impl for \"B\" does not meet well-formedness requirements" + } + } +} + +#[test] +fn cyclic_wf_requirement() { + lowering_success! { + program { + trait Foo where ::Value: Foo { + type Value; + } + + struct Unit { } + impl Foo for Unit { + type Value = Unit; + } + } + } +} + +#[test] +fn ill_formed_assoc_ty() { + lowering_error! { + program { + trait Foo { } + struct OnlyFoo where T: Foo { } + + struct i32 { } + + trait Bar { + type Value; + } + + impl Bar for i32 { + type Value = OnlyFoo; + } + } error_msg { + "trait impl for \"Bar\" does not meet well-formedness requirements" + } + } +} + +#[test] +fn implied_bounds() { + lowering_success! { + program { + trait Eq { } + trait Hash where Self: Eq { } + + struct Set where K: Hash { } + + struct OnlyEq where T: Eq { } + + trait Foo { + type Value; + } + + impl Foo for Set { + type Value = OnlyEq; + } + } + } +} + +#[test] +fn ill_formed_ty_decl() { + lowering_error! { + program { + trait Hash { } + struct Set where K: Hash { } + + struct MyType { + value: Set + } + } error_msg { + "type declaration \"MyType\" does not meet well-formedness requirements" + } + } +} + +#[test] +fn implied_bounds_on_ty_decl() { + lowering_success! { + program { + trait Eq { } + trait Hash where Self: Eq { } + struct OnlyEq where T: Eq { } + + struct MyType where K: Hash { + value: OnlyEq + } + } + } +} diff --git a/src/solve/test/bench.rs b/src/solve/test/bench.rs index 818402b19f0..23baba7f8bb 100644 --- a/src/solve/test/bench.rs +++ b/src/solve/test/bench.rs @@ -17,8 +17,9 @@ fn run_bench( goal_text: &str, bencher: &mut Bencher, expected: &str, + skip_coherence: bool ) { - let program = Arc::new(parse_and_lower_program(program_text, solver_choice).unwrap()); + let program = Arc::new(parse_and_lower_program(program_text, solver_choice, skip_coherence).unwrap()); let env = Arc::new(program.environment()); ir::tls::set_current_program(&program, || { let goal = parse_and_lower_goal(&program, goal_text).unwrap(); @@ -108,6 +109,7 @@ fn cycley_recursive_cached(b: &mut Bencher) { CYCLEY_GOAL, b, "Unique", + true ); } @@ -122,6 +124,7 @@ fn cycley_recursive_uncached(b: &mut Bencher) { CYCLEY_GOAL, b, "Unique", + true ); } @@ -135,5 +138,6 @@ fn cycley_slg(b: &mut Bencher) { CYCLEY_GOAL, b, "Unique", + false ); } diff --git a/src/solve/test/mod.rs b/src/solve/test/mod.rs index 7a31a1c3d2d..6802f1789ac 100644 --- a/src/solve/test/mod.rs +++ b/src/solve/test/mod.rs @@ -10,8 +10,14 @@ use std::sync::Arc; mod bench; -fn parse_and_lower_program(text: &str, solver_choice: SolverChoice) -> Result { - chalk_parse::parse_program(text)?.lower(solver_choice) +fn parse_and_lower_program(text: &str, solver_choice: SolverChoice, skip_coherence: bool) + -> Result +{ + if skip_coherence { + chalk_parse::parse_program(text)?.lower_without_coherence() + } else { + chalk_parse::parse_program(text)?.lower(solver_choice) + } } fn parse_and_lower_goal(program: &ir::Program, text: &str) -> Result> { @@ -98,7 +104,7 @@ fn solve_goal(program_text: &str, goals: Vec<(&str, SolverChoice, &str)>) { for (goal_text, solver_choice, expected) in goals { let (program, env) = program_env_cache.entry(solver_choice).or_insert_with(|| { let program_text = &program_text[1..program_text.len() - 1]; // exclude `{}` - let program = Arc::new(parse_and_lower_program(program_text, solver_choice).unwrap()); + let program = Arc::new(parse_and_lower_program(program_text, solver_choice, false).unwrap()); let env = Arc::new(program.environment()); (program, env) }); From a640beaf12a4ee55d9a648e104b8df9c6a01c67e Mon Sep 17 00:00:00 2001 From: scalexm Date: Mon, 5 Feb 2018 21:05:18 +0100 Subject: [PATCH 03/10] Add WF requirements for projection types --- src/ir/could_match.rs | 7 +--- src/ir/mod.rs | 7 ++++ src/lower/mod.rs | 97 +++++++++++++++++++++++++------------------ src/lower/test.rs | 68 +++++++++++++++++++++++++++++- src/lower/wf.rs | 13 +++--- 5 files changed, 140 insertions(+), 52 deletions(-) diff --git a/src/ir/could_match.rs b/src/ir/could_match.rs index f8365e59477..060c259c3bf 100644 --- a/src/ir/could_match.rs +++ b/src/ir/could_match.rs @@ -17,12 +17,7 @@ impl CouldMatch for T { fn zip_tys(&mut self, a: &Ty, b: &Ty) -> Fallible<()> { let could_match = match (a, b) { (&Ty::Apply(ref a), &Ty::Apply(ref b)) => { - let names_could_match = match (a.name, b.name) { - (TypeName::ItemId(item_a), TypeName::ItemId(item_b)) => { - item_a == item_b - } - _ => true, - }; + let names_could_match = a.name == b.name; names_could_match && a.parameters diff --git a/src/ir/mod.rs b/src/ir/mod.rs index 51448774445..75d03093974 100644 --- a/src/ir/mod.rs +++ b/src/ir/mod.rs @@ -296,6 +296,13 @@ impl Ty { _ => panic!("{:?} is not a projection", self), } } + + pub fn is_projection(&self) -> bool { + match *self { + Ty::Projection(..) | Ty::UnselectedProjection(..) => true, + _ => false, + } + } } /// for<'a...'z> X -- all binders are instantiated at once, diff --git a/src/lower/mod.rs b/src/lower/mod.rs index 70068578615..af5b8d03ded 100644 --- a/src/lower/mod.rs +++ b/src/lower/mod.rs @@ -1407,34 +1407,42 @@ impl ir::AssociatedTyDatum { } }; + // Construct an application from the projection. So if we have `::Item`, + // we would produce `(Iterator::Item)`. + let app = ir::ApplicationTy { + name: ir::TypeName::AssociatedType(self.id), + parameters, + }; + let app_ty = ir::Ty::Apply(app); + + let mut clauses = vec![]; + // forall { // ProjectionEq(::Assoc = (Foo::Assoc)) :- // T: Foo // } - let fallback_clause = { - // Construct an application from the projection. So if we have `::Item`, - // we would produce `(Iterator::Item)`. - let app = ir::ApplicationTy { - name: ir::TypeName::AssociatedType(self.id), - parameters, - }; - let app_ty = ir::Ty::Apply(app); - - ir::ProgramClause { - implication: ir::Binders { - binders: binders.clone(), - value: ir::ProgramClauseImplication { - consequence: ir::ProjectionEq { - projection: projection.clone(), - ty: app_ty, - }.cast(), - conditions: vec![ - trait_ref.clone().cast(), - ], - }, + clauses.push(ir::ProgramClause { + implication: 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()], }, + }, + }); + + clauses.push(ir::ProgramClause { + implication: ir::Binders { + binders: binders.clone(), + value: ir::ProgramClauseImplication { + consequence: ir::WellFormed::Ty(app_ty).cast(), + conditions: vec![], + } } - }; + }); // add new type parameter U let mut binders = binders; @@ -1448,22 +1456,21 @@ impl ir::AssociatedTyDatum { // ProjectionEq(::Assoc = U) :- // Normalize(::Assoc -> U) // } - let normalize_clause = - ir::ProgramClause { - implication: ir::Binders { - binders: binders.clone(), - value: ir::ProgramClauseImplication { - consequence: ir::ProjectionEq { - projection: projection.clone(), - ty, - }.cast(), - conditions: vec![normalize.clone().cast()], - }, + clauses.push(ir::ProgramClause { + implication: ir::Binders { + binders: binders.clone(), + value: ir::ProgramClauseImplication { + consequence: ir::ProjectionEq { + projection: projection.clone(), + ty, + }.cast(), + conditions: vec![normalize.clone().cast()], }, - }; + }, + }); - let well_formed_clause = ir::ProgramClause { + clauses.push(ir::ProgramClause { implication: ir::Binders { binders: binders.clone(), value: ir::ProgramClauseImplication { @@ -1474,18 +1481,28 @@ impl ir::AssociatedTyDatum { ], } } - }; + }); - let from_env_clause = ir::ProgramClause { + clauses.push(ir::ProgramClause { implication: ir::Binders { - binders, + binders: binders.clone(), value: ir::ProgramClauseImplication { consequence: ir::FromEnv::TraitRef(trait_ref).cast(), + conditions: vec![ir::FromEnv::Normalize(normalize.clone()).cast()], + }, + } + }); + + clauses.push(ir::ProgramClause { + implication: ir::Binders { + binders: binders, + value: ir::ProgramClauseImplication { + consequence: normalize.clone().cast(), conditions: vec![ir::FromEnv::Normalize(normalize).cast()], }, } - }; + }); - vec![fallback_clause, normalize_clause, well_formed_clause, from_env_clause] + clauses } } diff --git a/src/lower/test.rs b/src/lower/test.rs index 5318177d81f..bf707d8c7a0 100755 --- a/src/lower/test.rs +++ b/src/lower/test.rs @@ -605,7 +605,7 @@ fn cyclic_traits_error() { } #[test] -fn cyclic_wf_requirement() { +fn cyclic_wf_requirements() { lowering_success! { program { trait Foo where ::Value: Foo { @@ -694,3 +694,69 @@ fn implied_bounds_on_ty_decl() { } } } + +#[test] +fn wf_requiremements_for_projection() { + lowering_error! { + program { + trait Foo { + type Value; + } + + trait Iterator { + type Item; + } + + impl Foo for T { + type Value = ::Item; + } + } error_msg { + "trait impl for \"Foo\" does not meet well-formedness requirements" + } + } + + lowering_success! { + program { + trait Foo { + type Value; + } + + trait Iterator { + type Item; + } + + impl Foo for T where T: Iterator { + type Value = ::Item; + } + } + } +} + +#[test] +fn projection_type_in_header() { + lowering_error! { + program { + trait Foo { + type Value; + } + + trait Bar { } + + impl Bar for ::Value { } + } error_msg { + "trait impl for \"Bar\" does not meet well-formedness requirements" + } + } + + lowering_success! { + program { + trait Foo { + type Value; + } + + trait Bar { } + + impl Bar for ::Value where T: Foo { } + } + } +} diff --git a/src/lower/wf.rs b/src/lower/wf.rs index 6dc1a239904..97b9f4e7676 100644 --- a/src/lower/wf.rs +++ b/src/lower/wf.rs @@ -176,18 +176,21 @@ impl WfSolver { .iter() .filter_map(compute_assoc_ty_goal); + 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()); + let goals = input_types.into_iter() + .chain(header_projection_types.into_iter()) .map(|ty| WellFormed::Ty(ty).cast()) .chain(assoc_ty_goals) .chain(Some(WellFormed::TraitRef(trait_ref.clone())).cast()); let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))) .expect("at least one goal"); - - let mut input_types = Vec::new(); - trait_ref.fold(&mut input_types); - let hypotheses = impl_datum.binders .value @@ -195,7 +198,7 @@ impl WfSolver { .iter() .cloned() .map(|wc| wc.into_from_env_clause()) - .chain(input_types.into_iter().map(|ty| FromEnv::Ty(ty).cast())) + .chain(header_other_types.into_iter().map(|ty| FromEnv::Ty(ty).cast())) .collect(); let goal = Goal::Implies(hypotheses, Box::new(goal)) From 902d344f71e2f8f3e2c46e7b40b1f173876cb31f Mon Sep 17 00:00:00 2001 From: scalexm Date: Mon, 5 Feb 2018 22:31:29 +0100 Subject: [PATCH 04/10] Add documentation --- src/ir/mod.rs | 43 ++++++++++++++++++++++++ src/lower/mod.rs | 43 ++++++++++++++++++++---- src/lower/test.rs | 2 ++ src/lower/wf.rs | 76 ++++++++++++++++++++++++++++++++++++++----- src/solve/test/mod.rs | 6 ++-- 5 files changed, 152 insertions(+), 18 deletions(-) diff --git a/src/ir/mod.rs b/src/ir/mod.rs index 75d03093974..9a9e004412d 100644 --- a/src/ir/mod.rs +++ b/src/ir/mod.rs @@ -469,6 +469,10 @@ impl DomainGoal { } } + /// Turn a where clause into the WF version of it i.e.: + /// * `T: Trait` maps to `WellFormed(T: Trait)` + /// * `T: Trait` maps to `WellFormed(T: Trait)` + /// * any other clause maps to itself crate fn into_well_formed_clause(self) -> DomainGoal { match self { DomainGoal::Implemented(tr) => DomainGoal::WellFormed(WellFormed::TraitRef(tr)), @@ -477,6 +481,7 @@ impl DomainGoal { } } + /// Same as `into_well_formed_clause` but with the `FromEnv` predicate instead of `WellFormed`. crate fn into_from_env_clause(self) -> DomainGoal { match self { DomainGoal::Implemented(tr) => DomainGoal::FromEnv(FromEnv::TraitRef(tr)), @@ -502,6 +507,17 @@ pub struct EqGoal { } #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)] +/// A predicate which is true is some object is well-formed, e.g. a type or a trait ref. +/// For example, given the following type definition: +/// +/// ```notrust +/// struct Set where K: Hash { +/// ... +/// } +/// ``` +/// +/// then we have the following rule: `WellFormed(Set) :- (K: Hash)`. +/// See the complete rules in `lower.rs`. pub enum WellFormed { Ty(Ty), TraitRef(TraitRef), @@ -509,6 +525,25 @@ pub enum WellFormed { } #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)] +/// A predicate which enables deriving everything which should be true if we *know* that some object +/// is well-formed. For example, given the following trait definitions: +/// +/// ```notrust +/// trait Clone { ... } +/// trait Copy where Self: Clone { ... } +/// ``` +/// +/// then we can use `FromEnv(T: Copy)` to derive that `T: Clone`, like in: +/// +/// ```notrust +/// forall { +/// if (FromEnv(T: Copy)) { +/// T: Clone +/// } +/// } +/// ``` +/// +/// See the complete rules in `lower.rs`. pub enum FromEnv { Ty(Ty), TraitRef(TraitRef), @@ -718,8 +753,16 @@ impl UCanonical { } impl UCanonical> { +<<<<<<< HEAD /// A goal has coinductive semantics if it is of the form `T: AutoTrait`. crate fn is_coinductive(&self, program: &ProgramEnvironment) -> bool { +======= + /// A goal has coinductive semantics if it is of the form `T: AutoTrait`, or if it is of the + /// form `WellFormed(T: Trait)` where `Trait` is any trait. The latter is needed for dealing + /// with WF requirements and cyclic traits, which generates cycles in the proof tree which must + /// not be rejected but instead must be treated as a success. + pub fn is_coinductive(&self, program: &ProgramEnvironment) -> bool { +>>>>>>> Add documentation match &self.canonical.value.goal { Goal::Leaf(LeafGoal::DomainGoal(DomainGoal::Implemented(tr))) => { let trait_datum = &program.trait_data[&tr.trait_id]; diff --git a/src/lower/mod.rs b/src/lower/mod.rs index af5b8d03ded..a3e98bb1240 100644 --- a/src/lower/mod.rs +++ b/src/lower/mod.rs @@ -1247,8 +1247,8 @@ impl ir::StructDatum { // // we generate the following clause: // - // for WF(Foo) :- (?T: Eq). - // for FromEnv(?T: Eq) :- FromEnv(Foo). + // forall { WF(Foo) :- (T: Eq). } + // forall { FromEnv(T: Eq) :- FromEnv(Foo). } let wf = ir::ProgramClause { implication: self.binders.map_ref(|bound_datum| { @@ -1296,13 +1296,15 @@ impl ir::TraitDatum { // // trait Ord where Self: Eq { ... } // - // we generate the following clauses: + // we generate the following clause: // - // for WF(?Self: Ord) :- - // (?Self: Ord), WF(?Self: Eq) + // forall { + // WF(Self: Ord) :- (Self: Ord), WF(Self: Eq) + // } // - // for (?Self: Ord) :- FromEnv(?Self: Ord) - // for FromEnv(?Self: Ord) :- FromEnv(?Self: Ord) + // and the reverse rules: + // forall { (Self: Ord) :- FromEnv(Self: Ord) } + // forall { FromEnv(Self: Ord) :- FromEnv(Self: Ord) } let trait_ref = self.binders.value.trait_ref.clone(); @@ -1387,6 +1389,9 @@ impl ir::AssociatedTyDatum { // `ProjectionEq` to fallback *or* normalize it. So instead we // handle this kind of reasoning by expanding "projection // equality" predicates (see `DomainGoal::expanded`). + // + // We also generate rules specific to WF requirements and implied bounds, + // see below. let binders: Vec<_> = self.parameter_kinds .iter() @@ -1434,6 +1439,12 @@ impl ir::AssociatedTyDatum { }, }); + // 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: + // + // forall { + // WellFormed((Foo::Assoc)). + // } clauses.push(ir::ProgramClause { implication: ir::Binders { binders: binders.clone(), @@ -1470,6 +1481,14 @@ impl ir::AssociatedTyDatum { }); + // 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), Normalize(::Assoc -> U) + // } clauses.push(ir::ProgramClause { implication: ir::Binders { binders: binders.clone(), @@ -1483,6 +1502,11 @@ impl ir::AssociatedTyDatum { } }); + // We also have two proxy reverse rules, the first one being: + // + // forall { + // FromEnv(T: Foo) :- FromEnv(T: Foo) + // } clauses.push(ir::ProgramClause { implication: ir::Binders { binders: binders.clone(), @@ -1493,6 +1517,11 @@ impl ir::AssociatedTyDatum { } }); + // And the other one being: + // + // forall { + // Normalize(::Assoc -> U) :- FromEnv(T: Foo) + // } clauses.push(ir::ProgramClause { implication: ir::Binders { binders: binders, diff --git a/src/lower/test.rs b/src/lower/test.rs index bf707d8c7a0..2262ea1567c 100755 --- a/src/lower/test.rs +++ b/src/lower/test.rs @@ -32,6 +32,8 @@ macro_rules! lowering_error { fn parse_and_lower(text: &str) -> Result { + // Use the on-demand SLG solver to avoid ambiguities on projection types encountered when + // using the recursive solver. chalk_parse::parse_program(text)?.lower(SolverChoice::on_demand_slg()) } diff --git a/src/lower/wf.rs b/src/lower/wf.rs index 97b9f4e7676..355a5065c63 100644 --- a/src/lower/wf.rs +++ b/src/lower/wf.rs @@ -41,6 +41,7 @@ impl Program { } } +/// A trait for retrieving all types appearing in some Chalk construction. trait FoldInputTypes { fn fold(&self, accumulator: &mut Vec); } @@ -77,7 +78,10 @@ impl FoldInputTypes for Ty { accumulator.push(self.clone()); proj.parameters.fold(accumulator); } - _ => (), + + // Type parameters and higher-kinded types do not carry any input types (so we can sort + // of assume they are always WF). + Ty::Var(..) | Ty::ForAll(..) => (), } } } @@ -108,6 +112,7 @@ impl FoldInputTypes for DomainGoal { DomainGoal::Implemented(ref tr) => tr.fold(accumulator), DomainGoal::Normalize(ref n) => n.fold(accumulator), DomainGoal::UnselectedNormalize(ref n) => n.fold(accumulator), + DomainGoal::WellFormed(..) | DomainGoal::FromEnv(..) => panic!("unexpected where clause"), _ => (), } } @@ -115,6 +120,7 @@ impl FoldInputTypes for DomainGoal { impl WfSolver { fn verify_struct_decl(&self, struct_datum: &StructDatum) -> bool { + // We retrieve all the input types of the struct fields. let mut input_types = Vec::new(); struct_datum.binders.value.fields.fold(&mut input_types); struct_datum.binders.value.where_clauses.fold(&mut input_types); @@ -124,7 +130,6 @@ impl WfSolver { } let goals = input_types.into_iter().map(|ty| WellFormed::Ty(ty).cast()); - let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))) .expect("at least one goal"); @@ -137,6 +142,8 @@ impl WfSolver { .map(|wc| wc.into_from_env_clause()) .collect(); + // We ask that the above input types are well-formed provided that all the where-clauses + // on the struct definition hold. let goal = Goal::Implies(hypotheses, Box::new(goal)) .quantify(QuantifierKind::ForAll, struct_datum.binders.binders.clone()); @@ -152,9 +159,62 @@ impl WfSolver { _ => return true }; + // We retrieve all the input types of the where clauses appearing on the trait impl, + // e.g. in: + // ``` + // impl Foo for (Set, Vec>) { ... } + // ``` + // we would retrieve `Set`, `Box`, `Vec>`, `(Set, Vec>)`. + // We will have to prove that these types are well-formed. 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. + // + // Examples: + // ``` + // struct HashSet where K: Hash { ... } + // + // impl Foo for HashSet { + // // 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 + // associated type value, for example in: + // ``` + // trait Foo { + // type Item<'a> + // } + // + // impl Foo for Box { + // type Item<'a> = Box<&'a T>; + // } + // ``` + // we would issue the following subgoal: `forall<'a> { WellFormed(Box<&'a T>) }`. let compute_assoc_ty_goal = |assoc_ty: &AssociatedTyValue| { let mut input_types = Vec::new(); assoc_ty.value.value.ty.fold(&mut input_types); @@ -176,12 +236,8 @@ impl WfSolver { .iter() .filter_map(compute_assoc_ty_goal); - 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()); - + // Things to prove well-formed: input types of the where-clauses, projection types + // appearing in the header, associated type values, and of course the trait ref. let goals = input_types.into_iter() .chain(header_projection_types.into_iter()) @@ -191,6 +247,10 @@ impl WfSolver { let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))) .expect("at least one goal"); + + // Assumptions: types appearing in the header which are not projection types are + // assumed to be well-formed, and where clauses declared on the impl are assumed + // to hold. let hypotheses = impl_datum.binders .value diff --git a/src/solve/test/mod.rs b/src/solve/test/mod.rs index 6802f1789ac..ee263dcc641 100644 --- a/src/solve/test/mod.rs +++ b/src/solve/test/mod.rs @@ -14,6 +14,8 @@ fn parse_and_lower_program(text: &str, solver_choice: SolverChoice, skip_coheren -> Result { if skip_coherence { + // We disable WF checks for the recursive solver, because of ambiguities appearing + // with projection types. chalk_parse::parse_program(text)?.lower_without_coherence() } else { chalk_parse::parse_program(text)?.lower(solver_choice) @@ -1527,11 +1529,9 @@ fn coinductive_semantics() { } yields { "No possible solution" } - - // `WellFormed(T)` because of the hand-written impl for `Ptr`. goal { forall { - if (WellFormed(T), T: Send) { + if (T: Send) { List: Send } } From acd499f394b76049bcb7cdbde94ca48e87edb264 Mon Sep 17 00:00:00 2001 From: scalexm Date: Tue, 6 Feb 2018 16:56:45 +0100 Subject: [PATCH 05/10] Add more comments --- src/ir/mod.rs | 7 +------ src/lower/mod.rs | 3 +-- src/lower/test.rs | 30 +++++++++++++++++++++++------- src/lower/wf.rs | 16 +++++++++++----- src/solve/test/mod.rs | 2 +- 5 files changed, 37 insertions(+), 21 deletions(-) diff --git a/src/ir/mod.rs b/src/ir/mod.rs index 9a9e004412d..3ce09c739df 100644 --- a/src/ir/mod.rs +++ b/src/ir/mod.rs @@ -753,16 +753,11 @@ impl UCanonical { } impl UCanonical> { -<<<<<<< HEAD - /// A goal has coinductive semantics if it is of the form `T: AutoTrait`. - crate fn is_coinductive(&self, program: &ProgramEnvironment) -> bool { -======= /// A goal has coinductive semantics if it is of the form `T: AutoTrait`, or if it is of the /// form `WellFormed(T: Trait)` where `Trait` is any trait. The latter is needed for dealing /// with WF requirements and cyclic traits, which generates cycles in the proof tree which must /// not be rejected but instead must be treated as a success. - pub fn is_coinductive(&self, program: &ProgramEnvironment) -> bool { ->>>>>>> Add documentation + crate fn is_coinductive(&self, program: &ProgramEnvironment) -> bool { match &self.canonical.value.goal { Goal::Leaf(LeafGoal::DomainGoal(DomainGoal::Implemented(tr))) => { let trait_datum = &program.trait_data[&tr.trait_id]; diff --git a/src/lower/mod.rs b/src/lower/mod.rs index a3e98bb1240..0f0dc552e4a 100644 --- a/src/lower/mod.rs +++ b/src/lower/mod.rs @@ -1387,8 +1387,7 @@ impl ir::AssociatedTyDatum { // particular, whenever normalization is possible, we cannot // solve that projection uniquely, since we can now elaborate // `ProjectionEq` to fallback *or* normalize it. So instead we - // handle this kind of reasoning by expanding "projection - // equality" predicates (see `DomainGoal::expanded`). + // handle this kind of reasoning through the `FromEnv` predicate. // // We also generate rules specific to WF requirements and implied bounds, // see below. diff --git a/src/lower/test.rs b/src/lower/test.rs index 2262ea1567c..d5decf74f33 100755 --- a/src/lower/test.rs +++ b/src/lower/test.rs @@ -32,9 +32,9 @@ macro_rules! lowering_error { fn parse_and_lower(text: &str) -> Result { - // Use the on-demand SLG solver to avoid ambiguities on projection types encountered when - // using the recursive solver. - chalk_parse::parse_program(text)?.lower(SolverChoice::on_demand_slg()) + // FIXME: Use the SLG solver to avoid ambiguities on projection types encountered + // when using the recursive solver. + chalk_parse::parse_program(text)?.lower(SolverChoice::slg()) } fn parse_and_lower_goal(program: &Program, text: &str) -> Result> { @@ -575,7 +575,6 @@ fn ill_formed_trait_decl() { } } } - #[test] fn cyclic_traits() { lowering_success! { @@ -587,10 +586,7 @@ fn cyclic_traits() { impl A for T { } } } -} -#[test] -fn cyclic_traits_error() { lowering_error! { program { trait Copy { } @@ -598,12 +594,26 @@ fn cyclic_traits_error() { trait A where Self: B, Self: Copy {} trait B where Self: A { } + // This impl won't be able to prove that `T: Copy` holds. impl B for T {} + impl A for T where T: B {} } error_msg { "trait impl for \"B\" does not meet well-formedness requirements" } } + + lowering_success! { + program { + trait Copy { } + + trait A where Self: B, Self: Copy {} + trait B where Self: A { } + + impl B for T where T: Copy {} + impl A for T where T: B {} + } + } } #[test] @@ -636,6 +646,7 @@ fn ill_formed_assoc_ty() { } impl Bar for i32 { + // `OnlyFoo` is ill-formed because `i32: Foo` does not hold. type Value = OnlyFoo; } } error_msg { @@ -660,6 +671,7 @@ fn implied_bounds() { } impl Foo for Set { + // Here, `WF(Set)` implies `K: Hash` and hence `OnlyEq` is WF. type Value = OnlyEq; } } @@ -710,6 +722,8 @@ fn wf_requiremements_for_projection() { } impl Foo for T { + // The projection is well-formed if `T: Iterator` holds, which cannot + // be proved here. type Value = ::Item; } } error_msg { @@ -744,6 +758,8 @@ fn projection_type_in_header() { trait Bar { } + // 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 { } } error_msg { "trait impl for \"Bar\" does not meet well-formedness requirements" diff --git a/src/lower/wf.rs b/src/lower/wf.rs index 355a5065c63..58a2efddf9d 100644 --- a/src/lower/wf.rs +++ b/src/lower/wf.rs @@ -13,7 +13,7 @@ struct WfSolver { impl Program { pub fn verify_well_formedness(&self, solver_choice: SolverChoice) -> Result<()> { - set_current_program(&Arc::new(self.clone()), || self.solve_wf_requirements(solver_choice)) + tls::set_current_program(&Arc::new(self.clone()), || self.solve_wf_requirements(solver_choice)) } fn solve_wf_requirements(&self, solver_choice: SolverChoice) -> Result<()> { @@ -79,9 +79,15 @@ impl FoldInputTypes for Ty { proj.parameters.fold(accumulator); } - // Type parameters and higher-kinded types do not carry any input types (so we can sort - // of assume they are always WF). - Ty::Var(..) | Ty::ForAll(..) => (), + // Type parameters do not carry any input types (so we can sort of assume they are + // always WF). + Ty::Var(..) => (), + + // Higher-kinded types such as `for<'a> fn(&'a u32)` introduce their own implied + // bounds, and these bounds will be enforced upon calling such a function. In some + // sense, well-formedness requirements for the input types of an HKT will be enforced + // lazily, so no need to include them here. + Ty::ForAll(..) => (), } } } @@ -244,7 +250,7 @@ impl WfSolver { .map(|ty| WellFormed::Ty(ty).cast()) .chain(assoc_ty_goals) .chain(Some(WellFormed::TraitRef(trait_ref.clone())).cast()); - + let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))) .expect("at least one goal"); diff --git a/src/solve/test/mod.rs b/src/solve/test/mod.rs index ee263dcc641..e794df0ecee 100644 --- a/src/solve/test/mod.rs +++ b/src/solve/test/mod.rs @@ -14,7 +14,7 @@ fn parse_and_lower_program(text: &str, solver_choice: SolverChoice, skip_coheren -> Result { if skip_coherence { - // We disable WF checks for the recursive solver, because of ambiguities appearing + // FIXME: We disable WF checks for the recursive solver, because of ambiguities appearing // with projection types. chalk_parse::parse_program(text)?.lower_without_coherence() } else { From 4bac24700753db2946a8f0374b838cb4d0e125da Mon Sep 17 00:00:00 2001 From: scalexm Date: Tue, 6 Feb 2018 21:43:59 +0100 Subject: [PATCH 06/10] Elaborate implied bounds in `if` goals --- src/lower/mod.rs | 25 +++++++++++++++---------- src/solve/test/mod.rs | 13 +++++-------- 2 files changed, 20 insertions(+), 18 deletions(-) diff --git a/src/lower/mod.rs b/src/lower/mod.rs index 0f0dc552e4a..c3e9b8b0117 100644 --- a/src/lower/mod.rs +++ b/src/lower/mod.rs @@ -479,18 +479,14 @@ impl LowerWhereClause for WhereClause { Ok(match *self { WhereClause::Implemented { .. } | WhereClause::ProjectionEq { .. } - | WhereClause::Normalize { .. } => { + | WhereClause::Normalize { .. } + | WhereClause::TyWellFormed { .. } + | WhereClause::TraitRefWellFormed { .. } + | WhereClause::TyFromEnv { .. } + | WhereClause::TraitRefFromEnv { .. } => { let g: ir::DomainGoal = self.lower(env)?; g.cast() } - WhereClause::TyWellFormed { ref ty } => ir::WellFormed::Ty(ty.lower(env)?).cast(), - WhereClause::TraitRefWellFormed { ref trait_ref } => { - ir::WellFormed::TraitRef(trait_ref.lower(env)?).cast() - } - WhereClause::TyFromEnv { ref ty } => ir::FromEnv::Ty(ty.lower(env)?).cast(), - WhereClause::TraitRefFromEnv { ref trait_ref } => { - ir::FromEnv::TraitRef(trait_ref.lower(env)?).cast() - } WhereClause::UnifyTys { ref a, ref b } => ir::EqGoal { a: ir::ParameterKind::Ty(a.lower(env)?), b: ir::ParameterKind::Ty(b.lower(env)?), @@ -936,7 +932,16 @@ impl<'k> LowerGoal> for Goal { g.lower_quantified(env, ir::QuantifierKind::Exists, ids) } Goal::Implies(ref wc, ref g) => { - Ok(Box::new(ir::Goal::Implies(wc.lower(env)?, g.lower(env)?))) + // We "elaborate" implied bounds by lowering goals like `T: Trait` and + // `T: Trait` to `FromEnv(T: Trait)` and `FromEnv(T: Trait)` + // in the assumptions of an `if` goal, e.g. `if (T: Trait) { ... }` lowers to + // `if (FromEnv(T: Trait)) { ... /* this part is untouched */ ... }`. + let where_clauses = + wc.lower(env)? + .into_iter() + .map(|wc| wc.into_from_env_clause()) + .collect(); + Ok(Box::new(ir::Goal::Implies(where_clauses, g.lower(env)?))) } Goal::And(ref g1, ref g2) => { Ok(Box::new(ir::Goal::And(g1.lower(env)?, g2.lower(env)?))) diff --git a/src/solve/test/mod.rs b/src/solve/test/mod.rs index e794df0ecee..e4a9bdd9466 100644 --- a/src/solve/test/mod.rs +++ b/src/solve/test/mod.rs @@ -1157,10 +1157,9 @@ fn suggested_subst() { Foo: SomeTrait } } - } yields[SolverChoice::recursive()] { - "Ambiguous; suggested substitution [?0 := bool]" - } yields[SolverChoice::slg()] { - // FIXME: SLG does not impl the logic to privilege where clauses + } yields { + // FIXME: we need to rework the "favor environment" heuristic. + // Should be: "Ambiguous; suggested substitution [?0 := bool]" "Ambiguous; no inference guidance" } @@ -1190,10 +1189,8 @@ fn suggested_subst() { Bar: SomeTrait } } - } yields[SolverChoice::recursive()] { - "Ambiguous; suggested substitution [?0 := bool]" - } yields[SolverChoice::slg()] { - // FIXME: SLG does not impl the logic to privilege where clauses + } yields { + // FIXME: same as above, should be: "Ambiguous; suggested substitution [?0 := bool]" "Ambiguous; no inference guidance" } From 432c2ecc3fff3372b0e2de8fac4f52eba71a771c Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Thu, 8 Feb 2018 04:30:46 -0500 Subject: [PATCH 07/10] fix comment --- src/lower/mod.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/lower/mod.rs b/src/lower/mod.rs index c3e9b8b0117..43c0a0e6018 100644 --- a/src/lower/mod.rs +++ b/src/lower/mod.rs @@ -1308,8 +1308,9 @@ impl ir::TraitDatum { // } // // and the reverse rules: + // // forall { (Self: Ord) :- FromEnv(Self: Ord) } - // forall { FromEnv(Self: Ord) :- FromEnv(Self: Ord) } + // forall { FromEnv(Self: Eq) :- FromEnv(Self: Ord) } let trait_ref = self.binders.value.trait_ref.clone(); From 4506e42f141a3aeb9bc690666dbb202986dcde63 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Thu, 8 Feb 2018 04:30:50 -0500 Subject: [PATCH 08/10] fix test; we now create some `FromEnv` goals first I guess --- src/solve/slg/on_demand/test.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solve/slg/on_demand/test.rs b/src/solve/slg/on_demand/test.rs index d9ba901255c..388eebaa772 100644 --- a/src/solve/slg/on_demand/test.rs +++ b/src/solve/slg/on_demand/test.rs @@ -694,7 +694,7 @@ fn example_3_3_EWFS() { TableIndex(1) ), Negative( - TableIndex(2) + TableIndex(4) ) ] } From 91eda35062d6a75c8bb3ac0c1459eb5b7b6af599 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Thu, 8 Feb 2018 04:35:12 -0500 Subject: [PATCH 09/10] WIP add test I expect to pass --- src/solve/test/mod.rs | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/solve/test/mod.rs b/src/solve/test/mod.rs index e4a9bdd9466..2e39d7e9511 100644 --- a/src/solve/test/mod.rs +++ b/src/solve/test/mod.rs @@ -563,6 +563,28 @@ fn normalize_basic() { } } +#[test] +fn normalize_implied_bound() { + test! { + program { + trait Clone { } + trait Iterator where Self: Clone { type Item; } + struct u32 { } + } + + goal { + forall { + if (T: Iterator) { + T: Clone + } + } + } yields { + "Unique; substitution []" + } + } +} + + /// Demonstrates that, given the expected value of the associated /// type, we can use that to narrow down the relevant impls. #[test] From 249bd61e251e7297dc82c5017045d9b00091823d Mon Sep 17 00:00:00 2001 From: scalexm Date: Thu, 8 Feb 2018 11:58:01 +0100 Subject: [PATCH 10/10] Change `WellFormed/FromEnv::Normalize` to `WellFormed/FromEnv::ProjectionEq` --- src/fold/mod.rs | 4 ++-- src/ir/debug.rs | 4 ++-- src/ir/mod.rs | 8 ++++---- src/lower/mod.rs | 24 ++++++++++++------------ src/zip.rs | 4 ++-- 5 files changed, 22 insertions(+), 22 deletions(-) diff --git a/src/fold/mod.rs b/src/fold/mod.rs index 3afc6e14ec8..832b9eba23d 100644 --- a/src/fold/mod.rs +++ b/src/fold/mod.rs @@ -405,8 +405,8 @@ macro_rules! enum_fold { enum_fold!(PolarizedTraitRef[] { Positive(a), Negative(a) }); enum_fold!(ParameterKind[T,L] { Ty(a), Lifetime(a) } where T: Fold, L: Fold); enum_fold!(DomainGoal[] { Implemented(a), ProjectionEq(a), Normalize(a), UnselectedNormalize(a), WellFormed(a), FromEnv(a), InScope(a) }); -enum_fold!(WellFormed[] { Ty(a), TraitRef(a), Normalize(a) }); -enum_fold!(FromEnv[] { Ty(a), TraitRef(a), Normalize(a) }); +enum_fold!(WellFormed[] { Ty(a), TraitRef(a), ProjectionEq(a) }); +enum_fold!(FromEnv[] { Ty(a), TraitRef(a), ProjectionEq(a) }); enum_fold!(LeafGoal[] { EqGoal(a), DomainGoal(a) }); enum_fold!(Constraint[] { LifetimeEq(a, b) }); enum_fold!(Goal[] { Quantified(qkind, subgoal), Implies(wc, subgoal), And(g1, g2), Not(g), Leaf(wc), diff --git a/src/ir/debug.rs b/src/ir/debug.rs index b4941e9e0e4..6ed5362a331 100644 --- a/src/ir/debug.rs +++ b/src/ir/debug.rs @@ -202,7 +202,7 @@ impl Debug for WellFormed { let value: &Debug = match *self { WellFormed::Ty(ref t) => t, WellFormed::TraitRef(ref t) => t, - WellFormed::Normalize(ref t) => t, + WellFormed::ProjectionEq(ref t) => t, }; write!(fmt, "WellFormed({:?})", value) } @@ -213,7 +213,7 @@ impl Debug for FromEnv { let value: &Debug = match *self { FromEnv::Ty(ref t) => t, FromEnv::TraitRef(ref t) => t, - FromEnv::Normalize(ref t) => t, + FromEnv::ProjectionEq(ref t) => t, }; write!(fmt, "FromEnv({:?})", value) } diff --git a/src/ir/mod.rs b/src/ir/mod.rs index 3ce09c739df..585a58cc929 100644 --- a/src/ir/mod.rs +++ b/src/ir/mod.rs @@ -476,7 +476,7 @@ impl DomainGoal { crate fn into_well_formed_clause(self) -> DomainGoal { match self { DomainGoal::Implemented(tr) => DomainGoal::WellFormed(WellFormed::TraitRef(tr)), - DomainGoal::Normalize(n) => DomainGoal::WellFormed(WellFormed::Normalize(n)), + DomainGoal::ProjectionEq(n) => DomainGoal::WellFormed(WellFormed::ProjectionEq(n)), goal => goal, } } @@ -485,7 +485,7 @@ impl DomainGoal { crate fn into_from_env_clause(self) -> DomainGoal { match self { DomainGoal::Implemented(tr) => DomainGoal::FromEnv(FromEnv::TraitRef(tr)), - DomainGoal::Normalize(n) => DomainGoal::FromEnv(FromEnv::Normalize(n)), + DomainGoal::ProjectionEq(n) => DomainGoal::FromEnv(FromEnv::ProjectionEq(n)), goal => goal, } } @@ -521,7 +521,7 @@ pub struct EqGoal { pub enum WellFormed { Ty(Ty), TraitRef(TraitRef), - Normalize(Normalize), + ProjectionEq(ProjectionEq), } #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)] @@ -547,7 +547,7 @@ pub enum WellFormed { pub enum FromEnv { Ty(Ty), TraitRef(TraitRef), - Normalize(Normalize), + ProjectionEq(ProjectionEq), } /// Proves that the given projection **normalizes** to the given diff --git a/src/lower/mod.rs b/src/lower/mod.rs index 43c0a0e6018..401875db9b8 100644 --- a/src/lower/mod.rs +++ b/src/lower/mod.rs @@ -1468,6 +1468,9 @@ impl ir::AssociatedTyDatum { // `Normalize(::Assoc -> U)` let normalize = ir::Normalize { projection: projection.clone(), ty: ty.clone() }; + // `ProjectionEq(::Assoc = U)` + let projection_eq = ir::ProjectionEq { projection: projection.clone(), ty }; + // forall { // ProjectionEq(::Assoc = U) :- // Normalize(::Assoc -> U) @@ -1476,10 +1479,7 @@ impl ir::AssociatedTyDatum { implication: ir::Binders { binders: binders.clone(), value: ir::ProgramClauseImplication { - consequence: ir::ProjectionEq { - projection: projection.clone(), - ty, - }.cast(), + consequence: projection_eq.clone().cast(), conditions: vec![normalize.clone().cast()], }, }, @@ -1492,16 +1492,16 @@ impl ir::AssociatedTyDatum { // // forall { // WellFormed(T: Foo) :- - // WellFormed(T: Foo), Normalize(::Assoc -> U) + // WellFormed(T: Foo), ProjectionEq(::Assoc = U) // } clauses.push(ir::ProgramClause { implication: ir::Binders { binders: binders.clone(), value: ir::ProgramClauseImplication { - consequence: ir::WellFormed::Normalize(normalize.clone()).cast(), + consequence: ir::WellFormed::ProjectionEq(projection_eq.clone()).cast(), conditions: vec![ - normalize.clone().cast(), - ir::WellFormed::TraitRef(trait_ref.clone()).cast() + ir::WellFormed::TraitRef(trait_ref.clone()).cast(), + projection_eq.clone().cast() ], } } @@ -1517,7 +1517,7 @@ impl ir::AssociatedTyDatum { binders: binders.clone(), value: ir::ProgramClauseImplication { consequence: ir::FromEnv::TraitRef(trait_ref).cast(), - conditions: vec![ir::FromEnv::Normalize(normalize.clone()).cast()], + conditions: vec![ir::FromEnv::ProjectionEq(projection_eq.clone()).cast()], }, } }); @@ -1525,14 +1525,14 @@ impl ir::AssociatedTyDatum { // And the other one being: // // forall { - // Normalize(::Assoc -> U) :- FromEnv(T: Foo) + // ProjectionEq(::Assoc = U) :- FromEnv(T: Foo) // } clauses.push(ir::ProgramClause { implication: ir::Binders { binders: binders, value: ir::ProgramClauseImplication { - consequence: normalize.clone().cast(), - conditions: vec![ir::FromEnv::Normalize(normalize).cast()], + consequence: projection_eq.clone().cast(), + conditions: vec![ir::FromEnv::ProjectionEq(projection_eq).cast()], }, } }); diff --git a/src/zip.rs b/src/zip.rs index af14b21e3d2..36b49ffa940 100644 --- a/src/zip.rs +++ b/src/zip.rs @@ -224,8 +224,8 @@ enum_zip!(DomainGoal { InScope, }); enum_zip!(LeafGoal { DomainGoal, EqGoal }); -enum_zip!(WellFormed { Ty, TraitRef, Normalize }); -enum_zip!(FromEnv { Ty, TraitRef, Normalize }); +enum_zip!(WellFormed { Ty, TraitRef, ProjectionEq }); +enum_zip!(FromEnv { Ty, TraitRef, ProjectionEq }); // Annoyingly, Goal cannot use `enum_zip` because some variants have // two parameters, and I'm too lazy to make the macro account for the