8 files changed, 125 insertions, 438 deletions
diff --git a/crates/hir_ty/src/chalk_db.rs b/crates/hir_ty/src/chalk_db.rs
index 8f054d06b..b108fd559 100644
--- a/crates/hir_ty/src/chalk_db.rs
+++ b/crates/hir_ty/src/chalk_db.rs
@@ -344,20 +344,20 @@ impl<'a> chalk_solve::RustIrDatabase<Interner> for ChalkContext<'a> {
    }
    fn unification_database(&self) -> &dyn chalk_ir::UnificationDatabase<Interner> {
-        self
+        &self.db
    }
 }
-impl<'a> chalk_ir::UnificationDatabase<Interner> for ChalkContext<'a> {
+impl<'a> chalk_ir::UnificationDatabase<Interner> for &'a dyn HirDatabase {
    fn fn_def_variance(
        &self,
        fn_def_id: chalk_ir::FnDefId<Interner>,
    ) -> chalk_ir::Variances<Interner> {
-        self.db.fn_def_variance(self.krate, fn_def_id)
+        HirDatabase::fn_def_variance(*self, fn_def_id)
    }
    fn adt_variance(&self, adt_id: chalk_ir::AdtId<Interner>) -> chalk_ir::Variances<Interner> {
-        self.db.adt_variance(self.krate, adt_id)
+        HirDatabase::adt_variance(*self, adt_id)
    }
 }
@@ -651,11 +651,7 @@ pub(crate) fn fn_def_datum_query(
    Arc::new(datum)
 }
-pub(crate) fn fn_def_variance_query(
+pub(crate) fn fn_def_variance_query(db: &dyn HirDatabase, fn_def_id: FnDefId) -> Variances {
-    db: &dyn HirDatabase,
-    _krate: CrateId,
-    fn_def_id: FnDefId,
-) -> Variances {
    let callable_def: CallableDefId = from_chalk(db, fn_def_id);
    let generic_params = generics(db.upcast(), callable_def.into());
    Variances::from_iter(
@@ -666,7 +662,6 @@ pub(crate) fn fn_def_variance_query(
 pub(crate) fn adt_variance_query(
    db: &dyn HirDatabase,
-    _krate: CrateId,
    chalk_ir::AdtId(adt_id): AdtId,
 ) -> Variances {
    let generic_params = generics(db.upcast(), adt_id.into());
diff --git a/crates/hir_ty/src/db.rs b/crates/hir_ty/src/db.rs
index 9da0a02e3..f773aa621 100644
--- a/crates/hir_ty/src/db.rs
+++ b/crates/hir_ty/src/db.rs
@@ -117,10 +117,10 @@ pub trait HirDatabase: DefDatabase + Upcast<dyn DefDatabase> {
    fn fn_def_datum(&self, krate: CrateId, fn_def_id: FnDefId) -> Arc<chalk_db::FnDefDatum>;
    #[salsa::invoke(chalk_db::fn_def_variance_query)]
-    fn fn_def_variance(&self, krate: CrateId, fn_def_id: FnDefId) -> chalk_db::Variances;
+    fn fn_def_variance(&self, fn_def_id: FnDefId) -> chalk_db::Variances;
    #[salsa::invoke(chalk_db::adt_variance_query)]
-    fn adt_variance(&self, krate: CrateId, adt_id: chalk_db::AdtId) -> chalk_db::Variances;
+    fn adt_variance(&self, adt_id: chalk_db::AdtId) -> chalk_db::Variances;
    #[salsa::invoke(chalk_db::associated_ty_value_query)]
    fn associated_ty_value(
diff --git a/crates/hir_ty/src/infer.rs b/crates/hir_ty/src/infer.rs
index 0ee851a74..2a82f1b47 100644
--- a/crates/hir_ty/src/infer.rs
+++ b/crates/hir_ty/src/infer.rs
@@ -217,7 +217,7 @@ struct InferenceContext<'a> {
    owner: DefWithBodyId,
    body: Arc<Body>,
    resolver: Resolver,
-    table: unify::InferenceTable,
+    table: unify::InferenceTable<'a>,
    trait_env: Arc<TraitEnvironment>,
    obligations: Vec<DomainGoal>,
    last_obligations_check: Option<u32>,
@@ -252,15 +252,15 @@ fn find_breakable<'c>(
 impl<'a> InferenceContext<'a> {
    fn new(db: &'a dyn HirDatabase, owner: DefWithBodyId, resolver: Resolver) -> Self {
+        let trait_env =
+            owner.as_generic_def_id().map_or_else(Default::default, |d| db.trait_environment(d));
        InferenceContext {
            result: InferenceResult::default(),
-            table: unify::InferenceTable::new(),
+            table: unify::InferenceTable::new(db, trait_env.clone()),
            obligations: Vec::default(),
            last_obligations_check: None,
            return_ty: TyKind::Error.intern(&Interner), // set in collect_fn_signature
-            trait_env: owner
+            trait_env,
-                .as_generic_def_id()
-                .map_or_else(Default::default, |d| db.trait_environment(d)),
            db,
            owner,
            body: db.body(owner),
@@ -346,17 +346,12 @@ impl<'a> InferenceContext<'a> {
    }
    fn resolve_obligations_as_possible(&mut self) {
-        if self.last_obligations_check == Some(self.table.revision) {
-            // no change
-            return;
-        }
        let _span = profile::span("resolve_obligations_as_possible");
-        self.last_obligations_check = Some(self.table.revision);
        let obligations = mem::replace(&mut self.obligations, Vec::new());
        for obligation in obligations {
            let in_env = InEnvironment::new(&self.trait_env.env, obligation.clone());
-            let canonicalized = self.canonicalizer().canonicalize_obligation(in_env);
+            let canonicalized = self.canonicalize(in_env);
            let solution =
                self.db.trait_solve(self.resolver.krate().unwrap(), canonicalized.value.clone());
@@ -395,6 +390,7 @@ impl<'a> InferenceContext<'a> {
        self.table.unify(ty1, ty2)
    }
+    // FIXME get rid of this, instead resolve shallowly where necessary
    /// Resolves the type as far as currently possible, replacing type variables
    /// by their known types. All types returned by the infer_* functions should
    /// be resolved as far as possible, i.e. contain no type variables with
diff --git a/crates/hir_ty/src/infer/coerce.rs b/crates/hir_ty/src/infer/coerce.rs
index 1f463a425..ae858b1b0 100644
--- a/crates/hir_ty/src/infer/coerce.rs
+++ b/crates/hir_ty/src/infer/coerce.rs
@@ -7,7 +7,7 @@
 use chalk_ir::{cast::Cast, Mutability, TyVariableKind};
 use hir_def::lang_item::LangItemTarget;
-use crate::{autoderef, Canonical, Interner, Solution, Ty, TyBuilder, TyExt, TyKind};
+use crate::{autoderef, Canonical, DomainGoal, Interner, Solution, Ty, TyBuilder, TyExt, TyKind};
 use super::{InEnvironment, InferenceContext};
@@ -141,10 +141,10 @@ impl<'a> InferenceContext<'a> {
            b.push(from_ty.clone()).push(to_ty.clone()).build()
        };
-        let goal = InEnvironment::new(&self.trait_env.env, trait_ref.cast(&Interner));
+        let goal: InEnvironment<DomainGoal> =
+            InEnvironment::new(&self.trait_env.env, trait_ref.cast(&Interner));
-        let canonicalizer = self.canonicalizer();
+        let canonicalized = self.canonicalize(goal);
-        let canonicalized = canonicalizer.canonicalize_obligation(goal);
        let solution = self.db.trait_solve(krate, canonicalized.value.clone())?;
@@ -169,7 +169,7 @@ impl<'a> InferenceContext<'a> {
    ///
    /// Note that the parameters are already stripped the outer reference.
    fn unify_autoderef_behind_ref(&mut self, from_ty: &Ty, to_ty: &Ty) -> bool {
-        let canonicalized = self.canonicalizer().canonicalize_ty(from_ty.clone());
+        let canonicalized = self.canonicalize(from_ty.clone());
        let to_ty = self.resolve_ty_shallow(&to_ty);
        // FIXME: Auto DerefMut
        for derefed_ty in autoderef::autoderef(
diff --git a/crates/hir_ty/src/infer/expr.rs b/crates/hir_ty/src/infer/expr.rs
index 7278faeec..aab4d3153 100644
--- a/crates/hir_ty/src/infer/expr.rs
+++ b/crates/hir_ty/src/infer/expr.rs
@@ -98,7 +98,7 @@ impl<'a> InferenceContext<'a> {
            goal: projection.trait_ref(self.db).cast(&Interner),
            environment: trait_env,
        };
-        let canonical = self.canonicalizer().canonicalize_obligation(obligation.clone());
+        let canonical = self.canonicalize(obligation.clone());
        if self.db.trait_solve(krate, canonical.value).is_some() {
            self.push_obligation(obligation.goal);
            let return_ty = self.normalize_projection_ty(projection);
@@ -297,7 +297,7 @@ impl<'a> InferenceContext<'a> {
            }
            Expr::Call { callee, args } => {
                let callee_ty = self.infer_expr(*callee, &Expectation::none());
-                let canonicalized = self.canonicalizer().canonicalize_ty(callee_ty.clone());
+                let canonicalized = self.canonicalize(callee_ty.clone());
                let mut derefs = autoderef(
                    self.db,
                    self.resolver.krate(),
@@ -442,7 +442,7 @@ impl<'a> InferenceContext<'a> {
            }
            Expr::Field { expr, name } => {
                let receiver_ty = self.infer_expr_inner(*expr, &Expectation::none());
-                let canonicalized = self.canonicalizer().canonicalize_ty(receiver_ty);
+                let canonicalized = self.canonicalize(receiver_ty);
                let ty = autoderef::autoderef(
                    self.db,
                    self.resolver.krate(),
@@ -559,7 +559,7 @@ impl<'a> InferenceContext<'a> {
                match op {
                    UnaryOp::Deref => match self.resolver.krate() {
                        Some(krate) => {
-                            let canonicalized = self.canonicalizer().canonicalize_ty(inner_ty);
+                            let canonicalized = self.canonicalize(inner_ty);
                            match autoderef::deref(
                                self.db,
                                krate,
@@ -676,7 +676,7 @@ impl<'a> InferenceContext<'a> {
                if let (Some(index_trait), Some(krate)) =
                    (self.resolve_ops_index(), self.resolver.krate())
                {
-                    let canonicalized = self.canonicalizer().canonicalize_ty(base_ty);
+                    let canonicalized = self.canonicalize(base_ty);
                    let self_ty = method_resolution::resolve_indexing_op(
                        self.db,
                        &canonicalized.value,
@@ -852,7 +852,7 @@ impl<'a> InferenceContext<'a> {
        generic_args: Option<&GenericArgs>,
    ) -> Ty {
        let receiver_ty = self.infer_expr(receiver, &Expectation::none());
-        let canonicalized_receiver = self.canonicalizer().canonicalize_ty(receiver_ty.clone());
+        let canonicalized_receiver = self.canonicalize(receiver_ty.clone());
        let traits_in_scope = self.resolver.traits_in_scope(self.db.upcast());
diff --git a/crates/hir_ty/src/infer/path.rs b/crates/hir_ty/src/infer/path.rs
index 495282eba..bc64b612b 100644
--- a/crates/hir_ty/src/infer/path.rs
+++ b/crates/hir_ty/src/infer/path.rs
@@ -218,7 +218,7 @@ impl<'a> InferenceContext<'a> {
            return Some(result);
        }
-        let canonical_ty = self.canonicalizer().canonicalize_ty(ty.clone());
+        let canonical_ty = self.canonicalize(ty.clone());
        let krate = self.resolver.krate()?;
        let traits_in_scope = self.resolver.traits_in_scope(self.db.upcast());
diff --git a/crates/hir_ty/src/infer/unify.rs b/crates/hir_ty/src/infer/unify.rs
index d8e0b4320..9b28c76d6 100644
--- a/crates/hir_ty/src/infer/unify.rs
+++ b/crates/hir_ty/src/infer/unify.rs
@@ -1,133 +1,52 @@
 //! Unification and canonicalization logic.
-use std::borrow::Cow;
+use std::{borrow::Cow, fmt, sync::Arc};
 use chalk_ir::{
    cast::Cast, fold::Fold, interner::HasInterner, FloatTy, IntTy, TyVariableKind, UniverseIndex,
    VariableKind,
 };
-use ena::unify::{InPlaceUnificationTable, NoError, UnifyKey, UnifyValue};
+use chalk_solve::infer::ParameterEnaVariableExt;
+use ena::unify::UnifyKey;
-use super::{DomainGoal, InferenceContext};
+use super::InferenceContext;
 use crate::{
-    fold_tys, static_lifetime, AliasEq, AliasTy, BoundVar, Canonical, CanonicalVarKinds,
+    db::HirDatabase, fold_tys, static_lifetime, BoundVar, Canonical, DebruijnIndex, GenericArg,
-    DebruijnIndex, FnPointer, FnSubst, InEnvironment, InferenceVar, Interner, Scalar, Substitution,
+    InferenceVar, Interner, Scalar, Substitution, TraitEnvironment, Ty, TyKind,
-    Ty, TyExt, TyKind, WhereClause,
 };
 impl<'a> InferenceContext<'a> {
-    pub(super) fn canonicalizer<'b>(&'b mut self) -> Canonicalizer<'a, 'b>
+    pub(super) fn canonicalize<T: Fold<Interner> + HasInterner<Interner = Interner>>(
+        &mut self,
+        t: T,
+    ) -> Canonicalized<T::Result>
    where
-        'a: 'b,
+        T::Result: HasInterner<Interner = Interner>,
    {
-        Canonicalizer { ctx: self, free_vars: Vec::new(), var_stack: Vec::new() }
+        let result = self.table.var_unification_table.canonicalize(&Interner, t);
+        let free_vars = result
+            .free_vars
+            .into_iter()
+            .map(|free_var| free_var.to_generic_arg(&Interner))
+            .collect();
+        Canonicalized { value: result.quantified, free_vars }
    }
 }
-pub(super) struct Canonicalizer<'a, 'b>
-where
-    'a: 'b,
-{
-    ctx: &'b mut InferenceContext<'a>,
-    free_vars: Vec<(InferenceVar, TyVariableKind)>,
-    /// A stack of type variables that is used to detect recursive types (which
-    /// are an error, but we need to protect against them to avoid stack
-    /// overflows).
-    var_stack: Vec<TypeVarId>,
-}
 #[derive(Debug)]
 pub(super) struct Canonicalized<T>
 where
    T: HasInterner<Interner = Interner>,
 {
    pub(super) value: Canonical<T>,
-    free_vars: Vec<(InferenceVar, TyVariableKind)>,
+    free_vars: Vec<GenericArg>,
-}
-impl<'a, 'b> Canonicalizer<'a, 'b> {
-    fn add(&mut self, free_var: InferenceVar, kind: TyVariableKind) -> usize {
-        self.free_vars.iter().position(|&(v, _)| v == free_var).unwrap_or_else(|| {
-            let next_index = self.free_vars.len();
-            self.free_vars.push((free_var, kind));
-            next_index
-        })
-    }
-    fn do_canonicalize<T: Fold<Interner, Result = T> + HasInterner<Interner = Interner>>(
-        &mut self,
-        t: T,
-        binders: DebruijnIndex,
-    ) -> T {
-        fold_tys(
-            t,
-            |ty, binders| match ty.kind(&Interner) {
-                &TyKind::InferenceVar(var, kind) => {
-                    let inner = from_inference_var(var);
-                    if self.var_stack.contains(&inner) {
-                        // recursive type
-                        return self.ctx.table.type_variable_table.fallback_value(var, kind);
-                    }
-                    if let Some(known_ty) =
-                        self.ctx.table.var_unification_table.inlined_probe_value(inner).known()
-                    {
-                        self.var_stack.push(inner);
-                        let result = self.do_canonicalize(known_ty.clone(), binders);
-                        self.var_stack.pop();
-                        result
-                    } else {
-                        let root = self.ctx.table.var_unification_table.find(inner);
-                        let position = self.add(to_inference_var(root), kind);
-                        TyKind::BoundVar(BoundVar::new(binders, position)).intern(&Interner)
-                    }
-                }
-                _ => ty,
-            },
-            binders,
-        )
-    }
-    fn into_canonicalized<T: HasInterner<Interner = Interner>>(
-        self,
-        result: T,
-    ) -> Canonicalized<T> {
-        let kinds = self
-            .free_vars
-            .iter()
-            .map(|&(_, k)| chalk_ir::WithKind::new(VariableKind::Ty(k), UniverseIndex::ROOT));
-        Canonicalized {
-            value: Canonical {
-                value: result,
-                binders: CanonicalVarKinds::from_iter(&Interner, kinds),
-            },
-            free_vars: self.free_vars,
-        }
-    }
-    pub(crate) fn canonicalize_ty(mut self, ty: Ty) -> Canonicalized<Ty> {
-        let result = self.do_canonicalize(ty, DebruijnIndex::INNERMOST);
-        self.into_canonicalized(result)
-    }
-    pub(crate) fn canonicalize_obligation(
-        mut self,
-        obligation: InEnvironment<DomainGoal>,
-    ) -> Canonicalized<InEnvironment<DomainGoal>> {
-        let result = match obligation.goal {
-            DomainGoal::Holds(wc) => {
-                DomainGoal::Holds(self.do_canonicalize(wc, DebruijnIndex::INNERMOST))
-            }
-            _ => unimplemented!(),
-        };
-        self.into_canonicalized(InEnvironment { goal: result, environment: obligation.environment })
-    }
 }
 impl<T: HasInterner<Interner = Interner>> Canonicalized<T> {
    pub(super) fn decanonicalize_ty(&self, ty: Ty) -> Ty {
        crate::fold_free_vars(ty, |bound, _binders| {
-            let (v, k) = self.free_vars[bound.index];
+            let var = self.free_vars[bound.index];
-            TyKind::InferenceVar(v, k).intern(&Interner)
+            var.assert_ty_ref(&Interner).clone()
        })
    }
@@ -155,23 +74,29 @@ impl<T: HasInterner<Interner = Interner>> Canonicalized<T> {
            }),
        );
        for (i, ty) in solution.value.iter(&Interner).enumerate() {
-            let (v, k) = self.free_vars[i];
+            // FIXME: deal with non-type vars here -- the only problematic part is the normalization
+            // and maybe we don't need that with lazy normalization?
+            let var = self.free_vars[i];
            // eagerly replace projections in the type; we may be getting types
            // e.g. from where clauses where this hasn't happened yet
            let ty = ctx.normalize_associated_types_in(
                new_vars.apply(ty.assert_ty_ref(&Interner).clone(), &Interner),
            );
-            ctx.table.unify(&TyKind::InferenceVar(v, k).intern(&Interner), &ty);
+            ctx.table.unify(var.assert_ty_ref(&Interner), &ty);
        }
    }
 }
-pub fn could_unify(t1: &Ty, t2: &Ty) -> bool {
+pub fn could_unify(db: &dyn HirDatabase, env: Arc<TraitEnvironment>, t1: &Ty, t2: &Ty) -> bool {
-    InferenceTable::new().unify(t1, t2)
+    InferenceTable::new(db, env).unify(t1, t2)
 }
-pub(crate) fn unify(tys: &Canonical<(Ty, Ty)>) -> Option<Substitution> {
+pub(crate) fn unify(
-    let mut table = InferenceTable::new();
+    db: &dyn HirDatabase,
+    env: Arc<TraitEnvironment>,
+    tys: &Canonical<(Ty, Ty)>,
+) -> Option<Substitution> {
+    let mut table = InferenceTable::new(db, env);
    let vars = Substitution::from_iter(
        &Interner,
        tys.binders
@@ -214,16 +139,16 @@ impl TypeVariableTable {
    }
    pub(super) fn set_diverging(&mut self, iv: InferenceVar, diverging: bool) {
-        self.inner[from_inference_var(iv).0 as usize].diverging = diverging;
+        self.inner[iv.index() as usize].diverging = diverging;
    }
    fn is_diverging(&mut self, iv: InferenceVar) -> bool {
-        self.inner[from_inference_var(iv).0 as usize].diverging
+        self.inner[iv.index() as usize].diverging
    }
    fn fallback_value(&self, iv: InferenceVar, kind: TyVariableKind) -> Ty {
        match kind {
-            _ if self.inner[from_inference_var(iv).0 as usize].diverging => TyKind::Never,
+            _ if self.inner[iv.index() as usize].diverging => TyKind::Never,
            TyVariableKind::General => TyKind::Error,
            TyVariableKind::Integer => TyKind::Scalar(Scalar::Int(IntTy::I32)),
            TyVariableKind::Float => TyKind::Scalar(Scalar::Float(FloatTy::F64)),
@@ -237,27 +162,35 @@ pub(crate) struct TypeVariableData {
    diverging: bool,
 }
-#[derive(Clone, Debug)]
+type ChalkInferenceTable = chalk_solve::infer::InferenceTable<Interner>;
-pub(crate) struct InferenceTable {
-    pub(super) var_unification_table: InPlaceUnificationTable<TypeVarId>,
+#[derive(Clone)]
+pub(crate) struct InferenceTable<'a> {
+    db: &'a dyn HirDatabase,
+    trait_env: Arc<TraitEnvironment>,
+    pub(super) var_unification_table: ChalkInferenceTable,
    pub(super) type_variable_table: TypeVariableTable,
-    pub(super) revision: u32,
 }
-impl InferenceTable {
+impl<'a> InferenceTable<'a> {
-    pub(crate) fn new() -> Self {
+    pub(crate) fn new(db: &'a dyn HirDatabase, trait_env: Arc<TraitEnvironment>) -> Self {
        InferenceTable {
-            var_unification_table: InPlaceUnificationTable::new(),
+            db,
+            trait_env,
+            var_unification_table: ChalkInferenceTable::new(),
            type_variable_table: TypeVariableTable { inner: Vec::new() },
-            revision: 0,
        }
    }
    fn new_var(&mut self, kind: TyVariableKind, diverging: bool) -> Ty {
-        self.type_variable_table.push(TypeVariableData { diverging });
+        let var = self.var_unification_table.new_variable(UniverseIndex::ROOT);
-        let key = self.var_unification_table.new_key(TypeVarValue::Unknown);
+        self.type_variable_table.inner.extend(
-        assert_eq!(key.0 as usize, self.type_variable_table.inner.len() - 1);
+            (0..1 + var.index() as usize - self.type_variable_table.inner.len())
-        TyKind::InferenceVar(to_inference_var(key), kind).intern(&Interner)
+                .map(|_| TypeVariableData { diverging: false }),
+        );
+        assert_eq!(var.index() as usize, self.type_variable_table.inner.len() - 1);
+        self.type_variable_table.inner[var.index() as usize].diverging = diverging;
+        var.to_ty_with_kind(&Interner, kind)
    }
    pub(crate) fn new_type_var(&mut self) -> Ty {
@@ -280,240 +213,59 @@ impl InferenceTable {
        self.resolve_ty_completely_inner(&mut Vec::new(), ty)
    }
+    // FIXME get rid of this, instead resolve shallowly where necessary
    pub(crate) fn resolve_ty_as_possible(&mut self, ty: Ty) -> Ty {
        self.resolve_ty_as_possible_inner(&mut Vec::new(), ty)
    }
    pub(crate) fn unify(&mut self, ty1: &Ty, ty2: &Ty) -> bool {
-        self.unify_inner(ty1, ty2, 0)
+        let result = self.var_unification_table.relate(
-    }
+            &Interner,
+            &self.db,
-    pub(crate) fn unify_substs(
+            &self.trait_env.env,
-        &mut self,
+            chalk_ir::Variance::Invariant,
-        substs1: &Substitution,
+            ty1,
-        substs2: &Substitution,
+            ty2,
-        depth: usize,
+        );
-    ) -> bool {
+        let result = if let Ok(r) = result {
-        substs1.iter(&Interner).zip(substs2.iter(&Interner)).all(|(t1, t2)| {
+            r
-            self.unify_inner(t1.assert_ty_ref(&Interner), t2.assert_ty_ref(&Interner), depth)
-        })
-    }
-    fn unify_inner(&mut self, ty1: &Ty, ty2: &Ty, depth: usize) -> bool {
-        if depth > 1000 {
-            // prevent stackoverflows
-            panic!("infinite recursion in unification");
-        }
-        if ty1 == ty2 {
-            return true;
-        }
-        // try to resolve type vars first
-        let ty1 = self.resolve_ty_shallow(ty1);
-        let ty2 = self.resolve_ty_shallow(ty2);
-        if ty1.equals_ctor(&ty2) {
-            match (ty1.kind(&Interner), ty2.kind(&Interner)) {
-                (TyKind::Adt(_, substs1), TyKind::Adt(_, substs2))
-                | (TyKind::FnDef(_, substs1), TyKind::FnDef(_, substs2))
-                | (
-                    TyKind::Function(FnPointer { substitution: FnSubst(substs1), .. }),
-                    TyKind::Function(FnPointer { substitution: FnSubst(substs2), .. }),
-                )
-                | (TyKind::Tuple(_, substs1), TyKind::Tuple(_, substs2))
-                | (TyKind::OpaqueType(_, substs1), TyKind::OpaqueType(_, substs2))
-                | (TyKind::AssociatedType(_, substs1), TyKind::AssociatedType(_, substs2))
-                | (TyKind::Closure(.., substs1), TyKind::Closure(.., substs2)) => {
-                    self.unify_substs(substs1, substs2, depth + 1)
-                }
-                (TyKind::Array(ty1, c1), TyKind::Array(ty2, c2)) if c1 == c2 => {
-                    self.unify_inner(ty1, ty2, depth + 1)
-                }
-                (TyKind::Ref(_, _, ty1), TyKind::Ref(_, _, ty2))
-                | (TyKind::Raw(_, ty1), TyKind::Raw(_, ty2))
-                | (TyKind::Slice(ty1), TyKind::Slice(ty2)) => self.unify_inner(ty1, ty2, depth + 1),
-                _ => true, /* we checked equals_ctor already */
-            }
-        } else if let (TyKind::Closure(.., substs1), TyKind::Closure(.., substs2)) =
-            (ty1.kind(&Interner), ty2.kind(&Interner))
-        {
-            self.unify_substs(substs1, substs2, depth + 1)
        } else {
-            self.unify_inner_trivial(&ty1, &ty2, depth)
+            return false;
-        }
+        };
-    }
+        // TODO deal with new goals
+        true
-    pub(super) fn unify_inner_trivial(&mut self, ty1: &Ty, ty2: &Ty, depth: usize) -> bool {
-        match (ty1.kind(&Interner), ty2.kind(&Interner)) {
-            (TyKind::Error, _) | (_, TyKind::Error) => true,
-            (TyKind::Placeholder(p1), TyKind::Placeholder(p2)) if *p1 == *p2 => true,
-            (TyKind::Dyn(dyn1), TyKind::Dyn(dyn2))
-                if dyn1.bounds.skip_binders().interned().len()
-                    == dyn2.bounds.skip_binders().interned().len() =>
-            {
-                for (pred1, pred2) in dyn1
-                    .bounds
-                    .skip_binders()
-                    .interned()
-                    .iter()
-                    .zip(dyn2.bounds.skip_binders().interned().iter())
-                {
-                    if !self.unify_preds(pred1.skip_binders(), pred2.skip_binders(), depth + 1) {
-                        return false;
-                    }
-                }
-                true
-            }
-            (
-                TyKind::InferenceVar(tv1, TyVariableKind::General),
-                TyKind::InferenceVar(tv2, TyVariableKind::General),
-            )
-            | (
-                TyKind::InferenceVar(tv1, TyVariableKind::Integer),
-                TyKind::InferenceVar(tv2, TyVariableKind::Integer),
-            )
-            | (
-                TyKind::InferenceVar(tv1, TyVariableKind::Float),
-                TyKind::InferenceVar(tv2, TyVariableKind::Float),
-            ) if self.type_variable_table.is_diverging(*tv1)
-                == self.type_variable_table.is_diverging(*tv2) =>
-            {
-                // both type vars are unknown since we tried to resolve them
-                if !self
-                    .var_unification_table
-                    .unioned(from_inference_var(*tv1), from_inference_var(*tv2))
-                {
-                    self.var_unification_table
-                        .union(from_inference_var(*tv1), from_inference_var(*tv2));
-                    self.revision += 1;
-                }
-                true
-            }
-            // The order of MaybeNeverTypeVar matters here.
-            // Unifying MaybeNeverTypeVar and TypeVar will let the latter become MaybeNeverTypeVar.
-            // Unifying MaybeNeverTypeVar and other concrete type will let the former become it.
-            (TyKind::InferenceVar(tv, TyVariableKind::General), other)
-            | (other, TyKind::InferenceVar(tv, TyVariableKind::General))
-            | (
-                TyKind::InferenceVar(tv, TyVariableKind::Integer),
-                other @ TyKind::Scalar(Scalar::Int(_)),
-            )
-            | (
-                other @ TyKind::Scalar(Scalar::Int(_)),
-                TyKind::InferenceVar(tv, TyVariableKind::Integer),
-            )
-            | (
-                TyKind::InferenceVar(tv, TyVariableKind::Integer),
-                other @ TyKind::Scalar(Scalar::Uint(_)),
-            )
-            | (
-                other @ TyKind::Scalar(Scalar::Uint(_)),
-                TyKind::InferenceVar(tv, TyVariableKind::Integer),
-            )
-            | (
-                TyKind::InferenceVar(tv, TyVariableKind::Float),
-                other @ TyKind::Scalar(Scalar::Float(_)),
-            )
-            | (
-                other @ TyKind::Scalar(Scalar::Float(_)),
-                TyKind::InferenceVar(tv, TyVariableKind::Float),
-            ) => {
-                // the type var is unknown since we tried to resolve it
-                self.var_unification_table.union_value(
-                    from_inference_var(*tv),
-                    TypeVarValue::Known(other.clone().intern(&Interner)),
-                );
-                self.revision += 1;
-                true
-            }
-            _ => false,
-        }
-    }
-    fn unify_preds(&mut self, pred1: &WhereClause, pred2: &WhereClause, depth: usize) -> bool {
-        match (pred1, pred2) {
-            (WhereClause::Implemented(tr1), WhereClause::Implemented(tr2))
-                if tr1.trait_id == tr2.trait_id =>
-            {
-                self.unify_substs(&tr1.substitution, &tr2.substitution, depth + 1)
-            }
-            (
-                WhereClause::AliasEq(AliasEq { alias: alias1, ty: ty1 }),
-                WhereClause::AliasEq(AliasEq { alias: alias2, ty: ty2 }),
-            ) => {
-                let (substitution1, substitution2) = match (alias1, alias2) {
-                    (AliasTy::Projection(projection_ty1), AliasTy::Projection(projection_ty2))
-                        if projection_ty1.associated_ty_id == projection_ty2.associated_ty_id =>
-                    {
-                        (&projection_ty1.substitution, &projection_ty2.substitution)
-                    }
-                    (AliasTy::Opaque(opaque1), AliasTy::Opaque(opaque2))
-                        if opaque1.opaque_ty_id == opaque2.opaque_ty_id =>
-                    {
-                        (&opaque1.substitution, &opaque2.substitution)
-                    }
-                    _ => return false,
-                };
-                self.unify_substs(&substitution1, &substitution2, depth + 1)
-                    && self.unify_inner(&ty1, &ty2, depth + 1)
-            }
-            _ => false,
-        }
    }
    /// If `ty` is a type variable with known type, returns that type;
    /// otherwise, return ty.
+    // FIXME this could probably just return Ty
    pub(crate) fn resolve_ty_shallow<'b>(&mut self, ty: &'b Ty) -> Cow<'b, Ty> {
-        let mut ty = Cow::Borrowed(ty);
+        self.var_unification_table
-        // The type variable could resolve to a int/float variable. Hence try
+            .normalize_ty_shallow(&Interner, ty)
-        // resolving up to three times; each type of variable shouldn't occur
+            .map_or(Cow::Borrowed(ty), Cow::Owned)
-        // more than once
-        for i in 0..3 {
-            if i > 0 {
-                cov_mark::hit!(type_var_resolves_to_int_var);
-            }
-            match ty.kind(&Interner) {
-                TyKind::InferenceVar(tv, _) => {
-                    let inner = from_inference_var(*tv);
-                    match self.var_unification_table.inlined_probe_value(inner).known() {
-                        Some(known_ty) => {
-                            // The known_ty can't be a type var itself
-                            ty = Cow::Owned(known_ty.clone());
-                        }
-                        _ => return ty,
-                    }
-                }
-                _ => return ty,
-            }
-        }
-        log::error!("Inference variable still not resolved: {:?}", ty);
-        ty
    }
    /// Resolves the type as far as currently possible, replacing type variables
    /// by their known types. All types returned by the infer_* functions should
    /// be resolved as far as possible, i.e. contain no type variables with
    /// known type.
-    fn resolve_ty_as_possible_inner(&mut self, tv_stack: &mut Vec<TypeVarId>, ty: Ty) -> Ty {
+    fn resolve_ty_as_possible_inner(&mut self, tv_stack: &mut Vec<InferenceVar>, ty: Ty) -> Ty {
        fold_tys(
            ty,
            |ty, _| match ty.kind(&Interner) {
                &TyKind::InferenceVar(tv, kind) => {
-                    let inner = from_inference_var(tv);
+                    if tv_stack.contains(&tv) {
-                    if tv_stack.contains(&inner) {
                        cov_mark::hit!(type_var_cycles_resolve_as_possible);
                        // recursive type
                        return self.type_variable_table.fallback_value(tv, kind);
                    }
-                    if let Some(known_ty) =
+                    if let Some(known_ty) = self.var_unification_table.probe_var(tv) {
-                        self.var_unification_table.inlined_probe_value(inner).known()
-                    {
                        // known_ty may contain other variables that are known by now
-                        tv_stack.push(inner);
+                        tv_stack.push(tv);
-                        let result = self.resolve_ty_as_possible_inner(tv_stack, known_ty.clone());
+                        let result = self.resolve_ty_as_possible_inner(
+                            tv_stack,
+                            known_ty.assert_ty_ref(&Interner).clone(),
+                        );
                        tv_stack.pop();
                        result
                    } else {
@@ -528,23 +280,24 @@ impl InferenceTable {
    /// Resolves the type completely; type variables without known type are
    /// replaced by TyKind::Unknown.
-    fn resolve_ty_completely_inner(&mut self, tv_stack: &mut Vec<TypeVarId>, ty: Ty) -> Ty {
+    fn resolve_ty_completely_inner(&mut self, tv_stack: &mut Vec<InferenceVar>, ty: Ty) -> Ty {
+        // FIXME implement as a proper Folder, handle lifetimes and consts as well
        fold_tys(
            ty,
            |ty, _| match ty.kind(&Interner) {
                &TyKind::InferenceVar(tv, kind) => {
-                    let inner = from_inference_var(tv);
+                    if tv_stack.contains(&tv) {
-                    if tv_stack.contains(&inner) {
                        cov_mark::hit!(type_var_cycles_resolve_completely);
                        // recursive type
                        return self.type_variable_table.fallback_value(tv, kind);
                    }
-                    if let Some(known_ty) =
+                    if let Some(known_ty) = self.var_unification_table.probe_var(tv) {
-                        self.var_unification_table.inlined_probe_value(inner).known()
-                    {
                        // known_ty may contain other variables that are known by now
-                        tv_stack.push(inner);
+                        tv_stack.push(tv);
-                        let result = self.resolve_ty_completely_inner(tv_stack, known_ty.clone());
+                        let result = self.resolve_ty_completely_inner(
+                            tv_stack,
+                            known_ty.assert_ty_ref(&Interner).clone(),
+                        );
                        tv_stack.pop();
                        result
                    } else {
@@ -558,68 +311,10 @@ impl InferenceTable {
    }
 }
-/// The ID of a type variable.
+impl<'a> fmt::Debug for InferenceTable<'a> {
-#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-pub(super) struct TypeVarId(pub(super) u32);
+        f.debug_struct("InferenceTable")
+            .field("num_vars", &self.type_variable_table.inner.len())
-impl UnifyKey for TypeVarId {
+            .finish()
-    type Value = TypeVarValue;
-    fn index(&self) -> u32 {
-        self.0
-    }
-    fn from_index(i: u32) -> Self {
-        TypeVarId(i)
-    }
-    fn tag() -> &'static str {
-        "TypeVarId"
-    }
-}
-fn from_inference_var(var: InferenceVar) -> TypeVarId {
-    TypeVarId(var.index())
-}
-fn to_inference_var(TypeVarId(index): TypeVarId) -> InferenceVar {
-    index.into()
-}
-/// The value of a type variable: either we already know the type, or we don't
-/// know it yet.
-#[derive(Clone, PartialEq, Eq, Debug)]
-pub(super) enum TypeVarValue {
-    Known(Ty),
-    Unknown,
-}
-impl TypeVarValue {
-    fn known(&self) -> Option<&Ty> {
-        match self {
-            TypeVarValue::Known(ty) => Some(ty),
-            TypeVarValue::Unknown => None,
-        }
-    }
-}
-impl UnifyValue for TypeVarValue {
-    type Error = NoError;
-    fn unify_values(value1: &Self, value2: &Self) -> Result<Self, NoError> {
-        match (value1, value2) {
-            // We should never equate two type variables, both of which have
-            // known types. Instead, we recursively equate those types.
-            (TypeVarValue::Known(t1), TypeVarValue::Known(t2)) => panic!(
-                "equating two type variables, both of which have known types: {:?} and {:?}",
-                t1, t2
-            ),
-            // If one side is known, prefer that one.
-            (TypeVarValue::Known(..), TypeVarValue::Unknown) => Ok(value1.clone()),
-            (TypeVarValue::Unknown, TypeVarValue::Known(..)) => Ok(value2.clone()),
-            (TypeVarValue::Unknown, TypeVarValue::Unknown) => Ok(TypeVarValue::Unknown),
-        }
    }
 }
diff --git a/crates/hir_ty/src/method_resolution.rs b/crates/hir_ty/src/method_resolution.rs
index 48bbcfd9f..37e1f89d8 100644
--- a/crates/hir_ty/src/method_resolution.rs
+++ b/crates/hir_ty/src/method_resolution.rs
@@ -798,7 +798,8 @@ pub(crate) fn inherent_impl_substs(
        binders: CanonicalVarKinds::from_iter(&Interner, kinds),
        value: (self_ty_with_vars, self_ty.value.clone()),
    };
-    let substs = super::infer::unify(&tys)?;
+    let trait_env = Arc::new(TraitEnvironment::default()); // FIXME
+    let substs = super::infer::unify(db, trait_env, &tys)?;
    // We only want the substs for the vars we added, not the ones from self_ty.
    // Also, if any of the vars we added are still in there, we replace them by
    // Unknown. I think this can only really happen if self_ty contained