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: uses of `infcx.at` need to enable deferred projection equality once that's implemented.
  17
  18 use std::mem;
  19
  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,
  31 };
  32 use rustc_span::DUMMY_SP;
  33
  34 use crate::traits::ObligationCause;
  35
  36 mod assembly;
  37 mod fulfill;
  38 mod infcx_ext;
  39 mod project_goals;
  40 mod search_graph;
  41 mod trait_goals;
  42
  43 pub use fulfill::FulfillmentCtxt;
  44
  45 /// A goal is a statement, i.e. `predicate`, we want to prove
  46 /// given some assumptions, i.e. `param_env`.
  47 ///
  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>,
  53     predicate: P,
  54 }
  55
  56 impl<'tcx, P> Goal<'tcx, P> {
  57     pub fn new(
  58         tcx: TyCtxt<'tcx>,
  59         param_env: ty::ParamEnv<'tcx>,
  60         predicate: impl ToPredicate<'tcx, P>,
  61     ) -> Goal<'tcx, P> {
  62         Goal { param_env, predicate: predicate.to_predicate(tcx) }
  63     }
  64
  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) }
  68     }
  69 }
  70
  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 }
  74     }
  75 }
  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,
  82 }
  83
  84 #[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, TypeFoldable, TypeVisitable)]
  85 pub enum Certainty {
  86     Yes,
  87     Maybe(MaybeCause),
  88 }
  89
  90 impl Certainty {
  91     pub const AMBIGUOUS: Certainty = Certainty::Maybe(MaybeCause::Ambiguity);
  92
  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 {
  96         match (self, other) {
  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)
 102             }
 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)
 108             }
 109         }
 110     }
 111 }
 112
 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.
 119     Ambiguity,
 120     /// We gave up due to an overflow, most often by hitting the recursion limit.
 121     Overflow,
 122 }
 123
 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.
 127 ///
 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>;
 133
 134 pub trait InferCtxtEvalExt<'tcx> {
 135     /// Evaluates a goal from **outside** of the trait solver.
 136     ///
 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(
 140         &self,
 141         goal: Goal<'tcx, ty::Predicate<'tcx>>,
 142     ) -> Result<(bool, Certainty), NoSolution>;
 143 }
 144
 145 impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
 146     fn evaluate_root_goal(
 147         &self,
 148         goal: Goal<'tcx, ty::Predicate<'tcx>>,
 149     ) -> Result<(bool, Certainty), NoSolution> {
 150         let mut search_graph = search_graph::SearchGraph::new(self.tcx);
 151
 152         let result = EvalCtxt {
 153             search_graph: &mut search_graph,
 154             infcx: self,
 155             var_values: CanonicalVarValues::dummy(),
 156             in_projection_eq_hack: false,
 157         }
 158         .evaluate_goal(goal);
 159
 160         assert!(search_graph.is_empty());
 161         result
 162     }
 163 }
 164
 165 struct EvalCtxt<'a, 'tcx> {
 166     infcx: &'a InferCtxt<'tcx>,
 167     var_values: CanonicalVarValues<'tcx>,
 168
 169     search_graph: &'a mut search_graph::SearchGraph<'tcx>,
 170
 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,
 174 }
 175
 176 impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
 177     fn tcx(&self) -> TyCtxt<'tcx> {
 178         self.infcx.tcx
 179     }
 180
 181     /// The entry point of the solver.
 182     ///
 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.
 186     ///
 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
 189     /// outside of it.
 190     #[instrument(level = "debug", skip(tcx, search_graph), ret)]
 191     fn evaluate_canonical_goal(
 192         tcx: TyCtxt<'tcx>,
 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) {
 197             Ok(()) => {}
 198             // Our goal is already on the stack, eager return.
 199             Err(response) => return response,
 200         }
 201
 202         // We may have to repeatedly recompute the goal in case of coinductive cycles,
 203         // check out the `cache` module for more information.
 204         //
 205         // FIXME: Similar to `evaluate_all`, this has to check for overflow.
 206         loop {
 207             let (ref infcx, goal, var_values) =
 208                 tcx.infer_ctxt().build_with_canonical(DUMMY_SP, &canonical_goal);
 209             let mut ecx =
 210                 EvalCtxt { infcx, var_values, search_graph, in_projection_eq_hack: false };
 211             let result = ecx.compute_goal(goal);
 212
 213             if search_graph.try_finalize_goal(tcx, canonical_goal, result) {
 214                 return result;
 215             }
 216         }
 217     }
 218
 219     fn make_canonical_response(&self, certainty: Certainty) -> QueryResult<'tcx> {
 220         let external_constraints = compute_external_query_constraints(self.infcx)?;
 221
 222         Ok(self.infcx.canonicalize_response(Response {
 223             var_values: self.var_values,
 224             external_constraints,
 225             certainty,
 226         }))
 227     }
 228
 229     /// Recursively evaluates `goal`, returning whether any inference vars have
 230     /// been constrained and the certainty of the result.
 231     fn evaluate_goal(
 232         &mut self,
 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)?;
 239
 240         let has_changed = !canonical_response.value.var_values.is_identity();
 241         let certainty =
 242             instantiate_canonical_query_response(self.infcx, &orig_values, canonical_response);
 243
 244         // Check that rerunning this query with its inference constraints applied
 245         // doesn't result in new inference constraints and has the same result.
 246         //
 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
 250         // solver cycle.
 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);
 258         }
 259
 260         Ok((has_changed, certainty))
 261     }
 262
 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() {
 267             match kind {
 268                 ty::PredicateKind::Clause(ty::Clause::Trait(predicate)) => {
 269                     self.compute_trait_goal(Goal { param_env, predicate })
 270                 }
 271                 ty::PredicateKind::Clause(ty::Clause::Projection(predicate)) => {
 272                     self.compute_projection_goal(Goal { param_env, predicate })
 273                 }
 274                 ty::PredicateKind::Clause(ty::Clause::TypeOutlives(predicate)) => {
 275                     self.compute_type_outlives_goal(Goal { param_env, predicate })
 276                 }
 277                 ty::PredicateKind::Clause(ty::Clause::RegionOutlives(predicate)) => {
 278                     self.compute_region_outlives_goal(Goal { param_env, predicate })
 279                 }
 280                 ty::PredicateKind::Subtype(predicate) => {
 281                     self.compute_subtype_goal(Goal { param_env, predicate })
 282                 }
 283                 ty::PredicateKind::Coerce(predicate) => {
 284                     self.compute_coerce_goal(Goal { param_env, predicate })
 285                 }
 286                 ty::PredicateKind::ClosureKind(def_id, substs, kind) => self
 287                     .compute_closure_kind_goal(Goal {
 288                         param_env,
 289                         predicate: (def_id, substs, kind),
 290                     }),
 291                 ty::PredicateKind::ObjectSafe(trait_def_id) => {
 292                     self.compute_object_safe_goal(trait_def_id)
 293                 }
 294                 ty::PredicateKind::WellFormed(arg) => {
 295                     self.compute_well_formed_goal(Goal { param_env, predicate: arg })
 296                 }
 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)
 301                 }
 302                 ty::PredicateKind::TypeWellFormedFromEnv(..) => {
 303                     bug!("TypeWellFormedFromEnv is only used for Chalk")
 304                 }
 305             }
 306         } else {
 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)
 311         }
 312     }
 313
 314     fn compute_type_outlives_goal(
 315         &mut self,
 316         _goal: Goal<'tcx, TypeOutlivesPredicate<'tcx>>,
 317     ) -> QueryResult<'tcx> {
 318         self.make_canonical_response(Certainty::Yes)
 319     }
 320
 321     fn compute_region_outlives_goal(
 322         &mut self,
 323         _goal: Goal<'tcx, RegionOutlivesPredicate<'tcx>>,
 324     ) -> QueryResult<'tcx> {
 325         self.make_canonical_response(Certainty::Yes)
 326     }
 327
 328     fn compute_coerce_goal(
 329         &mut self,
 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,
 336                 a: goal.predicate.a,
 337                 b: goal.predicate.b,
 338             },
 339         })
 340     }
 341
 342     fn compute_subtype_goal(
 343         &mut self,
 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)
 350         } else {
 351             let InferOk { value: (), obligations } = self
 352                 .infcx
 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(),
 357             )
 358         }
 359     }
 360
 361     fn compute_closure_kind_goal(
 362         &mut self,
 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();
 367
 368         let Some(found_kind) = found_kind else {
 369             return self.make_canonical_response(Certainty::AMBIGUOUS);
 370         };
 371         if found_kind.extends(expected_kind) {
 372             self.make_canonical_response(Certainty::Yes)
 373         } else {
 374             Err(NoSolution)
 375         }
 376     }
 377
 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)
 381         } else {
 382             Err(NoSolution)
 383         }
 384     }
 385
 386     fn compute_well_formed_goal(
 387         &mut self,
 388         goal: Goal<'tcx, ty::GenericArg<'tcx>>,
 389     ) -> QueryResult<'tcx> {
 390         match crate::traits::wf::unnormalized_obligations(
 391             self.infcx,
 392             goal.param_env,
 393             goal.predicate,
 394         ) {
 395             Some(obligations) => self.evaluate_all_and_make_canonical_response(
 396                 obligations.into_iter().map(|o| o.into()).collect(),
 397             ),
 398             None => self.make_canonical_response(Certainty::AMBIGUOUS),
 399         }
 400     }
 401 }
 402
 403 impl<'tcx> EvalCtxt<'_, 'tcx> {
 404     // Recursively evaluates a list of goals to completion, returning the certainty
 405     // of all of the goals.
 406     fn evaluate_all(
 407         &mut self,
 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)),
 417                 };
 418
 419                 if changed {
 420                     has_changed = Ok(());
 421                 }
 422
 423                 match certainty {
 424                     Certainty::Yes => {}
 425                     Certainty::Maybe(_) => {
 426                         new_goals.push(goal);
 427                         has_changed = has_changed.map_err(|c| c.unify_and(certainty));
 428                     }
 429                 }
 430             }
 431
 432             match has_changed {
 433                 Ok(()) => {
 434                     mem::swap(&mut new_goals, &mut goals);
 435                     None
 436                 }
 437                 Err(certainty) => Some(Ok(certainty)),
 438             }
 439         })
 440     }
 441
 442     // Recursively evaluates a list of goals to completion, making a query response.
 443     //
 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(
 447         &mut self,
 448         goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
 449     ) -> QueryResult<'tcx> {
 450         self.evaluate_all(goals).and_then(|certainty| self.make_canonical_response(certainty))
 451     }
 452 }
 453
 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 :)
 462         //
 463         // Should also do the leak check here I think
 464         regions: drop(region_obligations),
 465         opaque_types,
 466     }))
 467 }
 468
 469 fn instantiate_canonical_query_response<'tcx>(
 470     infcx: &InferCtxt<'tcx>,
 471     original_values: &OriginalQueryValues<'tcx>,
 472     response: CanonicalResponse<'tcx>,
 473 ) -> Certainty {
 474     let Ok(InferOk { value, obligations }) = infcx
 475         .instantiate_query_response_and_region_obligations(
 476             &ObligationCause::dummy(),
 477             ty::ParamEnv::empty(),
 478             original_values,
 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,
 485                 },
 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,
 491             }),
 492         ) else { bug!(); };
 493     assert!(obligations.is_empty());
 494     value
 495 }
 496
 497 pub(super) fn response_no_constraints<'tcx>(
 498     tcx: TyCtxt<'tcx>,
 499     goal: Canonical<'tcx, impl Sized>,
 500     certainty: Certainty,
 501 ) -> QueryResult<'tcx> {
 502     Ok(Canonical {
 503         max_universe: goal.max_universe,
 504         variables: goal.variables,
 505         value: Response {
 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()),
 511             certainty,
 512         },
 513     })
 514 }