rustc_next_trait_solver/solve/
mod.rs

1//! The next-generation trait solver, currently still WIP.
2//!
3//! As a user of rust, you can use `-Znext-solver` to enable the new trait solver.
4//!
5//! As a developer of rustc, you shouldn't be using the new trait
6//! solver without asking the trait-system-refactor-initiative, but it can
7//! be enabled with `InferCtxtBuilder::with_next_trait_solver`. This will
8//! ensure that trait solving using that inference context will be routed
9//! to the new trait solver.
10//!
11//! For a high-level overview of how this solver works, check out the relevant
12//! section of the rustc-dev-guide.
13
14mod alias_relate;
15mod assembly;
16mod effect_goals;
17mod eval_ctxt;
18pub mod inspect;
19mod normalizes_to;
20mod project_goals;
21mod search_graph;
22mod trait_goals;
23
24use rustc_type_ir::inherent::*;
25pub use rustc_type_ir::solve::*;
26use rustc_type_ir::{self as ty, Interner, TypingMode};
27use tracing::instrument;
28
29pub use self::eval_ctxt::{EvalCtxt, GenerateProofTree, SolverDelegateEvalExt};
30use crate::delegate::SolverDelegate;
31
32/// How many fixpoint iterations we should attempt inside of the solver before bailing
33/// with overflow.
34///
35/// We previously used  `cx.recursion_limit().0.checked_ilog2().unwrap_or(0)` for this.
36/// However, it feels unlikely that uncreasing the recursion limit by a power of two
37/// to get one more itereation is every useful or desirable. We now instead used a constant
38/// here. If there ever ends up some use-cases where a bigger number of fixpoint iterations
39/// is required, we can add a new attribute for that or revert this to be dependant on the
40/// recursion limit again. However, this feels very unlikely.
41const FIXPOINT_STEP_LIMIT: usize = 8;
42
43#[derive(Debug, Copy, Clone, PartialEq, Eq)]
44enum GoalEvaluationKind {
45    Root,
46    Nested,
47}
48
49/// Whether evaluating this goal ended up changing the
50/// inference state.
51#[derive(PartialEq, Eq, Debug, Hash, Clone, Copy)]
52pub enum HasChanged {
53    Yes,
54    No,
55}
56
57// FIXME(trait-system-refactor-initiative#117): we don't detect whether a response
58// ended up pulling down any universes.
59fn has_no_inference_or_external_constraints<I: Interner>(
60    response: ty::Canonical<I, Response<I>>,
61) -> bool {
62    let ExternalConstraintsData {
63        ref region_constraints,
64        ref opaque_types,
65        ref normalization_nested_goals,
66    } = *response.value.external_constraints;
67    response.value.var_values.is_identity()
68        && region_constraints.is_empty()
69        && opaque_types.is_empty()
70        && normalization_nested_goals.is_empty()
71}
72
73fn has_only_region_constraints<I: Interner>(response: ty::Canonical<I, Response<I>>) -> bool {
74    let ExternalConstraintsData {
75        region_constraints: _,
76        ref opaque_types,
77        ref normalization_nested_goals,
78    } = *response.value.external_constraints;
79    response.value.var_values.is_identity_modulo_regions()
80        && opaque_types.is_empty()
81        && normalization_nested_goals.is_empty()
82}
83
84impl<'a, D, I> EvalCtxt<'a, D>
85where
86    D: SolverDelegate<Interner = I>,
87    I: Interner,
88{
89    #[instrument(level = "trace", skip(self))]
90    fn compute_type_outlives_goal(
91        &mut self,
92        goal: Goal<I, ty::OutlivesPredicate<I, I::Ty>>,
93    ) -> QueryResult<I> {
94        let ty::OutlivesPredicate(ty, lt) = goal.predicate;
95        self.register_ty_outlives(ty, lt);
96        self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
97    }
98
99    #[instrument(level = "trace", skip(self))]
100    fn compute_region_outlives_goal(
101        &mut self,
102        goal: Goal<I, ty::OutlivesPredicate<I, I::Region>>,
103    ) -> QueryResult<I> {
104        let ty::OutlivesPredicate(a, b) = goal.predicate;
105        self.register_region_outlives(a, b);
106        self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
107    }
108
109    #[instrument(level = "trace", skip(self))]
110    fn compute_coerce_goal(&mut self, goal: Goal<I, ty::CoercePredicate<I>>) -> QueryResult<I> {
111        self.compute_subtype_goal(Goal {
112            param_env: goal.param_env,
113            predicate: ty::SubtypePredicate {
114                a_is_expected: false,
115                a: goal.predicate.a,
116                b: goal.predicate.b,
117            },
118        })
119    }
120
121    #[instrument(level = "trace", skip(self))]
122    fn compute_subtype_goal(&mut self, goal: Goal<I, ty::SubtypePredicate<I>>) -> QueryResult<I> {
123        if goal.predicate.a.is_ty_var() && goal.predicate.b.is_ty_var() {
124            self.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
125        } else {
126            self.sub(goal.param_env, goal.predicate.a, goal.predicate.b)?;
127            self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
128        }
129    }
130
131    fn compute_dyn_compatible_goal(&mut self, trait_def_id: I::DefId) -> QueryResult<I> {
132        if self.cx().trait_is_dyn_compatible(trait_def_id) {
133            self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
134        } else {
135            Err(NoSolution)
136        }
137    }
138
139    #[instrument(level = "trace", skip(self))]
140    fn compute_well_formed_goal(&mut self, goal: Goal<I, I::Term>) -> QueryResult<I> {
141        match self.well_formed_goals(goal.param_env, goal.predicate) {
142            Some(goals) => {
143                self.add_goals(GoalSource::Misc, goals);
144                self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
145            }
146            None => self.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS),
147        }
148    }
149
150    #[instrument(level = "trace", skip(self))]
151    fn compute_const_evaluatable_goal(
152        &mut self,
153        Goal { param_env, predicate: ct }: Goal<I, I::Const>,
154    ) -> QueryResult<I> {
155        match ct.kind() {
156            ty::ConstKind::Unevaluated(uv) => {
157                // We never return `NoSolution` here as `evaluate_const` emits an
158                // error itself when failing to evaluate, so emitting an additional fulfillment
159                // error in that case is unnecessary noise. This may change in the future once
160                // evaluation failures are allowed to impact selection, e.g. generic const
161                // expressions in impl headers or `where`-clauses.
162
163                // FIXME(generic_const_exprs): Implement handling for generic
164                // const expressions here.
165                if let Some(_normalized) = self.evaluate_const(param_env, uv) {
166                    self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
167                } else {
168                    self.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
169                }
170            }
171            ty::ConstKind::Infer(_) => {
172                self.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
173            }
174            ty::ConstKind::Placeholder(_) | ty::ConstKind::Value(_) | ty::ConstKind::Error(_) => {
175                self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
176            }
177            // We can freely ICE here as:
178            // - `Param` gets replaced with a placeholder during canonicalization
179            // - `Bound` cannot exist as we don't have a binder around the self Type
180            // - `Expr` is part of `feature(generic_const_exprs)` and is not implemented yet
181            ty::ConstKind::Param(_) | ty::ConstKind::Bound(_, _) | ty::ConstKind::Expr(_) => {
182                panic!("unexpected const kind: {:?}", ct)
183            }
184        }
185    }
186
187    #[instrument(level = "trace", skip(self), ret)]
188    fn compute_const_arg_has_type_goal(
189        &mut self,
190        goal: Goal<I, (I::Const, I::Ty)>,
191    ) -> QueryResult<I> {
192        let (ct, ty) = goal.predicate;
193
194        let ct_ty = match ct.kind() {
195            ty::ConstKind::Infer(_) => {
196                return self.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS);
197            }
198            ty::ConstKind::Error(_) => {
199                return self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes);
200            }
201            ty::ConstKind::Unevaluated(uv) => {
202                self.cx().type_of(uv.def).instantiate(self.cx(), uv.args)
203            }
204            ty::ConstKind::Expr(_) => unimplemented!(
205                "`feature(generic_const_exprs)` is not supported in the new trait solver"
206            ),
207            ty::ConstKind::Param(_) => {
208                unreachable!("`ConstKind::Param` should have been canonicalized to `Placeholder`")
209            }
210            ty::ConstKind::Bound(_, _) => panic!("escaping bound vars in {:?}", ct),
211            ty::ConstKind::Value(cv) => cv.ty(),
212            ty::ConstKind::Placeholder(placeholder) => {
213                self.cx().find_const_ty_from_env(goal.param_env, placeholder)
214            }
215        };
216
217        self.eq(goal.param_env, ct_ty, ty)?;
218        self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
219    }
220}
221
222impl<D, I> EvalCtxt<'_, D>
223where
224    D: SolverDelegate<Interner = I>,
225    I: Interner,
226{
227    /// Try to merge multiple possible ways to prove a goal, if that is not possible returns `None`.
228    ///
229    /// In this case we tend to flounder and return ambiguity by calling `[EvalCtxt::flounder]`.
230    #[instrument(level = "trace", skip(self), ret)]
231    fn try_merge_responses(
232        &mut self,
233        responses: &[CanonicalResponse<I>],
234    ) -> Option<CanonicalResponse<I>> {
235        if responses.is_empty() {
236            return None;
237        }
238
239        // FIXME(-Znext-solver): We should instead try to find a `Certainty::Yes` response with
240        // a subset of the constraints that all the other responses have.
241        let one = responses[0];
242        if responses[1..].iter().all(|&resp| resp == one) {
243            return Some(one);
244        }
245
246        responses
247            .iter()
248            .find(|response| {
249                response.value.certainty == Certainty::Yes
250                    && has_no_inference_or_external_constraints(**response)
251            })
252            .copied()
253    }
254
255    fn bail_with_ambiguity(&mut self, responses: &[CanonicalResponse<I>]) -> CanonicalResponse<I> {
256        debug_assert!(responses.len() > 1);
257        let maybe_cause = responses.iter().fold(MaybeCause::Ambiguity, |maybe_cause, response| {
258            // Pull down the certainty of `Certainty::Yes` to ambiguity when combining
259            // these responses, b/c we're combining more than one response and this we
260            // don't know which one applies.
261            let candidate = match response.value.certainty {
262                Certainty::Yes => MaybeCause::Ambiguity,
263                Certainty::Maybe(candidate) => candidate,
264            };
265            maybe_cause.or(candidate)
266        });
267        self.make_ambiguous_response_no_constraints(maybe_cause)
268    }
269
270    /// If we fail to merge responses we flounder and return overflow or ambiguity.
271    #[instrument(level = "trace", skip(self), ret)]
272    fn flounder(&mut self, responses: &[CanonicalResponse<I>]) -> QueryResult<I> {
273        if responses.is_empty() {
274            return Err(NoSolution);
275        } else {
276            Ok(self.bail_with_ambiguity(responses))
277        }
278    }
279
280    /// Normalize a type for when it is structurally matched on.
281    ///
282    /// This function is necessary in nearly all cases before matching on a type.
283    /// Not doing so is likely to be incomplete and therefore unsound during
284    /// coherence.
285    #[instrument(level = "trace", skip(self, param_env), ret)]
286    fn structurally_normalize_ty(
287        &mut self,
288        param_env: I::ParamEnv,
289        ty: I::Ty,
290    ) -> Result<I::Ty, NoSolution> {
291        self.structurally_normalize_term(param_env, ty.into()).map(|term| term.expect_ty())
292    }
293
294    /// Normalize a const for when it is structurally matched on, or more likely
295    /// when it needs `.try_to_*` called on it (e.g. to turn it into a usize).
296    ///
297    /// This function is necessary in nearly all cases before matching on a const.
298    /// Not doing so is likely to be incomplete and therefore unsound during
299    /// coherence.
300    #[instrument(level = "trace", skip(self, param_env), ret)]
301    fn structurally_normalize_const(
302        &mut self,
303        param_env: I::ParamEnv,
304        ct: I::Const,
305    ) -> Result<I::Const, NoSolution> {
306        self.structurally_normalize_term(param_env, ct.into()).map(|term| term.expect_const())
307    }
308
309    /// Normalize a term for when it is structurally matched on.
310    ///
311    /// This function is necessary in nearly all cases before matching on a ty/const.
312    /// Not doing so is likely to be incomplete and therefore unsound during coherence.
313    fn structurally_normalize_term(
314        &mut self,
315        param_env: I::ParamEnv,
316        term: I::Term,
317    ) -> Result<I::Term, NoSolution> {
318        if let Some(_) = term.to_alias_term() {
319            let normalized_term = self.next_term_infer_of_kind(term);
320            let alias_relate_goal = Goal::new(
321                self.cx(),
322                param_env,
323                ty::PredicateKind::AliasRelate(
324                    term,
325                    normalized_term,
326                    ty::AliasRelationDirection::Equate,
327                ),
328            );
329            // We normalize the self type to be able to relate it with
330            // types from candidates.
331            self.add_goal(GoalSource::TypeRelating, alias_relate_goal);
332            self.try_evaluate_added_goals()?;
333            Ok(self.resolve_vars_if_possible(normalized_term))
334        } else {
335            Ok(term)
336        }
337    }
338
339    fn opaque_type_is_rigid(&self, def_id: I::DefId) -> bool {
340        match self.typing_mode() {
341            // Opaques are never rigid outside of analysis mode.
342            TypingMode::Coherence | TypingMode::PostAnalysis => false,
343            // During analysis, opaques are rigid unless they may be defined by
344            // the current body.
345            TypingMode::Analysis { defining_opaque_types_and_generators: non_rigid_opaques }
346            | TypingMode::Borrowck { defining_opaque_types: non_rigid_opaques }
347            | TypingMode::PostBorrowckAnalysis { defined_opaque_types: non_rigid_opaques } => {
348                !def_id.as_local().is_some_and(|def_id| non_rigid_opaques.contains(&def_id))
349            }
350        }
351    }
352}
353
354fn response_no_constraints_raw<I: Interner>(
355    cx: I,
356    max_universe: ty::UniverseIndex,
357    variables: I::CanonicalVarKinds,
358    certainty: Certainty,
359) -> CanonicalResponse<I> {
360    ty::Canonical {
361        max_universe,
362        variables,
363        value: Response {
364            var_values: ty::CanonicalVarValues::make_identity(cx, variables),
365            // FIXME: maybe we should store the "no response" version in cx, like
366            // we do for cx.types and stuff.
367            external_constraints: cx.mk_external_constraints(ExternalConstraintsData::default()),
368            certainty,
369        },
370    }
371}