1 //! Unification and canonicalization logic.
3 use std::{fmt, mem, sync::Arc};
6 cast::Cast, fold::Fold, interner::HasInterner, zip::Zip, FloatTy, IntTy, TyVariableKind,
9 use chalk_solve::infer::ParameterEnaVariableExt;
10 use ena::unify::UnifyKey;
12 use super::{InferOk, InferResult, InferenceContext, TypeError};
14 db::HirDatabase, fold_tys, static_lifetime, AliasEq, AliasTy, BoundVar, Canonical, Const,
15 DebruijnIndex, GenericArg, Goal, Guidance, InEnvironment, InferenceVar, Interner, Lifetime,
16 ProjectionTy, Scalar, Solution, Substitution, TraitEnvironment, Ty, TyKind, VariableKind,
19 impl<'a> InferenceContext<'a> {
20 pub(super) fn canonicalize<T: Fold<Interner> + HasInterner<Interner = Interner>>(
23 ) -> Canonicalized<T::Result>
25 T::Result: HasInterner<Interner = Interner>,
27 // try to resolve obligations before canonicalizing, since this might
28 // result in new knowledge about variables
29 self.resolve_obligations_as_possible();
30 self.table.canonicalize(t)
34 #[derive(Debug, Clone)]
35 pub(super) struct Canonicalized<T>
37 T: HasInterner<Interner = Interner>,
39 pub(super) value: Canonical<T>,
40 free_vars: Vec<GenericArg>,
43 impl<T: HasInterner<Interner = Interner>> Canonicalized<T> {
44 /// this method is wrong and shouldn't exist
45 pub(super) fn decanonicalize_ty(&self, table: &mut InferenceTable, ty: Canonical<Ty>) -> Ty {
46 let mut vars = self.free_vars.clone();
47 while ty.binders.len(&Interner) > vars.len() {
48 vars.push(table.new_type_var().cast(&Interner));
50 chalk_ir::Substitute::apply(&vars, ty.value, &Interner)
53 pub(super) fn apply_solution(
55 ctx: &mut InferenceTable,
56 solution: Canonical<Substitution>,
58 // the solution may contain new variables, which we need to convert to new inference vars
59 let new_vars = Substitution::from_iter(
61 solution.binders.iter(&Interner).map(|k| match k.kind {
62 VariableKind::Ty(TyVariableKind::General) => ctx.new_type_var().cast(&Interner),
63 VariableKind::Ty(TyVariableKind::Integer) => ctx.new_integer_var().cast(&Interner),
64 VariableKind::Ty(TyVariableKind::Float) => ctx.new_float_var().cast(&Interner),
65 // Chalk can sometimes return new lifetime variables. We just use the static lifetime everywhere
66 VariableKind::Lifetime => static_lifetime().cast(&Interner),
67 _ => panic!("const variable in solution"),
70 for (i, v) in solution.value.iter(&Interner).enumerate() {
71 let var = self.free_vars[i].clone();
72 if let Some(ty) = v.ty(&Interner) {
73 // eagerly replace projections in the type; we may be getting types
74 // e.g. from where clauses where this hasn't happened yet
75 let ty = ctx.normalize_associated_types_in(new_vars.apply(ty.clone(), &Interner));
76 ctx.unify(var.assert_ty_ref(&Interner), &ty);
78 let _ = ctx.try_unify(&var, &new_vars.apply(v.clone(), &Interner));
86 env: Arc<TraitEnvironment>,
87 tys: &Canonical<(Ty, Ty)>,
89 unify(db, env, tys).is_some()
94 env: Arc<TraitEnvironment>,
95 tys: &Canonical<(Ty, Ty)>,
96 ) -> Option<Substitution> {
97 let mut table = InferenceTable::new(db, env);
98 let vars = Substitution::from_iter(
102 // we always use type vars here because we want everything to
103 // fallback to Unknown in the end (kind of hacky, as below)
104 .map(|_| table.new_type_var()),
106 let ty1_with_vars = vars.apply(tys.value.0.clone(), &Interner);
107 let ty2_with_vars = vars.apply(tys.value.1.clone(), &Interner);
108 if !table.unify(&ty1_with_vars, &ty2_with_vars) {
111 // default any type vars that weren't unified back to their original bound vars
113 let find_var = |iv| {
114 vars.iter(&Interner).position(|v| match v.interned() {
115 chalk_ir::GenericArgData::Ty(ty) => ty.inference_var(&Interner),
116 chalk_ir::GenericArgData::Lifetime(lt) => lt.inference_var(&Interner),
117 chalk_ir::GenericArgData::Const(c) => c.inference_var(&Interner),
120 let fallback = |iv, kind, default, binder| match kind {
121 chalk_ir::VariableKind::Ty(_ty_kind) => find_var(iv)
122 .map_or(default, |i| BoundVar::new(binder, i).to_ty(&Interner).cast(&Interner)),
123 chalk_ir::VariableKind::Lifetime => find_var(iv)
124 .map_or(default, |i| BoundVar::new(binder, i).to_lifetime(&Interner).cast(&Interner)),
125 chalk_ir::VariableKind::Const(ty) => find_var(iv)
126 .map_or(default, |i| BoundVar::new(binder, i).to_const(&Interner, ty).cast(&Interner)),
128 Some(Substitution::from_iter(
131 .map(|v| table.resolve_with_fallback(v.assert_ty_ref(&Interner).clone(), fallback)),
135 #[derive(Copy, Clone, Debug)]
136 pub(crate) struct TypeVariableData {
140 type ChalkInferenceTable = chalk_solve::infer::InferenceTable<Interner>;
143 pub(crate) struct InferenceTable<'a> {
144 pub(crate) db: &'a dyn HirDatabase,
145 pub(crate) trait_env: Arc<TraitEnvironment>,
146 var_unification_table: ChalkInferenceTable,
147 type_variable_table: Vec<TypeVariableData>,
148 pending_obligations: Vec<Canonicalized<InEnvironment<Goal>>>,
151 pub(crate) struct InferenceTableSnapshot {
152 var_table_snapshot: chalk_solve::infer::InferenceSnapshot<Interner>,
153 // FIXME: snapshot type_variable_table, pending_obligations?
156 impl<'a> InferenceTable<'a> {
157 pub(crate) fn new(db: &'a dyn HirDatabase, trait_env: Arc<TraitEnvironment>) -> Self {
161 var_unification_table: ChalkInferenceTable::new(),
162 type_variable_table: Vec::new(),
163 pending_obligations: Vec::new(),
167 /// Chalk doesn't know about the `diverging` flag, so when it unifies two
168 /// type variables of which one is diverging, the chosen root might not be
169 /// diverging and we have no way of marking it as such at that time. This
170 /// function goes through all type variables and make sure their root is
171 /// marked as diverging if necessary, so that resolving them gives the right
173 pub(super) fn propagate_diverging_flag(&mut self) {
174 for i in 0..self.type_variable_table.len() {
175 if !self.type_variable_table[i].diverging {
178 let v = InferenceVar::from(i as u32);
179 let root = self.var_unification_table.inference_var_root(v);
180 if let Some(data) = self.type_variable_table.get_mut(root.index() as usize) {
181 data.diverging = true;
186 pub(super) fn set_diverging(&mut self, iv: InferenceVar, diverging: bool) {
187 self.type_variable_table[iv.index() as usize].diverging = diverging;
190 fn fallback_value(&self, iv: InferenceVar, kind: TyVariableKind) -> Ty {
194 .get(iv.index() as usize)
195 .map_or(false, |data| data.diverging) =>
199 TyVariableKind::General => TyKind::Error,
200 TyVariableKind::Integer => TyKind::Scalar(Scalar::Int(IntTy::I32)),
201 TyVariableKind::Float => TyKind::Scalar(Scalar::Float(FloatTy::F64)),
206 pub(super) fn canonicalize<T: Fold<Interner> + HasInterner<Interner = Interner>>(
209 ) -> Canonicalized<T::Result>
211 T::Result: HasInterner<Interner = Interner>,
213 let result = self.var_unification_table.canonicalize(&Interner, t);
214 let free_vars = result
217 .map(|free_var| free_var.to_generic_arg(&Interner))
219 Canonicalized { value: result.quantified, free_vars }
222 /// Recurses through the given type, normalizing associated types mentioned
223 /// in it by replacing them by type variables and registering obligations to
224 /// resolve later. This should be done once for every type we get from some
225 /// type annotation (e.g. from a let type annotation, field type or function
226 /// call). `make_ty` handles this already, but e.g. for field types we need
227 /// to do it as well.
228 pub(super) fn normalize_associated_types_in(&mut self, ty: Ty) -> Ty {
231 |ty, _| match ty.kind(&Interner) {
232 TyKind::Alias(AliasTy::Projection(proj_ty)) => {
233 self.normalize_projection_ty(proj_ty.clone())
237 DebruijnIndex::INNERMOST,
241 pub(super) fn normalize_projection_ty(&mut self, proj_ty: ProjectionTy) -> Ty {
242 let var = self.new_type_var();
243 let alias_eq = AliasEq { alias: AliasTy::Projection(proj_ty), ty: var.clone() };
244 let obligation = alias_eq.cast(&Interner);
245 self.register_obligation(obligation);
249 fn extend_type_variable_table(&mut self, to_index: usize) {
250 self.type_variable_table.extend(
251 (0..1 + to_index - self.type_variable_table.len())
252 .map(|_| TypeVariableData { diverging: false }),
256 fn new_var(&mut self, kind: TyVariableKind, diverging: bool) -> Ty {
257 let var = self.var_unification_table.new_variable(UniverseIndex::ROOT);
258 // Chalk might have created some type variables for its own purposes that we don't know about...
259 self.extend_type_variable_table(var.index() as usize);
260 assert_eq!(var.index() as usize, self.type_variable_table.len() - 1);
261 self.type_variable_table[var.index() as usize].diverging = diverging;
262 var.to_ty_with_kind(&Interner, kind)
265 pub(crate) fn new_type_var(&mut self) -> Ty {
266 self.new_var(TyVariableKind::General, false)
269 pub(crate) fn new_integer_var(&mut self) -> Ty {
270 self.new_var(TyVariableKind::Integer, false)
273 pub(crate) fn new_float_var(&mut self) -> Ty {
274 self.new_var(TyVariableKind::Float, false)
277 pub(crate) fn new_maybe_never_var(&mut self) -> Ty {
278 self.new_var(TyVariableKind::General, true)
281 pub(crate) fn new_const_var(&mut self, ty: Ty) -> Const {
282 let var = self.var_unification_table.new_variable(UniverseIndex::ROOT);
283 var.to_const(&Interner, ty)
286 pub(crate) fn new_lifetime_var(&mut self) -> Lifetime {
287 let var = self.var_unification_table.new_variable(UniverseIndex::ROOT);
288 var.to_lifetime(&Interner)
291 pub(crate) fn resolve_with_fallback<T>(
294 fallback: impl Fn(InferenceVar, VariableKind, GenericArg, DebruijnIndex) -> GenericArg,
297 T: HasInterner<Interner = Interner> + Fold<Interner>,
299 self.resolve_with_fallback_inner(&mut Vec::new(), t, &fallback)
302 fn resolve_with_fallback_inner<T>(
304 var_stack: &mut Vec<InferenceVar>,
306 fallback: &impl Fn(InferenceVar, VariableKind, GenericArg, DebruijnIndex) -> GenericArg,
309 T: HasInterner<Interner = Interner> + Fold<Interner>,
312 &mut resolve::Resolver { table: self, var_stack, fallback },
313 DebruijnIndex::INNERMOST,
315 .expect("fold failed unexpectedly")
318 pub(crate) fn resolve_completely<T>(&mut self, t: T) -> T::Result
320 T: HasInterner<Interner = Interner> + Fold<Interner>,
322 self.resolve_with_fallback(t, |_, _, d, _| d)
325 /// Unify two types and register new trait goals that arise from that.
326 pub(crate) fn unify(&mut self, ty1: &Ty, ty2: &Ty) -> bool {
327 let result = if let Ok(r) = self.try_unify(ty1, ty2) {
332 self.register_infer_ok(result);
336 /// Unify two types and return new trait goals arising from it, so the
337 /// caller needs to deal with them.
338 pub(crate) fn try_unify<T: Zip<Interner>>(&mut self, t1: &T, t2: &T) -> InferResult<()> {
339 match self.var_unification_table.relate(
343 chalk_ir::Variance::Invariant,
347 Ok(result) => Ok(InferOk { goals: result.goals, value: () }),
348 Err(chalk_ir::NoSolution) => Err(TypeError),
352 /// If `ty` is a type variable with known type, returns that type;
353 /// otherwise, return ty.
354 pub(crate) fn resolve_ty_shallow(&mut self, ty: &Ty) -> Ty {
355 self.var_unification_table.normalize_ty_shallow(&Interner, ty).unwrap_or_else(|| ty.clone())
358 pub(crate) fn snapshot(&mut self) -> InferenceTableSnapshot {
359 let snapshot = self.var_unification_table.snapshot();
360 InferenceTableSnapshot { var_table_snapshot: snapshot }
363 pub(crate) fn rollback_to(&mut self, snapshot: InferenceTableSnapshot) {
364 self.var_unification_table.rollback_to(snapshot.var_table_snapshot);
367 pub(crate) fn register_obligation(&mut self, goal: Goal) {
368 let in_env = InEnvironment::new(&self.trait_env.env, goal);
369 self.register_obligation_in_env(in_env)
372 fn register_obligation_in_env(&mut self, goal: InEnvironment<Goal>) {
373 let canonicalized = self.canonicalize(goal);
374 if !self.try_resolve_obligation(&canonicalized) {
375 self.pending_obligations.push(canonicalized);
379 pub(crate) fn register_infer_ok<T>(&mut self, infer_ok: InferOk<T>) {
380 infer_ok.goals.into_iter().for_each(|goal| self.register_obligation_in_env(goal));
383 pub(crate) fn resolve_obligations_as_possible(&mut self) {
384 let _span = profile::span("resolve_obligations_as_possible");
385 let mut changed = true;
386 let mut obligations = Vec::new();
389 mem::swap(&mut self.pending_obligations, &mut obligations);
390 for canonicalized in obligations.drain(..) {
391 if !self.check_changed(&canonicalized) {
392 self.pending_obligations.push(canonicalized);
396 let uncanonical = chalk_ir::Substitute::apply(
397 &canonicalized.free_vars,
398 canonicalized.value.value,
401 self.register_obligation_in_env(uncanonical);
406 pub(crate) fn fudge_inference<T: Fold<Interner>>(
408 f: impl FnOnce(&mut Self) -> T,
410 use chalk_ir::fold::Folder;
411 struct VarFudger<'a, 'b> {
412 table: &'a mut InferenceTable<'b>,
413 highest_known_var: InferenceVar,
415 impl<'a, 'b> Folder<'static, Interner> for VarFudger<'a, 'b> {
416 fn as_dyn(&mut self) -> &mut dyn Folder<'static, Interner> {
420 fn interner(&self) -> &'static Interner {
424 fn fold_inference_ty(
426 var: chalk_ir::InferenceVar,
427 kind: TyVariableKind,
428 _outer_binder: chalk_ir::DebruijnIndex,
429 ) -> chalk_ir::Fallible<chalk_ir::Ty<Interner>> {
430 Ok(if var < self.highest_known_var {
431 var.to_ty(&Interner, kind)
433 self.table.new_type_var()
437 fn fold_inference_lifetime(
439 var: chalk_ir::InferenceVar,
440 _outer_binder: chalk_ir::DebruijnIndex,
441 ) -> chalk_ir::Fallible<chalk_ir::Lifetime<Interner>> {
442 Ok(if var < self.highest_known_var {
443 var.to_lifetime(&Interner)
445 self.table.new_lifetime_var()
449 fn fold_inference_const(
451 ty: chalk_ir::Ty<Interner>,
452 var: chalk_ir::InferenceVar,
453 _outer_binder: chalk_ir::DebruijnIndex,
454 ) -> chalk_ir::Fallible<chalk_ir::Const<Interner>> {
455 Ok(if var < self.highest_known_var {
456 var.to_const(&Interner, ty)
458 self.table.new_const_var(ty)
463 let snapshot = self.snapshot();
464 let highest_known_var =
465 self.new_type_var().inference_var(&Interner).expect("inference_var");
466 let result = f(self);
467 self.rollback_to(snapshot);
469 .fold_with(&mut VarFudger { table: self, highest_known_var }, DebruijnIndex::INNERMOST)
470 .expect("fold_with with VarFudger")
473 /// This checks whether any of the free variables in the `canonicalized`
474 /// have changed (either been unified with another variable, or with a
475 /// value). If this is not the case, we don't need to try to solve the goal
476 /// again -- it'll give the same result as last time.
477 fn check_changed(&mut self, canonicalized: &Canonicalized<InEnvironment<Goal>>) -> bool {
478 canonicalized.free_vars.iter().any(|var| {
479 let iv = match var.data(&Interner) {
480 chalk_ir::GenericArgData::Ty(ty) => ty.inference_var(&Interner),
481 chalk_ir::GenericArgData::Lifetime(lt) => lt.inference_var(&Interner),
482 chalk_ir::GenericArgData::Const(c) => c.inference_var(&Interner),
484 .expect("free var is not inference var");
485 if self.var_unification_table.probe_var(iv).is_some() {
488 let root = self.var_unification_table.inference_var_root(iv);
493 fn try_resolve_obligation(
495 canonicalized: &Canonicalized<InEnvironment<Goal>>,
497 let solution = self.db.trait_solve(self.trait_env.krate, canonicalized.value.clone());
500 Some(Solution::Unique(canonical_subst)) => {
501 canonicalized.apply_solution(
504 binders: canonical_subst.binders,
505 // FIXME: handle constraints
506 value: canonical_subst.value.subst,
511 Some(Solution::Ambig(Guidance::Definite(substs))) => {
512 canonicalized.apply_solution(self, substs);
516 // FIXME use this when trying to resolve everything at the end
520 // FIXME obligation cannot be fulfilled => diagnostic
527 impl<'a> fmt::Debug for InferenceTable<'a> {
528 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
529 f.debug_struct("InferenceTable").field("num_vars", &self.type_variable_table.len()).finish()
534 use super::InferenceTable;
536 ConcreteConst, Const, ConstData, ConstValue, DebruijnIndex, GenericArg, InferenceVar,
537 Interner, Lifetime, Ty, TyVariableKind, VariableKind,
541 fold::{Fold, Folder},
544 use hir_def::type_ref::ConstScalar;
546 pub(super) struct Resolver<'a, 'b, F> {
547 pub(super) table: &'a mut InferenceTable<'b>,
548 pub(super) var_stack: &'a mut Vec<InferenceVar>,
549 pub(super) fallback: F,
551 impl<'a, 'b, 'i, F> Folder<'i, Interner> for Resolver<'a, 'b, F>
553 F: Fn(InferenceVar, VariableKind, GenericArg, DebruijnIndex) -> GenericArg + 'i,
555 fn as_dyn(&mut self) -> &mut dyn Folder<'i, Interner> {
559 fn interner(&self) -> &'i Interner {
563 fn fold_inference_ty(
566 kind: TyVariableKind,
567 outer_binder: DebruijnIndex,
569 let var = self.table.var_unification_table.inference_var_root(var);
570 if self.var_stack.contains(&var) {
572 let default = self.table.fallback_value(var, kind).cast(&Interner);
573 return Ok((self.fallback)(var, VariableKind::Ty(kind), default, outer_binder)
574 .assert_ty_ref(&Interner)
577 let result = if let Some(known_ty) = self.table.var_unification_table.probe_var(var) {
578 // known_ty may contain other variables that are known by now
579 self.var_stack.push(var);
581 known_ty.fold_with(self, outer_binder).expect("fold failed unexpectedly");
582 self.var_stack.pop();
583 result.assert_ty_ref(&Interner).clone()
585 let default = self.table.fallback_value(var, kind).cast(&Interner);
586 (self.fallback)(var, VariableKind::Ty(kind), default, outer_binder)
587 .assert_ty_ref(&Interner)
593 fn fold_inference_const(
597 outer_binder: DebruijnIndex,
598 ) -> Fallible<Const> {
599 let var = self.table.var_unification_table.inference_var_root(var);
600 let default = ConstData {
602 value: ConstValue::Concrete(ConcreteConst { interned: ConstScalar::Unknown }),
606 if self.var_stack.contains(&var) {
608 return Ok((self.fallback)(var, VariableKind::Const(ty), default, outer_binder)
609 .assert_const_ref(&Interner)
612 let result = if let Some(known_ty) = self.table.var_unification_table.probe_var(var) {
613 // known_ty may contain other variables that are known by now
614 self.var_stack.push(var);
616 known_ty.fold_with(self, outer_binder).expect("fold failed unexpectedly");
617 self.var_stack.pop();
618 result.assert_const_ref(&Interner).clone()
620 (self.fallback)(var, VariableKind::Const(ty), default, outer_binder)
621 .assert_const_ref(&Interner)
627 fn fold_inference_lifetime(
630 _outer_binder: DebruijnIndex,
631 ) -> Fallible<Lifetime> {
632 // fall back all lifetimes to 'static -- currently we don't deal
633 // with any lifetimes, but we can sometimes get some lifetime
634 // variables through Chalk's unification, and this at least makes
635 // sure we don't leak them outside of inference
636 Ok(crate::static_lifetime())