vendor/chalk-solve-0.14.0/src/infer/unify.rs

   1 use super::var::*;
   2 use super::*;
   3 use crate::debug_span;
   4 use crate::infer::instantiate::IntoBindersAndValue;
   5 use chalk_ir::cast::Cast;
   6 use chalk_ir::fold::{Fold, Folder};
   7 use chalk_ir::interner::{HasInterner, Interner};
   8 use chalk_ir::zip::{Zip, Zipper};
   9 use std::fmt::Debug;
  10
  11 impl<I: Interner> InferenceTable<I> {
  12     #[instrument(level = "debug", skip(self, interner, environment))]
  13     pub(crate) fn unify<T>(
  14         &mut self,
  15         interner: &I,
  16         environment: &Environment<I>,
  17         a: &T,
  18         b: &T,
  19     ) -> Fallible<UnificationResult<I>>
  20     where
  21         T: ?Sized + Zip<I>,
  22     {
  23         let snapshot = self.snapshot();
  24         match Unifier::new(interner, self, environment).unify(a, b) {
  25             Ok(r) => {
  26                 self.commit(snapshot);
  27                 Ok(r)
  28             }
  29             Err(e) => {
  30                 self.rollback_to(snapshot);
  31                 Err(e)
  32             }
  33         }
  34     }
  35 }
  36
  37 struct Unifier<'t, I: Interner> {
  38     table: &'t mut InferenceTable<I>,
  39     environment: &'t Environment<I>,
  40     goals: Vec<InEnvironment<DomainGoal<I>>>,
  41     constraints: Vec<InEnvironment<Constraint<I>>>,
  42     interner: &'t I,
  43 }
  44
  45 #[derive(Debug)]
  46 pub(crate) struct UnificationResult<I: Interner> {
  47     pub(crate) goals: Vec<InEnvironment<DomainGoal<I>>>,
  48     pub(crate) constraints: Vec<InEnvironment<Constraint<I>>>,
  49 }
  50
  51 impl<'t, I: Interner> Unifier<'t, I> {
  52     fn new(
  53         interner: &'t I,
  54         table: &'t mut InferenceTable<I>,
  55         environment: &'t Environment<I>,
  56     ) -> Self {
  57         Unifier {
  58             environment: environment,
  59             table: table,
  60             goals: vec![],
  61             constraints: vec![],
  62             interner,
  63         }
  64     }
  65
  66     /// The main entry point for the `Unifier` type and really the
  67     /// only type meant to be called externally. Performs a
  68     /// unification of `a` and `b` and returns the Unification Result.
  69     fn unify<T>(mut self, a: &T, b: &T) -> Fallible<UnificationResult<I>>
  70     where
  71         T: ?Sized + Zip<I>,
  72     {
  73         Zip::zip_with(&mut self, a, b)?;
  74         Ok(UnificationResult {
  75             goals: self.goals,
  76             constraints: self.constraints,
  77         })
  78     }
  79
  80     fn unify_ty_ty(&mut self, a: &Ty<I>, b: &Ty<I>) -> Fallible<()> {
  81         let interner = self.interner;
  82
  83         let n_a = self.table.normalize_ty_shallow(interner, a);
  84         let n_b = self.table.normalize_ty_shallow(interner, b);
  85         let a = n_a.as_ref().unwrap_or(a);
  86         let b = n_b.as_ref().unwrap_or(b);
  87
  88         debug_span!("unify_ty_ty", ?a, ?b);
  89         // let _s = span.enter();
  90
  91         match (a.data(interner), b.data(interner)) {
  92             // Unifying two inference variables: unify them in the underlying
  93             // ena table.
  94             (
  95                 &TyData::InferenceVar(var1, kind1),
  96                 &TyData::InferenceVar(var2, kind2),
  97             ) => {
  98                 if kind1 == kind2 {
  99                     self.unify_var_var(var1, var2)
 100                 } else if kind1 == TyKind::General {
 101                     self.unify_general_var_specific_ty(var1, b.clone())
 102                 } else if kind2 == TyKind::General {
 103                     self.unify_general_var_specific_ty(var2, a.clone())
 104                 } else {
 105                     debug!(
 106                         "Tried to unify mis-matching inference variables: {:?} and {:?}",
 107                         kind1, kind2
 108                     );
 109                     Err(NoSolution)
 110                 }
 111             }
 112
 113             // Unifying an inference variable with a non-inference variable.
 114             (&TyData::InferenceVar(var, kind), ty_data @ &TyData::Apply(_))
 115             | (&TyData::InferenceVar(var, kind), ty_data @ &TyData::Placeholder(_))
 116             | (&TyData::InferenceVar(var, kind), ty_data @ &TyData::Dyn(_))
 117             | (&TyData::InferenceVar(var, kind), ty_data @ &TyData::Function(_))
 118             // The reflexive matches
 119             | (ty_data @ &TyData::Apply(_), &TyData::InferenceVar(var, kind))
 120             | (ty_data @ &TyData::Placeholder(_), &TyData::InferenceVar(var, kind))
 121             | (ty_data @ &TyData::Dyn(_), &TyData::InferenceVar(var, kind))
 122             | (ty_data @ &TyData::Function(_), &TyData::InferenceVar(var, kind))
 123             => {
 124                 let ty = ty_data.clone().intern(interner);
 125
 126                 match (kind, ty.is_integer(interner), ty.is_float(interner)) {
 127                     // General inference variables can unify with any type
 128                     (TyKind::General, _, _)
 129                     // Integer inference variables can only unify with integer types
 130                     | (TyKind::Integer, true, _)
 131                     // Float inference variables can only unify with float types
 132                     | (TyKind::Float, _, true) => self.unify_var_ty(var, &ty),
 133                     _ => Err(NoSolution),
 134                 }
 135             }
 136
 137             // Unifying `forall<X> { T }` with some other forall type `forall<X> { U }`
 138             (&TyData::Function(ref fn1), &TyData::Function(ref fn2)) => {
 139                 self.unify_binders(fn1, fn2)
 140             }
 141
 142             // This would correspond to unifying a `fn` type with a non-fn
 143             // type in Rust; error.
 144             (&TyData::Function(_), &TyData::Apply(_))
 145             | (&TyData::Function(_), &TyData::Dyn(_))
 146             | (&TyData::Function(_), &TyData::Placeholder(_))
 147             | (&TyData::Apply(_), &TyData::Function(_))
 148             | (&TyData::Placeholder(_), &TyData::Function(_))
 149             | (&TyData::Dyn(_), &TyData::Function(_)) => Err(NoSolution),
 150
 151             (&TyData::Placeholder(ref p1), &TyData::Placeholder(ref p2)) => {
 152                 Zip::zip_with(self, p1, p2)
 153             }
 154
 155             (&TyData::Apply(ref apply1), &TyData::Apply(ref apply2)) => {
 156                 Zip::zip_with(self, apply1, apply2)
 157             }
 158
 159             // Cannot unify (e.g.) some struct type `Foo` and a placeholder like `T`
 160             (&TyData::Apply(_), &TyData::Placeholder(_))
 161             | (&TyData::Placeholder(_), &TyData::Apply(_)) => Err(NoSolution),
 162
 163             // Cannot unify `dyn Trait` with things like structs or placeholders
 164             (&TyData::Placeholder(_), &TyData::Dyn(_))
 165             | (&TyData::Dyn(_), &TyData::Placeholder(_))
 166             | (&TyData::Apply(_), &TyData::Dyn(_))
 167             | (&TyData::Dyn(_), &TyData::Apply(_)) => Err(NoSolution),
 168
 169             // Unifying two dyn is possible if they have the same bounds.
 170             (&TyData::Dyn(ref qwc1), &TyData::Dyn(ref qwc2)) => Zip::zip_with(self, qwc1, qwc2),
 171
 172             // Unifying an alias type with some other type `U`.
 173             (&TyData::Apply(_), &TyData::Alias(ref alias))
 174             | (&TyData::Placeholder(_), &TyData::Alias(ref alias))
 175             | (&TyData::Function(_), &TyData::Alias(ref alias))
 176             | (&TyData::InferenceVar(_, _), &TyData::Alias(ref alias))
 177             | (&TyData::Dyn(_), &TyData::Alias(ref alias)) => self.unify_alias_ty(alias, a),
 178
 179             (&TyData::Alias(ref alias), &TyData::Alias(_))
 180             | (&TyData::Alias(ref alias), &TyData::Apply(_))
 181             | (&TyData::Alias(ref alias), &TyData::Placeholder(_))
 182             | (&TyData::Alias(ref alias), &TyData::Function(_))
 183             | (&TyData::Alias(ref alias), &TyData::InferenceVar(_, _))
 184             | (&TyData::Alias(ref alias), &TyData::Dyn(_)) => self.unify_alias_ty(alias, b),
 185
 186             (TyData::BoundVar(_), _) | (_, TyData::BoundVar(_)) => panic!(
 187                 "unification encountered bound variable: a={:?} b={:?}",
 188                 a, b
 189             ),
 190         }
 191     }
 192
 193     /// Unify two inference variables
 194     fn unify_var_var(&mut self, a: InferenceVar, b: InferenceVar) -> Fallible<()> {
 195         debug!("unify_var_var({:?}, {:?})", a, b);
 196         let var1 = EnaVariable::from(a);
 197         let var2 = EnaVariable::from(b);
 198         Ok(self
 199             .table
 200             .unify
 201             .unify_var_var(var1, var2)
 202             .expect("unification of two unbound variables cannot fail"))
 203     }
 204
 205     /// Unify a general inference variable with a specific inference variable
 206     /// (type kind is not `General`). For example, unify a `TyKind::General`
 207     /// inference variable with a `TyKind::Integer` variable, resulting in the
 208     /// general inference variable narrowing to an integer variable.
 209     fn unify_general_var_specific_ty(
 210         &mut self,
 211         general_var: InferenceVar,
 212         specific_ty: Ty<I>,
 213     ) -> Fallible<()> {
 214         debug!(
 215             "unify_general_var_specific_var({:?}, {:?})",
 216             general_var, specific_ty
 217         );
 218
 219         self.table
 220             .unify
 221             .unify_var_value(
 222                 general_var,
 223                 InferenceValue::from_ty(self.interner, specific_ty),
 224             )
 225             .unwrap();
 226
 227         Ok(())
 228     }
 229
 230     fn unify_binders<'a, T, R>(
 231         &mut self,
 232         a: impl IntoBindersAndValue<'a, I, Value = T> + Copy + Debug,
 233         b: impl IntoBindersAndValue<'a, I, Value = T> + Copy + Debug,
 234     ) -> Fallible<()>
 235     where
 236         T: Fold<I, Result = R>,
 237         R: Zip<I> + Fold<I, Result = R>,
 238         't: 'a,
 239     {
 240         // for<'a...> T == for<'b...> U
 241         //
 242         // if:
 243         //
 244         // for<'a...> exists<'b...> T == U &&
 245         // for<'b...> exists<'a...> T == U
 246
 247         debug!("unify_binders({:?}, {:?})", a, b);
 248         let interner = self.interner;
 249
 250         {
 251             let a_universal = self.table.instantiate_binders_universally(interner, a);
 252             let b_existential = self.table.instantiate_binders_existentially(interner, b);
 253             Zip::zip_with(self, &a_universal, &b_existential)?;
 254         }
 255
 256         {
 257             let b_universal = self.table.instantiate_binders_universally(interner, b);
 258             let a_existential = self.table.instantiate_binders_existentially(interner, a);
 259             Zip::zip_with(self, &a_existential, &b_universal)
 260         }
 261     }
 262
 263     /// Unify an alias like `<T as Trait>::Item` or `impl Trait` with some other
 264     /// type `ty` (which might also be an alias). Creates a goal like
 265     ///
 266     /// ```notrust
 267     /// AliasEq(<T as Trait>::Item = U) // associated type projection
 268     /// AliasEq(impl Trait = U) // impl trait
 269     /// ```
 270     fn unify_alias_ty(&mut self, alias: &AliasTy<I>, ty: &Ty<I>) -> Fallible<()> {
 271         let interner = self.interner;
 272         Ok(self.goals.push(InEnvironment::new(
 273             self.environment,
 274             AliasEq {
 275                 alias: alias.clone(),
 276                 ty: ty.clone(),
 277             }
 278             .cast(interner),
 279         )))
 280     }
 281
 282     /// Unify an inference variable `var` with some non-inference
 283     /// variable `ty`, just bind `var` to `ty`. But we must enforce two conditions:
 284     ///
 285     /// - `var` does not appear inside of `ty` (the standard `OccursCheck`)
 286     /// - `ty` does not reference anything in a lifetime that could not be named in `var`
 287     ///   (the extended `OccursCheck` created to handle universes)
 288     fn unify_var_ty(&mut self, var: InferenceVar, ty: &Ty<I>) -> Fallible<()> {
 289         debug_span!("unify_var_ty", ?var, ?ty);
 290
 291         let interner = self.interner;
 292         let var = EnaVariable::from(var);
 293
 294         // Determine the universe index associated with this
 295         // variable. This is basically a count of the number of
 296         // `forall` binders that had been introduced at the point
 297         // this variable was created -- though it may change over time
 298         // as the variable is unified.
 299         let universe_index = self.table.universe_of_unbound_var(var);
 300
 301         let ty1 = ty.fold_with(
 302             &mut OccursCheck::new(self, var, universe_index),
 303             DebruijnIndex::INNERMOST,
 304         )?;
 305
 306         self.table
 307             .unify
 308             .unify_var_value(var, InferenceValue::from_ty(interner, ty1.clone()))
 309             .unwrap();
 310         debug!("unify_var_ty: var {:?} set to {:?}", var, ty1);
 311
 312         Ok(())
 313     }
 314
 315     fn unify_lifetime_lifetime(&mut self, a: &Lifetime<I>, b: &Lifetime<I>) -> Fallible<()> {
 316         let interner = self.interner;
 317
 318         let n_a = self.table.normalize_lifetime_shallow(interner, a);
 319         let n_b = self.table.normalize_lifetime_shallow(interner, b);
 320         let a = n_a.as_ref().unwrap_or(a);
 321         let b = n_b.as_ref().unwrap_or(b);
 322
 323         debug_span!("unify_lifetime_lifetime", ?a, ?b);
 324
 325         match (a.data(interner), b.data(interner)) {
 326             (&LifetimeData::InferenceVar(var_a), &LifetimeData::InferenceVar(var_b)) => {
 327                 let var_a = EnaVariable::from(var_a);
 328                 let var_b = EnaVariable::from(var_b);
 329                 debug!(
 330                     "unify_lifetime_lifetime: var_a={:?} var_b={:?}",
 331                     var_a, var_b
 332                 );
 333                 self.table.unify.unify_var_var(var_a, var_b).unwrap();
 334                 Ok(())
 335             }
 336
 337             (&LifetimeData::InferenceVar(a_var), &LifetimeData::Placeholder(b_idx)) => {
 338                 self.unify_lifetime_var(a, b, a_var, b, b_idx.ui)
 339             }
 340
 341             (&LifetimeData::Placeholder(a_idx), &LifetimeData::InferenceVar(b_var)) => {
 342                 self.unify_lifetime_var(a, b, b_var, a, a_idx.ui)
 343             }
 344
 345             (&LifetimeData::Placeholder(_), &LifetimeData::Placeholder(_)) => {
 346                 if a != b {
 347                     Ok(self.push_lifetime_eq_constraint(a.clone(), b.clone()))
 348                 } else {
 349                     Ok(())
 350                 }
 351             }
 352
 353             (LifetimeData::BoundVar(_), _) | (_, LifetimeData::BoundVar(_)) => panic!(
 354                 "unification encountered bound variable: a={:?} b={:?}",
 355                 a, b
 356             ),
 357
 358             (LifetimeData::Phantom(..), _) | (_, LifetimeData::Phantom(..)) => unreachable!(),
 359         }
 360     }
 361
 362     #[instrument(level = "debug", skip(self, a, b))]
 363     fn unify_lifetime_var(
 364         &mut self,
 365         a: &Lifetime<I>,
 366         b: &Lifetime<I>,
 367         var: InferenceVar,
 368         value: &Lifetime<I>,
 369         value_ui: UniverseIndex,
 370     ) -> Fallible<()> {
 371         let var = EnaVariable::from(var);
 372         let var_ui = self.table.universe_of_unbound_var(var);
 373         if var_ui.can_see(value_ui) {
 374             debug!(
 375                 "unify_lifetime_var: {:?} in {:?} can see {:?}; unifying",
 376                 var, var_ui, value_ui
 377             );
 378             self.table
 379                 .unify
 380                 .unify_var_value(
 381                     var,
 382                     InferenceValue::from_lifetime(&self.interner, value.clone()),
 383                 )
 384                 .unwrap();
 385             Ok(())
 386         } else {
 387             debug!(
 388                 "unify_lifetime_var: {:?} in {:?} cannot see {:?}; pushing constraint",
 389                 var, var_ui, value_ui
 390             );
 391             Ok(self.push_lifetime_eq_constraint(a.clone(), b.clone()))
 392         }
 393     }
 394
 395     fn unify_const_const<'a>(&mut self, a: &'a Const<I>, b: &'a Const<I>) -> Fallible<()> {
 396         let interner = self.interner;
 397
 398         let n_a = self.table.normalize_const_shallow(interner, a);
 399         let n_b = self.table.normalize_const_shallow(interner, b);
 400         let a = n_a.as_ref().unwrap_or(a);
 401         let b = n_b.as_ref().unwrap_or(b);
 402
 403         debug_span!("unify_const_const", ?a, ?b);
 404
 405         let ConstData {
 406             ty: a_ty,
 407             value: a_val,
 408         } = a.data(interner);
 409         let ConstData {
 410             ty: b_ty,
 411             value: b_val,
 412         } = b.data(interner);
 413
 414         self.unify_ty_ty(a_ty, b_ty)?;
 415
 416         match (a_val, b_val) {
 417             // Unifying two inference variables: unify them in the underlying
 418             // ena table.
 419             (&ConstValue::InferenceVar(var1), &ConstValue::InferenceVar(var2)) => {
 420                 // debug!("unify_ty_ty: unify_var_var({:?}, {:?})", var1, var2);
 421                 let var1 = EnaVariable::from(var1);
 422                 let var2 = EnaVariable::from(var2);
 423                 Ok(self
 424                     .table
 425                     .unify
 426                     .unify_var_var(var1, var2)
 427                     .expect("unification of two unbound variables cannot fail"))
 428             }
 429
 430             // Unifying an inference variables with a non-inference variable.
 431             (&ConstValue::InferenceVar(var), &ConstValue::Concrete(_))
 432             | (&ConstValue::InferenceVar(var), &ConstValue::Placeholder(_)) => {
 433                 debug!("unify_var_ty(var={:?}, ty={:?})", var, b);
 434                 self.unify_var_const(var, b)
 435             }
 436
 437             (&ConstValue::Concrete(_), &ConstValue::InferenceVar(var))
 438             | (&ConstValue::Placeholder(_), &ConstValue::InferenceVar(var)) => {
 439                 debug!("unify_var_ty(var={:?}, ty={:?})", var, a);
 440
 441                 self.unify_var_const(var, a)
 442             }
 443
 444             (&ConstValue::Placeholder(p1), &ConstValue::Placeholder(p2)) => {
 445                 Zip::zip_with(self, &p1, &p2)
 446             }
 447
 448             (&ConstValue::Concrete(ref ev1), &ConstValue::Concrete(ref ev2)) => {
 449                 if ev1.const_eq(a_ty, ev2, interner) {
 450                     Ok(())
 451                 } else {
 452                     Err(NoSolution)
 453                 }
 454             }
 455
 456             (&ConstValue::Concrete(_), &ConstValue::Placeholder(_))
 457             | (&ConstValue::Placeholder(_), &ConstValue::Concrete(_)) => Err(NoSolution),
 458
 459             (ConstValue::BoundVar(_), _) | (_, ConstValue::BoundVar(_)) => panic!(
 460                 "unification encountered bound variable: a={:?} b={:?}",
 461                 a, b
 462             ),
 463         }
 464     }
 465
 466     fn unify_var_const(&mut self, var: InferenceVar, c: &Const<I>) -> Fallible<()> {
 467         debug!("unify_var_const(var={:?}, c={:?})", var, c);
 468
 469         let interner = self.interner;
 470         let var = EnaVariable::from(var);
 471
 472         self.table
 473             .unify
 474             .unify_var_value(var, InferenceValue::from_const(interner, c.clone()))
 475             .unwrap();
 476         debug!("unify_var_const: var {:?} set to {:?}", var, c);
 477
 478         Ok(())
 479     }
 480
 481     fn push_lifetime_eq_constraint(&mut self, a: Lifetime<I>, b: Lifetime<I>) {
 482         self.constraints.push(InEnvironment::new(
 483             self.environment,
 484             Constraint::Outlives(a.clone(), b.clone()),
 485         ));
 486         self.constraints.push(InEnvironment::new(
 487             self.environment,
 488             Constraint::Outlives(b, a),
 489         ));
 490     }
 491 }
 492
 493 impl<'i, I: Interner> Zipper<'i, I> for Unifier<'i, I> {
 494     fn zip_tys(&mut self, a: &Ty<I>, b: &Ty<I>) -> Fallible<()> {
 495         self.unify_ty_ty(a, b)
 496     }
 497
 498     fn zip_lifetimes(&mut self, a: &Lifetime<I>, b: &Lifetime<I>) -> Fallible<()> {
 499         self.unify_lifetime_lifetime(a, b)
 500     }
 501
 502     fn zip_consts(&mut self, a: &Const<I>, b: &Const<I>) -> Fallible<()> {
 503         self.unify_const_const(a, b)
 504     }
 505
 506     fn zip_binders<T>(&mut self, a: &Binders<T>, b: &Binders<T>) -> Fallible<()>
 507     where
 508         T: HasInterner<Interner = I> + Zip<I> + Fold<I, Result = T>,
 509     {
 510         // The binders that appear in types (apart from quantified types, which are
 511         // handled in `unify_ty`) appear as part of `dyn Trait` and `impl Trait` types.
 512         //
 513         // They come in two varieties:
 514         //
 515         // * The existential binder from `dyn Trait` / `impl Trait`
 516         //   (representing the hidden "self" type)
 517         // * The `for<..>` binders from higher-ranked traits.
 518         //
 519         // In both cases we can use the same `unify_binders` routine.
 520
 521         self.unify_binders(a, b)
 522     }
 523
 524     fn interner(&self) -> &'i I {
 525         self.interner
 526     }
 527 }
 528
 529 struct OccursCheck<'u, 't, I: Interner> {
 530     unifier: &'u mut Unifier<'t, I>,
 531     var: EnaVariable<I>,
 532     universe_index: UniverseIndex,
 533 }
 534
 535 impl<'u, 't, I: Interner> OccursCheck<'u, 't, I> {
 536     fn new(
 537         unifier: &'u mut Unifier<'t, I>,
 538         var: EnaVariable<I>,
 539         universe_index: UniverseIndex,
 540     ) -> Self {
 541         OccursCheck {
 542             unifier,
 543             var,
 544             universe_index,
 545         }
 546     }
 547 }
 548
 549 impl<'i, I: Interner> Folder<'i, I> for OccursCheck<'_, 'i, I>
 550 where
 551     I: 'i,
 552 {
 553     fn as_dyn(&mut self) -> &mut dyn Folder<'i, I> {
 554         self
 555     }
 556
 557     fn fold_free_placeholder_ty(
 558         &mut self,
 559         universe: PlaceholderIndex,
 560         _outer_binder: DebruijnIndex,
 561     ) -> Fallible<Ty<I>> {
 562         let interner = self.interner();
 563         if self.universe_index < universe.ui {
 564             Err(NoSolution)
 565         } else {
 566             Ok(universe.to_ty(interner)) // no need to shift, not relative to depth
 567         }
 568     }
 569
 570     fn fold_free_placeholder_lifetime(
 571         &mut self,
 572         ui: PlaceholderIndex,
 573         _outer_binder: DebruijnIndex,
 574     ) -> Fallible<Lifetime<I>> {
 575         let interner = self.interner();
 576         if self.universe_index < ui.ui {
 577             // Scenario is like:
 578             //
 579             // exists<T> forall<'b> ?T = Foo<'b>
 580             //
 581             // unlike with a type variable, this **might** be
 582             // ok.  Ultimately it depends on whether the
 583             // `forall` also introduced relations to lifetimes
 584             // nameable in T. To handle that, we introduce a
 585             // fresh region variable `'x` in same universe as `T`
 586             // and add a side-constraint that `'x = 'b`:
 587             //
 588             // exists<'x> forall<'b> ?T = Foo<'x>, where 'x = 'b
 589
 590             let tick_x = self.unifier.table.new_variable(self.universe_index);
 591             self.unifier.push_lifetime_eq_constraint(
 592                 tick_x.to_lifetime(interner),
 593                 ui.to_lifetime(interner),
 594             );
 595             Ok(tick_x.to_lifetime(interner))
 596         } else {
 597             // If the `ui` is higher than `self.universe_index`, then we can name
 598             // this lifetime, no problem.
 599             Ok(ui.to_lifetime(interner)) // no need to shift, not relative to depth
 600         }
 601     }
 602
 603     fn fold_inference_ty(
 604         &mut self,
 605         var: InferenceVar,
 606         kind: TyKind,
 607         _outer_binder: DebruijnIndex,
 608     ) -> Fallible<Ty<I>> {
 609         let interner = self.interner();
 610         let var = EnaVariable::from(var);
 611         match self.unifier.table.unify.probe_value(var) {
 612             // If this variable already has a value, fold over that value instead.
 613             InferenceValue::Bound(normalized_ty) => {
 614                 let normalized_ty = normalized_ty.assert_ty_ref(interner);
 615                 let normalized_ty = normalized_ty.fold_with(self, DebruijnIndex::INNERMOST)?;
 616                 assert!(!normalized_ty.needs_shift(interner));
 617                 Ok(normalized_ty)
 618             }
 619
 620             // Otherwise, check the universe of the variable, and also
 621             // check for cycles with `self.var` (which this will soon
 622             // become the value of).
 623             InferenceValue::Unbound(ui) => {
 624                 if self.unifier.table.unify.unioned(var, self.var) {
 625                     return Err(NoSolution);
 626                 }
 627
 628                 if self.universe_index < ui {
 629                     // Scenario is like:
 630                     //
 631                     // ?A = foo(?B)
 632                     //
 633                     // where ?A is in universe 0 and ?B is in universe 1.
 634                     // This is OK, if ?B is promoted to universe 0.
 635                     self.unifier
 636                         .table
 637                         .unify
 638                         .unify_var_value(var, InferenceValue::Unbound(self.universe_index))
 639                         .unwrap();
 640                 }
 641
 642                 Ok(var.to_ty_with_kind(interner, kind))
 643             }
 644         }
 645     }
 646
 647     fn fold_inference_lifetime(
 648         &mut self,
 649         var: InferenceVar,
 650         outer_binder: DebruijnIndex,
 651     ) -> Fallible<Lifetime<I>> {
 652         // a free existentially bound region; find the
 653         // inference variable it corresponds to
 654         let interner = self.interner();
 655         let var = EnaVariable::from(var);
 656         match self.unifier.table.unify.probe_value(var) {
 657             InferenceValue::Unbound(ui) => {
 658                 if self.universe_index < ui {
 659                     // Scenario is like:
 660                     //
 661                     // exists<T> forall<'b> exists<'a> ?T = Foo<'a>
 662                     //
 663                     // where ?A is in universe 0 and `'b` is in universe 1.
 664                     // This is OK, if `'b` is promoted to universe 0.
 665                     self.unifier
 666                         .table
 667                         .unify
 668                         .unify_var_value(var, InferenceValue::Unbound(self.universe_index))
 669                         .unwrap();
 670                 }
 671                 Ok(var.to_lifetime(interner))
 672             }
 673
 674             InferenceValue::Bound(l) => {
 675                 let l = l.assert_lifetime_ref(interner);
 676                 let l = l.fold_with(self, outer_binder)?;
 677                 assert!(!l.needs_shift(interner));
 678                 Ok(l)
 679             }
 680         }
 681     }
 682
 683     fn forbid_free_vars(&self) -> bool {
 684         true
 685     }
 686
 687     fn interner(&self) -> &'i I {
 688         self.unifier.interner
 689     }
 690
 691     fn target_interner(&self) -> &'i I {
 692         self.interner()
 693     }
 694 }