rustc_type_ir/solve/
mod.rs

1pub mod inspect;
2
3use std::fmt;
4use std::hash::Hash;
5
6use derive_where::derive_where;
7#[cfg(feature = "nightly")]
8use rustc_macros::{Decodable_NoContext, Encodable_NoContext, HashStable_NoContext};
9use rustc_type_ir_macros::{Lift_Generic, TypeFoldable_Generic, TypeVisitable_Generic};
10
11use crate::lang_items::TraitSolverLangItem;
12use crate::search_graph::PathKind;
13use crate::{self as ty, Canonical, CanonicalVarValues, Interner, Upcast};
14
15pub type CanonicalInput<I, T = <I as Interner>::Predicate> =
16    ty::CanonicalQueryInput<I, QueryInput<I, T>>;
17pub type CanonicalResponse<I> = Canonical<I, Response<I>>;
18/// The result of evaluating a canonical query.
19///
20/// FIXME: We use a different type than the existing canonical queries. This is because
21/// we need to add a `Certainty` for `overflow` and may want to restructure this code without
22/// having to worry about changes to currently used code. Once we've made progress on this
23/// solver, merge the two responses again.
24pub type QueryResult<I> = Result<CanonicalResponse<I>, NoSolution>;
25
26#[derive(Copy, Clone, Debug, Hash, PartialEq, Eq)]
27#[cfg_attr(feature = "nightly", derive(HashStable_NoContext))]
28pub struct NoSolution;
29
30/// A goal is a statement, i.e. `predicate`, we want to prove
31/// given some assumptions, i.e. `param_env`.
32///
33/// Most of the time the `param_env` contains the `where`-bounds of the function
34/// we're currently typechecking while the `predicate` is some trait bound.
35#[derive_where(Clone; I: Interner, P: Clone)]
36#[derive_where(Copy; I: Interner, P: Copy)]
37#[derive_where(Hash; I: Interner, P: Hash)]
38#[derive_where(PartialEq; I: Interner, P: PartialEq)]
39#[derive_where(Eq; I: Interner, P: Eq)]
40#[derive_where(Debug; I: Interner, P: fmt::Debug)]
41#[derive(TypeVisitable_Generic, TypeFoldable_Generic, Lift_Generic)]
42#[cfg_attr(
43    feature = "nightly",
44    derive(Decodable_NoContext, Encodable_NoContext, HashStable_NoContext)
45)]
46pub struct Goal<I: Interner, P> {
47    pub param_env: I::ParamEnv,
48    pub predicate: P,
49}
50
51impl<I: Interner, P> Goal<I, P> {
52    pub fn new(cx: I, param_env: I::ParamEnv, predicate: impl Upcast<I, P>) -> Goal<I, P> {
53        Goal { param_env, predicate: predicate.upcast(cx) }
54    }
55
56    /// Updates the goal to one with a different `predicate` but the same `param_env`.
57    pub fn with<Q>(self, cx: I, predicate: impl Upcast<I, Q>) -> Goal<I, Q> {
58        Goal { param_env: self.param_env, predicate: predicate.upcast(cx) }
59    }
60}
61
62/// Why a specific goal has to be proven.
63///
64/// This is necessary as we treat nested goals different depending on
65/// their source. This is used to decide whether a cycle is coinductive.
66/// See the documentation of `EvalCtxt::step_kind_for_source` for more details
67/// about this.
68///
69/// It is also used by proof tree visitors, e.g. for diagnostics purposes.
70#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)]
71#[cfg_attr(feature = "nightly", derive(HashStable_NoContext))]
72pub enum GoalSource {
73    Misc,
74    /// A nested goal required to prove that types are equal/subtypes.
75    /// This is always an unproductive step.
76    ///
77    /// This is also used for all `NormalizesTo` goals as we they are used
78    /// to relate types in `AliasRelate`.
79    TypeRelating,
80    /// We're proving a where-bound of an impl.
81    ImplWhereBound,
82    /// Const conditions that need to hold for `[const]` alias bounds to hold.
83    AliasBoundConstCondition,
84    /// Instantiating a higher-ranked goal and re-proving it.
85    InstantiateHigherRanked,
86    /// Predicate required for an alias projection to be well-formed.
87    /// This is used in three places:
88    /// 1. projecting to an opaque whose hidden type is already registered in
89    ///    the opaque type storage,
90    /// 2. for rigid projections's trait goal,
91    /// 3. for GAT where clauses.
92    AliasWellFormed,
93    /// In case normalizing aliases in nested goals cycles, eagerly normalizing these
94    /// aliases in the context of the parent may incorrectly change the cycle kind.
95    /// Normalizing aliases in goals therefore tracks the original path kind for this
96    /// nested goal. See the comment of the `ReplaceAliasWithInfer` visitor for more
97    /// details.
98    NormalizeGoal(PathKind),
99}
100
101#[derive_where(Clone; I: Interner, Goal<I, P>: Clone)]
102#[derive_where(Copy; I: Interner, Goal<I, P>: Copy)]
103#[derive_where(Hash; I: Interner, Goal<I, P>: Hash)]
104#[derive_where(PartialEq; I: Interner, Goal<I, P>: PartialEq)]
105#[derive_where(Eq; I: Interner, Goal<I, P>: Eq)]
106#[derive_where(Debug; I: Interner, Goal<I, P>: fmt::Debug)]
107#[derive(TypeVisitable_Generic, TypeFoldable_Generic)]
108#[cfg_attr(
109    feature = "nightly",
110    derive(Decodable_NoContext, Encodable_NoContext, HashStable_NoContext)
111)]
112pub struct QueryInput<I: Interner, P> {
113    pub goal: Goal<I, P>,
114    pub predefined_opaques_in_body: I::PredefinedOpaques,
115}
116
117/// Opaques that are defined in the inference context before a query is called.
118#[derive_where(Clone, Hash, PartialEq, Eq, Debug, Default; I: Interner)]
119#[derive(TypeVisitable_Generic, TypeFoldable_Generic)]
120#[cfg_attr(
121    feature = "nightly",
122    derive(Decodable_NoContext, Encodable_NoContext, HashStable_NoContext)
123)]
124pub struct PredefinedOpaquesData<I: Interner> {
125    pub opaque_types: Vec<(ty::OpaqueTypeKey<I>, I::Ty)>,
126}
127
128/// Possible ways the given goal can be proven.
129#[derive_where(Clone, Copy, Hash, PartialEq, Eq, Debug; I: Interner)]
130pub enum CandidateSource<I: Interner> {
131    /// A user written impl.
132    ///
133    /// ## Examples
134    ///
135    /// ```rust
136    /// fn main() {
137    ///     let x: Vec<u32> = Vec::new();
138    ///     // This uses the impl from the standard library to prove `Vec<T>: Clone`.
139    ///     let y = x.clone();
140    /// }
141    /// ```
142    Impl(I::DefId),
143    /// A builtin impl generated by the compiler. When adding a new special
144    /// trait, try to use actual impls whenever possible. Builtin impls should
145    /// only be used in cases where the impl cannot be manually be written.
146    ///
147    /// Notable examples are auto traits, `Sized`, and `DiscriminantKind`.
148    /// For a list of all traits with builtin impls, check out the
149    /// `EvalCtxt::assemble_builtin_impl_candidates` method.
150    BuiltinImpl(BuiltinImplSource),
151    /// An assumption from the environment. Stores a [`ParamEnvSource`], since we
152    /// prefer non-global param-env candidates in candidate assembly.
153    ///
154    /// ## Examples
155    ///
156    /// ```rust
157    /// fn is_clone<T: Clone>(x: T) -> (T, T) {
158    ///     // This uses the assumption `T: Clone` from the `where`-bounds
159    ///     // to prove `T: Clone`.
160    ///     (x.clone(), x)
161    /// }
162    /// ```
163    ParamEnv(ParamEnvSource),
164    /// If the self type is an alias type, e.g. an opaque type or a projection,
165    /// we know the bounds on that alias to hold even without knowing its concrete
166    /// underlying type.
167    ///
168    /// More precisely this candidate is using the `n-th` bound in the `item_bounds` of
169    /// the self type.
170    ///
171    /// ## Examples
172    ///
173    /// ```rust
174    /// trait Trait {
175    ///     type Assoc: Clone;
176    /// }
177    ///
178    /// fn foo<T: Trait>(x: <T as Trait>::Assoc) {
179    ///     // We prove `<T as Trait>::Assoc` by looking at the bounds on `Assoc` in
180    ///     // in the trait definition.
181    ///     let _y = x.clone();
182    /// }
183    /// ```
184    AliasBound,
185    /// A candidate that is registered only during coherence to represent some
186    /// yet-unknown impl that could be produced downstream without violating orphan
187    /// rules.
188    // FIXME: Merge this with the forced ambiguity candidates, so those don't use `Misc`.
189    CoherenceUnknowable,
190}
191
192#[derive(Clone, Copy, Hash, PartialEq, Eq, Debug)]
193pub enum ParamEnvSource {
194    /// Preferred eagerly.
195    NonGlobal,
196    // Not considered unless there are non-global param-env candidates too.
197    Global,
198}
199
200#[derive(Clone, Copy, Hash, PartialEq, Eq, Debug)]
201#[cfg_attr(
202    feature = "nightly",
203    derive(HashStable_NoContext, Encodable_NoContext, Decodable_NoContext)
204)]
205pub enum BuiltinImplSource {
206    /// A built-in impl that is considered trivial, without any nested requirements. They
207    /// are preferred over where-clauses, and we want to track them explicitly.
208    Trivial,
209    /// Some built-in impl we don't need to differentiate. This should be used
210    /// unless more specific information is necessary.
211    Misc,
212    /// A built-in impl for trait objects. The index is only used in winnowing.
213    Object(usize),
214    /// A built-in implementation of `Upcast` for trait objects to other trait objects.
215    ///
216    /// The index is only used for winnowing.
217    TraitUpcasting(usize),
218}
219
220#[derive_where(Clone, Copy, Hash, PartialEq, Eq, Debug; I: Interner)]
221#[derive(TypeVisitable_Generic, TypeFoldable_Generic)]
222#[cfg_attr(feature = "nightly", derive(HashStable_NoContext))]
223pub struct Response<I: Interner> {
224    pub certainty: Certainty,
225    pub var_values: CanonicalVarValues<I>,
226    /// Additional constraints returned by this query.
227    pub external_constraints: I::ExternalConstraints,
228}
229
230/// Additional constraints returned on success.
231#[derive_where(Clone, Hash, PartialEq, Eq, Debug, Default; I: Interner)]
232#[derive(TypeVisitable_Generic, TypeFoldable_Generic)]
233#[cfg_attr(feature = "nightly", derive(HashStable_NoContext))]
234pub struct ExternalConstraintsData<I: Interner> {
235    pub region_constraints: Vec<ty::OutlivesPredicate<I, I::GenericArg>>,
236    pub opaque_types: Vec<(ty::OpaqueTypeKey<I>, I::Ty)>,
237    pub normalization_nested_goals: NestedNormalizationGoals<I>,
238}
239
240impl<I: Interner> ExternalConstraintsData<I> {
241    pub fn is_empty(&self) -> bool {
242        self.region_constraints.is_empty()
243            && self.opaque_types.is_empty()
244            && self.normalization_nested_goals.is_empty()
245    }
246}
247
248#[derive_where(Clone, Hash, PartialEq, Eq, Debug, Default; I: Interner)]
249#[derive(TypeVisitable_Generic, TypeFoldable_Generic)]
250#[cfg_attr(feature = "nightly", derive(HashStable_NoContext))]
251pub struct NestedNormalizationGoals<I: Interner>(pub Vec<(GoalSource, Goal<I, I::Predicate>)>);
252
253impl<I: Interner> NestedNormalizationGoals<I> {
254    pub fn empty() -> Self {
255        NestedNormalizationGoals(vec![])
256    }
257
258    pub fn is_empty(&self) -> bool {
259        self.0.is_empty()
260    }
261}
262
263#[derive(Clone, Copy, Hash, PartialEq, Eq, Debug)]
264#[cfg_attr(feature = "nightly", derive(HashStable_NoContext))]
265pub enum Certainty {
266    Yes,
267    Maybe(MaybeCause),
268}
269
270impl Certainty {
271    pub const AMBIGUOUS: Certainty = Certainty::Maybe(MaybeCause::Ambiguity);
272
273    /// Use this function to merge the certainty of multiple nested subgoals.
274    ///
275    /// Given an impl like `impl<T: Foo + Bar> Baz for T {}`, we have 2 nested
276    /// subgoals whenever we use the impl as a candidate: `T: Foo` and `T: Bar`.
277    /// If evaluating `T: Foo` results in ambiguity and `T: Bar` results in
278    /// success, we merge these two responses. This results in ambiguity.
279    ///
280    /// If we unify ambiguity with overflow, we return overflow. This doesn't matter
281    /// inside of the solver as we do not distinguish ambiguity from overflow. It does
282    /// however matter for diagnostics. If `T: Foo` resulted in overflow and `T: Bar`
283    /// in ambiguity without changing the inference state, we still want to tell the
284    /// user that `T: Baz` results in overflow.
285    pub fn and(self, other: Certainty) -> Certainty {
286        match (self, other) {
287            (Certainty::Yes, Certainty::Yes) => Certainty::Yes,
288            (Certainty::Yes, Certainty::Maybe(_)) => other,
289            (Certainty::Maybe(_), Certainty::Yes) => self,
290            (Certainty::Maybe(a), Certainty::Maybe(b)) => Certainty::Maybe(a.and(b)),
291        }
292    }
293
294    pub const fn overflow(suggest_increasing_limit: bool) -> Certainty {
295        Certainty::Maybe(MaybeCause::Overflow { suggest_increasing_limit, keep_constraints: false })
296    }
297}
298
299/// Why we failed to evaluate a goal.
300#[derive(Clone, Copy, Hash, PartialEq, Eq, Debug)]
301#[cfg_attr(feature = "nightly", derive(HashStable_NoContext))]
302pub enum MaybeCause {
303    /// We failed due to ambiguity. This ambiguity can either
304    /// be a true ambiguity, i.e. there are multiple different answers,
305    /// or we hit a case where we just don't bother, e.g. `?x: Trait` goals.
306    Ambiguity,
307    /// We gave up due to an overflow, most often by hitting the recursion limit.
308    Overflow { suggest_increasing_limit: bool, keep_constraints: bool },
309}
310
311impl MaybeCause {
312    fn and(self, other: MaybeCause) -> MaybeCause {
313        match (self, other) {
314            (MaybeCause::Ambiguity, MaybeCause::Ambiguity) => MaybeCause::Ambiguity,
315            (MaybeCause::Ambiguity, MaybeCause::Overflow { .. }) => other,
316            (MaybeCause::Overflow { .. }, MaybeCause::Ambiguity) => self,
317            (
318                MaybeCause::Overflow {
319                    suggest_increasing_limit: limit_a,
320                    keep_constraints: keep_a,
321                },
322                MaybeCause::Overflow {
323                    suggest_increasing_limit: limit_b,
324                    keep_constraints: keep_b,
325                },
326            ) => MaybeCause::Overflow {
327                suggest_increasing_limit: limit_a && limit_b,
328                keep_constraints: keep_a && keep_b,
329            },
330        }
331    }
332
333    pub fn or(self, other: MaybeCause) -> MaybeCause {
334        match (self, other) {
335            (MaybeCause::Ambiguity, MaybeCause::Ambiguity) => MaybeCause::Ambiguity,
336
337            // When combining ambiguity + overflow, we can keep constraints.
338            (
339                MaybeCause::Ambiguity,
340                MaybeCause::Overflow { suggest_increasing_limit, keep_constraints: _ },
341            ) => MaybeCause::Overflow { suggest_increasing_limit, keep_constraints: true },
342            (
343                MaybeCause::Overflow { suggest_increasing_limit, keep_constraints: _ },
344                MaybeCause::Ambiguity,
345            ) => MaybeCause::Overflow { suggest_increasing_limit, keep_constraints: true },
346
347            (
348                MaybeCause::Overflow {
349                    suggest_increasing_limit: limit_a,
350                    keep_constraints: keep_a,
351                },
352                MaybeCause::Overflow {
353                    suggest_increasing_limit: limit_b,
354                    keep_constraints: keep_b,
355                },
356            ) => MaybeCause::Overflow {
357                suggest_increasing_limit: limit_a || limit_b,
358                keep_constraints: keep_a || keep_b,
359            },
360        }
361    }
362}
363
364/// Indicates that a `impl Drop for Adt` is `const` or not.
365#[derive(Debug)]
366pub enum AdtDestructorKind {
367    NotConst,
368    Const,
369}
370
371/// Which sizedness trait - `Sized`, `MetaSized`? `PointeeSized` is omitted as it is removed during
372/// lowering.
373#[derive(Copy, Clone, Debug, Eq, Hash, PartialEq)]
374#[cfg_attr(feature = "nightly", derive(HashStable_NoContext))]
375pub enum SizedTraitKind {
376    /// `Sized` trait
377    Sized,
378    /// `MetaSized` trait
379    MetaSized,
380}
381
382impl SizedTraitKind {
383    /// Returns `DefId` of corresponding language item.
384    pub fn require_lang_item<I: Interner>(self, cx: I) -> I::DefId {
385        cx.require_lang_item(match self {
386            SizedTraitKind::Sized => TraitSolverLangItem::Sized,
387            SizedTraitKind::MetaSized => TraitSolverLangItem::MetaSized,
388        })
389    }
390}