diff options
author | Florian Diebold <[email protected]> | 2021-05-16 14:50:28 +0100 |
---|---|---|
committer | Florian Diebold <[email protected]> | 2021-05-21 16:48:34 +0100 |
commit | 1250ddc5cf58ff0a6bbf7c07e5bd9f7cc7db5a09 (patch) | |
tree | 51c6ed040c2b1ec6b33321501ced866d87701c71 /crates/hir_ty/src/infer | |
parent | a3d9cac69057db700c4f6e01b84dc59529ea6dfd (diff) |
Rework obligation handling
We can't do the easy hack that we did before anymore, where we kept
track of whether any inference variables changed since the last time we
rechecked obligations. Instead, we store the obligations in
canonicalized form; that way we can easily check the inference variables
to see whether they have changed since the goal was canonicalized.
Diffstat (limited to 'crates/hir_ty/src/infer')
-rw-r--r-- | crates/hir_ty/src/infer/coerce.rs | 7 | ||||
-rw-r--r-- | crates/hir_ty/src/infer/expr.rs | 6 | ||||
-rw-r--r-- | crates/hir_ty/src/infer/path.rs | 2 | ||||
-rw-r--r-- | crates/hir_ty/src/infer/unify.rs | 173 |
4 files changed, 157 insertions, 31 deletions
diff --git a/crates/hir_ty/src/infer/coerce.rs b/crates/hir_ty/src/infer/coerce.rs index 4d80b4a08..911343cb9 100644 --- a/crates/hir_ty/src/infer/coerce.rs +++ b/crates/hir_ty/src/infer/coerce.rs | |||
@@ -402,12 +402,15 @@ impl<'a> InferenceContext<'a> { | |||
402 | // solve `CoerceUnsized` and `Unsize` goals at this point and leaves the | 402 | // solve `CoerceUnsized` and `Unsize` goals at this point and leaves the |
403 | // rest for later. Also, there's some logic about sized type variables. | 403 | // rest for later. Also, there's some logic about sized type variables. |
404 | // Need to find out in what cases this is necessary | 404 | // Need to find out in what cases this is necessary |
405 | let solution = self.db.trait_solve(krate, canonicalized.value.clone()).ok_or(TypeError)?; | 405 | let solution = self |
406 | .db | ||
407 | .trait_solve(krate, canonicalized.value.clone().cast(&Interner)) | ||
408 | .ok_or(TypeError)?; | ||
406 | 409 | ||
407 | match solution { | 410 | match solution { |
408 | Solution::Unique(v) => { | 411 | Solution::Unique(v) => { |
409 | canonicalized.apply_solution( | 412 | canonicalized.apply_solution( |
410 | self, | 413 | &mut self.table, |
411 | Canonical { | 414 | Canonical { |
412 | binders: v.binders, | 415 | binders: v.binders, |
413 | // FIXME handle constraints | 416 | // FIXME handle constraints |
diff --git a/crates/hir_ty/src/infer/expr.rs b/crates/hir_ty/src/infer/expr.rs index f439169ea..6eaccd9b4 100644 --- a/crates/hir_ty/src/infer/expr.rs +++ b/crates/hir_ty/src/infer/expr.rs | |||
@@ -99,9 +99,9 @@ impl<'a> InferenceContext<'a> { | |||
99 | environment: trait_env, | 99 | environment: trait_env, |
100 | }; | 100 | }; |
101 | let canonical = self.canonicalize(obligation.clone()); | 101 | let canonical = self.canonicalize(obligation.clone()); |
102 | if self.db.trait_solve(krate, canonical.value).is_some() { | 102 | if self.db.trait_solve(krate, canonical.value.cast(&Interner)).is_some() { |
103 | self.push_obligation(obligation.goal); | 103 | self.push_obligation(obligation.goal); |
104 | let return_ty = self.normalize_projection_ty(projection); | 104 | let return_ty = self.table.normalize_projection_ty(projection); |
105 | Some((arg_tys, return_ty)) | 105 | Some((arg_tys, return_ty)) |
106 | } else { | 106 | } else { |
107 | None | 107 | None |
@@ -306,7 +306,7 @@ impl<'a> InferenceContext<'a> { | |||
306 | self.resolver.krate(), | 306 | self.resolver.krate(), |
307 | InEnvironment { | 307 | InEnvironment { |
308 | goal: canonicalized.value.clone(), | 308 | goal: canonicalized.value.clone(), |
309 | environment: self.trait_env.env.clone(), | 309 | environment: self.table.trait_env.env.clone(), |
310 | }, | 310 | }, |
311 | ); | 311 | ); |
312 | let (param_tys, ret_ty): (Vec<Ty>, Ty) = derefs | 312 | let (param_tys, ret_ty): (Vec<Ty>, Ty) = derefs |
diff --git a/crates/hir_ty/src/infer/path.rs b/crates/hir_ty/src/infer/path.rs index bc64b612b..fd366e121 100644 --- a/crates/hir_ty/src/infer/path.rs +++ b/crates/hir_ty/src/infer/path.rs | |||
@@ -225,7 +225,7 @@ impl<'a> InferenceContext<'a> { | |||
225 | method_resolution::iterate_method_candidates( | 225 | method_resolution::iterate_method_candidates( |
226 | &canonical_ty.value, | 226 | &canonical_ty.value, |
227 | self.db, | 227 | self.db, |
228 | self.trait_env.clone(), | 228 | self.table.trait_env.clone(), |
229 | krate, | 229 | krate, |
230 | &traits_in_scope, | 230 | &traits_in_scope, |
231 | None, | 231 | None, |
diff --git a/crates/hir_ty/src/infer/unify.rs b/crates/hir_ty/src/infer/unify.rs index 93cd54f0d..75e04e8b5 100644 --- a/crates/hir_ty/src/infer/unify.rs +++ b/crates/hir_ty/src/infer/unify.rs | |||
@@ -1,6 +1,6 @@ | |||
1 | //! Unification and canonicalization logic. | 1 | //! Unification and canonicalization logic. |
2 | 2 | ||
3 | use std::{borrow::Cow, fmt, sync::Arc}; | 3 | use std::{borrow::Cow, fmt, mem, sync::Arc}; |
4 | 4 | ||
5 | use chalk_ir::{ | 5 | use chalk_ir::{ |
6 | cast::Cast, fold::Fold, interner::HasInterner, zip::Zip, FloatTy, IntTy, TyVariableKind, | 6 | cast::Cast, fold::Fold, interner::HasInterner, zip::Zip, FloatTy, IntTy, TyVariableKind, |
@@ -11,8 +11,9 @@ use ena::unify::UnifyKey; | |||
11 | 11 | ||
12 | use super::{InferOk, InferResult, InferenceContext, TypeError}; | 12 | use super::{InferOk, InferResult, InferenceContext, TypeError}; |
13 | use crate::{ | 13 | use crate::{ |
14 | db::HirDatabase, fold_tys, static_lifetime, BoundVar, Canonical, DebruijnIndex, GenericArg, | 14 | db::HirDatabase, fold_tys, static_lifetime, AliasEq, AliasTy, BoundVar, Canonical, |
15 | InferenceVar, Interner, Scalar, Substitution, TraitEnvironment, Ty, TyKind, VariableKind, | 15 | DebruijnIndex, GenericArg, Goal, Guidance, InEnvironment, InferenceVar, Interner, ProjectionTy, |
16 | Scalar, Solution, Substitution, TraitEnvironment, Ty, TyKind, VariableKind, | ||
16 | }; | 17 | }; |
17 | 18 | ||
18 | impl<'a> InferenceContext<'a> { | 19 | impl<'a> InferenceContext<'a> { |
@@ -23,17 +24,11 @@ impl<'a> InferenceContext<'a> { | |||
23 | where | 24 | where |
24 | T::Result: HasInterner<Interner = Interner>, | 25 | T::Result: HasInterner<Interner = Interner>, |
25 | { | 26 | { |
26 | let result = self.table.var_unification_table.canonicalize(&Interner, t); | 27 | self.table.canonicalize(t) |
27 | let free_vars = result | ||
28 | .free_vars | ||
29 | .into_iter() | ||
30 | .map(|free_var| free_var.to_generic_arg(&Interner)) | ||
31 | .collect(); | ||
32 | Canonicalized { value: result.quantified, free_vars } | ||
33 | } | 28 | } |
34 | } | 29 | } |
35 | 30 | ||
36 | #[derive(Debug)] | 31 | #[derive(Debug, Clone)] |
37 | pub(super) struct Canonicalized<T> | 32 | pub(super) struct Canonicalized<T> |
38 | where | 33 | where |
39 | T: HasInterner<Interner = Interner>, | 34 | T: HasInterner<Interner = Interner>, |
@@ -49,22 +44,16 @@ impl<T: HasInterner<Interner = Interner>> Canonicalized<T> { | |||
49 | 44 | ||
50 | pub(super) fn apply_solution( | 45 | pub(super) fn apply_solution( |
51 | &self, | 46 | &self, |
52 | ctx: &mut InferenceContext<'_>, | 47 | ctx: &mut InferenceTable, |
53 | solution: Canonical<Substitution>, | 48 | solution: Canonical<Substitution>, |
54 | ) { | 49 | ) { |
55 | // the solution may contain new variables, which we need to convert to new inference vars | 50 | // the solution may contain new variables, which we need to convert to new inference vars |
56 | let new_vars = Substitution::from_iter( | 51 | let new_vars = Substitution::from_iter( |
57 | &Interner, | 52 | &Interner, |
58 | solution.binders.iter(&Interner).map(|k| match k.kind { | 53 | solution.binders.iter(&Interner).map(|k| match k.kind { |
59 | VariableKind::Ty(TyVariableKind::General) => { | 54 | VariableKind::Ty(TyVariableKind::General) => ctx.new_type_var().cast(&Interner), |
60 | ctx.table.new_type_var().cast(&Interner) | 55 | VariableKind::Ty(TyVariableKind::Integer) => ctx.new_integer_var().cast(&Interner), |
61 | } | 56 | VariableKind::Ty(TyVariableKind::Float) => ctx.new_float_var().cast(&Interner), |
62 | VariableKind::Ty(TyVariableKind::Integer) => { | ||
63 | ctx.table.new_integer_var().cast(&Interner) | ||
64 | } | ||
65 | VariableKind::Ty(TyVariableKind::Float) => { | ||
66 | ctx.table.new_float_var().cast(&Interner) | ||
67 | } | ||
68 | // Chalk can sometimes return new lifetime variables. We just use the static lifetime everywhere | 57 | // Chalk can sometimes return new lifetime variables. We just use the static lifetime everywhere |
69 | VariableKind::Lifetime => static_lifetime().cast(&Interner), | 58 | VariableKind::Lifetime => static_lifetime().cast(&Interner), |
70 | _ => panic!("const variable in solution"), | 59 | _ => panic!("const variable in solution"), |
@@ -76,9 +65,9 @@ impl<T: HasInterner<Interner = Interner>> Canonicalized<T> { | |||
76 | // eagerly replace projections in the type; we may be getting types | 65 | // eagerly replace projections in the type; we may be getting types |
77 | // e.g. from where clauses where this hasn't happened yet | 66 | // e.g. from where clauses where this hasn't happened yet |
78 | let ty = ctx.normalize_associated_types_in(new_vars.apply(ty.clone(), &Interner)); | 67 | let ty = ctx.normalize_associated_types_in(new_vars.apply(ty.clone(), &Interner)); |
79 | ctx.table.unify(var.assert_ty_ref(&Interner), &ty); | 68 | ctx.unify(var.assert_ty_ref(&Interner), &ty); |
80 | } else { | 69 | } else { |
81 | let _ = ctx.table.unify_inner(&var, &new_vars.apply(v.clone(), &Interner)); | 70 | let _ = ctx.unify_inner(&var, &new_vars.apply(v.clone(), &Interner)); |
82 | } | 71 | } |
83 | } | 72 | } |
84 | } | 73 | } |
@@ -167,10 +156,11 @@ type ChalkInferenceTable = chalk_solve::infer::InferenceTable<Interner>; | |||
167 | 156 | ||
168 | #[derive(Clone)] | 157 | #[derive(Clone)] |
169 | pub(crate) struct InferenceTable<'a> { | 158 | pub(crate) struct InferenceTable<'a> { |
170 | db: &'a dyn HirDatabase, | 159 | pub db: &'a dyn HirDatabase, |
171 | trait_env: Arc<TraitEnvironment>, | 160 | pub trait_env: Arc<TraitEnvironment>, |
172 | pub(super) var_unification_table: ChalkInferenceTable, | 161 | pub(super) var_unification_table: ChalkInferenceTable, |
173 | pub(super) type_variable_table: TypeVariableTable, | 162 | pub(super) type_variable_table: TypeVariableTable, |
163 | pending_obligations: Vec<Canonicalized<InEnvironment<Goal>>>, | ||
174 | } | 164 | } |
175 | 165 | ||
176 | impl<'a> InferenceTable<'a> { | 166 | impl<'a> InferenceTable<'a> { |
@@ -180,6 +170,7 @@ impl<'a> InferenceTable<'a> { | |||
180 | trait_env, | 170 | trait_env, |
181 | var_unification_table: ChalkInferenceTable::new(), | 171 | var_unification_table: ChalkInferenceTable::new(), |
182 | type_variable_table: TypeVariableTable { inner: Vec::new() }, | 172 | type_variable_table: TypeVariableTable { inner: Vec::new() }, |
173 | pending_obligations: Vec::new(), | ||
183 | } | 174 | } |
184 | } | 175 | } |
185 | 176 | ||
@@ -202,6 +193,50 @@ impl<'a> InferenceTable<'a> { | |||
202 | } | 193 | } |
203 | } | 194 | } |
204 | 195 | ||
196 | pub(super) fn canonicalize<T: Fold<Interner> + HasInterner<Interner = Interner>>( | ||
197 | &mut self, | ||
198 | t: T, | ||
199 | ) -> Canonicalized<T::Result> | ||
200 | where | ||
201 | T::Result: HasInterner<Interner = Interner>, | ||
202 | { | ||
203 | let result = self.var_unification_table.canonicalize(&Interner, t); | ||
204 | let free_vars = result | ||
205 | .free_vars | ||
206 | .into_iter() | ||
207 | .map(|free_var| free_var.to_generic_arg(&Interner)) | ||
208 | .collect(); | ||
209 | Canonicalized { value: result.quantified, free_vars } | ||
210 | } | ||
211 | |||
212 | /// Recurses through the given type, normalizing associated types mentioned | ||
213 | /// in it by replacing them by type variables and registering obligations to | ||
214 | /// resolve later. This should be done once for every type we get from some | ||
215 | /// type annotation (e.g. from a let type annotation, field type or function | ||
216 | /// call). `make_ty` handles this already, but e.g. for field types we need | ||
217 | /// to do it as well. | ||
218 | pub(super) fn normalize_associated_types_in(&mut self, ty: Ty) -> Ty { | ||
219 | let ty = self.resolve_ty_as_possible(ty); | ||
220 | fold_tys( | ||
221 | ty, | ||
222 | |ty, _| match ty.kind(&Interner) { | ||
223 | TyKind::Alias(AliasTy::Projection(proj_ty)) => { | ||
224 | self.normalize_projection_ty(proj_ty.clone()) | ||
225 | } | ||
226 | _ => ty, | ||
227 | }, | ||
228 | DebruijnIndex::INNERMOST, | ||
229 | ) | ||
230 | } | ||
231 | |||
232 | pub(super) fn normalize_projection_ty(&mut self, proj_ty: ProjectionTy) -> Ty { | ||
233 | let var = self.new_type_var(); | ||
234 | let alias_eq = AliasEq { alias: AliasTy::Projection(proj_ty), ty: var.clone() }; | ||
235 | let obligation = alias_eq.cast(&Interner); | ||
236 | self.register_obligation(obligation); | ||
237 | var | ||
238 | } | ||
239 | |||
205 | fn new_var(&mut self, kind: TyVariableKind, diverging: bool) -> Ty { | 240 | fn new_var(&mut self, kind: TyVariableKind, diverging: bool) -> Ty { |
206 | let var = self.var_unification_table.new_variable(UniverseIndex::ROOT); | 241 | let var = self.var_unification_table.new_variable(UniverseIndex::ROOT); |
207 | // Chalk might have created some type variables for its own purposes that we don't know about... | 242 | // Chalk might have created some type variables for its own purposes that we don't know about... |
@@ -341,6 +376,94 @@ impl<'a> InferenceTable<'a> { | |||
341 | DebruijnIndex::INNERMOST, | 376 | DebruijnIndex::INNERMOST, |
342 | ) | 377 | ) |
343 | } | 378 | } |
379 | |||
380 | pub fn register_obligation(&mut self, goal: Goal) { | ||
381 | let in_env = InEnvironment::new(&self.trait_env.env, goal); | ||
382 | self.register_obligation_in_env(in_env) | ||
383 | } | ||
384 | |||
385 | fn register_obligation_in_env(&mut self, goal: InEnvironment<Goal>) { | ||
386 | let canonicalized = self.canonicalize(goal); | ||
387 | if !self.try_resolve_obligation(&canonicalized) { | ||
388 | self.pending_obligations.push(canonicalized); | ||
389 | } | ||
390 | } | ||
391 | |||
392 | pub fn resolve_obligations_as_possible(&mut self) { | ||
393 | let _span = profile::span("resolve_obligations_as_possible"); | ||
394 | let mut changed = true; | ||
395 | let mut obligations = Vec::new(); | ||
396 | while changed { | ||
397 | changed = false; | ||
398 | mem::swap(&mut self.pending_obligations, &mut obligations); | ||
399 | for canonicalized in obligations.drain(..) { | ||
400 | if !self.check_changed(&canonicalized) { | ||
401 | self.pending_obligations.push(canonicalized); | ||
402 | continue; | ||
403 | } | ||
404 | changed = true; | ||
405 | let uncanonical = chalk_ir::Substitute::apply( | ||
406 | &canonicalized.free_vars, | ||
407 | canonicalized.value.value, | ||
408 | &Interner, | ||
409 | ); | ||
410 | self.register_obligation_in_env(uncanonical); | ||
411 | } | ||
412 | } | ||
413 | } | ||
414 | |||
415 | /// This checks whether any of the free variables in the `canonicalized` | ||
416 | /// have changed (either been unified with another variable, or with a | ||
417 | /// value). If this is not the case, we don't need to try to solve the goal | ||
418 | /// again -- it'll give the same result as last time. | ||
419 | fn check_changed(&mut self, canonicalized: &Canonicalized<InEnvironment<Goal>>) -> bool { | ||
420 | canonicalized.free_vars.iter().any(|var| { | ||
421 | let iv = match var.data(&Interner) { | ||
422 | chalk_ir::GenericArgData::Ty(ty) => ty.inference_var(&Interner), | ||
423 | chalk_ir::GenericArgData::Lifetime(lt) => lt.inference_var(&Interner), | ||
424 | chalk_ir::GenericArgData::Const(c) => c.inference_var(&Interner), | ||
425 | } | ||
426 | .expect("free var is not inference var"); | ||
427 | if self.var_unification_table.probe_var(iv).is_some() { | ||
428 | return true; | ||
429 | } | ||
430 | let root = self.var_unification_table.inference_var_root(iv); | ||
431 | iv != root | ||
432 | }) | ||
433 | } | ||
434 | |||
435 | fn try_resolve_obligation( | ||
436 | &mut self, | ||
437 | canonicalized: &Canonicalized<InEnvironment<Goal>>, | ||
438 | ) -> bool { | ||
439 | let solution = self.db.trait_solve(self.trait_env.krate, canonicalized.value.clone()); | ||
440 | |||
441 | match solution { | ||
442 | Some(Solution::Unique(canonical_subst)) => { | ||
443 | canonicalized.apply_solution( | ||
444 | self, | ||
445 | Canonical { | ||
446 | binders: canonical_subst.binders, | ||
447 | // FIXME: handle constraints | ||
448 | value: canonical_subst.value.subst, | ||
449 | }, | ||
450 | ); | ||
451 | true | ||
452 | } | ||
453 | Some(Solution::Ambig(Guidance::Definite(substs))) => { | ||
454 | canonicalized.apply_solution(self, substs); | ||
455 | false | ||
456 | } | ||
457 | Some(_) => { | ||
458 | // FIXME use this when trying to resolve everything at the end | ||
459 | false | ||
460 | } | ||
461 | None => { | ||
462 | // FIXME obligation cannot be fulfilled => diagnostic | ||
463 | true | ||
464 | } | ||
465 | } | ||
466 | } | ||
344 | } | 467 | } |
345 | 468 | ||
346 | impl<'a> fmt::Debug for InferenceTable<'a> { | 469 | impl<'a> fmt::Debug for InferenceTable<'a> { |