compiler/rustc_trait_selection/src/solve/mod.rs

   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
  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.
  15
  16 // FIXME: `CanonicalVarValues` should be interned and `Copy`.
  17
  18 // FIXME: uses of `infcx.at` need to enable deferred projection equality once that's implemented.
  19
  20 use std::mem;
  21
  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,
  32 };
  33 use rustc_span::DUMMY_SP;
  34
  35 use crate::traits::ObligationCause;
  36
  37 mod assembly;
  38 mod fulfill;
  39 mod infcx_ext;
  40 mod project_goals;
  41 mod search_graph;
  42 mod trait_goals;
  43
  44 pub use fulfill::FulfillmentCtxt;
  45
  46 /// A goal is a statement, i.e. `predicate`, we want to prove
  47 /// given some assumptions, i.e. `param_env`.
  48 ///
  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>,
  54     predicate: P,
  55 }
  56
  57 impl<'tcx, P> Goal<'tcx, P> {
  58     pub fn new(
  59         tcx: TyCtxt<'tcx>,
  60         param_env: ty::ParamEnv<'tcx>,
  61         predicate: impl ToPredicate<'tcx, P>,
  62     ) -> Goal<'tcx, P> {
  63         Goal { param_env, predicate: predicate.to_predicate(tcx) }
  64     }
  65
  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) }
  69     }
  70 }
  71
  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 }
  75     }
  76 }
  77
  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,
  84 }
  85
  86 #[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, TypeFoldable, TypeVisitable)]
  87 pub enum Certainty {
  88     Yes,
  89     Maybe(MaybeCause),
  90 }
  91
  92 impl Certainty {
  93     pub const AMBIGUOUS: Certainty = Certainty::Maybe(MaybeCause::Ambiguity);
  94
  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 {
  98         match (self, other) {
  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)
 104             }
 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)
 110             }
 111         }
 112     }
 113 }
 114
 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.
 121     Ambiguity,
 122     /// We gave up due to an overflow, most often by hitting the recursion limit.
 123     Overflow,
 124 }
 125
 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.
 130     regions: (),
 131     opaque_types: Vec<(Ty<'tcx>, Ty<'tcx>)>,
 132 }
 133
 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.
 137 ///
 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>;
 143
 144 pub trait TyCtxtExt<'tcx> {
 145     fn evaluate_goal(self, goal: CanonicalGoal<'tcx>) -> QueryResult<'tcx>;
 146 }
 147
 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)
 152     }
 153 }
 154
 155 pub trait InferCtxtEvalExt<'tcx> {
 156     /// Evaluates a goal from **outside** of the trait solver.
 157     ///
 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(
 161         &self,
 162         goal: Goal<'tcx, ty::Predicate<'tcx>>,
 163     ) -> Result<(bool, Certainty), NoSolution>;
 164 }
 165
 166 impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
 167     fn evaluate_root_goal(
 168         &self,
 169         goal: Goal<'tcx, ty::Predicate<'tcx>>,
 170     ) -> Result<(bool, Certainty), NoSolution> {
 171         let mut search_graph = search_graph::SearchGraph::new(self.tcx);
 172
 173         let result = EvalCtxt {
 174             search_graph: &mut search_graph,
 175             infcx: self,
 176             var_values: CanonicalVarValues::dummy(),
 177         }
 178         .evaluate_goal(goal);
 179
 180         assert!(search_graph.is_empty());
 181         result
 182     }
 183 }
 184
 185 struct EvalCtxt<'a, 'tcx> {
 186     infcx: &'a InferCtxt<'tcx>,
 187     var_values: CanonicalVarValues<'tcx>,
 188
 189     search_graph: &'a mut search_graph::SearchGraph<'tcx>,
 190 }
 191
 192 impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
 193     fn tcx(&self) -> TyCtxt<'tcx> {
 194         self.infcx.tcx
 195     }
 196
 197     #[instrument(level = "debug", skip(tcx, search_graph), ret)]
 198     fn evaluate_canonical_goal(
 199         tcx: TyCtxt<'tcx>,
 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) {
 204             Ok(()) => {}
 205             // Our goal is already on the stack, eager return.
 206             Err(response) => return response,
 207         }
 208
 209         // We may have to repeatedly recompute the goal in case of coinductive cycles,
 210         // check out the `cache` module for more information.
 211         //
 212         // FIXME: Similar to `evaluate_all`, this has to check for overflow.
 213         loop {
 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);
 218
 219             // FIXME: `Response` should be `Copy`
 220             if search_graph.try_finalize_goal(tcx, canonical_goal, result.clone()) {
 221                 return result;
 222             }
 223         }
 224     }
 225
 226     fn make_canonical_response(&self, certainty: Certainty) -> QueryResult<'tcx> {
 227         let external_constraints = take_external_constraints(self.infcx)?;
 228
 229         Ok(self.infcx.canonicalize_response(Response {
 230             var_values: self.var_values.clone(),
 231             external_constraints,
 232             certainty,
 233         }))
 234     }
 235
 236     /// Recursively evaluates `goal`, returning whether any inference vars have
 237     /// been constrained and the certainty of the result.
 238     fn evaluate_goal(
 239         &mut self,
 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)?;
 246         Ok((
 247             !canonical_response.value.var_values.is_identity(),
 248             instantiate_canonical_query_response(self.infcx, &orig_values, canonical_response),
 249         ))
 250     }
 251
 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() {
 256             match kind {
 257                 ty::PredicateKind::Clause(ty::Clause::Trait(predicate)) => {
 258                     self.compute_trait_goal(Goal { param_env, predicate })
 259                 }
 260                 ty::PredicateKind::Clause(ty::Clause::Projection(predicate)) => {
 261                     self.compute_projection_goal(Goal { param_env, predicate })
 262                 }
 263                 ty::PredicateKind::Clause(ty::Clause::TypeOutlives(predicate)) => {
 264                     self.compute_type_outlives_goal(Goal { param_env, predicate })
 265                 }
 266                 ty::PredicateKind::Clause(ty::Clause::RegionOutlives(predicate)) => {
 267                     self.compute_region_outlives_goal(Goal { param_env, predicate })
 268                 }
 269                 ty::PredicateKind::Subtype(predicate) => {
 270                     self.compute_subtype_goal(Goal { param_env, predicate })
 271                 }
 272                 ty::PredicateKind::Coerce(predicate) => {
 273                     self.compute_coerce_goal(Goal { param_env, predicate })
 274                 }
 275                 ty::PredicateKind::ClosureKind(def_id, substs, kind) => self
 276                     .compute_closure_kind_goal(Goal {
 277                         param_env,
 278                         predicate: (def_id, substs, kind),
 279                     }),
 280                 ty::PredicateKind::ObjectSafe(trait_def_id) => {
 281                     self.compute_object_safe_goal(trait_def_id)
 282                 }
 283                 ty::PredicateKind::WellFormed(arg) => {
 284                     self.compute_well_formed_goal(Goal { param_env, predicate: arg })
 285                 }
 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)
 290                 }
 291                 ty::PredicateKind::TypeWellFormedFromEnv(..) => {
 292                     bug!("TypeWellFormedFromEnv is only used for Chalk")
 293                 }
 294             }
 295         } else {
 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)
 300         }
 301     }
 302
 303     fn compute_type_outlives_goal(
 304         &mut self,
 305         _goal: Goal<'tcx, TypeOutlivesPredicate<'tcx>>,
 306     ) -> QueryResult<'tcx> {
 307         self.make_canonical_response(Certainty::Yes)
 308     }
 309
 310     fn compute_region_outlives_goal(
 311         &mut self,
 312         _goal: Goal<'tcx, RegionOutlivesPredicate<'tcx>>,
 313     ) -> QueryResult<'tcx> {
 314         self.make_canonical_response(Certainty::Yes)
 315     }
 316
 317     fn compute_coerce_goal(
 318         &mut self,
 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,
 325                 a: goal.predicate.a,
 326                 b: goal.predicate.b,
 327             },
 328         })
 329     }
 330
 331     fn compute_subtype_goal(
 332         &mut self,
 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)
 339         } else {
 340             let InferOk { value: (), obligations } = self
 341                 .infcx
 342                 .at(&ObligationCause::dummy(), goal.param_env)
 343                 .sub(goal.predicate.a, goal.predicate.b)?;
 344             self.evaluate_all_and_make_canonical_response(
 345                 obligations.into_iter().map(|pred| pred.into()).collect(),
 346             )
 347         }
 348     }
 349
 350     fn compute_closure_kind_goal(
 351         &mut self,
 352         goal: Goal<'tcx, (DefId, ty::SubstsRef<'tcx>, ty::ClosureKind)>,
 353     ) -> QueryResult<'tcx> {
 354         let (_, substs, expected_kind) = goal.predicate;
 355         let found_kind = substs.as_closure().kind_ty().to_opt_closure_kind();
 356
 357         let Some(found_kind) = found_kind else {
 358             return self.make_canonical_response(Certainty::AMBIGUOUS);
 359         };
 360         if found_kind.extends(expected_kind) {
 361             self.make_canonical_response(Certainty::Yes)
 362         } else {
 363             Err(NoSolution)
 364         }
 365     }
 366
 367     fn compute_object_safe_goal(&mut self, trait_def_id: DefId) -> QueryResult<'tcx> {
 368         if self.tcx().is_object_safe(trait_def_id) {
 369             self.make_canonical_response(Certainty::Yes)
 370         } else {
 371             Err(NoSolution)
 372         }
 373     }
 374
 375     fn compute_well_formed_goal(
 376         &mut self,
 377         goal: Goal<'tcx, ty::GenericArg<'tcx>>,
 378     ) -> QueryResult<'tcx> {
 379         match crate::traits::wf::unnormalized_obligations(
 380             self.infcx,
 381             goal.param_env,
 382             goal.predicate,
 383         ) {
 384             Some(obligations) => self.evaluate_all_and_make_canonical_response(
 385                 obligations.into_iter().map(|o| o.into()).collect(),
 386             ),
 387             None => self.make_canonical_response(Certainty::AMBIGUOUS),
 388         }
 389     }
 390 }
 391
 392 impl<'tcx> EvalCtxt<'_, 'tcx> {
 393     // Recursively evaluates a list of goals to completion, returning the certainty
 394     // of all of the goals.
 395     fn evaluate_all(
 396         &mut self,
 397         mut goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
 398     ) -> Result<Certainty, NoSolution> {
 399         let mut new_goals = Vec::new();
 400         self.repeat_while_none(|this| {
 401             let mut has_changed = Err(Certainty::Yes);
 402             for goal in goals.drain(..) {
 403                 let (changed, certainty) = match this.evaluate_goal(goal) {
 404                     Ok(result) => result,
 405                     Err(NoSolution) => return Some(Err(NoSolution)),
 406                 };
 407
 408                 if changed {
 409                     has_changed = Ok(());
 410                 }
 411
 412                 match certainty {
 413                     Certainty::Yes => {}
 414                     Certainty::Maybe(_) => {
 415                         new_goals.push(goal);
 416                         has_changed = has_changed.map_err(|c| c.unify_and(certainty));
 417                     }
 418                 }
 419             }
 420
 421             match has_changed {
 422                 Ok(()) => {
 423                     mem::swap(&mut new_goals, &mut goals);
 424                     None
 425                 }
 426                 Err(certainty) => Some(Ok(certainty)),
 427             }
 428         })
 429     }
 430
 431     // Recursively evaluates a list of goals to completion, making a query response.
 432     //
 433     // This is just a convenient way of calling [`EvalCtxt::evaluate_all`],
 434     // then [`EvalCtxt::make_canonical_response`].
 435     fn evaluate_all_and_make_canonical_response(
 436         &mut self,
 437         goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
 438     ) -> QueryResult<'tcx> {
 439         self.evaluate_all(goals).and_then(|certainty| self.make_canonical_response(certainty))
 440     }
 441 }
 442
 443 #[instrument(level = "debug", skip(infcx), ret)]
 444 fn take_external_constraints<'tcx>(
 445     infcx: &InferCtxt<'tcx>,
 446 ) -> Result<ExternalConstraints<'tcx>, NoSolution> {
 447     let region_obligations = infcx.take_registered_region_obligations();
 448     let opaque_types = infcx.take_opaque_types_for_query_response();
 449     Ok(ExternalConstraints {
 450         // FIXME: Now that's definitely wrong :)
 451         //
 452         // Should also do the leak check here I think
 453         regions: drop(region_obligations),
 454         opaque_types,
 455     })
 456 }
 457
 458 fn instantiate_canonical_query_response<'tcx>(
 459     infcx: &InferCtxt<'tcx>,
 460     original_values: &OriginalQueryValues<'tcx>,
 461     response: CanonicalResponse<'tcx>,
 462 ) -> Certainty {
 463     let Ok(InferOk { value, obligations }) = infcx
 464         .instantiate_query_response_and_region_obligations(
 465             &ObligationCause::dummy(),
 466             ty::ParamEnv::empty(),
 467             original_values,
 468             &response.unchecked_map(|resp| QueryResponse {
 469                 var_values: resp.var_values,
 470                 region_constraints: QueryRegionConstraints::default(),
 471                 certainty: match resp.certainty {
 472                     Certainty::Yes => OldCertainty::Proven,
 473                     Certainty::Maybe(_) => OldCertainty::Ambiguous,
 474                 },
 475                 opaque_types: resp.external_constraints.opaque_types,
 476                 value: resp.certainty,
 477             }),
 478         ) else { bug!(); };
 479     assert!(obligations.is_empty());
 480     value
 481 }
 482
 483 pub(super) fn response_no_constraints<'tcx>(
 484     tcx: TyCtxt<'tcx>,
 485     goal: Canonical<'tcx, impl Sized>,
 486     certainty: Certainty,
 487 ) -> QueryResult<'tcx> {
 488     let var_values = goal
 489         .variables
 490         .iter()
 491         .enumerate()
 492         .map(|(i, info)| match info.kind {
 493             CanonicalVarKind::Ty(_) | CanonicalVarKind::PlaceholderTy(_) => {
 494                 tcx.mk_ty(ty::Bound(ty::INNERMOST, ty::BoundVar::from_usize(i).into())).into()
 495             }
 496             CanonicalVarKind::Region(_) | CanonicalVarKind::PlaceholderRegion(_) => {
 497                 let br = ty::BoundRegion {
 498                     var: ty::BoundVar::from_usize(i),
 499                     kind: ty::BrAnon(i as u32, None),
 500                 };
 501                 tcx.mk_region(ty::ReLateBound(ty::INNERMOST, br)).into()
 502             }
 503             CanonicalVarKind::Const(_, ty) | CanonicalVarKind::PlaceholderConst(_, ty) => tcx
 504                 .mk_const(ty::ConstKind::Bound(ty::INNERMOST, ty::BoundVar::from_usize(i)), ty)
 505                 .into(),
 506         })
 507         .collect();
 508
 509     Ok(Canonical {
 510         max_universe: goal.max_universe,
 511         variables: goal.variables,
 512         value: Response {
 513             var_values: CanonicalVarValues { var_values },
 514             external_constraints: Default::default(),
 515             certainty,
 516         },
 517     })
 518 }