diff options
Diffstat (limited to 'vendor/chalk-solve-0.87.0/src/clauses/program_clauses.rs')
| -rw-r--r-- | vendor/chalk-solve-0.87.0/src/clauses/program_clauses.rs | 921 |
1 files changed, 921 insertions, 0 deletions
diff --git a/vendor/chalk-solve-0.87.0/src/clauses/program_clauses.rs b/vendor/chalk-solve-0.87.0/src/clauses/program_clauses.rs new file mode 100644 index 000000000..19811ff8b --- /dev/null +++ b/vendor/chalk-solve-0.87.0/src/clauses/program_clauses.rs @@ -0,0 +1,921 @@ +use crate::clauses::builder::ClauseBuilder; +use crate::rust_ir::*; +use crate::split::Split; +use chalk_ir::cast::{Cast, Caster}; +use chalk_ir::interner::Interner; +use chalk_ir::*; +use std::iter; +use tracing::instrument; + +/// Trait for lowering a given piece of rust-ir source (e.g., an impl +/// or struct definition) into its associated "program clauses" -- +/// that is, into the lowered, logical rules that it defines. +pub trait ToProgramClauses<I: Interner> { + fn to_program_clauses(&self, builder: &mut ClauseBuilder<'_, I>, environment: &Environment<I>); +} + +impl<I: Interner> ToProgramClauses<I> for ImplDatum<I> { + /// Given `impl<T: Clone> Clone for Vec<T> { ... }`, generate: + /// + /// ```notrust + /// -- Rule Implemented-From-Impl + /// forall<T> { + /// Implemented(Vec<T>: Clone) :- Implemented(T: Clone). + /// } + /// ``` + /// + /// For a negative impl like `impl... !Clone for ...`, however, we + /// generate nothing -- this is just a way to *opt out* from the + /// default auto trait impls, it doesn't have any positive effect + /// on its own. + fn to_program_clauses( + &self, + builder: &mut ClauseBuilder<'_, I>, + _environment: &Environment<I>, + ) { + if self.is_positive() { + let binders = self.binders.clone(); + builder.push_binders( + binders, + |builder, + ImplDatumBound { + trait_ref, + where_clauses, + }| { + builder.push_clause(trait_ref, where_clauses); + }, + ); + } + } +} + +impl<I: Interner> ToProgramClauses<I> for AssociatedTyValue<I> { + /// Given the following trait: + /// + /// ```notrust + /// trait Iterable { + /// type IntoIter<'a>: 'a; + /// } + /// ``` + /// + /// Then for the following impl: + /// ```notrust + /// impl<T> Iterable for Vec<T> where T: Clone { + /// type IntoIter<'a> = Iter<'a, T>; + /// } + /// ``` + /// + /// we generate: + /// + /// ```notrust + /// -- Rule Normalize-From-Impl + /// forall<'a, T> { + /// Normalize(<Vec<T> as Iterable>::IntoIter<'a> -> Iter<'a, T>>) :- + /// Implemented(T: Clone), // (1) + /// Implemented(Iter<'a, T>: 'a). // (2) + /// } + /// ``` + fn to_program_clauses( + &self, + builder: &mut ClauseBuilder<'_, I>, + _environment: &Environment<I>, + ) { + let impl_datum = builder.db.impl_datum(self.impl_id); + let associated_ty = builder.db.associated_ty_data(self.associated_ty_id); + + builder.push_binders(self.value.clone(), |builder, assoc_ty_value| { + let all_parameters = builder.placeholders_in_scope().to_vec(); + + // Get the projection for this associated type: + // + // * `impl_params`: `[!T]` + // * `projection`: `<Vec<!T> as Iterable>::Iter<'!a>` + let (impl_params, projection) = builder + .db + .impl_parameters_and_projection_from_associated_ty_value(&all_parameters, self); + + // Assemble the full list of conditions for projection to be valid. + // This comes in two parts, marked as (1) and (2) in doc above: + // + // 1. require that the where clauses from the impl apply + let interner = builder.db.interner(); + let impl_where_clauses = impl_datum + .binders + .map_ref(|b| &b.where_clauses) + .into_iter() + .map(|wc| wc.cloned().substitute(interner, impl_params)); + + // 2. any where-clauses from the `type` declaration in the trait: the + // parameters must be substituted with those of the impl + let assoc_ty_where_clauses = associated_ty + .binders + .map_ref(|b| &b.where_clauses) + .into_iter() + .map(|wc| wc.cloned().substitute(interner, &projection.substitution)); + + // Create the final program clause: + // + // ```notrust + // -- Rule Normalize-From-Impl + // forall<'a, T> { + // Normalize(<Vec<T> as Iterable>::IntoIter<'a> -> Iter<'a, T>>) :- + // Implemented(T: Clone), // (1) + // Implemented(Iter<'a, T>: 'a). // (2) + // } + // ``` + builder.push_clause( + Normalize { + alias: AliasTy::Projection(projection.clone()), + ty: assoc_ty_value.ty, + }, + impl_where_clauses.chain(assoc_ty_where_clauses), + ); + }); + } +} + +impl<I: Interner> ToProgramClauses<I> for OpaqueTyDatum<I> { + /// Given `opaque type T<U>: A + B = HiddenTy where U: C;`, we generate: + /// + /// ```notrust + /// AliasEq(T<U> = HiddenTy) :- Reveal. + /// AliasEq(T<U> = !T<U>). + /// WF(T<U>) :- WF(U: C). + /// Implemented(!T<U>: A). + /// Implemented(!T<U>: B). + /// ``` + /// where `!T<..>` is the placeholder for the unnormalized type `T<..>`. + #[instrument(level = "debug", skip(builder))] + fn to_program_clauses( + &self, + builder: &mut ClauseBuilder<'_, I>, + _environment: &Environment<I>, + ) { + builder.push_binders(self.bound.clone(), |builder, opaque_ty_bound| { + let interner = builder.interner(); + let substitution = builder.substitution_in_scope(); + let alias = AliasTy::Opaque(OpaqueTy { + opaque_ty_id: self.opaque_ty_id, + substitution: substitution.clone(), + }); + + let alias_placeholder_ty = + TyKind::OpaqueType(self.opaque_ty_id, substitution).intern(interner); + + // AliasEq(T<..> = HiddenTy) :- Reveal. + builder.push_clause( + DomainGoal::Holds( + AliasEq { + alias: alias.clone(), + ty: builder.db.hidden_opaque_type(self.opaque_ty_id), + } + .cast(interner), + ), + iter::once(DomainGoal::Reveal), + ); + + // AliasEq(T<..> = !T<..>). + builder.push_fact(DomainGoal::Holds( + AliasEq { + alias, + ty: alias_placeholder_ty.clone(), + } + .cast(interner), + )); + + // WF(!T<..>) :- WF(WC). + builder.push_binders(opaque_ty_bound.where_clauses, |builder, where_clauses| { + builder.push_clause( + WellFormed::Ty(alias_placeholder_ty.clone()), + where_clauses + .into_iter() + .map(|wc| wc.into_well_formed_goal(interner)), + ); + }); + + let substitution = Substitution::from1(interner, alias_placeholder_ty); + for bound in opaque_ty_bound.bounds { + let bound_with_placeholder_ty = bound.substitute(interner, &substitution); + builder.push_binders(bound_with_placeholder_ty, |builder, bound| match &bound { + // For the implemented traits, we need to elaborate super traits and add where clauses from the trait + WhereClause::Implemented(trait_ref) => { + super::super_traits::push_trait_super_clauses( + builder.db, + builder, + trait_ref.clone(), + ) + } + // FIXME: Associated item bindings are just taken as facts (?) + WhereClause::AliasEq(_) => builder.push_fact(bound), + WhereClause::LifetimeOutlives(..) => {} + WhereClause::TypeOutlives(..) => {} + }); + } + }); + } +} + +/// Generates the "well-formed" program clauses for an applicative type +/// with the name `type_name`. For example, given a struct definition: +/// +/// ```ignore +/// struct Foo<T: Eq> { } +/// ``` +/// +/// we would generate the clause: +/// +/// ```notrust +/// forall<T> { +/// WF(Foo<T>) :- WF(T: Eq). +/// } +/// ``` +/// +/// # Parameters +/// - builder -- the clause builder. We assume all the generic types from `Foo` are in scope +/// - type_name -- in our example above, the name `Foo` +/// - where_clauses -- the list of where clauses declared on the type (`T: Eq`, in our example) +fn well_formed_program_clauses<'a, I, Wc>( + builder: &'a mut ClauseBuilder<'_, I>, + ty: Ty<I>, + where_clauses: Wc, +) where + I: Interner, + Wc: Iterator<Item = &'a QuantifiedWhereClause<I>>, +{ + let interner = builder.interner(); + builder.push_clause( + WellFormed::Ty(ty), + where_clauses + .cloned() + .map(|qwc| qwc.into_well_formed_goal(interner)), + ); +} + +/// Generates the "fully visible" program clauses for an applicative type +/// with the name `type_name`. For example, given a struct definition: +/// +/// ```ignore +/// struct Foo<T: Eq> { } +/// ``` +/// +/// we would generate the clause: +/// +/// ```notrust +/// forall<T> { +/// IsFullyVisible(Foo<T>) :- IsFullyVisible(T). +/// } +/// ``` +/// +/// # Parameters +/// +/// - builder -- the clause builder. We assume all the generic types from `Foo` are in scope +/// - type_name -- in our example above, the name `Foo` +fn fully_visible_program_clauses<I>( + builder: &mut ClauseBuilder<'_, I>, + ty: Ty<I>, + subst: &Substitution<I>, +) where + I: Interner, +{ + let interner = builder.interner(); + builder.push_clause( + DomainGoal::IsFullyVisible(ty), + subst + .type_parameters(interner) + .map(|typ| DomainGoal::IsFullyVisible(typ).cast::<Goal<_>>(interner)), + ); +} + +/// Generates the "implied bounds" clauses for an applicative +/// type with the name `type_name`. For example, if `type_name` +/// represents a struct `S` that is declared like: +/// +/// ```ignore +/// struct S<T> where T: Eq { } +/// ``` +/// +/// then we would generate the rule: +/// +/// ```notrust +/// FromEnv(T: Eq) :- FromEnv(S<T>) +/// ``` +/// +/// # Parameters +/// +/// - builder -- the clause builder. We assume all the generic types from `S` are in scope. +/// - type_name -- in our example above, the name `S` +/// - where_clauses -- the list of where clauses declared on the type (`T: Eq`, in our example). +fn implied_bounds_program_clauses<'a, I, Wc>( + builder: &'a mut ClauseBuilder<'_, I>, + ty: &Ty<I>, + where_clauses: Wc, +) where + I: Interner, + Wc: Iterator<Item = &'a QuantifiedWhereClause<I>>, +{ + let interner = builder.interner(); + + for qwc in where_clauses { + builder.push_binders(qwc.clone(), |builder, wc| { + builder.push_clause(wc.into_from_env_goal(interner), Some(ty.clone().from_env())); + }); + } +} + +impl<I: Interner> ToProgramClauses<I> for AdtDatum<I> { + /// Given the following type definition: `struct Foo<T: Eq> { }`, generate: + /// + /// ```notrust + /// -- Rule WellFormed-Type + /// forall<T> { + /// WF(Foo<T>) :- WF(T: Eq). + /// } + /// + /// -- Rule Implied-Bound-From-Type + /// forall<T> { + /// FromEnv(T: Eq) :- FromEnv(Foo<T>). + /// } + /// + /// forall<T> { + /// IsFullyVisible(Foo<T>) :- IsFullyVisible(T). + /// } + /// ``` + /// + /// If the type `Foo` is marked `#[upstream]`, we also generate: + /// + /// ```notrust + /// forall<T> { IsUpstream(Foo<T>). } + /// ``` + /// + /// Otherwise, if the type `Foo` is not marked `#[upstream]`, we generate: + /// ```notrust + /// forall<T> { IsLocal(Foo<T>). } + /// ``` + /// + /// Given an `#[upstream]` type that is also fundamental: + /// + /// ```notrust + /// #[upstream] + /// #[fundamental] + /// struct Box<T, U> {} + /// ``` + /// + /// We generate the following clauses: + /// + /// ```notrust + /// forall<T, U> { IsLocal(Box<T, U>) :- IsLocal(T). } + /// forall<T, U> { IsLocal(Box<T, U>) :- IsLocal(U). } + /// + /// forall<T, U> { IsUpstream(Box<T, U>) :- IsUpstream(T), IsUpstream(U). } + /// + /// // Generated for both upstream and local fundamental types + /// forall<T, U> { DownstreamType(Box<T, U>) :- DownstreamType(T). } + /// forall<T, U> { DownstreamType(Box<T, U>) :- DownstreamType(U). } + /// ``` + /// + #[instrument(level = "debug", skip(builder))] + fn to_program_clauses( + &self, + builder: &mut ClauseBuilder<'_, I>, + _environment: &Environment<I>, + ) { + let interner = builder.interner(); + let binders = self.binders.map_ref(|b| &b.where_clauses).cloned(); + + builder.push_binders(binders, |builder, where_clauses| { + let self_ty = TyKind::Adt(self.id, builder.substitution_in_scope()).intern(interner); + + well_formed_program_clauses(builder, self_ty.clone(), where_clauses.iter()); + + implied_bounds_program_clauses(builder, &self_ty, where_clauses.iter()); + + fully_visible_program_clauses( + builder, + self_ty.clone(), + &builder.substitution_in_scope(), + ); + + // Types that are not marked `#[upstream]` satisfy IsLocal(Ty) + if !self.flags.upstream { + // `IsLocalTy(Ty)` depends *only* on whether the type + // is marked #[upstream] and nothing else + builder.push_fact(DomainGoal::IsLocal(self_ty.clone())); + } else if self.flags.fundamental { + // If a type is `#[upstream]`, but is also + // `#[fundamental]`, it satisfies IsLocal if and only + // if its parameters satisfy IsLocal + for type_param in builder.substitution_in_scope().type_parameters(interner) { + builder.push_clause( + DomainGoal::IsLocal(self_ty.clone()), + Some(DomainGoal::IsLocal(type_param)), + ); + } + builder.push_clause( + DomainGoal::IsUpstream(self_ty.clone()), + builder + .substitution_in_scope() + .type_parameters(interner) + .map(|type_param| DomainGoal::IsUpstream(type_param)), + ); + } else { + // The type is just upstream and not fundamental + builder.push_fact(DomainGoal::IsUpstream(self_ty.clone())); + } + + if self.flags.fundamental { + assert!( + builder + .substitution_in_scope() + .type_parameters(interner) + .count() + >= 1, + "Only fundamental types with type parameters are supported" + ); + for type_param in builder.substitution_in_scope().type_parameters(interner) { + builder.push_clause( + DomainGoal::DownstreamType(self_ty.clone()), + Some(DomainGoal::DownstreamType(type_param)), + ); + } + } + }); + } +} + +impl<I: Interner> ToProgramClauses<I> for FnDefDatum<I> { + /// Given the following function definition: `fn bar<T>() where T: Eq`, generate: + /// + /// ```notrust + /// -- Rule WellFormed-Type + /// forall<T> { + /// WF(bar<T>) :- WF(T: Eq) + /// } + /// + /// -- Rule Implied-Bound-From-Type + /// forall<T> { + /// FromEnv(T: Eq) :- FromEnv(bar<T>). + /// } + /// + /// forall<T> { + /// IsFullyVisible(bar<T>) :- IsFullyVisible(T). + /// } + /// ``` + #[instrument(level = "debug", skip(builder))] + fn to_program_clauses( + &self, + builder: &mut ClauseBuilder<'_, I>, + _environment: &Environment<I>, + ) { + let interner = builder.interner(); + let binders = self.binders.map_ref(|b| &b.where_clauses).cloned(); + + builder.push_binders(binders, |builder, where_clauses| { + let ty = TyKind::FnDef(self.id, builder.substitution_in_scope()).intern(interner); + + well_formed_program_clauses(builder, ty.clone(), where_clauses.iter()); + + implied_bounds_program_clauses(builder, &ty, where_clauses.iter()); + + fully_visible_program_clauses(builder, ty, &builder.substitution_in_scope()); + }); + } +} + +impl<I: Interner> ToProgramClauses<I> for TraitDatum<I> { + /// Given the following trait declaration: `trait Ord<T> where Self: Eq<T> { ... }`, generate: + /// + /// ```notrust + /// -- Rule WellFormed-TraitRef + /// forall<Self, T> { + /// WF(Self: Ord<T>) :- Implemented(Self: Ord<T>), WF(Self: Eq<T>). + /// } + /// ``` + /// + /// and the reverse rules: + /// + /// ```notrust + /// -- Rule Implemented-From-Env + /// forall<Self, T> { + /// (Self: Ord<T>) :- FromEnv(Self: Ord<T>). + /// } + /// + /// -- Rule Implied-Bound-From-Trait + /// forall<Self, T> { + /// FromEnv(Self: Eq<T>) :- FromEnv(Self: Ord<T>). + /// } + /// ``` + /// + /// As specified in the orphan rules, if a trait is not marked `#[upstream]`, the current crate + /// can implement it for any type. To represent that, we generate: + /// + /// ```notrust + /// // `Ord<T>` would not be `#[upstream]` when compiling `std` + /// forall<Self, T> { LocalImplAllowed(Self: Ord<T>). } + /// ``` + /// + /// For traits that are `#[upstream]` (i.e. not in the current crate), the orphan rules dictate + /// that impls are allowed as long as at least one type parameter is local and each type + /// prior to that is fully visible. That means that each type prior to the first local + /// type cannot contain any of the type parameters of the impl. + /// + /// This rule is fairly complex, so we expand it and generate a program clause for each + /// possible case. This is represented as follows: + /// + /// ```notrust + /// // for `#[upstream] trait Foo<T, U, V> where Self: Eq<T> { ... }` + /// forall<Self, T, U, V> { + /// LocalImplAllowed(Self: Foo<T, U, V>) :- IsLocal(Self). + /// } + /// + /// forall<Self, T, U, V> { + /// LocalImplAllowed(Self: Foo<T, U, V>) :- + /// IsFullyVisible(Self), + /// IsLocal(T). + /// } + /// + /// forall<Self, T, U, V> { + /// LocalImplAllowed(Self: Foo<T, U, V>) :- + /// IsFullyVisible(Self), + /// IsFullyVisible(T), + /// IsLocal(U). + /// } + /// + /// forall<Self, T, U, V> { + /// LocalImplAllowed(Self: Foo<T, U, V>) :- + /// IsFullyVisible(Self), + /// IsFullyVisible(T), + /// IsFullyVisible(U), + /// IsLocal(V). + /// } + /// ``` + /// + /// The overlap check uses compatible { ... } mode to ensure that it accounts for impls that + /// may exist in some other *compatible* world. For every upstream trait, we add a rule to + /// account for the fact that upstream crates are able to compatibly add impls of upstream + /// traits for upstream types. + /// + /// ```notrust + /// // For `#[upstream] trait Foo<T, U, V> where Self: Eq<T> { ... }` + /// forall<Self, T, U, V> { + /// Implemented(Self: Foo<T, U, V>) :- + /// Implemented(Self: Eq<T>), // where clauses + /// Compatible, // compatible modality + /// IsUpstream(Self), + /// IsUpstream(T), + /// IsUpstream(U), + /// IsUpstream(V), + /// CannotProve. // returns ambiguous + /// } + /// ``` + /// + /// In certain situations, this is too restrictive. Consider the following code: + /// + /// ```notrust + /// /* In crate std */ + /// trait Sized { } + /// struct str { } + /// + /// /* In crate bar (depends on std) */ + /// trait Bar { } + /// impl Bar for str { } + /// impl<T> Bar for T where T: Sized { } + /// ``` + /// + /// Here, because of the rules we've defined, these two impls overlap. The std crate is + /// upstream to bar, and thus it is allowed to compatibly implement Sized for str. If str + /// can implement Sized in a compatible future, these two impls definitely overlap since the + /// second impl covers all types that implement Sized. + /// + /// The solution we've got right now is to mark Sized as "fundamental" when it is defined. + /// This signals to the Rust compiler that it can rely on the fact that str does not + /// implement Sized in all contexts. A consequence of this is that we can no longer add an + /// implementation of Sized compatibly for str. This is the trade off you make when defining + /// a fundamental trait. + /// + /// To implement fundamental traits, we simply just do not add the rule above that allows + /// upstream types to implement upstream traits. Fundamental traits are not allowed to + /// compatibly do that. + fn to_program_clauses(&self, builder: &mut ClauseBuilder<'_, I>, environment: &Environment<I>) { + let interner = builder.interner(); + let binders = self.binders.map_ref(|b| &b.where_clauses).cloned(); + builder.push_binders(binders, |builder, where_clauses| { + let trait_ref = chalk_ir::TraitRef { + trait_id: self.id, + substitution: builder.substitution_in_scope(), + }; + + builder.push_clause( + trait_ref.clone().well_formed(), + where_clauses + .iter() + .cloned() + .map(|qwc| qwc.into_well_formed_goal(interner)) + .casted::<Goal<_>>(interner) + .chain(Some(trait_ref.clone().cast(interner))), + ); + + // The number of parameters will always be at least 1 + // because of the Self parameter that is automatically + // added to every trait. This is important because + // otherwise the added program clauses would not have any + // conditions. + let type_parameters: Vec<_> = trait_ref.type_parameters(interner).collect(); + + if environment.has_compatible_clause(interner) { + // Note: even though we do check for a `Compatible` clause here, + // we also keep it as a condition for the clauses below, purely + // for logical consistency. But really, it's not needed and could be + // removed. + + // Drop trait can't have downstream implementation because it can only + // be implemented with the same genericity as the struct definition, + // i.e. Drop implementation for `struct S<T: Eq> {}` is forced to be + // `impl Drop<T: Eq> for S<T> { ... }`. That means that orphan rules + // prevent Drop from being implemented in downstream crates. + if self.well_known != Some(WellKnownTrait::Drop) { + // Add all cases for potential downstream impls that could exist + for i in 0..type_parameters.len() { + builder.push_clause( + trait_ref.clone(), + where_clauses + .iter() + .cloned() + .casted(interner) + .chain(iter::once(DomainGoal::Compatible.cast(interner))) + .chain((0..i).map(|j| { + DomainGoal::IsFullyVisible(type_parameters[j].clone()) + .cast(interner) + })) + .chain(iter::once( + DomainGoal::DownstreamType(type_parameters[i].clone()) + .cast(interner), + )) + .chain(iter::once(GoalData::CannotProve.intern(interner))), + ); + } + } + + // Fundamental traits can be reasoned about negatively without any ambiguity, so no + // need for this rule if the trait is fundamental. + if !self.flags.fundamental { + builder.push_clause( + trait_ref.clone(), + where_clauses + .iter() + .cloned() + .casted(interner) + .chain(iter::once(DomainGoal::Compatible.cast(interner))) + .chain( + trait_ref + .type_parameters(interner) + .map(|ty| DomainGoal::IsUpstream(ty).cast(interner)), + ) + .chain(iter::once(GoalData::CannotProve.intern(interner))), + ); + } + } + + // Orphan rules: + if !self.flags.upstream { + // Impls for traits declared locally always pass the impl rules + builder.push_fact(DomainGoal::LocalImplAllowed(trait_ref.clone())); + } else { + // Impls for remote traits must have a local type in the right place + for i in 0..type_parameters.len() { + builder.push_clause( + DomainGoal::LocalImplAllowed(trait_ref.clone()), + (0..i) + .map(|j| DomainGoal::IsFullyVisible(type_parameters[j].clone())) + .chain(Some(DomainGoal::IsLocal(type_parameters[i].clone()))), + ); + } + } + + // Reverse implied bound rules: given (e.g.) `trait Foo: Bar + Baz`, + // we create rules like: + // + // ``` + // FromEnv(T: Bar) :- FromEnv(T: Foo) + // ``` + // + // and + // + // ``` + // FromEnv(T: Baz) :- FromEnv(T: Foo) + // ``` + for qwc in where_clauses { + builder.push_binders(qwc, |builder, wc| { + builder.push_clause( + wc.into_from_env_goal(interner), + Some(trait_ref.clone().from_env()), + ); + }); + } + + // Finally, for every trait `Foo` we make a rule + // + // ``` + // Implemented(T: Foo) :- FromEnv(T: Foo) + // ``` + builder.push_clause(trait_ref.clone(), Some(trait_ref.from_env())); + }); + } +} + +impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> { + /// For each associated type, we define the "projection + /// equality" rules. There are always two; one for a successful normalization, + /// and one for the "fallback" notion of equality. + /// + /// Given: (here, `'a` and `T` represent zero or more parameters) + /// + /// ```notrust + /// trait Foo { + /// type Assoc<'a, T>: Bounds where WC; + /// } + /// ``` + /// + /// we generate the 'fallback' rule: + /// + /// ```notrust + /// -- Rule AliasEq-Placeholder + /// forall<Self, 'a, T> { + /// AliasEq(<Self as Foo>::Assoc<'a, T> = (Foo::Assoc<'a, T>)<Self>). + /// } + /// ``` + /// + /// and + /// + /// ```notrust + /// -- Rule AliasEq-Normalize + /// forall<Self, 'a, T, U> { + /// AliasEq(<T as Foo>::Assoc<'a, T> = U) :- + /// Normalize(<T as Foo>::Assoc -> U). + /// } + /// ``` + /// + /// We used to generate an "elaboration" rule like this: + /// + /// ```notrust + /// forall<T> { + /// T: Foo :- exists<U> { AliasEq(<T as Foo>::Assoc = U) }. + /// } + /// ``` + /// + /// but this caused problems with the recursive solver. In + /// particular, whenever normalization is possible, we cannot + /// solve that projection uniquely, since we can now elaborate + /// `AliasEq` to fallback *or* normalize it. So instead we + /// handle this kind of reasoning through the `FromEnv` predicate. + /// + /// We also generate rules specific to WF requirements and implied bounds: + /// + /// ```notrust + /// -- Rule WellFormed-AssocTy + /// forall<Self, 'a, T> { + /// WellFormed((Foo::Assoc)<Self, 'a, T>) :- WellFormed(Self: Foo), WellFormed(WC). + /// } + /// + /// -- Rule Implied-WC-From-AssocTy + /// forall<Self, 'a, T> { + /// FromEnv(WC) :- FromEnv((Foo::Assoc)<Self, 'a, T>). + /// } + /// + /// -- Rule Implied-Bound-From-AssocTy + /// forall<Self, 'a, T> { + /// FromEnv(<Self as Foo>::Assoc<'a,T>: Bounds) :- FromEnv(Self: Foo), WC. + /// } + /// + /// -- Rule Implied-Trait-From-AssocTy + /// forall<Self,'a, T> { + /// FromEnv(Self: Foo) :- FromEnv((Foo::Assoc)<Self, 'a,T>). + /// } + /// ``` + fn to_program_clauses( + &self, + builder: &mut ClauseBuilder<'_, I>, + _environment: &Environment<I>, + ) { + let interner = builder.interner(); + let binders = self.binders.clone(); + builder.push_binders( + binders, + |builder, + AssociatedTyDatumBound { + where_clauses, + bounds, + }| { + let substitution = builder.substitution_in_scope(); + + let projection = ProjectionTy { + associated_ty_id: self.id, + substitution: substitution.clone(), + }; + let projection_ty = AliasTy::Projection(projection.clone()).intern(interner); + + // Retrieve the trait ref embedding the associated type + let trait_ref = builder.db.trait_ref_from_projection(&projection); + + // Construct an application from the projection. So if we have `<T as Iterator>::Item`, + // we would produce `(Iterator::Item)<T>`. + let ty = TyKind::AssociatedType(self.id, substitution).intern(interner); + + let projection_eq = AliasEq { + alias: AliasTy::Projection(projection.clone()), + ty: ty.clone(), + }; + + // Fallback rule. The solver uses this to move between the projection + // and placeholder type. + // + // forall<Self> { + // AliasEq(<Self as Foo>::Assoc = (Foo::Assoc)<Self>). + // } + builder.push_fact_with_priority(projection_eq, None, ClausePriority::Low); + + // Well-formedness of projection type. + // + // forall<Self> { + // WellFormed((Foo::Assoc)<Self>) :- WellFormed(Self: Foo), WellFormed(WC). + // } + builder.push_clause( + WellFormed::Ty(ty.clone()), + iter::once(WellFormed::Trait(trait_ref.clone()).cast::<Goal<_>>(interner)) + .chain( + where_clauses + .iter() + .cloned() + .map(|qwc| qwc.into_well_formed_goal(interner)) + .casted(interner), + ), + ); + + // Assuming well-formedness of projection type means we can assume + // the trait ref as well. Mostly used in function bodies. + // + // forall<Self> { + // FromEnv(Self: Foo) :- FromEnv((Foo::Assoc)<Self>). + // } + builder.push_clause(FromEnv::Trait(trait_ref.clone()), Some(ty.from_env())); + + // Reverse rule for where clauses. + // + // forall<Self> { + // FromEnv(WC) :- FromEnv((Foo::Assoc)<Self>). + // } + // + // This is really a family of clauses, one for each where clause. + for qwc in &where_clauses { + builder.push_binders(qwc.clone(), |builder, wc| { + builder.push_clause( + wc.into_from_env_goal(interner), + Some(FromEnv::Ty(ty.clone())), + ); + }); + } + + // Reverse rule for implied bounds. + // + // forall<Self> { + // FromEnv(<Self as Foo>::Assoc: Bounds) :- FromEnv(Self: Foo), WC + // } + for quantified_bound in bounds { + builder.push_binders(quantified_bound, |builder, bound| { + for wc in bound.into_where_clauses(interner, projection_ty.clone()) { + builder.push_clause( + wc.into_from_env_goal(interner), + iter::once( + FromEnv::Trait(trait_ref.clone()).cast::<Goal<_>>(interner), + ) + .chain(where_clauses.iter().cloned().casted(interner)), + ); + } + }); + } + + // add new type parameter U + builder.push_bound_ty(|builder, ty| { + // `Normalize(<T as Foo>::Assoc -> U)` + let normalize = Normalize { + alias: AliasTy::Projection(projection.clone()), + ty: ty.clone(), + }; + + // `AliasEq(<T as Foo>::Assoc = U)` + let projection_eq = AliasEq { + alias: AliasTy::Projection(projection), + ty, + }; + + // Projection equality rule from above. + // + // forall<T, U> { + // AliasEq(<T as Foo>::Assoc = U) :- + // Normalize(<T as Foo>::Assoc -> U). + // } + builder.push_clause(projection_eq, Some(normalize)); + }); + }, + ); + } +} |