vendor/chalk-solve/src/clauses/program_clauses.rs

   1 use crate::clauses::builder::ClauseBuilder;
   2 use crate::rust_ir::*;
   3 use crate::split::Split;
   4 use chalk_ir::cast::{Cast, Caster};
   5 use chalk_ir::interner::Interner;
   6 use chalk_ir::*;
   7 use std::iter;
   8 use tracing::instrument;
   9
  10 /// Trait for lowering a given piece of rust-ir source (e.g., an impl
  11 /// or struct definition) into its associated "program clauses" --
  12 /// that is, into the lowered, logical rules that it defines.
  13 pub trait ToProgramClauses<I: Interner> {
  14     fn to_program_clauses(&self, builder: &mut ClauseBuilder<'_, I>, environment: &Environment<I>);
  15 }
  16
  17 impl<I: Interner> ToProgramClauses<I> for ImplDatum<I> {
  18     /// Given `impl<T: Clone> Clone for Vec<T> { ... }`, generate:
  19     ///
  20     /// ```notrust
  21     /// -- Rule Implemented-From-Impl
  22     /// forall<T> {
  23     ///     Implemented(Vec<T>: Clone) :- Implemented(T: Clone).
  24     /// }
  25     /// ```
  26     ///
  27     /// For a negative impl like `impl... !Clone for ...`, however, we
  28     /// generate nothing -- this is just a way to *opt out* from the
  29     /// default auto trait impls, it doesn't have any positive effect
  30     /// on its own.
  31     fn to_program_clauses(
  32         &self,
  33         builder: &mut ClauseBuilder<'_, I>,
  34         _environment: &Environment<I>,
  35     ) {
  36         if self.is_positive() {
  37             let binders = self.binders.clone();
  38             builder.push_binders(
  39                 binders,
  40                 |builder,
  41                  ImplDatumBound {
  42                      trait_ref,
  43                      where_clauses,
  44                  }| {
  45                     builder.push_clause(trait_ref, where_clauses);
  46                 },
  47             );
  48         }
  49     }
  50 }
  51
  52 impl<I: Interner> ToProgramClauses<I> for AssociatedTyValue<I> {
  53     /// Given the following trait:
  54     ///
  55     /// ```notrust
  56     /// trait Iterable {
  57     ///     type IntoIter<'a>: 'a;
  58     /// }
  59     /// ```
  60     ///
  61     /// Then for the following impl:
  62     /// ```notrust
  63     /// impl<T> Iterable for Vec<T> where T: Clone {
  64     ///     type IntoIter<'a> = Iter<'a, T>;
  65     /// }
  66     /// ```
  67     ///
  68     /// we generate:
  69     ///
  70     /// ```notrust
  71     /// -- Rule Normalize-From-Impl
  72     /// forall<'a, T> {
  73     ///     Normalize(<Vec<T> as Iterable>::IntoIter<'a> -> Iter<'a, T>>) :-
  74     ///         Implemented(T: Clone),  // (1)
  75     ///         Implemented(Iter<'a, T>: 'a).   // (2)
  76     /// }
  77     /// ```
  78     fn to_program_clauses(
  79         &self,
  80         builder: &mut ClauseBuilder<'_, I>,
  81         _environment: &Environment<I>,
  82     ) {
  83         let impl_datum = builder.db.impl_datum(self.impl_id);
  84         let associated_ty = builder.db.associated_ty_data(self.associated_ty_id);
  85
  86         builder.push_binders(self.value.clone(), |builder, assoc_ty_value| {
  87             let all_parameters = builder.placeholders_in_scope().to_vec();
  88
  89             // Get the projection for this associated type:
  90             //
  91             // * `impl_params`: `[!T]`
  92             // * `projection`: `<Vec<!T> as Iterable>::Iter<'!a>`
  93             let (impl_params, projection) = builder
  94                 .db
  95                 .impl_parameters_and_projection_from_associated_ty_value(&all_parameters, self);
  96
  97             // Assemble the full list of conditions for projection to be valid.
  98             // This comes in two parts, marked as (1) and (2) in doc above:
  99             //
 100             // 1. require that the where clauses from the impl apply
 101             let interner = builder.db.interner();
 102             let impl_where_clauses = impl_datum
 103                 .binders
 104                 .map_ref(|b| &b.where_clauses)
 105                 .into_iter()
 106                 .map(|wc| wc.cloned().substitute(interner, impl_params));
 107
 108             // 2. any where-clauses from the `type` declaration in the trait: the
 109             //    parameters must be substituted with those of the impl
 110             let assoc_ty_where_clauses = associated_ty
 111                 .binders
 112                 .map_ref(|b| &b.where_clauses)
 113                 .into_iter()
 114                 .map(|wc| wc.cloned().substitute(interner, &projection.substitution));
 115
 116             // Create the final program clause:
 117             //
 118             // ```notrust
 119             // -- Rule Normalize-From-Impl
 120             // forall<'a, T> {
 121             //     Normalize(<Vec<T> as Iterable>::IntoIter<'a> -> Iter<'a, T>>) :-
 122             //         Implemented(T: Clone),  // (1)
 123             //         Implemented(Iter<'a, T>: 'a).   // (2)
 124             // }
 125             // ```
 126             builder.push_clause(
 127                 Normalize {
 128                     alias: AliasTy::Projection(projection.clone()),
 129                     ty: assoc_ty_value.ty,
 130                 },
 131                 impl_where_clauses.chain(assoc_ty_where_clauses),
 132             );
 133         });
 134     }
 135 }
 136
 137 impl<I: Interner> ToProgramClauses<I> for OpaqueTyDatum<I> {
 138     /// Given `opaque type T<U>: A + B = HiddenTy where U: C;`, we generate:
 139     ///
 140     /// ```notrust
 141     /// AliasEq(T<U> = HiddenTy) :- Reveal.
 142     /// AliasEq(T<U> = !T<U>).
 143     /// WF(T<U>) :- WF(U: C).
 144     /// Implemented(!T<U>: A).
 145     /// Implemented(!T<U>: B).
 146     /// ```
 147     /// where `!T<..>` is the placeholder for the unnormalized type `T<..>`.
 148     #[instrument(level = "debug", skip(builder))]
 149     fn to_program_clauses(
 150         &self,
 151         builder: &mut ClauseBuilder<'_, I>,
 152         _environment: &Environment<I>,
 153     ) {
 154         builder.push_binders(self.bound.clone(), |builder, opaque_ty_bound| {
 155             let interner = builder.interner();
 156             let substitution = builder.substitution_in_scope();
 157             let alias = AliasTy::Opaque(OpaqueTy {
 158                 opaque_ty_id: self.opaque_ty_id,
 159                 substitution: substitution.clone(),
 160             });
 161
 162             let alias_placeholder_ty =
 163                 TyKind::OpaqueType(self.opaque_ty_id, substitution).intern(interner);
 164
 165             // AliasEq(T<..> = HiddenTy) :- Reveal.
 166             builder.push_clause(
 167                 DomainGoal::Holds(
 168                     AliasEq {
 169                         alias: alias.clone(),
 170                         ty: builder.db.hidden_opaque_type(self.opaque_ty_id),
 171                     }
 172                     .cast(interner),
 173                 ),
 174                 iter::once(DomainGoal::Reveal),
 175             );
 176
 177             // AliasEq(T<..> = !T<..>).
 178             builder.push_fact(DomainGoal::Holds(
 179                 AliasEq {
 180                     alias,
 181                     ty: alias_placeholder_ty.clone(),
 182                 }
 183                 .cast(interner),
 184             ));
 185
 186             // WF(!T<..>) :- WF(WC).
 187             builder.push_binders(opaque_ty_bound.where_clauses, |builder, where_clauses| {
 188                 builder.push_clause(
 189                     WellFormed::Ty(alias_placeholder_ty.clone()),
 190                     where_clauses
 191                         .into_iter()
 192                         .map(|wc| wc.into_well_formed_goal(interner)),
 193                 );
 194             });
 195
 196             let substitution = Substitution::from1(interner, alias_placeholder_ty);
 197             for bound in opaque_ty_bound.bounds {
 198                 let bound_with_placeholder_ty = bound.substitute(interner, &substitution);
 199                 builder.push_binders(bound_with_placeholder_ty, |builder, bound| match &bound {
 200                     // For the implemented traits, we need to elaborate super traits and add where clauses from the trait
 201                     WhereClause::Implemented(trait_ref) => {
 202                         super::super_traits::push_trait_super_clauses(
 203                             builder.db,
 204                             builder,
 205                             trait_ref.clone(),
 206                         )
 207                     }
 208                     // FIXME: Associated item bindings are just taken as facts (?)
 209                     WhereClause::AliasEq(_) => builder.push_fact(bound),
 210                     WhereClause::LifetimeOutlives(..) => {}
 211                     WhereClause::TypeOutlives(..) => {}
 212                 });
 213             }
 214         });
 215     }
 216 }
 217
 218 /// Generates the "well-formed" program clauses for an applicative type
 219 /// with the name `type_name`. For example, given a struct definition:
 220 ///
 221 /// ```ignore
 222 /// struct Foo<T: Eq> { }
 223 /// ```
 224 ///
 225 /// we would generate the clause:
 226 ///
 227 /// ```notrust
 228 /// forall<T> {
 229 ///     WF(Foo<T>) :- WF(T: Eq).
 230 /// }
 231 /// ```
 232 ///
 233 /// # Parameters
 234 /// - builder -- the clause builder. We assume all the generic types from `Foo` are in scope
 235 /// - type_name -- in our example above, the name `Foo`
 236 /// - where_clauses -- the list of where clauses declared on the type (`T: Eq`, in our example)
 237 fn well_formed_program_clauses<'a, I, Wc>(
 238     builder: &'a mut ClauseBuilder<'_, I>,
 239     ty: Ty<I>,
 240     where_clauses: Wc,
 241 ) where
 242     I: Interner,
 243     Wc: Iterator<Item = &'a QuantifiedWhereClause<I>>,
 244 {
 245     let interner = builder.interner();
 246     builder.push_clause(
 247         WellFormed::Ty(ty),
 248         where_clauses
 249             .cloned()
 250             .map(|qwc| qwc.into_well_formed_goal(interner)),
 251     );
 252 }
 253
 254 /// Generates the "fully visible" program clauses for an applicative type
 255 /// with the name `type_name`. For example, given a struct definition:
 256 ///
 257 /// ```ignore
 258 /// struct Foo<T: Eq> { }
 259 /// ```
 260 ///
 261 /// we would generate the clause:
 262 ///
 263 /// ```notrust
 264 /// forall<T> {
 265 ///     IsFullyVisible(Foo<T>) :- IsFullyVisible(T).
 266 /// }
 267 /// ```
 268 ///
 269 /// # Parameters
 270 ///
 271 /// - builder -- the clause builder. We assume all the generic types from `Foo` are in scope
 272 /// - type_name -- in our example above, the name `Foo`
 273 fn fully_visible_program_clauses<I>(
 274     builder: &mut ClauseBuilder<'_, I>,
 275     ty: Ty<I>,
 276     subst: &Substitution<I>,
 277 ) where
 278     I: Interner,
 279 {
 280     let interner = builder.interner();
 281     builder.push_clause(
 282         DomainGoal::IsFullyVisible(ty),
 283         subst
 284             .type_parameters(interner)
 285             .map(|typ| DomainGoal::IsFullyVisible(typ).cast::<Goal<_>>(interner)),
 286     );
 287 }
 288
 289 /// Generates the "implied bounds" clauses for an applicative
 290 /// type with the name `type_name`. For example, if `type_name`
 291 /// represents a struct `S` that is declared like:
 292 ///
 293 /// ```ignore
 294 /// struct S<T> where T: Eq {  }
 295 /// ```
 296 ///
 297 /// then we would generate the rule:
 298 ///
 299 /// ```notrust
 300 /// FromEnv(T: Eq) :- FromEnv(S<T>)
 301 /// ```
 302 ///
 303 /// # Parameters
 304 ///
 305 /// - builder -- the clause builder. We assume all the generic types from `S` are in scope.
 306 /// - type_name -- in our example above, the name `S`
 307 /// - where_clauses -- the list of where clauses declared on the type (`T: Eq`, in our example).
 308 fn implied_bounds_program_clauses<'a, I, Wc>(
 309     builder: &'a mut ClauseBuilder<'_, I>,
 310     ty: &Ty<I>,
 311     where_clauses: Wc,
 312 ) where
 313     I: Interner,
 314     Wc: Iterator<Item = &'a QuantifiedWhereClause<I>>,
 315 {
 316     let interner = builder.interner();
 317
 318     for qwc in where_clauses {
 319         builder.push_binders(qwc.clone(), |builder, wc| {
 320             builder.push_clause(wc.into_from_env_goal(interner), Some(ty.clone().from_env()));
 321         });
 322     }
 323 }
 324
 325 impl<I: Interner> ToProgramClauses<I> for AdtDatum<I> {
 326     /// Given the following type definition: `struct Foo<T: Eq> { }`, generate:
 327     ///
 328     /// ```notrust
 329     /// -- Rule WellFormed-Type
 330     /// forall<T> {
 331     ///     WF(Foo<T>) :- WF(T: Eq).
 332     /// }
 333     ///
 334     /// -- Rule Implied-Bound-From-Type
 335     /// forall<T> {
 336     ///     FromEnv(T: Eq) :- FromEnv(Foo<T>).
 337     /// }
 338     ///
 339     /// forall<T> {
 340     ///     IsFullyVisible(Foo<T>) :- IsFullyVisible(T).
 341     /// }
 342     /// ```
 343     ///
 344     /// If the type `Foo` is marked `#[upstream]`, we also generate:
 345     ///
 346     /// ```notrust
 347     /// forall<T> { IsUpstream(Foo<T>). }
 348     /// ```
 349     ///
 350     /// Otherwise, if the type `Foo` is not marked `#[upstream]`, we generate:
 351     /// ```notrust
 352     /// forall<T> { IsLocal(Foo<T>). }
 353     /// ```
 354     ///
 355     /// Given an `#[upstream]` type that is also fundamental:
 356     ///
 357     /// ```notrust
 358     /// #[upstream]
 359     /// #[fundamental]
 360     /// struct Box<T, U> {}
 361     /// ```
 362     ///
 363     /// We generate the following clauses:
 364     ///
 365     /// ```notrust
 366     /// forall<T, U> { IsLocal(Box<T, U>) :- IsLocal(T). }
 367     /// forall<T, U> { IsLocal(Box<T, U>) :- IsLocal(U). }
 368     ///
 369     /// forall<T, U> { IsUpstream(Box<T, U>) :- IsUpstream(T), IsUpstream(U). }
 370     ///
 371     /// // Generated for both upstream and local fundamental types
 372     /// forall<T, U> { DownstreamType(Box<T, U>) :- DownstreamType(T). }
 373     /// forall<T, U> { DownstreamType(Box<T, U>) :- DownstreamType(U). }
 374     /// ```
 375     ///
 376     #[instrument(level = "debug", skip(builder))]
 377     fn to_program_clauses(
 378         &self,
 379         builder: &mut ClauseBuilder<'_, I>,
 380         _environment: &Environment<I>,
 381     ) {
 382         let interner = builder.interner();
 383         let binders = self.binders.map_ref(|b| &b.where_clauses).cloned();
 384
 385         builder.push_binders(binders, |builder, where_clauses| {
 386             let self_ty = TyKind::Adt(self.id, builder.substitution_in_scope()).intern(interner);
 387
 388             well_formed_program_clauses(builder, self_ty.clone(), where_clauses.iter());
 389
 390             implied_bounds_program_clauses(builder, &self_ty, where_clauses.iter());
 391
 392             fully_visible_program_clauses(
 393                 builder,
 394                 self_ty.clone(),
 395                 &builder.substitution_in_scope(),
 396             );
 397
 398             // Types that are not marked `#[upstream]` satisfy IsLocal(Ty)
 399             if !self.flags.upstream {
 400                 // `IsLocalTy(Ty)` depends *only* on whether the type
 401                 // is marked #[upstream] and nothing else
 402                 builder.push_fact(DomainGoal::IsLocal(self_ty.clone()));
 403             } else if self.flags.fundamental {
 404                 // If a type is `#[upstream]`, but is also
 405                 // `#[fundamental]`, it satisfies IsLocal if and only
 406                 // if its parameters satisfy IsLocal
 407                 for type_param in builder.substitution_in_scope().type_parameters(interner) {
 408                     builder.push_clause(
 409                         DomainGoal::IsLocal(self_ty.clone()),
 410                         Some(DomainGoal::IsLocal(type_param)),
 411                     );
 412                 }
 413                 builder.push_clause(
 414                     DomainGoal::IsUpstream(self_ty.clone()),
 415                     builder
 416                         .substitution_in_scope()
 417                         .type_parameters(interner)
 418                         .map(|type_param| DomainGoal::IsUpstream(type_param)),
 419                 );
 420             } else {
 421                 // The type is just upstream and not fundamental
 422                 builder.push_fact(DomainGoal::IsUpstream(self_ty.clone()));
 423             }
 424
 425             if self.flags.fundamental {
 426                 assert!(
 427                     builder
 428                         .substitution_in_scope()
 429                         .type_parameters(interner)
 430                         .count()
 431                         >= 1,
 432                     "Only fundamental types with type parameters are supported"
 433                 );
 434                 for type_param in builder.substitution_in_scope().type_parameters(interner) {
 435                     builder.push_clause(
 436                         DomainGoal::DownstreamType(self_ty.clone()),
 437                         Some(DomainGoal::DownstreamType(type_param)),
 438                     );
 439                 }
 440             }
 441         });
 442     }
 443 }
 444
 445 impl<I: Interner> ToProgramClauses<I> for FnDefDatum<I> {
 446     /// Given the following function definition: `fn bar<T>() where T: Eq`, generate:
 447     ///
 448     /// ```notrust
 449     /// -- Rule WellFormed-Type
 450     /// forall<T> {
 451     ///     WF(bar<T>) :- WF(T: Eq)
 452     /// }
 453     ///
 454     /// -- Rule Implied-Bound-From-Type
 455     /// forall<T> {
 456     ///     FromEnv(T: Eq) :- FromEnv(bar<T>).
 457     /// }
 458     ///
 459     /// forall<T> {
 460     ///     IsFullyVisible(bar<T>) :- IsFullyVisible(T).
 461     /// }
 462     /// ```
 463     #[instrument(level = "debug", skip(builder))]
 464     fn to_program_clauses(
 465         &self,
 466         builder: &mut ClauseBuilder<'_, I>,
 467         _environment: &Environment<I>,
 468     ) {
 469         let interner = builder.interner();
 470         let binders = self.binders.map_ref(|b| &b.where_clauses).cloned();
 471
 472         builder.push_binders(binders, |builder, where_clauses| {
 473             let ty = TyKind::FnDef(self.id, builder.substitution_in_scope()).intern(interner);
 474
 475             well_formed_program_clauses(builder, ty.clone(), where_clauses.iter());
 476
 477             implied_bounds_program_clauses(builder, &ty, where_clauses.iter());
 478
 479             fully_visible_program_clauses(builder, ty, &builder.substitution_in_scope());
 480         });
 481     }
 482 }
 483
 484 impl<I: Interner> ToProgramClauses<I> for TraitDatum<I> {
 485     /// Given the following trait declaration: `trait Ord<T> where Self: Eq<T> { ... }`, generate:
 486     ///
 487     /// ```notrust
 488     /// -- Rule WellFormed-TraitRef
 489     /// forall<Self, T> {
 490     ///    WF(Self: Ord<T>) :- Implemented(Self: Ord<T>), WF(Self: Eq<T>).
 491     /// }
 492     /// ```
 493     ///
 494     /// and the reverse rules:
 495     ///
 496     /// ```notrust
 497     /// -- Rule Implemented-From-Env
 498     /// forall<Self, T> {
 499     ///    (Self: Ord<T>) :- FromEnv(Self: Ord<T>).
 500     /// }
 501     ///
 502     /// -- Rule Implied-Bound-From-Trait
 503     /// forall<Self, T> {
 504     ///     FromEnv(Self: Eq<T>) :- FromEnv(Self: Ord<T>).
 505     /// }
 506     /// ```
 507     ///
 508     /// As specified in the orphan rules, if a trait is not marked `#[upstream]`, the current crate
 509     /// can implement it for any type. To represent that, we generate:
 510     ///
 511     /// ```notrust
 512     /// // `Ord<T>` would not be `#[upstream]` when compiling `std`
 513     /// forall<Self, T> { LocalImplAllowed(Self: Ord<T>). }
 514     /// ```
 515     ///
 516     /// For traits that are `#[upstream]` (i.e. not in the current crate), the orphan rules dictate
 517     /// that impls are allowed as long as at least one type parameter is local and each type
 518     /// prior to that is fully visible. That means that each type prior to the first local
 519     /// type cannot contain any of the type parameters of the impl.
 520     ///
 521     /// This rule is fairly complex, so we expand it and generate a program clause for each
 522     /// possible case. This is represented as follows:
 523     ///
 524     /// ```notrust
 525     /// // for `#[upstream] trait Foo<T, U, V> where Self: Eq<T> { ... }`
 526     /// forall<Self, T, U, V> {
 527     ///     LocalImplAllowed(Self: Foo<T, U, V>) :- IsLocal(Self).
 528     /// }
 529     ///
 530     /// forall<Self, T, U, V> {
 531     ///     LocalImplAllowed(Self: Foo<T, U, V>) :-
 532     ///         IsFullyVisible(Self),
 533     ///         IsLocal(T).
 534     /// }
 535     ///
 536     /// forall<Self, T, U, V> {
 537     ///     LocalImplAllowed(Self: Foo<T, U, V>) :-
 538     ///         IsFullyVisible(Self),
 539     ///         IsFullyVisible(T),
 540     ///         IsLocal(U).
 541     /// }
 542     ///
 543     /// forall<Self, T, U, V> {
 544     ///     LocalImplAllowed(Self: Foo<T, U, V>) :-
 545     ///         IsFullyVisible(Self),
 546     ///         IsFullyVisible(T),
 547     ///         IsFullyVisible(U),
 548     ///         IsLocal(V).
 549     /// }
 550     /// ```
 551     ///
 552     /// The overlap check uses compatible { ... } mode to ensure that it accounts for impls that
 553     /// may exist in some other *compatible* world. For every upstream trait, we add a rule to
 554     /// account for the fact that upstream crates are able to compatibly add impls of upstream
 555     /// traits for upstream types.
 556     ///
 557     /// ```notrust
 558     /// // For `#[upstream] trait Foo<T, U, V> where Self: Eq<T> { ... }`
 559     /// forall<Self, T, U, V> {
 560     ///     Implemented(Self: Foo<T, U, V>) :-
 561     ///         Implemented(Self: Eq<T>), // where clauses
 562     ///         Compatible,               // compatible modality
 563     ///         IsUpstream(Self),
 564     ///         IsUpstream(T),
 565     ///         IsUpstream(U),
 566     ///         IsUpstream(V),
 567     ///         CannotProve.              // returns ambiguous
 568     /// }
 569     /// ```
 570     ///
 571     /// In certain situations, this is too restrictive. Consider the following code:
 572     ///
 573     /// ```notrust
 574     /// /* In crate std */
 575     /// trait Sized { }
 576     /// struct str { }
 577     ///
 578     /// /* In crate bar (depends on std) */
 579     /// trait Bar { }
 580     /// impl Bar for str { }
 581     /// impl<T> Bar for T where T: Sized { }
 582     /// ```
 583     ///
 584     /// Here, because of the rules we've defined, these two impls overlap. The std crate is
 585     /// upstream to bar, and thus it is allowed to compatibly implement Sized for str. If str
 586     /// can implement Sized in a compatible future, these two impls definitely overlap since the
 587     /// second impl covers all types that implement Sized.
 588     ///
 589     /// The solution we've got right now is to mark Sized as "fundamental" when it is defined.
 590     /// This signals to the Rust compiler that it can rely on the fact that str does not
 591     /// implement Sized in all contexts. A consequence of this is that we can no longer add an
 592     /// implementation of Sized compatibly for str. This is the trade off you make when defining
 593     /// a fundamental trait.
 594     ///
 595     /// To implement fundamental traits, we simply just do not add the rule above that allows
 596     /// upstream types to implement upstream traits. Fundamental traits are not allowed to
 597     /// compatibly do that.
 598     fn to_program_clauses(&self, builder: &mut ClauseBuilder<'_, I>, environment: &Environment<I>) {
 599         let interner = builder.interner();
 600         let binders = self.binders.map_ref(|b| &b.where_clauses).cloned();
 601         builder.push_binders(binders, |builder, where_clauses| {
 602             let trait_ref = chalk_ir::TraitRef {
 603                 trait_id: self.id,
 604                 substitution: builder.substitution_in_scope(),
 605             };
 606
 607             builder.push_clause(
 608                 trait_ref.clone().well_formed(),
 609                 where_clauses
 610                     .iter()
 611                     .cloned()
 612                     .map(|qwc| qwc.into_well_formed_goal(interner))
 613                     .casted::<Goal<_>>(interner)
 614                     .chain(Some(trait_ref.clone().cast(interner))),
 615             );
 616
 617             // The number of parameters will always be at least 1
 618             // because of the Self parameter that is automatically
 619             // added to every trait. This is important because
 620             // otherwise the added program clauses would not have any
 621             // conditions.
 622             let type_parameters: Vec<_> = trait_ref.type_parameters(interner).collect();
 623
 624             if environment.has_compatible_clause(interner) {
 625                 // Note: even though we do check for a `Compatible` clause here,
 626                 // we also keep it as a condition for the clauses below, purely
 627                 // for logical consistency. But really, it's not needed and could be
 628                 // removed.
 629
 630                 // Drop trait can't have downstream implementation because it can only
 631                 // be implemented with the same genericity as the struct definition,
 632                 // i.e. Drop implementation for `struct S<T: Eq> {}` is forced to be
 633                 // `impl Drop<T: Eq> for S<T> { ... }`. That means that orphan rules
 634                 // prevent Drop from being implemented in downstream crates.
 635                 if self.well_known != Some(WellKnownTrait::Drop) {
 636                     // Add all cases for potential downstream impls that could exist
 637                     for i in 0..type_parameters.len() {
 638                         builder.push_clause(
 639                             trait_ref.clone(),
 640                             where_clauses
 641                                 .iter()
 642                                 .cloned()
 643                                 .casted(interner)
 644                                 .chain(iter::once(DomainGoal::Compatible.cast(interner)))
 645                                 .chain((0..i).map(|j| {
 646                                     DomainGoal::IsFullyVisible(type_parameters[j].clone())
 647                                         .cast(interner)
 648                                 }))
 649                                 .chain(iter::once(
 650                                     DomainGoal::DownstreamType(type_parameters[i].clone())
 651                                         .cast(interner),
 652                                 ))
 653                                 .chain(iter::once(GoalData::CannotProve.intern(interner))),
 654                         );
 655                     }
 656                 }
 657
 658                 // Fundamental traits can be reasoned about negatively without any ambiguity, so no
 659                 // need for this rule if the trait is fundamental.
 660                 if !self.flags.fundamental {
 661                     builder.push_clause(
 662                         trait_ref.clone(),
 663                         where_clauses
 664                             .iter()
 665                             .cloned()
 666                             .casted(interner)
 667                             .chain(iter::once(DomainGoal::Compatible.cast(interner)))
 668                             .chain(
 669                                 trait_ref
 670                                     .type_parameters(interner)
 671                                     .map(|ty| DomainGoal::IsUpstream(ty).cast(interner)),
 672                             )
 673                             .chain(iter::once(GoalData::CannotProve.intern(interner))),
 674                     );
 675                 }
 676             }
 677
 678             // Orphan rules:
 679             if !self.flags.upstream {
 680                 // Impls for traits declared locally always pass the impl rules
 681                 builder.push_fact(DomainGoal::LocalImplAllowed(trait_ref.clone()));
 682             } else {
 683                 // Impls for remote traits must have a local type in the right place
 684                 for i in 0..type_parameters.len() {
 685                     builder.push_clause(
 686                         DomainGoal::LocalImplAllowed(trait_ref.clone()),
 687                         (0..i)
 688                             .map(|j| DomainGoal::IsFullyVisible(type_parameters[j].clone()))
 689                             .chain(Some(DomainGoal::IsLocal(type_parameters[i].clone()))),
 690                     );
 691                 }
 692             }
 693
 694             // Reverse implied bound rules: given (e.g.) `trait Foo: Bar + Baz`,
 695             // we create rules like:
 696             //
 697             // ```
 698             // FromEnv(T: Bar) :- FromEnv(T: Foo)
 699             // ```
 700             //
 701             // and
 702             //
 703             // ```
 704             // FromEnv(T: Baz) :- FromEnv(T: Foo)
 705             // ```
 706             for qwc in where_clauses {
 707                 builder.push_binders(qwc, |builder, wc| {
 708                     builder.push_clause(
 709                         wc.into_from_env_goal(interner),
 710                         Some(trait_ref.clone().from_env()),
 711                     );
 712                 });
 713             }
 714
 715             // Finally, for every trait `Foo` we make a rule
 716             //
 717             // ```
 718             // Implemented(T: Foo) :- FromEnv(T: Foo)
 719             // ```
 720             builder.push_clause(trait_ref.clone(), Some(trait_ref.from_env()));
 721         });
 722     }
 723 }
 724
 725 impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
 726     /// For each associated type, we define the "projection
 727     /// equality" rules. There are always two; one for a successful normalization,
 728     /// and one for the "fallback" notion of equality.
 729     ///
 730     /// Given: (here, `'a` and `T` represent zero or more parameters)
 731     ///
 732     /// ```notrust
 733     /// trait Foo {
 734     ///     type Assoc<'a, T>: Bounds where WC;
 735     /// }
 736     /// ```
 737     ///
 738     /// we generate the 'fallback' rule:
 739     ///
 740     /// ```notrust
 741     /// -- Rule AliasEq-Placeholder
 742     /// forall<Self, 'a, T> {
 743     ///     AliasEq(<Self as Foo>::Assoc<'a, T> = (Foo::Assoc<'a, T>)<Self>).
 744     /// }
 745     /// ```
 746     ///
 747     /// and
 748     ///
 749     /// ```notrust
 750     /// -- Rule AliasEq-Normalize
 751     /// forall<Self, 'a, T, U> {
 752     ///     AliasEq(<T as Foo>::Assoc<'a, T> = U) :-
 753     ///         Normalize(<T as Foo>::Assoc -> U).
 754     /// }
 755     /// ```
 756     ///
 757     /// We used to generate an "elaboration" rule like this:
 758     ///
 759     /// ```notrust
 760     /// forall<T> {
 761     ///     T: Foo :- exists<U> { AliasEq(<T as Foo>::Assoc = U) }.
 762     /// }
 763     /// ```
 764     ///
 765     /// but this caused problems with the recursive solver. In
 766     /// particular, whenever normalization is possible, we cannot
 767     /// solve that projection uniquely, since we can now elaborate
 768     /// `AliasEq` to fallback *or* normalize it. So instead we
 769     /// handle this kind of reasoning through the `FromEnv` predicate.
 770     ///
 771     /// We also generate rules specific to WF requirements and implied bounds:
 772     ///
 773     /// ```notrust
 774     /// -- Rule WellFormed-AssocTy
 775     /// forall<Self, 'a, T> {
 776     ///     WellFormed((Foo::Assoc)<Self, 'a, T>) :- WellFormed(Self: Foo), WellFormed(WC).
 777     /// }
 778     ///
 779     /// -- Rule Implied-WC-From-AssocTy
 780     /// forall<Self, 'a, T> {
 781     ///     FromEnv(WC) :- FromEnv((Foo::Assoc)<Self, 'a, T>).
 782     /// }
 783     ///
 784     /// -- Rule Implied-Bound-From-AssocTy
 785     /// forall<Self, 'a, T> {
 786     ///     FromEnv(<Self as Foo>::Assoc<'a,T>: Bounds) :- FromEnv(Self: Foo), WC.
 787     /// }
 788     ///
 789     /// -- Rule Implied-Trait-From-AssocTy
 790     /// forall<Self,'a, T> {
 791     ///     FromEnv(Self: Foo) :- FromEnv((Foo::Assoc)<Self, 'a,T>).
 792     /// }
 793     /// ```
 794     fn to_program_clauses(
 795         &self,
 796         builder: &mut ClauseBuilder<'_, I>,
 797         _environment: &Environment<I>,
 798     ) {
 799         let interner = builder.interner();
 800         let binders = self.binders.clone();
 801         builder.push_binders(
 802             binders,
 803             |builder,
 804              AssociatedTyDatumBound {
 805                  where_clauses,
 806                  bounds,
 807              }| {
 808                 let substitution = builder.substitution_in_scope();
 809
 810                 let projection = ProjectionTy {
 811                     associated_ty_id: self.id,
 812                     substitution: substitution.clone(),
 813                 };
 814                 let projection_ty = AliasTy::Projection(projection.clone()).intern(interner);
 815
 816                 // Retrieve the trait ref embedding the associated type
 817                 let trait_ref = builder.db.trait_ref_from_projection(&projection);
 818
 819                 // Construct an application from the projection. So if we have `<T as Iterator>::Item`,
 820                 // we would produce `(Iterator::Item)<T>`.
 821                 let ty = TyKind::AssociatedType(self.id, substitution).intern(interner);
 822
 823                 let projection_eq = AliasEq {
 824                     alias: AliasTy::Projection(projection.clone()),
 825                     ty: ty.clone(),
 826                 };
 827
 828                 // Fallback rule. The solver uses this to move between the projection
 829                 // and placeholder type.
 830                 //
 831                 //    forall<Self> {
 832                 //        AliasEq(<Self as Foo>::Assoc = (Foo::Assoc)<Self>).
 833                 //    }
 834                 builder.push_fact_with_priority(projection_eq, None, ClausePriority::Low);
 835
 836                 // Well-formedness of projection type.
 837                 //
 838                 //    forall<Self> {
 839                 //        WellFormed((Foo::Assoc)<Self>) :- WellFormed(Self: Foo), WellFormed(WC).
 840                 //    }
 841                 builder.push_clause(
 842                     WellFormed::Ty(ty.clone()),
 843                     iter::once(WellFormed::Trait(trait_ref.clone()).cast::<Goal<_>>(interner))
 844                         .chain(
 845                             where_clauses
 846                                 .iter()
 847                                 .cloned()
 848                                 .map(|qwc| qwc.into_well_formed_goal(interner))
 849                                 .casted(interner),
 850                         ),
 851                 );
 852
 853                 // Assuming well-formedness of projection type means we can assume
 854                 // the trait ref as well. Mostly used in function bodies.
 855                 //
 856                 //    forall<Self> {
 857                 //        FromEnv(Self: Foo) :- FromEnv((Foo::Assoc)<Self>).
 858                 //    }
 859                 builder.push_clause(FromEnv::Trait(trait_ref.clone()), Some(ty.from_env()));
 860
 861                 // Reverse rule for where clauses.
 862                 //
 863                 //    forall<Self> {
 864                 //        FromEnv(WC) :- FromEnv((Foo::Assoc)<Self>).
 865                 //    }
 866                 //
 867                 // This is really a family of clauses, one for each where clause.
 868                 for qwc in &where_clauses {
 869                     builder.push_binders(qwc.clone(), |builder, wc| {
 870                         builder.push_clause(
 871                             wc.into_from_env_goal(interner),
 872                             Some(FromEnv::Ty(ty.clone())),
 873                         );
 874                     });
 875                 }
 876
 877                 // Reverse rule for implied bounds.
 878                 //
 879                 //    forall<Self> {
 880                 //        FromEnv(<Self as Foo>::Assoc: Bounds) :- FromEnv(Self: Foo), WC
 881                 //    }
 882                 for quantified_bound in bounds {
 883                     builder.push_binders(quantified_bound, |builder, bound| {
 884                         for wc in bound.into_where_clauses(interner, projection_ty.clone()) {
 885                             builder.push_clause(
 886                                 wc.into_from_env_goal(interner),
 887                                 iter::once(
 888                                     FromEnv::Trait(trait_ref.clone()).cast::<Goal<_>>(interner),
 889                                 )
 890                                 .chain(where_clauses.iter().cloned().casted(interner)),
 891                             );
 892                         }
 893                     });
 894                 }
 895
 896                 // add new type parameter U
 897                 builder.push_bound_ty(|builder, ty| {
 898                     // `Normalize(<T as Foo>::Assoc -> U)`
 899                     let normalize = Normalize {
 900                         alias: AliasTy::Projection(projection.clone()),
 901                         ty: ty.clone(),
 902                     };
 903
 904                     // `AliasEq(<T as Foo>::Assoc = U)`
 905                     let projection_eq = AliasEq {
 906                         alias: AliasTy::Projection(projection),
 907                         ty,
 908                     };
 909
 910                     // Projection equality rule from above.
 911                     //
 912                     //    forall<T, U> {
 913                     //        AliasEq(<T as Foo>::Assoc = U) :-
 914                     //            Normalize(<T as Foo>::Assoc -> U).
 915                     //    }
 916                     builder.push_clause(projection_eq, Some(normalize));
 917                 });
 918             },
 919         );
 920     }
 921 }