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::rust_ir
::{Movability, WellKnownTrait}
;
6 use crate::split
::Split
;
7 use crate::RustIrDatabase
;
8 use chalk_ir
::cast
::{Cast, Caster}
;
9 use chalk_ir
::could_match
::CouldMatch
;
10 use chalk_ir
::interner
::Interner
;
12 use rustc_hash
::FxHashSet
;
14 use std
::marker
::PhantomData
;
15 use tracing
::{debug, instrument}
;
22 pub mod program_clauses
;
25 // yields the types "contained" in `app_ty`
26 fn constituent_types
<I
: Interner
>(db
: &dyn RustIrDatabase
<I
>, ty
: &TyKind
<I
>) -> Vec
<Ty
<I
>> {
27 let interner
= db
.interner();
30 // For non-phantom_data adts we collect its variants/fields
31 TyKind
::Adt(adt_id
, substitution
) if !db
.adt_datum(*adt_id
).flags
.phantom_data
=> {
32 let adt_datum
= &db
.adt_datum(*adt_id
);
33 let adt_datum_bound
= adt_datum
.binders
.clone().substitute(interner
, substitution
);
37 .flat_map(|variant
| variant
.fields
.into_iter())
40 // And for `PhantomData<T>`, we pass `T`.
41 TyKind
::Adt(_
, substitution
)
42 | TyKind
::Tuple(_
, substitution
)
43 | TyKind
::FnDef(_
, substitution
) => substitution
45 .filter_map(|x
| x
.ty(interner
))
49 TyKind
::Array(ty
, _
) | TyKind
::Slice(ty
) | TyKind
::Raw(_
, ty
) | TyKind
::Ref(_
, _
, ty
) => {
53 TyKind
::Str
| TyKind
::Never
| TyKind
::Scalar(_
) => Vec
::new(),
55 TyKind
::Generator(generator_id
, substitution
) => {
56 let generator_datum
= &db
.generator_datum(*generator_id
);
57 let generator_datum_bound
= generator_datum
60 .substitute(interner
, &substitution
);
62 let mut tys
= generator_datum_bound
.upvars
;
64 TyKind
::GeneratorWitness(*generator_id
, substitution
.clone()).intern(interner
),
69 TyKind
::Closure(_
, _
) => panic
!("this function should not be called for closures"),
70 TyKind
::GeneratorWitness(_
, _
) => {
71 panic
!("this function should not be called for generator witnesses")
73 TyKind
::Function(_
) => panic
!("this function should not be called for functions"),
74 TyKind
::InferenceVar(_
, _
) | TyKind
::BoundVar(_
) => {
75 panic
!("this function should not be called for inference or bound vars")
77 TyKind
::Placeholder(_
) => panic
!("this function should not be called for placeholders"),
78 TyKind
::Dyn(_
) => panic
!("this function should not be called for dyn types"),
79 TyKind
::Alias(_
) => panic
!("this function should not be called for alias"),
80 TyKind
::Foreign(_
) => panic
!("constituent_types of foreign types are unknown!"),
81 TyKind
::Error
=> Vec
::new(),
82 TyKind
::OpaqueType(_
, _
) => panic
!("constituent_types of opaque types are unknown!"),
83 TyKind
::AssociatedType(_
, _
) => {
84 panic
!("constituent_types of associated types are unknown!")
89 /// FIXME(#505) update comments for ADTs
90 /// For auto-traits, we generate a default rule for every struct,
91 /// unless there is a manual impl for that struct given explicitly.
93 /// So, if you have `impl Send for MyList<Foo>`, then we would
94 /// generate no rule for `MyList` at all -- similarly if you have
95 /// `impl !Send for MyList<Foo>`, or `impl<T> Send for MyList<T>`.
97 /// But if you have no rules at all for `Send` / `MyList`, then we
98 /// generate an impl based on the field types of `MyList`. For example
99 /// given the following program:
102 /// #[auto] trait Send { }
104 /// struct MyList<T> {
106 /// next: Box<Option<MyList<T>>>,
115 /// Implemented(MyList<T>: Send) :-
116 /// Implemented(T: Send),
117 /// Implemented(Box<Option<MyList<T>>>: Send).
120 #[instrument(level = "debug", skip(builder))]
121 pub fn push_auto_trait_impls
<I
: Interner
>(
122 builder
: &mut ClauseBuilder
<'_
, I
>,
123 auto_trait_id
: TraitId
<I
>,
125 ) -> Result
<(), Floundered
> {
126 let interner
= builder
.interner();
128 // Must be an auto trait.
129 assert
!(builder
.db
.trait_datum(auto_trait_id
).is_auto_trait());
131 // Auto traits never have generic parameters of their own (apart from `Self`).
133 builder
.db
.trait_datum(auto_trait_id
).binders
.len(interner
),
137 // If there is a `impl AutoTrait for Foo<..>` or `impl !AutoTrait
138 // for Foo<..>`, where `Foo` is the adt we're looking at, then
139 // we don't generate our own rules.
140 if builder
.db
.impl_provided_for(auto_trait_id
, ty
) {
141 debug
!("impl provided");
145 let mk_ref
= |ty
: Ty
<I
>| TraitRef
{
146 trait_id
: auto_trait_id
,
147 substitution
: Substitution
::from1(interner
, ty
.cast(interner
)),
150 let consequence
= mk_ref(ty
.clone().intern(interner
));
153 // function-types implement auto traits unconditionally
154 TyKind
::Function(_
) => {
155 builder
.push_fact(consequence
);
158 TyKind
::InferenceVar(_
, _
) | TyKind
::BoundVar(_
) => Err(Floundered
),
160 // auto traits are not implemented for foreign types
161 TyKind
::Foreign(_
) => Ok(()),
163 // closures require binders, while the other types do not
164 TyKind
::Closure(closure_id
, substs
) => {
165 let closure_fn_substitution
= builder
.db
.closure_fn_substitution(*closure_id
, substs
);
166 let binders
= builder
.db
.closure_upvars(*closure_id
, substs
);
167 let upvars
= binders
.substitute(builder
.db
.interner(), &closure_fn_substitution
);
169 // in a same behavior as for non-auto traits (reuse the code) we can require that
170 // every bound type must implement this auto-trait
171 use crate::clauses
::builtin_traits
::needs_impl_for_tys
;
172 needs_impl_for_tys(builder
.db
, builder
, consequence
, Some(upvars
).into_iter());
176 TyKind
::Generator(generator_id
, _
) => {
177 if Some(auto_trait_id
) == builder
.db
.well_known_trait_id(WellKnownTrait
::Unpin
) {
178 match builder
.db
.generator_datum(*generator_id
).movability
{
179 // immovable generators are never `Unpin`
180 Movability
::Static
=> (),
181 // movable generators are always `Unpin`
182 Movability
::Movable
=> builder
.push_fact(consequence
),
185 // if trait is not `Unpin`, use regular auto trait clause
186 let conditions
= constituent_types(builder
.db
, ty
).into_iter().map(mk_ref
);
187 builder
.push_clause(consequence
, conditions
);
192 TyKind
::GeneratorWitness(generator_id
, _
) => {
193 push_auto_trait_impls_generator_witness(builder
, auto_trait_id
, *generator_id
);
197 TyKind
::OpaqueType(opaque_ty_id
, _
) => {
198 push_auto_trait_impls_opaque(builder
, auto_trait_id
, *opaque_ty_id
);
203 TyKind
::AssociatedType(_
, _
)
204 | TyKind
::Placeholder(_
)
206 | TyKind
::Alias(_
) => Ok(()),
208 // app_ty implements AutoTrait if all constituents of app_ty implement AutoTrait
210 let conditions
= constituent_types(builder
.db
, ty
).into_iter().map(mk_ref
);
212 builder
.push_clause(consequence
, conditions
);
218 /// Leak auto traits for opaque types, just like `push_auto_trait_impls` does for structs.
220 /// For example, given the following program:
223 /// #[auto] trait Send { }
226 /// opaque type Foo: Trait = Bar
228 /// Checking the goal `Foo: Send` would generate the following:
231 /// Foo: Send :- Bar: Send
233 #[instrument(level = "debug", skip(builder))]
234 pub fn push_auto_trait_impls_opaque
<I
: Interner
>(
235 builder
: &mut ClauseBuilder
<'_
, I
>,
236 auto_trait_id
: TraitId
<I
>,
237 opaque_id
: OpaqueTyId
<I
>,
239 let opaque_ty_datum
= &builder
.db
.opaque_ty_data(opaque_id
);
240 let interner
= builder
.interner();
242 // Must be an auto trait.
243 assert
!(builder
.db
.trait_datum(auto_trait_id
).is_auto_trait());
245 // Auto traits never have generic parameters of their own (apart from `Self`).
247 builder
.db
.trait_datum(auto_trait_id
).binders
.len(interner
),
251 let hidden_ty
= builder
.db
.hidden_opaque_type(opaque_id
);
252 let binders
= opaque_ty_datum
.bound
.clone();
253 builder
.push_binders(binders
, |builder
, _
| {
255 TyKind
::OpaqueType(opaque_id
, builder
.substitution_in_scope()).intern(interner
);
257 // trait_ref = `OpaqueType<...>: MyAutoTrait`
258 let auto_trait_ref
= TraitRef
{
259 trait_id
: auto_trait_id
,
260 substitution
: Substitution
::from1(interner
, self_ty
),
263 // OpaqueType<...>: MyAutoTrait :- HiddenType: MyAutoTrait
266 std
::iter
::once(TraitRef
{
267 trait_id
: auto_trait_id
,
268 substitution
: Substitution
::from1(interner
, hidden_ty
.clone()),
274 #[instrument(level = "debug", skip(builder))]
275 pub fn push_auto_trait_impls_generator_witness
<I
: Interner
>(
276 builder
: &mut ClauseBuilder
<'_
, I
>,
277 auto_trait_id
: TraitId
<I
>,
278 generator_id
: GeneratorId
<I
>,
280 let witness_datum
= builder
.db
.generator_witness_datum(generator_id
);
281 let interner
= builder
.interner();
283 // Must be an auto trait.
284 assert
!(builder
.db
.trait_datum(auto_trait_id
).is_auto_trait());
286 // Auto traits never have generic parameters of their own (apart from `Self`).
288 builder
.db
.trait_datum(auto_trait_id
).binders
.len(interner
),
292 // Push binders for the generator generic parameters. These can be used by
293 // both upvars and witness types
294 builder
.push_binders(witness_datum
.inner_types
.clone(), |builder
, inner_types
| {
295 let witness_ty
= TyKind
::GeneratorWitness(generator_id
, builder
.substitution_in_scope())
298 // trait_ref = `GeneratorWitness<...>: MyAutoTrait`
299 let auto_trait_ref
= TraitRef
{
300 trait_id
: auto_trait_id
,
301 substitution
: Substitution
::from1(interner
, witness_ty
),
304 // Create a goal of the form:
305 // forall<L0, L1, ..., LN> {
306 // WitnessType1<L0, L1, ... LN, P0, P1, ..., PN>: MyAutoTrait,
308 // WitnessTypeN<L0, L1, ... LN, P0, P1, ..., PN>: MyAutoTrait,
312 // where `L0, L1, ...LN` are our existentially bound witness lifetimes,
313 // and `P0, P1, ..., PN` are the normal generator generics.
315 // We create a 'forall' goal due to the fact that our witness lifetimes
316 // are *existentially* quantified - the precise reigon is erased during
317 // type checking, so we just know that the type takes *some* region
318 // as a parameter. Therefore, we require that the auto trait bound
319 // hold for *all* regions, which guarantees that the bound will
320 // hold for the original lifetime (before it was erased).
322 // This does not take into account well-formed information from
323 // the witness types. For example, if we have the type
324 // `struct Foo<'a, 'b> { val: &'a &'b u8 }`
325 // then `'b: 'a` must hold for `Foo<'a, 'b>` to be well-formed.
326 // If we have `Foo<'a, 'b>` stored as a witness type, we will
327 // not currently use this information to determine a more precise
328 // relationship between 'a and 'b. In the future, we will likely
329 // do this to avoid incorrectly rejecting correct code.
330 let gb
= &mut GoalBuilder
::new(builder
.db
);
331 let witness_goal
= gb
.forall(
334 |gb
, _subst
, types
, auto_trait_id
| {
337 GoalData
::All(Goals
::from_iter(
339 types
.iter().map(|witness_ty
| TraitRef
{
340 trait_id
: auto_trait_id
,
341 substitution
: Substitution
::from1(gb
.interner(), witness_ty
.clone()),
348 // GeneratorWitnessType: AutoTrait :- forall<...> ...
349 // where 'forall<...> ...' is the goal described above.
350 builder
.push_clause(auto_trait_ref
, std
::iter
::once(witness_goal
));
354 /// Given some goal `goal` that must be proven, along with
355 /// its `environment`, figures out the program clauses that apply
356 /// to this goal from the Rust program. So for example if the goal
357 /// is `Implemented(T: Clone)`, then this function might return clauses
358 /// derived from the trait `Clone` and its impls.
359 #[instrument(level = "debug", skip(db))]
360 pub fn program_clauses_for_goal
<'db
, I
: Interner
>(
361 db
: &'db
dyn RustIrDatabase
<I
>,
362 goal
: &UCanonical
<InEnvironment
<DomainGoal
<I
>>>,
363 ) -> Result
<Vec
<ProgramClause
<I
>>, Floundered
> {
364 let interner
= db
.interner();
366 let custom_clauses
= db
.custom_clauses().into_iter();
367 let clauses_that_could_match
=
368 program_clauses_that_could_match(db
, goal
).map(|cl
| cl
.into_iter())?
;
370 let clauses
: Vec
<ProgramClause
<I
>> = custom_clauses
371 .chain(clauses_that_could_match
)
373 db
.program_clauses_for_env(&goal
.canonical
.value
.environment
)
380 db
.unification_database(),
381 &goal
.canonical
.value
.goal
,
391 /// Returns a set of program clauses that could possibly match
392 /// `goal`. This can be any superset of the correct set, but the
393 /// more precise you can make it, the more efficient solving will
395 #[instrument(level = "debug", skip(db))]
396 pub fn program_clauses_that_could_match
<I
: Interner
>(
397 db
: &dyn RustIrDatabase
<I
>,
398 goal
: &UCanonical
<InEnvironment
<DomainGoal
<I
>>>,
399 ) -> Result
<Vec
<ProgramClause
<I
>>, Floundered
> {
400 let interner
= db
.interner();
401 let mut clauses
: Vec
<ProgramClause
<I
>> = vec
![];
402 let builder
= &mut ClauseBuilder
::new(db
, &mut clauses
);
407 value
: InEnvironment { environment, goal }
,
414 DomainGoal
::Holds(WhereClause
::Implemented(trait_ref
)) => {
415 let self_ty
= trait_ref
.self_type_parameter(interner
);
417 let trait_id
= trait_ref
.trait_id
;
418 let trait_datum
= db
.trait_datum(trait_id
);
420 match self_ty
.kind(interner
) {
421 TyKind
::InferenceVar(_
, _
) => {
422 panic
!("Inference vars not allowed when getting program clauses")
424 TyKind
::Alias(alias
) => {
425 // An alias could normalize to anything, including `dyn trait`
426 // or an opaque type, so push a clause that asks for the
427 // self type to be normalized and return.
428 push_alias_implemented_clause(builder
, trait_ref
.clone(), alias
.clone());
432 _
if self_ty
.is_general_var(interner
, binders
) => {
433 if trait_datum
.is_non_enumerable_trait() || trait_datum
.is_auto_trait() {
434 return Err(Floundered
);
438 TyKind
::OpaqueType(opaque_ty_id
, _
) => {
439 db
.opaque_ty_data(*opaque_ty_id
)
440 .to_program_clauses(builder
, environment
);
444 // If the self type is a `dyn trait` type, generate program-clauses
445 // that indicates that it implements its own traits.
446 // FIXME: This is presently rather wasteful, in that we don't check that the
447 // these program clauses we are generating are actually relevant to the goal
448 // `goal` that we are actually *trying* to prove (though there is some later
449 // code that will screen out irrelevant stuff).
451 // In other words, if we were trying to prove `Implemented(dyn
452 // Fn(&u8): Clone)`, we would still generate two clauses that are
453 // totally irrelevant to that goal, because they let us prove other
454 // things but not `Clone`.
455 dyn_ty
::build_dyn_self_ty_clauses(db
, builder
, self_ty
.clone())
458 // We don't actually do anything here, but we need to record the types when logging
459 TyKind
::Adt(adt_id
, _
) => {
460 let _
= db
.adt_datum(*adt_id
);
463 TyKind
::FnDef(fn_def_id
, _
) => {
464 let _
= db
.fn_def_datum(*fn_def_id
);
470 // This is needed for the coherence related impls, as well
471 // as for the `Implemented(Foo) :- FromEnv(Foo)` rule.
472 trait_datum
.to_program_clauses(builder
, environment
);
474 for impl_id
in db
.impls_for_trait(
476 trait_ref
.substitution
.as_slice(interner
),
479 db
.impl_datum(impl_id
)
480 .to_program_clauses(builder
, environment
);
483 // If this is a `Foo: Send` (or any auto-trait), then add
484 // the automatic impls for `Foo`.
485 let trait_datum
= db
.trait_datum(trait_id
);
486 if trait_datum
.is_auto_trait() {
487 let generalized
= generalize
::Generalize
::apply(db
.interner(), trait_ref
.clone());
488 builder
.push_binders(generalized
, |builder
, trait_ref
| {
489 let ty
= trait_ref
.self_type_parameter(interner
);
490 push_auto_trait_impls(builder
, trait_id
, ty
.kind(interner
))
494 if let Some(well_known
) = trait_datum
.well_known
{
495 builtin_traits
::add_builtin_program_clauses(
504 DomainGoal
::Holds(WhereClause
::AliasEq(alias_eq
)) => match &alias_eq
.alias
{
505 AliasTy
::Projection(proj
) => {
506 let trait_self_ty
= db
507 .trait_ref_from_projection(proj
)
508 .self_type_parameter(interner
);
510 match trait_self_ty
.kind(interner
) {
511 TyKind
::Alias(alias
) => {
512 // An alias could normalize to anything, including an
513 // opaque type, so push a clause that asks for the self
514 // type to be normalized and return.
515 push_alias_alias_eq_clause(
523 TyKind
::OpaqueType(opaque_ty_id
, _
) => {
524 db
.opaque_ty_data(*opaque_ty_id
)
525 .to_program_clauses(builder
, environment
);
527 // If the self type is a `dyn trait` type, generate program-clauses
528 // for any associated type bindings it contains.
529 // FIXME: see the fixme for the analogous code for Implemented goals.
531 dyn_ty
::build_dyn_self_ty_clauses(db
, builder
, trait_self_ty
.clone())
536 db
.associated_ty_data(proj
.associated_ty_id
)
537 .to_program_clauses(builder
, environment
)
539 AliasTy
::Opaque(opaque_ty
) => db
540 .opaque_ty_data(opaque_ty
.opaque_ty_id
)
541 .to_program_clauses(builder
, environment
),
543 DomainGoal
::Holds(WhereClause
::LifetimeOutlives(..)) => {
544 builder
.push_bound_lifetime(|builder
, a
| {
545 builder
.push_bound_lifetime(|builder
, b
| {
546 builder
.push_fact_with_constraints(
547 DomainGoal
::Holds(WhereClause
::LifetimeOutlives(LifetimeOutlives
{
551 Some(InEnvironment
::new(
552 &Environment
::new(interner
),
553 Constraint
::LifetimeOutlives(a
, b
),
559 DomainGoal
::Holds(WhereClause
::TypeOutlives(..)) => {
560 builder
.push_bound_ty(|builder
, ty
| {
561 builder
.push_bound_lifetime(|builder
, lifetime
| {
562 builder
.push_fact_with_constraints(
563 DomainGoal
::Holds(WhereClause
::TypeOutlives(TypeOutlives
{
565 lifetime
: lifetime
.clone(),
567 Some(InEnvironment
::new(
568 &Environment
::new(interner
),
569 Constraint
::TypeOutlives(ty
, lifetime
),
575 DomainGoal
::WellFormed(WellFormed
::Trait(trait_ref
))
576 | DomainGoal
::LocalImplAllowed(trait_ref
) => {
577 db
.trait_datum(trait_ref
.trait_id
)
578 .to_program_clauses(builder
, environment
);
580 DomainGoal
::ObjectSafe(trait_id
) => {
581 if builder
.db
.is_object_safe(*trait_id
) {
582 builder
.push_fact(DomainGoal
::ObjectSafe(*trait_id
));
585 DomainGoal
::WellFormed(WellFormed
::Ty(ty
))
586 | DomainGoal
::IsUpstream(ty
)
587 | DomainGoal
::DownstreamType(ty
)
588 | DomainGoal
::IsFullyVisible(ty
)
589 | DomainGoal
::IsLocal(ty
) => match_ty(builder
, environment
, ty
)?
,
590 DomainGoal
::FromEnv(_
) => (), // Computed in the environment
591 DomainGoal
::Normalize(Normalize { alias, ty: _ }
) => match alias
{
592 AliasTy
::Projection(proj
) => {
593 // Normalize goals derive from `AssociatedTyValue` datums,
594 // which are found in impls. That is, if we are
595 // normalizing (e.g.) `<T as Iterator>::Item>`, then
596 // search for impls of iterator and, within those impls,
597 // for associated type values:
600 // impl Iterator for Foo {
601 // type Item = Bar; // <-- associated type value
604 let associated_ty_datum
= db
.associated_ty_data(proj
.associated_ty_id
);
605 let trait_id
= associated_ty_datum
.trait_id
;
606 let trait_ref
= db
.trait_ref_from_projection(proj
);
607 let trait_parameters
= trait_ref
.substitution
.as_parameters(interner
);
609 let trait_datum
= db
.trait_datum(trait_id
);
611 let self_ty
= trait_ref
.self_type_parameter(interner
);
612 if let TyKind
::InferenceVar(_
, _
) = self_ty
.kind(interner
) {
613 panic
!("Inference vars not allowed when getting program clauses");
616 // Flounder if the self-type is unknown and the trait is non-enumerable.
618 // e.g., Normalize(<?X as Iterator>::Item = u32)
619 if (self_ty
.is_general_var(interner
, binders
))
620 && trait_datum
.is_non_enumerable_trait()
622 return Err(Floundered
);
625 if let Some(well_known
) = trait_datum
.well_known
{
626 builtin_traits
::add_builtin_assoc_program_clauses(
627 db
, builder
, well_known
, self_ty
,
631 push_program_clauses_for_associated_type_values_in_impls_of(
639 if environment
.has_compatible_clause(interner
) {
640 push_clauses_for_compatible_normalize(
645 proj
.associated_ty_id
,
649 AliasTy
::Opaque(_
) => (),
651 DomainGoal
::Compatible
| DomainGoal
::Reveal
=> (),
657 /// Adds clauses to allow normalizing possible downstream associated type
658 /// implementations when in the "compatible" mode. Example clauses:
661 /// for<type, type, type> Normalize(<^0.0 as Trait<^0.1>>::Item -> ^0.2)
662 /// :- Compatible, Implemented(^0.0: Trait<^0.1>), DownstreamType(^0.1), CannotProve
663 /// for<type, type, type> Normalize(<^0.0 as Trait<^0.1>>::Item -> ^0.2)
664 /// :- Compatible, Implemented(^0.0: Trait<^0.1>), IsFullyVisible(^0.0), DownstreamType(^0.1), CannotProve
666 fn push_clauses_for_compatible_normalize
<I
: Interner
>(
667 db
: &dyn RustIrDatabase
<I
>,
668 builder
: &mut ClauseBuilder
<'_
, I
>,
670 trait_id
: TraitId
<I
>,
671 associated_ty_id
: AssocTypeId
<I
>,
673 let trait_datum
= db
.trait_datum(trait_id
);
674 let trait_binders
= trait_datum
.binders
.map_ref(|b
| &b
.where_clauses
).cloned();
675 builder
.push_binders(trait_binders
, |builder
, where_clauses
| {
676 let projection
= ProjectionTy
{
678 substitution
: builder
.substitution_in_scope(),
680 let trait_ref
= TraitRef
{
682 substitution
: builder
.substitution_in_scope(),
684 let type_parameters
: Vec
<_
> = trait_ref
.type_parameters(interner
).collect();
686 builder
.push_bound_ty(|builder
, target_ty
| {
687 for i
in 0..type_parameters
.len() {
689 DomainGoal
::Normalize(Normalize
{
690 ty
: target_ty
.clone(),
691 alias
: AliasTy
::Projection(projection
.clone()),
697 .chain(iter
::once(DomainGoal
::Compatible
.cast(interner
)))
699 WhereClause
::Implemented(trait_ref
.clone()).cast(interner
),
701 .chain((0..i
).map(|j
| {
702 DomainGoal
::IsFullyVisible(type_parameters
[j
].clone()).cast(interner
)
705 DomainGoal
::DownstreamType(type_parameters
[i
].clone()).cast(interner
),
707 .chain(iter
::once(GoalData
::CannotProve
.intern(interner
))),
714 /// Generate program clauses from the associated-type values
715 /// found in impls of the given trait. i.e., if `trait_id` = Iterator,
716 /// then we would generate program clauses from each `type Item = ...`
717 /// found in any impls of `Iterator`:
718 /// which are found in impls. That is, if we are
719 /// normalizing (e.g.) `<T as Iterator>::Item>`, then
720 /// search for impls of iterator and, within those impls,
721 /// for associated type values:
724 /// impl Iterator for Foo {
725 /// type Item = Bar; // <-- associated type value
728 #[instrument(level = "debug", skip(builder))]
729 fn push_program_clauses_for_associated_type_values_in_impls_of
<I
: Interner
>(
730 builder
: &mut ClauseBuilder
<'_
, I
>,
731 environment
: &Environment
<I
>,
732 trait_id
: TraitId
<I
>,
733 trait_parameters
: &[GenericArg
<I
>],
734 binders
: &CanonicalVarKinds
<I
>,
736 for impl_id
in builder
738 .impls_for_trait(trait_id
, trait_parameters
, binders
)
740 let impl_datum
= builder
.db
.impl_datum(impl_id
);
741 if !impl_datum
.is_positive() {
747 for &atv_id
in &impl_datum
.associated_ty_value_ids
{
748 let atv
= builder
.db
.associated_ty_value(atv_id
);
749 debug
!(?atv_id
, ?atv
);
750 atv
.to_program_clauses(builder
, environment
);
755 fn push_alias_implemented_clause
<I
: Interner
>(
756 builder
: &mut ClauseBuilder
<'_
, I
>,
757 trait_ref
: TraitRef
<I
>,
760 let interner
= builder
.interner();
762 *trait_ref
.self_type_parameter(interner
).kind(interner
),
763 TyKind
::Alias(alias
.clone())
766 // TODO: instead generate clauses without reference to the specific type parameters of the goal?
767 let generalized
= generalize
::Generalize
::apply(interner
, (trait_ref
, alias
));
768 builder
.push_binders(generalized
, |builder
, (trait_ref
, alias
)| {
769 let binders
= Binders
::with_fresh_type_var(interner
, |ty_var
| ty_var
);
772 // <X as Y>::Z: Trait :- T: Trait, <X as Y>::Z == T
774 builder
.push_binders(binders
, |builder
, bound_var
| {
775 let fresh_self_subst
= Substitution
::from_iter(
777 std
::iter
::once(bound_var
.clone().cast(interner
)).chain(
778 trait_ref
.substitution
.as_slice(interner
)[1..]
783 let fresh_self_trait_ref
= TraitRef
{
784 trait_id
: trait_ref
.trait_id
,
785 substitution
: fresh_self_subst
,
788 DomainGoal
::Holds(WhereClause
::Implemented(trait_ref
.clone())),
790 DomainGoal
::Holds(WhereClause
::Implemented(fresh_self_trait_ref
)),
791 DomainGoal
::Holds(WhereClause
::AliasEq(AliasEq
{
792 alias
: alias
.clone(),
801 fn push_alias_alias_eq_clause
<I
: Interner
>(
802 builder
: &mut ClauseBuilder
<'_
, I
>,
803 projection_ty
: ProjectionTy
<I
>,
807 let interner
= builder
.interner();
808 let self_ty
= builder
810 .trait_ref_from_projection(&projection_ty
)
811 .self_type_parameter(interner
);
812 assert_eq
!(*self_ty
.kind(interner
), TyKind
::Alias(alias
.clone()));
814 // TODO: instead generate clauses without reference to the specific type parameters of the goal?
815 let generalized
= generalize
::Generalize
::apply(interner
, (projection_ty
, ty
, alias
));
816 builder
.push_binders(generalized
, |builder
, (projection_ty
, ty
, alias
)| {
817 let binders
= Binders
::with_fresh_type_var(interner
, |ty_var
| ty_var
);
820 // <<X as Y>::A as Z>::B == U :- <T as Z>::B == U, <X as Y>::A == T
822 builder
.push_binders(binders
, |builder
, bound_var
| {
823 let fresh_self_subst
= Substitution
::from_iter(
825 std
::iter
::once(bound_var
.clone().cast(interner
)).chain(
826 projection_ty
.substitution
.as_slice(interner
)[1..]
831 let fresh_alias
= AliasTy
::Projection(ProjectionTy
{
832 associated_ty_id
: projection_ty
.associated_ty_id
,
833 substitution
: fresh_self_subst
,
836 DomainGoal
::Holds(WhereClause
::AliasEq(AliasEq
{
837 alias
: AliasTy
::Projection(projection_ty
.clone()),
841 DomainGoal
::Holds(WhereClause
::AliasEq(AliasEq
{
845 DomainGoal
::Holds(WhereClause
::AliasEq(AliasEq
{
846 alias
: alias
.clone(),
855 /// Examine `T` and push clauses that may be relevant to proving the
856 /// following sorts of goals (and maybe others):
858 /// * `DomainGoal::WellFormed(T)`
859 /// * `DomainGoal::IsUpstream(T)`
860 /// * `DomainGoal::DownstreamType(T)`
861 /// * `DomainGoal::IsFullyVisible(T)`
862 /// * `DomainGoal::IsLocal(T)`
864 /// Note that the type `T` must not be an unbound inference variable;
865 /// earlier parts of the logic should "flounder" in that case.
866 fn match_ty
<I
: Interner
>(
867 builder
: &mut ClauseBuilder
<'_
, I
>,
868 environment
: &Environment
<I
>,
870 ) -> Result
<(), Floundered
> {
871 let interner
= builder
.interner();
872 match ty
.kind(interner
) {
873 TyKind
::InferenceVar(_
, _
) => {
874 panic
!("Inference vars not allowed when getting program clauses")
876 TyKind
::Adt(adt_id
, _
) => builder
879 .to_program_clauses(builder
, environment
),
880 TyKind
::OpaqueType(opaque_ty_id
, _
) => builder
882 .opaque_ty_data(*opaque_ty_id
)
883 .to_program_clauses(builder
, environment
),
885 TyKind
::AssociatedType(type_id
, _
) => builder
887 .associated_ty_data(*type_id
)
888 .to_program_clauses(builder
, environment
),
889 TyKind
::FnDef(fn_def_id
, _
) => builder
891 .fn_def_datum(*fn_def_id
)
892 .to_program_clauses(builder
, environment
),
897 | TyKind
::Tuple(0, _
) => {
898 // These have no substitutions, so they are trivially WF
899 builder
.push_fact(WellFormed
::Ty(ty
.clone()));
901 TyKind
::Raw(mutbl
, _
) => {
902 // forall<T> WF(*const T) :- WF(T);
903 builder
.push_bound_ty(|builder
, ty
| {
905 WellFormed
::Ty(TyKind
::Raw(*mutbl
, ty
.clone()).intern(builder
.interner())),
906 Some(WellFormed
::Ty(ty
)),
910 TyKind
::Ref(mutbl
, _
, _
) => {
911 // forall<'a, T> WF(&'a T) :- WF(T), T: 'a
912 builder
.push_bound_ty(|builder
, ty
| {
913 builder
.push_bound_lifetime(|builder
, lifetime
| {
914 let ref_ty
= TyKind
::Ref(*mutbl
, lifetime
.clone(), ty
.clone())
915 .intern(builder
.interner());
917 WellFormed
::Ty(ref_ty
),
919 DomainGoal
::WellFormed(WellFormed
::Ty(ty
.clone())),
920 DomainGoal
::Holds(WhereClause
::TypeOutlives(TypeOutlives
{
929 TyKind
::Slice(_
) => {
930 // forall<T> WF([T]) :- T: Sized, WF(T)
931 builder
.push_bound_ty(|builder
, ty
| {
932 let sized
= builder
.db
.well_known_trait_id(WellKnownTrait
::Sized
);
934 WellFormed
::Ty(TyKind
::Slice(ty
.clone()).intern(builder
.interner())),
937 DomainGoal
::Holds(WhereClause
::Implemented(TraitRef
{
939 substitution
: Substitution
::from1(interner
, ty
.clone()),
943 .chain(Some(DomainGoal
::WellFormed(WellFormed
::Ty(ty
)))),
947 TyKind
::Array(..) => {
948 // forall<T. const N: usize> WF([T, N]) :- T: Sized
949 let interner
= builder
.interner();
950 let binders
= Binders
::new(
951 VariableKinds
::from_iter(
954 VariableKind
::Ty(TyVariableKind
::General
),
956 TyKind
::Scalar(Scalar
::Uint(UintTy
::Usize
)).intern(interner
),
962 builder
.push_binders(binders
, |builder
, PhantomData
| {
963 let placeholders_in_scope
= builder
.placeholders_in_scope();
964 let placeholder_count
= placeholders_in_scope
.len();
965 let ty
= placeholders_in_scope
[placeholder_count
- 2]
966 .assert_ty_ref(interner
)
968 let size
= placeholders_in_scope
[placeholder_count
- 1]
969 .assert_const_ref(interner
)
972 let sized
= builder
.db
.well_known_trait_id(WellKnownTrait
::Sized
);
973 let array_ty
= TyKind
::Array(ty
.clone(), size
).intern(interner
);
975 WellFormed
::Ty(array_ty
),
978 DomainGoal
::Holds(WhereClause
::Implemented(TraitRef
{
980 substitution
: Substitution
::from1(interner
, ty
.clone()),
984 .chain(Some(DomainGoal
::WellFormed(WellFormed
::Ty(ty
)))),
988 TyKind
::Tuple(len
, _
) => {
989 // WF((T0, ..., Tn, U)) :- T0: Sized, ..., Tn: Sized, WF(T0), ..., WF(Tn), WF(U)
990 let interner
= builder
.interner();
991 let binders
= Binders
::new(
992 VariableKinds
::from_iter(
994 iter
::repeat_with(|| VariableKind
::Ty(TyVariableKind
::General
)).take(*len
),
998 builder
.push_binders(binders
, |builder
, PhantomData
| {
999 let placeholders_in_scope
= builder
.placeholders_in_scope();
1001 let substs
= Substitution
::from_iter(
1003 &placeholders_in_scope
[placeholders_in_scope
.len() - len
..],
1006 let tuple_ty
= TyKind
::Tuple(*len
, substs
.clone()).intern(interner
);
1007 let sized
= builder
.db
.well_known_trait_id(WellKnownTrait
::Sized
);
1008 builder
.push_clause(
1009 WellFormed
::Ty(tuple_ty
),
1010 substs
.as_slice(interner
)[..*len
- 1]
1013 let ty_var
= s
.assert_ty_ref(interner
).clone();
1015 DomainGoal
::Holds(WhereClause
::Implemented(TraitRef
{
1017 substitution
: Substitution
::from1(interner
, ty_var
),
1021 .chain(substs
.iter(interner
).map(|subst
| {
1022 DomainGoal
::WellFormed(WellFormed
::Ty(
1023 subst
.assert_ty_ref(interner
).clone(),
1029 TyKind
::Closure(_
, _
) | TyKind
::Generator(_
, _
) | TyKind
::GeneratorWitness(_
, _
) => {
1030 let ty
= generalize
::Generalize
::apply(builder
.db
.interner(), ty
.clone());
1031 builder
.push_binders(ty
, |builder
, ty
| {
1032 builder
.push_fact(WellFormed
::Ty(ty
));
1035 TyKind
::Placeholder(_
) => {
1036 builder
.push_fact(WellFormed
::Ty(ty
.clone()));
1038 TyKind
::Alias(AliasTy
::Projection(proj
)) => builder
1040 .associated_ty_data(proj
.associated_ty_id
)
1041 .to_program_clauses(builder
, environment
),
1042 TyKind
::Alias(AliasTy
::Opaque(opaque_ty
)) => builder
1044 .opaque_ty_data(opaque_ty
.opaque_ty_id
)
1045 .to_program_clauses(builder
, environment
),
1046 TyKind
::Function(_quantified_ty
) => {
1047 let ty
= generalize
::Generalize
::apply(builder
.db
.interner(), ty
.clone());
1048 builder
.push_binders(ty
, |builder
, ty
| builder
.push_fact(WellFormed
::Ty(ty
)));
1050 TyKind
::BoundVar(_
) => return Err(Floundered
),
1051 TyKind
::Dyn(dyn_ty
) => {
1053 // - Object safety? (not needed with RFC 2027)
1055 // - Bounds on the associated types
1056 // - Checking that all associated types are specified, including
1057 // those on supertraits.
1058 // - For trait objects with GATs, if we allow them in the future,
1059 // check that the bounds are fully general (
1060 // `dyn for<'a> StreamingIterator<Item<'a> = &'a ()>` is OK,
1061 // `dyn StreamingIterator<Item<'static> = &'static ()>` is not).
1062 let generalized_ty
=
1063 generalize
::Generalize
::apply(builder
.db
.interner(), dyn_ty
.clone());
1064 builder
.push_binders(generalized_ty
, |builder
, dyn_ty
| {
1067 .substitute(interner
, &[ty
.clone().cast
::<GenericArg
<I
>>(interner
)]);
1069 let mut wf_goals
= Vec
::new();
1071 wf_goals
.extend(bounds
.iter(interner
).flat_map(|bound
| {
1072 bound
.map_ref(|bound
| -> Vec
<_
> {
1074 WhereClause
::Implemented(trait_ref
) => {
1075 vec
![DomainGoal
::WellFormed(WellFormed
::Trait(trait_ref
.clone()))]
1077 WhereClause
::AliasEq(_
)
1078 | WhereClause
::LifetimeOutlives(_
)
1079 | WhereClause
::TypeOutlives(_
) => vec
![],
1084 builder
.push_clause(WellFormed
::Ty(ty
.clone()), wf_goals
);
1091 fn match_alias_ty
<I
: Interner
>(
1092 builder
: &mut ClauseBuilder
<'_
, I
>,
1093 environment
: &Environment
<I
>,
1096 if let AliasTy
::Projection(projection_ty
) = alias
{
1099 .associated_ty_data(projection_ty
.associated_ty_id
)
1100 .to_program_clauses(builder
, environment
)
1104 #[instrument(level = "debug", skip(db))]
1105 pub fn program_clauses_for_env
<'db
, I
: Interner
>(
1106 db
: &'db
dyn RustIrDatabase
<I
>,
1107 environment
: &Environment
<I
>,
1108 ) -> ProgramClauses
<I
> {
1109 let mut last_round
= environment
1111 .as_slice(db
.interner())
1114 .collect
::<FxHashSet
<_
>>();
1115 let mut closure
= last_round
.clone();
1116 let mut next_round
= FxHashSet
::default();
1117 while !last_round
.is_empty() {
1118 elaborate_env_clauses(
1120 &last_round
.drain().collect
::<Vec
<_
>>(),
1127 .filter(|clause
| closure
.insert(clause
.clone())),
1131 ProgramClauses
::from_iter(db
.interner(), closure
)