src/librustc_traits/chalk_context/mod.rs

   1 mod program_clauses;
   2 mod resolvent_ops;
   3 mod unify;
   4
   5 use chalk_engine::fallible::Fallible;
   6 use chalk_engine::forest::Forest;
   7 use chalk_engine::{context, hh::HhGoal, DelayedLiteral, ExClause, Literal};
   8 use rustc::infer::canonical::{
   9     Canonical, CanonicalVarValues, Certainty, OriginalQueryValues, QueryRegionConstraints,
  10     QueryResponse,
  11 };
  12 use rustc::infer::{InferCtxt, LateBoundRegionConversionTime};
  13 use rustc::traits::{
  14     self, ChalkCanonicalGoal, ChalkContextLift, Clause, DomainGoal, Environment, ExClauseFold,
  15     Goal, GoalKind, InEnvironment, QuantifierKind,
  16 };
  17 use rustc::ty::fold::{TypeFoldable, TypeFolder, TypeVisitor};
  18 use rustc::ty::query::Providers;
  19 use rustc::ty::subst::{GenericArg, GenericArgKind};
  20 use rustc::ty::{self, TyCtxt};
  21 use rustc_macros::{Lift, TypeFoldable};
  22 use rustc_span::DUMMY_SP;
  23
  24 use std::fmt::{self, Debug};
  25 use std::marker::PhantomData;
  26
  27 use self::unify::*;
  28
  29 #[derive(Copy, Clone, Debug)]
  30 crate struct ChalkArenas<'tcx> {
  31     _phantom: PhantomData<&'tcx ()>,
  32 }
  33
  34 #[derive(Copy, Clone)]
  35 crate struct ChalkContext<'tcx> {
  36     _arenas: ChalkArenas<'tcx>,
  37     tcx: TyCtxt<'tcx>,
  38 }
  39
  40 #[derive(Copy, Clone)]
  41 crate struct ChalkInferenceContext<'cx, 'tcx> {
  42     infcx: &'cx InferCtxt<'cx, 'tcx>,
  43 }
  44
  45 #[derive(Copy, Clone, Debug)]
  46 crate struct UniverseMap;
  47
  48 crate type RegionConstraint<'tcx> = ty::OutlivesPredicate<GenericArg<'tcx>, ty::Region<'tcx>>;
  49
  50 #[derive(Clone, Debug, PartialEq, Eq, Hash, TypeFoldable, Lift)]
  51 crate struct ConstrainedSubst<'tcx> {
  52     subst: CanonicalVarValues<'tcx>,
  53     constraints: Vec<RegionConstraint<'tcx>>,
  54 }
  55
  56 impl context::Context for ChalkArenas<'tcx> {
  57     type CanonicalExClause = Canonical<'tcx, ChalkExClause<'tcx>>;
  58
  59     type CanonicalGoalInEnvironment = Canonical<'tcx, InEnvironment<'tcx, Goal<'tcx>>>;
  60
  61     // u-canonicalization not yet implemented
  62     type UCanonicalGoalInEnvironment = Canonical<'tcx, InEnvironment<'tcx, Goal<'tcx>>>;
  63
  64     type CanonicalConstrainedSubst = Canonical<'tcx, ConstrainedSubst<'tcx>>;
  65
  66     // u-canonicalization not yet implemented
  67     type UniverseMap = UniverseMap;
  68
  69     type Solution = Canonical<'tcx, QueryResponse<'tcx, ()>>;
  70
  71     type InferenceNormalizedSubst = CanonicalVarValues<'tcx>;
  72
  73     type GoalInEnvironment = InEnvironment<'tcx, Goal<'tcx>>;
  74
  75     type RegionConstraint = RegionConstraint<'tcx>;
  76
  77     type Substitution = CanonicalVarValues<'tcx>;
  78
  79     type Environment = Environment<'tcx>;
  80
  81     type Goal = Goal<'tcx>;
  82
  83     type DomainGoal = DomainGoal<'tcx>;
  84
  85     type BindersGoal = ty::Binder<Goal<'tcx>>;
  86
  87     type Parameter = GenericArg<'tcx>;
  88
  89     type ProgramClause = Clause<'tcx>;
  90
  91     type ProgramClauses = Vec<Clause<'tcx>>;
  92
  93     type UnificationResult = UnificationResult<'tcx>;
  94
  95     type Variance = ty::Variance;
  96
  97     fn goal_in_environment(
  98         env: &Environment<'tcx>,
  99         goal: Goal<'tcx>,
 100     ) -> InEnvironment<'tcx, Goal<'tcx>> {
 101         env.with(goal)
 102     }
 103 }
 104
 105 impl context::AggregateOps<ChalkArenas<'tcx>> for ChalkContext<'tcx> {
 106     fn make_solution(
 107         &self,
 108         root_goal: &Canonical<'tcx, InEnvironment<'tcx, Goal<'tcx>>>,
 109         mut simplified_answers: impl context::AnswerStream<ChalkArenas<'tcx>>,
 110     ) -> Option<Canonical<'tcx, QueryResponse<'tcx, ()>>> {
 111         use chalk_engine::SimplifiedAnswer;
 112
 113         debug!("make_solution(root_goal = {:?})", root_goal);
 114
 115         if simplified_answers.peek_answer().is_none() {
 116             return None;
 117         }
 118
 119         let SimplifiedAnswer { subst: constrained_subst, ambiguous } =
 120             simplified_answers.next_answer().unwrap();
 121
 122         debug!("make_solution: ambiguous flag = {}", ambiguous);
 123
 124         let ambiguous = simplified_answers.peek_answer().is_some() || ambiguous;
 125
 126         let solution = constrained_subst.unchecked_map(|cs| match ambiguous {
 127             true => QueryResponse {
 128                 var_values: cs.subst.make_identity(self.tcx),
 129                 region_constraints: QueryRegionConstraints::default(),
 130                 certainty: Certainty::Ambiguous,
 131                 value: (),
 132             },
 133
 134             false => QueryResponse {
 135                 var_values: cs.subst,
 136                 region_constraints: QueryRegionConstraints::default(),
 137
 138                 // FIXME: restore this later once we get better at handling regions
 139                 // region_constraints: cs.constraints
 140                 //     .into_iter()
 141                 //     .map(|c| ty::Binder::bind(c))
 142                 //     .collect(),
 143                 certainty: Certainty::Proven,
 144                 value: (),
 145             },
 146         });
 147
 148         debug!("make_solution: solution = {:?}", solution);
 149
 150         Some(solution)
 151     }
 152 }
 153
 154 impl context::ContextOps<ChalkArenas<'tcx>> for ChalkContext<'tcx> {
 155     /// Returns `true` if this is a coinductive goal: basically proving that an auto trait
 156     /// is implemented or proving that a trait reference is well-formed.
 157     fn is_coinductive(&self, goal: &Canonical<'tcx, InEnvironment<'tcx, Goal<'tcx>>>) -> bool {
 158         use rustc::traits::{WellFormed, WhereClause};
 159
 160         let mut goal = goal.value.goal;
 161         loop {
 162             match goal {
 163                 GoalKind::DomainGoal(domain_goal) => match domain_goal {
 164                     DomainGoal::WellFormed(WellFormed::Trait(..)) => return true,
 165                     DomainGoal::Holds(WhereClause::Implemented(trait_predicate)) => {
 166                         return self.tcx.trait_is_auto(trait_predicate.def_id());
 167                     }
 168                     _ => return false,
 169                 },
 170
 171                 GoalKind::Quantified(_, bound_goal) => goal = *bound_goal.skip_binder(),
 172                 _ => return false,
 173             }
 174         }
 175     }
 176
 177     /// Creates an inference table for processing a new goal and instantiate that goal
 178     /// in that context, returning "all the pieces".
 179     ///
 180     /// More specifically: given a u-canonical goal `arg`, creates a
 181     /// new inference table `T` and populates it with the universes
 182     /// found in `arg`. Then, creates a substitution `S` that maps
 183     /// each bound variable in `arg` to a fresh inference variable
 184     /// from T. Returns:
 185     ///
 186     /// - the table `T`,
 187     /// - the substitution `S`,
 188     /// - the environment and goal found by substitution `S` into `arg`.
 189     fn instantiate_ucanonical_goal<R>(
 190         &self,
 191         arg: &Canonical<'tcx, InEnvironment<'tcx, Goal<'tcx>>>,
 192         op: impl context::WithInstantiatedUCanonicalGoal<ChalkArenas<'tcx>, Output = R>,
 193     ) -> R {
 194         self.tcx.infer_ctxt().enter_with_canonical(DUMMY_SP, arg, |ref infcx, arg, subst| {
 195             let chalk_infcx = &mut ChalkInferenceContext { infcx };
 196             op.with(chalk_infcx, subst, arg.environment, arg.goal)
 197         })
 198     }
 199
 200     fn instantiate_ex_clause<R>(
 201         &self,
 202         _num_universes: usize,
 203         arg: &Canonical<'tcx, ChalkExClause<'tcx>>,
 204         op: impl context::WithInstantiatedExClause<ChalkArenas<'tcx>, Output = R>,
 205     ) -> R {
 206         self.tcx.infer_ctxt().enter_with_canonical(DUMMY_SP, &arg.upcast(), |ref infcx, arg, _| {
 207             let chalk_infcx = &mut ChalkInferenceContext { infcx };
 208             op.with(chalk_infcx, arg)
 209         })
 210     }
 211
 212     /// Returns `true` if this solution has no region constraints.
 213     fn empty_constraints(ccs: &Canonical<'tcx, ConstrainedSubst<'tcx>>) -> bool {
 214         ccs.value.constraints.is_empty()
 215     }
 216
 217     fn inference_normalized_subst_from_ex_clause(
 218         canon_ex_clause: &'a Canonical<'tcx, ChalkExClause<'tcx>>,
 219     ) -> &'a CanonicalVarValues<'tcx> {
 220         &canon_ex_clause.value.subst
 221     }
 222
 223     fn inference_normalized_subst_from_subst(
 224         canon_subst: &'a Canonical<'tcx, ConstrainedSubst<'tcx>>,
 225     ) -> &'a CanonicalVarValues<'tcx> {
 226         &canon_subst.value.subst
 227     }
 228
 229     fn canonical(
 230         u_canon: &'a Canonical<'tcx, InEnvironment<'tcx, Goal<'tcx>>>,
 231     ) -> &'a Canonical<'tcx, InEnvironment<'tcx, Goal<'tcx>>> {
 232         u_canon
 233     }
 234
 235     fn is_trivial_substitution(
 236         u_canon: &Canonical<'tcx, InEnvironment<'tcx, Goal<'tcx>>>,
 237         canonical_subst: &Canonical<'tcx, ConstrainedSubst<'tcx>>,
 238     ) -> bool {
 239         let subst = &canonical_subst.value.subst;
 240         assert_eq!(u_canon.variables.len(), subst.var_values.len());
 241         subst.var_values.iter_enumerated().all(|(cvar, kind)| match kind.unpack() {
 242             GenericArgKind::Lifetime(r) => match r {
 243                 &ty::ReLateBound(debruijn, br) => {
 244                     debug_assert_eq!(debruijn, ty::INNERMOST);
 245                     cvar == br.assert_bound_var()
 246                 }
 247                 _ => false,
 248             },
 249             GenericArgKind::Type(ty) => match ty.kind {
 250                 ty::Bound(debruijn, bound_ty) => {
 251                     debug_assert_eq!(debruijn, ty::INNERMOST);
 252                     cvar == bound_ty.var
 253                 }
 254                 _ => false,
 255             },
 256             GenericArgKind::Const(ct) => match ct.val {
 257                 ty::ConstKind::Bound(debruijn, bound_ct) => {
 258                     debug_assert_eq!(debruijn, ty::INNERMOST);
 259                     cvar == bound_ct
 260                 }
 261                 _ => false,
 262             },
 263         })
 264     }
 265
 266     fn num_universes(canon: &Canonical<'tcx, InEnvironment<'tcx, Goal<'tcx>>>) -> usize {
 267         canon.max_universe.index() + 1
 268     }
 269
 270     /// Convert a goal G *from* the canonical universes *into* our
 271     /// local universes. This will yield a goal G' that is the same
 272     /// but for the universes of universally quantified names.
 273     fn map_goal_from_canonical(
 274         _map: &UniverseMap,
 275         value: &Canonical<'tcx, InEnvironment<'tcx, Goal<'tcx>>>,
 276     ) -> Canonical<'tcx, InEnvironment<'tcx, Goal<'tcx>>> {
 277         *value // FIXME universe maps not implemented yet
 278     }
 279
 280     fn map_subst_from_canonical(
 281         _map: &UniverseMap,
 282         value: &Canonical<'tcx, ConstrainedSubst<'tcx>>,
 283     ) -> Canonical<'tcx, ConstrainedSubst<'tcx>> {
 284         value.clone() // FIXME universe maps not implemented yet
 285     }
 286 }
 287
 288 impl context::InferenceTable<ChalkArenas<'tcx>, ChalkArenas<'tcx>>
 289     for ChalkInferenceContext<'cx, 'tcx>
 290 {
 291     fn into_goal(&self, domain_goal: DomainGoal<'tcx>) -> Goal<'tcx> {
 292         self.infcx.tcx.mk_goal(GoalKind::DomainGoal(domain_goal))
 293     }
 294
 295     fn cannot_prove(&self) -> Goal<'tcx> {
 296         self.infcx.tcx.mk_goal(GoalKind::CannotProve)
 297     }
 298
 299     fn into_hh_goal(&mut self, goal: Goal<'tcx>) -> ChalkHhGoal<'tcx> {
 300         match *goal {
 301             GoalKind::Implies(hypotheses, goal) => {
 302                 HhGoal::Implies(hypotheses.iter().cloned().collect(), goal)
 303             }
 304             GoalKind::And(left, right) => HhGoal::And(left, right),
 305             GoalKind::Not(subgoal) => HhGoal::Not(subgoal),
 306             GoalKind::DomainGoal(d) => HhGoal::DomainGoal(d),
 307             GoalKind::Quantified(QuantifierKind::Universal, binder) => HhGoal::ForAll(binder),
 308             GoalKind::Quantified(QuantifierKind::Existential, binder) => HhGoal::Exists(binder),
 309             GoalKind::Subtype(a, b) => HhGoal::Unify(ty::Variance::Covariant, a.into(), b.into()),
 310             GoalKind::CannotProve => HhGoal::CannotProve,
 311         }
 312     }
 313
 314     fn add_clauses(
 315         &mut self,
 316         env: &Environment<'tcx>,
 317         clauses: Vec<Clause<'tcx>>,
 318     ) -> Environment<'tcx> {
 319         Environment {
 320             clauses: self
 321                 .infcx
 322                 .tcx
 323                 .mk_clauses(env.clauses.iter().cloned().chain(clauses.into_iter())),
 324         }
 325     }
 326 }
 327
 328 impl context::TruncateOps<ChalkArenas<'tcx>, ChalkArenas<'tcx>>
 329     for ChalkInferenceContext<'cx, 'tcx>
 330 {
 331     fn truncate_goal(
 332         &mut self,
 333         _subgoal: &InEnvironment<'tcx, Goal<'tcx>>,
 334     ) -> Option<InEnvironment<'tcx, Goal<'tcx>>> {
 335         None // FIXME we should truncate at some point!
 336     }
 337
 338     fn truncate_answer(
 339         &mut self,
 340         _subst: &CanonicalVarValues<'tcx>,
 341     ) -> Option<CanonicalVarValues<'tcx>> {
 342         None // FIXME we should truncate at some point!
 343     }
 344 }
 345
 346 impl context::UnificationOps<ChalkArenas<'tcx>, ChalkArenas<'tcx>>
 347     for ChalkInferenceContext<'cx, 'tcx>
 348 {
 349     fn program_clauses(
 350         &self,
 351         environment: &Environment<'tcx>,
 352         goal: &DomainGoal<'tcx>,
 353     ) -> Vec<Clause<'tcx>> {
 354         self.program_clauses_impl(environment, goal)
 355     }
 356
 357     fn instantiate_binders_universally(&mut self, arg: &ty::Binder<Goal<'tcx>>) -> Goal<'tcx> {
 358         self.infcx.replace_bound_vars_with_placeholders(arg).0
 359     }
 360
 361     fn instantiate_binders_existentially(&mut self, arg: &ty::Binder<Goal<'tcx>>) -> Goal<'tcx> {
 362         self.infcx
 363             .replace_bound_vars_with_fresh_vars(
 364                 DUMMY_SP,
 365                 LateBoundRegionConversionTime::HigherRankedType,
 366                 arg,
 367             )
 368             .0
 369     }
 370
 371     fn debug_ex_clause(&mut self, value: &'v ChalkExClause<'tcx>) -> Box<dyn Debug + 'v> {
 372         let string = format!("{:?}", self.infcx.resolve_vars_if_possible(value));
 373         Box::new(string)
 374     }
 375
 376     fn canonicalize_goal(
 377         &mut self,
 378         value: &InEnvironment<'tcx, Goal<'tcx>>,
 379     ) -> Canonical<'tcx, InEnvironment<'tcx, Goal<'tcx>>> {
 380         let mut _orig_values = OriginalQueryValues::default();
 381         self.infcx.canonicalize_query(value, &mut _orig_values)
 382     }
 383
 384     fn canonicalize_ex_clause(
 385         &mut self,
 386         value: &ChalkExClause<'tcx>,
 387     ) -> Canonical<'tcx, ChalkExClause<'tcx>> {
 388         self.infcx.canonicalize_response(value)
 389     }
 390
 391     fn canonicalize_constrained_subst(
 392         &mut self,
 393         subst: CanonicalVarValues<'tcx>,
 394         constraints: Vec<RegionConstraint<'tcx>>,
 395     ) -> Canonical<'tcx, ConstrainedSubst<'tcx>> {
 396         self.infcx.canonicalize_response(&ConstrainedSubst { subst, constraints })
 397     }
 398
 399     fn u_canonicalize_goal(
 400         &mut self,
 401         value: &Canonical<'tcx, InEnvironment<'tcx, Goal<'tcx>>>,
 402     ) -> (Canonical<'tcx, InEnvironment<'tcx, Goal<'tcx>>>, UniverseMap) {
 403         (value.clone(), UniverseMap)
 404     }
 405
 406     fn invert_goal(
 407         &mut self,
 408         _value: &InEnvironment<'tcx, Goal<'tcx>>,
 409     ) -> Option<InEnvironment<'tcx, Goal<'tcx>>> {
 410         panic!("goal inversion not yet implemented")
 411     }
 412
 413     fn unify_parameters(
 414         &mut self,
 415         environment: &Environment<'tcx>,
 416         variance: ty::Variance,
 417         a: &GenericArg<'tcx>,
 418         b: &GenericArg<'tcx>,
 419     ) -> Fallible<UnificationResult<'tcx>> {
 420         self.infcx.commit_if_ok(|_| {
 421             unify(self.infcx, *environment, variance, a, b)
 422                 .map_err(|_| chalk_engine::fallible::NoSolution)
 423         })
 424     }
 425
 426     fn sink_answer_subset(
 427         &self,
 428         value: &Canonical<'tcx, ConstrainedSubst<'tcx>>,
 429     ) -> Canonical<'tcx, ConstrainedSubst<'tcx>> {
 430         value.clone()
 431     }
 432
 433     fn lift_delayed_literal(
 434         &self,
 435         value: DelayedLiteral<ChalkArenas<'tcx>>,
 436     ) -> DelayedLiteral<ChalkArenas<'tcx>> {
 437         match self.infcx.tcx.lift(&value) {
 438             Some(literal) => literal,
 439             None => bug!("cannot lift {:?}", value),
 440         }
 441     }
 442
 443     fn into_ex_clause(
 444         &mut self,
 445         result: UnificationResult<'tcx>,
 446         ex_clause: &mut ChalkExClause<'tcx>,
 447     ) {
 448         into_ex_clause(result, ex_clause);
 449     }
 450 }
 451
 452 crate fn into_ex_clause(result: UnificationResult<'tcx>, ex_clause: &mut ChalkExClause<'tcx>) {
 453     ex_clause.subgoals.extend(result.goals.into_iter().map(Literal::Positive));
 454
 455     // FIXME: restore this later once we get better at handling regions
 456     let _ = result.constraints.len(); // trick `-D dead-code`
 457     // ex_clause.constraints.extend(result.constraints);
 458 }
 459
 460 type ChalkHhGoal<'tcx> = HhGoal<ChalkArenas<'tcx>>;
 461
 462 type ChalkExClause<'tcx> = ExClause<ChalkArenas<'tcx>>;
 463
 464 impl Debug for ChalkContext<'tcx> {
 465     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
 466         write!(f, "ChalkContext")
 467     }
 468 }
 469
 470 impl Debug for ChalkInferenceContext<'cx, 'tcx> {
 471     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
 472         write!(f, "ChalkInferenceContext")
 473     }
 474 }
 475
 476 impl ChalkContextLift<'tcx> for ChalkArenas<'a> {
 477     type LiftedExClause = ChalkExClause<'tcx>;
 478     type LiftedDelayedLiteral = DelayedLiteral<ChalkArenas<'tcx>>;
 479     type LiftedLiteral = Literal<ChalkArenas<'tcx>>;
 480
 481     fn lift_ex_clause_to_tcx(
 482         ex_clause: &ChalkExClause<'a>,
 483         tcx: TyCtxt<'tcx>,
 484     ) -> Option<Self::LiftedExClause> {
 485         Some(ChalkExClause {
 486             subst: tcx.lift(&ex_clause.subst)?,
 487             delayed_literals: tcx.lift(&ex_clause.delayed_literals)?,
 488             constraints: tcx.lift(&ex_clause.constraints)?,
 489             subgoals: tcx.lift(&ex_clause.subgoals)?,
 490         })
 491     }
 492
 493     fn lift_delayed_literal_to_tcx(
 494         literal: &DelayedLiteral<ChalkArenas<'a>>,
 495         tcx: TyCtxt<'tcx>,
 496     ) -> Option<Self::LiftedDelayedLiteral> {
 497         Some(match literal {
 498             DelayedLiteral::CannotProve(()) => DelayedLiteral::CannotProve(()),
 499             DelayedLiteral::Negative(index) => DelayedLiteral::Negative(*index),
 500             DelayedLiteral::Positive(index, subst) => {
 501                 DelayedLiteral::Positive(*index, tcx.lift(subst)?)
 502             }
 503         })
 504     }
 505
 506     fn lift_literal_to_tcx(
 507         literal: &Literal<ChalkArenas<'a>>,
 508         tcx: TyCtxt<'tcx>,
 509     ) -> Option<Self::LiftedLiteral> {
 510         Some(match literal {
 511             Literal::Negative(goal) => Literal::Negative(tcx.lift(goal)?),
 512             Literal::Positive(goal) => Literal::Positive(tcx.lift(goal)?),
 513         })
 514     }
 515 }
 516
 517 impl ExClauseFold<'tcx> for ChalkArenas<'tcx> {
 518     fn fold_ex_clause_with<F: TypeFolder<'tcx>>(
 519         ex_clause: &ChalkExClause<'tcx>,
 520         folder: &mut F,
 521     ) -> ChalkExClause<'tcx> {
 522         ExClause {
 523             subst: ex_clause.subst.fold_with(folder),
 524             delayed_literals: ex_clause.delayed_literals.fold_with(folder),
 525             constraints: ex_clause.constraints.fold_with(folder),
 526             subgoals: ex_clause.subgoals.fold_with(folder),
 527         }
 528     }
 529
 530     fn visit_ex_clause_with<V: TypeVisitor<'tcx>>(
 531         ex_clause: &ExClause<Self>,
 532         visitor: &mut V,
 533     ) -> bool {
 534         let ExClause { subst, delayed_literals, constraints, subgoals } = ex_clause;
 535         subst.visit_with(visitor)
 536             || delayed_literals.visit_with(visitor)
 537             || constraints.visit_with(visitor)
 538             || subgoals.visit_with(visitor)
 539     }
 540 }
 541
 542 trait Upcast<'tcx>: 'tcx {
 543     type Upcasted: 'tcx;
 544
 545     fn upcast(&self) -> Self::Upcasted;
 546 }
 547
 548 impl<'tcx> Upcast<'tcx> for DelayedLiteral<ChalkArenas<'tcx>> {
 549     type Upcasted = DelayedLiteral<ChalkArenas<'tcx>>;
 550
 551     fn upcast(&self) -> Self::Upcasted {
 552         match self {
 553             &DelayedLiteral::CannotProve(..) => DelayedLiteral::CannotProve(()),
 554             &DelayedLiteral::Negative(index) => DelayedLiteral::Negative(index),
 555             DelayedLiteral::Positive(index, subst) => {
 556                 DelayedLiteral::Positive(*index, subst.clone())
 557             }
 558         }
 559     }
 560 }
 561
 562 impl<'tcx> Upcast<'tcx> for Literal<ChalkArenas<'tcx>> {
 563     type Upcasted = Literal<ChalkArenas<'tcx>>;
 564
 565     fn upcast(&self) -> Self::Upcasted {
 566         match self {
 567             &Literal::Negative(goal) => Literal::Negative(goal),
 568             &Literal::Positive(goal) => Literal::Positive(goal),
 569         }
 570     }
 571 }
 572
 573 impl<'tcx> Upcast<'tcx> for ExClause<ChalkArenas<'tcx>> {
 574     type Upcasted = ExClause<ChalkArenas<'tcx>>;
 575
 576     fn upcast(&self) -> Self::Upcasted {
 577         ExClause {
 578             subst: self.subst.clone(),
 579             delayed_literals: self.delayed_literals.iter().map(|l| l.upcast()).collect(),
 580             constraints: self.constraints.clone(),
 581             subgoals: self.subgoals.iter().map(|g| g.upcast()).collect(),
 582         }
 583     }
 584 }
 585
 586 impl<'tcx, T> Upcast<'tcx> for Canonical<'tcx, T>
 587 where
 588     T: Upcast<'tcx>,
 589 {
 590     type Upcasted = Canonical<'tcx, T::Upcasted>;
 591
 592     fn upcast(&self) -> Self::Upcasted {
 593         Canonical {
 594             max_universe: self.max_universe,
 595             value: self.value.upcast(),
 596             variables: self.variables,
 597         }
 598     }
 599 }
 600
 601 crate fn provide(p: &mut Providers<'_>) {
 602     *p = Providers { evaluate_goal, ..*p };
 603 }
 604
 605 crate fn evaluate_goal<'tcx>(
 606     tcx: TyCtxt<'tcx>,
 607     goal: ChalkCanonicalGoal<'tcx>,
 608 ) -> Result<&'tcx Canonical<'tcx, QueryResponse<'tcx, ()>>, traits::query::NoSolution> {
 609     use crate::lowering::Lower;
 610     use rustc::traits::WellFormed;
 611
 612     let goal = goal.unchecked_map(|goal| InEnvironment {
 613         environment: goal.environment,
 614         goal: match goal.goal {
 615             ty::Predicate::WellFormed(ty) => {
 616                 tcx.mk_goal(GoalKind::DomainGoal(DomainGoal::WellFormed(WellFormed::Ty(ty))))
 617             }
 618
 619             ty::Predicate::Subtype(predicate) => tcx.mk_goal(GoalKind::Quantified(
 620                 QuantifierKind::Universal,
 621                 predicate.map_bound(|pred| tcx.mk_goal(GoalKind::Subtype(pred.a, pred.b))),
 622             )),
 623
 624             other => tcx.mk_goal(GoalKind::from_poly_domain_goal(other.lower(), tcx)),
 625         },
 626     });
 627
 628     debug!("evaluate_goal(goal = {:?})", goal);
 629
 630     let context = ChalkContext { _arenas: ChalkArenas { _phantom: PhantomData }, tcx };
 631
 632     let mut forest = Forest::new(context);
 633     let solution = forest.solve(&goal);
 634
 635     debug!("evaluate_goal: solution = {:?}", solution);
 636
 637     solution.map(|ok| Ok(&*tcx.arena.alloc(ok))).unwrap_or(Err(traits::query::NoSolution))
 638 }