From 2a9067199483fb236f04be8927c6a776f66a27c8 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Sun, 26 Apr 2020 13:20:56 +0200 Subject: [PATCH] Make `dyn Trait` implement its super traits as well This implements the impl rules from #203, as far as I understood them. It doesn't do the well-formedness or object safety rules. --- chalk-integration/src/lowering.rs | 3 +- chalk-ir/src/lib.rs | 99 ++++++++++++++++ chalk-rust-ir/src/lib.rs | 50 +++----- chalk-solve/src/clauses.rs | 81 +++---------- chalk-solve/src/clauses/builder.rs | 1 - chalk-solve/src/clauses/dyn_ty.rs | 181 +++++++++++++++++++++++++++++ chalk-solve/src/goal_builder.rs | 1 - tests/test/existential_types.rs | 123 ++++++++++++++++++++ 8 files changed, 430 insertions(+), 109 deletions(-) create mode 100644 chalk-solve/src/clauses/dyn_ty.rs diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index 97e680998c9..031b8e72987 100644 --- a/chalk-integration/src/lowering.rs +++ b/chalk-integration/src/lowering.rs @@ -2,13 +2,12 @@ use chalk_ir::cast::{Cast, Caster}; use chalk_ir::interner::{ChalkIr, HasInterner}; use chalk_ir::{ self, AssocTypeId, BoundVar, ClausePriority, DebruijnIndex, ImplId, OpaqueTyId, ParameterKinds, - QuantifiedWhereClauses, StructId, Substitution, TraitId, + QuantifiedWhereClauses, StructId, Substitution, ToParameter, TraitId, }; use chalk_parse::ast::*; use chalk_rust_ir as rust_ir; use chalk_rust_ir::{ Anonymize, AssociatedTyValueId, IntoWhereClauses, OpaqueTyDatum, OpaqueTyDatumBound, - ToParameter, }; use lalrpop_intern::intern; use std::collections::BTreeMap; diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index b7a2db0fe3c..f05db48da7e 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -1250,6 +1250,14 @@ impl Binders { Self { binders, value } } + /// Wraps the given value in a binder without variables, i.e. `for<> + /// (value)`. Since our deBruijn indices count binders, not variables, this + /// is sometimes useful. + pub fn empty(interner: &T::Interner, value: T) -> Self { + let binders = ParameterKinds::new(interner); + Self { binders, value } + } + /// Skips the binder and returns the "bound" value. This is a /// risky thing to do because it's easy to get confused about /// De Bruijn indices and the like. `skip_binder` is only valid @@ -1287,6 +1295,20 @@ impl Binders { } } + /// Transforms the inner value according to the given function; returns + /// `None` if the function returns `None`. + pub fn filter_map(self, op: OP) -> Option> + where + OP: FnOnce(T) -> Option, + U: HasInterner, + { + let value = op(self.value)?; + Some(Binders { + binders: self.binders, + value, + }) + } + pub fn map_ref<'a, U, OP>(&'a self, op: OP) -> Binders where OP: FnOnce(&'a T) -> U, @@ -1295,6 +1317,19 @@ impl Binders { self.as_ref().map(op) } + /// Creates a `Substitution` containing bound vars such that applying this + /// substitution will not change the value, i.e. `^0.0, ^0.1, ^0.2` and so + /// on. + pub fn identity_substitution(&self, interner: &T::Interner) -> Substitution { + Substitution::from( + interner, + self.binders + .iter(interner) + .enumerate() + .map(|(i, pk)| (pk, i).to_parameter(interner)), + ) + } + /// Creates a fresh binders that contains a single type /// variable. The result of the closure will be embedded in this /// binder. Note that you should be careful with what you return @@ -1317,6 +1352,36 @@ impl Binders { } } +impl Binders> +where + T: Fold + HasInterner, + T::Result: HasInterner, + I: Interner, +{ + /// This turns two levels of binders (`for for`) into one level (`for`). + pub fn fuse_binders(self, interner: &T::Interner) -> Binders { + let num_binders = self.len(interner); + // generate a substitution to shift the indexes of the inner binder: + let subst = Substitution::from( + interner, + self.value + .binders + .iter(interner) + .enumerate() + .map(|(i, pk)| (pk, i + num_binders).to_parameter(interner)), + ); + let value = self.value.substitute(interner, &subst); + let binders = ParameterKinds::from( + interner, + self.binders + .iter(interner) + .chain(self.value.binders.iter(interner)) + .cloned(), + ); + Binders { binders, value } + } +} + impl From> for (ParameterKinds, T) { fn from(binders: Binders) -> Self { (binders.binders, binders.value) @@ -2073,6 +2138,40 @@ where } } +pub trait ToParameter { + /// Utility for converting a list of all the binders into scope + /// into references to those binders. Simply pair the binders with + /// the indices, and invoke `to_parameter()` on the `(binder, + /// index)` pair. The result will be a reference to a bound + /// variable of appropriate kind at the corresponding index. + fn to_parameter(&self, interner: &I) -> Parameter { + self.to_parameter_at_depth(interner, DebruijnIndex::INNERMOST) + } + + fn to_parameter_at_depth( + &self, + interner: &I, + debruijn: DebruijnIndex, + ) -> Parameter; +} + +impl<'a> ToParameter for (&'a ParameterKind<()>, usize) { + fn to_parameter_at_depth( + &self, + interner: &I, + debruijn: DebruijnIndex, + ) -> Parameter { + let &(binder, index) = self; + let bound_var = BoundVar::new(debruijn, index); + match *binder { + ParameterKind::Lifetime(_) => LifetimeData::BoundVar(bound_var) + .intern(interner) + .cast(interner), + ParameterKind::Ty(_) => TyData::BoundVar(bound_var).intern(interner).cast(interner), + } + } +} + impl<'i, I: Interner> Folder<'i, I> for &SubstFolder<'i, I> { fn as_dyn(&mut self) -> &mut dyn Folder<'i, I> { self diff --git a/chalk-rust-ir/src/lib.rs b/chalk-rust-ir/src/lib.rs index c5c688d7810..eca8416effb 100644 --- a/chalk-rust-ir/src/lib.rs +++ b/chalk-rust-ir/src/lib.rs @@ -9,9 +9,9 @@ use chalk_ir::cast::Cast; use chalk_ir::fold::shift::Shift; use chalk_ir::interner::{Interner, TargetInterner}; use chalk_ir::{ - AliasEq, AliasTy, AssocTypeId, Binders, BoundVar, DebruijnIndex, ImplId, LifetimeData, - OpaqueTyId, Parameter, ParameterKind, ProjectionTy, QuantifiedWhereClause, StructId, - Substitution, TraitId, TraitRef, Ty, TyData, TypeName, WhereClause, + AliasEq, AliasTy, AssocTypeId, Binders, DebruijnIndex, ImplId, OpaqueTyId, Parameter, + ParameterKind, ProjectionTy, QuantifiedWhereClause, StructId, Substitution, ToParameter, + TraitId, TraitRef, Ty, TyData, TypeName, WhereClause, }; use std::iter; @@ -167,6 +167,16 @@ impl TraitDatum { pub fn is_coinductive_trait(&self) -> bool { self.flags.coinductive } + + /// Gives access to the where clauses of the trait, quantified over the type parameters of the trait: + /// + /// ```ignore + /// trait Foo where T: Debug { } + /// ^^^^^^^^^^^^^^ + /// ``` + pub fn where_clauses(&self) -> Binders<&Vec>> { + self.binders.as_ref().map(|td| &td.where_clauses) + } } #[derive(Clone, Debug, PartialEq, Eq, Hash, HasInterner)] @@ -331,40 +341,6 @@ impl Anonymize for [ParameterKind] { } } -pub trait ToParameter { - /// Utility for converting a list of all the binders into scope - /// into references to those binders. Simply pair the binders with - /// the indices, and invoke `to_parameter()` on the `(binder, - /// index)` pair. The result will be a reference to a bound - /// variable of appropriate kind at the corresponding index. - fn to_parameter(&self, interner: &I) -> Parameter { - self.to_parameter_at_depth(interner, DebruijnIndex::INNERMOST) - } - - fn to_parameter_at_depth( - &self, - interner: &I, - debruijn: DebruijnIndex, - ) -> Parameter; -} - -impl<'a> ToParameter for (&'a ParameterKind<()>, usize) { - fn to_parameter_at_depth( - &self, - interner: &I, - debruijn: DebruijnIndex, - ) -> Parameter { - let &(binder, index) = self; - let bound_var = BoundVar::new(debruijn, index); - match *binder { - ParameterKind::Lifetime(_) => LifetimeData::BoundVar(bound_var) - .intern(interner) - .cast(interner), - ParameterKind::Ty(_) => TyData::BoundVar(bound_var).intern(interner).cast(interner), - } - } -} - /// Represents an associated type declaration found inside of a trait: /// /// ```notrust diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index 3c6ef4c1ed6..c87f430757c 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -12,6 +12,7 @@ use rustc_hash::FxHashSet; pub mod builder; mod builtin_traits; +mod dyn_ty; mod env_elaborator; mod generalize; pub mod program_clauses; @@ -198,76 +199,20 @@ fn program_clauses_that_could_match( } } - // If the self type `S` is a `dyn trait` type, we wish to generate program-clauses - // that indicates that it implements its own traits. For example, a `dyn Write` type - // implements `Write` and so on. + // If the self type is a `dyn trait` type, generate program-clauses + // that indicates that it implements its own traits. + // FIXME: This is presently rather wasteful, in that we don't check that the + // these program clauses we are generating are actually relevant to the goal + // `goal` that we are actually *trying* to prove (though there is some later + // code that will screen out irrelevant stuff). // - // To see how this works, consider as an example the type `dyn Fn(&u8)`. This is - // really shorthand for `dyn for<'a> Fn<(&'a u8), Output = ()>`, and we represent - // that type as something like this: - // - // ``` - // dyn(exists { - // forall<'a> { Implemented(T: Fn<'a>) }, - // forall<'a> { AliasEq(>::Output, ()) }, - // }) - // ``` - // - // so what we will do is to generate one program clause - // for each of the conditions. Thus we get two program - // clauses: - // - // ``` - // forall<'a> { Implemented(dyn Fn(&u8): Fn<(&'a u8)>) } - // ``` - // - // and - // - // ``` - // forall<'a> { AliasEq(>::Output, ()) }, - // ``` - // - // FIXME. This is presently rather wasteful, in that we - // don't check that the these program clauses we are - // generating are actually relevant to the goal `goal` - // that we are actually *trying* to prove (though there is - // some later code that will screen out irrelevant - // stuff). - // - // In other words, in our example, if we were trying to - // prove `Implemented(dyn Fn(&u8): Clone)`, we would have - // generated two clauses that are totally irrelevant to - // that goal, because they let us prove other things but - // not `Clone`. + // In other words, if we were trying to prove `Implemented(dyn + // Fn(&u8): Clone)`, we would still generate two clauses that are + // totally irrelevant to that goal, because they let us prove other + // things but not `Clone`. let self_ty = trait_ref.self_type_parameter(interner); - if let TyData::Dyn(dyn_ty) = self_ty.data(interner) { - // In this arm, `self_ty` is the `dyn Fn(&u8)`, - // and `bounded_ty` is the `exists { .. }` - // clauses shown above. - - // Turn free BoundVars in the type into new existentials. E.g. - // we might get some `dyn Foo`, and we don't want to return - // a clause with a free variable. We can instead return a - // slightly more general clause by basically turning this into - // `exists dyn Foo`. - let generalized_dyn_ty = generalize::Generalize::apply(db.interner(), dyn_ty); - - builder.push_binders(&generalized_dyn_ty, |builder, dyn_ty| { - for exists_qwc in dyn_ty.bounds.map_ref(|r| r.iter(interner)) { - // Replace the `T` from `exists { .. }` with `self_ty`, - // yielding clases like - // - // ``` - // forall<'a> { Implemented(dyn Fn(&u8): Fn<(&'a u8)>) } - // ``` - let qwc = - exists_qwc.substitute(interner, &[self_ty.clone().cast(interner)]); - - builder.push_binders(&qwc, |builder, wc| { - builder.push_fact(wc); - }); - } - }); + if let TyData::Dyn(_) = self_ty.data(interner) { + dyn_ty::build_dyn_self_ty_clauses(db, builder, self_ty.clone()) } match self_ty.data(interner) { diff --git a/chalk-solve/src/clauses/builder.rs b/chalk-solve/src/clauses/builder.rs index 755e635041c..a7111c2fe4b 100644 --- a/chalk-solve/src/clauses/builder.rs +++ b/chalk-solve/src/clauses/builder.rs @@ -3,7 +3,6 @@ use crate::RustIrDatabase; use chalk_ir::fold::Fold; use chalk_ir::interner::{HasInterner, Interner}; use chalk_ir::*; -use chalk_rust_ir::*; use std::marker::PhantomData; /// The "clause builder" is a useful tool for building up sets of diff --git a/chalk-solve/src/clauses/dyn_ty.rs b/chalk-solve/src/clauses/dyn_ty.rs new file mode 100644 index 00000000000..1343e1a2fd1 --- /dev/null +++ b/chalk-solve/src/clauses/dyn_ty.rs @@ -0,0 +1,181 @@ +use rustc_hash::FxHashSet; + +use super::{builder::ClauseBuilder, generalize}; +use crate::RustIrDatabase; +use chalk_ir::{ + cast::Cast, fold::shift::Shift, interner::Interner, Binders, BoundVar, DebruijnIndex, TraitId, + TraitRef, Ty, TyData, WhereClause, +}; + +/// If the self type `S` of an `Implemented` goal is a `dyn trait` type, we wish +/// to generate program-clauses that indicates that it implements its own +/// traits. For example, a `dyn Write` type implements `Write` and so on. +/// +/// To see how this works, consider as an example the type `dyn Fn(&u8)`. This +/// is really shorthand for `dyn for<'a> Fn<(&'a u8), Output = ()>`, and we +/// represent that type as something like this: +/// +/// ```ignore +/// dyn(exists { +/// forall<'a> { Implemented(T: Fn<'a>) }, +/// forall<'a> { AliasEq(>::Output, ()) }, +/// }) +/// ``` +/// +/// so what we will do is to generate one program clause for each of the +/// conditions. Thus we get two program clauses: +/// +/// ```ignore +/// forall<'a> { Implemented(dyn Fn(&u8): Fn<(&'a u8)>) } +/// ``` +/// +/// and +/// +/// ```ignore +/// forall<'a> { AliasEq(>::Output, ()) }, +/// ``` +pub(super) fn build_dyn_self_ty_clauses( + db: &dyn RustIrDatabase, + builder: &mut ClauseBuilder<'_, I>, + self_ty: Ty, +) { + let interner = db.interner(); + let dyn_ty = match self_ty.data(interner) { + TyData::Dyn(dyn_ty) => dyn_ty, + _ => return, + }; + let generalized_dyn_ty = generalize::Generalize::apply(db.interner(), dyn_ty); + + // Here, `self_ty` is the `dyn Fn(&u8)`, and `dyn_ty` is the `exists { .. + // }` clauses shown above. + + // Turn free BoundVars in the type into new existentials. E.g. + // we might get some `dyn Foo`, and we don't want to return + // a clause with a free variable. We can instead return a + // slightly more general clause by basically turning this into + // `exists dyn Foo`. + + builder.push_binders(&generalized_dyn_ty, |builder, dyn_ty| { + for exists_qwc in dyn_ty.bounds.map_ref(|r| r.iter(interner)) { + // Replace the `T` from `exists { .. }` with `self_ty`, + // yielding clases like + // + // ``` + // forall<'a> { Implemented(dyn Fn(&u8): Fn<(&'a u8)>) } + // ``` + let qwc = exists_qwc.substitute(interner, &[self_ty.clone().cast(interner)]); + + builder.push_binders(&qwc, |builder, wc| match &wc { + // For the implemented traits, we need to elaborate super traits and add where clauses from the trait + WhereClause::Implemented(trait_ref) => { + push_dyn_ty_impl_clauses(db, builder, trait_ref.clone()) + } + // Associated item bindings are just taken as facts (?) + WhereClause::AliasEq(_) => builder.push_fact(wc), + }); + } + }); +} + +/// Generate `Implemented` clauses for a `dyn Trait` type. We need to generate +/// `Implemented` clauses for all super traits, and for each trait we require +/// its where clauses. (See #203.) +fn push_dyn_ty_impl_clauses( + db: &dyn RustIrDatabase, + builder: &mut ClauseBuilder<'_, I>, + trait_ref: TraitRef, +) { + let interner = db.interner(); + // We have some `dyn Trait`, and some `trait SuperTrait: WC` + // which is a super trait of `Trait` (including actually + // just being the same trait); then we want to push + // `Implemented(dyn Trait: SuperTrait) :- WC`. + + let super_trait_refs = + super_traits(db, trait_ref.trait_id).substitute(interner, &trait_ref.substitution); + + for q_super_trait_ref in super_trait_refs { + builder.push_binders(&q_super_trait_ref, |builder, super_trait_ref| { + let trait_datum = db.trait_datum(super_trait_ref.trait_id); + let wc = trait_datum + .where_clauses() + .substitute(interner, &super_trait_ref.substitution); + builder.push_clause(super_trait_ref, wc); + }); + } +} + +pub fn super_traits( + db: &dyn RustIrDatabase, + trait_id: TraitId, +) -> Binders>>> { + let interner = db.interner(); + let mut seen_traits = FxHashSet::default(); + let trait_datum = db.trait_datum(trait_id); + let trait_ref = Binders::empty( + db.interner(), + TraitRef { + trait_id, + substitution: trait_datum + .binders + .identity_substitution(interner) + .shifted_in(interner), + }, + ); + let mut trait_refs = Vec::new(); + go(db, trait_ref, &mut seen_traits, &mut trait_refs); + + fn go( + db: &dyn RustIrDatabase, + trait_ref: Binders>, + seen_traits: &mut FxHashSet>, + trait_refs: &mut Vec>>, + ) { + let interner = db.interner(); + let trait_id = trait_ref.skip_binders().trait_id; + trait_refs.push(trait_ref.clone()); + let trait_datum = db.trait_datum(trait_id); + let super_trait_refs = trait_datum + .binders + .map_ref(|td| { + td.where_clauses + .iter() + .filter_map(|qwc| { + qwc.as_ref().filter_map(|wc| match wc { + WhereClause::Implemented(tr) => { + let self_ty = tr.self_type_parameter(db.interner()); + + // We're looking for where clauses + // of the form `Self: Trait`. That's + // ^1.0 because we're one binder in. + if self_ty.bound(db.interner()) + != Some(BoundVar::new(DebruijnIndex::ONE, 0)) + { + return None; + } + // Avoid cycles + if !seen_traits.insert(tr.trait_id) { + return None; + } + Some(tr.clone()) + } + WhereClause::AliasEq(_) => None, + }) + }) + .collect::>() + }) + // we skip binders on the trait_ref here and add them to the binders + // on the trait ref in the loop below. We could probably avoid this if + // we could turn the `Binders>` into a `Vec>` easily. + .substitute(db.interner(), &trait_ref.skip_binders().substitution); + for q_super_trait_ref in super_trait_refs { + // So now we need to combine the binders of trait_ref with the + // binders of super_trait_ref. + let actual_binders = Binders::new(trait_ref.binders.clone(), q_super_trait_ref); + let q_super_trait_ref = actual_binders.fuse_binders(interner); + go(db, q_super_trait_ref, seen_traits, trait_refs); + } + } + + Binders::new(trait_datum.binders.binders.clone(), trait_refs) +} diff --git a/chalk-solve/src/goal_builder.rs b/chalk-solve/src/goal_builder.rs index b915a0d84b7..027cc028f5f 100644 --- a/chalk-solve/src/goal_builder.rs +++ b/chalk-solve/src/goal_builder.rs @@ -3,7 +3,6 @@ use cast::CastTo; use chalk_ir::cast::Cast; use chalk_ir::cast::Caster; use chalk_ir::*; -use chalk_rust_ir::ToParameter; use fold::shift::Shift; use fold::Fold; use interner::{HasInterner, Interner}; diff --git a/tests/test/existential_types.rs b/tests/test/existential_types.rs index 7318fb8d684..8412a2fd412 100644 --- a/tests/test/existential_types.rs +++ b/tests/test/existential_types.rs @@ -121,6 +121,129 @@ fn dyn_Foo_Bar() { } } +#[test] +fn dyn_super_trait_simple() { + test! { + program { + trait Foo {} + trait Bar where Self: Foo {} + + struct A {} + struct B {} + } + + goal { + dyn Bar: Bar + } yields { + "Unique" + } + + goal { + dyn Bar: Foo + } yields { + "Unique" + } + + goal { + dyn Bar: Foo + } yields { + "No possible solution" + } + + goal { + exists { + dyn Bar: Foo + } + } yields { + "Unique; substitution [?0 := B], lifetime constraints []" + } + } +} + +#[test] +fn dyn_super_trait_cycle() { + test! { + program { + trait Foo where Self: Bar {} + trait Bar where Self: Foo {} + + struct A {} + struct B {} + } + + // We currently can't prove this because of the cyclic where clauses. + // But importantly, we don't crash or get into an infinite loop. + goal { + dyn Bar: Bar + } yields { + "No possible solution" + } + } +} + +#[test] +fn dyn_super_trait_higher_ranked() { + test! { + program { + trait Foo<'a> {} + trait Bar<'a> where forall<'b> Self: Foo<'b> {} + trait Baz where forall<'a> Self: Bar<'a> {} + + struct A {} + struct B {} + } + + goal { + forall<'x> { + dyn Baz: Bar<'x> + } + } yields { + "Unique" + } + + goal { + forall<'x> { + dyn Baz: Foo<'x> + } + } yields { + "Unique" + } + + goal { + forall<'x, 'y> { + dyn Bar<'y>: Foo<'x> + } + } yields { + "Unique" + } + } +} + +#[test] +fn dyn_super_trait_non_super_trait_clause() { + test! { + program { + trait Bar {} + trait Foo where A: Bar {} + + struct A {} + impl Bar for A {} + } + + goal { + dyn Foo: Foo + } yields { + "Unique" + } + + goal { + dyn Foo: Bar + } yields { + "No possible solution" + } + } +} + #[test] fn dyn_higher_ranked_type_arguments() { test! {