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))