]>
Commit | Line | Data |
---|---|---|
9c376795 FG |
1 | //! The new trait solver, currently still WIP. |
2 | //! | |
3 | //! As a user of the trait system, you can use `TyCtxt::evaluate_goal` to | |
4 | //! interact with this solver. | |
5 | //! | |
6 | //! For a high-level overview of how this solver works, check out the relevant | |
7 | //! section of the rustc-dev-guide. | |
8 | //! | |
9 | //! FIXME(@lcnr): Write that section. If you read this before then ask me | |
10 | //! about it on zulip. | |
11 | ||
9ffffee4 FG |
12 | use rustc_hir::def_id::DefId; |
13 | use rustc_infer::infer::canonical::{Canonical, CanonicalVarValues}; | |
9c376795 | 14 | use rustc_infer::traits::query::NoSolution; |
353b0b11 FG |
15 | use rustc_middle::traits::solve::{ |
16 | CanonicalResponse, Certainty, ExternalConstraintsData, Goal, QueryResult, Response, | |
17 | }; | |
9c376795 | 18 | use rustc_middle::ty::{self, Ty, TyCtxt}; |
9ffffee4 | 19 | use rustc_middle::ty::{ |
353b0b11 | 20 | CoercePredicate, RegionOutlivesPredicate, SubtypePredicate, TypeOutlivesPredicate, |
9ffffee4 | 21 | }; |
9c376795 FG |
22 | |
23 | mod assembly; | |
353b0b11 | 24 | mod canonicalize; |
9ffffee4 | 25 | mod eval_ctxt; |
9c376795 | 26 | mod fulfill; |
9c376795 FG |
27 | mod project_goals; |
28 | mod search_graph; | |
29 | mod trait_goals; | |
30 | ||
353b0b11 | 31 | pub use eval_ctxt::{EvalCtxt, InferCtxtEvalExt}; |
9c376795 FG |
32 | pub use fulfill::FulfillmentCtxt; |
33 | ||
353b0b11 FG |
34 | #[derive(Debug, Clone, Copy)] |
35 | enum SolverMode { | |
36 | /// Ordinary trait solving, using everywhere except for coherence. | |
37 | Normal, | |
38 | /// Trait solving during coherence. There are a few notable differences | |
39 | /// between coherence and ordinary trait solving. | |
40 | /// | |
41 | /// Most importantly, trait solving during coherence must not be incomplete, | |
42 | /// i.e. return `Err(NoSolution)` for goals for which a solution exists. | |
43 | /// This means that we must not make any guesses or arbitrary choices. | |
44 | Coherence, | |
9c376795 FG |
45 | } |
46 | ||
9ffffee4 FG |
47 | trait CanonicalResponseExt { |
48 | fn has_no_inference_or_external_constraints(&self) -> bool; | |
353b0b11 FG |
49 | |
50 | fn has_only_region_constraints(&self) -> bool; | |
9ffffee4 FG |
51 | } |
52 | ||
53 | impl<'tcx> CanonicalResponseExt for Canonical<'tcx, Response<'tcx>> { | |
54 | fn has_no_inference_or_external_constraints(&self) -> bool { | |
55 | self.value.external_constraints.region_constraints.is_empty() | |
56 | && self.value.var_values.is_identity() | |
57 | && self.value.external_constraints.opaque_types.is_empty() | |
58 | } | |
9ffffee4 | 59 | |
353b0b11 FG |
60 | fn has_only_region_constraints(&self) -> bool { |
61 | self.value.var_values.is_identity_modulo_regions() | |
62 | && self.value.external_constraints.opaque_types.is_empty() | |
9ffffee4 | 63 | } |
9c376795 FG |
64 | } |
65 | ||
66 | impl<'a, 'tcx> EvalCtxt<'a, 'tcx> { | |
353b0b11 | 67 | #[instrument(level = "debug", skip(self))] |
9c376795 FG |
68 | fn compute_type_outlives_goal( |
69 | &mut self, | |
9ffffee4 | 70 | goal: Goal<'tcx, TypeOutlivesPredicate<'tcx>>, |
9c376795 | 71 | ) -> QueryResult<'tcx> { |
9ffffee4 | 72 | let ty::OutlivesPredicate(ty, lt) = goal.predicate; |
353b0b11 FG |
73 | self.register_ty_outlives(ty, lt); |
74 | self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes) | |
9c376795 FG |
75 | } |
76 | ||
353b0b11 | 77 | #[instrument(level = "debug", skip(self))] |
9c376795 FG |
78 | fn compute_region_outlives_goal( |
79 | &mut self, | |
9ffffee4 | 80 | goal: Goal<'tcx, RegionOutlivesPredicate<'tcx>>, |
9c376795 | 81 | ) -> QueryResult<'tcx> { |
353b0b11 FG |
82 | let ty::OutlivesPredicate(a, b) = goal.predicate; |
83 | self.register_region_outlives(a, b); | |
84 | self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes) | |
9c376795 | 85 | } |
9ffffee4 | 86 | |
353b0b11 | 87 | #[instrument(level = "debug", skip(self))] |
9ffffee4 FG |
88 | fn compute_coerce_goal( |
89 | &mut self, | |
90 | goal: Goal<'tcx, CoercePredicate<'tcx>>, | |
91 | ) -> QueryResult<'tcx> { | |
92 | self.compute_subtype_goal(Goal { | |
93 | param_env: goal.param_env, | |
94 | predicate: SubtypePredicate { | |
95 | a_is_expected: false, | |
96 | a: goal.predicate.a, | |
97 | b: goal.predicate.b, | |
98 | }, | |
99 | }) | |
100 | } | |
101 | ||
353b0b11 | 102 | #[instrument(level = "debug", skip(self))] |
9ffffee4 FG |
103 | fn compute_subtype_goal( |
104 | &mut self, | |
105 | goal: Goal<'tcx, SubtypePredicate<'tcx>>, | |
106 | ) -> QueryResult<'tcx> { | |
107 | if goal.predicate.a.is_ty_var() && goal.predicate.b.is_ty_var() { | |
353b0b11 | 108 | self.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS) |
9ffffee4 | 109 | } else { |
353b0b11 FG |
110 | self.sub(goal.param_env, goal.predicate.a, goal.predicate.b)?; |
111 | self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes) | |
9ffffee4 FG |
112 | } |
113 | } | |
114 | ||
353b0b11 | 115 | #[instrument(level = "debug", skip(self))] |
9ffffee4 FG |
116 | fn compute_closure_kind_goal( |
117 | &mut self, | |
118 | goal: Goal<'tcx, (DefId, ty::SubstsRef<'tcx>, ty::ClosureKind)>, | |
119 | ) -> QueryResult<'tcx> { | |
120 | let (_, substs, expected_kind) = goal.predicate; | |
121 | let found_kind = substs.as_closure().kind_ty().to_opt_closure_kind(); | |
122 | ||
123 | let Some(found_kind) = found_kind else { | |
353b0b11 | 124 | return self.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS); |
9ffffee4 FG |
125 | }; |
126 | if found_kind.extends(expected_kind) { | |
353b0b11 | 127 | self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes) |
9ffffee4 FG |
128 | } else { |
129 | Err(NoSolution) | |
130 | } | |
131 | } | |
132 | ||
353b0b11 | 133 | #[instrument(level = "debug", skip(self))] |
9ffffee4 FG |
134 | fn compute_object_safe_goal(&mut self, trait_def_id: DefId) -> QueryResult<'tcx> { |
135 | if self.tcx().check_is_object_safe(trait_def_id) { | |
353b0b11 | 136 | self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes) |
9ffffee4 FG |
137 | } else { |
138 | Err(NoSolution) | |
139 | } | |
140 | } | |
141 | ||
353b0b11 | 142 | #[instrument(level = "debug", skip(self))] |
9ffffee4 FG |
143 | fn compute_well_formed_goal( |
144 | &mut self, | |
145 | goal: Goal<'tcx, ty::GenericArg<'tcx>>, | |
146 | ) -> QueryResult<'tcx> { | |
353b0b11 FG |
147 | match self.well_formed_goals(goal.param_env, goal.predicate) { |
148 | Some(goals) => { | |
149 | self.add_goals(goals); | |
150 | self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes) | |
151 | } | |
152 | None => self.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS), | |
9ffffee4 FG |
153 | } |
154 | } | |
155 | ||
156 | #[instrument(level = "debug", skip(self), ret)] | |
353b0b11 | 157 | fn compute_alias_relate_goal( |
9ffffee4 | 158 | &mut self, |
353b0b11 | 159 | goal: Goal<'tcx, (ty::Term<'tcx>, ty::Term<'tcx>, ty::AliasRelationDirection)>, |
9ffffee4 FG |
160 | ) -> QueryResult<'tcx> { |
161 | let tcx = self.tcx(); | |
353b0b11 FG |
162 | // We may need to invert the alias relation direction if dealing an alias on the RHS. |
163 | #[derive(Debug)] | |
164 | enum Invert { | |
165 | No, | |
166 | Yes, | |
167 | } | |
168 | let evaluate_normalizes_to = | |
169 | |ecx: &mut EvalCtxt<'_, 'tcx>, alias, other, direction, invert| { | |
170 | let span = tracing::span!( | |
171 | tracing::Level::DEBUG, | |
172 | "compute_alias_relate_goal(evaluate_normalizes_to)", | |
173 | ?alias, | |
174 | ?other, | |
175 | ?direction, | |
176 | ?invert | |
177 | ); | |
178 | let _enter = span.enter(); | |
179 | let result = ecx.probe(|ecx| { | |
180 | let other = match direction { | |
181 | // This is purely an optimization. | |
182 | ty::AliasRelationDirection::Equate => other, | |
183 | ||
184 | ty::AliasRelationDirection::Subtype => { | |
185 | let fresh = ecx.next_term_infer_of_kind(other); | |
186 | let (sub, sup) = match invert { | |
187 | Invert::No => (fresh, other), | |
188 | Invert::Yes => (other, fresh), | |
189 | }; | |
190 | ecx.sub(goal.param_env, sub, sup)?; | |
191 | fresh | |
192 | } | |
193 | }; | |
194 | ecx.add_goal(goal.with( | |
195 | tcx, | |
196 | ty::Binder::dummy(ty::ProjectionPredicate { | |
197 | projection_ty: alias, | |
198 | term: other, | |
199 | }), | |
200 | )); | |
201 | ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes) | |
202 | }); | |
203 | debug!(?result); | |
204 | result | |
205 | }; | |
9ffffee4 | 206 | |
353b0b11 | 207 | let (lhs, rhs, direction) = goal.predicate; |
9ffffee4 | 208 | |
353b0b11 | 209 | if lhs.is_infer() || rhs.is_infer() { |
9ffffee4 | 210 | bug!( |
353b0b11 | 211 | "`AliasRelate` goal with an infer var on lhs or rhs which should have been instantiated" |
9ffffee4 FG |
212 | ); |
213 | } | |
214 | ||
353b0b11 FG |
215 | match (lhs.to_projection_term(tcx), rhs.to_projection_term(tcx)) { |
216 | (None, None) => bug!("`AliasRelate` goal without an alias on either lhs or rhs"), | |
9ffffee4 | 217 | |
353b0b11 FG |
218 | // RHS is not a projection, only way this is true is if LHS normalizes-to RHS |
219 | (Some(alias_lhs), None) => { | |
220 | evaluate_normalizes_to(self, alias_lhs, rhs, direction, Invert::No) | |
221 | } | |
222 | ||
223 | // LHS is not a projection, only way this is true is if RHS normalizes-to LHS | |
224 | (None, Some(alias_rhs)) => { | |
225 | evaluate_normalizes_to(self, alias_rhs, lhs, direction, Invert::Yes) | |
226 | } | |
9ffffee4 | 227 | |
353b0b11 FG |
228 | (Some(alias_lhs), Some(alias_rhs)) => { |
229 | debug!("both sides are aliases"); | |
230 | ||
231 | let mut candidates = Vec::new(); | |
232 | // LHS normalizes-to RHS | |
233 | candidates.extend( | |
234 | evaluate_normalizes_to(self, alias_lhs, rhs, direction, Invert::No).ok(), | |
235 | ); | |
236 | // RHS normalizes-to RHS | |
237 | candidates.extend( | |
238 | evaluate_normalizes_to(self, alias_rhs, lhs, direction, Invert::Yes).ok(), | |
239 | ); | |
240 | // Relate via substs | |
241 | candidates.extend( | |
242 | self.probe(|ecx| { | |
243 | let span = tracing::span!( | |
244 | tracing::Level::DEBUG, | |
245 | "compute_alias_relate_goal(relate_via_substs)", | |
246 | ?alias_lhs, | |
247 | ?alias_rhs, | |
248 | ?direction | |
249 | ); | |
250 | let _enter = span.enter(); | |
251 | ||
252 | match direction { | |
253 | ty::AliasRelationDirection::Equate => { | |
254 | ecx.eq(goal.param_env, alias_lhs, alias_rhs)?; | |
255 | } | |
256 | ty::AliasRelationDirection::Subtype => { | |
257 | ecx.sub(goal.param_env, alias_lhs, alias_rhs)?; | |
258 | } | |
259 | } | |
9ffffee4 | 260 | |
353b0b11 FG |
261 | ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes) |
262 | }) | |
263 | .ok(), | |
264 | ); | |
9ffffee4 FG |
265 | debug!(?candidates); |
266 | ||
353b0b11 FG |
267 | if let Some(merged) = self.try_merge_responses(&candidates) { |
268 | Ok(merged) | |
269 | } else { | |
270 | self.flounder(&candidates) | |
271 | } | |
9ffffee4 FG |
272 | } |
273 | } | |
274 | } | |
275 | ||
276 | #[instrument(level = "debug", skip(self), ret)] | |
277 | fn compute_const_arg_has_type_goal( | |
278 | &mut self, | |
279 | goal: Goal<'tcx, (ty::Const<'tcx>, Ty<'tcx>)>, | |
280 | ) -> QueryResult<'tcx> { | |
281 | let (ct, ty) = goal.predicate; | |
353b0b11 FG |
282 | self.eq(goal.param_env, ct.ty(), ty)?; |
283 | self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes) | |
9ffffee4 | 284 | } |
9c376795 FG |
285 | } |
286 | ||
287 | impl<'tcx> EvalCtxt<'_, 'tcx> { | |
353b0b11 FG |
288 | #[instrument(level = "debug", skip(self))] |
289 | fn set_normalizes_to_hack_goal(&mut self, goal: Goal<'tcx, ty::ProjectionPredicate<'tcx>>) { | |
290 | assert!( | |
291 | self.nested_goals.normalizes_to_hack_goal.is_none(), | |
292 | "attempted to set the projection eq hack goal when one already exists" | |
293 | ); | |
294 | self.nested_goals.normalizes_to_hack_goal = Some(goal); | |
295 | } | |
9c376795 | 296 | |
353b0b11 FG |
297 | #[instrument(level = "debug", skip(self))] |
298 | fn add_goal(&mut self, goal: Goal<'tcx, ty::Predicate<'tcx>>) { | |
299 | self.nested_goals.goals.push(goal); | |
9c376795 FG |
300 | } |
301 | ||
353b0b11 FG |
302 | #[instrument(level = "debug", skip(self, goals))] |
303 | fn add_goals(&mut self, goals: impl IntoIterator<Item = Goal<'tcx, ty::Predicate<'tcx>>>) { | |
304 | let current_len = self.nested_goals.goals.len(); | |
305 | self.nested_goals.goals.extend(goals); | |
306 | debug!("added_goals={:?}", &self.nested_goals.goals[current_len..]); | |
9c376795 | 307 | } |
9c376795 | 308 | |
353b0b11 FG |
309 | /// Try to merge multiple possible ways to prove a goal, if that is not possible returns `None`. |
310 | /// | |
311 | /// In this case we tend to flounder and return ambiguity by calling `[EvalCtxt::flounder]`. | |
312 | #[instrument(level = "debug", skip(self), ret)] | |
9ffffee4 FG |
313 | fn try_merge_responses( |
314 | &mut self, | |
353b0b11 FG |
315 | responses: &[CanonicalResponse<'tcx>], |
316 | ) -> Option<CanonicalResponse<'tcx>> { | |
317 | if responses.is_empty() { | |
318 | return None; | |
9ffffee4 FG |
319 | } |
320 | ||
353b0b11 | 321 | // FIXME(-Ztrait-solver=next): We should instead try to find a `Certainty::Yes` response with |
9ffffee4 | 322 | // a subset of the constraints that all the other responses have. |
353b0b11 FG |
323 | let one = responses[0]; |
324 | if responses[1..].iter().all(|&resp| resp == one) { | |
325 | return Some(one); | |
9ffffee4 FG |
326 | } |
327 | ||
353b0b11 FG |
328 | responses |
329 | .iter() | |
330 | .find(|response| { | |
331 | response.value.certainty == Certainty::Yes | |
332 | && response.has_no_inference_or_external_constraints() | |
333 | }) | |
334 | .copied() | |
335 | } | |
9ffffee4 | 336 | |
353b0b11 FG |
337 | /// If we fail to merge responses we flounder and return overflow or ambiguity. |
338 | #[instrument(level = "debug", skip(self), ret)] | |
339 | fn flounder(&mut self, responses: &[CanonicalResponse<'tcx>]) -> QueryResult<'tcx> { | |
340 | if responses.is_empty() { | |
341 | return Err(NoSolution); | |
342 | } | |
343 | let certainty = responses.iter().fold(Certainty::AMBIGUOUS, |certainty, response| { | |
344 | certainty.unify_with(response.value.certainty) | |
9ffffee4 | 345 | }); |
353b0b11 FG |
346 | |
347 | let response = self.evaluate_added_goals_and_make_canonical_response(certainty); | |
348 | if let Ok(response) = response { | |
9ffffee4 | 349 | assert!(response.has_no_inference_or_external_constraints()); |
353b0b11 FG |
350 | Ok(response) |
351 | } else { | |
352 | bug!("failed to make floundered response: {responses:?}"); | |
9ffffee4 | 353 | } |
9ffffee4 | 354 | } |
9c376795 FG |
355 | } |
356 | ||
357 | pub(super) fn response_no_constraints<'tcx>( | |
358 | tcx: TyCtxt<'tcx>, | |
359 | goal: Canonical<'tcx, impl Sized>, | |
360 | certainty: Certainty, | |
361 | ) -> QueryResult<'tcx> { | |
9c376795 FG |
362 | Ok(Canonical { |
363 | max_universe: goal.max_universe, | |
364 | variables: goal.variables, | |
365 | value: Response { | |
9ffffee4 FG |
366 | var_values: CanonicalVarValues::make_identity(tcx, goal.variables), |
367 | // FIXME: maybe we should store the "no response" version in tcx, like | |
368 | // we do for tcx.types and stuff. | |
369 | external_constraints: tcx.mk_external_constraints(ExternalConstraintsData::default()), | |
9c376795 FG |
370 | certainty, |
371 | }, | |
372 | }) | |
373 | } |