5 files changed, 848 insertions, 660 deletions

diff --git a/crates/hir_ty/src/infer/coerce.rs b/crates/hir_ty/src/infer/coerce.rs
index 1f463a425..765a02b1c 100644
--- a/crates/hir_ty/src/infer/coerce.rs
+++ b/crates/hir_ty/src/infer/coerce.rs
@@ -2,156 +2,414 @@
 //! happen in certain places, e.g. weakening `&mut` to `&` or deref coercions
 //! like going from `&Vec<T>` to `&[T]`.
 //!
-//! See: https://doc.rust-lang.org/nomicon/coercions.html
+//! See https://doc.rust-lang.org/nomicon/coercions.html and
+//! librustc_typeck/check/coercion.rs.
 
 use chalk_ir::{cast::Cast, Mutability, TyVariableKind};
-use hir_def::lang_item::LangItemTarget;
+use hir_def::{expr::ExprId, lang_item::LangItemTarget};
 
-use crate::{autoderef, Canonical, Interner, Solution, Ty, TyBuilder, TyExt, TyKind};
+use crate::{
+    autoderef, infer::TypeMismatch, static_lifetime, Canonical, DomainGoal, FnPointer, FnSig,
+    Interner, Solution, Substitution, Ty, TyBuilder, TyExt, TyKind,
+};
 
-use super::{InEnvironment, InferenceContext};
+use super::{InEnvironment, InferOk, InferResult, InferenceContext, TypeError};
 
 impl<'a> InferenceContext<'a> {
     /// Unify two types, but may coerce the first one to the second one
     /// using "implicit coercion rules" if needed.
     pub(super) fn coerce(&mut self, from_ty: &Ty, to_ty: &Ty) -> bool {
-        let from_ty = self.resolve_ty_shallow(from_ty).into_owned();
+        let from_ty = self.resolve_ty_shallow(from_ty);
         let to_ty = self.resolve_ty_shallow(to_ty);
-        self.coerce_inner(from_ty, &to_ty)
+        match self.coerce_inner(from_ty, &to_ty) {
+            Ok(result) => {
+                self.table.register_infer_ok(result);
+                true
+            }
+            Err(_) => {
+                // FIXME deal with error
+                false
+            }
+        }
     }
 
     /// Merge two types from different branches, with possible coercion.
     ///
     /// Mostly this means trying to coerce one to the other, but
-    ///  - if we have two function types for different functions, we need to
+    ///  - if we have two function types for different functions or closures, we need to
     ///    coerce both to function pointers;
     ///  - if we were concerned with lifetime subtyping, we'd need to look for a
     ///    least upper bound.
-    pub(super) fn coerce_merge_branch(&mut self, ty1: &Ty, ty2: &Ty) -> Ty {
-        if self.coerce(ty1, ty2) {
-            ty2.clone()
-        } else if self.coerce(ty2, ty1) {
+    pub(super) fn coerce_merge_branch(&mut self, id: Option<ExprId>, ty1: &Ty, ty2: &Ty) -> Ty {
+        let ty1 = self.resolve_ty_shallow(ty1);
+        let ty2 = self.resolve_ty_shallow(ty2);
+        // Special case: two function types. Try to coerce both to
+        // pointers to have a chance at getting a match. See
+        // https://github.com/rust-lang/rust/blob/7b805396bf46dce972692a6846ce2ad8481c5f85/src/librustc_typeck/check/coercion.rs#L877-L916
+        let sig = match (ty1.kind(&Interner), ty2.kind(&Interner)) {
+            (TyKind::FnDef(..), TyKind::FnDef(..))
+            | (TyKind::Closure(..), TyKind::FnDef(..))
+            | (TyKind::FnDef(..), TyKind::Closure(..))
+            | (TyKind::Closure(..), TyKind::Closure(..)) => {
+                // FIXME: we're ignoring safety here. To be more correct, if we have one FnDef and one Closure,
+                // we should be coercing the closure to a fn pointer of the safety of the FnDef
+                cov_mark::hit!(coerce_fn_reification);
+                let sig = ty1.callable_sig(self.db).expect("FnDef without callable sig");
+                Some(sig)
+            }
+            _ => None,
+        };
+        if let Some(sig) = sig {
+            let target_ty = TyKind::Function(sig.to_fn_ptr()).intern(&Interner);
+            let result1 = self.coerce_inner(ty1.clone(), &target_ty);
+            let result2 = self.coerce_inner(ty2.clone(), &target_ty);
+            if let (Ok(result1), Ok(result2)) = (result1, result2) {
+                self.table.register_infer_ok(result1);
+                self.table.register_infer_ok(result2);
+                return target_ty;
+            }
+        }
+
+        // It might not seem like it, but order is important here: ty1 is our
+        // "previous" type, ty2 is the "new" one being added. If the previous
+        // type is a type variable and the new one is `!`, trying it the other
+        // way around first would mean we make the type variable `!`, instead of
+        // just marking it as possibly diverging.
+        if self.coerce(&ty2, &ty1) {
             ty1.clone()
+        } else if self.coerce(&ty1, &ty2) {
+            ty2.clone()
         } else {
-            if let (TyKind::FnDef(..), TyKind::FnDef(..)) =
-                (ty1.kind(&Interner), ty2.kind(&Interner))
-            {
-                cov_mark::hit!(coerce_fn_reification);
-                // Special case: two function types. Try to coerce both to
-                // pointers to have a chance at getting a match. See
-                // https://github.com/rust-lang/rust/blob/7b805396bf46dce972692a6846ce2ad8481c5f85/src/librustc_typeck/check/coercion.rs#L877-L916
-                let sig1 = ty1.callable_sig(self.db).expect("FnDef without callable sig");
-                let sig2 = ty2.callable_sig(self.db).expect("FnDef without callable sig");
-                let ptr_ty1 = TyBuilder::fn_ptr(sig1);
-                let ptr_ty2 = TyBuilder::fn_ptr(sig2);
-                self.coerce_merge_branch(&ptr_ty1, &ptr_ty2)
-            } else {
-                cov_mark::hit!(coerce_merge_fail_fallback);
-                ty1.clone()
+            if let Some(id) = id {
+                self.result
+                    .type_mismatches
+                    .insert(id.into(), TypeMismatch { expected: ty1.clone(), actual: ty2.clone() });
             }
+            cov_mark::hit!(coerce_merge_fail_fallback);
+            ty1.clone()
         }
     }
 
-    fn coerce_inner(&mut self, mut from_ty: Ty, to_ty: &Ty) -> bool {
-        match (from_ty.kind(&Interner), to_ty.kind(&Interner)) {
-            // Never type will make type variable to fallback to Never Type instead of Unknown.
-            (TyKind::Never, TyKind::InferenceVar(tv, TyVariableKind::General)) => {
-                self.table.type_variable_table.set_diverging(*tv, true);
-                return true;
+    fn coerce_inner(&mut self, from_ty: Ty, to_ty: &Ty) -> InferResult {
+        if from_ty.is_never() {
+            // Subtle: If we are coercing from `!` to `?T`, where `?T` is an unbound
+            // type variable, we want `?T` to fallback to `!` if not
+            // otherwise constrained. An example where this arises:
+            //
+            //     let _: Option<?T> = Some({ return; });
+            //
+            // here, we would coerce from `!` to `?T`.
+            match to_ty.kind(&Interner) {
+                TyKind::InferenceVar(tv, TyVariableKind::General) => {
+                    self.table.set_diverging(*tv, true);
+                }
+                _ => {}
             }
-            (TyKind::Never, _) => return true,
+            return Ok(InferOk { goals: Vec::new() });
+        }
 
-            // Trivial cases, this should go after `never` check to
-            // avoid infer result type to be never
-            _ => {
-                if self.table.unify_inner_trivial(&from_ty, &to_ty, 0) {
-                    return true;
-                }
+        // Consider coercing the subtype to a DST
+        if let Ok(ret) = self.try_coerce_unsized(&from_ty, &to_ty) {
+            return Ok(ret);
+        }
+
+        // Examine the supertype and consider auto-borrowing.
+        match to_ty.kind(&Interner) {
+            TyKind::Raw(mt, _) => {
+                return self.coerce_ptr(from_ty, to_ty, *mt);
             }
+            TyKind::Ref(mt, _, _) => {
+                return self.coerce_ref(from_ty, to_ty, *mt);
+            }
+            _ => {}
         }
 
-        // Pointer weakening and function to pointer
-        match (from_ty.kind(&Interner), to_ty.kind(&Interner)) {
-            // `*mut T` -> `*const T`
-            (TyKind::Raw(_, inner), TyKind::Raw(m2 @ Mutability::Not, ..)) => {
-                from_ty = TyKind::Raw(*m2, inner.clone()).intern(&Interner);
+        match from_ty.kind(&Interner) {
+            TyKind::FnDef(..) => {
+                // Function items are coercible to any closure
+                // type; function pointers are not (that would
+                // require double indirection).
+                // Additionally, we permit coercion of function
+                // items to drop the unsafe qualifier.
+                self.coerce_from_fn_item(from_ty, to_ty)
             }
-            // `&mut T` -> `&T`
-            (TyKind::Ref(_, lt, inner), TyKind::Ref(m2 @ Mutability::Not, ..)) => {
-                from_ty = TyKind::Ref(*m2, lt.clone(), inner.clone()).intern(&Interner);
+            TyKind::Function(from_fn_ptr) => {
+                // We permit coercion of fn pointers to drop the
+                // unsafe qualifier.
+                self.coerce_from_fn_pointer(from_ty.clone(), from_fn_ptr, to_ty)
             }
-            // `&T` -> `*const T`
-            // `&mut T` -> `*mut T`/`*const T`
-            (TyKind::Ref(.., substs), &TyKind::Raw(m2 @ Mutability::Not, ..))
-            | (TyKind::Ref(Mutability::Mut, _, substs), &TyKind::Raw(m2, ..)) => {
-                from_ty = TyKind::Raw(m2, substs.clone()).intern(&Interner);
+            TyKind::Closure(_, from_substs) => {
+                // Non-capturing closures are coercible to
+                // function pointers or unsafe function pointers.
+                // It cannot convert closures that require unsafe.
+                self.coerce_closure_to_fn(from_ty.clone(), from_substs, to_ty)
             }
+            _ => {
+                // Otherwise, just use unification rules.
+                self.table.try_unify(&from_ty, to_ty)
+            }
+        }
+    }
 
-            // Illegal mutability conversion
-            (TyKind::Raw(Mutability::Not, ..), TyKind::Raw(Mutability::Mut, ..))
-            | (TyKind::Ref(Mutability::Not, ..), TyKind::Ref(Mutability::Mut, ..)) => return false,
+    fn coerce_ptr(&mut self, from_ty: Ty, to_ty: &Ty, to_mt: Mutability) -> InferResult {
+        let (_is_ref, from_mt, from_inner) = match from_ty.kind(&Interner) {
+            TyKind::Ref(mt, _, ty) => (true, mt, ty),
+            TyKind::Raw(mt, ty) => (false, mt, ty),
+            _ => return self.table.try_unify(&from_ty, to_ty),
+        };
 
-            // `{function_type}` -> `fn()`
-            (TyKind::FnDef(..), TyKind::Function { .. }) => match from_ty.callable_sig(self.db) {
-                None => return false,
-                Some(sig) => {
-                    from_ty = TyBuilder::fn_ptr(sig);
-                }
+        coerce_mutabilities(*from_mt, to_mt)?;
+
+        // Check that the types which they point at are compatible.
+        let from_raw = TyKind::Raw(to_mt, from_inner.clone()).intern(&Interner);
+        // FIXME: behavior differs based on is_ref once we're computing adjustments
+        self.table.try_unify(&from_raw, to_ty)
+    }
+
+    /// Reborrows `&mut A` to `&mut B` and `&(mut) A` to `&B`.
+    /// To match `A` with `B`, autoderef will be performed,
+    /// calling `deref`/`deref_mut` where necessary.
+    fn coerce_ref(&mut self, from_ty: Ty, to_ty: &Ty, to_mt: Mutability) -> InferResult {
+        match from_ty.kind(&Interner) {
+            TyKind::Ref(mt, _, _) => {
+                coerce_mutabilities(*mt, to_mt)?;
+            }
+            _ => return self.table.try_unify(&from_ty, to_ty),
+        };
+
+        // NOTE: this code is mostly copied and adapted from rustc, and
+        // currently more complicated than necessary, carrying errors around
+        // etc.. This complication will become necessary when we actually track
+        // details of coercion errors though, so I think it's useful to leave
+        // the structure like it is.
+
+        let canonicalized = self.canonicalize(from_ty.clone());
+        let autoderef = autoderef::autoderef(
+            self.db,
+            self.resolver.krate(),
+            InEnvironment {
+                goal: canonicalized.value.clone(),
+                environment: self.trait_env.env.clone(),
             },
+        );
+        let mut first_error = None;
+        let mut found = None;
 
-            (TyKind::Closure(.., substs), TyKind::Function { .. }) => {
-                from_ty = substs.at(&Interner, 0).assert_ty_ref(&Interner).clone();
+        for (autoderefs, referent_ty) in autoderef.enumerate() {
+            if autoderefs == 0 {
+                // Don't let this pass, otherwise it would cause
+                // &T to autoref to &&T.
+                continue;
             }
 
-            _ => {}
+            let referent_ty = canonicalized.decanonicalize_ty(referent_ty.value);
+
+            // At this point, we have deref'd `a` to `referent_ty`.  So
+            // imagine we are coercing from `&'a mut Vec<T>` to `&'b mut [T]`.
+            // In the autoderef loop for `&'a mut Vec<T>`, we would get
+            // three callbacks:
+            //
+            // - `&'a mut Vec<T>` -- 0 derefs, just ignore it
+            // - `Vec<T>` -- 1 deref
+            // - `[T]` -- 2 deref
+            //
+            // At each point after the first callback, we want to
+            // check to see whether this would match out target type
+            // (`&'b mut [T]`) if we autoref'd it. We can't just
+            // compare the referent types, though, because we still
+            // have to consider the mutability. E.g., in the case
+            // we've been considering, we have an `&mut` reference, so
+            // the `T` in `[T]` needs to be unified with equality.
+            //
+            // Therefore, we construct reference types reflecting what
+            // the types will be after we do the final auto-ref and
+            // compare those. Note that this means we use the target
+            // mutability [1], since it may be that we are coercing
+            // from `&mut T` to `&U`.
+            let lt = static_lifetime(); // FIXME: handle lifetimes correctly, see rustc
+            let derefd_from_ty = TyKind::Ref(to_mt, lt, referent_ty).intern(&Interner);
+            match self.table.try_unify(&derefd_from_ty, to_ty) {
+                Ok(result) => {
+                    found = Some(result);
+                    break;
+                }
+                Err(err) => {
+                    if first_error.is_none() {
+                        first_error = Some(err);
+                    }
+                }
+            }
         }
 
-        if let Some(ret) = self.try_coerce_unsized(&from_ty, &to_ty) {
-            return ret;
+        // Extract type or return an error. We return the first error
+        // we got, which should be from relating the "base" type
+        // (e.g., in example above, the failure from relating `Vec<T>`
+        // to the target type), since that should be the least
+        // confusing.
+        let result = match found {
+            Some(d) => d,
+            None => {
+                let err = first_error.expect("coerce_borrowed_pointer had no error");
+                return Err(err);
+            }
+        };
+
+        Ok(result)
+    }
+
+    /// Attempts to coerce from the type of a Rust function item into a function pointer.
+    fn coerce_from_fn_item(&mut self, from_ty: Ty, to_ty: &Ty) -> InferResult {
+        match to_ty.kind(&Interner) {
+            TyKind::Function(_) => {
+                let from_sig = from_ty.callable_sig(self.db).expect("FnDef had no sig");
+
+                // FIXME check ABI: Intrinsics are not coercible to function pointers
+                // FIXME Safe `#[target_feature]` functions are not assignable to safe fn pointers (RFC 2396)
+
+                // FIXME rustc normalizes assoc types in the sig here, not sure if necessary
+
+                let from_sig = from_sig.to_fn_ptr();
+                let from_fn_pointer = TyKind::Function(from_sig.clone()).intern(&Interner);
+                let ok = self.coerce_from_safe_fn(from_fn_pointer, &from_sig, to_ty)?;
+
+                Ok(ok)
+            }
+            _ => self.table.try_unify(&from_ty, to_ty),
         }
+    }
+
+    fn coerce_from_fn_pointer(
+        &mut self,
+        from_ty: Ty,
+        from_f: &FnPointer,
+        to_ty: &Ty,
+    ) -> InferResult {
+        self.coerce_from_safe_fn(from_ty, from_f, to_ty)
+    }
 
-        // Auto Deref if cannot coerce
-        match (from_ty.kind(&Interner), to_ty.kind(&Interner)) {
-            // FIXME: DerefMut
-            (TyKind::Ref(.., st1), TyKind::Ref(.., st2)) => {
-                self.unify_autoderef_behind_ref(st1, st2)
+    fn coerce_from_safe_fn(
+        &mut self,
+        from_ty: Ty,
+        from_fn_ptr: &FnPointer,
+        to_ty: &Ty,
+    ) -> InferResult {
+        if let TyKind::Function(to_fn_ptr) = to_ty.kind(&Interner) {
+            if let (chalk_ir::Safety::Safe, chalk_ir::Safety::Unsafe) =
+                (from_fn_ptr.sig.safety, to_fn_ptr.sig.safety)
+            {
+                let from_unsafe =
+                    TyKind::Function(safe_to_unsafe_fn_ty(from_fn_ptr.clone())).intern(&Interner);
+                return self.table.try_unify(&from_unsafe, to_ty);
             }
+        }
+        self.table.try_unify(&from_ty, to_ty)
+    }
 
-            // Otherwise, normal unify
-            _ => self.unify(&from_ty, to_ty),
+    /// Attempts to coerce from the type of a non-capturing closure into a
+    /// function pointer.
+    fn coerce_closure_to_fn(
+        &mut self,
+        from_ty: Ty,
+        from_substs: &Substitution,
+        to_ty: &Ty,
+    ) -> InferResult {
+        match to_ty.kind(&Interner) {
+            TyKind::Function(fn_ty) /* if from_substs is non-capturing (FIXME) */ => {
+                // We coerce the closure, which has fn type
+                //     `extern "rust-call" fn((arg0,arg1,...)) -> _`
+                // to
+                //     `fn(arg0,arg1,...) -> _`
+                // or
+                //     `unsafe fn(arg0,arg1,...) -> _`
+                let safety = fn_ty.sig.safety;
+                let pointer_ty = coerce_closure_fn_ty(from_substs, safety);
+                self.table.try_unify(&pointer_ty, to_ty)
+            }
+            _ => self.table.try_unify(&from_ty, to_ty),
         }
     }
 
     /// Coerce a type using `from_ty: CoerceUnsized<ty_ty>`
     ///
     /// See: https://doc.rust-lang.org/nightly/std/marker/trait.CoerceUnsized.html
-    fn try_coerce_unsized(&mut self, from_ty: &Ty, to_ty: &Ty) -> Option<bool> {
+    fn try_coerce_unsized(&mut self, from_ty: &Ty, to_ty: &Ty) -> InferResult {
+        // These 'if' statements require some explanation.
+        // The `CoerceUnsized` trait is special - it is only
+        // possible to write `impl CoerceUnsized<B> for A` where
+        // A and B have 'matching' fields. This rules out the following
+        // two types of blanket impls:
+        //
+        // `impl<T> CoerceUnsized<T> for SomeType`
+        // `impl<T> CoerceUnsized<SomeType> for T`
+        //
+        // Both of these trigger a special `CoerceUnsized`-related error (E0376)
+        //
+        // We can take advantage of this fact to avoid performing unecessary work.
+        // If either `source` or `target` is a type variable, then any applicable impl
+        // would need to be generic over the self-type (`impl<T> CoerceUnsized<SomeType> for T`)
+        // or generic over the `CoerceUnsized` type parameter (`impl<T> CoerceUnsized<T> for
+        // SomeType`).
+        //
+        // However, these are exactly the kinds of impls which are forbidden by
+        // the compiler! Therefore, we can be sure that coercion will always fail
+        // when either the source or target type is a type variable. This allows us
+        // to skip performing any trait selection, and immediately bail out.
+        if from_ty.is_ty_var() {
+            return Err(TypeError);
+        }
+        if to_ty.is_ty_var() {
+            return Err(TypeError);
+        }
+
+        // Handle reborrows before trying to solve `Source: CoerceUnsized<Target>`.
+        let coerce_from = match (from_ty.kind(&Interner), to_ty.kind(&Interner)) {
+            (TyKind::Ref(from_mt, _, from_inner), TyKind::Ref(to_mt, _, _)) => {
+                coerce_mutabilities(*from_mt, *to_mt)?;
+
+                let lt = static_lifetime();
+                TyKind::Ref(*to_mt, lt, from_inner.clone()).intern(&Interner)
+            }
+            (TyKind::Ref(from_mt, _, from_inner), TyKind::Raw(to_mt, _)) => {
+                coerce_mutabilities(*from_mt, *to_mt)?;
+
+                TyKind::Raw(*to_mt, from_inner.clone()).intern(&Interner)
+            }
+            _ => from_ty.clone(),
+        };
+
         let krate = self.resolver.krate().unwrap();
         let coerce_unsized_trait = match self.db.lang_item(krate, "coerce_unsized".into()) {
             Some(LangItemTarget::TraitId(trait_)) => trait_,
-            _ => return None,
+            _ => return Err(TypeError),
         };
 
         let trait_ref = {
             let b = TyBuilder::trait_ref(self.db, coerce_unsized_trait);
             if b.remaining() != 2 {
                 // The CoerceUnsized trait should have two generic params: Self and T.
-                return None;
+                return Err(TypeError);
             }
-            b.push(from_ty.clone()).push(to_ty.clone()).build()
+            b.push(coerce_from.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 = canonicalizer.canonicalize_obligation(goal);
+        let canonicalized = self.canonicalize(goal);
 
-        let solution = self.db.trait_solve(krate, canonicalized.value.clone())?;
+        // FIXME: rustc's coerce_unsized is more specialized -- it only tries to
+        // solve `CoerceUnsized` and `Unsize` goals at this point and leaves the
+        // rest for later. Also, there's some logic about sized type variables.
+        // Need to find out in what cases this is necessary
+        let solution = self
+            .db
+            .trait_solve(krate, canonicalized.value.clone().cast(&Interner))
+            .ok_or(TypeError)?;
 
         match solution {
             Solution::Unique(v) => {
                 canonicalized.apply_solution(
-                    self,
+                    &mut self.table,
                     Canonical {
                         binders: v.binders,
                         // FIXME handle constraints
@@ -159,38 +417,40 @@ impl<'a> InferenceContext<'a> {
                     },
                 );
             }
-            _ => return None,
+            // FIXME: should we accept ambiguous results here?
+            _ => return Err(TypeError),
         };
 
-        Some(true)
+        Ok(InferOk { goals: Vec::new() })
     }
+}
 
-    /// Unify `from_ty` to `to_ty` with optional auto Deref
-    ///
-    /// 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 to_ty = self.resolve_ty_shallow(&to_ty);
-        // FIXME: Auto DerefMut
-        for derefed_ty in autoderef::autoderef(
-            self.db,
-            self.resolver.krate(),
-            InEnvironment {
-                goal: canonicalized.value.clone(),
-                environment: self.trait_env.env.clone(),
-            },
-        ) {
-            let derefed_ty = canonicalized.decanonicalize_ty(derefed_ty.value);
-            let from_ty = self.resolve_ty_shallow(&derefed_ty);
-            // Stop when constructor matches.
-            if from_ty.equals_ctor(&to_ty) {
-                // It will not recurse to `coerce`.
-                return self.table.unify(&from_ty, &to_ty);
-            } else if self.table.unify_inner_trivial(&derefed_ty, &to_ty, 0) {
-                return true;
-            }
-        }
+fn coerce_closure_fn_ty(closure_substs: &Substitution, safety: chalk_ir::Safety) -> Ty {
+    let closure_sig = closure_substs.at(&Interner, 0).assert_ty_ref(&Interner).clone();
+    match closure_sig.kind(&Interner) {
+        TyKind::Function(fn_ty) => TyKind::Function(FnPointer {
+            num_binders: fn_ty.num_binders,
+            sig: FnSig { safety, ..fn_ty.sig },
+            substitution: fn_ty.substitution.clone(),
+        })
+        .intern(&Interner),
+        _ => TyKind::Error.intern(&Interner),
+    }
+}
+
+fn safe_to_unsafe_fn_ty(fn_ty: FnPointer) -> FnPointer {
+    FnPointer {
+        num_binders: fn_ty.num_binders,
+        sig: FnSig { safety: chalk_ir::Safety::Unsafe, ..fn_ty.sig },
+        substitution: fn_ty.substitution,
+    }
+}
 
-        false
+fn coerce_mutabilities(from: Mutability, to: Mutability) -> Result<(), TypeError> {
+    match (from, to) {
+        (Mutability::Mut, Mutability::Mut)
+        | (Mutability::Mut, Mutability::Not)
+        | (Mutability::Not, Mutability::Not) => Ok(()),
+        (Mutability::Not, Mutability::Mut) => Err(TypeError),
     }
 }
diff --git a/crates/hir_ty/src/infer/expr.rs b/crates/hir_ty/src/infer/expr.rs
index 7278faeec..08c05c67c 100644
--- a/crates/hir_ty/src/infer/expr.rs
+++ b/crates/hir_ty/src/infer/expr.rs
@@ -35,39 +35,43 @@ use super::{
 impl<'a> InferenceContext<'a> {
     pub(super) fn infer_expr(&mut self, tgt_expr: ExprId, expected: &Expectation) -> Ty {
         let ty = self.infer_expr_inner(tgt_expr, expected);
-        if ty.is_never() {
+        if self.resolve_ty_shallow(&ty).is_never() {
             // Any expression that produces a value of type `!` must have diverged
             self.diverges = Diverges::Always;
         }
-        let could_unify = self.unify(&ty, &expected.ty);
-        if !could_unify {
-            self.result.type_mismatches.insert(
-                tgt_expr.into(),
-                TypeMismatch { expected: expected.ty.clone(), actual: ty.clone() },
-            );
+        if let Some(expected_ty) = expected.only_has_type(&mut self.table) {
+            let could_unify = self.unify(&ty, &expected_ty);
+            if !could_unify {
+                self.result.type_mismatches.insert(
+                    tgt_expr.into(),
+                    TypeMismatch { expected: expected_ty.clone(), actual: ty.clone() },
+                );
+            }
         }
-        self.resolve_ty_as_possible(ty)
+        ty
     }
 
     /// Infer type of expression with possibly implicit coerce to the expected type.
     /// Return the type after possible coercion.
     pub(super) fn infer_expr_coerce(&mut self, expr: ExprId, expected: &Expectation) -> Ty {
         let ty = self.infer_expr_inner(expr, &expected);
-        let ty = if !self.coerce(&ty, &expected.coercion_target()) {
-            self.result.type_mismatches.insert(
-                expr.into(),
-                TypeMismatch { expected: expected.ty.clone(), actual: ty.clone() },
-            );
-            // Return actual type when type mismatch.
-            // This is needed for diagnostic when return type mismatch.
-            ty
-        } else if expected.coercion_target().is_unknown() {
-            ty
+        let ty = if let Some(target) = expected.only_has_type(&mut self.table) {
+            if !self.coerce(&ty, &target) {
+                self.result.type_mismatches.insert(
+                    expr.into(),
+                    TypeMismatch { expected: target.clone(), actual: ty.clone() },
+                );
+                // Return actual type when type mismatch.
+                // This is needed for diagnostic when return type mismatch.
+                ty
+            } else {
+                target.clone()
+            }
         } else {
-            expected.ty.clone()
+            ty
         };
 
-        self.resolve_ty_as_possible(ty)
+        ty
     }
 
     fn callable_sig_from_fn_trait(&mut self, ty: &Ty, num_args: usize) -> Option<(Vec<Ty>, Ty)> {
@@ -98,10 +102,10 @@ impl<'a> InferenceContext<'a> {
             goal: projection.trait_ref(self.db).cast(&Interner),
             environment: trait_env,
         };
-        let canonical = self.canonicalizer().canonicalize_obligation(obligation.clone());
-        if self.db.trait_solve(krate, canonical.value).is_some() {
+        let canonical = self.canonicalize(obligation.clone());
+        if self.db.trait_solve(krate, canonical.value.cast(&Interner)).is_some() {
             self.push_obligation(obligation.goal);
-            let return_ty = self.normalize_projection_ty(projection);
+            let return_ty = self.table.normalize_projection_ty(projection);
             Some((arg_tys, return_ty))
         } else {
             None
@@ -131,17 +135,21 @@ impl<'a> InferenceContext<'a> {
                 let condition_diverges = mem::replace(&mut self.diverges, Diverges::Maybe);
                 let mut both_arms_diverge = Diverges::Always;
 
+                let mut result_ty = self.table.new_type_var();
                 let then_ty = self.infer_expr_inner(*then_branch, &expected);
                 both_arms_diverge &= mem::replace(&mut self.diverges, Diverges::Maybe);
+                result_ty = self.coerce_merge_branch(Some(*then_branch), &result_ty, &then_ty);
                 let else_ty = match else_branch {
                     Some(else_branch) => self.infer_expr_inner(*else_branch, &expected),
                     None => TyBuilder::unit(),
                 };
                 both_arms_diverge &= self.diverges;
+                // FIXME: create a synthetic `else {}` so we have something to refer to here instead of None?
+                result_ty = self.coerce_merge_branch(*else_branch, &result_ty, &else_ty);
 
                 self.diverges = condition_diverges | both_arms_diverge;
 
-                self.coerce_merge_branch(&then_ty, &else_ty)
+                result_ty
             }
             Expr::Block { statements, tail, label, id: _ } => {
                 let old_resolver = mem::replace(
@@ -277,12 +285,13 @@ impl<'a> InferenceContext<'a> {
                 // Eagerly try to relate the closure type with the expected
                 // type, otherwise we often won't have enough information to
                 // infer the body.
-                self.coerce(&closure_ty, &expected.ty);
+                if let Some(t) = expected.only_has_type(&mut self.table) {
+                    self.coerce(&closure_ty, &t);
+                }
 
                 // Now go through the argument patterns
                 for (arg_pat, arg_ty) in args.iter().zip(sig_tys) {
-                    let resolved = self.resolve_ty_as_possible(arg_ty);
-                    self.infer_pat(*arg_pat, &resolved, BindingMode::default());
+                    self.infer_pat(*arg_pat, &arg_ty, BindingMode::default());
                 }
 
                 let prev_diverges = mem::replace(&mut self.diverges, Diverges::Maybe);
@@ -297,13 +306,13 @@ 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(),
                     InEnvironment {
                         goal: canonicalized.value.clone(),
-                        environment: self.trait_env.env.clone(),
+                        environment: self.table.trait_env.env.clone(),
                     },
                 );
                 let (param_tys, ret_ty): (Vec<Ty>, Ty) = derefs
@@ -350,7 +359,7 @@ impl<'a> InferenceContext<'a> {
 
                     let arm_ty = self.infer_expr_inner(arm.expr, &expected);
                     all_arms_diverge &= self.diverges;
-                    result_ty = self.coerce_merge_branch(&result_ty, &arm_ty);
+                    result_ty = self.coerce_merge_branch(Some(arm.expr), &result_ty, &arm_ty);
                 }
 
                 self.diverges = matchee_diverges | all_arms_diverge;
@@ -364,12 +373,6 @@ impl<'a> InferenceContext<'a> {
             }
             Expr::Continue { .. } => TyKind::Never.intern(&Interner),
             Expr::Break { expr, label } => {
-                let val_ty = if let Some(expr) = expr {
-                    self.infer_expr(*expr, &Expectation::none())
-                } else {
-                    TyBuilder::unit()
-                };
-
                 let last_ty =
                     if let Some(ctxt) = find_breakable(&mut self.breakables, label.as_ref()) {
                         ctxt.break_ty.clone()
@@ -377,7 +380,14 @@ impl<'a> InferenceContext<'a> {
                         self.err_ty()
                     };
 
-                let merged_type = self.coerce_merge_branch(&last_ty, &val_ty);
+                let val_ty = if let Some(expr) = expr {
+                    self.infer_expr(*expr, &Expectation::none())
+                } else {
+                    TyBuilder::unit()
+                };
+
+                // FIXME: create a synthetic `()` during lowering so we have something to refer to here?
+                let merged_type = self.coerce_merge_branch(*expr, &last_ty, &val_ty);
 
                 if let Some(ctxt) = find_breakable(&mut self.breakables, label.as_ref()) {
                     ctxt.break_ty = merged_type;
@@ -411,7 +421,9 @@ impl<'a> InferenceContext<'a> {
                     self.write_variant_resolution(tgt_expr.into(), variant);
                 }
 
-                self.unify(&ty, &expected.ty);
+                if let Some(t) = expected.only_has_type(&mut self.table) {
+                    self.unify(&ty, &t);
+                }
 
                 let substs = ty
                     .as_adt()
@@ -442,7 +454,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(),
@@ -514,6 +526,7 @@ impl<'a> InferenceContext<'a> {
                 self.resolve_associated_type(inner_ty, self.resolve_ops_try_ok())
             }
             Expr::Cast { expr, type_ref } => {
+                // FIXME: propagate the "castable to" expectation (and find a test case that shows this is necessary)
                 let _inner_ty = self.infer_expr_inner(*expr, &Expectation::none());
                 let cast_ty = self.make_ty(type_ref);
                 // FIXME check the cast...
@@ -521,15 +534,17 @@ impl<'a> InferenceContext<'a> {
             }
             Expr::Ref { expr, rawness, mutability } => {
                 let mutability = lower_to_chalk_mutability(*mutability);
-                let expectation = if let Some((exp_inner, exp_rawness, exp_mutability)) =
-                    &expected.ty.as_reference_or_ptr()
+                let expectation = if let Some((exp_inner, exp_rawness, exp_mutability)) = expected
+                    .only_has_type(&mut self.table)
+                    .as_ref()
+                    .and_then(|t| t.as_reference_or_ptr())
                 {
-                    if *exp_mutability == Mutability::Mut && mutability == Mutability::Not {
-                        // FIXME: throw type error - expected mut reference but found shared ref,
+                    if exp_mutability == Mutability::Mut && mutability == Mutability::Not {
+                        // FIXME: record type error - expected mut reference but found shared ref,
                         // which cannot be coerced
                     }
-                    if *exp_rawness == Rawness::Ref && *rawness == Rawness::RawPtr {
-                        // FIXME: throw type error - expected reference but found ptr,
+                    if exp_rawness == Rawness::Ref && *rawness == Rawness::RawPtr {
+                        // FIXME: record type error - expected reference but found ptr,
                         // which cannot be coerced
                     }
                     Expectation::rvalue_hint(Ty::clone(exp_inner))
@@ -556,10 +571,11 @@ impl<'a> InferenceContext<'a> {
             }
             Expr::UnaryOp { expr, op } => {
                 let inner_ty = self.infer_expr_inner(*expr, &Expectation::none());
+                let inner_ty = self.resolve_ty_shallow(&inner_ty);
                 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,
@@ -612,8 +628,10 @@ impl<'a> InferenceContext<'a> {
                         _ => Expectation::none(),
                     };
                     let lhs_ty = self.infer_expr(*lhs, &lhs_expectation);
+                    let lhs_ty = self.resolve_ty_shallow(&lhs_ty);
                     let rhs_expectation = op::binary_op_rhs_expectation(*op, lhs_ty.clone());
                     let rhs_ty = self.infer_expr(*rhs, &Expectation::has_type(rhs_expectation));
+                    let rhs_ty = self.resolve_ty_shallow(&rhs_ty);
 
                     let ret = op::binary_op_return_ty(*op, lhs_ty.clone(), rhs_ty.clone());
 
@@ -676,7 +694,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,
@@ -696,8 +714,12 @@ impl<'a> InferenceContext<'a> {
                 }
             }
             Expr::Tuple { exprs } => {
-                let mut tys = match expected.ty.kind(&Interner) {
-                    TyKind::Tuple(_, substs) => substs
+                let mut tys = match expected
+                    .only_has_type(&mut self.table)
+                    .as_ref()
+                    .map(|t| t.kind(&Interner))
+                {
+                    Some(TyKind::Tuple(_, substs)) => substs
                         .iter(&Interner)
                         .map(|a| a.assert_ty_ref(&Interner).clone())
                         .chain(repeat_with(|| self.table.new_type_var()))
@@ -713,14 +735,16 @@ impl<'a> InferenceContext<'a> {
                 TyKind::Tuple(tys.len(), Substitution::from_iter(&Interner, tys)).intern(&Interner)
             }
             Expr::Array(array) => {
-                let elem_ty = match expected.ty.kind(&Interner) {
-                    TyKind::Array(st, _) | TyKind::Slice(st) => st.clone(),
-                    _ => self.table.new_type_var(),
-                };
+                let elem_ty =
+                    match expected.to_option(&mut self.table).as_ref().map(|t| t.kind(&Interner)) {
+                        Some(TyKind::Array(st, _)) | Some(TyKind::Slice(st)) => st.clone(),
+                        _ => self.table.new_type_var(),
+                    };
 
                 let len = match array {
                     Array::ElementList(items) => {
                         for expr in items.iter() {
+                            // FIXME: use CoerceMany (coerce_merge_branch)
                             self.infer_expr_coerce(*expr, &Expectation::has_type(elem_ty.clone()));
                         }
                         Some(items.len() as u64)
@@ -785,7 +809,6 @@ impl<'a> InferenceContext<'a> {
         };
         // use a new type variable if we got unknown here
         let ty = self.insert_type_vars_shallow(ty);
-        let ty = self.resolve_ty_as_possible(ty);
         self.write_expr_ty(tgt_expr, ty.clone());
         ty
     }
@@ -813,7 +836,6 @@ impl<'a> InferenceContext<'a> {
                         }
                     }
 
-                    let ty = self.resolve_ty_as_possible(ty);
                     self.infer_pat(*pat, &ty, BindingMode::default());
                 }
                 Statement::Expr { expr, .. } => {
@@ -836,7 +858,9 @@ impl<'a> InferenceContext<'a> {
                 // we don't even make an attempt at coercion
                 self.table.new_maybe_never_var()
             } else {
-                self.coerce(&TyBuilder::unit(), &expected.coercion_target());
+                if let Some(t) = expected.only_has_type(&mut self.table) {
+                    self.coerce(&TyBuilder::unit(), &t);
+                }
                 TyBuilder::unit()
             }
         };
@@ -852,7 +876,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());
 
@@ -891,7 +915,8 @@ impl<'a> InferenceContext<'a> {
         };
         // Apply autoref so the below unification works correctly
         // FIXME: return correct autorefs from lookup_method
-        let actual_receiver_ty = match expected_receiver_ty.as_reference() {
+        let actual_receiver_ty = match self.resolve_ty_shallow(&expected_receiver_ty).as_reference()
+        {
             Some((_, lifetime, mutability)) => {
                 TyKind::Ref(mutability, lifetime, derefed_receiver_ty).intern(&Interner)
             }
@@ -971,6 +996,7 @@ impl<'a> InferenceContext<'a> {
     }
 
     fn register_obligations_for_call(&mut self, callable_ty: &Ty) {
+        let callable_ty = self.resolve_ty_shallow(&callable_ty);
         if let TyKind::FnDef(fn_def, parameters) = callable_ty.kind(&Interner) {
             let def: CallableDefId = from_chalk(self.db, *fn_def);
             let generic_predicates = self.db.generic_predicates(def.into());
diff --git a/crates/hir_ty/src/infer/pat.rs b/crates/hir_ty/src/infer/pat.rs
index b15f4977d..9c8e3b6ae 100644
--- a/crates/hir_ty/src/infer/pat.rs
+++ b/crates/hir_ty/src/infer/pat.rs
@@ -94,14 +94,15 @@ impl<'a> InferenceContext<'a> {
     pub(super) fn infer_pat(
         &mut self,
         pat: PatId,
-        mut expected: &Ty,
+        expected: &Ty,
         mut default_bm: BindingMode,
     ) -> Ty {
         let body = Arc::clone(&self.body); // avoid borrow checker problem
+        let mut expected = self.resolve_ty_shallow(expected);
 
         if is_non_ref_pat(&body, pat) {
             while let Some((inner, _lifetime, mutability)) = expected.as_reference() {
-                expected = inner;
+                expected = self.resolve_ty_shallow(inner);
                 default_bm = match default_bm {
                     BindingMode::Move => BindingMode::Ref(mutability),
                     BindingMode::Ref(Mutability::Not) => BindingMode::Ref(Mutability::Not),
@@ -147,9 +148,9 @@ impl<'a> InferenceContext<'a> {
             }
             Pat::Or(ref pats) => {
                 if let Some((first_pat, rest)) = pats.split_first() {
-                    let ty = self.infer_pat(*first_pat, expected, default_bm);
+                    let ty = self.infer_pat(*first_pat, &expected, default_bm);
                     for pat in rest {
-                        self.infer_pat(*pat, expected, default_bm);
+                        self.infer_pat(*pat, &expected, default_bm);
                     }
                     ty
                 } else {
@@ -173,13 +174,13 @@ impl<'a> InferenceContext<'a> {
             Pat::TupleStruct { path: p, args: subpats, ellipsis } => self.infer_tuple_struct_pat(
                 p.as_deref(),
                 subpats,
-                expected,
+                &expected,
                 default_bm,
                 pat,
                 *ellipsis,
             ),
             Pat::Record { path: p, args: fields, ellipsis: _ } => {
-                self.infer_record_pat(p.as_deref(), fields, expected, default_bm, pat)
+                self.infer_record_pat(p.as_deref(), fields, &expected, default_bm, pat)
             }
             Pat::Path(path) => {
                 // FIXME use correct resolver for the surrounding expression
@@ -193,7 +194,7 @@ impl<'a> InferenceContext<'a> {
                     BindingMode::convert(*mode)
                 };
                 let inner_ty = if let Some(subpat) = subpat {
-                    self.infer_pat(*subpat, expected, default_bm)
+                    self.infer_pat(*subpat, &expected, default_bm)
                 } else {
                     expected.clone()
                 };
@@ -206,7 +207,6 @@ impl<'a> InferenceContext<'a> {
                     }
                     BindingMode::Move => inner_ty.clone(),
                 };
-                let bound_ty = self.resolve_ty_as_possible(bound_ty);
                 self.write_pat_ty(pat, bound_ty);
                 return inner_ty;
             }
@@ -265,13 +265,12 @@ impl<'a> InferenceContext<'a> {
         };
         // use a new type variable if we got error type here
         let ty = self.insert_type_vars_shallow(ty);
-        if !self.unify(&ty, expected) {
+        if !self.unify(&ty, &expected) {
             self.result.type_mismatches.insert(
                 pat.into(),
                 TypeMismatch { expected: expected.clone(), actual: ty.clone() },
             );
         }
-        let ty = self.resolve_ty_as_possible(ty);
         self.write_pat_ty(pat, ty.clone());
         ty
     }
diff --git a/crates/hir_ty/src/infer/path.rs b/crates/hir_ty/src/infer/path.rs
index 495282eba..14c99eafd 100644
--- a/crates/hir_ty/src/infer/path.rs
+++ b/crates/hir_ty/src/infer/path.rs
@@ -65,7 +65,6 @@ impl<'a> InferenceContext<'a> {
         let typable: ValueTyDefId = match value {
             ValueNs::LocalBinding(pat) => {
                 let ty = self.result.type_of_pat.get(pat)?.clone();
-                let ty = self.resolve_ty_as_possible(ty);
                 return Some(ty);
             }
             ValueNs::FunctionId(it) => it.into(),
@@ -218,14 +217,14 @@ 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());
 
         method_resolution::iterate_method_candidates(
             &canonical_ty.value,
             self.db,
-            self.trait_env.clone(),
+            self.table.trait_env.clone(),
             krate,
             &traits_in_scope,
             None,
@@ -275,6 +274,7 @@ impl<'a> InferenceContext<'a> {
         name: &Name,
         id: ExprOrPatId,
     ) -> Option<(ValueNs, Option<Substitution>)> {
+        let ty = self.resolve_ty_shallow(ty);
         let (enum_id, subst) = match ty.as_adt() {
             Some((AdtId::EnumId(e), subst)) => (e, subst),
             _ => return None,
diff --git a/crates/hir_ty/src/infer/unify.rs b/crates/hir_ty/src/infer/unify.rs
index d8e0b4320..21d3fb54e 100644
--- a/crates/hir_ty/src/infer/unify.rs
+++ b/crates/hir_ty/src/infer/unify.rs
@@ -1,177 +1,95 @@
 //! Unification and canonicalization logic.
 
-use std::borrow::Cow;
+use std::{fmt, mem, sync::Arc};
 
 use chalk_ir::{
-    cast::Cast, fold::Fold, interner::HasInterner, FloatTy, IntTy, TyVariableKind, UniverseIndex,
-    VariableKind,
+    cast::Cast, fold::Fold, interner::HasInterner, zip::Zip, FloatTy, IntTy, TyVariableKind,
+    UniverseIndex,
 };
-use ena::unify::{InPlaceUnificationTable, NoError, UnifyKey, UnifyValue};
+use chalk_solve::infer::ParameterEnaVariableExt;
+use ena::unify::UnifyKey;
 
-use super::{DomainGoal, InferenceContext};
+use super::{InferOk, InferResult, InferenceContext, TypeError};
 use crate::{
-    fold_tys, static_lifetime, AliasEq, AliasTy, BoundVar, Canonical, CanonicalVarKinds,
-    DebruijnIndex, FnPointer, FnSubst, InEnvironment, InferenceVar, Interner, Scalar, Substitution,
-    Ty, TyExt, TyKind, WhereClause,
+    db::HirDatabase, fold_tys, static_lifetime, AliasEq, AliasTy, BoundVar, Canonical,
+    DebruijnIndex, GenericArg, Goal, Guidance, InEnvironment, InferenceVar, Interner, ProjectionTy,
+    Scalar, Solution, Substitution, TraitEnvironment, Ty, TyKind, VariableKind,
 };
 
 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() }
+        // try to resolve obligations before canonicalizing, since this might
+        // result in new knowledge about variables
+        self.resolve_obligations_as_possible();
+        self.table.canonicalize(t)
     }
 }
 
-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)]
+#[derive(Debug, Clone)]
 pub(super) struct Canonicalized<T>
 where
     T: HasInterner<Interner = Interner>,
 {
     pub(super) value: Canonical<T>,
-    free_vars: Vec<(InferenceVar, TyVariableKind)>,
-}
-
-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 })
-    }
+    free_vars: Vec<GenericArg>,
 }
 
 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];
-            TyKind::InferenceVar(v, k).intern(&Interner)
-        })
+        chalk_ir::Substitute::apply(&self.free_vars, ty, &Interner)
     }
 
     pub(super) fn apply_solution(
         &self,
-        ctx: &mut InferenceContext<'_>,
+        ctx: &mut InferenceTable,
         solution: Canonical<Substitution>,
     ) {
         // the solution may contain new variables, which we need to convert to new inference vars
         let new_vars = Substitution::from_iter(
             &Interner,
             solution.binders.iter(&Interner).map(|k| match k.kind {
-                VariableKind::Ty(TyVariableKind::General) => {
-                    ctx.table.new_type_var().cast(&Interner)
-                }
-                VariableKind::Ty(TyVariableKind::Integer) => {
-                    ctx.table.new_integer_var().cast(&Interner)
-                }
-                VariableKind::Ty(TyVariableKind::Float) => {
-                    ctx.table.new_float_var().cast(&Interner)
-                }
+                VariableKind::Ty(TyVariableKind::General) => ctx.new_type_var().cast(&Interner),
+                VariableKind::Ty(TyVariableKind::Integer) => ctx.new_integer_var().cast(&Interner),
+                VariableKind::Ty(TyVariableKind::Float) => ctx.new_float_var().cast(&Interner),
                 // Chalk can sometimes return new lifetime variables. We just use the static lifetime everywhere
                 VariableKind::Lifetime => static_lifetime().cast(&Interner),
                 _ => panic!("const variable in solution"),
             }),
         );
-        for (i, ty) in solution.value.iter(&Interner).enumerate() {
-            let (v, k) = 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);
+        for (i, v) in solution.value.iter(&Interner).enumerate() {
+            let var = self.free_vars[i].clone();
+            if let Some(ty) = v.ty(&Interner) {
+                // 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.clone(), &Interner));
+                ctx.unify(var.assert_ty_ref(&Interner), &ty);
+            } else {
+                let _ = ctx.try_unify(&var, &new_vars.apply(v.clone(), &Interner));
+            }
         }
     }
 }
 
-pub fn could_unify(t1: &Ty, t2: &Ty) -> bool {
-    InferenceTable::new().unify(t1, t2)
+pub fn could_unify(
+    db: &dyn HirDatabase,
+    env: Arc<TraitEnvironment>,
+    tys: &Canonical<(Ty, Ty)>,
+) -> bool {
+    unify(db, env, tys).is_some()
 }
 
-pub(crate) fn unify(tys: &Canonical<(Ty, Ty)>) -> Option<Substitution> {
-    let mut table = InferenceTable::new();
+pub(crate) fn unify(
+    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
@@ -187,77 +105,151 @@ pub(crate) fn unify(tys: &Canonical<(Ty, Ty)>) -> Option<Substitution> {
     }
     // default any type vars that weren't unified back to their original bound vars
     // (kind of hacky)
-    for (i, var) in vars.iter(&Interner).enumerate() {
-        let var = var.assert_ty_ref(&Interner);
-        if &*table.resolve_ty_shallow(var) == var {
-            table.unify(
-                var,
-                &TyKind::BoundVar(BoundVar::new(DebruijnIndex::INNERMOST, i)).intern(&Interner),
-            );
-        }
-    }
+    let find_var = |iv| {
+        vars.iter(&Interner).position(|v| match v.interned() {
+            chalk_ir::GenericArgData::Ty(ty) => ty.inference_var(&Interner),
+            chalk_ir::GenericArgData::Lifetime(lt) => lt.inference_var(&Interner),
+            chalk_ir::GenericArgData::Const(c) => c.inference_var(&Interner),
+        } == Some(iv))
+    };
+    let fallback = |iv, kind, default, binder| match kind {
+        chalk_ir::VariableKind::Ty(_ty_kind) => find_var(iv)
+            .map_or(default, |i| BoundVar::new(binder, i).to_ty(&Interner).cast(&Interner)),
+        chalk_ir::VariableKind::Lifetime => find_var(iv)
+            .map_or(default, |i| BoundVar::new(binder, i).to_lifetime(&Interner).cast(&Interner)),
+        chalk_ir::VariableKind::Const(ty) => find_var(iv)
+            .map_or(default, |i| BoundVar::new(binder, i).to_const(&Interner, ty).cast(&Interner)),
+    };
     Some(Substitution::from_iter(
         &Interner,
         vars.iter(&Interner)
-            .map(|v| table.resolve_ty_completely(v.assert_ty_ref(&Interner).clone())),
+            .map(|v| table.resolve_with_fallback(v.assert_ty_ref(&Interner).clone(), fallback)),
     ))
 }
 
-#[derive(Clone, Debug)]
-pub(super) struct TypeVariableTable {
-    inner: Vec<TypeVariableData>,
+#[derive(Copy, Clone, Debug)]
+pub(crate) struct TypeVariableData {
+    diverging: bool,
 }
 
-impl TypeVariableTable {
-    fn push(&mut self, data: TypeVariableData) {
-        self.inner.push(data);
+type ChalkInferenceTable = chalk_solve::infer::InferenceTable<Interner>;
+
+#[derive(Clone)]
+pub(crate) struct InferenceTable<'a> {
+    pub(crate) db: &'a dyn HirDatabase,
+    pub(crate) trait_env: Arc<TraitEnvironment>,
+    var_unification_table: ChalkInferenceTable,
+    type_variable_table: Vec<TypeVariableData>,
+    pending_obligations: Vec<Canonicalized<InEnvironment<Goal>>>,
+}
+
+impl<'a> InferenceTable<'a> {
+    pub(crate) fn new(db: &'a dyn HirDatabase, trait_env: Arc<TraitEnvironment>) -> Self {
+        InferenceTable {
+            db,
+            trait_env,
+            var_unification_table: ChalkInferenceTable::new(),
+            type_variable_table: Vec::new(),
+            pending_obligations: Vec::new(),
+        }
     }
 
-    pub(super) fn set_diverging(&mut self, iv: InferenceVar, diverging: bool) {
-        self.inner[from_inference_var(iv).0 as usize].diverging = diverging;
+    /// Chalk doesn't know about the `diverging` flag, so when it unifies two
+    /// type variables of which one is diverging, the chosen root might not be
+    /// diverging and we have no way of marking it as such at that time. This
+    /// function goes through all type variables and make sure their root is
+    /// marked as diverging if necessary, so that resolving them gives the right
+    /// result.
+    pub(super) fn propagate_diverging_flag(&mut self) {
+        for i in 0..self.type_variable_table.len() {
+            if !self.type_variable_table[i].diverging {
+                continue;
+            }
+            let v = InferenceVar::from(i as u32);
+            let root = self.var_unification_table.inference_var_root(v);
+            if let Some(data) = self.type_variable_table.get_mut(root.index() as usize) {
+                data.diverging = true;
+            }
+        }
     }
 
-    fn is_diverging(&mut self, iv: InferenceVar) -> bool {
-        self.inner[from_inference_var(iv).0 as usize].diverging
+    pub(super) fn set_diverging(&mut self, iv: InferenceVar, diverging: bool) {
+        self.type_variable_table[iv.index() as usize].diverging = 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
+                .type_variable_table
+                .get(iv.index() as usize)
+                .map_or(false, |data| data.diverging) =>
+            {
+                TyKind::Never
+            }
             TyVariableKind::General => TyKind::Error,
             TyVariableKind::Integer => TyKind::Scalar(Scalar::Int(IntTy::I32)),
             TyVariableKind::Float => TyKind::Scalar(Scalar::Float(FloatTy::F64)),
         }
         .intern(&Interner)
     }
-}
 
-#[derive(Copy, Clone, Debug)]
-pub(crate) struct TypeVariableData {
-    diverging: bool,
-}
+    pub(super) fn canonicalize<T: Fold<Interner> + HasInterner<Interner = Interner>>(
+        &mut self,
+        t: T,
+    ) -> Canonicalized<T::Result>
+    where
+        T::Result: HasInterner<Interner = Interner>,
+    {
+        let result = self.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 }
+    }
+
+    /// Recurses through the given type, normalizing associated types mentioned
+    /// in it by replacing them by type variables and registering obligations to
+    /// resolve later. This should be done once for every type we get from some
+    /// type annotation (e.g. from a let type annotation, field type or function
+    /// call). `make_ty` handles this already, but e.g. for field types we need
+    /// to do it as well.
+    pub(super) fn normalize_associated_types_in(&mut self, ty: Ty) -> Ty {
+        fold_tys(
+            ty,
+            |ty, _| match ty.kind(&Interner) {
+                TyKind::Alias(AliasTy::Projection(proj_ty)) => {
+                    self.normalize_projection_ty(proj_ty.clone())
+                }
+                _ => ty,
+            },
+            DebruijnIndex::INNERMOST,
+        )
+    }
 
-#[derive(Clone, Debug)]
-pub(crate) struct InferenceTable {
-    pub(super) var_unification_table: InPlaceUnificationTable<TypeVarId>,
-    pub(super) type_variable_table: TypeVariableTable,
-    pub(super) revision: u32,
-}
+    pub(super) fn normalize_projection_ty(&mut self, proj_ty: ProjectionTy) -> Ty {
+        let var = self.new_type_var();
+        let alias_eq = AliasEq { alias: AliasTy::Projection(proj_ty), ty: var.clone() };
+        let obligation = alias_eq.cast(&Interner);
+        self.register_obligation(obligation);
+        var
+    }
 
-impl InferenceTable {
-    pub(crate) fn new() -> Self {
-        InferenceTable {
-            var_unification_table: InPlaceUnificationTable::new(),
-            type_variable_table: TypeVariableTable { inner: Vec::new() },
-            revision: 0,
-        }
+    fn extend_type_variable_table(&mut self, to_index: usize) {
+        self.type_variable_table.extend(
+            (0..1 + to_index - self.type_variable_table.len())
+                .map(|_| TypeVariableData { diverging: false }),
+        );
     }
 
     fn new_var(&mut self, kind: TyVariableKind, diverging: bool) -> Ty {
-        self.type_variable_table.push(TypeVariableData { diverging });
-        let key = self.var_unification_table.new_key(TypeVarValue::Unknown);
-        assert_eq!(key.0 as usize, self.type_variable_table.inner.len() - 1);
-        TyKind::InferenceVar(to_inference_var(key), kind).intern(&Interner)
+        let var = self.var_unification_table.new_variable(UniverseIndex::ROOT);
+        // Chalk might have created some type variables for its own purposes that we don't know about...
+        self.extend_type_variable_table(var.index() as usize);
+        assert_eq!(var.index() as usize, self.type_variable_table.len() - 1);
+        self.type_variable_table[var.index() as usize].diverging = diverging;
+        var.to_ty_with_kind(&Interner, kind)
     }
 
     pub(crate) fn new_type_var(&mut self) -> Ty {
@@ -276,350 +268,261 @@ impl InferenceTable {
         self.new_var(TyVariableKind::General, true)
     }
 
-    pub(crate) fn resolve_ty_completely(&mut self, ty: Ty) -> Ty {
-        self.resolve_ty_completely_inner(&mut Vec::new(), ty)
+    pub(crate) fn resolve_with_fallback<T>(
+        &mut self,
+        t: T,
+        fallback: impl Fn(InferenceVar, VariableKind, GenericArg, DebruijnIndex) -> GenericArg,
+    ) -> T::Result
+    where
+        T: HasInterner<Interner = Interner> + Fold<Interner>,
+    {
+        self.resolve_with_fallback_inner(&mut Vec::new(), t, &fallback)
     }
 
-    pub(crate) fn resolve_ty_as_possible(&mut self, ty: Ty) -> Ty {
-        self.resolve_ty_as_possible_inner(&mut Vec::new(), ty)
+    fn resolve_with_fallback_inner<T>(
+        &mut self,
+        var_stack: &mut Vec<InferenceVar>,
+        t: T,
+        fallback: &impl Fn(InferenceVar, VariableKind, GenericArg, DebruijnIndex) -> GenericArg,
+    ) -> T::Result
+    where
+        T: HasInterner<Interner = Interner> + Fold<Interner>,
+    {
+        t.fold_with(
+            &mut resolve::Resolver { table: self, var_stack, fallback },
+            DebruijnIndex::INNERMOST,
+        )
+        .expect("fold failed unexpectedly")
     }
 
-    pub(crate) fn unify(&mut self, ty1: &Ty, ty2: &Ty) -> bool {
-        self.unify_inner(ty1, ty2, 0)
+    pub(crate) fn resolve_ty_completely(&mut self, ty: Ty) -> Ty {
+        self.resolve_with_fallback(ty, |_, _, d, _| d)
     }
 
-    pub(crate) fn unify_substs(
-        &mut self,
-        substs1: &Substitution,
-        substs2: &Substitution,
-        depth: usize,
-    ) -> bool {
-        substs1.iter(&Interner).zip(substs2.iter(&Interner)).all(|(t1, t2)| {
-            self.unify_inner(t1.assert_ty_ref(&Interner), t2.assert_ty_ref(&Interner), depth)
-        })
+    /// Unify two types and register new trait goals that arise from that.
+    pub(crate) fn unify(&mut self, ty1: &Ty, ty2: &Ty) -> bool {
+        let result = if let Ok(r) = self.try_unify(ty1, ty2) {
+            r
+        } else {
+            return false;
+        };
+        self.register_infer_ok(result);
+        true
     }
 
-    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)
+    /// Unify two types and return new trait goals arising from it, so the
+    /// caller needs to deal with them.
+    pub(crate) fn try_unify<T: Zip<Interner>>(&mut self, t1: &T, t2: &T) -> InferResult {
+        match self.var_unification_table.relate(
+            &Interner,
+            &self.db,
+            &self.trait_env.env,
+            chalk_ir::Variance::Invariant,
+            t1,
+            t2,
+        ) {
+            Ok(result) => Ok(InferOk { goals: result.goals }),
+            Err(chalk_ir::NoSolution) => Err(TypeError),
         }
     }
 
-    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,
+    /// If `ty` is a type variable with known type, returns that type;
+    /// otherwise, return ty.
+    pub(crate) fn resolve_ty_shallow(&mut self, ty: &Ty) -> Ty {
+        self.var_unification_table.normalize_ty_shallow(&Interner, ty).unwrap_or_else(|| ty.clone())
+    }
 
-            (TyKind::Placeholder(p1), TyKind::Placeholder(p2)) if *p1 == *p2 => true,
+    pub(crate) fn register_obligation(&mut self, goal: Goal) {
+        let in_env = InEnvironment::new(&self.trait_env.env, goal);
+        self.register_obligation_in_env(in_env)
+    }
 
-            (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
-            }
+    fn register_obligation_in_env(&mut self, goal: InEnvironment<Goal>) {
+        let canonicalized = self.canonicalize(goal);
+        if !self.try_resolve_obligation(&canonicalized) {
+            self.pending_obligations.push(canonicalized);
+        }
+    }
 
-            (
-                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
-            }
+    pub(crate) fn register_infer_ok(&mut self, infer_ok: InferOk) {
+        infer_ok.goals.into_iter().for_each(|goal| self.register_obligation_in_env(goal));
+    }
 
-            // 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)),
+    pub(crate) fn resolve_obligations_as_possible(&mut self) {
+        let _span = profile::span("resolve_obligations_as_possible");
+        let mut changed = true;
+        let mut obligations = Vec::new();
+        while changed {
+            changed = false;
+            mem::swap(&mut self.pending_obligations, &mut obligations);
+            for canonicalized in obligations.drain(..) {
+                if !self.check_changed(&canonicalized) {
+                    self.pending_obligations.push(canonicalized);
+                    continue;
+                }
+                changed = true;
+                let uncanonical = chalk_ir::Substitute::apply(
+                    &canonicalized.free_vars,
+                    canonicalized.value.value,
+                    &Interner,
                 );
-                self.revision += 1;
-                true
+                self.register_obligation_in_env(uncanonical);
             }
-
-            _ => 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)
+    /// This checks whether any of the free variables in the `canonicalized`
+    /// have changed (either been unified with another variable, or with a
+    /// value). If this is not the case, we don't need to try to solve the goal
+    /// again -- it'll give the same result as last time.
+    fn check_changed(&mut self, canonicalized: &Canonicalized<InEnvironment<Goal>>) -> bool {
+        canonicalized.free_vars.iter().any(|var| {
+            let iv = match var.data(&Interner) {
+                chalk_ir::GenericArgData::Ty(ty) => ty.inference_var(&Interner),
+                chalk_ir::GenericArgData::Lifetime(lt) => lt.inference_var(&Interner),
+                chalk_ir::GenericArgData::Const(c) => c.inference_var(&Interner),
             }
-            (
-                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)
+            .expect("free var is not inference var");
+            if self.var_unification_table.probe_var(iv).is_some() {
+                return true;
             }
-            _ => false,
-        }
+            let root = self.var_unification_table.inference_var_root(iv);
+            iv != root
+        })
     }
 
-    /// If `ty` is a type variable with known type, returns that type;
-    /// otherwise, return ty.
-    pub(crate) fn resolve_ty_shallow<'b>(&mut self, ty: &'b Ty) -> Cow<'b, Ty> {
-        let mut ty = Cow::Borrowed(ty);
-        // The type variable could resolve to a int/float variable. Hence try
-        // resolving up to three times; each type of variable shouldn't occur
-        // more than once
-        for i in 0..3 {
-            if i > 0 {
-                cov_mark::hit!(type_var_resolves_to_int_var);
+    fn try_resolve_obligation(
+        &mut self,
+        canonicalized: &Canonicalized<InEnvironment<Goal>>,
+    ) -> bool {
+        let solution = self.db.trait_solve(self.trait_env.krate, canonicalized.value.clone());
+
+        match solution {
+            Some(Solution::Unique(canonical_subst)) => {
+                canonicalized.apply_solution(
+                    self,
+                    Canonical {
+                        binders: canonical_subst.binders,
+                        // FIXME: handle constraints
+                        value: canonical_subst.value.subst,
+                    },
+                );
+                true
             }
-            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,
+            Some(Solution::Ambig(Guidance::Definite(substs))) => {
+                canonicalized.apply_solution(self, substs);
+                false
+            }
+            Some(_) => {
+                // FIXME use this when trying to resolve everything at the end
+                false
+            }
+            None => {
+                // FIXME obligation cannot be fulfilled => diagnostic
+                true
             }
         }
-        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 {
-        fold_tys(
-            ty,
-            |ty, _| match ty.kind(&Interner) {
-                &TyKind::InferenceVar(tv, kind) => {
-                    let inner = from_inference_var(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) =
-                        self.var_unification_table.inlined_probe_value(inner).known()
-                    {
-                        // known_ty may contain other variables that are known by now
-                        tv_stack.push(inner);
-                        let result = self.resolve_ty_as_possible_inner(tv_stack, known_ty.clone());
-                        tv_stack.pop();
-                        result
-                    } else {
-                        ty
-                    }
-                }
-                _ => ty,
-            },
-            DebruijnIndex::INNERMOST,
-        )
-    }
-
-    /// 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 {
-        fold_tys(
-            ty,
-            |ty, _| match ty.kind(&Interner) {
-                &TyKind::InferenceVar(tv, kind) => {
-                    let inner = from_inference_var(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) =
-                        self.var_unification_table.inlined_probe_value(inner).known()
-                    {
-                        // known_ty may contain other variables that are known by now
-                        tv_stack.push(inner);
-                        let result = self.resolve_ty_completely_inner(tv_stack, known_ty.clone());
-                        tv_stack.pop();
-                        result
-                    } else {
-                        self.type_variable_table.fallback_value(tv, kind)
-                    }
-                }
-                _ => ty,
-            },
-            DebruijnIndex::INNERMOST,
-        )
     }
 }
 
-/// The ID of a type variable.
-#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
-pub(super) struct TypeVarId(pub(super) u32);
-
-impl UnifyKey for TypeVarId {
-    type Value = TypeVarValue;
-
-    fn index(&self) -> u32 {
-        self.0
-    }
-
-    fn from_index(i: u32) -> Self {
-        TypeVarId(i)
+impl<'a> fmt::Debug for InferenceTable<'a> {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        f.debug_struct("InferenceTable").field("num_vars", &self.type_variable_table.len()).finish()
     }
-
-    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,
+mod resolve {
+    use super::InferenceTable;
+    use crate::{
+        ConcreteConst, Const, ConstData, ConstValue, DebruijnIndex, GenericArg, InferenceVar,
+        Interner, Ty, TyVariableKind, VariableKind,
+    };
+    use chalk_ir::{
+        cast::Cast,
+        fold::{Fold, Folder},
+        Fallible,
+    };
+    use hir_def::type_ref::ConstScalar;
+
+    pub(super) struct Resolver<'a, 'b, F> {
+        pub(super) table: &'a mut InferenceTable<'b>,
+        pub(super) var_stack: &'a mut Vec<InferenceVar>,
+        pub(super) fallback: F,
+    }
+    impl<'a, 'b, 'i, F> Folder<'i, Interner> for Resolver<'a, 'b, F>
+    where
+        F: Fn(InferenceVar, VariableKind, GenericArg, DebruijnIndex) -> GenericArg + 'i,
+    {
+        fn as_dyn(&mut self) -> &mut dyn Folder<'i, Interner> {
+            self
         }
-    }
-}
-
-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
-            ),
+        fn interner(&self) -> &'i Interner {
+            &Interner
+        }
 
-            // If one side is known, prefer that one.
-            (TypeVarValue::Known(..), TypeVarValue::Unknown) => Ok(value1.clone()),
-            (TypeVarValue::Unknown, TypeVarValue::Known(..)) => Ok(value2.clone()),
+        fn fold_inference_ty(
+            &mut self,
+            var: InferenceVar,
+            kind: TyVariableKind,
+            outer_binder: DebruijnIndex,
+        ) -> Fallible<Ty> {
+            let var = self.table.var_unification_table.inference_var_root(var);
+            if self.var_stack.contains(&var) {
+                // recursive type
+                let default = self.table.fallback_value(var, kind).cast(&Interner);
+                return Ok((self.fallback)(var, VariableKind::Ty(kind), default, outer_binder)
+                    .assert_ty_ref(&Interner)
+                    .clone());
+            }
+            let result = if let Some(known_ty) = self.table.var_unification_table.probe_var(var) {
+                // known_ty may contain other variables that are known by now
+                self.var_stack.push(var);
+                let result =
+                    known_ty.fold_with(self, outer_binder).expect("fold failed unexpectedly");
+                self.var_stack.pop();
+                result.assert_ty_ref(&Interner).clone()
+            } else {
+                let default = self.table.fallback_value(var, kind).cast(&Interner);
+                (self.fallback)(var, VariableKind::Ty(kind), default, outer_binder)
+                    .assert_ty_ref(&Interner)
+                    .clone()
+            };
+            Ok(result)
+        }
 
-            (TypeVarValue::Unknown, TypeVarValue::Unknown) => Ok(TypeVarValue::Unknown),
+        fn fold_inference_const(
+            &mut self,
+            ty: Ty,
+            var: InferenceVar,
+            outer_binder: DebruijnIndex,
+        ) -> Fallible<Const> {
+            let var = self.table.var_unification_table.inference_var_root(var);
+            let default = ConstData {
+                ty: ty.clone(),
+                value: ConstValue::Concrete(ConcreteConst { interned: ConstScalar::Unknown }),
+            }
+            .intern(&Interner)
+            .cast(&Interner);
+            if self.var_stack.contains(&var) {
+                // recursive
+                return Ok((self.fallback)(var, VariableKind::Const(ty), default, outer_binder)
+                    .assert_const_ref(&Interner)
+                    .clone());
+            }
+            let result = if let Some(known_ty) = self.table.var_unification_table.probe_var(var) {
+                // known_ty may contain other variables that are known by now
+                self.var_stack.push(var);
+                let result =
+                    known_ty.fold_with(self, outer_binder).expect("fold failed unexpectedly");
+                self.var_stack.pop();
+                result.assert_const_ref(&Interner).clone()
+            } else {
+                (self.fallback)(var, VariableKind::Const(ty), default, outer_binder)
+                    .assert_const_ref(&Interner)
+                    .clone()
+            };
+            Ok(result)
         }
     }
 }