chalk_solve/clauses/program_clauses.rs
1use crate::clauses::builder::ClauseBuilder;
2use crate::rust_ir::*;
3use crate::split::Split;
4use chalk_ir::cast::{Cast, Caster};
5use chalk_ir::interner::Interner;
6use chalk_ir::*;
7use std::iter;
8use 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.
13pub trait ToProgramClauses<I: Interner> {
14 fn to_program_clauses(&self, builder: &mut ClauseBuilder<'_, I>, environment: &Environment<I>);
15}
16
17impl<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
52impl<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
137impl<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)
237fn 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`
273fn 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).
308fn 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
325impl<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
445impl<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
484impl<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
725impl<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 /// Another set of clauses we generate for each associated type is about placeholder associated
772 /// types (i.e. `TyKind::AssociatedType`). Given
773 ///
774 /// ```notrust
775 /// trait Foo {
776 /// type Assoc<'a, T>: Bar<U = Ty> where WC;
777 /// }
778 /// ```
779 ///
780 /// we generate
781 ///
782 /// ```notrust
783 /// forall<Self, 'a, T> {
784 /// Implemented((Foo::Assoc<'a, T>)<Self>: Bar) :- WC.
785 /// AliasEq(<<(Foo::Assoc<'a, T>)<Self>> as Bar>::U = Ty) :- WC.
786 /// }
787 /// ```
788 ///
789 /// We also generate rules specific to WF requirements and implied bounds:
790 ///
791 /// ```notrust
792 /// -- Rule WellFormed-AssocTy
793 /// forall<Self, 'a, T> {
794 /// WellFormed((Foo::Assoc)<Self, 'a, T>) :- WellFormed(Self: Foo), WellFormed(WC).
795 /// }
796 ///
797 /// -- Rule Implied-WC-From-AssocTy
798 /// forall<Self, 'a, T> {
799 /// FromEnv(WC) :- FromEnv((Foo::Assoc)<Self, 'a, T>).
800 /// }
801 ///
802 /// -- Rule Implied-Bound-From-AssocTy
803 /// forall<Self, 'a, T> {
804 /// FromEnv(<Self as Foo>::Assoc<'a,T>: Bounds) :- FromEnv(Self: Foo), WC.
805 /// }
806 ///
807 /// -- Rule Implied-Trait-From-AssocTy
808 /// forall<Self,'a, T> {
809 /// FromEnv(Self: Foo) :- FromEnv((Foo::Assoc)<Self, 'a,T>).
810 /// }
811 /// ```
812 fn to_program_clauses(
813 &self,
814 builder: &mut ClauseBuilder<'_, I>,
815 _environment: &Environment<I>,
816 ) {
817 let interner = builder.interner();
818 let binders = self.binders.clone();
819 builder.push_binders(
820 binders,
821 |builder,
822 AssociatedTyDatumBound {
823 where_clauses,
824 bounds,
825 }| {
826 let substitution = builder.substitution_in_scope();
827
828 let projection = ProjectionTy {
829 associated_ty_id: self.id,
830 substitution: substitution.clone(),
831 };
832 let projection_ty = AliasTy::Projection(projection.clone()).intern(interner);
833
834 // Retrieve the trait ref embedding the associated type
835 let trait_ref = builder.db.trait_ref_from_projection(&projection);
836
837 // Construct an application from the projection. So if we have `<T as Iterator>::Item`,
838 // we would produce `(Iterator::Item)<T>`.
839 let placeholder_ty = TyKind::AssociatedType(self.id, substitution).intern(interner);
840
841 let projection_eq = AliasEq {
842 alias: AliasTy::Projection(projection.clone()),
843 ty: placeholder_ty.clone(),
844 };
845
846 // Fallback rule. The solver uses this to move between the projection
847 // and placeholder type.
848 //
849 // forall<Self> {
850 // AliasEq(<Self as Foo>::Assoc = (Foo::Assoc)<Self>).
851 // }
852 builder.push_fact_with_priority(projection_eq, None, ClausePriority::Low);
853
854 // Well-formedness of projection type.
855 //
856 // forall<Self> {
857 // WellFormed((Foo::Assoc)<Self>) :- WellFormed(Self: Foo), WellFormed(WC).
858 // }
859 builder.push_clause(
860 WellFormed::Ty(placeholder_ty.clone()),
861 iter::once(WellFormed::Trait(trait_ref.clone()).cast::<Goal<_>>(interner))
862 .chain(
863 where_clauses
864 .iter()
865 .cloned()
866 .map(|qwc| qwc.into_well_formed_goal(interner))
867 .casted(interner),
868 ),
869 );
870
871 // Assuming well-formedness of projection type means we can assume
872 // the trait ref as well. Mostly used in function bodies.
873 //
874 // forall<Self> {
875 // FromEnv(Self: Foo) :- FromEnv((Foo::Assoc)<Self>).
876 // }
877 builder.push_clause(
878 FromEnv::Trait(trait_ref.clone()),
879 Some(placeholder_ty.from_env()),
880 );
881
882 // Reverse rule for where clauses.
883 //
884 // forall<Self> {
885 // FromEnv(WC) :- FromEnv((Foo::Assoc)<Self>).
886 // }
887 //
888 // This is really a family of clauses, one for each where clause.
889 for qwc in &where_clauses {
890 builder.push_binders(qwc.clone(), |builder, wc| {
891 builder.push_clause(
892 wc.into_from_env_goal(interner),
893 Some(FromEnv::Ty(placeholder_ty.clone())),
894 );
895 });
896 }
897
898 for quantified_bound in bounds {
899 builder.push_binders(quantified_bound, |builder, bound| {
900 // Reverse rule for implied bounds.
901 //
902 // forall<Self> {
903 // FromEnv(<Self as Foo>::Assoc: Bounds) :- FromEnv(Self: Foo), WC
904 // }
905 for wc in bound.into_where_clauses(interner, projection_ty.clone()) {
906 builder.push_clause(
907 wc.into_from_env_goal(interner),
908 iter::once(
909 FromEnv::Trait(trait_ref.clone()).cast::<Goal<_>>(interner),
910 )
911 .chain(where_clauses.iter().cloned().casted(interner)),
912 );
913 }
914
915 // Rules for the corresponding placeholder type.
916 //
917 // When `Foo::Assoc` has a bound `type Assoc: Trait<T = Ty>`, we generate:
918 //
919 // forall<Self> {
920 // Implemented((Foo::Assoc)<Self>: Trait) :- WC
921 // AliasEq(<(Foo::Assoc)<Self> as Trait>::T = Ty) :- WC
922 // }
923 for wc in bound.into_where_clauses(interner, placeholder_ty.clone()) {
924 builder.push_clause(wc, where_clauses.iter().cloned());
925 }
926 });
927 }
928
929 // add new type parameter U
930 builder.push_bound_ty(|builder, ty| {
931 // `Normalize(<T as Foo>::Assoc -> U)`
932 let normalize = Normalize {
933 alias: AliasTy::Projection(projection.clone()),
934 ty: ty.clone(),
935 };
936
937 // `AliasEq(<T as Foo>::Assoc = U)`
938 let projection_eq = AliasEq {
939 alias: AliasTy::Projection(projection),
940 ty,
941 };
942
943 // Projection equality rule from above.
944 //
945 // forall<T, U> {
946 // AliasEq(<T as Foo>::Assoc = U) :-
947 // Normalize(<T as Foo>::Assoc -> U).
948 // }
949 builder.push_clause(projection_eq, Some(normalize));
950 });
951 },
952 );
953 }
954}