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_infer::infer::canonical::{Canonical, CanonicalVarKind, CanonicalVarValues};
  23 use rustc_infer::infer::canonical::{OriginalQueryValues, QueryRegionConstraints, QueryResponse};
  24 use rustc_infer::infer::{InferCtxt, InferOk, TyCtxtInferExt};
  25 use rustc_infer::traits::query::NoSolution;
  26 use rustc_infer::traits::Obligation;
  27 use rustc_middle::infer::canonical::Certainty as OldCertainty;
  28 use rustc_middle::ty::{self, Ty, TyCtxt};
  29 use rustc_middle::ty::{RegionOutlivesPredicate, ToPredicate, TypeOutlivesPredicate};
  30 use rustc_span::DUMMY_SP;
  31
  32 use crate::traits::ObligationCause;
  33
  34 mod assembly;
  35 mod fulfill;
  36 mod infcx_ext;
  37 mod project_goals;
  38 mod search_graph;
  39 mod trait_goals;
  40
  41 pub use fulfill::FulfillmentCtxt;
  42
  43 /// A goal is a statement, i.e. `predicate`, we want to prove
  44 /// given some assumptions, i.e. `param_env`.
  45 ///
  46 /// Most of the time the `param_env` contains the `where`-bounds of the function
  47 /// we're currently typechecking while the `predicate` is some trait bound.
  48 #[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, TypeFoldable, TypeVisitable)]
  49 pub struct Goal<'tcx, P> {
  50     param_env: ty::ParamEnv<'tcx>,
  51     predicate: P,
  52 }
  53
  54 impl<'tcx, P> Goal<'tcx, P> {
  55     pub fn new(
  56         tcx: TyCtxt<'tcx>,
  57         param_env: ty::ParamEnv<'tcx>,
  58         predicate: impl ToPredicate<'tcx, P>,
  59     ) -> Goal<'tcx, P> {
  60         Goal { param_env, predicate: predicate.to_predicate(tcx) }
  61     }
  62
  63     /// Updates the goal to one with a different `predicate` but the same `param_env`.
  64     fn with<Q>(self, tcx: TyCtxt<'tcx>, predicate: impl ToPredicate<'tcx, Q>) -> Goal<'tcx, Q> {
  65         Goal { param_env: self.param_env, predicate: predicate.to_predicate(tcx) }
  66     }
  67 }
  68
  69 impl<'tcx, P> From<Obligation<'tcx, P>> for Goal<'tcx, P> {
  70     fn from(obligation: Obligation<'tcx, P>) -> Goal<'tcx, P> {
  71         Goal { param_env: obligation.param_env, predicate: obligation.predicate }
  72     }
  73 }
  74
  75 #[derive(Debug, PartialEq, Eq, Clone, Hash, TypeFoldable, TypeVisitable)]
  76 pub struct Response<'tcx> {
  77     pub var_values: CanonicalVarValues<'tcx>,
  78     /// Additional constraints returned by this query.
  79     pub external_constraints: ExternalConstraints<'tcx>,
  80     pub certainty: Certainty,
  81 }
  82
  83 #[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, TypeFoldable, TypeVisitable)]
  84 pub enum Certainty {
  85     Yes,
  86     Maybe(MaybeCause),
  87 }
  88
  89 impl Certainty {
  90     /// When proving multiple goals using **AND**, e.g. nested obligations for an impl,
  91     /// use this function to unify the certainty of these goals
  92     pub fn unify_and(self, other: Certainty) -> Certainty {
  93         match (self, other) {
  94             (Certainty::Yes, Certainty::Yes) => Certainty::Yes,
  95             (Certainty::Yes, Certainty::Maybe(_)) => other,
  96             (Certainty::Maybe(_), Certainty::Yes) => self,
  97             (Certainty::Maybe(MaybeCause::Overflow), Certainty::Maybe(MaybeCause::Overflow)) => {
  98                 Certainty::Maybe(MaybeCause::Overflow)
  99             }
 100             // If at least one of the goals is ambiguous, hide the overflow as the ambiguous goal
 101             // may still result in failure.
 102             (Certainty::Maybe(MaybeCause::Ambiguity), Certainty::Maybe(_))
 103             | (Certainty::Maybe(_), Certainty::Maybe(MaybeCause::Ambiguity)) => {
 104                 Certainty::Maybe(MaybeCause::Ambiguity)
 105             }
 106         }
 107     }
 108 }
 109
 110 /// Why we failed to evaluate a goal.
 111 #[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, TypeFoldable, TypeVisitable)]
 112 pub enum MaybeCause {
 113     /// We failed due to ambiguity. This ambiguity can either
 114     /// be a true ambiguity, i.e. there are multiple different answers,
 115     /// or we hit a case where we just don't bother, e.g. `?x: Trait` goals.
 116     Ambiguity,
 117     /// We gave up due to an overflow, most often by hitting the recursion limit.
 118     Overflow,
 119 }
 120
 121 /// Additional constraints returned on success.
 122 #[derive(Debug, PartialEq, Eq, Clone, Hash, TypeFoldable, TypeVisitable, Default)]
 123 pub struct ExternalConstraints<'tcx> {
 124     // FIXME: implement this.
 125     regions: (),
 126     opaque_types: Vec<(Ty<'tcx>, Ty<'tcx>)>,
 127 }
 128
 129 type CanonicalGoal<'tcx, T = ty::Predicate<'tcx>> = Canonical<'tcx, Goal<'tcx, T>>;
 130 type CanonicalResponse<'tcx> = Canonical<'tcx, Response<'tcx>>;
 131 /// The result of evaluating a canonical query.
 132 ///
 133 /// FIXME: We use a different type than the existing canonical queries. This is because
 134 /// we need to add a `Certainty` for `overflow` and may want to restructure this code without
 135 /// having to worry about changes to currently used code. Once we've made progress on this
 136 /// solver, merge the two responses again.
 137 pub type QueryResult<'tcx> = Result<CanonicalResponse<'tcx>, NoSolution>;
 138
 139 pub trait TyCtxtExt<'tcx> {
 140     fn evaluate_goal(self, goal: CanonicalGoal<'tcx>) -> QueryResult<'tcx>;
 141 }
 142
 143 impl<'tcx> TyCtxtExt<'tcx> for TyCtxt<'tcx> {
 144     fn evaluate_goal(self, goal: CanonicalGoal<'tcx>) -> QueryResult<'tcx> {
 145         let mut search_graph = search_graph::SearchGraph::new(self);
 146         EvalCtxt::evaluate_canonical_goal(self, &mut search_graph, goal)
 147     }
 148 }
 149
 150 struct EvalCtxt<'a, 'tcx> {
 151     infcx: &'a InferCtxt<'tcx>,
 152     var_values: CanonicalVarValues<'tcx>,
 153
 154     search_graph: &'a mut search_graph::SearchGraph<'tcx>,
 155 }
 156
 157 impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
 158     fn tcx(&self) -> TyCtxt<'tcx> {
 159         self.infcx.tcx
 160     }
 161
 162     /// Creates a new evaluation context outside of the trait solver.
 163     ///
 164     /// With this solver making a canonical response doesn't make much sense.
 165     /// The `search_graph` for this solver has to be completely empty.
 166     fn new_outside_solver(
 167         infcx: &'a InferCtxt<'tcx>,
 168         search_graph: &'a mut search_graph::SearchGraph<'tcx>,
 169     ) -> EvalCtxt<'a, 'tcx> {
 170         assert!(search_graph.is_empty());
 171         EvalCtxt { infcx, var_values: CanonicalVarValues::dummy(), search_graph }
 172     }
 173
 174     #[instrument(level = "debug", skip(tcx, search_graph), ret)]
 175     fn evaluate_canonical_goal(
 176         tcx: TyCtxt<'tcx>,
 177         search_graph: &'a mut search_graph::SearchGraph<'tcx>,
 178         canonical_goal: CanonicalGoal<'tcx>,
 179     ) -> QueryResult<'tcx> {
 180         match search_graph.try_push_stack(tcx, canonical_goal) {
 181             Ok(()) => {}
 182             // Our goal is already on the stack, eager return.
 183             Err(response) => return response,
 184         }
 185
 186         // We may have to repeatedly recompute the goal in case of coinductive cycles,
 187         // check out the `cache` module for more information.
 188         //
 189         // FIXME: Similar to `evaluate_all`, this has to check for overflow.
 190         loop {
 191             let (ref infcx, goal, var_values) =
 192                 tcx.infer_ctxt().build_with_canonical(DUMMY_SP, &canonical_goal);
 193             let mut ecx = EvalCtxt { infcx, var_values, search_graph };
 194             let result = ecx.compute_goal(goal);
 195
 196             // FIXME: `Response` should be `Copy`
 197             if search_graph.try_finalize_goal(tcx, canonical_goal, result.clone()) {
 198                 return result;
 199             }
 200         }
 201     }
 202
 203     fn make_canonical_response(&self, certainty: Certainty) -> QueryResult<'tcx> {
 204         let external_constraints = take_external_constraints(self.infcx)?;
 205
 206         Ok(self.infcx.canonicalize_response(Response {
 207             var_values: self.var_values.clone(),
 208             external_constraints,
 209             certainty,
 210         }))
 211     }
 212
 213     /// Recursively evaluates `goal`, returning whether any inference vars have
 214     /// been constrained and the certainty of the result.
 215     fn evaluate_goal(
 216         &mut self,
 217         goal: Goal<'tcx, ty::Predicate<'tcx>>,
 218     ) -> Result<(bool, Certainty), NoSolution> {
 219         let mut orig_values = OriginalQueryValues::default();
 220         let canonical_goal = self.infcx.canonicalize_query(goal, &mut orig_values);
 221         let canonical_response =
 222             EvalCtxt::evaluate_canonical_goal(self.tcx(), self.search_graph, canonical_goal)?;
 223         Ok((
 224             !canonical_response.value.var_values.is_identity(),
 225             instantiate_canonical_query_response(self.infcx, &orig_values, canonical_response),
 226         ))
 227     }
 228
 229     fn compute_goal(&mut self, goal: Goal<'tcx, ty::Predicate<'tcx>>) -> QueryResult<'tcx> {
 230         let Goal { param_env, predicate } = goal;
 231         let kind = predicate.kind();
 232         if let Some(kind) = kind.no_bound_vars() {
 233             match kind {
 234                 ty::PredicateKind::Clause(ty::Clause::Trait(predicate)) => {
 235                     self.compute_trait_goal(Goal { param_env, predicate })
 236                 }
 237                 ty::PredicateKind::Clause(ty::Clause::Projection(predicate)) => {
 238                     self.compute_projection_goal(Goal { param_env, predicate })
 239                 }
 240                 ty::PredicateKind::Clause(ty::Clause::TypeOutlives(predicate)) => {
 241                     self.compute_type_outlives_goal(Goal { param_env, predicate })
 242                 }
 243                 ty::PredicateKind::Clause(ty::Clause::RegionOutlives(predicate)) => {
 244                     self.compute_region_outlives_goal(Goal { param_env, predicate })
 245                 }
 246                 // FIXME: implement these predicates :)
 247                 ty::PredicateKind::WellFormed(_)
 248                 | ty::PredicateKind::ObjectSafe(_)
 249                 | ty::PredicateKind::ClosureKind(_, _, _)
 250                 | ty::PredicateKind::Subtype(_)
 251                 | ty::PredicateKind::Coerce(_)
 252                 | ty::PredicateKind::ConstEvaluatable(_)
 253                 | ty::PredicateKind::ConstEquate(_, _)
 254                 | ty::PredicateKind::TypeWellFormedFromEnv(_)
 255                 | ty::PredicateKind::Ambiguous => self.make_canonical_response(Certainty::Yes),
 256             }
 257         } else {
 258             let kind = self.infcx.replace_bound_vars_with_placeholders(kind);
 259             let goal = goal.with(self.tcx(), ty::Binder::dummy(kind));
 260             let (_, certainty) = self.evaluate_goal(goal)?;
 261             self.make_canonical_response(certainty)
 262         }
 263     }
 264
 265     fn compute_type_outlives_goal(
 266         &mut self,
 267         _goal: Goal<'tcx, TypeOutlivesPredicate<'tcx>>,
 268     ) -> QueryResult<'tcx> {
 269         self.make_canonical_response(Certainty::Yes)
 270     }
 271
 272     fn compute_region_outlives_goal(
 273         &mut self,
 274         _goal: Goal<'tcx, RegionOutlivesPredicate<'tcx>>,
 275     ) -> QueryResult<'tcx> {
 276         self.make_canonical_response(Certainty::Yes)
 277     }
 278 }
 279
 280 impl<'tcx> EvalCtxt<'_, 'tcx> {
 281     fn evaluate_all(
 282         &mut self,
 283         mut goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
 284     ) -> Result<Certainty, NoSolution> {
 285         let mut new_goals = Vec::new();
 286         self.repeat_while_none(|this| {
 287             let mut has_changed = Err(Certainty::Yes);
 288             for goal in goals.drain(..) {
 289                 let (changed, certainty) = match this.evaluate_goal(goal) {
 290                     Ok(result) => result,
 291                     Err(NoSolution) => return Some(Err(NoSolution)),
 292                 };
 293
 294                 if changed {
 295                     has_changed = Ok(());
 296                 }
 297
 298                 match certainty {
 299                     Certainty::Yes => {}
 300                     Certainty::Maybe(_) => {
 301                         new_goals.push(goal);
 302                         has_changed = has_changed.map_err(|c| c.unify_and(certainty));
 303                     }
 304                 }
 305             }
 306
 307             match has_changed {
 308                 Ok(()) => {
 309                     mem::swap(&mut new_goals, &mut goals);
 310                     None
 311                 }
 312                 Err(certainty) => Some(Ok(certainty)),
 313             }
 314         })
 315     }
 316 }
 317
 318 #[instrument(level = "debug", skip(infcx), ret)]
 319 fn take_external_constraints<'tcx>(
 320     infcx: &InferCtxt<'tcx>,
 321 ) -> Result<ExternalConstraints<'tcx>, NoSolution> {
 322     let region_obligations = infcx.take_registered_region_obligations();
 323     let opaque_types = infcx.take_opaque_types_for_query_response();
 324     Ok(ExternalConstraints {
 325         // FIXME: Now that's definitely wrong :)
 326         //
 327         // Should also do the leak check here I think
 328         regions: drop(region_obligations),
 329         opaque_types,
 330     })
 331 }
 332
 333 fn instantiate_canonical_query_response<'tcx>(
 334     infcx: &InferCtxt<'tcx>,
 335     original_values: &OriginalQueryValues<'tcx>,
 336     response: CanonicalResponse<'tcx>,
 337 ) -> Certainty {
 338     let Ok(InferOk { value, obligations }) = infcx
 339         .instantiate_query_response_and_region_obligations(
 340             &ObligationCause::dummy(),
 341             ty::ParamEnv::empty(),
 342             original_values,
 343             &response.unchecked_map(|resp| QueryResponse {
 344                 var_values: resp.var_values,
 345                 region_constraints: QueryRegionConstraints::default(),
 346                 certainty: match resp.certainty {
 347                     Certainty::Yes => OldCertainty::Proven,
 348                     Certainty::Maybe(_) => OldCertainty::Ambiguous,
 349                 },
 350                 opaque_types: resp.external_constraints.opaque_types,
 351                 value: resp.certainty,
 352             }),
 353         ) else { bug!(); };
 354     assert!(obligations.is_empty());
 355     value
 356 }
 357
 358 pub(super) fn response_no_constraints<'tcx>(
 359     tcx: TyCtxt<'tcx>,
 360     goal: Canonical<'tcx, impl Sized>,
 361     certainty: Certainty,
 362 ) -> QueryResult<'tcx> {
 363     let var_values = goal
 364         .variables
 365         .iter()
 366         .enumerate()
 367         .map(|(i, info)| match info.kind {
 368             CanonicalVarKind::Ty(_) | CanonicalVarKind::PlaceholderTy(_) => {
 369                 tcx.mk_ty(ty::Bound(ty::INNERMOST, ty::BoundVar::from_usize(i).into())).into()
 370             }
 371             CanonicalVarKind::Region(_) | CanonicalVarKind::PlaceholderRegion(_) => {
 372                 let br = ty::BoundRegion {
 373                     var: ty::BoundVar::from_usize(i),
 374                     kind: ty::BrAnon(i as u32, None),
 375                 };
 376                 tcx.mk_region(ty::ReLateBound(ty::INNERMOST, br)).into()
 377             }
 378             CanonicalVarKind::Const(_, ty) | CanonicalVarKind::PlaceholderConst(_, ty) => tcx
 379                 .mk_const(ty::ConstKind::Bound(ty::INNERMOST, ty::BoundVar::from_usize(i)), ty)
 380                 .into(),
 381         })
 382         .collect();
 383
 384     Ok(Canonical {
 385         max_universe: goal.max_universe,
 386         variables: goal.variables,
 387         value: Response {
 388             var_values: CanonicalVarValues { var_values },
 389             external_constraints: Default::default(),
 390             certainty,
 391         },
 392     })
 393 }