aboutsummaryrefslogtreecommitdiff
path: root/crates/hir_ty/src/traits.rs
diff options
context:
space:
mode:
Diffstat (limited to 'crates/hir_ty/src/traits.rs')
-rw-r--r--crates/hir_ty/src/traits.rs140
1 files changed, 13 insertions, 127 deletions
diff --git a/crates/hir_ty/src/traits.rs b/crates/hir_ty/src/traits.rs
index ccee0e5ad..9936d0803 100644
--- a/crates/hir_ty/src/traits.rs
+++ b/crates/hir_ty/src/traits.rs
@@ -1,28 +1,26 @@
1//! Trait solving using Chalk. 1//! Trait solving using Chalk.
2
2use std::env::var; 3use std::env::var;
3 4
4use base_db::CrateId;
5use chalk_ir::cast::Cast; 5use chalk_ir::cast::Cast;
6use chalk_solve::{logging_db::LoggingRustIrDatabase, Solver}; 6use chalk_solve::{logging_db::LoggingRustIrDatabase, Solver};
7
8use base_db::CrateId;
7use hir_def::{lang_item::LangItemTarget, TraitId}; 9use hir_def::{lang_item::LangItemTarget, TraitId};
8use stdx::panic_context; 10use stdx::panic_context;
9 11
10use crate::{ 12use crate::{
11 db::HirDatabase, AliasTy, Canonical, DebruijnIndex, HirDisplay, Substitution, Ty, TyKind, 13 db::HirDatabase, AliasEq, AliasTy, Canonical, DomainGoal, Guidance, HirDisplay, InEnvironment,
12 TypeWalk, WhereClause, 14 Interner, Solution, TraitRefExt, Ty, TyKind, WhereClause,
13}; 15};
14 16
15use self::chalk::{from_chalk, Interner, ToChalk};
16
17pub(crate) mod chalk;
18
19/// This controls how much 'time' we give the Chalk solver before giving up. 17/// This controls how much 'time' we give the Chalk solver before giving up.
20const CHALK_SOLVER_FUEL: i32 = 100; 18const CHALK_SOLVER_FUEL: i32 = 100;
21 19
22#[derive(Debug, Copy, Clone)] 20#[derive(Debug, Copy, Clone)]
23struct ChalkContext<'a> { 21pub(crate) struct ChalkContext<'a> {
24 db: &'a dyn HirDatabase, 22 pub(crate) db: &'a dyn HirDatabase,
25 krate: CrateId, 23 pub(crate) krate: CrateId,
26} 24}
27 25
28fn create_chalk_solver() -> chalk_recursive::RecursiveSolver<Interner> { 26fn create_chalk_solver() -> chalk_recursive::RecursiveSolver<Interner> {
@@ -70,55 +68,6 @@ impl Default for TraitEnvironment {
70 } 68 }
71} 69}
72 70
73/// Something (usually a goal), along with an environment.
74#[derive(Clone, Debug, PartialEq, Eq, Hash)]
75pub struct InEnvironment<T> {
76 pub environment: chalk_ir::Environment<Interner>,
77 pub goal: T,
78}
79
80impl<T> InEnvironment<T> {
81 pub fn new(environment: chalk_ir::Environment<Interner>, value: T) -> InEnvironment<T> {
82 InEnvironment { environment, goal: value }
83 }
84}
85
86/// Something that needs to be proven (by Chalk) during type checking, e.g. that
87/// a certain type implements a certain trait. Proving the Obligation might
88/// result in additional information about inference variables.
89#[derive(Clone, Debug, PartialEq, Eq, Hash)]
90pub enum DomainGoal {
91 Holds(WhereClause),
92}
93
94#[derive(Clone, Debug, PartialEq, Eq, Hash)]
95pub struct AliasEq {
96 pub alias: AliasTy,
97 pub ty: Ty,
98}
99
100impl TypeWalk for AliasEq {
101 fn walk(&self, f: &mut impl FnMut(&Ty)) {
102 self.ty.walk(f);
103 match &self.alias {
104 AliasTy::Projection(projection_ty) => projection_ty.walk(f),
105 AliasTy::Opaque(opaque) => opaque.walk(f),
106 }
107 }
108
109 fn walk_mut_binders(
110 &mut self,
111 f: &mut impl FnMut(&mut Ty, DebruijnIndex),
112 binders: DebruijnIndex,
113 ) {
114 self.ty.walk_mut_binders(f, binders);
115 match &mut self.alias {
116 AliasTy::Projection(projection_ty) => projection_ty.walk_mut_binders(f, binders),
117 AliasTy::Opaque(opaque) => opaque.walk_mut_binders(f, binders),
118 }
119 }
120}
121
122/// Solve a trait goal using Chalk. 71/// Solve a trait goal using Chalk.
123pub(crate) fn trait_solve_query( 72pub(crate) fn trait_solve_query(
124 db: &dyn HirDatabase, 73 db: &dyn HirDatabase,
@@ -130,6 +79,7 @@ pub(crate) fn trait_solve_query(
130 db.trait_data(it.hir_trait_id()).name.to_string() 79 db.trait_data(it.hir_trait_id()).name.to_string()
131 } 80 }
132 DomainGoal::Holds(WhereClause::AliasEq(_)) => "alias_eq".to_string(), 81 DomainGoal::Holds(WhereClause::AliasEq(_)) => "alias_eq".to_string(),
82 _ => "??".to_string(),
133 }); 83 });
134 log::info!("trait_solve_query({})", goal.value.goal.display(db)); 84 log::info!("trait_solve_query({})", goal.value.goal.display(db));
135 85
@@ -138,19 +88,18 @@ pub(crate) fn trait_solve_query(
138 .. 88 ..
139 })) = &goal.value.goal 89 })) = &goal.value.goal
140 { 90 {
141 if let TyKind::BoundVar(_) = &projection_ty.substitution[0].interned(&Interner) { 91 if let TyKind::BoundVar(_) = projection_ty.self_type_parameter(&Interner).kind(&Interner) {
142 // Hack: don't ask Chalk to normalize with an unknown self type, it'll say that's impossible 92 // Hack: don't ask Chalk to normalize with an unknown self type, it'll say that's impossible
143 return Some(Solution::Ambig(Guidance::Unknown)); 93 return Some(Solution::Ambig(Guidance::Unknown));
144 } 94 }
145 } 95 }
146 96
147 let canonical = goal.to_chalk(db).cast(&Interner); 97 let canonical = goal.cast(&Interner);
148 98
149 // We currently don't deal with universes (I think / hope they're not yet 99 // We currently don't deal with universes (I think / hope they're not yet
150 // relevant for our use cases?) 100 // relevant for our use cases?)
151 let u_canonical = chalk_ir::UCanonical { canonical, universes: 1 }; 101 let u_canonical = chalk_ir::UCanonical { canonical, universes: 1 };
152 let solution = solve(db, krate, &u_canonical); 102 solve(db, krate, &u_canonical)
153 solution.map(|solution| solution_from_chalk(db, solution))
154} 103}
155 104
156fn solve( 105fn solve(
@@ -197,7 +146,7 @@ fn solve(
197 // don't set the TLS for Chalk unless Chalk debugging is active, to make 146 // don't set the TLS for Chalk unless Chalk debugging is active, to make
198 // extra sure we only use it for debugging 147 // extra sure we only use it for debugging
199 let solution = 148 let solution =
200 if is_chalk_debug() { chalk::tls::set_current_program(db, solve) } else { solve() }; 149 if is_chalk_debug() { crate::tls::set_current_program(db, solve) } else { solve() };
201 150
202 solution 151 solution
203} 152}
@@ -218,69 +167,6 @@ fn is_chalk_print() -> bool {
218 std::env::var("CHALK_PRINT").is_ok() 167 std::env::var("CHALK_PRINT").is_ok()
219} 168}
220 169
221fn solution_from_chalk(
222 db: &dyn HirDatabase,
223 solution: chalk_solve::Solution<Interner>,
224) -> Solution {
225 let convert_subst = |subst: chalk_ir::Canonical<chalk_ir::Substitution<Interner>>| {
226 let result = from_chalk(db, subst);
227 SolutionVariables(result)
228 };
229 match solution {
230 chalk_solve::Solution::Unique(constr_subst) => {
231 let subst = chalk_ir::Canonical {
232 value: constr_subst.value.subst,
233 binders: constr_subst.binders,
234 };
235 Solution::Unique(convert_subst(subst))
236 }
237 chalk_solve::Solution::Ambig(chalk_solve::Guidance::Definite(subst)) => {
238 Solution::Ambig(Guidance::Definite(convert_subst(subst)))
239 }
240 chalk_solve::Solution::Ambig(chalk_solve::Guidance::Suggested(subst)) => {
241 Solution::Ambig(Guidance::Suggested(convert_subst(subst)))
242 }
243 chalk_solve::Solution::Ambig(chalk_solve::Guidance::Unknown) => {
244 Solution::Ambig(Guidance::Unknown)
245 }
246 }
247}
248
249#[derive(Clone, Debug, PartialEq, Eq)]
250pub struct SolutionVariables(pub Canonical<Substitution>);
251
252#[derive(Clone, Debug, PartialEq, Eq)]
253/// A (possible) solution for a proposed goal.
254pub enum Solution {
255 /// The goal indeed holds, and there is a unique value for all existential
256 /// variables.
257 Unique(SolutionVariables),
258
259 /// The goal may be provable in multiple ways, but regardless we may have some guidance
260 /// for type inference. In this case, we don't return any lifetime
261 /// constraints, since we have not "committed" to any particular solution
262 /// yet.
263 Ambig(Guidance),
264}
265
266#[derive(Clone, Debug, PartialEq, Eq)]
267/// When a goal holds ambiguously (e.g., because there are multiple possible
268/// solutions), we issue a set of *guidance* back to type inference.
269pub enum Guidance {
270 /// The existential variables *must* have the given values if the goal is
271 /// ever to hold, but that alone isn't enough to guarantee the goal will
272 /// actually hold.
273 Definite(SolutionVariables),
274
275 /// There are multiple plausible values for the existentials, but the ones
276 /// here are suggested as the preferred choice heuristically. These should
277 /// be used for inference fallback only.
278 Suggested(SolutionVariables),
279
280 /// There's no useful information to feed back to type inference
281 Unknown,
282}
283
284#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)] 170#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
285pub enum FnTrait { 171pub enum FnTrait {
286 FnOnce, 172 FnOnce,