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::{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::infer::canonical::{Canonical, CanonicalVarValues};
  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 use self::cache::response_no_constraints;
  35 use self::infcx_ext::InferCtxtExt;
  36
  37 mod assembly;
  38 mod cache;
  39 mod fulfill;
  40 mod infcx_ext;
  41 mod overflow;
  42 mod project_goals;
  43 mod trait_goals;
  44
  45 pub use fulfill::FulfillmentCtxt;
  46
  47 /// A goal is a statement, i.e. `predicate`, we want to prove
  48 /// given some assumptions, i.e. `param_env`.
  49 ///
  50 /// Most of the time the `param_env` contains the `where`-bounds of the function
  51 /// we're currently typechecking while the `predicate` is some trait bound.
  52 #[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, TypeFoldable, TypeVisitable)]
  53 pub struct Goal<'tcx, P> {
  54     param_env: ty::ParamEnv<'tcx>,
  55     predicate: P,
  56 }
  57
  58 impl<'tcx, P> Goal<'tcx, P> {
  59     pub fn new(
  60         tcx: TyCtxt<'tcx>,
  61         param_env: ty::ParamEnv<'tcx>,
  62         predicate: impl ToPredicate<'tcx, P>,
  63     ) -> Goal<'tcx, P> {
  64         Goal { param_env, predicate: predicate.to_predicate(tcx) }
  65     }
  66
  67     /// Updates the goal to one with a different `predicate` but the same `param_env`.
  68     fn with<Q>(self, tcx: TyCtxt<'tcx>, predicate: impl ToPredicate<'tcx, Q>) -> Goal<'tcx, Q> {
  69         Goal { param_env: self.param_env, predicate: predicate.to_predicate(tcx) }
  70     }
  71 }
  72
  73 impl<'tcx, P> From<Obligation<'tcx, P>> for Goal<'tcx, P> {
  74     fn from(obligation: Obligation<'tcx, P>) -> Goal<'tcx, P> {
  75         Goal { param_env: obligation.param_env, predicate: obligation.predicate }
  76     }
  77 }
  78
  79 #[derive(Debug, PartialEq, Eq, Clone, Hash, TypeFoldable, TypeVisitable)]
  80 pub struct Response<'tcx> {
  81     pub var_values: CanonicalVarValues<'tcx>,
  82     /// Additional constraints returned by this query.
  83     pub external_constraints: ExternalConstraints<'tcx>,
  84     pub certainty: Certainty,
  85 }
  86
  87 #[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, TypeFoldable, TypeVisitable)]
  88 pub enum Certainty {
  89     Yes,
  90     Maybe(MaybeCause),
  91 }
  92
  93 impl Certainty {
  94     /// When proving multiple goals using **AND**, e.g. nested obligations for an impl,
  95     /// use this function to unify the certainty of these goals
  96     pub fn unify_and(self, other: Certainty) -> Certainty {
  97         match (self, other) {
  98             (Certainty::Yes, Certainty::Yes) => Certainty::Yes,
  99             (Certainty::Yes, Certainty::Maybe(_)) => other,
 100             (Certainty::Maybe(_), Certainty::Yes) => self,
 101             (Certainty::Maybe(MaybeCause::Overflow), Certainty::Maybe(MaybeCause::Overflow)) => {
 102                 Certainty::Maybe(MaybeCause::Overflow)
 103             }
 104             // If at least one of the goals is ambiguous, hide the overflow as the ambiguous goal
 105             // may still result in failure.
 106             (Certainty::Maybe(MaybeCause::Ambiguity), Certainty::Maybe(_))
 107             | (Certainty::Maybe(_), Certainty::Maybe(MaybeCause::Ambiguity)) => {
 108                 Certainty::Maybe(MaybeCause::Ambiguity)
 109             }
 110         }
 111     }
 112 }
 113
 114 /// Why we failed to evaluate a goal.
 115 #[derive(Debug, PartialEq, Eq, Clone, Copy, Hash, TypeFoldable, TypeVisitable)]
 116 pub enum MaybeCause {
 117     /// We failed due to ambiguity. This ambiguity can either
 118     /// be a true ambiguity, i.e. there are multiple different answers,
 119     /// or we hit a case where we just don't bother, e.g. `?x: Trait` goals.
 120     Ambiguity,
 121     /// We gave up due to an overflow, most often by hitting the recursion limit.
 122     Overflow,
 123 }
 124
 125 /// Additional constraints returned on success.
 126 #[derive(Debug, PartialEq, Eq, Clone, Hash, TypeFoldable, TypeVisitable, Default)]
 127 pub struct ExternalConstraints<'tcx> {
 128     // FIXME: implement this.
 129     regions: (),
 130     opaque_types: Vec<(Ty<'tcx>, Ty<'tcx>)>,
 131 }
 132
 133 type CanonicalGoal<'tcx, T = ty::Predicate<'tcx>> = Canonical<'tcx, Goal<'tcx, T>>;
 134 type CanonicalResponse<'tcx> = Canonical<'tcx, Response<'tcx>>;
 135 /// The result of evaluating a canonical query.
 136 ///
 137 /// FIXME: We use a different type than the existing canonical queries. This is because
 138 /// we need to add a `Certainty` for `overflow` and may want to restructure this code without
 139 /// having to worry about changes to currently used code. Once we've made progress on this
 140 /// solver, merge the two responses again.
 141 pub type QueryResult<'tcx> = Result<CanonicalResponse<'tcx>, NoSolution>;
 142
 143 pub trait TyCtxtExt<'tcx> {
 144     fn evaluate_goal(self, goal: CanonicalGoal<'tcx>) -> QueryResult<'tcx>;
 145 }
 146
 147 impl<'tcx> TyCtxtExt<'tcx> for TyCtxt<'tcx> {
 148     fn evaluate_goal(self, goal: CanonicalGoal<'tcx>) -> QueryResult<'tcx> {
 149         let mut cx = EvalCtxt::new(self);
 150         cx.evaluate_canonical_goal(goal)
 151     }
 152 }
 153
 154 struct EvalCtxt<'tcx> {
 155     tcx: TyCtxt<'tcx>,
 156
 157     provisional_cache: cache::ProvisionalCache<'tcx>,
 158     overflow_data: overflow::OverflowData,
 159 }
 160
 161 impl<'tcx> EvalCtxt<'tcx> {
 162     fn new(tcx: TyCtxt<'tcx>) -> EvalCtxt<'tcx> {
 163         EvalCtxt {
 164             tcx,
 165             provisional_cache: cache::ProvisionalCache::empty(),
 166             overflow_data: overflow::OverflowData::new(tcx),
 167         }
 168     }
 169
 170     /// Recursively evaluates `goal`, returning whether any inference vars have
 171     /// been constrained and the certainty of the result.
 172     fn evaluate_goal(
 173         &mut self,
 174         infcx: &InferCtxt<'tcx>,
 175         goal: Goal<'tcx, ty::Predicate<'tcx>>,
 176     ) -> Result<(bool, Certainty), NoSolution> {
 177         let mut orig_values = OriginalQueryValues::default();
 178         let canonical_goal = infcx.canonicalize_query(goal, &mut orig_values);
 179         let canonical_response = self.evaluate_canonical_goal(canonical_goal)?;
 180         Ok((
 181             true, // FIXME: check whether `var_values` are an identity substitution.
 182             instantiate_canonical_query_response(infcx, &orig_values, canonical_response),
 183         ))
 184     }
 185
 186     fn evaluate_canonical_goal(&mut self, goal: CanonicalGoal<'tcx>) -> QueryResult<'tcx> {
 187         match self.try_push_stack(goal) {
 188             Ok(()) => {}
 189             // Our goal is already on the stack, eager return.
 190             Err(response) => return response,
 191         }
 192
 193         // We may have to repeatedly recompute the goal in case of coinductive cycles,
 194         // check out the `cache` module for more information.
 195         //
 196         // FIXME: Similar to `evaluate_all`, this has to check for overflow.
 197         loop {
 198             let result = self.compute_goal(goal);
 199
 200             // FIXME: `Response` should be `Copy`
 201             if self.try_finalize_goal(goal, result.clone()) {
 202                 return result;
 203             }
 204         }
 205     }
 206
 207     fn compute_goal(&mut self, canonical_goal: CanonicalGoal<'tcx>) -> QueryResult<'tcx> {
 208         // WARNING: We're looking at a canonical value without instantiating it here.
 209         //
 210         // We have to be incredibly careful to not change the order of bound variables or
 211         // remove any. As we go from `Goal<'tcx, Predicate>` to `Goal` with the variants
 212         // of `PredicateKind` this is the case and it is and faster than instantiating and
 213         // recanonicalizing.
 214         let Goal { param_env, predicate } = canonical_goal.value;
 215
 216         if let Some(kind) = predicate.kind().no_bound_vars_ignoring_escaping(self.tcx) {
 217             match kind {
 218                 ty::PredicateKind::Clause(ty::Clause::Trait(predicate)) => self.compute_trait_goal(
 219                     canonical_goal.unchecked_rebind(Goal { param_env, predicate }),
 220                 ),
 221                 ty::PredicateKind::Clause(ty::Clause::Projection(predicate)) => self
 222                     .compute_projection_goal(
 223                         canonical_goal.unchecked_rebind(Goal { param_env, predicate }),
 224                     ),
 225                 ty::PredicateKind::Clause(ty::Clause::TypeOutlives(predicate)) => self
 226                     .compute_type_outlives_goal(
 227                         canonical_goal.unchecked_rebind(Goal { param_env, predicate }),
 228                     ),
 229                 ty::PredicateKind::Clause(ty::Clause::RegionOutlives(predicate)) => self
 230                     .compute_region_outlives_goal(
 231                         canonical_goal.unchecked_rebind(Goal { param_env, predicate }),
 232                     ),
 233                 // FIXME: implement these predicates :)
 234                 ty::PredicateKind::WellFormed(_)
 235                 | ty::PredicateKind::ObjectSafe(_)
 236                 | ty::PredicateKind::ClosureKind(_, _, _)
 237                 | ty::PredicateKind::Subtype(_)
 238                 | ty::PredicateKind::Coerce(_)
 239                 | ty::PredicateKind::ConstEvaluatable(_)
 240                 | ty::PredicateKind::ConstEquate(_, _)
 241                 | ty::PredicateKind::TypeWellFormedFromEnv(_)
 242                 | ty::PredicateKind::Ambiguous => {
 243                     // FIXME
 244                     response_no_constraints(self.tcx, canonical_goal, Certainty::Yes)
 245                 }
 246             }
 247         } else {
 248             let (infcx, goal, var_values) =
 249                 self.tcx.infer_ctxt().build_with_canonical(DUMMY_SP, &canonical_goal);
 250             let kind = infcx.replace_bound_vars_with_placeholders(goal.predicate.kind());
 251             let goal = goal.with(self.tcx, ty::Binder::dummy(kind));
 252             let (_, certainty) = self.evaluate_goal(&infcx, goal)?;
 253             infcx.make_canonical_response(var_values, certainty)
 254         }
 255     }
 256
 257     fn compute_type_outlives_goal(
 258         &mut self,
 259         goal: CanonicalGoal<'tcx, TypeOutlivesPredicate<'tcx>>,
 260     ) -> QueryResult<'tcx> {
 261         // FIXME
 262         response_no_constraints(self.tcx, goal, Certainty::Yes)
 263     }
 264
 265     fn compute_region_outlives_goal(
 266         &mut self,
 267         goal: CanonicalGoal<'tcx, RegionOutlivesPredicate<'tcx>>,
 268     ) -> QueryResult<'tcx> {
 269         // FIXME
 270         response_no_constraints(self.tcx, goal, Certainty::Yes)
 271     }
 272 }
 273
 274 impl<'tcx> EvalCtxt<'tcx> {
 275     fn evaluate_all(
 276         &mut self,
 277         infcx: &InferCtxt<'tcx>,
 278         mut goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
 279     ) -> Result<Certainty, NoSolution> {
 280         let mut new_goals = Vec::new();
 281         self.repeat_while_none(|this| {
 282             let mut has_changed = Err(Certainty::Yes);
 283             for goal in goals.drain(..) {
 284                 let (changed, certainty) = match this.evaluate_goal(infcx, goal) {
 285                     Ok(result) => result,
 286                     Err(NoSolution) => return Some(Err(NoSolution)),
 287                 };
 288
 289                 if changed {
 290                     has_changed = Ok(());
 291                 }
 292
 293                 match certainty {
 294                     Certainty::Yes => {}
 295                     Certainty::Maybe(_) => {
 296                         new_goals.push(goal);
 297                         has_changed = has_changed.map_err(|c| c.unify_and(certainty));
 298                     }
 299                 }
 300             }
 301
 302             match has_changed {
 303                 Ok(()) => {
 304                     mem::swap(&mut new_goals, &mut goals);
 305                     None
 306                 }
 307                 Err(certainty) => Some(Ok(certainty)),
 308             }
 309         })
 310     }
 311 }
 312
 313 fn instantiate_canonical_query_response<'tcx>(
 314     infcx: &InferCtxt<'tcx>,
 315     original_values: &OriginalQueryValues<'tcx>,
 316     response: CanonicalResponse<'tcx>,
 317 ) -> Certainty {
 318     let Ok(InferOk { value, obligations }) = infcx
 319         .instantiate_query_response_and_region_obligations(
 320             &ObligationCause::dummy(),
 321             ty::ParamEnv::empty(),
 322             original_values,
 323             &response.unchecked_map(|resp| QueryResponse {
 324                 var_values: resp.var_values,
 325                 region_constraints: QueryRegionConstraints::default(),
 326                 certainty: match resp.certainty {
 327                     Certainty::Yes => OldCertainty::Proven,
 328                     Certainty::Maybe(_) => OldCertainty::Ambiguous,
 329                 },
 330                 opaque_types: resp.external_constraints.opaque_types,
 331                 value: resp.certainty,
 332             }),
 333         ) else { bug!(); };
 334     assert!(obligations.is_empty());
 335     value
 336 }