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;
  23 use rustc_infer::infer::{InferCtxt, TyCtxtInferExt};
  24 use rustc_infer::traits::query::NoSolution;
  25 use rustc_infer::traits::Obligation;
  26 use rustc_middle::infer::canonical::{Canonical, CanonicalVarValues};
  27 use rustc_middle::ty::{self, Ty, TyCtxt};
  28 use rustc_middle::ty::{RegionOutlivesPredicate, ToPredicate, TypeOutlivesPredicate};
  29 use rustc_span::DUMMY_SP;
  30
  31 use self::infcx_ext::InferCtxtExt;
  32
  33 mod assembly;
  34 mod cache;
  35 mod fulfill;
  36 mod infcx_ext;
  37 mod overflow;
  38 mod project_goals;
  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)]
 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 cx = EvalCtxt::new(self);
 146         cx.evaluate_canonical_goal(goal)
 147     }
 148 }
 149
 150 struct EvalCtxt<'tcx> {
 151     tcx: TyCtxt<'tcx>,
 152
 153     provisional_cache: cache::ProvisionalCache<'tcx>,
 154     overflow_data: overflow::OverflowData,
 155 }
 156
 157 impl<'tcx> EvalCtxt<'tcx> {
 158     fn new(tcx: TyCtxt<'tcx>) -> EvalCtxt<'tcx> {
 159         EvalCtxt {
 160             tcx,
 161             provisional_cache: cache::ProvisionalCache::empty(),
 162             overflow_data: overflow::OverflowData::new(tcx),
 163         }
 164     }
 165
 166     /// Recursively evaluates `goal`, returning whether any inference vars have
 167     /// been constrained and the certainty of the result.
 168     fn evaluate_goal(
 169         &mut self,
 170         infcx: &InferCtxt<'tcx>,
 171         goal: Goal<'tcx, ty::Predicate<'tcx>>,
 172     ) -> Result<(bool, Certainty), NoSolution> {
 173         let mut orig_values = OriginalQueryValues::default();
 174         let canonical_goal = infcx.canonicalize_query(goal, &mut orig_values);
 175         let canonical_response = self.evaluate_canonical_goal(canonical_goal)?;
 176         Ok((
 177             true, // FIXME: check whether `var_values` are an identity substitution.
 178             fixme_instantiate_canonical_query_response(infcx, &orig_values, canonical_response),
 179         ))
 180     }
 181
 182     fn evaluate_canonical_goal(&mut self, goal: CanonicalGoal<'tcx>) -> QueryResult<'tcx> {
 183         match self.try_push_stack(goal) {
 184             Ok(()) => {}
 185             // Our goal is already on the stack, eager return.
 186             Err(response) => return response,
 187         }
 188
 189         // We may have to repeatedly recompute the goal in case of coinductive cycles,
 190         // check out the `cache` module for more information.
 191         //
 192         // FIXME: Similar to `evaluate_all`, this has to check for overflow.
 193         loop {
 194             let result = self.compute_goal(goal);
 195
 196             // FIXME: `Response` should be `Copy`
 197             if self.try_finalize_goal(goal, result.clone()) {
 198                 return result;
 199             }
 200         }
 201     }
 202
 203     fn compute_goal(&mut self, canonical_goal: CanonicalGoal<'tcx>) -> QueryResult<'tcx> {
 204         // WARNING: We're looking at a canonical value without instantiating it here.
 205         //
 206         // We have to be incredibly careful to not change the order of bound variables or
 207         // remove any. As we go from `Goal<'tcx, Predicate>` to `Goal` with the variants
 208         // of `PredicateKind` this is the case and it is and faster than instantiating and
 209         // recanonicalizing.
 210         let Goal { param_env, predicate } = canonical_goal.value;
 211         if let Some(kind) = predicate.kind().no_bound_vars() {
 212             match kind {
 213                 ty::PredicateKind::Clause(ty::Clause::Trait(predicate)) => self.compute_trait_goal(
 214                     canonical_goal.unchecked_rebind(Goal { param_env, predicate }),
 215                 ),
 216                 ty::PredicateKind::Clause(ty::Clause::Projection(predicate)) => self
 217                     .compute_projection_goal(
 218                         canonical_goal.unchecked_rebind(Goal { param_env, predicate }),
 219                     ),
 220                 ty::PredicateKind::Clause(ty::Clause::TypeOutlives(predicate)) => self
 221                     .compute_type_outlives_goal(
 222                         canonical_goal.unchecked_rebind(Goal { param_env, predicate }),
 223                     ),
 224                 ty::PredicateKind::Clause(ty::Clause::RegionOutlives(predicate)) => self
 225                     .compute_region_outlives_goal(
 226                         canonical_goal.unchecked_rebind(Goal { param_env, predicate }),
 227                     ),
 228                 // FIXME: implement these predicates :)
 229                 ty::PredicateKind::WellFormed(_)
 230                 | ty::PredicateKind::ObjectSafe(_)
 231                 | ty::PredicateKind::ClosureKind(_, _, _)
 232                 | ty::PredicateKind::Subtype(_)
 233                 | ty::PredicateKind::Coerce(_)
 234                 | ty::PredicateKind::ConstEvaluatable(_)
 235                 | ty::PredicateKind::ConstEquate(_, _)
 236                 | ty::PredicateKind::TypeWellFormedFromEnv(_)
 237                 | ty::PredicateKind::Ambiguous => unimplemented!(),
 238             }
 239         } else {
 240             let (infcx, goal, var_values) =
 241                 self.tcx.infer_ctxt().build_with_canonical(DUMMY_SP, &canonical_goal);
 242             let kind = infcx.replace_bound_vars_with_placeholders(goal.predicate.kind());
 243             let goal = goal.with(self.tcx, ty::Binder::dummy(kind));
 244             let (_, certainty) = self.evaluate_goal(&infcx, goal)?;
 245             infcx.make_canonical_response(var_values, certainty)
 246         }
 247     }
 248
 249     fn compute_type_outlives_goal(
 250         &mut self,
 251         _goal: CanonicalGoal<'tcx, TypeOutlivesPredicate<'tcx>>,
 252     ) -> QueryResult<'tcx> {
 253         todo!()
 254     }
 255
 256     fn compute_region_outlives_goal(
 257         &mut self,
 258         _goal: CanonicalGoal<'tcx, RegionOutlivesPredicate<'tcx>>,
 259     ) -> QueryResult<'tcx> {
 260         todo!()
 261     }
 262 }
 263
 264 impl<'tcx> EvalCtxt<'tcx> {
 265     fn evaluate_all(
 266         &mut self,
 267         infcx: &InferCtxt<'tcx>,
 268         mut goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
 269     ) -> Result<Certainty, NoSolution> {
 270         let mut new_goals = Vec::new();
 271         self.repeat_while_none(|this| {
 272             let mut has_changed = Err(Certainty::Yes);
 273             for goal in goals.drain(..) {
 274                 let (changed, certainty) = match this.evaluate_goal(infcx, goal) {
 275                     Ok(result) => result,
 276                     Err(NoSolution) => return Some(Err(NoSolution)),
 277                 };
 278
 279                 if changed {
 280                     has_changed = Ok(());
 281                 }
 282
 283                 match certainty {
 284                     Certainty::Yes => {}
 285                     Certainty::Maybe(_) => {
 286                         new_goals.push(goal);
 287                         has_changed = has_changed.map_err(|c| c.unify_and(certainty));
 288                     }
 289                 }
 290             }
 291
 292             match has_changed {
 293                 Ok(()) => {
 294                     mem::swap(&mut new_goals, &mut goals);
 295                     None
 296                 }
 297                 Err(certainty) => Some(Ok(certainty)),
 298             }
 299         })
 300     }
 301 }
 302
 303 fn fixme_instantiate_canonical_query_response<'tcx>(
 304     _: &InferCtxt<'tcx>,
 305     _: &OriginalQueryValues<'tcx>,
 306     _: CanonicalResponse<'tcx>,
 307 ) -> Certainty {
 308     unimplemented!()
 309 }