13 use rustc
::ty
::subst
::{Substs, Subst}
;
15 use rustc
::hir
::def_id
::DefId
;
16 use rustc_target
::spec
::abi
;
17 use super::ChalkInferenceContext
;
18 use crate::lowering
::Lower
;
19 use crate::generic_types
;
22 fn assemble_clauses_from_impls
<'tcx
>(
23 tcx
: ty
::TyCtxt
<'_
, '_
, 'tcx
>,
25 clauses
: &mut Vec
<Clause
<'tcx
>>
27 tcx
.for_each_impl(trait_def_id
, |impl_def_id
| {
29 tcx
.program_clauses_for(impl_def_id
)
36 fn assemble_clauses_from_assoc_ty_values
<'tcx
>(
37 tcx
: ty
::TyCtxt
<'_
, '_
, 'tcx
>,
39 clauses
: &mut Vec
<Clause
<'tcx
>>
41 tcx
.for_each_impl(trait_def_id
, |impl_def_id
| {
42 for def_id
in tcx
.associated_item_def_ids(impl_def_id
).iter() {
44 tcx
.program_clauses_for(*def_id
)
52 fn assemble_builtin_sized_impls
<'tcx
>(
53 tcx
: ty
::TyCtxt
<'_
, '_
, 'tcx
>,
56 clauses
: &mut Vec
<Clause
<'tcx
>>
58 let mut push_builtin_impl
= |ty
: ty
::Ty
<'tcx
>, nested
: &[ty
::Ty
<'tcx
>]| {
59 let clause
= ProgramClause
{
60 goal
: ty
::TraitPredicate
{
61 trait_ref
: ty
::TraitRef
{
63 substs
: tcx
.mk_substs_trait(ty
, &[]),
66 hypotheses
: tcx
.mk_goals(
69 .map(|nested_ty
| ty
::TraitRef
{
71 substs
: tcx
.mk_substs_trait(nested_ty
, &[]),
73 .map(|trait_ref
| ty
::TraitPredicate { trait_ref }
)
74 .map(|pred
| GoalKind
::DomainGoal(pred
.lower()))
75 .map(|goal_kind
| tcx
.mk_goal(goal_kind
))
77 category
: ProgramClauseCategory
::Other
,
79 // Bind innermost bound vars that may exist in `ty` and `nested`.
80 clauses
.push(Clause
::ForAll(ty
::Binder
::bind(clause
)));
84 // Non parametric primitive types.
91 ty
::Never
=> push_builtin_impl(ty
, &[]),
93 // These ones are always `Sized`.
94 &ty
::Array(_
, length
) => {
95 push_builtin_impl(tcx
.mk_ty(ty
::Array(generic_types
::bound(tcx
, 0), length
)), &[]);
98 push_builtin_impl(generic_types
::raw_ptr(tcx
, ptr
.mutbl
), &[]);
100 &ty
::Ref(_
, _
, mutbl
) => {
101 push_builtin_impl(generic_types
::ref_ty(tcx
, mutbl
), &[]);
103 ty
::FnPtr(fn_ptr
) => {
104 let fn_ptr
= fn_ptr
.skip_binder();
105 let fn_ptr
= generic_types
::fn_ptr(
107 fn_ptr
.inputs_and_output
.len(),
112 push_builtin_impl(fn_ptr
, &[]);
114 &ty
::FnDef(def_id
, ..) => {
115 push_builtin_impl(generic_types
::fn_def(tcx
, def_id
), &[]);
117 &ty
::Closure(def_id
, ..) => {
118 push_builtin_impl(generic_types
::closure(tcx
, def_id
), &[]);
120 &ty
::Generator(def_id
, ..) => {
121 push_builtin_impl(generic_types
::generator(tcx
, def_id
), &[]);
124 // `Sized` if the last type is `Sized` (because else we will get a WF error anyway).
125 &ty
::Tuple(type_list
) => {
126 let type_list
= generic_types
::type_list(tcx
, type_list
.len());
127 push_builtin_impl(tcx
.mk_ty(ty
::Tuple(type_list
)), &**type_list
);
131 ty
::Adt(adt_def
, _
) => {
132 let substs
= Substs
::bound_vars_for_item(tcx
, adt_def
.did
);
133 let adt
= tcx
.mk_ty(ty
::Adt(adt_def
, substs
));
134 let sized_constraint
= adt_def
.sized_constraint(tcx
)
136 .map(|ty
| ty
.subst(tcx
, substs
))
137 .collect
::<Vec
<_
>>();
138 push_builtin_impl(adt
, &sized_constraint
);
141 // Artificially trigger an ambiguity.
143 // Everybody can find at least two types to unify against:
144 // general ty vars, int vars and float vars.
145 push_builtin_impl(tcx
.types
.i32, &[]);
146 push_builtin_impl(tcx
.types
.u32, &[]);
147 push_builtin_impl(tcx
.types
.f32, &[]);
148 push_builtin_impl(tcx
.types
.f64, &[]);
151 ty
::Projection(_projection_ty
) => {
152 // FIXME: add builtin impls from the associated type values found in
153 // trait impls of `projection_ty.trait_ref(tcx)`.
156 // The `Sized` bound can only come from the environment.
158 ty
::Placeholder(..) |
159 ty
::UnnormalizedProjection(..) => (),
161 // Definitely not `Sized`.
166 ty
::Opaque(..) => (),
169 ty
::GeneratorWitness(..) => bug
!("unexpected type {:?}", ty
),
173 fn wf_clause_for_raw_ptr
<'tcx
>(
174 tcx
: ty
::TyCtxt
<'_
, '_
, 'tcx
>,
175 mutbl
: hir
::Mutability
177 let ptr_ty
= generic_types
::raw_ptr(tcx
, mutbl
);
179 let wf_clause
= ProgramClause
{
180 goal
: DomainGoal
::WellFormed(WellFormed
::Ty(ptr_ty
)),
181 hypotheses
: ty
::List
::empty(),
182 category
: ProgramClauseCategory
::WellFormed
,
184 let wf_clause
= Clause
::Implies(wf_clause
);
186 // `forall<T> { WellFormed(*const T). }`
187 tcx
.mk_clauses(iter
::once(wf_clause
))
190 fn wf_clause_for_fn_ptr
<'tcx
>(
191 tcx
: ty
::TyCtxt
<'_
, '_
, 'tcx
>,
192 arity_and_output
: usize,
194 unsafety
: hir
::Unsafety
,
197 let fn_ptr
= generic_types
::fn_ptr(tcx
, arity_and_output
, variadic
, unsafety
, abi
);
199 let wf_clause
= ProgramClause
{
200 goal
: DomainGoal
::WellFormed(WellFormed
::Ty(fn_ptr
)),
201 hypotheses
: ty
::List
::empty(),
202 category
: ProgramClauseCategory
::WellFormed
,
204 let wf_clause
= Clause
::ForAll(ty
::Binder
::bind(wf_clause
));
206 // `forall <T1, ..., Tn+1> { WellFormed(for<> fn(T1, ..., Tn) -> Tn+1). }`
207 // where `n + 1` == `arity_and_output`
208 tcx
.mk_clauses(iter
::once(wf_clause
))
211 fn wf_clause_for_slice
<'tcx
>(tcx
: ty
::TyCtxt
<'_
, '_
, 'tcx
>) -> Clauses
<'tcx
> {
212 let ty
= generic_types
::bound(tcx
, 0);
213 let slice_ty
= tcx
.mk_slice(ty
);
215 let sized_trait
= match tcx
.lang_items().sized_trait() {
216 Some(def_id
) => def_id
,
217 None
=> return ty
::List
::empty(),
219 let sized_implemented
= ty
::TraitRef
{
221 substs
: tcx
.mk_substs_trait(ty
, ty
::List
::empty()),
223 let sized_implemented
: DomainGoal
= ty
::TraitPredicate
{
224 trait_ref
: sized_implemented
227 let wf_clause
= ProgramClause
{
228 goal
: DomainGoal
::WellFormed(WellFormed
::Ty(slice_ty
)),
229 hypotheses
: tcx
.mk_goals(
230 iter
::once(tcx
.mk_goal(GoalKind
::DomainGoal(sized_implemented
)))
232 category
: ProgramClauseCategory
::WellFormed
,
234 let wf_clause
= Clause
::ForAll(ty
::Binder
::bind(wf_clause
));
236 // `forall<T> { WellFormed([T]) :- Implemented(T: Sized). }`
237 tcx
.mk_clauses(iter
::once(wf_clause
))
240 fn wf_clause_for_array
<'tcx
>(
241 tcx
: ty
::TyCtxt
<'_
, '_
, 'tcx
>,
242 length
: &'tcx ty
::LazyConst
<'tcx
>
244 let ty
= generic_types
::bound(tcx
, 0);
245 let array_ty
= tcx
.mk_ty(ty
::Array(ty
, length
));
247 let sized_trait
= match tcx
.lang_items().sized_trait() {
248 Some(def_id
) => def_id
,
249 None
=> return ty
::List
::empty(),
251 let sized_implemented
= ty
::TraitRef
{
253 substs
: tcx
.mk_substs_trait(ty
, ty
::List
::empty()),
255 let sized_implemented
: DomainGoal
= ty
::TraitPredicate
{
256 trait_ref
: sized_implemented
259 let wf_clause
= ProgramClause
{
260 goal
: DomainGoal
::WellFormed(WellFormed
::Ty(array_ty
)),
261 hypotheses
: tcx
.mk_goals(
262 iter
::once(tcx
.mk_goal(GoalKind
::DomainGoal(sized_implemented
)))
264 category
: ProgramClauseCategory
::WellFormed
,
266 let wf_clause
= Clause
::ForAll(ty
::Binder
::bind(wf_clause
));
268 // `forall<T> { WellFormed([T; length]) :- Implemented(T: Sized). }`
269 tcx
.mk_clauses(iter
::once(wf_clause
))
272 fn wf_clause_for_tuple
<'tcx
>(
273 tcx
: ty
::TyCtxt
<'_
, '_
, 'tcx
>,
276 let type_list
= generic_types
::type_list(tcx
, arity
);
277 let tuple_ty
= tcx
.mk_ty(ty
::Tuple(type_list
));
279 let sized_trait
= match tcx
.lang_items().sized_trait() {
280 Some(def_id
) => def_id
,
281 None
=> return ty
::List
::empty(),
284 // If `arity == 0` (i.e. the unit type) or `arity == 1`, this list of
285 // hypotheses is actually empty.
286 let sized_implemented
= type_list
[0 .. std
::cmp
::max(arity
, 1) - 1].iter()
287 .map(|ty
| ty
::TraitRef
{
289 substs
: tcx
.mk_substs_trait(*ty
, ty
::List
::empty()),
291 .map(|trait_ref
| ty
::TraitPredicate { trait_ref }
)
292 .map(|predicate
| predicate
.lower());
294 let wf_clause
= ProgramClause
{
295 goal
: DomainGoal
::WellFormed(WellFormed
::Ty(tuple_ty
)),
296 hypotheses
: tcx
.mk_goals(
297 sized_implemented
.map(|domain_goal
| {
298 tcx
.mk_goal(GoalKind
::DomainGoal(domain_goal
))
301 category
: ProgramClauseCategory
::WellFormed
,
303 let wf_clause
= Clause
::ForAll(ty
::Binder
::bind(wf_clause
));
306 // forall<T1, ..., Tn-1, Tn> {
307 // WellFormed((T1, ..., Tn)) :-
308 // Implemented(T1: Sized),
310 // Implemented(Tn-1: Sized).
313 tcx
.mk_clauses(iter
::once(wf_clause
))
316 fn wf_clause_for_ref
<'tcx
>(
317 tcx
: ty
::TyCtxt
<'_
, '_
, 'tcx
>,
318 mutbl
: hir
::Mutability
320 let region
= tcx
.mk_region(
321 ty
::ReLateBound(ty
::INNERMOST
, ty
::BoundRegion
::BrAnon(0))
323 let ty
= generic_types
::bound(tcx
, 1);
324 let ref_ty
= tcx
.mk_ref(region
, ty
::TypeAndMut
{
329 let _outlives
: DomainGoal
= ty
::OutlivesPredicate(ty
, region
).lower();
330 let wf_clause
= ProgramClause
{
331 goal
: DomainGoal
::WellFormed(WellFormed
::Ty(ref_ty
)),
332 hypotheses
: ty
::List
::empty(),
334 // FIXME: restore this later once we get better at handling regions
335 // hypotheses: tcx.mk_goals(
336 // iter::once(tcx.mk_goal(outlives.into_goal()))
338 category
: ProgramClauseCategory
::WellFormed
,
340 let wf_clause
= Clause
::ForAll(ty
::Binder
::bind(wf_clause
));
342 // `forall<'a, T> { WellFormed(&'a T) :- Outlives(T: 'a). }`
343 tcx
.mk_clauses(iter
::once(wf_clause
))
346 fn wf_clause_for_fn_def
<'tcx
>(
347 tcx
: ty
::TyCtxt
<'_
, '_
, 'tcx
>,
350 let fn_def
= generic_types
::fn_def(tcx
, def_id
);
352 let wf_clause
= ProgramClause
{
353 goal
: DomainGoal
::WellFormed(WellFormed
::Ty(fn_def
)),
354 hypotheses
: ty
::List
::empty(),
355 category
: ProgramClauseCategory
::WellFormed
,
357 let wf_clause
= Clause
::ForAll(ty
::Binder
::bind(wf_clause
));
359 // `forall <T1, ..., Tn+1> { WellFormed(fn some_fn(T1, ..., Tn) -> Tn+1). }`
360 // where `def_id` maps to the `some_fn` function definition
361 tcx
.mk_clauses(iter
::once(wf_clause
))
364 impl ChalkInferenceContext
<'cx
, 'gcx
, 'tcx
> {
365 pub(super) fn program_clauses_impl(
367 environment
: &Environment
<'tcx
>,
368 goal
: &DomainGoal
<'tcx
>,
369 ) -> Vec
<Clause
<'tcx
>> {
370 use rustc
::traits
::WhereClause
::*;
371 use rustc
::infer
::canonical
::OriginalQueryValues
;
373 let goal
= self.infcx
.resolve_type_vars_if_possible(goal
);
375 debug
!("program_clauses(goal = {:?})", goal
);
377 let mut clauses
= match goal
{
378 DomainGoal
::Holds(Implemented(trait_predicate
)) => {
380 // * implementations of the trait itself (rule `Implemented-From-Impl`)
381 // * the trait decl (rule `Implemented-From-Env`)
383 let mut clauses
= vec
![];
385 assemble_clauses_from_impls(
387 trait_predicate
.def_id(),
391 if Some(trait_predicate
.def_id()) == self.infcx
.tcx
.lang_items().sized_trait() {
392 assemble_builtin_sized_impls(
394 trait_predicate
.def_id(),
395 trait_predicate
.self_ty(),
400 // FIXME: we need to add special rules for builtin impls:
401 // * `Copy` / `Clone`
405 // * `FnOnce` / `FnMut` / `Fn`
409 // Rule `Implemented-From-Env` will be computed from the environment.
413 DomainGoal
::Holds(ProjectionEq(projection_predicate
)) => {
415 // * the assoc type definition (rule `ProjectionEq-Placeholder`)
416 // * normalization of the assoc ty values (rule `ProjectionEq-Normalize`)
417 // * implied bounds from trait definitions (rule `Implied-Bound-From-Trait`)
418 // * implied bounds from type definitions (rule `Implied-Bound-From-Type`)
420 let clauses
= self.infcx
.tcx
.program_clauses_for(
421 projection_predicate
.projection_ty
.item_def_id
424 // only select `ProjectionEq-Placeholder` and `ProjectionEq-Normalize`
425 .filter(|clause
| clause
.category() == ProgramClauseCategory
::Other
)
428 .collect
::<Vec
<_
>>();
430 // Rules `Implied-Bound-From-Trait` and `Implied-Bound-From-Type` will be computed
431 // from the environment.
435 DomainGoal
::Holds(RegionOutlives(..)) => {
437 // * implied bounds from trait definitions (rule `Implied-Bound-From-Trait`)
438 // * implied bounds from type definitions (rule `Implied-Bound-From-Type`)
440 // All of these rules are computed in the environment.
444 DomainGoal
::Holds(TypeOutlives(..)) => {
446 // * implied bounds from trait definitions (rule `Implied-Bound-From-Trait`)
447 // * implied bounds from type definitions (rule `Implied-Bound-From-Type`)
449 // All of these rules are computed in the environment.
453 DomainGoal
::WellFormed(WellFormed
::Trait(trait_predicate
)) => {
454 // These come from -- the trait decl (rule `WellFormed-TraitRef`).
455 self.infcx
.tcx
.program_clauses_for(trait_predicate
.def_id())
458 // only select `WellFormed-TraitRef`
459 .filter(|clause
| clause
.category() == ProgramClauseCategory
::WellFormed
)
465 DomainGoal
::WellFormed(WellFormed
::Ty(ty
)) => {
467 // * the associated type definition if `ty` refers to an unnormalized
468 // associated type (rule `WellFormed-AssocTy`)
469 // * custom rules for built-in types
470 // * the type definition otherwise (rule `WellFormed-Type`)
471 let clauses
= match ty
.sty
{
472 ty
::Projection(data
) => {
473 self.infcx
.tcx
.program_clauses_for(data
.item_def_id
)
476 // These types are always WF.
484 ty
::Placeholder(..) |
487 let wf_clause
= ProgramClause
{
488 goal
: DomainGoal
::WellFormed(WellFormed
::Ty(ty
)),
489 hypotheses
: ty
::List
::empty(),
490 category
: ProgramClauseCategory
::WellFormed
,
492 let wf_clause
= Clause
::Implies(wf_clause
);
494 self.infcx
.tcx
.mk_clauses(iter
::once(wf_clause
))
497 // Always WF (recall that we do not check for parameters to be WF).
498 ty
::RawPtr(ptr
) => wf_clause_for_raw_ptr(self.infcx
.tcx
, ptr
.mutbl
),
500 // Always WF (recall that we do not check for parameters to be WF).
501 ty
::FnPtr(fn_ptr
) => {
502 let fn_ptr
= fn_ptr
.skip_binder();
503 wf_clause_for_fn_ptr(
505 fn_ptr
.inputs_and_output
.len(),
512 // WF if inner type is `Sized`.
513 ty
::Slice(..) => wf_clause_for_slice(self.infcx
.tcx
),
515 // WF if inner type is `Sized`.
516 ty
::Array(_
, length
) => wf_clause_for_array(self.infcx
.tcx
, length
),
518 // WF if all types but the last one are `Sized`.
519 ty
::Tuple(types
) => wf_clause_for_tuple(
524 // WF if `sub_ty` outlives `region`.
525 ty
::Ref(_
, _
, mutbl
) => wf_clause_for_ref(self.infcx
.tcx
, mutbl
),
527 ty
::FnDef(def_id
, ..) => wf_clause_for_fn_def(self.infcx
.tcx
, def_id
),
530 // FIXME: no rules yet for trait objects
534 ty
::Adt(def
, ..) => {
535 self.infcx
.tcx
.program_clauses_for(def
.did
)
538 // FIXME: these are probably wrong
539 ty
::Foreign(def_id
) |
540 ty
::Closure(def_id
, ..) |
541 ty
::Generator(def_id
, ..) |
542 ty
::Opaque(def_id
, ..) => {
543 self.infcx
.tcx
.program_clauses_for(def_id
)
546 // Artificially trigger an ambiguity.
548 let tcx
= self.infcx
.tcx
;
549 let types
= [tcx
.types
.i32, tcx
.types
.u32, tcx
.types
.f32, tcx
.types
.f64];
550 let clauses
= types
.iter()
552 .map(|ty
| ProgramClause
{
553 goal
: DomainGoal
::WellFormed(WellFormed
::Ty(ty
)),
554 hypotheses
: ty
::List
::empty(),
555 category
: ProgramClauseCategory
::WellFormed
,
557 .map(|clause
| Clause
::Implies(clause
));
558 tcx
.mk_clauses(clauses
)
561 ty
::GeneratorWitness(..) |
562 ty
::UnnormalizedProjection(..) |
564 bug
!("unexpected type {:?}", ty
)
569 .filter(|clause
| clause
.category() == ProgramClauseCategory
::WellFormed
)
574 DomainGoal
::FromEnv(FromEnv
::Trait(..)) => {
576 // * implied bounds from trait definitions (rule `Implied-Bound-From-Trait`)
577 // * implied bounds from type definitions (rule `Implied-Bound-From-Type`)
578 // * implied bounds from assoc type defs (rules `Implied-Trait-From-AssocTy`,
579 // `Implied-Bound-From-AssocTy` and `Implied-WC-From-AssocTy`)
581 // All of these rules are computed in the environment.
585 DomainGoal
::FromEnv(FromEnv
::Ty(..)) => {
586 // There are no `FromEnv::Ty(..) :- ...` rules (this predicate only
587 // comes from the environment).
591 DomainGoal
::Normalize(projection_predicate
) => {
592 // These come from -- assoc ty values (rule `Normalize-From-Impl`).
593 let mut clauses
= vec
![];
595 assemble_clauses_from_assoc_ty_values(
597 projection_predicate
.projection_ty
.trait_ref(self.infcx
.tcx
).def_id
,
605 debug
!("program_clauses: clauses = {:?}", clauses
);
606 debug
!("program_clauses: adding clauses from environment = {:?}", environment
);
608 let mut _orig_query_values
= OriginalQueryValues
::default();
609 let canonical_environment
= self.infcx
.canonicalize_query(
611 &mut _orig_query_values
613 let env_clauses
= self.infcx
.tcx
.program_clauses_for_env(canonical_environment
);
615 debug
!("program_clauses: env_clauses = {:?}", env_clauses
);
617 clauses
.extend(env_clauses
.into_iter().cloned());
618 clauses
.extend(environment
.clauses
.iter().cloned());