2019-05-01 10:06:11 -05:00
|
|
|
//! Trait solving using Chalk.
|
2020-03-06 16:04:14 -06:00
|
|
|
use std::{panic, sync::Arc};
|
2019-03-31 13:02:16 -05:00
|
|
|
|
2019-12-21 07:46:15 -06:00
|
|
|
use chalk_ir::cast::Cast;
|
2019-11-27 03:02:54 -06:00
|
|
|
use hir_def::{expr::ExprId, DefWithBodyId, ImplId, TraitId, TypeAliasId};
|
2020-03-06 16:04:14 -06:00
|
|
|
use ra_db::{impl_intern_key, salsa, CrateId};
|
2019-05-21 08:04:17 -05:00
|
|
|
use ra_prof::profile;
|
2019-07-04 15:05:17 -05:00
|
|
|
use rustc_hash::FxHashSet;
|
2019-03-31 13:02:16 -05:00
|
|
|
|
2020-04-05 11:24:18 -05:00
|
|
|
use crate::{db::HirDatabase, DebruijnIndex};
|
2019-11-26 09:02:50 -06:00
|
|
|
|
2019-09-03 06:10:00 -05:00
|
|
|
use super::{Canonical, GenericPredicate, HirDisplay, ProjectionTy, TraitRef, Ty, TypeWalk};
|
2019-05-01 10:06:11 -05:00
|
|
|
|
2020-02-24 14:36:57 -06:00
|
|
|
use self::chalk::{from_chalk, Interner, ToChalk};
|
2019-05-01 10:06:11 -05:00
|
|
|
|
2019-06-26 04:54:13 -05:00
|
|
|
pub(crate) mod chalk;
|
2019-12-03 05:16:39 -06:00
|
|
|
mod builtin;
|
2019-03-31 13:02:16 -05:00
|
|
|
|
2019-05-07 10:35:45 -05:00
|
|
|
/// This controls the maximum size of types Chalk considers. If we set this too
|
|
|
|
/// high, we can run into slow edge cases; if we set it too low, Chalk won't
|
|
|
|
/// find some solutions.
|
2020-01-27 14:38:20 -06:00
|
|
|
const CHALK_SOLVER_MAX_SIZE: usize = 10;
|
2020-01-17 15:12:15 -06:00
|
|
|
/// This controls how much 'time' we give the Chalk solver before giving up.
|
|
|
|
const CHALK_SOLVER_FUEL: i32 = 100;
|
2019-05-07 10:35:45 -05:00
|
|
|
|
2019-04-20 05:34:36 -05:00
|
|
|
#[derive(Debug, Copy, Clone)]
|
2020-03-13 10:05:46 -05:00
|
|
|
struct ChalkContext<'a> {
|
|
|
|
db: &'a dyn HirDatabase,
|
2019-11-27 00:42:55 -06:00
|
|
|
krate: CrateId,
|
2019-04-20 05:34:36 -05:00
|
|
|
}
|
2019-03-31 13:02:16 -05:00
|
|
|
|
2020-02-24 14:36:57 -06:00
|
|
|
fn create_chalk_solver() -> chalk_solve::Solver<Interner> {
|
2020-01-17 15:12:15 -06:00
|
|
|
let solver_choice =
|
|
|
|
chalk_solve::SolverChoice::SLG { max_size: CHALK_SOLVER_MAX_SIZE, expected_answers: None };
|
2020-01-13 10:15:50 -06:00
|
|
|
solver_choice.into_solver()
|
2019-04-20 05:34:36 -05:00
|
|
|
}
|
|
|
|
|
|
|
|
/// Collects impls for the given trait in the whole dependency tree of `krate`.
|
2019-05-21 04:44:08 -05:00
|
|
|
pub(crate) fn impls_for_trait_query(
|
2020-03-13 10:05:46 -05:00
|
|
|
db: &dyn HirDatabase,
|
2019-11-26 13:26:47 -06:00
|
|
|
krate: CrateId,
|
|
|
|
trait_: TraitId,
|
2019-11-27 03:02:54 -06:00
|
|
|
) -> Arc<[ImplId]> {
|
2019-05-07 05:09:57 -05:00
|
|
|
let mut impls = FxHashSet::default();
|
2019-04-20 05:34:36 -05:00
|
|
|
// We call the query recursively here. On the one hand, this means we can
|
|
|
|
// reuse results from queries for different crates; on the other hand, this
|
|
|
|
// will only ever get called for a few crates near the root of the tree (the
|
|
|
|
// ones the user is editing), so this may actually be a waste of memory. I'm
|
|
|
|
// doing it like this mainly for simplicity for now.
|
2020-03-09 05:11:59 -05:00
|
|
|
for dep in &db.crate_graph()[krate].dependencies {
|
2019-11-26 13:26:47 -06:00
|
|
|
impls.extend(db.impls_for_trait(dep.crate_id, trait_).iter());
|
2019-04-20 05:34:36 -05:00
|
|
|
}
|
2020-02-29 14:24:40 -06:00
|
|
|
let crate_impl_defs = db.impls_in_crate(krate);
|
|
|
|
impls.extend(crate_impl_defs.lookup_impl_defs_for_trait(trait_));
|
2019-10-13 23:06:05 -05:00
|
|
|
impls.into_iter().collect()
|
2019-04-20 05:34:36 -05:00
|
|
|
}
|
|
|
|
|
2019-06-29 10:40:00 -05:00
|
|
|
/// A set of clauses that we assume to be true. E.g. if we are inside this function:
|
|
|
|
/// ```rust
|
|
|
|
/// fn foo<T: Default>(t: T) {}
|
|
|
|
/// ```
|
|
|
|
/// we assume that `T: Default`.
|
2019-06-29 12:14:52 -05:00
|
|
|
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
|
2019-07-09 14:34:23 -05:00
|
|
|
pub struct TraitEnvironment {
|
2019-06-29 12:14:52 -05:00
|
|
|
pub predicates: Vec<GenericPredicate>,
|
|
|
|
}
|
2019-06-29 10:40:00 -05:00
|
|
|
|
2019-09-07 09:24:26 -05:00
|
|
|
impl TraitEnvironment {
|
|
|
|
/// Returns trait refs with the given self type which are supposed to hold
|
|
|
|
/// in this trait env. E.g. if we are in `foo<T: SomeTrait>()`, this will
|
|
|
|
/// find that `T: SomeTrait` if we call it for `T`.
|
|
|
|
pub(crate) fn trait_predicates_for_self_ty<'a>(
|
|
|
|
&'a self,
|
|
|
|
ty: &'a Ty,
|
|
|
|
) -> impl Iterator<Item = &'a TraitRef> + 'a {
|
|
|
|
self.predicates.iter().filter_map(move |pred| match pred {
|
|
|
|
GenericPredicate::Implemented(tr) if tr.self_ty() == ty => Some(tr),
|
|
|
|
_ => None,
|
|
|
|
})
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2019-06-29 10:40:00 -05:00
|
|
|
/// Something (usually a goal), along with an environment.
|
2019-06-29 12:14:52 -05:00
|
|
|
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
|
2019-06-29 10:40:00 -05:00
|
|
|
pub struct InEnvironment<T> {
|
2019-07-09 14:34:23 -05:00
|
|
|
pub environment: Arc<TraitEnvironment>,
|
2019-06-29 10:40:00 -05:00
|
|
|
pub value: T,
|
|
|
|
}
|
|
|
|
|
|
|
|
impl<T> InEnvironment<T> {
|
2019-07-09 14:34:23 -05:00
|
|
|
pub fn new(environment: Arc<TraitEnvironment>, value: T) -> InEnvironment<T> {
|
2019-06-29 10:40:00 -05:00
|
|
|
InEnvironment { environment, value }
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2019-03-31 13:02:16 -05:00
|
|
|
/// Something that needs to be proven (by Chalk) during type checking, e.g. that
|
|
|
|
/// a certain type implements a certain trait. Proving the Obligation might
|
|
|
|
/// result in additional information about inference variables.
|
2019-07-08 14:43:52 -05:00
|
|
|
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
|
2019-03-31 13:02:16 -05:00
|
|
|
pub enum Obligation {
|
|
|
|
/// Prove that a certain type implements a trait (the type is the `Self` type
|
|
|
|
/// parameter to the `TraitRef`).
|
|
|
|
Trait(TraitRef),
|
2019-07-07 02:31:09 -05:00
|
|
|
Projection(ProjectionPredicate),
|
2019-05-12 10:53:44 -05:00
|
|
|
}
|
|
|
|
|
2019-07-06 09:41:04 -05:00
|
|
|
impl Obligation {
|
|
|
|
pub fn from_predicate(predicate: GenericPredicate) -> Option<Obligation> {
|
|
|
|
match predicate {
|
|
|
|
GenericPredicate::Implemented(trait_ref) => Some(Obligation::Trait(trait_ref)),
|
2019-08-23 10:19:37 -05:00
|
|
|
GenericPredicate::Projection(projection_pred) => {
|
|
|
|
Some(Obligation::Projection(projection_pred))
|
|
|
|
}
|
2019-07-06 09:41:04 -05:00
|
|
|
GenericPredicate::Error => None,
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2019-05-12 10:53:44 -05:00
|
|
|
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
|
|
|
|
pub struct ProjectionPredicate {
|
2019-05-12 11:33:47 -05:00
|
|
|
pub projection_ty: ProjectionTy,
|
|
|
|
pub ty: Ty,
|
2019-03-31 13:02:16 -05:00
|
|
|
}
|
|
|
|
|
2019-09-03 06:10:00 -05:00
|
|
|
impl TypeWalk for ProjectionPredicate {
|
|
|
|
fn walk(&self, f: &mut impl FnMut(&Ty)) {
|
2019-08-23 10:19:37 -05:00
|
|
|
self.projection_ty.walk(f);
|
|
|
|
self.ty.walk(f);
|
|
|
|
}
|
|
|
|
|
2020-04-05 11:24:18 -05:00
|
|
|
fn walk_mut_binders(
|
|
|
|
&mut self,
|
|
|
|
f: &mut impl FnMut(&mut Ty, DebruijnIndex),
|
|
|
|
binders: DebruijnIndex,
|
|
|
|
) {
|
2019-11-16 05:53:13 -06:00
|
|
|
self.projection_ty.walk_mut_binders(f, binders);
|
|
|
|
self.ty.walk_mut_binders(f, binders);
|
2019-08-23 10:19:37 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2019-07-08 14:43:52 -05:00
|
|
|
/// Solve a trait goal using Chalk.
|
2019-07-09 14:34:23 -05:00
|
|
|
pub(crate) fn trait_solve_query(
|
2020-03-13 10:05:46 -05:00
|
|
|
db: &dyn HirDatabase,
|
2019-11-27 00:42:55 -06:00
|
|
|
krate: CrateId,
|
2019-08-10 05:13:39 -05:00
|
|
|
goal: Canonical<InEnvironment<Obligation>>,
|
2019-04-20 05:34:36 -05:00
|
|
|
) -> Option<Solution> {
|
2020-03-06 10:23:08 -06:00
|
|
|
let _p = profile("trait_solve_query").detail(|| match &goal.value.value {
|
|
|
|
Obligation::Trait(it) => db.trait_data(it.trait_).name.to_string(),
|
|
|
|
Obligation::Projection(_) => "projection".to_string(),
|
|
|
|
});
|
2020-04-06 08:01:58 -05:00
|
|
|
log::info!("trait_solve_query({})", goal.value.value.display(db));
|
2019-09-24 12:04:53 -05:00
|
|
|
|
|
|
|
if let Obligation::Projection(pred) = &goal.value.value {
|
|
|
|
if let Ty::Bound(_) = &pred.projection_ty.parameters[0] {
|
|
|
|
// Hack: don't ask Chalk to normalize with an unknown self type, it'll say that's impossible
|
|
|
|
return Some(Solution::Ambig(Guidance::Unknown));
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2020-03-27 08:50:08 -05:00
|
|
|
let canonical = goal.to_chalk(db).cast(&Interner);
|
2019-11-16 05:53:13 -06:00
|
|
|
|
2019-05-21 12:57:36 -05:00
|
|
|
// We currently don't deal with universes (I think / hope they're not yet
|
|
|
|
// relevant for our use cases?)
|
|
|
|
let u_canonical = chalk_ir::UCanonical { canonical, universes: 1 };
|
2020-03-06 16:04:14 -06:00
|
|
|
let solution = solve(db, krate, &u_canonical);
|
2019-05-21 12:57:36 -05:00
|
|
|
solution.map(|solution| solution_from_chalk(db, solution))
|
2019-03-31 13:02:16 -05:00
|
|
|
}
|
|
|
|
|
2020-03-06 16:04:14 -06:00
|
|
|
fn solve(
|
2020-03-13 10:05:46 -05:00
|
|
|
db: &dyn HirDatabase,
|
2020-03-06 16:04:14 -06:00
|
|
|
krate: CrateId,
|
|
|
|
goal: &chalk_ir::UCanonical<chalk_ir::InEnvironment<chalk_ir::Goal<Interner>>>,
|
|
|
|
) -> Option<chalk_solve::Solution<Interner>> {
|
|
|
|
let context = ChalkContext { db, krate };
|
|
|
|
log::debug!("solve goal: {:?}", goal);
|
|
|
|
let mut solver = create_chalk_solver();
|
|
|
|
|
|
|
|
let fuel = std::cell::Cell::new(CHALK_SOLVER_FUEL);
|
|
|
|
|
|
|
|
let solution = solver.solve_limited(&context, goal, || {
|
|
|
|
context.db.check_canceled();
|
|
|
|
let remaining = fuel.get();
|
|
|
|
fuel.set(remaining - 1);
|
|
|
|
if remaining == 0 {
|
|
|
|
log::debug!("fuel exhausted");
|
|
|
|
}
|
|
|
|
remaining > 0
|
|
|
|
});
|
|
|
|
|
|
|
|
log::debug!("solve({:?}) => {:?}", goal, solution);
|
|
|
|
solution
|
|
|
|
}
|
|
|
|
|
2019-11-16 06:21:51 -06:00
|
|
|
fn solution_from_chalk(
|
2020-03-13 10:05:46 -05:00
|
|
|
db: &dyn HirDatabase,
|
2020-02-24 14:36:57 -06:00
|
|
|
solution: chalk_solve::Solution<Interner>,
|
2019-11-16 06:21:51 -06:00
|
|
|
) -> Solution {
|
2020-02-24 14:36:57 -06:00
|
|
|
let convert_subst = |subst: chalk_ir::Canonical<chalk_ir::Substitution<Interner>>| {
|
2019-04-20 05:34:36 -05:00
|
|
|
let value = subst
|
|
|
|
.value
|
2020-03-27 08:50:08 -05:00
|
|
|
.iter(&Interner)
|
|
|
|
.map(|p| match p.ty(&Interner) {
|
2020-02-18 07:32:19 -06:00
|
|
|
Some(ty) => from_chalk(db, ty.clone()),
|
|
|
|
None => unimplemented!(),
|
2019-04-20 05:34:36 -05:00
|
|
|
})
|
|
|
|
.collect();
|
|
|
|
let result = Canonical { value, num_vars: subst.binders.len() };
|
|
|
|
SolutionVariables(result)
|
|
|
|
};
|
|
|
|
match solution {
|
2019-05-01 09:37:52 -05:00
|
|
|
chalk_solve::Solution::Unique(constr_subst) => {
|
2019-04-20 05:34:36 -05:00
|
|
|
let subst = chalk_ir::Canonical {
|
|
|
|
value: constr_subst.value.subst,
|
|
|
|
binders: constr_subst.binders,
|
|
|
|
};
|
2019-05-01 09:37:52 -05:00
|
|
|
Solution::Unique(convert_subst(subst))
|
2019-04-20 05:34:36 -05:00
|
|
|
}
|
2019-05-01 09:37:52 -05:00
|
|
|
chalk_solve::Solution::Ambig(chalk_solve::Guidance::Definite(subst)) => {
|
|
|
|
Solution::Ambig(Guidance::Definite(convert_subst(subst)))
|
2019-04-20 05:34:36 -05:00
|
|
|
}
|
2019-05-01 09:37:52 -05:00
|
|
|
chalk_solve::Solution::Ambig(chalk_solve::Guidance::Suggested(subst)) => {
|
|
|
|
Solution::Ambig(Guidance::Suggested(convert_subst(subst)))
|
2019-03-31 13:02:16 -05:00
|
|
|
}
|
2019-05-01 09:37:52 -05:00
|
|
|
chalk_solve::Solution::Ambig(chalk_solve::Guidance::Unknown) => {
|
|
|
|
Solution::Ambig(Guidance::Unknown)
|
2019-04-20 05:34:36 -05:00
|
|
|
}
|
2019-03-31 13:02:16 -05:00
|
|
|
}
|
2019-04-20 05:34:36 -05:00
|
|
|
}
|
|
|
|
|
|
|
|
#[derive(Clone, Debug, PartialEq, Eq)]
|
2019-05-05 09:04:31 -05:00
|
|
|
pub struct SolutionVariables(pub Canonical<Vec<Ty>>);
|
2019-04-20 05:34:36 -05:00
|
|
|
|
|
|
|
#[derive(Clone, Debug, PartialEq, Eq)]
|
|
|
|
/// A (possible) solution for a proposed goal.
|
2019-05-05 09:04:31 -05:00
|
|
|
pub enum Solution {
|
2019-04-20 05:34:36 -05:00
|
|
|
/// The goal indeed holds, and there is a unique value for all existential
|
|
|
|
/// variables.
|
|
|
|
Unique(SolutionVariables),
|
|
|
|
|
|
|
|
/// The goal may be provable in multiple ways, but regardless we may have some guidance
|
|
|
|
/// for type inference. In this case, we don't return any lifetime
|
|
|
|
/// constraints, since we have not "committed" to any particular solution
|
|
|
|
/// yet.
|
|
|
|
Ambig(Guidance),
|
|
|
|
}
|
|
|
|
|
|
|
|
#[derive(Clone, Debug, PartialEq, Eq)]
|
|
|
|
/// When a goal holds ambiguously (e.g., because there are multiple possible
|
|
|
|
/// solutions), we issue a set of *guidance* back to type inference.
|
2019-05-05 09:04:31 -05:00
|
|
|
pub enum Guidance {
|
2019-04-20 05:34:36 -05:00
|
|
|
/// The existential variables *must* have the given values if the goal is
|
|
|
|
/// ever to hold, but that alone isn't enough to guarantee the goal will
|
|
|
|
/// actually hold.
|
|
|
|
Definite(SolutionVariables),
|
|
|
|
|
|
|
|
/// There are multiple plausible values for the existentials, but the ones
|
|
|
|
/// here are suggested as the preferred choice heuristically. These should
|
|
|
|
/// be used for inference fallback only.
|
|
|
|
Suggested(SolutionVariables),
|
|
|
|
|
|
|
|
/// There's no useful information to feed back to type inference
|
|
|
|
Unknown,
|
2019-03-31 13:02:16 -05:00
|
|
|
}
|
2019-09-09 15:10:58 -05:00
|
|
|
|
|
|
|
#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
|
|
|
|
pub enum FnTrait {
|
|
|
|
FnOnce,
|
|
|
|
FnMut,
|
|
|
|
Fn,
|
|
|
|
}
|
|
|
|
|
|
|
|
impl FnTrait {
|
|
|
|
fn lang_item_name(self) -> &'static str {
|
|
|
|
match self {
|
|
|
|
FnTrait::FnOnce => "fn_once",
|
|
|
|
FnTrait::FnMut => "fn_mut",
|
|
|
|
FnTrait::Fn => "fn",
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2019-12-21 08:00:44 -06:00
|
|
|
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
|
2019-09-09 15:10:58 -05:00
|
|
|
pub struct ClosureFnTraitImplData {
|
2019-11-25 09:31:48 -06:00
|
|
|
def: DefWithBodyId,
|
2019-09-09 15:10:58 -05:00
|
|
|
expr: ExprId,
|
|
|
|
fn_trait: FnTrait,
|
|
|
|
}
|
|
|
|
|
2020-02-21 12:05:27 -06:00
|
|
|
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
|
|
|
|
pub struct UnsizeToSuperTraitObjectData {
|
|
|
|
trait_: TraitId,
|
|
|
|
super_trait: TraitId,
|
|
|
|
}
|
|
|
|
|
2019-09-09 15:10:58 -05:00
|
|
|
/// An impl. Usually this comes from an impl block, but some built-in types get
|
|
|
|
/// synthetic impls.
|
2019-12-21 08:00:44 -06:00
|
|
|
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
|
2019-09-09 15:10:58 -05:00
|
|
|
pub enum Impl {
|
|
|
|
/// A normal impl from an impl block.
|
2020-02-29 14:24:40 -06:00
|
|
|
ImplDef(ImplId),
|
2019-09-09 15:10:58 -05:00
|
|
|
/// Closure types implement the Fn traits synthetically.
|
|
|
|
ClosureFnTraitImpl(ClosureFnTraitImplData),
|
2020-02-21 11:24:18 -06:00
|
|
|
/// [T; n]: Unsize<[T]>
|
|
|
|
UnsizeArray,
|
2020-02-21 12:05:27 -06:00
|
|
|
/// T: Unsize<dyn Trait> where T: Trait
|
|
|
|
UnsizeToTraitObject(TraitId),
|
|
|
|
/// dyn Trait: Unsize<dyn SuperTrait> if Trait: SuperTrait
|
|
|
|
UnsizeToSuperTraitObject(UnsizeToSuperTraitObjectData),
|
2019-09-09 15:10:58 -05:00
|
|
|
}
|
2019-11-24 05:25:48 -06:00
|
|
|
/// This exists just for Chalk, because our ImplIds are only unique per module.
|
|
|
|
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
|
|
|
|
pub struct GlobalImplId(salsa::InternId);
|
|
|
|
impl_intern_key!(GlobalImplId);
|
2019-11-15 13:32:58 -06:00
|
|
|
|
|
|
|
/// An associated type value. Usually this comes from a `type` declaration
|
|
|
|
/// inside an impl block, but for built-in impls we have to synthesize it.
|
|
|
|
/// (We only need this because Chalk wants a unique ID for each of these.)
|
|
|
|
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
|
|
|
|
pub enum AssocTyValue {
|
|
|
|
/// A normal assoc type value from an impl block.
|
2019-11-27 02:40:10 -06:00
|
|
|
TypeAlias(TypeAliasId),
|
2019-11-15 13:32:58 -06:00
|
|
|
/// The output type of the Fn trait implementation.
|
|
|
|
ClosureFnTraitImplOutput(ClosureFnTraitImplData),
|
|
|
|
}
|
2019-11-24 05:25:48 -06:00
|
|
|
/// This exists just for Chalk, because it needs a unique ID for each associated
|
|
|
|
/// type value in an impl (even synthetic ones).
|
|
|
|
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
|
|
|
|
pub struct AssocTyValueId(salsa::InternId);
|
|
|
|
impl_intern_key!(AssocTyValueId);
|