1 use self::builder
::ClauseBuilder
;
2 use self::env_elaborator
::elaborate_env_clauses
;
3 use self::program_clauses
::ToProgramClauses
;
4 use crate::goal_builder
::GoalBuilder
;
5 use crate::split
::Split
;
6 use crate::RustIrDatabase
;
7 use chalk_ir
::cast
::{Cast, Caster}
;
8 use chalk_ir
::could_match
::CouldMatch
;
9 use chalk_ir
::interner
::Interner
;
11 use rustc_hash
::FxHashSet
;
13 use tracing
::{debug, instrument}
;
20 pub mod program_clauses
;
22 // yields the types "contained" in `app_ty`
23 fn constituent_types
<I
: Interner
>(db
: &dyn RustIrDatabase
<I
>, ty
: &TyKind
<I
>) -> Vec
<Ty
<I
>> {
24 let interner
= db
.interner();
27 // For non-phantom_data adts we collect its variants/fields
28 TyKind
::Adt(adt_id
, substitution
) if !db
.adt_datum(*adt_id
).flags
.phantom_data
=> {
29 let adt_datum
= &db
.adt_datum(*adt_id
);
30 let adt_datum_bound
= adt_datum
.binders
.clone().substitute(interner
, substitution
);
34 .flat_map(|variant
| variant
.fields
.into_iter())
37 // And for `PhantomData<T>`, we pass `T`.
38 TyKind
::Adt(_
, substitution
)
39 | TyKind
::Tuple(_
, substitution
)
40 | TyKind
::FnDef(_
, substitution
) => substitution
42 .filter_map(|x
| x
.ty(interner
))
46 TyKind
::Array(ty
, _
) | TyKind
::Slice(ty
) | TyKind
::Raw(_
, ty
) | TyKind
::Ref(_
, _
, ty
) => {
50 TyKind
::Str
| TyKind
::Never
| TyKind
::Scalar(_
) => Vec
::new(),
52 TyKind
::Generator(generator_id
, substitution
) => {
53 let generator_datum
= &db
.generator_datum(*generator_id
);
54 let generator_datum_bound
= generator_datum
57 .substitute(interner
, &substitution
);
59 let mut tys
= generator_datum_bound
.upvars
;
61 TyKind
::GeneratorWitness(*generator_id
, substitution
.clone()).intern(interner
),
66 TyKind
::Closure(_
, _
) => panic
!("this function should not be called for closures"),
67 TyKind
::GeneratorWitness(_
, _
) => {
68 panic
!("this function should not be called for generator witnesses")
70 TyKind
::Function(_
) => panic
!("this function should not be called for functions"),
71 TyKind
::InferenceVar(_
, _
) | TyKind
::BoundVar(_
) => {
72 panic
!("this function should not be called for inference or bound vars")
74 TyKind
::Placeholder(_
) => panic
!("this function should not be called for placeholders"),
75 TyKind
::Dyn(_
) => panic
!("this function should not be called for dyn types"),
76 TyKind
::Alias(_
) => panic
!("this function should not be called for alias"),
77 TyKind
::Foreign(_
) => panic
!("constituent_types of foreign types are unknown!"),
78 TyKind
::Error
=> Vec
::new(),
79 TyKind
::OpaqueType(_
, _
) => panic
!("constituent_types of opaque types are unknown!"),
80 TyKind
::AssociatedType(_
, _
) => {
81 panic
!("constituent_types of associated types are unknown!")
86 /// FIXME(#505) update comments for ADTs
87 /// For auto-traits, we generate a default rule for every struct,
88 /// unless there is a manual impl for that struct given explicitly.
90 /// So, if you have `impl Send for MyList<Foo>`, then we would
91 /// generate no rule for `MyList` at all -- similarly if you have
92 /// `impl !Send for MyList<Foo>`, or `impl<T> Send for MyList<T>`.
94 /// But if you have no rules at all for `Send` / `MyList`, then we
95 /// generate an impl based on the field types of `MyList`. For example
96 /// given the following program:
99 /// #[auto] trait Send { }
101 /// struct MyList<T> {
103 /// next: Box<Option<MyList<T>>>,
112 /// Implemented(MyList<T>: Send) :-
113 /// Implemented(T: Send),
114 /// Implemented(Box<Option<MyList<T>>>: Send).
117 #[instrument(level = "debug", skip(builder))]
118 pub fn push_auto_trait_impls
<I
: Interner
>(
119 builder
: &mut ClauseBuilder
<'_
, I
>,
120 auto_trait_id
: TraitId
<I
>,
122 ) -> Result
<(), Floundered
> {
123 let interner
= builder
.interner();
125 // Must be an auto trait.
126 assert
!(builder
.db
.trait_datum(auto_trait_id
).is_auto_trait());
128 // Auto traits never have generic parameters of their own (apart from `Self`).
130 builder
.db
.trait_datum(auto_trait_id
).binders
.len(interner
),
134 // If there is a `impl AutoTrait for Foo<..>` or `impl !AutoTrait
135 // for Foo<..>`, where `Foo` is the adt we're looking at, then
136 // we don't generate our own rules.
137 if builder
.db
.impl_provided_for(auto_trait_id
, ty
) {
138 debug
!("impl provided");
142 let mk_ref
= |ty
: Ty
<I
>| TraitRef
{
143 trait_id
: auto_trait_id
,
144 substitution
: Substitution
::from1(interner
, ty
.cast(interner
)),
147 let consequence
= mk_ref(ty
.clone().intern(interner
));
150 // function-types implement auto traits unconditionally
151 TyKind
::Function(_
) => {
152 let auto_trait_ref
= TraitRef
{
153 trait_id
: auto_trait_id
,
154 substitution
: Substitution
::from1(interner
, ty
.clone().intern(interner
)),
157 builder
.push_fact(auto_trait_ref
);
160 TyKind
::InferenceVar(_
, _
) | TyKind
::BoundVar(_
) => Err(Floundered
),
162 // auto traits are not implemented for foreign types
163 TyKind
::Foreign(_
) => Ok(()),
165 // closures require binders, while the other types do not
166 TyKind
::Closure(closure_id
, _
) => {
167 let binders
= builder
169 .closure_upvars(*closure_id
, &Substitution
::empty(interner
));
170 builder
.push_binders(binders
, |builder
, upvar_ty
| {
171 let conditions
= iter
::once(mk_ref(upvar_ty
));
172 builder
.push_clause(consequence
, conditions
);
177 TyKind
::GeneratorWitness(generator_id
, _
) => {
178 push_auto_trait_impls_generator_witness(builder
, auto_trait_id
, *generator_id
);
182 TyKind
::OpaqueType(opaque_ty_id
, _
) => {
183 push_auto_trait_impls_opaque(builder
, auto_trait_id
, *opaque_ty_id
);
188 TyKind
::AssociatedType(_
, _
)
189 | TyKind
::Placeholder(_
)
191 | TyKind
::Alias(_
) => Ok(()),
193 // app_ty implements AutoTrait if all constituents of app_ty implement AutoTrait
195 let conditions
= constituent_types(builder
.db
, ty
).into_iter().map(mk_ref
);
197 builder
.push_clause(consequence
, conditions
);
203 /// Leak auto traits for opaque types, just like `push_auto_trait_impls` does for structs.
205 /// For example, given the following program:
208 /// #[auto] trait Send { }
211 /// opaque type Foo: Trait = Bar
213 /// Checking the goal `Foo: Send` would generate the following:
216 /// Foo: Send :- Bar: Send
218 #[instrument(level = "debug", skip(builder))]
219 pub fn push_auto_trait_impls_opaque
<I
: Interner
>(
220 builder
: &mut ClauseBuilder
<'_
, I
>,
221 auto_trait_id
: TraitId
<I
>,
222 opaque_id
: OpaqueTyId
<I
>,
224 let opaque_ty_datum
= &builder
.db
.opaque_ty_data(opaque_id
);
225 let interner
= builder
.interner();
227 // Must be an auto trait.
228 assert
!(builder
.db
.trait_datum(auto_trait_id
).is_auto_trait());
230 // Auto traits never have generic parameters of their own (apart from `Self`).
232 builder
.db
.trait_datum(auto_trait_id
).binders
.len(interner
),
236 let hidden_ty
= builder
.db
.hidden_opaque_type(opaque_id
);
237 let binders
= opaque_ty_datum
.bound
.clone();
238 builder
.push_binders(binders
, |builder
, _
| {
240 TyKind
::OpaqueType(opaque_id
, builder
.substitution_in_scope()).intern(interner
);
242 // trait_ref = `OpaqueType<...>: MyAutoTrait`
243 let auto_trait_ref
= TraitRef
{
244 trait_id
: auto_trait_id
,
245 substitution
: Substitution
::from1(interner
, self_ty
),
248 // OpaqueType<...>: MyAutoTrait :- HiddenType: MyAutoTrait
251 std
::iter
::once(TraitRef
{
252 trait_id
: auto_trait_id
,
253 substitution
: Substitution
::from1(interner
, hidden_ty
.clone()),
259 #[instrument(level = "debug", skip(builder))]
260 pub fn push_auto_trait_impls_generator_witness
<I
: Interner
>(
261 builder
: &mut ClauseBuilder
<'_
, I
>,
262 auto_trait_id
: TraitId
<I
>,
263 generator_id
: GeneratorId
<I
>,
265 let witness_datum
= builder
.db
.generator_witness_datum(generator_id
);
266 let interner
= builder
.interner();
268 // Must be an auto trait.
269 assert
!(builder
.db
.trait_datum(auto_trait_id
).is_auto_trait());
271 // Auto traits never have generic parameters of their own (apart from `Self`).
273 builder
.db
.trait_datum(auto_trait_id
).binders
.len(interner
),
277 // Push binders for the generator generic parameters. These can be used by
278 // both upvars and witness types
279 builder
.push_binders(witness_datum
.inner_types
.clone(), |builder
, inner_types
| {
280 let witness_ty
= TyKind
::GeneratorWitness(generator_id
, builder
.substitution_in_scope())
283 // trait_ref = `GeneratorWitness<...>: MyAutoTrait`
284 let auto_trait_ref
= TraitRef
{
285 trait_id
: auto_trait_id
,
286 substitution
: Substitution
::from1(interner
, witness_ty
),
289 // Create a goal of the form:
290 // forall<L0, L1, ..., LN> {
291 // WitnessType1<L0, L1, ... LN, P0, P1, ..., PN>: MyAutoTrait,
293 // WitnessTypeN<L0, L1, ... LN, P0, P1, ..., PN>: MyAutoTrait,
297 // where `L0, L1, ...LN` are our existentially bound witness lifetimes,
298 // and `P0, P1, ..., PN` are the normal generator generics.
300 // We create a 'forall' goal due to the fact that our witness lifetimes
301 // are *existentially* quantified - the precise reigon is erased during
302 // type checking, so we just know that the type takes *some* region
303 // as a parameter. Therefore, we require that the auto trait bound
304 // hold for *all* regions, which guarantees that the bound will
305 // hold for the original lifetime (before it was erased).
307 // This does not take into account well-formed information from
308 // the witness types. For example, if we have the type
309 // `struct Foo<'a, 'b> { val: &'a &'b u8 }`
310 // then `'b: 'a` must hold for `Foo<'a, 'b>` to be well-formed.
311 // If we have `Foo<'a, 'b>` stored as a witness type, we will
312 // not currently use this information to determine a more precise
313 // relationship between 'a and 'b. In the future, we will likely
314 // do this to avoid incorrectly rejecting correct code.
315 let gb
= &mut GoalBuilder
::new(builder
.db
);
316 let witness_goal
= gb
.forall(
319 |gb
, _subst
, types
, auto_trait_id
| {
322 GoalData
::All(Goals
::from_iter(
324 types
.iter().map(|witness_ty
| TraitRef
{
325 trait_id
: auto_trait_id
,
326 substitution
: Substitution
::from1(gb
.interner(), witness_ty
.clone()),
333 // GeneratorWitnessType: AutoTrait :- forall<...> ...
334 // where 'forall<...> ...' is the goal described above.
335 builder
.push_clause(auto_trait_ref
, std
::iter
::once(witness_goal
));
339 /// Given some goal `goal` that must be proven, along with
340 /// its `environment`, figures out the program clauses that apply
341 /// to this goal from the Rust program. So for example if the goal
342 /// is `Implemented(T: Clone)`, then this function might return clauses
343 /// derived from the trait `Clone` and its impls.
344 #[instrument(level = "debug", skip(db))]
345 pub fn program_clauses_for_goal
<'db
, I
: Interner
>(
346 db
: &'db
dyn RustIrDatabase
<I
>,
347 goal
: &UCanonical
<InEnvironment
<DomainGoal
<I
>>>,
348 ) -> Result
<Vec
<ProgramClause
<I
>>, Floundered
> {
349 let interner
= db
.interner();
351 let custom_clauses
= db
.custom_clauses().into_iter();
352 let clauses_that_could_match
=
353 program_clauses_that_could_match(db
, goal
).map(|cl
| cl
.into_iter())?
;
355 let clauses
: Vec
<ProgramClause
<I
>> = custom_clauses
356 .chain(clauses_that_could_match
)
358 db
.program_clauses_for_env(&goal
.canonical
.value
.environment
)
365 db
.unification_database(),
366 &goal
.canonical
.value
.goal
,
376 /// Returns a set of program clauses that could possibly match
377 /// `goal`. This can be any superset of the correct set, but the
378 /// more precise you can make it, the more efficient solving will
380 #[instrument(level = "debug", skip(db))]
381 pub fn program_clauses_that_could_match
<I
: Interner
>(
382 db
: &dyn RustIrDatabase
<I
>,
383 goal
: &UCanonical
<InEnvironment
<DomainGoal
<I
>>>,
384 ) -> Result
<Vec
<ProgramClause
<I
>>, Floundered
> {
385 let interner
= db
.interner();
386 let mut clauses
: Vec
<ProgramClause
<I
>> = vec
![];
387 let builder
= &mut ClauseBuilder
::new(db
, &mut clauses
);
392 value
: InEnvironment { environment, goal }
,
399 DomainGoal
::Holds(WhereClause
::Implemented(trait_ref
)) => {
400 let self_ty
= trait_ref
.self_type_parameter(interner
);
402 let trait_id
= trait_ref
.trait_id
;
403 let trait_datum
= db
.trait_datum(trait_id
);
405 match self_ty
.kind(interner
) {
406 TyKind
::InferenceVar(_
, _
) => {
407 panic
!("Inference vars not allowed when getting program clauses")
409 TyKind
::Alias(alias
) => {
410 // An alias could normalize to anything, including `dyn trait`
411 // or an opaque type, so push a clause that asks for the
412 // self type to be normalized and return.
413 push_alias_implemented_clause(builder
, trait_ref
.clone(), alias
.clone());
417 _
if self_ty
.is_general_var(interner
, binders
) => {
418 if trait_datum
.is_non_enumerable_trait() || trait_datum
.is_auto_trait() {
419 return Err(Floundered
);
423 TyKind
::OpaqueType(opaque_ty_id
, _
) => {
424 db
.opaque_ty_data(*opaque_ty_id
)
425 .to_program_clauses(builder
, environment
);
429 // If the self type is a `dyn trait` type, generate program-clauses
430 // that indicates that it implements its own traits.
431 // FIXME: This is presently rather wasteful, in that we don't check that the
432 // these program clauses we are generating are actually relevant to the goal
433 // `goal` that we are actually *trying* to prove (though there is some later
434 // code that will screen out irrelevant stuff).
436 // In other words, if we were trying to prove `Implemented(dyn
437 // Fn(&u8): Clone)`, we would still generate two clauses that are
438 // totally irrelevant to that goal, because they let us prove other
439 // things but not `Clone`.
440 dyn_ty
::build_dyn_self_ty_clauses(db
, builder
, self_ty
.clone())
443 // We don't actually do anything here, but we need to record the types when logging
444 TyKind
::Adt(adt_id
, _
) => {
445 let _
= db
.adt_datum(*adt_id
);
448 TyKind
::FnDef(fn_def_id
, _
) => {
449 let _
= db
.fn_def_datum(*fn_def_id
);
455 // This is needed for the coherence related impls, as well
456 // as for the `Implemented(Foo) :- FromEnv(Foo)` rule.
457 trait_datum
.to_program_clauses(builder
, environment
);
459 for impl_id
in db
.impls_for_trait(
461 trait_ref
.substitution
.as_slice(interner
),
464 db
.impl_datum(impl_id
)
465 .to_program_clauses(builder
, environment
);
468 // If this is a `Foo: Send` (or any auto-trait), then add
469 // the automatic impls for `Foo`.
470 let trait_datum
= db
.trait_datum(trait_id
);
471 if trait_datum
.is_auto_trait() {
472 let generalized
= generalize
::Generalize
::apply(db
.interner(), trait_ref
.clone());
473 builder
.push_binders(generalized
, |builder
, trait_ref
| {
474 let ty
= trait_ref
.self_type_parameter(interner
);
475 push_auto_trait_impls(builder
, trait_id
, &ty
.kind(interner
))
479 if let Some(well_known
) = trait_datum
.well_known
{
480 builtin_traits
::add_builtin_program_clauses(
489 DomainGoal
::Holds(WhereClause
::AliasEq(alias_eq
)) => match &alias_eq
.alias
{
490 AliasTy
::Projection(proj
) => {
491 let trait_self_ty
= db
492 .trait_ref_from_projection(proj
)
493 .self_type_parameter(interner
);
495 match trait_self_ty
.kind(interner
) {
496 TyKind
::Alias(alias
) => {
497 // An alias could normalize to anything, including an
498 // opaque type, so push a clause that asks for the self
499 // type to be normalized and return.
500 push_alias_alias_eq_clause(
508 TyKind
::OpaqueType(opaque_ty_id
, _
) => {
509 db
.opaque_ty_data(*opaque_ty_id
)
510 .to_program_clauses(builder
, environment
);
512 // If the self type is a `dyn trait` type, generate program-clauses
513 // for any associated type bindings it contains.
514 // FIXME: see the fixme for the analogous code for Implemented goals.
516 dyn_ty
::build_dyn_self_ty_clauses(db
, builder
, trait_self_ty
.clone())
521 db
.associated_ty_data(proj
.associated_ty_id
)
522 .to_program_clauses(builder
, environment
)
524 AliasTy
::Opaque(opaque_ty
) => db
525 .opaque_ty_data(opaque_ty
.opaque_ty_id
)
526 .to_program_clauses(builder
, environment
),
528 DomainGoal
::Holds(WhereClause
::LifetimeOutlives(..)) => {
529 builder
.push_bound_lifetime(|builder
, a
| {
530 builder
.push_bound_lifetime(|builder
, b
| {
531 builder
.push_fact_with_constraints(
532 DomainGoal
::Holds(WhereClause
::LifetimeOutlives(LifetimeOutlives
{
536 Some(InEnvironment
::new(
537 &Environment
::new(interner
),
538 Constraint
::LifetimeOutlives(a
, b
),
544 DomainGoal
::Holds(WhereClause
::TypeOutlives(..)) => {
545 builder
.push_bound_ty(|builder
, ty
| {
546 builder
.push_bound_lifetime(|builder
, lifetime
| {
547 builder
.push_fact_with_constraints(
548 DomainGoal
::Holds(WhereClause
::TypeOutlives(TypeOutlives
{
550 lifetime
: lifetime
.clone(),
552 Some(InEnvironment
::new(
553 &Environment
::new(interner
),
554 Constraint
::TypeOutlives(ty
, lifetime
),
560 DomainGoal
::WellFormed(WellFormed
::Trait(trait_ref
))
561 | DomainGoal
::LocalImplAllowed(trait_ref
) => {
562 db
.trait_datum(trait_ref
.trait_id
)
563 .to_program_clauses(builder
, environment
);
565 DomainGoal
::ObjectSafe(trait_id
) => {
566 if builder
.db
.is_object_safe(*trait_id
) {
567 builder
.push_fact(DomainGoal
::ObjectSafe(*trait_id
));
570 DomainGoal
::WellFormed(WellFormed
::Ty(ty
))
571 | DomainGoal
::IsUpstream(ty
)
572 | DomainGoal
::DownstreamType(ty
)
573 | DomainGoal
::IsFullyVisible(ty
)
574 | DomainGoal
::IsLocal(ty
) => match_ty(builder
, environment
, ty
)?
,
575 DomainGoal
::FromEnv(_
) => (), // Computed in the environment
576 DomainGoal
::Normalize(Normalize { alias, ty: _ }
) => match alias
{
577 AliasTy
::Projection(proj
) => {
578 // Normalize goals derive from `AssociatedTyValue` datums,
579 // which are found in impls. That is, if we are
580 // normalizing (e.g.) `<T as Iterator>::Item>`, then
581 // search for impls of iterator and, within those impls,
582 // for associated type values:
585 // impl Iterator for Foo {
586 // type Item = Bar; // <-- associated type value
589 let associated_ty_datum
= db
.associated_ty_data(proj
.associated_ty_id
);
590 let trait_id
= associated_ty_datum
.trait_id
;
591 let trait_parameters
= db
.trait_parameters_from_projection(proj
);
593 let trait_datum
= db
.trait_datum(trait_id
);
595 let self_ty
= alias
.self_type_parameter(interner
);
596 if let TyKind
::InferenceVar(_
, _
) = self_ty
.kind(interner
) {
597 panic
!("Inference vars not allowed when getting program clauses");
600 // Flounder if the self-type is unknown and the trait is non-enumerable.
602 // e.g., Normalize(<?X as Iterator>::Item = u32)
603 if (self_ty
.is_general_var(interner
, binders
))
604 && trait_datum
.is_non_enumerable_trait()
606 return Err(Floundered
);
609 if let Some(well_known
) = trait_datum
.well_known
{
610 builtin_traits
::add_builtin_assoc_program_clauses(
611 db
, builder
, well_known
, self_ty
,
615 push_program_clauses_for_associated_type_values_in_impls_of(
623 if environment
.has_compatible_clause(interner
) {
624 push_clauses_for_compatible_normalize(
629 proj
.associated_ty_id
,
633 AliasTy
::Opaque(_
) => (),
635 DomainGoal
::Compatible
| DomainGoal
::Reveal
=> (),
641 /// Adds clauses to allow normalizing possible downstream associated type
642 /// implementations when in the "compatible" mode. Example clauses:
645 /// for<type, type, type> Normalize(<^0.0 as Trait<^0.1>>::Item -> ^0.2)
646 /// :- Compatible, Implemented(^0.0: Trait<^0.1>), DownstreamType(^0.1), CannotProve
647 /// for<type, type, type> Normalize(<^0.0 as Trait<^0.1>>::Item -> ^0.2)
648 /// :- Compatible, Implemented(^0.0: Trait<^0.1>), IsFullyVisible(^0.0), DownstreamType(^0.1), CannotProve
650 fn push_clauses_for_compatible_normalize
<I
: Interner
>(
651 db
: &dyn RustIrDatabase
<I
>,
652 builder
: &mut ClauseBuilder
<'_
, I
>,
654 trait_id
: TraitId
<I
>,
655 associated_ty_id
: AssocTypeId
<I
>,
657 let trait_datum
= db
.trait_datum(trait_id
);
658 let trait_binders
= trait_datum
.binders
.map_ref(|b
| &b
.where_clauses
).cloned();
659 builder
.push_binders(trait_binders
, |builder
, where_clauses
| {
660 let projection
= ProjectionTy
{
662 substitution
: builder
.substitution_in_scope(),
664 let trait_ref
= TraitRef
{
666 substitution
: builder
.substitution_in_scope(),
668 let type_parameters
: Vec
<_
> = trait_ref
.type_parameters(interner
).collect();
670 builder
.push_bound_ty(|builder
, target_ty
| {
671 for i
in 0..type_parameters
.len() {
673 DomainGoal
::Normalize(Normalize
{
674 ty
: target_ty
.clone(),
675 alias
: AliasTy
::Projection(projection
.clone()),
681 .chain(iter
::once(DomainGoal
::Compatible
.cast(interner
)))
683 WhereClause
::Implemented(trait_ref
.clone()).cast(interner
),
685 .chain((0..i
).map(|j
| {
686 DomainGoal
::IsFullyVisible(type_parameters
[j
].clone()).cast(interner
)
689 DomainGoal
::DownstreamType(type_parameters
[i
].clone()).cast(interner
),
691 .chain(iter
::once(GoalData
::CannotProve
.intern(interner
))),
698 /// Generate program clauses from the associated-type values
699 /// found in impls of the given trait. i.e., if `trait_id` = Iterator,
700 /// then we would generate program clauses from each `type Item = ...`
701 /// found in any impls of `Iterator`:
702 /// which are found in impls. That is, if we are
703 /// normalizing (e.g.) `<T as Iterator>::Item>`, then
704 /// search for impls of iterator and, within those impls,
705 /// for associated type values:
708 /// impl Iterator for Foo {
709 /// type Item = Bar; // <-- associated type value
712 #[instrument(level = "debug", skip(builder))]
713 fn push_program_clauses_for_associated_type_values_in_impls_of
<I
: Interner
>(
714 builder
: &mut ClauseBuilder
<'_
, I
>,
715 environment
: &Environment
<I
>,
716 trait_id
: TraitId
<I
>,
717 trait_parameters
: &[GenericArg
<I
>],
718 binders
: &CanonicalVarKinds
<I
>,
720 for impl_id
in builder
722 .impls_for_trait(trait_id
, trait_parameters
, binders
)
724 let impl_datum
= builder
.db
.impl_datum(impl_id
);
725 if !impl_datum
.is_positive() {
731 for &atv_id
in &impl_datum
.associated_ty_value_ids
{
732 let atv
= builder
.db
.associated_ty_value(atv_id
);
733 debug
!(?atv_id
, ?atv
);
734 atv
.to_program_clauses(builder
, environment
);
739 fn push_alias_implemented_clause
<I
: Interner
>(
740 builder
: &mut ClauseBuilder
<'_
, I
>,
741 trait_ref
: TraitRef
<I
>,
744 let interner
= builder
.interner();
746 *trait_ref
.self_type_parameter(interner
).kind(interner
),
747 TyKind
::Alias(alias
.clone())
750 // TODO: instead generate clauses without reference to the specific type parameters of the goal?
751 let generalized
= generalize
::Generalize
::apply(interner
, (trait_ref
, alias
));
752 builder
.push_binders(generalized
, |builder
, (trait_ref
, alias
)| {
753 let binders
= Binders
::with_fresh_type_var(interner
, |ty_var
| ty_var
);
756 // <X as Y>::Z: Trait :- T: Trait, <X as Y>::Z == T
758 builder
.push_binders(binders
, |builder
, bound_var
| {
759 let fresh_self_subst
= Substitution
::from_iter(
761 std
::iter
::once(bound_var
.clone().cast(interner
)).chain(
762 trait_ref
.substitution
.as_slice(interner
)[1..]
767 let fresh_self_trait_ref
= TraitRef
{
768 trait_id
: trait_ref
.trait_id
,
769 substitution
: fresh_self_subst
,
772 DomainGoal
::Holds(WhereClause
::Implemented(trait_ref
.clone())),
774 DomainGoal
::Holds(WhereClause
::Implemented(fresh_self_trait_ref
)),
775 DomainGoal
::Holds(WhereClause
::AliasEq(AliasEq
{
776 alias
: alias
.clone(),
785 fn push_alias_alias_eq_clause
<I
: Interner
>(
786 builder
: &mut ClauseBuilder
<'_
, I
>,
787 projection_ty
: ProjectionTy
<I
>,
791 let interner
= builder
.interner();
793 *projection_ty
.self_type_parameter(interner
).kind(interner
),
794 TyKind
::Alias(alias
.clone())
797 // TODO: instead generate clauses without reference to the specific type parameters of the goal?
798 let generalized
= generalize
::Generalize
::apply(interner
, (projection_ty
, ty
, alias
));
799 builder
.push_binders(generalized
, |builder
, (projection_ty
, ty
, alias
)| {
800 let binders
= Binders
::with_fresh_type_var(interner
, |ty_var
| ty_var
);
803 // <<X as Y>::A as Z>::B == U :- <T as Z>::B == U, <X as Y>::A == T
805 builder
.push_binders(binders
, |builder
, bound_var
| {
806 let fresh_self_subst
= Substitution
::from_iter(
808 std
::iter
::once(bound_var
.clone().cast(interner
)).chain(
809 projection_ty
.substitution
.as_slice(interner
)[1..]
814 let fresh_alias
= AliasTy
::Projection(ProjectionTy
{
815 associated_ty_id
: projection_ty
.associated_ty_id
,
816 substitution
: fresh_self_subst
,
819 DomainGoal
::Holds(WhereClause
::AliasEq(AliasEq
{
820 alias
: AliasTy
::Projection(projection_ty
.clone()),
824 DomainGoal
::Holds(WhereClause
::AliasEq(AliasEq
{
828 DomainGoal
::Holds(WhereClause
::AliasEq(AliasEq
{
829 alias
: alias
.clone(),
838 /// Examine `T` and push clauses that may be relevant to proving the
839 /// following sorts of goals (and maybe others):
841 /// * `DomainGoal::WellFormed(T)`
842 /// * `DomainGoal::IsUpstream(T)`
843 /// * `DomainGoal::DownstreamType(T)`
844 /// * `DomainGoal::IsFullyVisible(T)`
845 /// * `DomainGoal::IsLocal(T)`
847 /// Note that the type `T` must not be an unbound inference variable;
848 /// earlier parts of the logic should "flounder" in that case.
849 fn match_ty
<I
: Interner
>(
850 builder
: &mut ClauseBuilder
<'_
, I
>,
851 environment
: &Environment
<I
>,
853 ) -> Result
<(), Floundered
> {
854 let interner
= builder
.interner();
855 Ok(match ty
.kind(interner
) {
856 TyKind
::InferenceVar(_
, _
) => {
857 panic
!("Inference vars not allowed when getting program clauses")
859 TyKind
::Adt(adt_id
, _
) => builder
862 .to_program_clauses(builder
, environment
),
863 TyKind
::OpaqueType(opaque_ty_id
, _
) => builder
865 .opaque_ty_data(*opaque_ty_id
)
866 .to_program_clauses(builder
, environment
),
868 TyKind
::AssociatedType(type_id
, _
) => builder
870 .associated_ty_data(*type_id
)
871 .to_program_clauses(builder
, environment
),
872 TyKind
::FnDef(fn_def_id
, _
) => builder
874 .fn_def_datum(*fn_def_id
)
875 .to_program_clauses(builder
, environment
),
876 TyKind
::Str
| TyKind
::Never
| TyKind
::Scalar(_
) | TyKind
::Foreign(_
) => {
877 // These have no substitutions, so they are trivially WF
878 builder
.push_fact(WellFormed
::Ty(ty
.clone()));
880 TyKind
::Raw(mutbl
, _
) => {
881 builder
.push_bound_ty(|builder
, ty
| {
882 builder
.push_fact(WellFormed
::Ty(
883 TyKind
::Raw(*mutbl
, ty
).intern(builder
.interner()),
887 TyKind
::Ref(mutbl
, _
, _
) => {
888 builder
.push_bound_ty(|builder
, ty
| {
889 builder
.push_bound_lifetime(|builder
, lifetime
| {
890 builder
.push_fact(WellFormed
::Ty(
891 TyKind
::Ref(*mutbl
, lifetime
, ty
).intern(builder
.interner()),
896 TyKind
::Slice(_
) => {
897 builder
.push_bound_ty(|builder
, ty
| {
898 builder
.push_fact(WellFormed
::Ty(TyKind
::Slice(ty
).intern(builder
.interner())));
902 | TyKind
::Array(_
, _
)
903 | TyKind
::Closure(_
, _
)
904 | TyKind
::Generator(_
, _
)
905 | TyKind
::GeneratorWitness(_
, _
) => {
906 let ty
= generalize
::Generalize
::apply(builder
.db
.interner(), ty
.clone());
907 builder
.push_binders(ty
, |builder
, ty
| {
908 builder
.push_fact(WellFormed
::Ty(ty
.clone()));
911 TyKind
::Placeholder(_
) => {
912 builder
.push_clause(WellFormed
::Ty(ty
.clone()), Some(FromEnv
::Ty(ty
.clone())));
914 TyKind
::Alias(AliasTy
::Projection(proj
)) => builder
916 .associated_ty_data(proj
.associated_ty_id
)
917 .to_program_clauses(builder
, environment
),
918 TyKind
::Alias(AliasTy
::Opaque(opaque_ty
)) => builder
920 .opaque_ty_data(opaque_ty
.opaque_ty_id
)
921 .to_program_clauses(builder
, environment
),
922 TyKind
::Function(_quantified_ty
) => {
923 let ty
= generalize
::Generalize
::apply(builder
.db
.interner(), ty
.clone());
924 builder
.push_binders(ty
, |builder
, ty
| {
925 builder
.push_fact(WellFormed
::Ty(ty
.clone()))
928 TyKind
::BoundVar(_
) => return Err(Floundered
),
929 TyKind
::Dyn(dyn_ty
) => {
931 // - Object safety? (not needed with RFC 2027)
933 // - Bounds on the associated types
934 // - Checking that all associated types are specified, including
935 // those on supertraits.
936 // - For trait objects with GATs, check that the bounds are fully
937 // general (`dyn for<'a> StreamingIterator<Item<'a> = &'a ()>` is OK,
938 // `dyn StreamingIterator<Item<'static> = &'static ()>` is not).
942 .substitute(interner
, &[ty
.clone().cast
::<GenericArg
<I
>>(interner
)]);
944 let mut wf_goals
= Vec
::new();
946 wf_goals
.extend(bounds
.iter(interner
).flat_map(|bound
| {
947 bound
.map_ref(|bound
| -> Vec
<_
> {
949 WhereClause
::Implemented(trait_ref
) => {
950 vec
![DomainGoal
::WellFormed(WellFormed
::Trait(trait_ref
.clone()))]
952 WhereClause
::AliasEq(_
)
953 | WhereClause
::LifetimeOutlives(_
)
954 | WhereClause
::TypeOutlives(_
) => vec
![],
959 builder
.push_clause(WellFormed
::Ty(ty
.clone()), wf_goals
);
964 fn match_alias_ty
<I
: Interner
>(
965 builder
: &mut ClauseBuilder
<'_
, I
>,
966 environment
: &Environment
<I
>,
970 AliasTy
::Projection(projection_ty
) => builder
972 .associated_ty_data(projection_ty
.associated_ty_id
)
973 .to_program_clauses(builder
, environment
),
978 #[instrument(level = "debug", skip(db))]
979 pub fn program_clauses_for_env
<'db
, I
: Interner
>(
980 db
: &'db
dyn RustIrDatabase
<I
>,
981 environment
: &Environment
<I
>,
982 ) -> ProgramClauses
<I
> {
983 let mut last_round
= environment
985 .as_slice(db
.interner())
988 .collect
::<FxHashSet
<_
>>();
989 let mut closure
= last_round
.clone();
990 let mut next_round
= FxHashSet
::default();
991 while !last_round
.is_empty() {
992 elaborate_env_clauses(
994 &last_round
.drain().collect
::<Vec
<_
>>(),
1001 .filter(|clause
| closure
.insert(clause
.clone())),
1005 ProgramClauses
::from_iter(db
.interner(), closure
)