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