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: `CanonicalVarValues` should be interned and `Copy`.
18 // FIXME: uses of `infcx.at` need to enable deferred projection equality once that's implemented.
22 use rustc_hir::def_id::DefId;
23 use rustc_infer::infer::canonical::{Canonical, CanonicalVarKind, CanonicalVarValues};
24 use rustc_infer::infer::canonical::{OriginalQueryValues, QueryRegionConstraints, QueryResponse};
25 use rustc_infer::infer::{InferCtxt, InferOk, TyCtxtInferExt};
26 use rustc_infer::traits::query::NoSolution;
27 use rustc_infer::traits::Obligation;
28 use rustc_middle::infer::canonical::Certainty as OldCertainty;
29 use rustc_middle::ty::{self, Ty, TyCtxt};
30 use rustc_middle::ty::{
31 CoercePredicate, RegionOutlivesPredicate, SubtypePredicate, ToPredicate, TypeOutlivesPredicate,
33 use rustc_span::DUMMY_SP;
35 use crate::traits::ObligationCause;
44 pub use fulfill::FulfillmentCtxt;
46 /// A goal is a statement, i.e. `predicate`, we want to prove
47 /// given some assumptions, i.e. `param_env`.
49 /// Most of the time the `param_env` contains the `where`-bounds of the function
50 /// we're currently typechecking while the `predicate` is some trait bound.
51 #[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, TypeFoldable, TypeVisitable)]
52 pub struct Goal<'tcx, P> {
53 param_env: ty::ParamEnv<'tcx>,
57 impl<'tcx, P> Goal<'tcx, P> {
60 param_env: ty::ParamEnv<'tcx>,
61 predicate: impl ToPredicate<'tcx, P>,
63 Goal { param_env, predicate: predicate.to_predicate(tcx) }
66 /// Updates the goal to one with a different `predicate` but the same `param_env`.
67 fn with<Q>(self, tcx: TyCtxt<'tcx>, predicate: impl ToPredicate<'tcx, Q>) -> Goal<'tcx, Q> {
68 Goal { param_env: self.param_env, predicate: predicate.to_predicate(tcx) }
72 impl<'tcx, P> From<Obligation<'tcx, P>> for Goal<'tcx, P> {
73 fn from(obligation: Obligation<'tcx, P>) -> Goal<'tcx, P> {
74 Goal { param_env: obligation.param_env, predicate: obligation.predicate }
78 #[derive(Debug, PartialEq, Eq, Clone, Hash, TypeFoldable, TypeVisitable)]
79 pub struct Response<'tcx> {
80 pub var_values: CanonicalVarValues<'tcx>,
81 /// Additional constraints returned by this query.
82 pub external_constraints: ExternalConstraints<'tcx>,
83 pub certainty: Certainty,
86 #[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, TypeFoldable, TypeVisitable)]
93 pub const AMBIGUOUS: Certainty = Certainty::Maybe(MaybeCause::Ambiguity);
95 /// When proving multiple goals using **AND**, e.g. nested obligations for an impl,
96 /// use this function to unify the certainty of these goals
97 pub fn unify_and(self, other: Certainty) -> Certainty {
99 (Certainty::Yes, Certainty::Yes) => Certainty::Yes,
100 (Certainty::Yes, Certainty::Maybe(_)) => other,
101 (Certainty::Maybe(_), Certainty::Yes) => self,
102 (Certainty::Maybe(MaybeCause::Overflow), Certainty::Maybe(MaybeCause::Overflow)) => {
103 Certainty::Maybe(MaybeCause::Overflow)
105 // If at least one of the goals is ambiguous, hide the overflow as the ambiguous goal
106 // may still result in failure.
107 (Certainty::Maybe(MaybeCause::Ambiguity), Certainty::Maybe(_))
108 | (Certainty::Maybe(_), Certainty::Maybe(MaybeCause::Ambiguity)) => {
109 Certainty::Maybe(MaybeCause::Ambiguity)
115 /// Why we failed to evaluate a goal.
116 #[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, TypeFoldable, TypeVisitable)]
117 pub enum MaybeCause {
118 /// We failed due to ambiguity. This ambiguity can either
119 /// be a true ambiguity, i.e. there are multiple different answers,
120 /// or we hit a case where we just don't bother, e.g. `?x: Trait` goals.
122 /// We gave up due to an overflow, most often by hitting the recursion limit.
126 /// Additional constraints returned on success.
127 #[derive(Debug, PartialEq, Eq, Clone, Hash, TypeFoldable, TypeVisitable, Default)]
128 pub struct ExternalConstraints<'tcx> {
129 // FIXME: implement this.
131 opaque_types: Vec<(Ty<'tcx>, Ty<'tcx>)>,
134 type CanonicalGoal<'tcx, T = ty::Predicate<'tcx>> = Canonical<'tcx, Goal<'tcx, T>>;
135 type CanonicalResponse<'tcx> = Canonical<'tcx, Response<'tcx>>;
136 /// The result of evaluating a canonical query.
138 /// FIXME: We use a different type than the existing canonical queries. This is because
139 /// we need to add a `Certainty` for `overflow` and may want to restructure this code without
140 /// having to worry about changes to currently used code. Once we've made progress on this
141 /// solver, merge the two responses again.
142 pub type QueryResult<'tcx> = Result<CanonicalResponse<'tcx>, NoSolution>;
144 pub trait TyCtxtExt<'tcx> {
145 fn evaluate_goal(self, goal: CanonicalGoal<'tcx>) -> QueryResult<'tcx>;
148 impl<'tcx> TyCtxtExt<'tcx> for TyCtxt<'tcx> {
149 fn evaluate_goal(self, goal: CanonicalGoal<'tcx>) -> QueryResult<'tcx> {
150 let mut search_graph = search_graph::SearchGraph::new(self);
151 EvalCtxt::evaluate_canonical_goal(self, &mut search_graph, goal)
155 pub trait InferCtxtEvalExt<'tcx> {
156 /// Evaluates a goal from **outside** of the trait solver.
158 /// Using this while inside of the solver is wrong as it uses a new
159 /// search graph which would break cycle detection.
160 fn evaluate_root_goal(
162 goal: Goal<'tcx, ty::Predicate<'tcx>>,
163 ) -> Result<(bool, Certainty), NoSolution>;
166 impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
167 fn evaluate_root_goal(
169 goal: Goal<'tcx, ty::Predicate<'tcx>>,
170 ) -> Result<(bool, Certainty), NoSolution> {
171 let mut search_graph = search_graph::SearchGraph::new(self.tcx);
173 let result = EvalCtxt {
174 search_graph: &mut search_graph,
176 var_values: CanonicalVarValues::dummy(),
178 .evaluate_goal(goal);
180 assert!(search_graph.is_empty());
185 struct EvalCtxt<'a, 'tcx> {
186 infcx: &'a InferCtxt<'tcx>,
187 var_values: CanonicalVarValues<'tcx>,
189 search_graph: &'a mut search_graph::SearchGraph<'tcx>,
192 impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
193 fn tcx(&self) -> TyCtxt<'tcx> {
197 #[instrument(level = "debug", skip(tcx, search_graph), ret)]
198 fn evaluate_canonical_goal(
200 search_graph: &'a mut search_graph::SearchGraph<'tcx>,
201 canonical_goal: CanonicalGoal<'tcx>,
202 ) -> QueryResult<'tcx> {
203 match search_graph.try_push_stack(tcx, canonical_goal) {
205 // Our goal is already on the stack, eager return.
206 Err(response) => return response,
209 // We may have to repeatedly recompute the goal in case of coinductive cycles,
210 // check out the `cache` module for more information.
212 // FIXME: Similar to `evaluate_all`, this has to check for overflow.
214 let (ref infcx, goal, var_values) =
215 tcx.infer_ctxt().build_with_canonical(DUMMY_SP, &canonical_goal);
216 let mut ecx = EvalCtxt { infcx, var_values, search_graph };
217 let result = ecx.compute_goal(goal);
219 // FIXME: `Response` should be `Copy`
220 if search_graph.try_finalize_goal(tcx, canonical_goal, result.clone()) {
226 fn make_canonical_response(&self, certainty: Certainty) -> QueryResult<'tcx> {
227 let external_constraints = take_external_constraints(self.infcx)?;
229 Ok(self.infcx.canonicalize_response(Response {
230 var_values: self.var_values.clone(),
231 external_constraints,
236 /// Recursively evaluates `goal`, returning whether any inference vars have
237 /// been constrained and the certainty of the result.
240 goal: Goal<'tcx, ty::Predicate<'tcx>>,
241 ) -> Result<(bool, Certainty), NoSolution> {
242 let mut orig_values = OriginalQueryValues::default();
243 let canonical_goal = self.infcx.canonicalize_query(goal, &mut orig_values);
244 let canonical_response =
245 EvalCtxt::evaluate_canonical_goal(self.tcx(), self.search_graph, canonical_goal)?;
247 !canonical_response.value.var_values.is_identity(),
248 instantiate_canonical_query_response(self.infcx, &orig_values, canonical_response),
252 fn compute_goal(&mut self, goal: Goal<'tcx, ty::Predicate<'tcx>>) -> QueryResult<'tcx> {
253 let Goal { param_env, predicate } = goal;
254 let kind = predicate.kind();
255 if let Some(kind) = kind.no_bound_vars() {
257 ty::PredicateKind::Clause(ty::Clause::Trait(predicate)) => {
258 self.compute_trait_goal(Goal { param_env, predicate })
260 ty::PredicateKind::Clause(ty::Clause::Projection(predicate)) => {
261 self.compute_projection_goal(Goal { param_env, predicate })
263 ty::PredicateKind::Clause(ty::Clause::TypeOutlives(predicate)) => {
264 self.compute_type_outlives_goal(Goal { param_env, predicate })
266 ty::PredicateKind::Clause(ty::Clause::RegionOutlives(predicate)) => {
267 self.compute_region_outlives_goal(Goal { param_env, predicate })
269 ty::PredicateKind::Subtype(predicate) => {
270 self.compute_subtype_goal(Goal { param_env, predicate })
272 ty::PredicateKind::Coerce(predicate) => {
273 self.compute_coerce_goal(Goal { param_env, predicate })
275 ty::PredicateKind::ClosureKind(def_id, substs, kind) => self
276 .compute_closure_kind_goal(Goal {
278 predicate: (def_id, substs, kind),
280 ty::PredicateKind::ObjectSafe(trait_def_id) => {
281 self.compute_object_safe_goal(trait_def_id)
283 ty::PredicateKind::WellFormed(arg) => {
284 self.compute_well_formed_goal(Goal { param_env, predicate: arg })
286 ty::PredicateKind::Ambiguous => self.make_canonical_response(Certainty::AMBIGUOUS),
287 // FIXME: implement these predicates :)
288 ty::PredicateKind::ConstEvaluatable(_) | ty::PredicateKind::ConstEquate(_, _) => {
289 self.make_canonical_response(Certainty::Yes)
291 ty::PredicateKind::TypeWellFormedFromEnv(..) => {
292 bug!("TypeWellFormedFromEnv is only used for Chalk")
296 let kind = self.infcx.replace_bound_vars_with_placeholders(kind);
297 let goal = goal.with(self.tcx(), ty::Binder::dummy(kind));
298 let (_, certainty) = self.evaluate_goal(goal)?;
299 self.make_canonical_response(certainty)
303 fn compute_type_outlives_goal(
305 _goal: Goal<'tcx, TypeOutlivesPredicate<'tcx>>,
306 ) -> QueryResult<'tcx> {
307 self.make_canonical_response(Certainty::Yes)
310 fn compute_region_outlives_goal(
312 _goal: Goal<'tcx, RegionOutlivesPredicate<'tcx>>,
313 ) -> QueryResult<'tcx> {
314 self.make_canonical_response(Certainty::Yes)
317 fn compute_coerce_goal(
319 goal: Goal<'tcx, CoercePredicate<'tcx>>,
320 ) -> QueryResult<'tcx> {
321 self.compute_subtype_goal(Goal {
322 param_env: goal.param_env,
323 predicate: SubtypePredicate {
324 a_is_expected: false,
331 fn compute_subtype_goal(
333 goal: Goal<'tcx, SubtypePredicate<'tcx>>,
334 ) -> QueryResult<'tcx> {
335 if goal.predicate.a.is_ty_var() && goal.predicate.b.is_ty_var() {
336 // FIXME: Do we want to register a subtype relation between these vars?
337 // That won't actually reflect in the query response, so it seems moot.
338 self.make_canonical_response(Certainty::AMBIGUOUS)
340 self.infcx.probe(|_| {
341 let InferOk { value: (), obligations } = self
343 .at(&ObligationCause::dummy(), goal.param_env)
344 .sub(goal.predicate.a, goal.predicate.b)?;
345 self.evaluate_all_and_make_canonical_response(
346 obligations.into_iter().map(|pred| pred.into()).collect(),
352 fn compute_closure_kind_goal(
354 goal: Goal<'tcx, (DefId, ty::SubstsRef<'tcx>, ty::ClosureKind)>,
355 ) -> QueryResult<'tcx> {
356 let (_, substs, expected_kind) = goal.predicate;
357 let found_kind = substs.as_closure().kind_ty().to_opt_closure_kind();
359 let Some(found_kind) = found_kind else {
360 return self.make_canonical_response(Certainty::AMBIGUOUS);
362 if found_kind.extends(expected_kind) {
363 self.make_canonical_response(Certainty::Yes)
369 fn compute_object_safe_goal(&mut self, trait_def_id: DefId) -> QueryResult<'tcx> {
370 if self.tcx().is_object_safe(trait_def_id) {
371 self.make_canonical_response(Certainty::Yes)
377 fn compute_well_formed_goal(
379 goal: Goal<'tcx, ty::GenericArg<'tcx>>,
380 ) -> QueryResult<'tcx> {
381 self.infcx.probe(|_| {
382 match crate::traits::wf::unnormalized_obligations(
387 Some(obligations) => self.evaluate_all_and_make_canonical_response(
388 obligations.into_iter().map(|o| o.into()).collect(),
390 None => self.make_canonical_response(Certainty::AMBIGUOUS),
396 impl<'tcx> EvalCtxt<'_, 'tcx> {
399 mut goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
400 ) -> Result<Certainty, NoSolution> {
401 let mut new_goals = Vec::new();
402 self.repeat_while_none(|this| {
403 let mut has_changed = Err(Certainty::Yes);
404 for goal in goals.drain(..) {
405 let (changed, certainty) = match this.evaluate_goal(goal) {
406 Ok(result) => result,
407 Err(NoSolution) => return Some(Err(NoSolution)),
411 has_changed = Ok(());
416 Certainty::Maybe(_) => {
417 new_goals.push(goal);
418 has_changed = has_changed.map_err(|c| c.unify_and(certainty));
425 mem::swap(&mut new_goals, &mut goals);
428 Err(certainty) => Some(Ok(certainty)),
433 fn evaluate_all_and_make_canonical_response(
435 goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
436 ) -> QueryResult<'tcx> {
437 self.evaluate_all(goals).and_then(|certainty| self.make_canonical_response(certainty))
441 #[instrument(level = "debug", skip(infcx), ret)]
442 fn take_external_constraints<'tcx>(
443 infcx: &InferCtxt<'tcx>,
444 ) -> Result<ExternalConstraints<'tcx>, NoSolution> {
445 let region_obligations = infcx.take_registered_region_obligations();
446 let opaque_types = infcx.take_opaque_types_for_query_response();
447 Ok(ExternalConstraints {
448 // FIXME: Now that's definitely wrong :)
450 // Should also do the leak check here I think
451 regions: drop(region_obligations),
456 fn instantiate_canonical_query_response<'tcx>(
457 infcx: &InferCtxt<'tcx>,
458 original_values: &OriginalQueryValues<'tcx>,
459 response: CanonicalResponse<'tcx>,
461 let Ok(InferOk { value, obligations }) = infcx
462 .instantiate_query_response_and_region_obligations(
463 &ObligationCause::dummy(),
464 ty::ParamEnv::empty(),
466 &response.unchecked_map(|resp| QueryResponse {
467 var_values: resp.var_values,
468 region_constraints: QueryRegionConstraints::default(),
469 certainty: match resp.certainty {
470 Certainty::Yes => OldCertainty::Proven,
471 Certainty::Maybe(_) => OldCertainty::Ambiguous,
473 opaque_types: resp.external_constraints.opaque_types,
474 value: resp.certainty,
477 assert!(obligations.is_empty());
481 pub(super) fn response_no_constraints<'tcx>(
483 goal: Canonical<'tcx, impl Sized>,
484 certainty: Certainty,
485 ) -> QueryResult<'tcx> {
486 let var_values = goal
490 .map(|(i, info)| match info.kind {
491 CanonicalVarKind::Ty(_) | CanonicalVarKind::PlaceholderTy(_) => {
492 tcx.mk_ty(ty::Bound(ty::INNERMOST, ty::BoundVar::from_usize(i).into())).into()
494 CanonicalVarKind::Region(_) | CanonicalVarKind::PlaceholderRegion(_) => {
495 let br = ty::BoundRegion {
496 var: ty::BoundVar::from_usize(i),
497 kind: ty::BrAnon(i as u32, None),
499 tcx.mk_region(ty::ReLateBound(ty::INNERMOST, br)).into()
501 CanonicalVarKind::Const(_, ty) | CanonicalVarKind::PlaceholderConst(_, ty) => tcx
502 .mk_const(ty::ConstKind::Bound(ty::INNERMOST, ty::BoundVar::from_usize(i)), ty)
508 max_universe: goal.max_universe,
509 variables: goal.variables,
511 var_values: CanonicalVarValues { var_values },
512 external_constraints: Default::default(),