compiler/rustc_traits/src/chalk/mod.rs

   1 //! Calls `chalk-solve` to solve a `ty::Predicate`
   2 //!
   3 //! In order to call `chalk-solve`, this file must convert a `CanonicalChalkEnvironmentAndGoal` into
   4 //! a Chalk uncanonical goal. It then calls Chalk, and converts the answer back into rustc solution.
   5
   6 pub(crate) mod db;
   7 pub(crate) mod lowering;
   8
   9 use rustc_data_structures::fx::FxHashMap;
  10
  11 use rustc_index::vec::IndexVec;
  12
  13 use rustc_middle::infer::canonical::{CanonicalTyVarKind, CanonicalVarKind};
  14 use rustc_middle::traits::ChalkRustInterner;
  15 use rustc_middle::ty::query::Providers;
  16 use rustc_middle::ty::subst::GenericArg;
  17 use rustc_middle::ty::{self, BoundVar, ParamTy, TyCtxt, TypeFoldable, TypeVisitable};
  18
  19 use rustc_infer::infer::canonical::{
  20     Canonical, CanonicalVarValues, Certainty, QueryRegionConstraints, QueryResponse,
  21 };
  22 use rustc_infer::traits::{self, CanonicalChalkEnvironmentAndGoal};
  23
  24 use crate::chalk::db::RustIrDatabase as ChalkRustIrDatabase;
  25 use crate::chalk::lowering::LowerInto;
  26 use crate::chalk::lowering::{ParamsSubstitutor, PlaceholdersCollector, ReverseParamsSubstitutor};
  27
  28 use chalk_solve::Solution;
  29
  30 pub(crate) fn provide(p: &mut Providers) {
  31     *p = Providers { evaluate_goal, ..*p };
  32 }
  33
  34 pub(crate) fn evaluate_goal<'tcx>(
  35     tcx: TyCtxt<'tcx>,
  36     obligation: CanonicalChalkEnvironmentAndGoal<'tcx>,
  37 ) -> Result<&'tcx Canonical<'tcx, QueryResponse<'tcx, ()>>, traits::query::NoSolution> {
  38     let interner = ChalkRustInterner { tcx };
  39
  40     // Chalk doesn't have a notion of `Params`, so instead we use placeholders.
  41     let mut placeholders_collector = PlaceholdersCollector::new();
  42     obligation.visit_with(&mut placeholders_collector);
  43
  44     let mut params_substitutor =
  45         ParamsSubstitutor::new(tcx, placeholders_collector.next_ty_placeholder);
  46     let obligation = obligation.fold_with(&mut params_substitutor);
  47     let params: FxHashMap<usize, ParamTy> = params_substitutor.params;
  48
  49     let max_universe = obligation.max_universe.index();
  50
  51     let lowered_goal: chalk_ir::UCanonical<
  52         chalk_ir::InEnvironment<chalk_ir::Goal<ChalkRustInterner<'tcx>>>,
  53     > = chalk_ir::UCanonical {
  54         canonical: chalk_ir::Canonical {
  55             binders: chalk_ir::CanonicalVarKinds::from_iter(
  56                 interner,
  57                 obligation.variables.iter().map(|v| match v.kind {
  58                     CanonicalVarKind::PlaceholderTy(_ty) => unimplemented!(),
  59                     CanonicalVarKind::PlaceholderRegion(_ui) => unimplemented!(),
  60                     CanonicalVarKind::Ty(ty) => match ty {
  61                         CanonicalTyVarKind::General(ui) => chalk_ir::WithKind::new(
  62                             chalk_ir::VariableKind::Ty(chalk_ir::TyVariableKind::General),
  63                             chalk_ir::UniverseIndex { counter: ui.index() },
  64                         ),
  65                         CanonicalTyVarKind::Int => chalk_ir::WithKind::new(
  66                             chalk_ir::VariableKind::Ty(chalk_ir::TyVariableKind::Integer),
  67                             chalk_ir::UniverseIndex::root(),
  68                         ),
  69                         CanonicalTyVarKind::Float => chalk_ir::WithKind::new(
  70                             chalk_ir::VariableKind::Ty(chalk_ir::TyVariableKind::Float),
  71                             chalk_ir::UniverseIndex::root(),
  72                         ),
  73                     },
  74                     CanonicalVarKind::Region(ui) => chalk_ir::WithKind::new(
  75                         chalk_ir::VariableKind::Lifetime,
  76                         chalk_ir::UniverseIndex { counter: ui.index() },
  77                     ),
  78                     CanonicalVarKind::Const(_ui, _ty) => unimplemented!(),
  79                     CanonicalVarKind::PlaceholderConst(_pc, _ty) => unimplemented!(),
  80                 }),
  81             ),
  82             value: obligation.value.lower_into(interner),
  83         },
  84         universes: max_universe + 1,
  85     };
  86
  87     use chalk_solve::Solver;
  88     let mut solver = chalk_engine::solve::SLGSolver::new(32, None);
  89     let db = ChalkRustIrDatabase { interner };
  90     debug!(?lowered_goal);
  91     let solution = solver.solve(&db, &lowered_goal);
  92     debug!(?obligation, ?solution, "evaluate goal");
  93
  94     // Ideally, the code to convert *back* to rustc types would live close to
  95     // the code to convert *from* rustc types. Right now though, we don't
  96     // really need this and so it's really minimal.
  97     // Right now, we also treat a `Unique` solution the same as
  98     // `Ambig(Definite)`. This really isn't right.
  99     let make_solution = |subst: chalk_ir::Substitution<_>,
 100                          binders: chalk_ir::CanonicalVarKinds<_>| {
 101         use rustc_middle::infer::canonical::CanonicalVarInfo;
 102
 103         let mut var_values: IndexVec<BoundVar, GenericArg<'tcx>> = IndexVec::new();
 104         let mut reverse_param_substitutor = ReverseParamsSubstitutor::new(tcx, params);
 105         subst.as_slice(interner).iter().for_each(|p| {
 106             var_values.push(p.lower_into(interner).fold_with(&mut reverse_param_substitutor));
 107         });
 108         let variables: Vec<_> = binders
 109             .iter(interner)
 110             .map(|var| {
 111                 let kind = match var.kind {
 112                     chalk_ir::VariableKind::Ty(ty_kind) => CanonicalVarKind::Ty(match ty_kind {
 113                         chalk_ir::TyVariableKind::General => CanonicalTyVarKind::General(
 114                             ty::UniverseIndex::from_usize(var.skip_kind().counter),
 115                         ),
 116                         chalk_ir::TyVariableKind::Integer => CanonicalTyVarKind::Int,
 117                         chalk_ir::TyVariableKind::Float => CanonicalTyVarKind::Float,
 118                     }),
 119                     chalk_ir::VariableKind::Lifetime => CanonicalVarKind::Region(
 120                         ty::UniverseIndex::from_usize(var.skip_kind().counter),
 121                     ),
 122                     // FIXME(compiler-errors): We don't currently have a way of turning
 123                     // a Chalk ty back into a rustc ty, right?
 124                     chalk_ir::VariableKind::Const(_) => todo!(),
 125                 };
 126                 CanonicalVarInfo { kind }
 127             })
 128             .collect();
 129         let max_universe = binders.iter(interner).map(|v| v.skip_kind().counter).max().unwrap_or(0);
 130         let sol = Canonical {
 131             max_universe: ty::UniverseIndex::from_usize(max_universe),
 132             variables: tcx.intern_canonical_var_infos(&variables),
 133             value: QueryResponse {
 134                 var_values: CanonicalVarValues { var_values },
 135                 region_constraints: QueryRegionConstraints::default(),
 136                 certainty: Certainty::Proven,
 137                 opaque_types: vec![],
 138                 value: (),
 139             },
 140         };
 141         tcx.arena.alloc(sol)
 142     };
 143     solution
 144         .map(|s| match s {
 145             Solution::Unique(subst) => {
 146                 // FIXME(chalk): handle constraints
 147                 make_solution(subst.value.subst, subst.binders)
 148             }
 149             Solution::Ambig(guidance) => {
 150                 match guidance {
 151                     chalk_solve::Guidance::Definite(subst) => {
 152                         make_solution(subst.value, subst.binders)
 153                     }
 154                     chalk_solve::Guidance::Suggested(_) => unimplemented!(),
 155                     chalk_solve::Guidance::Unknown => {
 156                         // chalk_fulfill doesn't use the var_values here, so
 157                         // let's just ignore that
 158                         let sol = Canonical {
 159                             max_universe: ty::UniverseIndex::from_usize(0),
 160                             variables: obligation.variables,
 161                             value: QueryResponse {
 162                                 var_values: CanonicalVarValues { var_values: IndexVec::new() }
 163                                     .make_identity(tcx),
 164                                 region_constraints: QueryRegionConstraints::default(),
 165                                 certainty: Certainty::Ambiguous,
 166                                 opaque_types: vec![],
 167                                 value: (),
 168                             },
 169                         };
 170                         &*tcx.arena.alloc(sol)
 171                     }
 172                 }
 173             }
 174         })
 175         .ok_or(traits::query::NoSolution)
 176 }