From e0d0490d3c83cb3405cc6f981ccb8f6c978053c6 Mon Sep 17 00:00:00 2001 From: Nathan Whitaker Date: Wed, 22 Jul 2020 12:53:49 -0400 Subject: [PATCH 1/4] Check well-formedness of opaque type declarations --- chalk-integration/src/query.rs | 4 ++ chalk-solve/src/wf.rs | 70 ++++++++++++++++++++++++++++++++++ 2 files changed, 74 insertions(+) diff --git a/chalk-integration/src/query.rs b/chalk-integration/src/query.rs index d60858505fc..f7633e2a08c 100644 --- a/chalk-integration/src/query.rs +++ b/chalk-integration/src/query.rs @@ -177,6 +177,10 @@ fn checked_program(db: &dyn LoweringDatabase) -> Result, ChalkError solver.verify_adt_decl(id)?; } + for &opaque_ty_id in program.opaque_ty_data.keys() { + solver.verify_opaque_ty_decl(opaque_ty_id)?; + } + for &impl_id in program.impl_data.keys() { solver.verify_trait_impl(impl_id)?; } diff --git a/chalk-solve/src/wf.rs b/chalk-solve/src/wf.rs index 03c60e66daa..057f4a20f62 100644 --- a/chalk-solve/src/wf.rs +++ b/chalk-solve/src/wf.rs @@ -16,6 +16,7 @@ use tracing::debug; #[derive(Debug)] pub enum WfError { IllFormedTypeDecl(chalk_ir::AdtId), + IllFormedOpaqueTypeDecl(chalk_ir::OpaqueTyId), IllFormedTraitImpl(chalk_ir::TraitId), } @@ -27,6 +28,11 @@ impl fmt::Display for WfError { "type declaration `{:?}` does not meet well-formedness requirements", id ), + WfError::IllFormedOpaqueTypeDecl(id) => write!( + f, + "opaque type declaration `{:?}` does not meet well-formedness requirements", + id + ), WfError::IllFormedTraitImpl(id) => write!( f, "trait impl for `{:?}` does not meet well-formedness requirements", @@ -262,6 +268,70 @@ where Err(WfError::IllFormedTraitImpl(trait_id)) } } + + pub fn verify_opaque_ty_decl(&self, opaque_ty_id: OpaqueTyId) -> Result<(), WfError> { + // Given an opaque type like + // ```notrust + // opaque type Foo: Clone where T: Bar = Baz; + // ``` + let interner = self.db.interner(); + + let mut gb = GoalBuilder::new(self.db); + + let datum = self.db.opaque_ty_data(opaque_ty_id); + let bound = &datum.bound; + + // We make a goal like + // + // forall + let goal = gb.forall(&bound, opaque_ty_id, |gb, _, bound, opaque_ty_id| { + // exists + gb.exists( + &bound.where_clauses, + (opaque_ty_id, &bound.bounds), + |gb, _, where_clauses, (opaque_ty_id, bounds)| { + let interner = gb.interner(); + let clauses = where_clauses + .iter() + .cloned() + .map(|wc| wc.into_from_env_goal(interner)); + let subst = + Substitution::from1(interner, gb.db().hidden_opaque_type(opaque_ty_id)); + + // if (WellFormed(T: Bar)) + gb.implies(clauses, |gb| { + let interner = gb.interner(); + + // all(WellFormed(Baz: Clone)) + gb.all( + bounds + .substitute(interner, &subst) + .iter() + .cloned() + .map(|b| b.into_well_formed_goal(interner)), + ) + }) + }, + ) + }); + + debug!("WF opaque type goal: {:#?}", goal); + + let is_legal = match self + .solver_choice + .into() + .solve(self.db, &goal.into_closed_goal(interner)) + { + Some(sol) => sol.is_unique(), + None => false, + }; + + if is_legal { + Ok(()) + } else { + Err(WfError::IllFormedOpaqueTypeDecl(opaque_ty_id)) + } + } } fn impl_header_wf_goal( From c0b0be82c2bf4912b8ceb24bf65f61f317bb64ee Mon Sep 17 00:00:00 2001 From: Nathan Whitaker Date: Wed, 22 Jul 2020 12:54:27 -0400 Subject: [PATCH 2/4] Update tests --- tests/test/opaque_types.rs | 16 ++++++++++++++++ tests/test/wf_lowering.rs | 14 ++++++++++++++ 2 files changed, 30 insertions(+) diff --git a/tests/test/opaque_types.rs b/tests/test/opaque_types.rs index 6ef9c0a9c07..1ee115888f0 100644 --- a/tests/test/opaque_types.rs +++ b/tests/test/opaque_types.rs @@ -7,6 +7,9 @@ fn opaque_bounds() { struct Ty { } trait Clone { } + + impl Clone for Ty { } + opaque type T: Clone = Ty; } @@ -27,6 +30,7 @@ fn opaque_reveal() { impl Trait for Ty { } trait Clone { } + impl Clone for Ty { } opaque type T: Clone = Ty; } @@ -53,11 +57,16 @@ fn opaque_where_clause() { struct Ty { } trait Clone { } + impl Clone for Ty { } + trait Trait { } impl Trait for Ty { } + opaque type T: Clone where T: Trait = Ty; struct Vec { } + + impl Clone for Vec { } impl Trait for Vec { } opaque type S: Clone where U: Trait = Vec; @@ -130,6 +139,10 @@ fn opaque_generics() { struct Vec { } struct Bar { } + impl Iterator for Vec { + type Item = T; + } + opaque type Foo: Iterator = Vec; } @@ -167,6 +180,9 @@ fn opaque_auto_traits() { struct Baz { } trait Trait { } + impl Trait for Bar { } + impl Trait for Baz { } + #[auto] trait Send { } diff --git a/tests/test/wf_lowering.rs b/tests/test/wf_lowering.rs index 754227c73ec..83f2c4e3f45 100644 --- a/tests/test/wf_lowering.rs +++ b/tests/test/wf_lowering.rs @@ -1103,3 +1103,17 @@ fn no_unsize_impls() { } } } + +#[test] +fn ill_formed_opaque_ty() { + lowering_error! { + program { + trait Foo {} + struct Bar {} + + opaque type T: Foo = Bar; + } error_msg { + "opaque type declaration `T` does not meet well-formedness requirements" + } + } +} From 4642c4664cb1e228c6d08d85576c810177b0de36 Mon Sep 17 00:00:00 2001 From: Nathan Whitaker Date: Fri, 31 Jul 2020 14:31:27 -0400 Subject: [PATCH 3/4] Substitute hidden type for `Self` --- chalk-solve/src/wf.rs | 48 ++++++++++++++++++--------------------- tests/test/wf_lowering.rs | 12 ++++++++++ 2 files changed, 34 insertions(+), 26 deletions(-) diff --git a/chalk-solve/src/wf.rs b/chalk-solve/src/wf.rs index 057f4a20f62..76bbd6e7c2a 100644 --- a/chalk-solve/src/wf.rs +++ b/chalk-solve/src/wf.rs @@ -285,34 +285,30 @@ where // // forall let goal = gb.forall(&bound, opaque_ty_id, |gb, _, bound, opaque_ty_id| { - // exists - gb.exists( - &bound.where_clauses, - (opaque_ty_id, &bound.bounds), - |gb, _, where_clauses, (opaque_ty_id, bounds)| { - let interner = gb.interner(); - let clauses = where_clauses - .iter() - .cloned() - .map(|wc| wc.into_from_env_goal(interner)); - let subst = - Substitution::from1(interner, gb.db().hidden_opaque_type(opaque_ty_id)); + let interner = gb.interner(); - // if (WellFormed(T: Bar)) - gb.implies(clauses, |gb| { - let interner = gb.interner(); + let subst = Substitution::from1(interner, gb.db().hidden_opaque_type(opaque_ty_id)); - // all(WellFormed(Baz: Clone)) - gb.all( - bounds - .substitute(interner, &subst) - .iter() - .cloned() - .map(|b| b.into_well_formed_goal(interner)), - ) - }) - }, - ) + let bounds = bound.bounds.substitute(interner, &subst); + let where_clauses = bound.where_clauses.substitute(interner, &subst); + + let clauses = where_clauses + .iter() + .cloned() + .map(|wc| wc.into_from_env_goal(interner)); + + // if (WellFormed(T: Bar)) + gb.implies(clauses, |gb| { + let interner = gb.interner(); + + // all(WellFormed(Baz: Clone)) + gb.all( + bounds + .iter() + .cloned() + .map(|b| b.into_well_formed_goal(interner)), + ) + }) }); debug!("WF opaque type goal: {:#?}", goal); diff --git a/tests/test/wf_lowering.rs b/tests/test/wf_lowering.rs index 83f2c4e3f45..9943238ec97 100644 --- a/tests/test/wf_lowering.rs +++ b/tests/test/wf_lowering.rs @@ -1116,4 +1116,16 @@ fn ill_formed_opaque_ty() { "opaque type declaration `T` does not meet well-formedness requirements" } } + + lowering_error! { + program { + trait Foo { } + struct NotFoo { } + struct IsFoo { } + impl Foo for IsFoo { } + opaque type T: Foo = NotFoo; + } error_msg { + "opaque type declaration `T` does not meet well-formedness requirements" + } + } } From 22963e27bdd89ae70473c76204ce2f8f290c9ab5 Mon Sep 17 00:00:00 2001 From: Nathan Whitaker Date: Thu, 3 Sep 2020 17:42:25 -0400 Subject: [PATCH 4/4] Fixup --- chalk-solve/src/wf.rs | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/chalk-solve/src/wf.rs b/chalk-solve/src/wf.rs index 76bbd6e7c2a..bd2179e9539 100644 --- a/chalk-solve/src/wf.rs +++ b/chalk-solve/src/wf.rs @@ -313,11 +313,8 @@ where debug!("WF opaque type goal: {:#?}", goal); - let is_legal = match self - .solver_choice - .into() - .solve(self.db, &goal.into_closed_goal(interner)) - { + let mut new_solver = (self.solver_builder)(); + let is_legal = match new_solver.solve(self.db, &goal.into_closed_goal(interner)) { Some(sol) => sol.is_unique(), None => false, };