1 //! The new trait solver, currently still WIP.
3 //! As a user of the trait system, you can use `TyCtxt::evaluate_goal` to
4 //! interact with this solver.
6 //! For a high-level overview of how this solver works, check out the relevant
7 //! section of the rustc-dev-guide.
9 //! FIXME(@lcnr): Write that section. If you read this before then ask me
10 //! about it on zulip.
12 // FIXME: Instead of using `infcx.canonicalize_query` we have to add a new routine which
13 // preserves universes and creates a unique var (in the highest universe) for each
14 // appearance of a region.
16 // FIXME: uses of `infcx.at` need to enable deferred projection equality once that's implemented.
20 use rustc_hir::def_id::DefId;
21 use rustc_infer::infer::canonical::{Canonical, CanonicalVarValues};
22 use rustc_infer::infer::canonical::{OriginalQueryValues, QueryRegionConstraints, QueryResponse};
23 use rustc_infer::infer::{InferCtxt, InferOk, TyCtxtInferExt};
24 use rustc_infer::traits::query::NoSolution;
25 use rustc_infer::traits::Obligation;
26 use rustc_middle::infer::canonical::Certainty as OldCertainty;
27 use rustc_middle::traits::solve::{ExternalConstraints, ExternalConstraintsData};
28 use rustc_middle::ty::{self, TyCtxt};
29 use rustc_middle::ty::{
30 CoercePredicate, RegionOutlivesPredicate, SubtypePredicate, ToPredicate, TypeOutlivesPredicate,
32 use rustc_span::DUMMY_SP;
34 use crate::traits::ObligationCause;
43 pub use fulfill::FulfillmentCtxt;
45 /// A goal is a statement, i.e. `predicate`, we want to prove
46 /// given some assumptions, i.e. `param_env`.
48 /// Most of the time the `param_env` contains the `where`-bounds of the function
49 /// we're currently typechecking while the `predicate` is some trait bound.
50 #[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, TypeFoldable, TypeVisitable)]
51 pub struct Goal<'tcx, P> {
52 param_env: ty::ParamEnv<'tcx>,
56 impl<'tcx, P> Goal<'tcx, P> {
59 param_env: ty::ParamEnv<'tcx>,
60 predicate: impl ToPredicate<'tcx, P>,
62 Goal { param_env, predicate: predicate.to_predicate(tcx) }
65 /// Updates the goal to one with a different `predicate` but the same `param_env`.
66 fn with<Q>(self, tcx: TyCtxt<'tcx>, predicate: impl ToPredicate<'tcx, Q>) -> Goal<'tcx, Q> {
67 Goal { param_env: self.param_env, predicate: predicate.to_predicate(tcx) }
71 impl<'tcx, P> From<Obligation<'tcx, P>> for Goal<'tcx, P> {
72 fn from(obligation: Obligation<'tcx, P>) -> Goal<'tcx, P> {
73 Goal { param_env: obligation.param_env, predicate: obligation.predicate }
76 #[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, TypeFoldable, TypeVisitable)]
77 pub struct Response<'tcx> {
78 pub var_values: CanonicalVarValues<'tcx>,
79 /// Additional constraints returned by this query.
80 pub external_constraints: ExternalConstraints<'tcx>,
81 pub certainty: Certainty,
84 #[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, TypeFoldable, TypeVisitable)]
91 pub const AMBIGUOUS: Certainty = Certainty::Maybe(MaybeCause::Ambiguity);
93 /// When proving multiple goals using **AND**, e.g. nested obligations for an impl,
94 /// use this function to unify the certainty of these goals
95 pub fn unify_and(self, other: Certainty) -> Certainty {
97 (Certainty::Yes, Certainty::Yes) => Certainty::Yes,
98 (Certainty::Yes, Certainty::Maybe(_)) => other,
99 (Certainty::Maybe(_), Certainty::Yes) => self,
100 (Certainty::Maybe(MaybeCause::Overflow), Certainty::Maybe(MaybeCause::Overflow)) => {
101 Certainty::Maybe(MaybeCause::Overflow)
103 // If at least one of the goals is ambiguous, hide the overflow as the ambiguous goal
104 // may still result in failure.
105 (Certainty::Maybe(MaybeCause::Ambiguity), Certainty::Maybe(_))
106 | (Certainty::Maybe(_), Certainty::Maybe(MaybeCause::Ambiguity)) => {
107 Certainty::Maybe(MaybeCause::Ambiguity)
113 /// Why we failed to evaluate a goal.
114 #[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, TypeFoldable, TypeVisitable)]
115 pub enum MaybeCause {
116 /// We failed due to ambiguity. This ambiguity can either
117 /// be a true ambiguity, i.e. there are multiple different answers,
118 /// or we hit a case where we just don't bother, e.g. `?x: Trait` goals.
120 /// We gave up due to an overflow, most often by hitting the recursion limit.
124 type CanonicalGoal<'tcx, T = ty::Predicate<'tcx>> = Canonical<'tcx, Goal<'tcx, T>>;
125 type CanonicalResponse<'tcx> = Canonical<'tcx, Response<'tcx>>;
126 /// The result of evaluating a canonical query.
128 /// FIXME: We use a different type than the existing canonical queries. This is because
129 /// we need to add a `Certainty` for `overflow` and may want to restructure this code without
130 /// having to worry about changes to currently used code. Once we've made progress on this
131 /// solver, merge the two responses again.
132 pub type QueryResult<'tcx> = Result<CanonicalResponse<'tcx>, NoSolution>;
134 pub trait InferCtxtEvalExt<'tcx> {
135 /// Evaluates a goal from **outside** of the trait solver.
137 /// Using this while inside of the solver is wrong as it uses a new
138 /// search graph which would break cycle detection.
139 fn evaluate_root_goal(
141 goal: Goal<'tcx, ty::Predicate<'tcx>>,
142 ) -> Result<(bool, Certainty), NoSolution>;
145 impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
146 fn evaluate_root_goal(
148 goal: Goal<'tcx, ty::Predicate<'tcx>>,
149 ) -> Result<(bool, Certainty), NoSolution> {
150 let mut search_graph = search_graph::SearchGraph::new(self.tcx);
152 let result = EvalCtxt {
153 search_graph: &mut search_graph,
155 var_values: CanonicalVarValues::dummy(),
156 in_projection_eq_hack: false,
158 .evaluate_goal(goal);
160 assert!(search_graph.is_empty());
165 struct EvalCtxt<'a, 'tcx> {
166 infcx: &'a InferCtxt<'tcx>,
167 var_values: CanonicalVarValues<'tcx>,
169 search_graph: &'a mut search_graph::SearchGraph<'tcx>,
171 /// This field is used by a debug assertion in [`EvalCtxt::evaluate_goal`],
172 /// see the comment in that method for more details.
173 in_projection_eq_hack: bool,
176 impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
177 fn tcx(&self) -> TyCtxt<'tcx> {
181 /// The entry point of the solver.
183 /// This function deals with (coinductive) cycles, overflow, and caching
184 /// and then calls [`EvalCtxt::compute_goal`] which contains the actual
185 /// logic of the solver.
187 /// Instead of calling this function directly, use either [EvalCtxt::evaluate_goal]
188 /// if you're inside of the solver or [InferCtxtEvalExt::evaluate_root_goal] if you're
190 #[instrument(level = "debug", skip(tcx, search_graph), ret)]
191 fn evaluate_canonical_goal(
193 search_graph: &'a mut search_graph::SearchGraph<'tcx>,
194 canonical_goal: CanonicalGoal<'tcx>,
195 ) -> QueryResult<'tcx> {
196 match search_graph.try_push_stack(tcx, canonical_goal) {
198 // Our goal is already on the stack, eager return.
199 Err(response) => return response,
202 // We may have to repeatedly recompute the goal in case of coinductive cycles,
203 // check out the `cache` module for more information.
205 // FIXME: Similar to `evaluate_all`, this has to check for overflow.
207 let (ref infcx, goal, var_values) =
208 tcx.infer_ctxt().build_with_canonical(DUMMY_SP, &canonical_goal);
210 EvalCtxt { infcx, var_values, search_graph, in_projection_eq_hack: false };
211 let result = ecx.compute_goal(goal);
213 if search_graph.try_finalize_goal(tcx, canonical_goal, result) {
219 fn make_canonical_response(&self, certainty: Certainty) -> QueryResult<'tcx> {
220 let external_constraints = compute_external_query_constraints(self.infcx)?;
222 Ok(self.infcx.canonicalize_response(Response {
223 var_values: self.var_values,
224 external_constraints,
229 /// Recursively evaluates `goal`, returning whether any inference vars have
230 /// been constrained and the certainty of the result.
233 goal: Goal<'tcx, ty::Predicate<'tcx>>,
234 ) -> Result<(bool, Certainty), NoSolution> {
235 let mut orig_values = OriginalQueryValues::default();
236 let canonical_goal = self.infcx.canonicalize_query(goal, &mut orig_values);
237 let canonical_response =
238 EvalCtxt::evaluate_canonical_goal(self.tcx(), self.search_graph, canonical_goal)?;
240 let has_changed = !canonical_response.value.var_values.is_identity();
242 instantiate_canonical_query_response(self.infcx, &orig_values, canonical_response);
244 // Check that rerunning this query with its inference constraints applied
245 // doesn't result in new inference constraints and has the same result.
247 // If we have projection goals like `<T as Trait>::Assoc == u32` we recursively
248 // call `exists<U> <T as Trait>::Assoc == U` to enable better caching. This goal
249 // could constrain `U` to `u32` which would cause this check to result in a
251 if cfg!(debug_assertions) && has_changed && !self.in_projection_eq_hack {
252 let mut orig_values = OriginalQueryValues::default();
253 let canonical_goal = self.infcx.canonicalize_query(goal, &mut orig_values);
254 let canonical_response =
255 EvalCtxt::evaluate_canonical_goal(self.tcx(), self.search_graph, canonical_goal)?;
256 assert!(canonical_response.value.var_values.is_identity());
257 assert_eq!(certainty, canonical_response.value.certainty);
260 Ok((has_changed, certainty))
263 fn compute_goal(&mut self, goal: Goal<'tcx, ty::Predicate<'tcx>>) -> QueryResult<'tcx> {
264 let Goal { param_env, predicate } = goal;
265 let kind = predicate.kind();
266 if let Some(kind) = kind.no_bound_vars() {
268 ty::PredicateKind::Clause(ty::Clause::Trait(predicate)) => {
269 self.compute_trait_goal(Goal { param_env, predicate })
271 ty::PredicateKind::Clause(ty::Clause::Projection(predicate)) => {
272 self.compute_projection_goal(Goal { param_env, predicate })
274 ty::PredicateKind::Clause(ty::Clause::TypeOutlives(predicate)) => {
275 self.compute_type_outlives_goal(Goal { param_env, predicate })
277 ty::PredicateKind::Clause(ty::Clause::RegionOutlives(predicate)) => {
278 self.compute_region_outlives_goal(Goal { param_env, predicate })
280 ty::PredicateKind::Subtype(predicate) => {
281 self.compute_subtype_goal(Goal { param_env, predicate })
283 ty::PredicateKind::Coerce(predicate) => {
284 self.compute_coerce_goal(Goal { param_env, predicate })
286 ty::PredicateKind::ClosureKind(def_id, substs, kind) => self
287 .compute_closure_kind_goal(Goal {
289 predicate: (def_id, substs, kind),
291 ty::PredicateKind::ObjectSafe(trait_def_id) => {
292 self.compute_object_safe_goal(trait_def_id)
294 ty::PredicateKind::WellFormed(arg) => {
295 self.compute_well_formed_goal(Goal { param_env, predicate: arg })
297 ty::PredicateKind::Ambiguous => self.make_canonical_response(Certainty::AMBIGUOUS),
298 // FIXME: implement these predicates :)
299 ty::PredicateKind::ConstEvaluatable(_) | ty::PredicateKind::ConstEquate(_, _) => {
300 self.make_canonical_response(Certainty::Yes)
302 ty::PredicateKind::TypeWellFormedFromEnv(..) => {
303 bug!("TypeWellFormedFromEnv is only used for Chalk")
307 let kind = self.infcx.instantiate_binder_with_placeholders(kind);
308 let goal = goal.with(self.tcx(), ty::Binder::dummy(kind));
309 let (_, certainty) = self.evaluate_goal(goal)?;
310 self.make_canonical_response(certainty)
314 fn compute_type_outlives_goal(
316 _goal: Goal<'tcx, TypeOutlivesPredicate<'tcx>>,
317 ) -> QueryResult<'tcx> {
318 self.make_canonical_response(Certainty::Yes)
321 fn compute_region_outlives_goal(
323 _goal: Goal<'tcx, RegionOutlivesPredicate<'tcx>>,
324 ) -> QueryResult<'tcx> {
325 self.make_canonical_response(Certainty::Yes)
328 fn compute_coerce_goal(
330 goal: Goal<'tcx, CoercePredicate<'tcx>>,
331 ) -> QueryResult<'tcx> {
332 self.compute_subtype_goal(Goal {
333 param_env: goal.param_env,
334 predicate: SubtypePredicate {
335 a_is_expected: false,
342 fn compute_subtype_goal(
344 goal: Goal<'tcx, SubtypePredicate<'tcx>>,
345 ) -> QueryResult<'tcx> {
346 if goal.predicate.a.is_ty_var() && goal.predicate.b.is_ty_var() {
347 // FIXME: Do we want to register a subtype relation between these vars?
348 // That won't actually reflect in the query response, so it seems moot.
349 self.make_canonical_response(Certainty::AMBIGUOUS)
351 let InferOk { value: (), obligations } = self
353 .at(&ObligationCause::dummy(), goal.param_env)
354 .sub(goal.predicate.a, goal.predicate.b)?;
355 self.evaluate_all_and_make_canonical_response(
356 obligations.into_iter().map(|pred| pred.into()).collect(),
361 fn compute_closure_kind_goal(
363 goal: Goal<'tcx, (DefId, ty::SubstsRef<'tcx>, ty::ClosureKind)>,
364 ) -> QueryResult<'tcx> {
365 let (_, substs, expected_kind) = goal.predicate;
366 let found_kind = substs.as_closure().kind_ty().to_opt_closure_kind();
368 let Some(found_kind) = found_kind else {
369 return self.make_canonical_response(Certainty::AMBIGUOUS);
371 if found_kind.extends(expected_kind) {
372 self.make_canonical_response(Certainty::Yes)
378 fn compute_object_safe_goal(&mut self, trait_def_id: DefId) -> QueryResult<'tcx> {
379 if self.tcx().check_is_object_safe(trait_def_id) {
380 self.make_canonical_response(Certainty::Yes)
386 fn compute_well_formed_goal(
388 goal: Goal<'tcx, ty::GenericArg<'tcx>>,
389 ) -> QueryResult<'tcx> {
390 match crate::traits::wf::unnormalized_obligations(
395 Some(obligations) => self.evaluate_all_and_make_canonical_response(
396 obligations.into_iter().map(|o| o.into()).collect(),
398 None => self.make_canonical_response(Certainty::AMBIGUOUS),
403 impl<'tcx> EvalCtxt<'_, 'tcx> {
404 // Recursively evaluates a list of goals to completion, returning the certainty
405 // of all of the goals.
408 mut goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
409 ) -> Result<Certainty, NoSolution> {
410 let mut new_goals = Vec::new();
411 self.repeat_while_none(|this| {
412 let mut has_changed = Err(Certainty::Yes);
413 for goal in goals.drain(..) {
414 let (changed, certainty) = match this.evaluate_goal(goal) {
415 Ok(result) => result,
416 Err(NoSolution) => return Some(Err(NoSolution)),
420 has_changed = Ok(());
425 Certainty::Maybe(_) => {
426 new_goals.push(goal);
427 has_changed = has_changed.map_err(|c| c.unify_and(certainty));
434 mem::swap(&mut new_goals, &mut goals);
437 Err(certainty) => Some(Ok(certainty)),
442 // Recursively evaluates a list of goals to completion, making a query response.
444 // This is just a convenient way of calling [`EvalCtxt::evaluate_all`],
445 // then [`EvalCtxt::make_canonical_response`].
446 fn evaluate_all_and_make_canonical_response(
448 goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
449 ) -> QueryResult<'tcx> {
450 self.evaluate_all(goals).and_then(|certainty| self.make_canonical_response(certainty))
454 #[instrument(level = "debug", skip(infcx), ret)]
455 fn compute_external_query_constraints<'tcx>(
456 infcx: &InferCtxt<'tcx>,
457 ) -> Result<ExternalConstraints<'tcx>, NoSolution> {
458 let region_obligations = infcx.take_registered_region_obligations();
459 let opaque_types = infcx.take_opaque_types_for_query_response();
460 Ok(infcx.tcx.intern_external_constraints(ExternalConstraintsData {
461 // FIXME: Now that's definitely wrong :)
463 // Should also do the leak check here I think
464 regions: drop(region_obligations),
469 fn instantiate_canonical_query_response<'tcx>(
470 infcx: &InferCtxt<'tcx>,
471 original_values: &OriginalQueryValues<'tcx>,
472 response: CanonicalResponse<'tcx>,
474 let Ok(InferOk { value, obligations }) = infcx
475 .instantiate_query_response_and_region_obligations(
476 &ObligationCause::dummy(),
477 ty::ParamEnv::empty(),
479 &response.unchecked_map(|resp| QueryResponse {
480 var_values: resp.var_values,
481 region_constraints: QueryRegionConstraints::default(),
482 certainty: match resp.certainty {
483 Certainty::Yes => OldCertainty::Proven,
484 Certainty::Maybe(_) => OldCertainty::Ambiguous,
486 // FIXME: This to_owned makes me sad, but we should eventually impl
487 // `instantiate_query_response_and_region_obligations` separately
488 // instead of piggybacking off of the old implementation.
489 opaque_types: resp.external_constraints.opaque_types.to_owned(),
490 value: resp.certainty,
493 assert!(obligations.is_empty());
497 pub(super) fn response_no_constraints<'tcx>(
499 goal: Canonical<'tcx, impl Sized>,
500 certainty: Certainty,
501 ) -> QueryResult<'tcx> {
503 max_universe: goal.max_universe,
504 variables: goal.variables,
506 var_values: CanonicalVarValues::make_identity(tcx, goal.variables),
507 // FIXME: maybe we should store the "no response" version in tcx, like
508 // we do for tcx.types and stuff.
509 external_constraints: tcx
510 .intern_external_constraints(ExternalConstraintsData::default()),