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

   1 use super::var::*;
   2 use super::*;
   3 use crate::debug_span;
   4 use chalk_ir::cast::Cast;
   5 use chalk_ir::fold::{Fold, Folder};
   6 use chalk_ir::interner::{HasInterner, Interner};
   7 use chalk_ir::zip::{Zip, Zipper};
   8 use chalk_ir::UnificationDatabase;
   9 use std::fmt::Debug;
  10 use tracing::{debug, instrument};
  11
  12 impl<I: Interner> InferenceTable<I> {
  13     pub fn relate<T>(
  14         &mut self,
  15         interner: I,
  16         db: &dyn UnificationDatabase<I>,
  17         environment: &Environment<I>,
  18         variance: Variance,
  19         a: &T,
  20         b: &T,
  21     ) -> Fallible<RelationResult<I>>
  22     where
  23         T: ?Sized + Zip<I>,
  24     {
  25         let snapshot = self.snapshot();
  26         match Unifier::new(interner, db, self, environment).relate(variance, a, b) {
  27             Ok(r) => {
  28                 self.commit(snapshot);
  29                 Ok(r)
  30             }
  31             Err(e) => {
  32                 self.rollback_to(snapshot);
  33                 Err(e)
  34             }
  35         }
  36     }
  37 }
  38
  39 struct Unifier<'t, I: Interner> {
  40     table: &'t mut InferenceTable<I>,
  41     environment: &'t Environment<I>,
  42     goals: Vec<InEnvironment<Goal<I>>>,
  43     interner: I,
  44     db: &'t dyn UnificationDatabase<I>,
  45 }
  46
  47 #[derive(Debug)]
  48 pub struct RelationResult<I: Interner> {
  49     pub goals: Vec<InEnvironment<Goal<I>>>,
  50 }
  51
  52 impl<'t, I: Interner> Unifier<'t, I> {
  53     fn new(
  54         interner: I,
  55         db: &'t dyn UnificationDatabase<I>,
  56         table: &'t mut InferenceTable<I>,
  57         environment: &'t Environment<I>,
  58     ) -> Self {
  59         Unifier {
  60             environment,
  61             table,
  62             goals: vec![],
  63             interner,
  64             db,
  65         }
  66     }
  67
  68     /// The main entry point for the `Unifier` type and really the
  69     /// only type meant to be called externally. Performs a
  70     /// relation of `a` and `b` and returns the Unification Result.
  71     #[instrument(level = "debug", skip(self))]
  72     fn relate<T>(mut self, variance: Variance, a: &T, b: &T) -> Fallible<RelationResult<I>>
  73     where
  74         T: ?Sized + Zip<I>,
  75     {
  76         Zip::zip_with(&mut self, variance, a, b)?;
  77         let interner = self.interner();
  78         let mut goals = self.goals;
  79         let table = self.table;
  80         // Sometimes we'll produce a lifetime outlives goal which we later solve by unification
  81         // Technically, these *will* get canonicalized to the same bound var and so that will end up
  82         // as a goal like `^0.0 <: ^0.0`, which is trivially true. But, we remove those *here*, which
  83         // might help caching.
  84         goals.retain(|g| match g.goal.data(interner) {
  85             GoalData::SubtypeGoal(SubtypeGoal { a, b }) => {
  86                 let n_a = table.ty_root(interner, a);
  87                 let n_b = table.ty_root(interner, b);
  88                 let a = n_a.as_ref().unwrap_or(a);
  89                 let b = n_b.as_ref().unwrap_or(b);
  90                 a != b
  91             }
  92             _ => true,
  93         });
  94         Ok(RelationResult { goals })
  95     }
  96
  97     /// Relate `a`, `b` with the variance such that if `variance = Covariant`, `a` is
  98     /// a subtype of `b`.
  99     fn relate_ty_ty(&mut self, variance: Variance, a: &Ty<I>, b: &Ty<I>) -> Fallible<()> {
 100         let interner = self.interner;
 101
 102         let n_a = self.table.normalize_ty_shallow(interner, a);
 103         let n_b = self.table.normalize_ty_shallow(interner, b);
 104         let a = n_a.as_ref().unwrap_or(a);
 105         let b = n_b.as_ref().unwrap_or(b);
 106
 107         debug_span!("relate_ty_ty", ?variance, ?a, ?b);
 108
 109         if a.kind(interner) == b.kind(interner) {
 110             return Ok(());
 111         }
 112
 113         match (a.kind(interner), b.kind(interner)) {
 114             // Relating two inference variables:
 115             // First, if either variable is a float or int kind, then we always
 116             // unify if they match. This is because float and ints don't have
 117             // subtype relationships.
 118             // If both kinds are general then:
 119             // If `Invariant`, unify them in the underlying ena table.
 120             // If `Covariant` or `Contravariant`, push `SubtypeGoal`
 121             (&TyKind::InferenceVar(var1, kind1), &TyKind::InferenceVar(var2, kind2)) => {
 122                 if matches!(kind1, TyVariableKind::General)
 123                     && matches!(kind2, TyVariableKind::General)
 124                 {
 125                     // Both variable kinds are general; so unify if invariant, otherwise push subtype goal
 126                     match variance {
 127                         Variance::Invariant => self.unify_var_var(var1, var2),
 128                         Variance::Covariant => {
 129                             self.push_subtype_goal(a.clone(), b.clone());
 130                             Ok(())
 131                         }
 132                         Variance::Contravariant => {
 133                             self.push_subtype_goal(b.clone(), a.clone());
 134                             Ok(())
 135                         }
 136                     }
 137                 } else if kind1 == kind2 {
 138                     // At least one kind is not general, but they match, so unify
 139                     self.unify_var_var(var1, var2)
 140                 } else if kind1 == TyVariableKind::General {
 141                     // First kind is general, second isn't, unify
 142                     self.unify_general_var_specific_ty(var1, b.clone())
 143                 } else if kind2 == TyVariableKind::General {
 144                     // Second kind is general, first isn't, unify
 145                     self.unify_general_var_specific_ty(var2, a.clone())
 146                 } else {
 147                     debug!(
 148                         "Tried to unify mis-matching inference variables: {:?} and {:?}",
 149                         kind1, kind2
 150                     );
 151                     Err(NoSolution)
 152                 }
 153             }
 154
 155             // Unifying `forall<X> { T }` with some other forall type `forall<X> { U }`
 156             (&TyKind::Function(ref fn1), &TyKind::Function(ref fn2)) => {
 157                 if fn1.sig == fn2.sig {
 158                     Zip::zip_with(
 159                         self,
 160                         variance,
 161                         &fn1.clone().into_binders(interner),
 162                         &fn2.clone().into_binders(interner),
 163                     )
 164                 } else {
 165                     Err(NoSolution)
 166                 }
 167             }
 168
 169             (&TyKind::Placeholder(ref p1), &TyKind::Placeholder(ref p2)) => {
 170                 Zip::zip_with(self, variance, p1, p2)
 171             }
 172
 173             // Unifying two dyn is possible if they have the same bounds.
 174             (&TyKind::Dyn(ref qwc1), &TyKind::Dyn(ref qwc2)) => {
 175                 Zip::zip_with(self, variance, qwc1, qwc2)
 176             }
 177
 178             (TyKind::BoundVar(_), _) | (_, TyKind::BoundVar(_)) => panic!(
 179                 "unification encountered bound variable: a={:?} b={:?}",
 180                 a, b
 181             ),
 182
 183             // Unifying an alias type with some other type `U`.
 184             (_, &TyKind::Alias(ref alias)) => self.relate_alias_ty(variance.invert(), alias, a),
 185             (&TyKind::Alias(ref alias), _) => self.relate_alias_ty(variance, alias, b),
 186
 187             (&TyKind::InferenceVar(var, kind), ty_data) => {
 188                 let ty = ty_data.clone().intern(interner);
 189                 self.relate_var_ty(variance, var, kind, &ty)
 190             }
 191             (ty_data, &TyKind::InferenceVar(var, kind)) => {
 192                 // We need to invert the variance if inference var is `b` because we pass it in
 193                 // as `a` to relate_var_ty
 194                 let ty = ty_data.clone().intern(interner);
 195                 self.relate_var_ty(variance.invert(), var, kind, &ty)
 196             }
 197
 198             // This would correspond to unifying a `fn` type with a non-fn
 199             // type in Rust; error.
 200             (&TyKind::Function(_), _) | (_, &TyKind::Function(_)) => Err(NoSolution),
 201
 202             // Cannot unify (e.g.) some struct type `Foo` and a placeholder like `T`
 203             (_, &TyKind::Placeholder(_)) | (&TyKind::Placeholder(_), _) => Err(NoSolution),
 204
 205             // Cannot unify `dyn Trait` with things like structs or placeholders
 206             (_, &TyKind::Dyn(_)) | (&TyKind::Dyn(_), _) => Err(NoSolution),
 207
 208             (TyKind::Adt(id_a, substitution_a), TyKind::Adt(id_b, substitution_b)) => {
 209                 if id_a != id_b {
 210                     return Err(NoSolution);
 211                 }
 212                 self.zip_substs(
 213                     variance,
 214                     Some(self.unification_database().adt_variance(*id_a)),
 215                     substitution_a.as_slice(interner),
 216                     substitution_b.as_slice(interner),
 217                 )
 218             }
 219             (
 220                 TyKind::AssociatedType(id_a, substitution_a),
 221                 TyKind::AssociatedType(id_b, substitution_b),
 222             ) => {
 223                 if id_a != id_b {
 224                     return Err(NoSolution);
 225                 }
 226                 self.zip_substs(
 227                     variance,
 228                     None, // TODO: AssociatedType variances?
 229                     substitution_a.as_slice(interner),
 230                     substitution_b.as_slice(interner),
 231                 )
 232             }
 233             (TyKind::Scalar(scalar_a), TyKind::Scalar(scalar_b)) => {
 234                 Zip::zip_with(self, variance, scalar_a, scalar_b)
 235             }
 236             (TyKind::Str, TyKind::Str) => Ok(()),
 237             (TyKind::Tuple(arity_a, substitution_a), TyKind::Tuple(arity_b, substitution_b)) => {
 238                 if arity_a != arity_b {
 239                     return Err(NoSolution);
 240                 }
 241                 self.zip_substs(
 242                     variance,
 243                     Some(Variances::from_iter(
 244                         self.interner,
 245                         std::iter::repeat(Variance::Covariant).take(*arity_a),
 246                     )),
 247                     substitution_a.as_slice(interner),
 248                     substitution_b.as_slice(interner),
 249                 )
 250             }
 251             (
 252                 TyKind::OpaqueType(id_a, substitution_a),
 253                 TyKind::OpaqueType(id_b, substitution_b),
 254             ) => {
 255                 if id_a != id_b {
 256                     return Err(NoSolution);
 257                 }
 258                 self.zip_substs(
 259                     variance,
 260                     None,
 261                     substitution_a.as_slice(interner),
 262                     substitution_b.as_slice(interner),
 263                 )
 264             }
 265             (TyKind::Slice(ty_a), TyKind::Slice(ty_b)) => Zip::zip_with(self, variance, ty_a, ty_b),
 266             (TyKind::FnDef(id_a, substitution_a), TyKind::FnDef(id_b, substitution_b)) => {
 267                 if id_a != id_b {
 268                     return Err(NoSolution);
 269                 }
 270                 self.zip_substs(
 271                     variance,
 272                     Some(self.unification_database().fn_def_variance(*id_a)),
 273                     substitution_a.as_slice(interner),
 274                     substitution_b.as_slice(interner),
 275                 )
 276             }
 277             (
 278                 TyKind::Ref(mutability_a, lifetime_a, ty_a),
 279                 TyKind::Ref(mutability_b, lifetime_b, ty_b),
 280             ) => {
 281                 if mutability_a != mutability_b {
 282                     return Err(NoSolution);
 283                 }
 284                 // The lifetime is `Contravariant`
 285                 Zip::zip_with(
 286                     self,
 287                     variance.xform(Variance::Contravariant),
 288                     lifetime_a,
 289                     lifetime_b,
 290                 )?;
 291                 // The type is `Covariant` when not mut, `Invariant` otherwise
 292                 let output_variance = match mutability_a {
 293                     Mutability::Not => Variance::Covariant,
 294                     Mutability::Mut => Variance::Invariant,
 295                 };
 296                 Zip::zip_with(self, variance.xform(output_variance), ty_a, ty_b)
 297             }
 298             (TyKind::Raw(mutability_a, ty_a), TyKind::Raw(mutability_b, ty_b)) => {
 299                 if mutability_a != mutability_b {
 300                     return Err(NoSolution);
 301                 }
 302                 let ty_variance = match mutability_a {
 303                     Mutability::Not => Variance::Covariant,
 304                     Mutability::Mut => Variance::Invariant,
 305                 };
 306                 Zip::zip_with(self, variance.xform(ty_variance), ty_a, ty_b)
 307             }
 308             (TyKind::Never, TyKind::Never) => Ok(()),
 309             (TyKind::Array(ty_a, const_a), TyKind::Array(ty_b, const_b)) => {
 310                 Zip::zip_with(self, variance, ty_a, ty_b)?;
 311                 Zip::zip_with(self, variance, const_a, const_b)
 312             }
 313             (TyKind::Closure(id_a, substitution_a), TyKind::Closure(id_b, substitution_b)) => {
 314                 if id_a != id_b {
 315                     return Err(NoSolution);
 316                 }
 317                 self.zip_substs(
 318                     variance,
 319                     None,
 320                     substitution_a.as_slice(interner),
 321                     substitution_b.as_slice(interner),
 322                 )
 323             }
 324             (TyKind::Generator(id_a, substitution_a), TyKind::Generator(id_b, substitution_b)) => {
 325                 if id_a != id_b {
 326                     return Err(NoSolution);
 327                 }
 328                 self.zip_substs(
 329                     variance,
 330                     None,
 331                     substitution_a.as_slice(interner),
 332                     substitution_b.as_slice(interner),
 333                 )
 334             }
 335             (
 336                 TyKind::GeneratorWitness(id_a, substitution_a),
 337                 TyKind::GeneratorWitness(id_b, substitution_b),
 338             ) => {
 339                 if id_a != id_b {
 340                     return Err(NoSolution);
 341                 }
 342                 self.zip_substs(
 343                     variance,
 344                     None,
 345                     substitution_a.as_slice(interner),
 346                     substitution_b.as_slice(interner),
 347                 )
 348             }
 349             (TyKind::Foreign(id_a), TyKind::Foreign(id_b)) => {
 350                 Zip::zip_with(self, variance, id_a, id_b)
 351             }
 352             (TyKind::Error, TyKind::Error) => Ok(()),
 353
 354             (_, _) => Err(NoSolution),
 355         }
 356     }
 357
 358     /// Unify two inference variables
 359     #[instrument(level = "debug", skip(self))]
 360     fn unify_var_var(&mut self, a: InferenceVar, b: InferenceVar) -> Fallible<()> {
 361         let var1 = EnaVariable::from(a);
 362         let var2 = EnaVariable::from(b);
 363         self.table
 364             .unify
 365             .unify_var_var(var1, var2)
 366             .expect("unification of two unbound variables cannot fail");
 367         Ok(())
 368     }
 369
 370     /// Unify a general inference variable with a specific inference variable
 371     /// (type kind is not `General`). For example, unify a `TyVariableKind::General`
 372     /// inference variable with a `TyVariableKind::Integer` variable, resulting in the
 373     /// general inference variable narrowing to an integer variable.
 374
 375     #[instrument(level = "debug", skip(self))]
 376     fn unify_general_var_specific_ty(
 377         &mut self,
 378         general_var: InferenceVar,
 379         specific_ty: Ty<I>,
 380     ) -> Fallible<()> {
 381         self.table
 382             .unify
 383             .unify_var_value(
 384                 general_var,
 385                 InferenceValue::from_ty(self.interner, specific_ty),
 386             )
 387             .unwrap();
 388
 389         Ok(())
 390     }
 391
 392     #[instrument(level = "debug", skip(self))]
 393     fn relate_binders<'a, T, R>(
 394         &mut self,
 395         variance: Variance,
 396         a: &Binders<T>,
 397         b: &Binders<T>,
 398     ) -> Fallible<()>
 399     where
 400         T: Clone + Fold<I, Result = R> + HasInterner<Interner = I>,
 401         R: Zip<I> + Fold<I, Result = R>,
 402         't: 'a,
 403     {
 404         // for<'a...> T == for<'b...> U
 405         //
 406         // if:
 407         //
 408         // for<'a...> exists<'b...> T == U &&
 409         // for<'b...> exists<'a...> T == U
 410
 411         // for<'a...> T <: for<'b...> U
 412         //
 413         // if
 414         //
 415         // for<'b...> exists<'a...> T <: U
 416
 417         let interner = self.interner;
 418
 419         if let Variance::Invariant | Variance::Contravariant = variance {
 420             let a_universal = self
 421                 .table
 422                 .instantiate_binders_universally(interner, a.clone());
 423             let b_existential = self
 424                 .table
 425                 .instantiate_binders_existentially(interner, b.clone());
 426             Zip::zip_with(self, Variance::Contravariant, &a_universal, &b_existential)?;
 427         }
 428
 429         if let Variance::Invariant | Variance::Covariant = variance {
 430             let b_universal = self
 431                 .table
 432                 .instantiate_binders_universally(interner, b.clone());
 433             let a_existential = self
 434                 .table
 435                 .instantiate_binders_existentially(interner, a.clone());
 436             Zip::zip_with(self, Variance::Covariant, &a_existential, &b_universal)?;
 437         }
 438
 439         Ok(())
 440     }
 441
 442     /// Relate an alias like `<T as Trait>::Item` or `impl Trait` with some other
 443     /// type `ty`. If the variance is `Invariant`, creates a goal like
 444     ///
 445     /// ```notrust
 446     /// AliasEq(<T as Trait>::Item = U) // associated type projection
 447     /// AliasEq(impl Trait = U) // impl trait
 448     /// ```
 449     /// Otherwise, this creates a new variable `?X`, creates a goal like
 450     /// ```notrust
 451     /// AliasEq(Alias = ?X)
 452     /// ```
 453     /// and relates `?X` and `ty`.
 454     #[instrument(level = "debug", skip(self))]
 455     fn relate_alias_ty(
 456         &mut self,
 457         variance: Variance,
 458         alias: &AliasTy<I>,
 459         ty: &Ty<I>,
 460     ) -> Fallible<()> {
 461         let interner = self.interner;
 462         match variance {
 463             Variance::Invariant => {
 464                 self.goals.push(InEnvironment::new(
 465                     self.environment,
 466                     AliasEq {
 467                         alias: alias.clone(),
 468                         ty: ty.clone(),
 469                     }
 470                     .cast(interner),
 471                 ));
 472                 Ok(())
 473             }
 474             Variance::Covariant | Variance::Contravariant => {
 475                 let var = self
 476                     .table
 477                     .new_variable(UniverseIndex::root())
 478                     .to_ty(interner);
 479                 self.goals.push(InEnvironment::new(
 480                     self.environment,
 481                     AliasEq {
 482                         alias: alias.clone(),
 483                         ty: var.clone(),
 484                     }
 485                     .cast(interner),
 486                 ));
 487                 self.relate_ty_ty(variance, &var, ty)
 488             }
 489         }
 490     }
 491
 492     #[instrument(level = "debug", skip(self))]
 493     fn generalize_ty(
 494         &mut self,
 495         ty: &Ty<I>,
 496         universe_index: UniverseIndex,
 497         variance: Variance,
 498     ) -> Ty<I> {
 499         let interner = self.interner;
 500         match ty.kind(interner) {
 501             TyKind::Adt(id, substitution) => {
 502                 let variances = if matches!(variance, Variance::Invariant) {
 503                     None
 504                 } else {
 505                     Some(self.unification_database().adt_variance(*id))
 506                 };
 507                 let get_variance = |i| {
 508                     variances
 509                         .as_ref()
 510                         .map(|v| v.as_slice(interner)[i])
 511                         .unwrap_or(Variance::Invariant)
 512                 };
 513                 TyKind::Adt(
 514                     *id,
 515                     self.generalize_substitution(substitution, universe_index, get_variance),
 516                 )
 517                 .intern(interner)
 518             }
 519             TyKind::AssociatedType(id, substitution) => TyKind::AssociatedType(
 520                 *id,
 521                 self.generalize_substitution(substitution, universe_index, |_| variance),
 522             )
 523             .intern(interner),
 524             TyKind::Scalar(scalar) => TyKind::Scalar(*scalar).intern(interner),
 525             TyKind::Str => TyKind::Str.intern(interner),
 526             TyKind::Tuple(arity, substitution) => TyKind::Tuple(
 527                 *arity,
 528                 self.generalize_substitution(substitution, universe_index, |_| variance),
 529             )
 530             .intern(interner),
 531             TyKind::OpaqueType(id, substitution) => TyKind::OpaqueType(
 532                 *id,
 533                 self.generalize_substitution(substitution, universe_index, |_| variance),
 534             )
 535             .intern(interner),
 536             TyKind::Slice(ty) => {
 537                 TyKind::Slice(self.generalize_ty(ty, universe_index, variance)).intern(interner)
 538             }
 539             TyKind::FnDef(id, substitution) => {
 540                 let variances = if matches!(variance, Variance::Invariant) {
 541                     None
 542                 } else {
 543                     Some(self.unification_database().fn_def_variance(*id))
 544                 };
 545                 let get_variance = |i| {
 546                     variances
 547                         .as_ref()
 548                         .map(|v| v.as_slice(interner)[i])
 549                         .unwrap_or(Variance::Invariant)
 550                 };
 551                 TyKind::FnDef(
 552                     *id,
 553                     self.generalize_substitution(substitution, universe_index, get_variance),
 554                 )
 555                 .intern(interner)
 556             }
 557             TyKind::Ref(mutability, lifetime, ty) => {
 558                 let lifetime_variance = variance.xform(Variance::Contravariant);
 559                 let ty_variance = match mutability {
 560                     Mutability::Not => Variance::Covariant,
 561                     Mutability::Mut => Variance::Invariant,
 562                 };
 563                 TyKind::Ref(
 564                     *mutability,
 565                     self.generalize_lifetime(lifetime, universe_index, lifetime_variance),
 566                     self.generalize_ty(ty, universe_index, ty_variance),
 567                 )
 568                 .intern(interner)
 569             }
 570             TyKind::Raw(mutability, ty) => {
 571                 let ty_variance = match mutability {
 572                     Mutability::Not => Variance::Covariant,
 573                     Mutability::Mut => Variance::Invariant,
 574                 };
 575                 TyKind::Raw(
 576                     *mutability,
 577                     self.generalize_ty(ty, universe_index, ty_variance),
 578                 )
 579                 .intern(interner)
 580             }
 581             TyKind::Never => TyKind::Never.intern(interner),
 582             TyKind::Array(ty, const_) => TyKind::Array(
 583                 self.generalize_ty(ty, universe_index, variance),
 584                 self.generalize_const(const_, universe_index),
 585             )
 586             .intern(interner),
 587             TyKind::Closure(id, substitution) => TyKind::Closure(
 588                 *id,
 589                 self.generalize_substitution(substitution, universe_index, |_| variance),
 590             )
 591             .intern(interner),
 592             TyKind::Generator(id, substitution) => TyKind::Generator(
 593                 *id,
 594                 self.generalize_substitution(substitution, universe_index, |_| variance),
 595             )
 596             .intern(interner),
 597             TyKind::GeneratorWitness(id, substitution) => TyKind::GeneratorWitness(
 598                 *id,
 599                 self.generalize_substitution(substitution, universe_index, |_| variance),
 600             )
 601             .intern(interner),
 602             TyKind::Foreign(id) => TyKind::Foreign(*id).intern(interner),
 603             TyKind::Error => TyKind::Error.intern(interner),
 604             TyKind::Dyn(dyn_ty) => {
 605                 let DynTy { bounds, lifetime } = dyn_ty;
 606                 let lifetime = self.generalize_lifetime(
 607                     lifetime,
 608                     universe_index,
 609                     variance.xform(Variance::Contravariant),
 610                 );
 611
 612                 let bounds = bounds.map_ref(|value| {
 613                     let iter = value.iter(interner).map(|sub_var| {
 614                         sub_var.map_ref(|clause| {
 615                             match clause {
 616                                 WhereClause::Implemented(trait_ref) => {
 617                                     let TraitRef {
 618                                         ref substitution,
 619                                         trait_id,
 620                                     } = *trait_ref;
 621                                     let substitution = self.generalize_substitution_skip_self(
 622                                         substitution,
 623                                         universe_index,
 624                                         |_| Some(variance),
 625                                     );
 626                                     WhereClause::Implemented(TraitRef {
 627                                         substitution,
 628                                         trait_id,
 629                                     })
 630                                 }
 631                                 WhereClause::AliasEq(alias_eq) => {
 632                                     let AliasEq { alias, ty: _ } = alias_eq;
 633                                     let alias = match alias {
 634                                         AliasTy::Opaque(opaque_ty) => {
 635                                             let OpaqueTy {
 636                                                 ref substitution,
 637                                                 opaque_ty_id,
 638                                             } = *opaque_ty;
 639                                             let substitution = self.generalize_substitution(
 640                                                 substitution,
 641                                                 universe_index,
 642                                                 |_| variance,
 643                                             );
 644                                             AliasTy::Opaque(OpaqueTy {
 645                                                 substitution,
 646                                                 opaque_ty_id,
 647                                             })
 648                                         }
 649                                         AliasTy::Projection(projection_ty) => {
 650                                             let ProjectionTy {
 651                                                 ref substitution,
 652                                                 associated_ty_id,
 653                                             } = *projection_ty;
 654                                             // TODO: We should be skipping "self", which
 655                                             // would be the first element of
 656                                             // "trait_params" if we had a
 657                                             // `RustIrDatabase` to call
 658                                             // `split_projection` on...
 659                                             // let (assoc_ty_datum, trait_params, assoc_type_params) = s.db().split_projection(&self);
 660                                             let substitution = self.generalize_substitution(
 661                                                 substitution,
 662                                                 universe_index,
 663                                                 |_| variance,
 664                                             );
 665                                             AliasTy::Projection(ProjectionTy {
 666                                                 substitution,
 667                                                 associated_ty_id,
 668                                             })
 669                                         }
 670                                     };
 671                                     let ty =
 672                                         self.table.new_variable(universe_index).to_ty(interner);
 673                                     WhereClause::AliasEq(AliasEq { alias, ty })
 674                                 }
 675                                 WhereClause::TypeOutlives(_) => {
 676                                     let lifetime_var = self.table.new_variable(universe_index);
 677                                     let lifetime = lifetime_var.to_lifetime(interner);
 678                                     let ty_var = self.table.new_variable(universe_index);
 679                                     let ty = ty_var.to_ty(interner);
 680                                     WhereClause::TypeOutlives(TypeOutlives { ty, lifetime })
 681                                 }
 682                                 WhereClause::LifetimeOutlives(_) => {
 683                                     unreachable!("dyn Trait never contains LifetimeOutlive bounds")
 684                                 }
 685                             }
 686                         })
 687                     });
 688                     QuantifiedWhereClauses::from_iter(interner, iter)
 689                 });
 690
 691                 TyKind::Dyn(DynTy { bounds, lifetime }).intern(interner)
 692             }
 693             TyKind::Function(fn_ptr) => {
 694                 let FnPointer {
 695                     num_binders,
 696                     sig,
 697                     ref substitution,
 698                 } = *fn_ptr;
 699
 700                 let len = substitution.0.len(interner);
 701                 let vars = substitution.0.iter(interner).enumerate().map(|(i, var)| {
 702                     if i < len - 1 {
 703                         self.generalize_generic_var(
 704                             var,
 705                             universe_index,
 706                             variance.xform(Variance::Contravariant),
 707                         )
 708                     } else {
 709                         self.generalize_generic_var(
 710                             substitution.0.as_slice(interner).last().unwrap(),
 711                             universe_index,
 712                             variance,
 713                         )
 714                     }
 715                 });
 716
 717                 let substitution = FnSubst(Substitution::from_iter(interner, vars));
 718
 719                 TyKind::Function(FnPointer {
 720                     num_binders,
 721                     sig,
 722                     substitution,
 723                 })
 724                 .intern(interner)
 725             }
 726             TyKind::Placeholder(_) | TyKind::BoundVar(_) => {
 727                 debug!("just generalizing to the ty itself: {:?}", ty);
 728                 // BoundVar and PlaceHolder have no internal values to be
 729                 // generic over, so we just relate directly to it
 730                 ty.clone()
 731             }
 732             TyKind::Alias(_) => {
 733                 let ena_var = self.table.new_variable(universe_index);
 734                 ena_var.to_ty(interner)
 735             }
 736             TyKind::InferenceVar(_var, kind) => {
 737                 if matches!(kind, TyVariableKind::Integer | TyVariableKind::Float) {
 738                     ty.clone()
 739                 } else if let Some(ty) = self.table.normalize_ty_shallow(interner, ty) {
 740                     self.generalize_ty(&ty, universe_index, variance)
 741                 } else if matches!(variance, Variance::Invariant) {
 742                     ty.clone()
 743                 } else {
 744                     let ena_var = self.table.new_variable(universe_index);
 745                     ena_var.to_ty(interner)
 746                 }
 747             }
 748         }
 749     }
 750
 751     #[instrument(level = "debug", skip(self))]
 752     fn generalize_lifetime(
 753         &mut self,
 754         lifetime: &Lifetime<I>,
 755         universe_index: UniverseIndex,
 756         variance: Variance,
 757     ) -> Lifetime<I> {
 758         if matches!(lifetime.data(self.interner), LifetimeData::BoundVar(_))
 759             || matches!(variance, Variance::Invariant)
 760         {
 761             lifetime.clone()
 762         } else {
 763             self.table
 764                 .new_variable(universe_index)
 765                 .to_lifetime(self.interner)
 766         }
 767     }
 768
 769     #[instrument(level = "debug", skip(self))]
 770     fn generalize_const(&mut self, const_: &Const<I>, universe_index: UniverseIndex) -> Const<I> {
 771         let data = const_.data(self.interner);
 772         if matches!(data.value, ConstValue::BoundVar(_)) {
 773             const_.clone()
 774         } else {
 775             self.table
 776                 .new_variable(universe_index)
 777                 .to_const(self.interner, data.ty.clone())
 778         }
 779     }
 780
 781     fn generalize_generic_var(
 782         &mut self,
 783         sub_var: &GenericArg<I>,
 784         universe_index: UniverseIndex,
 785         variance: Variance,
 786     ) -> GenericArg<I> {
 787         let interner = self.interner;
 788         (match sub_var.data(interner) {
 789             GenericArgData::Ty(ty) => {
 790                 GenericArgData::Ty(self.generalize_ty(ty, universe_index, variance))
 791             }
 792             GenericArgData::Lifetime(lifetime) => GenericArgData::Lifetime(
 793                 self.generalize_lifetime(lifetime, universe_index, variance),
 794             ),
 795             GenericArgData::Const(const_value) => {
 796                 GenericArgData::Const(self.generalize_const(const_value, universe_index))
 797             }
 798         })
 799         .intern(interner)
 800     }
 801
 802     /// Generalizes all but the first
 803     #[instrument(level = "debug", skip(self, get_variance))]
 804     fn generalize_substitution_skip_self<F: Fn(usize) -> Option<Variance>>(
 805         &mut self,
 806         substitution: &Substitution<I>,
 807         universe_index: UniverseIndex,
 808         get_variance: F,
 809     ) -> Substitution<I> {
 810         let interner = self.interner;
 811         let vars = substitution.iter(interner).enumerate().map(|(i, sub_var)| {
 812             if i == 0 {
 813                 sub_var.clone()
 814             } else {
 815                 let variance = get_variance(i).unwrap_or(Variance::Invariant);
 816                 self.generalize_generic_var(sub_var, universe_index, variance)
 817             }
 818         });
 819         Substitution::from_iter(interner, vars)
 820     }
 821
 822     #[instrument(level = "debug", skip(self, get_variance))]
 823     fn generalize_substitution<F: Fn(usize) -> Variance>(
 824         &mut self,
 825         substitution: &Substitution<I>,
 826         universe_index: UniverseIndex,
 827         get_variance: F,
 828     ) -> Substitution<I> {
 829         let interner = self.interner;
 830         let vars = substitution.iter(interner).enumerate().map(|(i, sub_var)| {
 831             let variance = get_variance(i);
 832             self.generalize_generic_var(sub_var, universe_index, variance)
 833         });
 834
 835         Substitution::from_iter(interner, vars)
 836     }
 837
 838     /// Unify an inference variable `var` with some non-inference
 839     /// variable `ty`, just bind `var` to `ty`. But we must enforce two conditions:
 840     ///
 841     /// - `var` does not appear inside of `ty` (the standard `OccursCheck`)
 842     /// - `ty` does not reference anything in a lifetime that could not be named in `var`
 843     ///   (the extended `OccursCheck` created to handle universes)
 844     #[instrument(level = "debug", skip(self))]
 845     fn relate_var_ty(
 846         &mut self,
 847         variance: Variance,
 848         var: InferenceVar,
 849         var_kind: TyVariableKind,
 850         ty: &Ty<I>,
 851     ) -> Fallible<()> {
 852         let interner = self.interner;
 853
 854         match (var_kind, ty.is_integer(interner), ty.is_float(interner)) {
 855             // General inference variables can unify with any type
 856             (TyVariableKind::General, _, _)
 857             // Integer inference variables can only unify with integer types
 858             | (TyVariableKind::Integer, true, _)
 859             // Float inference variables can only unify with float types
 860             | (TyVariableKind::Float, _, true) => {
 861             },
 862             _ => return Err(NoSolution),
 863         }
 864
 865         let var = EnaVariable::from(var);
 866
 867         // Determine the universe index associated with this
 868         // variable. This is basically a count of the number of
 869         // `forall` binders that had been introduced at the point
 870         // this variable was created -- though it may change over time
 871         // as the variable is unified.
 872         let universe_index = self.table.universe_of_unbound_var(var);
 873         // let universe_index = self.table.max_universe();
 874
 875         debug!("relate_var_ty: universe index of var: {:?}", universe_index);
 876
 877         debug!("trying fold_with on {:?}", ty);
 878         let ty1 = ty
 879             .clone()
 880             .fold_with(
 881                 &mut OccursCheck::new(self, var, universe_index),
 882                 DebruijnIndex::INNERMOST,
 883             )
 884             .map_err(|e| {
 885                 debug!("failed to fold {:?}", ty);
 886                 e
 887             })?;
 888
 889         // "Generalize" types. This ensures that we aren't accidentally forcing
 890         // too much onto `var`. Instead of directly setting `var` equal to `ty`,
 891         // we just take the outermost structure we _know_ `var` holds, and then
 892         // apply that to `ty`. This involves creating new inference vars for
 893         // everything inside `var`, then calling `relate_ty_ty` to relate those
 894         // inference vars to the things they generalized with the correct
 895         // variance.
 896
 897         // The main problem this solves is that lifetime relationships are
 898         // relationships, not just eq ones. So when solving &'a u32 <: U,
 899         // generalizing we would end up with U = &'a u32. Instead, we want
 900         // U = &'b u32, with a lifetime constraint 'a <: 'b. This matters
 901         // especially when solving multiple constraints - for example, &'a u32
 902         // <: U, &'b u32 <: U (where without generalizing, we'd end up with 'a
 903         // <: 'b, where we really want 'a <: 'c, 'b <: 'c for some 'c).
 904
 905         // Example operation: consider `ty` as `&'x SomeType`. To generalize
 906         // this, we create two new vars `'0` and `1`. Then we relate `var` with
 907         // `&'0 1` and `&'0 1` with `&'x SomeType`. The second relation will
 908         // recurse, and we'll end up relating `'0` with `'x` and `1` with `SomeType`.
 909         let generalized_val = self.generalize_ty(&ty1, universe_index, variance);
 910
 911         debug!("var {:?} generalized to {:?}", var, generalized_val);
 912
 913         self.table
 914             .unify
 915             .unify_var_value(
 916                 var,
 917                 InferenceValue::from_ty(interner, generalized_val.clone()),
 918             )
 919             .unwrap();
 920         debug!("var {:?} set to {:?}", var, generalized_val);
 921
 922         self.relate_ty_ty(variance, &generalized_val, &ty1)?;
 923
 924         debug!(
 925             "generalized version {:?} related to original {:?}",
 926             generalized_val, ty1
 927         );
 928
 929         Ok(())
 930     }
 931
 932     fn relate_lifetime_lifetime(
 933         &mut self,
 934         variance: Variance,
 935         a: &Lifetime<I>,
 936         b: &Lifetime<I>,
 937     ) -> Fallible<()> {
 938         let interner = self.interner;
 939
 940         let n_a = self.table.normalize_lifetime_shallow(interner, a);
 941         let n_b = self.table.normalize_lifetime_shallow(interner, b);
 942         let a = n_a.as_ref().unwrap_or(a);
 943         let b = n_b.as_ref().unwrap_or(b);
 944
 945         debug_span!("relate_lifetime_lifetime", ?variance, ?a, ?b);
 946
 947         match (a.data(interner), b.data(interner)) {
 948             (&LifetimeData::InferenceVar(var_a), &LifetimeData::InferenceVar(var_b)) => {
 949                 let var_a = EnaVariable::from(var_a);
 950                 let var_b = EnaVariable::from(var_b);
 951                 debug!(?var_a, ?var_b);
 952                 self.table.unify.unify_var_var(var_a, var_b).unwrap();
 953                 Ok(())
 954             }
 955
 956             (
 957                 &LifetimeData::InferenceVar(a_var),
 958                 &LifetimeData::Placeholder(PlaceholderIndex { ui, .. }),
 959             )
 960             | (&LifetimeData::InferenceVar(a_var), &LifetimeData::Empty(ui)) => {
 961                 self.unify_lifetime_var(variance, a_var, b, ui)
 962             }
 963
 964             (
 965                 &LifetimeData::Placeholder(PlaceholderIndex { ui, .. }),
 966                 &LifetimeData::InferenceVar(b_var),
 967             )
 968             | (&LifetimeData::Empty(ui), &LifetimeData::InferenceVar(b_var)) => {
 969                 self.unify_lifetime_var(variance.invert(), b_var, a, ui)
 970             }
 971
 972             (&LifetimeData::InferenceVar(a_var), &LifetimeData::Erased)
 973             | (&LifetimeData::InferenceVar(a_var), &LifetimeData::Static) => {
 974                 self.unify_lifetime_var(variance, a_var, b, UniverseIndex::root())
 975             }
 976
 977             (&LifetimeData::Erased, &LifetimeData::InferenceVar(b_var))
 978             | (&LifetimeData::Static, &LifetimeData::InferenceVar(b_var)) => {
 979                 self.unify_lifetime_var(variance.invert(), b_var, a, UniverseIndex::root())
 980             }
 981
 982             (&LifetimeData::Static, &LifetimeData::Static)
 983             | (&LifetimeData::Erased, &LifetimeData::Erased) => Ok(()),
 984
 985             (&LifetimeData::Static, &LifetimeData::Placeholder(_))
 986             | (&LifetimeData::Static, &LifetimeData::Empty(_))
 987             | (&LifetimeData::Static, &LifetimeData::Erased)
 988             | (&LifetimeData::Placeholder(_), &LifetimeData::Static)
 989             | (&LifetimeData::Placeholder(_), &LifetimeData::Placeholder(_))
 990             | (&LifetimeData::Placeholder(_), &LifetimeData::Empty(_))
 991             | (&LifetimeData::Placeholder(_), &LifetimeData::Erased)
 992             | (&LifetimeData::Empty(_), &LifetimeData::Static)
 993             | (&LifetimeData::Empty(_), &LifetimeData::Placeholder(_))
 994             | (&LifetimeData::Empty(_), &LifetimeData::Empty(_))
 995             | (&LifetimeData::Empty(_), &LifetimeData::Erased)
 996             | (&LifetimeData::Erased, &LifetimeData::Static)
 997             | (&LifetimeData::Erased, &LifetimeData::Placeholder(_))
 998             | (&LifetimeData::Erased, &LifetimeData::Empty(_)) => {
 999                 if a != b {
1000                     self.push_lifetime_outlives_goals(variance, a.clone(), b.clone());
1001                     Ok(())
1002                 } else {
1003                     Ok(())
1004                 }
1005             }
1006
1007             (LifetimeData::BoundVar(_), _) | (_, LifetimeData::BoundVar(_)) => panic!(
1008                 "unification encountered bound variable: a={:?} b={:?}",
1009                 a, b
1010             ),
1011
1012             (LifetimeData::Phantom(..), _) | (_, LifetimeData::Phantom(..)) => unreachable!(),
1013         }
1014     }
1015
1016     #[instrument(level = "debug", skip(self))]
1017     fn unify_lifetime_var(
1018         &mut self,
1019         variance: Variance,
1020         var: InferenceVar,
1021         value: &Lifetime<I>,
1022         value_ui: UniverseIndex,
1023     ) -> Fallible<()> {
1024         let var = EnaVariable::from(var);
1025         let var_ui = self.table.universe_of_unbound_var(var);
1026         if var_ui.can_see(value_ui) && matches!(variance, Variance::Invariant) {
1027             debug!("{:?} in {:?} can see {:?}; unifying", var, var_ui, value_ui);
1028             self.table
1029                 .unify
1030                 .unify_var_value(
1031                     var,
1032                     InferenceValue::from_lifetime(self.interner, value.clone()),
1033                 )
1034                 .unwrap();
1035             Ok(())
1036         } else {
1037             debug!(
1038                 "{:?} in {:?} cannot see {:?}; pushing constraint",
1039                 var, var_ui, value_ui
1040             );
1041             self.push_lifetime_outlives_goals(
1042                 variance,
1043                 var.to_lifetime(self.interner),
1044                 value.clone(),
1045             );
1046             Ok(())
1047         }
1048     }
1049
1050     fn relate_const_const<'a>(
1051         &mut self,
1052         variance: Variance,
1053         a: &'a Const<I>,
1054         b: &'a Const<I>,
1055     ) -> Fallible<()> {
1056         let interner = self.interner;
1057
1058         let n_a = self.table.normalize_const_shallow(interner, a);
1059         let n_b = self.table.normalize_const_shallow(interner, b);
1060         let a = n_a.as_ref().unwrap_or(a);
1061         let b = n_b.as_ref().unwrap_or(b);
1062
1063         debug_span!("relate_const_const", ?variance, ?a, ?b);
1064
1065         let ConstData {
1066             ty: a_ty,
1067             value: a_val,
1068         } = a.data(interner);
1069         let ConstData {
1070             ty: b_ty,
1071             value: b_val,
1072         } = b.data(interner);
1073
1074         self.relate_ty_ty(variance, a_ty, b_ty)?;
1075
1076         match (a_val, b_val) {
1077             // Unifying two inference variables: unify them in the underlying
1078             // ena table.
1079             (&ConstValue::InferenceVar(var1), &ConstValue::InferenceVar(var2)) => {
1080                 debug!(?var1, ?var2, "relate_ty_ty");
1081                 let var1 = EnaVariable::from(var1);
1082                 let var2 = EnaVariable::from(var2);
1083                 self.table
1084                     .unify
1085                     .unify_var_var(var1, var2)
1086                     .expect("unification of two unbound variables cannot fail");
1087                 Ok(())
1088             }
1089
1090             // Unifying an inference variables with a non-inference variable.
1091             (&ConstValue::InferenceVar(var), &ConstValue::Concrete(_))
1092             | (&ConstValue::InferenceVar(var), &ConstValue::Placeholder(_)) => {
1093                 debug!(?var, ty=?b, "unify_var_ty");
1094                 self.unify_var_const(var, b)
1095             }
1096
1097             (&ConstValue::Concrete(_), &ConstValue::InferenceVar(var))
1098             | (&ConstValue::Placeholder(_), &ConstValue::InferenceVar(var)) => {
1099                 debug!(?var, ty=?a, "unify_var_ty");
1100                 self.unify_var_const(var, a)
1101             }
1102
1103             (&ConstValue::Placeholder(p1), &ConstValue::Placeholder(p2)) => {
1104                 Zip::zip_with(self, variance, &p1, &p2)
1105             }
1106
1107             (&ConstValue::Concrete(ref ev1), &ConstValue::Concrete(ref ev2)) => {
1108                 if ev1.const_eq(a_ty, ev2, interner) {
1109                     Ok(())
1110                 } else {
1111                     Err(NoSolution)
1112                 }
1113             }
1114
1115             (&ConstValue::Concrete(_), &ConstValue::Placeholder(_))
1116             | (&ConstValue::Placeholder(_), &ConstValue::Concrete(_)) => Err(NoSolution),
1117
1118             (ConstValue::BoundVar(_), _) | (_, ConstValue::BoundVar(_)) => panic!(
1119                 "unification encountered bound variable: a={:?} b={:?}",
1120                 a, b
1121             ),
1122         }
1123     }
1124
1125     #[instrument(level = "debug", skip(self))]
1126     fn unify_var_const(&mut self, var: InferenceVar, c: &Const<I>) -> Fallible<()> {
1127         let interner = self.interner;
1128         let var = EnaVariable::from(var);
1129
1130         // Determine the universe index associated with this
1131         // variable. This is basically a count of the number of
1132         // `forall` binders that had been introduced at the point
1133         // this variable was created -- though it may change over time
1134         // as the variable is unified.
1135         let universe_index = self.table.universe_of_unbound_var(var);
1136
1137         let c1 = c.clone().fold_with(
1138             &mut OccursCheck::new(self, var, universe_index),
1139             DebruijnIndex::INNERMOST,
1140         )?;
1141
1142         debug!("unify_var_const: var {:?} set to {:?}", var, c1);
1143         self.table
1144             .unify
1145             .unify_var_value(var, InferenceValue::from_const(interner, c1))
1146             .unwrap();
1147
1148         Ok(())
1149     }
1150
1151     /// Relate `a`, `b` such that if `variance = Covariant`, `a` is a subtype of
1152     /// `b` and thus `a` must outlive `b`.
1153     fn push_lifetime_outlives_goals(&mut self, variance: Variance, a: Lifetime<I>, b: Lifetime<I>) {
1154         debug!(
1155             "pushing lifetime outlives goals for a={:?} b={:?} with variance {:?}",
1156             a, b, variance
1157         );
1158         if matches!(variance, Variance::Invariant | Variance::Contravariant) {
1159             self.goals.push(InEnvironment::new(
1160                 self.environment,
1161                 WhereClause::LifetimeOutlives(LifetimeOutlives {
1162                     a: a.clone(),
1163                     b: b.clone(),
1164                 })
1165                 .cast(self.interner),
1166             ));
1167         }
1168         if matches!(variance, Variance::Invariant | Variance::Covariant) {
1169             self.goals.push(InEnvironment::new(
1170                 self.environment,
1171                 WhereClause::LifetimeOutlives(LifetimeOutlives { a: b, b: a }).cast(self.interner),
1172             ));
1173         }
1174     }
1175
1176     /// Pushes a goal of `a` being a subtype of `b`.
1177     fn push_subtype_goal(&mut self, a: Ty<I>, b: Ty<I>) {
1178         let subtype_goal = GoalData::SubtypeGoal(SubtypeGoal { a, b }).intern(self.interner());
1179         self.goals
1180             .push(InEnvironment::new(self.environment, subtype_goal));
1181     }
1182 }
1183
1184 impl<'i, I: Interner> Zipper<I> for Unifier<'i, I> {
1185     fn zip_tys(&mut self, variance: Variance, a: &Ty<I>, b: &Ty<I>) -> Fallible<()> {
1186         debug!("zip_tys {:?}, {:?}, {:?}", variance, a, b);
1187         self.relate_ty_ty(variance, a, b)
1188     }
1189
1190     fn zip_lifetimes(
1191         &mut self,
1192         variance: Variance,
1193         a: &Lifetime<I>,
1194         b: &Lifetime<I>,
1195     ) -> Fallible<()> {
1196         self.relate_lifetime_lifetime(variance, a, b)
1197     }
1198
1199     fn zip_consts(&mut self, variance: Variance, a: &Const<I>, b: &Const<I>) -> Fallible<()> {
1200         self.relate_const_const(variance, a, b)
1201     }
1202
1203     fn zip_binders<T>(&mut self, variance: Variance, a: &Binders<T>, b: &Binders<T>) -> Fallible<()>
1204     where
1205         T: Clone + HasInterner<Interner = I> + Zip<I> + Fold<I, Result = T>,
1206     {
1207         // The binders that appear in types (apart from quantified types, which are
1208         // handled in `unify_ty`) appear as part of `dyn Trait` and `impl Trait` types.
1209         //
1210         // They come in two varieties:
1211         //
1212         // * The existential binder from `dyn Trait` / `impl Trait`
1213         //   (representing the hidden "self" type)
1214         // * The `for<..>` binders from higher-ranked traits.
1215         //
1216         // In both cases we can use the same `relate_binders` routine.
1217
1218         self.relate_binders(variance, a, b)
1219     }
1220
1221     fn interner(&self) -> I {
1222         self.interner
1223     }
1224
1225     fn unification_database(&self) -> &dyn UnificationDatabase<I> {
1226         self.db
1227     }
1228 }
1229
1230 struct OccursCheck<'u, 't, I: Interner> {
1231     unifier: &'u mut Unifier<'t, I>,
1232     var: EnaVariable<I>,
1233     universe_index: UniverseIndex,
1234 }
1235
1236 impl<'u, 't, I: Interner> OccursCheck<'u, 't, I> {
1237     fn new(
1238         unifier: &'u mut Unifier<'t, I>,
1239         var: EnaVariable<I>,
1240         universe_index: UniverseIndex,
1241     ) -> Self {
1242         OccursCheck {
1243             unifier,
1244             var,
1245             universe_index,
1246         }
1247     }
1248 }
1249
1250 impl<'i, I: Interner> Folder<I> for OccursCheck<'_, 'i, I> {
1251     type Error = NoSolution;
1252
1253     fn as_dyn(&mut self) -> &mut dyn Folder<I, Error = Self::Error> {
1254         self
1255     }
1256
1257     fn fold_free_placeholder_ty(
1258         &mut self,
1259         universe: PlaceholderIndex,
1260         _outer_binder: DebruijnIndex,
1261     ) -> Fallible<Ty<I>> {
1262         let interner = self.interner();
1263         if self.universe_index < universe.ui {
1264             debug!(
1265                 "OccursCheck aborting because self.universe_index ({:?}) < universe.ui ({:?})",
1266                 self.universe_index, universe.ui
1267             );
1268             Err(NoSolution)
1269         } else {
1270             Ok(universe.to_ty(interner)) // no need to shift, not relative to depth
1271         }
1272     }
1273
1274     fn fold_free_placeholder_const(
1275         &mut self,
1276         ty: Ty<I>,
1277         universe: PlaceholderIndex,
1278         _outer_binder: DebruijnIndex,
1279     ) -> Fallible<Const<I>> {
1280         let interner = self.interner();
1281         if self.universe_index < universe.ui {
1282             Err(NoSolution)
1283         } else {
1284             Ok(universe.to_const(interner, ty)) // no need to shift, not relative to depth
1285         }
1286     }
1287
1288     #[instrument(level = "debug", skip(self))]
1289     fn fold_free_placeholder_lifetime(
1290         &mut self,
1291         ui: PlaceholderIndex,
1292         _outer_binder: DebruijnIndex,
1293     ) -> Fallible<Lifetime<I>> {
1294         let interner = self.interner();
1295         if self.universe_index < ui.ui {
1296             // Scenario is like:
1297             //
1298             // exists<T> forall<'b> ?T = Foo<'b>
1299             //
1300             // unlike with a type variable, this **might** be
1301             // ok.  Ultimately it depends on whether the
1302             // `forall` also introduced relations to lifetimes
1303             // nameable in T. To handle that, we introduce a
1304             // fresh region variable `'x` in same universe as `T`
1305             // and add a side-constraint that `'x = 'b`:
1306             //
1307             // exists<'x> forall<'b> ?T = Foo<'x>, where 'x = 'b
1308
1309             let tick_x = self.unifier.table.new_variable(self.universe_index);
1310             self.unifier.push_lifetime_outlives_goals(
1311                 Variance::Invariant,
1312                 tick_x.to_lifetime(interner),
1313                 ui.to_lifetime(interner),
1314             );
1315             Ok(tick_x.to_lifetime(interner))
1316         } else {
1317             // If the `ui` is higher than `self.universe_index`, then we can name
1318             // this lifetime, no problem.
1319             Ok(ui.to_lifetime(interner)) // no need to shift, not relative to depth
1320         }
1321     }
1322
1323     fn fold_inference_ty(
1324         &mut self,
1325         var: InferenceVar,
1326         kind: TyVariableKind,
1327         _outer_binder: DebruijnIndex,
1328     ) -> Fallible<Ty<I>> {
1329         let interner = self.interner();
1330         let var = EnaVariable::from(var);
1331         match self.unifier.table.unify.probe_value(var) {
1332             // If this variable already has a value, fold over that value instead.
1333             InferenceValue::Bound(normalized_ty) => {
1334                 let normalized_ty = normalized_ty.assert_ty_ref(interner);
1335                 let normalized_ty = normalized_ty
1336                     .clone()
1337                     .fold_with(self, DebruijnIndex::INNERMOST)?;
1338                 assert!(!normalized_ty.needs_shift(interner));
1339                 Ok(normalized_ty)
1340             }
1341
1342             // Otherwise, check the universe of the variable, and also
1343             // check for cycles with `self.var` (which this will soon
1344             // become the value of).
1345             InferenceValue::Unbound(ui) => {
1346                 if self.unifier.table.unify.unioned(var, self.var) {
1347                     debug!(
1348                         "OccursCheck aborting because {:?} unioned with {:?}",
1349                         var, self.var,
1350                     );
1351                     return Err(NoSolution);
1352                 }
1353
1354                 if self.universe_index < ui {
1355                     // Scenario is like:
1356                     //
1357                     // ?A = foo(?B)
1358                     //
1359                     // where ?A is in universe 0 and ?B is in universe 1.
1360                     // This is OK, if ?B is promoted to universe 0.
1361                     self.unifier
1362                         .table
1363                         .unify
1364                         .unify_var_value(var, InferenceValue::Unbound(self.universe_index))
1365                         .unwrap();
1366                 }
1367
1368                 Ok(var.to_ty_with_kind(interner, kind))
1369             }
1370         }
1371     }
1372
1373     fn fold_inference_const(
1374         &mut self,
1375         ty: Ty<I>,
1376         var: InferenceVar,
1377         _outer_binder: DebruijnIndex,
1378     ) -> Fallible<Const<I>> {
1379         let interner = self.interner();
1380         let var = EnaVariable::from(var);
1381         match self.unifier.table.unify.probe_value(var) {
1382             // If this variable already has a value, fold over that value instead.
1383             InferenceValue::Bound(normalized_const) => {
1384                 let normalized_const = normalized_const.assert_const_ref(interner);
1385                 let normalized_const = normalized_const
1386                     .clone()
1387                     .fold_with(self, DebruijnIndex::INNERMOST)?;
1388                 assert!(!normalized_const.needs_shift(interner));
1389                 Ok(normalized_const)
1390             }
1391
1392             // Otherwise, check the universe of the variable, and also
1393             // check for cycles with `self.var` (which this will soon
1394             // become the value of).
1395             InferenceValue::Unbound(ui) => {
1396                 if self.unifier.table.unify.unioned(var, self.var) {
1397                     return Err(NoSolution);
1398                 }
1399
1400                 if self.universe_index < ui {
1401                     // Scenario is like:
1402                     //
1403                     // forall<const A> exists<const B> ?C = Foo<B>
1404                     //
1405                     // where A is in universe 0 and B is in universe 1.
1406                     // This is OK, if B is promoted to universe 0.
1407                     self.unifier
1408                         .table
1409                         .unify
1410                         .unify_var_value(var, InferenceValue::Unbound(self.universe_index))
1411                         .unwrap();
1412                 }
1413
1414                 Ok(var.to_const(interner, ty))
1415             }
1416         }
1417     }
1418
1419     fn fold_inference_lifetime(
1420         &mut self,
1421         var: InferenceVar,
1422         outer_binder: DebruijnIndex,
1423     ) -> Fallible<Lifetime<I>> {
1424         // a free existentially bound region; find the
1425         // inference variable it corresponds to
1426         let interner = self.interner();
1427         let var = EnaVariable::from(var);
1428         match self.unifier.table.unify.probe_value(var) {
1429             InferenceValue::Unbound(ui) => {
1430                 if self.universe_index < ui {
1431                     // Scenario is like:
1432                     //
1433                     // exists<T> forall<'b> exists<'a> ?T = Foo<'a>
1434                     //
1435                     // where ?A is in universe 0 and `'b` is in universe 1.
1436                     // This is OK, if `'b` is promoted to universe 0.
1437                     self.unifier
1438                         .table
1439                         .unify
1440                         .unify_var_value(var, InferenceValue::Unbound(self.universe_index))
1441                         .unwrap();
1442                 }
1443                 Ok(var.to_lifetime(interner))
1444             }
1445
1446             InferenceValue::Bound(l) => {
1447                 let l = l.assert_lifetime_ref(interner);
1448                 let l = l.clone().fold_with(self, outer_binder)?;
1449                 assert!(!l.needs_shift(interner));
1450                 Ok(l)
1451             }
1452         }
1453     }
1454
1455     fn forbid_free_vars(&self) -> bool {
1456         true
1457     }
1458
1459     fn interner(&self) -> I {
1460         self.unifier.interner
1461     }
1462 }