aboutsummaryrefslogtreecommitdiff
path: root/crates/hir_ty/src/infer/unify.rs
diff options
context:
space:
mode:
Diffstat (limited to 'crates/hir_ty/src/infer/unify.rs')
-rw-r--r--crates/hir_ty/src/infer/unify.rs154
1 files changed, 92 insertions, 62 deletions
diff --git a/crates/hir_ty/src/infer/unify.rs b/crates/hir_ty/src/infer/unify.rs
index 75250a369..2ea9dd920 100644
--- a/crates/hir_ty/src/infer/unify.rs
+++ b/crates/hir_ty/src/infer/unify.rs
@@ -7,8 +7,9 @@ use ena::unify::{InPlaceUnificationTable, NoError, UnifyKey, UnifyValue};
7 7
8use super::{DomainGoal, InferenceContext}; 8use super::{DomainGoal, InferenceContext};
9use crate::{ 9use crate::{
10 AliasEq, AliasTy, BoundVar, Canonical, CanonicalVarKinds, DebruijnIndex, FnPointer, 10 AliasEq, AliasTy, BoundVar, Canonical, CanonicalVarKinds, DebruijnIndex, FnPointer, FnSubst,
11 InEnvironment, InferenceVar, Interner, Scalar, Substitution, Ty, TyKind, TypeWalk, WhereClause, 11 InEnvironment, InferenceVar, Interner, Scalar, Substitution, Ty, TyExt, TyKind, TypeWalk,
12 WhereClause,
12}; 13};
13 14
14impl<'a> InferenceContext<'a> { 15impl<'a> InferenceContext<'a> {
@@ -49,9 +50,9 @@ impl<'a, 'b> Canonicalizer<'a, 'b> {
49 50
50 fn do_canonicalize<T: TypeWalk>(&mut self, t: T, binders: DebruijnIndex) -> T { 51 fn do_canonicalize<T: TypeWalk>(&mut self, t: T, binders: DebruijnIndex) -> T {
51 t.fold_binders( 52 t.fold_binders(
52 &mut |ty, binders| match ty.interned(&Interner) { 53 &mut |ty, binders| match ty.kind(&Interner) {
53 &TyKind::InferenceVar(var, kind) => { 54 &TyKind::InferenceVar(var, kind) => {
54 let inner = var.to_inner(); 55 let inner = from_inference_var(var);
55 if self.var_stack.contains(&inner) { 56 if self.var_stack.contains(&inner) {
56 // recursive type 57 // recursive type
57 return self.ctx.table.type_variable_table.fallback_value(var, kind); 58 return self.ctx.table.type_variable_table.fallback_value(var, kind);
@@ -65,7 +66,7 @@ impl<'a, 'b> Canonicalizer<'a, 'b> {
65 result 66 result
66 } else { 67 } else {
67 let root = self.ctx.table.var_unification_table.find(inner); 68 let root = self.ctx.table.var_unification_table.find(inner);
68 let position = self.add(InferenceVar::from_inner(root), kind); 69 let position = self.add(to_inference_var(root), kind);
69 TyKind::BoundVar(BoundVar::new(binders, position)).intern(&Interner) 70 TyKind::BoundVar(BoundVar::new(binders, position)).intern(&Interner)
70 } 71 }
71 } 72 }
@@ -108,19 +109,22 @@ impl<'a, 'b> Canonicalizer<'a, 'b> {
108} 109}
109 110
110impl<T> Canonicalized<T> { 111impl<T> Canonicalized<T> {
111 pub(super) fn decanonicalize_ty(&self, mut ty: Ty) -> Ty { 112 pub(super) fn decanonicalize_ty(&self, ty: Ty) -> Ty {
112 ty.walk_mut_binders( 113 ty.fold_binders(
113 &mut |ty, binders| { 114 &mut |ty, binders| {
114 if let &mut TyKind::BoundVar(bound) = ty.interned_mut() { 115 if let TyKind::BoundVar(bound) = ty.kind(&Interner) {
115 if bound.debruijn >= binders { 116 if bound.debruijn >= binders {
116 let (v, k) = self.free_vars[bound.index]; 117 let (v, k) = self.free_vars[bound.index];
117 *ty = TyKind::InferenceVar(v, k).intern(&Interner); 118 TyKind::InferenceVar(v, k).intern(&Interner)
119 } else {
120 ty
118 } 121 }
122 } else {
123 ty
119 } 124 }
120 }, 125 },
121 DebruijnIndex::INNERMOST, 126 DebruijnIndex::INNERMOST,
122 ); 127 )
123 ty
124 } 128 }
125 129
126 pub(super) fn apply_solution( 130 pub(super) fn apply_solution(
@@ -129,52 +133,56 @@ impl<T> Canonicalized<T> {
129 solution: Canonical<Substitution>, 133 solution: Canonical<Substitution>,
130 ) { 134 ) {
131 // the solution may contain new variables, which we need to convert to new inference vars 135 // the solution may contain new variables, which we need to convert to new inference vars
132 let new_vars = Substitution( 136 let new_vars = Substitution::from_iter(
133 solution 137 &Interner,
134 .binders 138 solution.binders.iter(&Interner).map(|k| match k.kind {
135 .iter(&Interner) 139 VariableKind::Ty(TyVariableKind::General) => ctx.table.new_type_var(),
136 .map(|k| match k.kind { 140 VariableKind::Ty(TyVariableKind::Integer) => ctx.table.new_integer_var(),
137 VariableKind::Ty(TyVariableKind::General) => ctx.table.new_type_var(), 141 VariableKind::Ty(TyVariableKind::Float) => ctx.table.new_float_var(),
138 VariableKind::Ty(TyVariableKind::Integer) => ctx.table.new_integer_var(), 142 // HACK: Chalk can sometimes return new lifetime variables. We
139 VariableKind::Ty(TyVariableKind::Float) => ctx.table.new_float_var(), 143 // want to just skip them, but to not mess up the indices of
140 // HACK: Chalk can sometimes return new lifetime variables. We 144 // other variables, we'll just create a new type variable in
141 // want to just skip them, but to not mess up the indices of 145 // their place instead. This should not matter (we never see the
142 // other variables, we'll just create a new type variable in 146 // actual *uses* of the lifetime variable).
143 // their place instead. This should not matter (we never see the 147 VariableKind::Lifetime => ctx.table.new_type_var(),
144 // actual *uses* of the lifetime variable). 148 _ => panic!("const variable in solution"),
145 VariableKind::Lifetime => ctx.table.new_type_var(), 149 }),
146 _ => panic!("const variable in solution"),
147 })
148 .collect(),
149 ); 150 );
150 for (i, ty) in solution.value.into_iter().enumerate() { 151 for (i, ty) in solution.value.iter(&Interner).enumerate() {
151 let (v, k) = self.free_vars[i]; 152 let (v, k) = self.free_vars[i];
152 // eagerly replace projections in the type; we may be getting types 153 // eagerly replace projections in the type; we may be getting types
153 // e.g. from where clauses where this hasn't happened yet 154 // e.g. from where clauses where this hasn't happened yet
154 let ty = ctx.normalize_associated_types_in(ty.clone().subst_bound_vars(&new_vars)); 155 let ty = ctx.normalize_associated_types_in(
156 new_vars.apply(ty.assert_ty_ref(&Interner).clone(), &Interner),
157 );
155 ctx.table.unify(&TyKind::InferenceVar(v, k).intern(&Interner), &ty); 158 ctx.table.unify(&TyKind::InferenceVar(v, k).intern(&Interner), &ty);
156 } 159 }
157 } 160 }
158} 161}
159 162
163pub fn could_unify(t1: &Ty, t2: &Ty) -> bool {
164 InferenceTable::new().unify(t1, t2)
165}
166
160pub(crate) fn unify(tys: &Canonical<(Ty, Ty)>) -> Option<Substitution> { 167pub(crate) fn unify(tys: &Canonical<(Ty, Ty)>) -> Option<Substitution> {
161 let mut table = InferenceTable::new(); 168 let mut table = InferenceTable::new();
162 let vars = Substitution( 169 let vars = Substitution::from_iter(
170 &Interner,
163 tys.binders 171 tys.binders
164 .iter(&Interner) 172 .iter(&Interner)
165 // we always use type vars here because we want everything to 173 // we always use type vars here because we want everything to
166 // fallback to Unknown in the end (kind of hacky, as below) 174 // fallback to Unknown in the end (kind of hacky, as below)
167 .map(|_| table.new_type_var()) 175 .map(|_| table.new_type_var()),
168 .collect(),
169 ); 176 );
170 let ty1_with_vars = tys.value.0.clone().subst_bound_vars(&vars); 177 let ty1_with_vars = vars.apply(tys.value.0.clone(), &Interner);
171 let ty2_with_vars = tys.value.1.clone().subst_bound_vars(&vars); 178 let ty2_with_vars = vars.apply(tys.value.1.clone(), &Interner);
172 if !table.unify(&ty1_with_vars, &ty2_with_vars) { 179 if !table.unify(&ty1_with_vars, &ty2_with_vars) {
173 return None; 180 return None;
174 } 181 }
175 // default any type vars that weren't unified back to their original bound vars 182 // default any type vars that weren't unified back to their original bound vars
176 // (kind of hacky) 183 // (kind of hacky)
177 for (i, var) in vars.iter().enumerate() { 184 for (i, var) in vars.iter(&Interner).enumerate() {
185 let var = var.assert_ty_ref(&Interner);
178 if &*table.resolve_ty_shallow(var) == var { 186 if &*table.resolve_ty_shallow(var) == var {
179 table.unify( 187 table.unify(
180 var, 188 var,
@@ -182,11 +190,11 @@ pub(crate) fn unify(tys: &Canonical<(Ty, Ty)>) -> Option<Substitution> {
182 ); 190 );
183 } 191 }
184 } 192 }
185 Some( 193 Some(Substitution::from_iter(
186 Substitution::builder(tys.binders.len(&Interner)) 194 &Interner,
187 .fill(vars.iter().map(|v| table.resolve_ty_completely(v.clone()))) 195 vars.iter(&Interner)
188 .build(), 196 .map(|v| table.resolve_ty_completely(v.assert_ty_ref(&Interner).clone())),
189 ) 197 ))
190} 198}
191 199
192#[derive(Clone, Debug)] 200#[derive(Clone, Debug)]
@@ -200,17 +208,17 @@ impl TypeVariableTable {
200 } 208 }
201 209
202 pub(super) fn set_diverging(&mut self, iv: InferenceVar, diverging: bool) { 210 pub(super) fn set_diverging(&mut self, iv: InferenceVar, diverging: bool) {
203 self.inner[iv.to_inner().0 as usize].diverging = diverging; 211 self.inner[from_inference_var(iv).0 as usize].diverging = diverging;
204 } 212 }
205 213
206 fn is_diverging(&mut self, iv: InferenceVar) -> bool { 214 fn is_diverging(&mut self, iv: InferenceVar) -> bool {
207 self.inner[iv.to_inner().0 as usize].diverging 215 self.inner[from_inference_var(iv).0 as usize].diverging
208 } 216 }
209 217
210 fn fallback_value(&self, iv: InferenceVar, kind: TyVariableKind) -> Ty { 218 fn fallback_value(&self, iv: InferenceVar, kind: TyVariableKind) -> Ty {
211 match kind { 219 match kind {
212 _ if self.inner[iv.to_inner().0 as usize].diverging => TyKind::Never, 220 _ if self.inner[from_inference_var(iv).0 as usize].diverging => TyKind::Never,
213 TyVariableKind::General => TyKind::Unknown, 221 TyVariableKind::General => TyKind::Error,
214 TyVariableKind::Integer => TyKind::Scalar(Scalar::Int(IntTy::I32)), 222 TyVariableKind::Integer => TyKind::Scalar(Scalar::Int(IntTy::I32)),
215 TyVariableKind::Float => TyKind::Scalar(Scalar::Float(FloatTy::F64)), 223 TyVariableKind::Float => TyKind::Scalar(Scalar::Float(FloatTy::F64)),
216 } 224 }
@@ -227,6 +235,7 @@ pub(crate) struct TypeVariableData {
227pub(crate) struct InferenceTable { 235pub(crate) struct InferenceTable {
228 pub(super) var_unification_table: InPlaceUnificationTable<TypeVarId>, 236 pub(super) var_unification_table: InPlaceUnificationTable<TypeVarId>,
229 pub(super) type_variable_table: TypeVariableTable, 237 pub(super) type_variable_table: TypeVariableTable,
238 pub(super) revision: u32,
230} 239}
231 240
232impl InferenceTable { 241impl InferenceTable {
@@ -234,6 +243,7 @@ impl InferenceTable {
234 InferenceTable { 243 InferenceTable {
235 var_unification_table: InPlaceUnificationTable::new(), 244 var_unification_table: InPlaceUnificationTable::new(),
236 type_variable_table: TypeVariableTable { inner: Vec::new() }, 245 type_variable_table: TypeVariableTable { inner: Vec::new() },
246 revision: 0,
237 } 247 }
238 } 248 }
239 249
@@ -241,7 +251,7 @@ impl InferenceTable {
241 self.type_variable_table.push(TypeVariableData { diverging }); 251 self.type_variable_table.push(TypeVariableData { diverging });
242 let key = self.var_unification_table.new_key(TypeVarValue::Unknown); 252 let key = self.var_unification_table.new_key(TypeVarValue::Unknown);
243 assert_eq!(key.0 as usize, self.type_variable_table.inner.len() - 1); 253 assert_eq!(key.0 as usize, self.type_variable_table.inner.len() - 1);
244 TyKind::InferenceVar(InferenceVar::from_inner(key), kind).intern(&Interner) 254 TyKind::InferenceVar(to_inference_var(key), kind).intern(&Interner)
245 } 255 }
246 256
247 pub(crate) fn new_type_var(&mut self) -> Ty { 257 pub(crate) fn new_type_var(&mut self) -> Ty {
@@ -278,7 +288,9 @@ impl InferenceTable {
278 substs2: &Substitution, 288 substs2: &Substitution,
279 depth: usize, 289 depth: usize,
280 ) -> bool { 290 ) -> bool {
281 substs1.0.iter().zip(substs2.0.iter()).all(|(t1, t2)| self.unify_inner(t1, t2, depth)) 291 substs1.iter(&Interner).zip(substs2.iter(&Interner)).all(|(t1, t2)| {
292 self.unify_inner(t1.assert_ty_ref(&Interner), t2.assert_ty_ref(&Interner), depth)
293 })
282 } 294 }
283 295
284 fn unify_inner(&mut self, ty1: &Ty, ty2: &Ty, depth: usize) -> bool { 296 fn unify_inner(&mut self, ty1: &Ty, ty2: &Ty, depth: usize) -> bool {
@@ -293,12 +305,12 @@ impl InferenceTable {
293 let ty1 = self.resolve_ty_shallow(ty1); 305 let ty1 = self.resolve_ty_shallow(ty1);
294 let ty2 = self.resolve_ty_shallow(ty2); 306 let ty2 = self.resolve_ty_shallow(ty2);
295 if ty1.equals_ctor(&ty2) { 307 if ty1.equals_ctor(&ty2) {
296 match (ty1.interned(&Interner), ty2.interned(&Interner)) { 308 match (ty1.kind(&Interner), ty2.kind(&Interner)) {
297 (TyKind::Adt(_, substs1), TyKind::Adt(_, substs2)) 309 (TyKind::Adt(_, substs1), TyKind::Adt(_, substs2))
298 | (TyKind::FnDef(_, substs1), TyKind::FnDef(_, substs2)) 310 | (TyKind::FnDef(_, substs1), TyKind::FnDef(_, substs2))
299 | ( 311 | (
300 TyKind::Function(FnPointer { substs: substs1, .. }), 312 TyKind::Function(FnPointer { substitution: FnSubst(substs1), .. }),
301 TyKind::Function(FnPointer { substs: substs2, .. }), 313 TyKind::Function(FnPointer { substitution: FnSubst(substs2), .. }),
302 ) 314 )
303 | (TyKind::Tuple(_, substs1), TyKind::Tuple(_, substs2)) 315 | (TyKind::Tuple(_, substs1), TyKind::Tuple(_, substs2))
304 | (TyKind::OpaqueType(_, substs1), TyKind::OpaqueType(_, substs2)) 316 | (TyKind::OpaqueType(_, substs1), TyKind::OpaqueType(_, substs2))
@@ -306,9 +318,11 @@ impl InferenceTable {
306 | (TyKind::Closure(.., substs1), TyKind::Closure(.., substs2)) => { 318 | (TyKind::Closure(.., substs1), TyKind::Closure(.., substs2)) => {
307 self.unify_substs(substs1, substs2, depth + 1) 319 self.unify_substs(substs1, substs2, depth + 1)
308 } 320 }
309 (TyKind::Ref(_, ty1), TyKind::Ref(_, ty2)) 321 (TyKind::Array(ty1, c1), TyKind::Array(ty2, c2)) if c1 == c2 => {
322 self.unify_inner(ty1, ty2, depth + 1)
323 }
324 (TyKind::Ref(_, _, ty1), TyKind::Ref(_, _, ty2))
310 | (TyKind::Raw(_, ty1), TyKind::Raw(_, ty2)) 325 | (TyKind::Raw(_, ty1), TyKind::Raw(_, ty2))
311 | (TyKind::Array(ty1), TyKind::Array(ty2))
312 | (TyKind::Slice(ty1), TyKind::Slice(ty2)) => self.unify_inner(ty1, ty2, depth + 1), 326 | (TyKind::Slice(ty1), TyKind::Slice(ty2)) => self.unify_inner(ty1, ty2, depth + 1),
313 _ => true, /* we checked equals_ctor already */ 327 _ => true, /* we checked equals_ctor already */
314 } 328 }
@@ -318,8 +332,8 @@ impl InferenceTable {
318 } 332 }
319 333
320 pub(super) fn unify_inner_trivial(&mut self, ty1: &Ty, ty2: &Ty, depth: usize) -> bool { 334 pub(super) fn unify_inner_trivial(&mut self, ty1: &Ty, ty2: &Ty, depth: usize) -> bool {
321 match (ty1.interned(&Interner), ty2.interned(&Interner)) { 335 match (ty1.kind(&Interner), ty2.kind(&Interner)) {
322 (TyKind::Unknown, _) | (_, TyKind::Unknown) => true, 336 (TyKind::Error, _) | (_, TyKind::Error) => true,
323 337
324 (TyKind::Placeholder(p1), TyKind::Placeholder(p2)) if *p1 == *p2 => true, 338 (TyKind::Placeholder(p1), TyKind::Placeholder(p2)) if *p1 == *p2 => true,
325 339
@@ -356,7 +370,14 @@ impl InferenceTable {
356 == self.type_variable_table.is_diverging(*tv2) => 370 == self.type_variable_table.is_diverging(*tv2) =>
357 { 371 {
358 // both type vars are unknown since we tried to resolve them 372 // both type vars are unknown since we tried to resolve them
359 self.var_unification_table.union(tv1.to_inner(), tv2.to_inner()); 373 if !self
374 .var_unification_table
375 .unioned(from_inference_var(*tv1), from_inference_var(*tv2))
376 {
377 self.var_unification_table
378 .union(from_inference_var(*tv1), from_inference_var(*tv2));
379 self.revision += 1;
380 }
360 true 381 true
361 } 382 }
362 383
@@ -391,9 +412,10 @@ impl InferenceTable {
391 ) => { 412 ) => {
392 // the type var is unknown since we tried to resolve it 413 // the type var is unknown since we tried to resolve it
393 self.var_unification_table.union_value( 414 self.var_unification_table.union_value(
394 tv.to_inner(), 415 from_inference_var(*tv),
395 TypeVarValue::Known(other.clone().intern(&Interner)), 416 TypeVarValue::Known(other.clone().intern(&Interner)),
396 ); 417 );
418 self.revision += 1;
397 true 419 true
398 } 420 }
399 421
@@ -443,9 +465,9 @@ impl InferenceTable {
443 if i > 0 { 465 if i > 0 {
444 cov_mark::hit!(type_var_resolves_to_int_var); 466 cov_mark::hit!(type_var_resolves_to_int_var);
445 } 467 }
446 match ty.interned(&Interner) { 468 match ty.kind(&Interner) {
447 TyKind::InferenceVar(tv, _) => { 469 TyKind::InferenceVar(tv, _) => {
448 let inner = tv.to_inner(); 470 let inner = from_inference_var(*tv);
449 match self.var_unification_table.inlined_probe_value(inner).known() { 471 match self.var_unification_table.inlined_probe_value(inner).known() {
450 Some(known_ty) => { 472 Some(known_ty) => {
451 // The known_ty can't be a type var itself 473 // The known_ty can't be a type var itself
@@ -466,9 +488,9 @@ impl InferenceTable {
466 /// be resolved as far as possible, i.e. contain no type variables with 488 /// be resolved as far as possible, i.e. contain no type variables with
467 /// known type. 489 /// known type.
468 fn resolve_ty_as_possible_inner(&mut self, tv_stack: &mut Vec<TypeVarId>, ty: Ty) -> Ty { 490 fn resolve_ty_as_possible_inner(&mut self, tv_stack: &mut Vec<TypeVarId>, ty: Ty) -> Ty {
469 ty.fold(&mut |ty| match ty.interned(&Interner) { 491 ty.fold(&mut |ty| match ty.kind(&Interner) {
470 &TyKind::InferenceVar(tv, kind) => { 492 &TyKind::InferenceVar(tv, kind) => {
471 let inner = tv.to_inner(); 493 let inner = from_inference_var(tv);
472 if tv_stack.contains(&inner) { 494 if tv_stack.contains(&inner) {
473 cov_mark::hit!(type_var_cycles_resolve_as_possible); 495 cov_mark::hit!(type_var_cycles_resolve_as_possible);
474 // recursive type 496 // recursive type
@@ -493,9 +515,9 @@ impl InferenceTable {
493 /// Resolves the type completely; type variables without known type are 515 /// Resolves the type completely; type variables without known type are
494 /// replaced by TyKind::Unknown. 516 /// replaced by TyKind::Unknown.
495 fn resolve_ty_completely_inner(&mut self, tv_stack: &mut Vec<TypeVarId>, ty: Ty) -> Ty { 517 fn resolve_ty_completely_inner(&mut self, tv_stack: &mut Vec<TypeVarId>, ty: Ty) -> Ty {
496 ty.fold(&mut |ty| match ty.interned(&Interner) { 518 ty.fold(&mut |ty| match ty.kind(&Interner) {
497 &TyKind::InferenceVar(tv, kind) => { 519 &TyKind::InferenceVar(tv, kind) => {
498 let inner = tv.to_inner(); 520 let inner = from_inference_var(tv);
499 if tv_stack.contains(&inner) { 521 if tv_stack.contains(&inner) {
500 cov_mark::hit!(type_var_cycles_resolve_completely); 522 cov_mark::hit!(type_var_cycles_resolve_completely);
501 // recursive type 523 // recursive type
@@ -538,6 +560,14 @@ impl UnifyKey for TypeVarId {
538 } 560 }
539} 561}
540 562
563fn from_inference_var(var: InferenceVar) -> TypeVarId {
564 TypeVarId(var.index())
565}
566
567fn to_inference_var(TypeVarId(index): TypeVarId) -> InferenceVar {
568 index.into()
569}
570
541/// The value of a type variable: either we already know the type, or we don't 571/// The value of a type variable: either we already know the type, or we don't
542/// know it yet. 572/// know it yet.
543#[derive(Clone, PartialEq, Eq, Debug)] 573#[derive(Clone, PartialEq, Eq, Debug)]