Merge #1216

1216: Basic Chalk integration r=matklad a=flodiebold

This replaces the ad-hoc `implements` check by Chalk. It doesn't yet any new functionality (e.g. where clauses aren't passed to Chalk yet). The tests that exist actually work, but it needs some refactoring, currently crashes when running analysis on the RA repo, and depends on rust-lang/chalk#216 which isn't merged yet :smile: 

The main work here is converting stuff back and forth and providing Chalk with the information it needs, and the canonicalization logic. Since canonicalization depends a lot on the inference table, I don't think we can currently reuse the logic from Chalk, so we need to implement it ourselves; it's not actually that complicated anyway ;) I realized that we need a `Ty::Bound` variant separate from `Ty::Param` -- these are two different things, and I think type parameters inside a function actually need to be represented in Chalk as `Placeholder` types.

~~Currently this crashes in the 'real' world because we don't yet do canonicalization when filtering method candidates. Proper canonicalization needs the inference table (to collapse different inference variables that have already been unified), but we need to be able to call the method candidate selection from the completion code... So I'm currently thinking how to best handle that :smile:~~

Co-authored-by: Florian Diebold <[email protected]>

15 files changed, 905 insertions, 279 deletions

diff --git a/crates/ra_hir/Cargo.toml b/crates/ra_hir/Cargo.toml
index a2858dad9..68ffcb2e9 100644
--- a/crates/ra_hir/Cargo.toml
+++ b/crates/ra_hir/Cargo.toml
@@ -19,7 +19,11 @@ ra_db = { path = "../ra_db" }
 mbe = { path = "../ra_mbe", package = "ra_mbe" }
 tt = { path = "../ra_tt", package = "ra_tt" }
 test_utils = { path = "../test_utils" }
-ra_prof = {path = "../ra_prof" }
+ra_prof = { path = "../ra_prof" }
+
+chalk-solve = { git = "https://github.com/rust-lang/chalk.git" }
+chalk-rust-ir = { git = "https://github.com/rust-lang/chalk.git" }
+chalk-ir = { git = "https://github.com/rust-lang/chalk.git" }
 
 [dev-dependencies]
 flexi_logger = "0.11.0"
diff --git a/crates/ra_hir/src/code_model_api.rs b/crates/ra_hir/src/code_model_api.rs
index 8f1ed1086..9dcae50a5 100644
--- a/crates/ra_hir/src/code_model_api.rs
+++ b/crates/ra_hir/src/code_model_api.rs
@@ -9,7 +9,7 @@ use crate::{
     type_ref::TypeRef,
     nameres::{ModuleScope, Namespace, ImportId, CrateModuleId},
     expr::{Body, BodySourceMap},
-    ty::InferenceResult,
+    ty::{ TraitRef, InferenceResult},
     adt::{EnumVariantId, StructFieldId, VariantDef},
     generics::HasGenericParams,
     docs::{Documentation, Docs, docs_from_ast},
@@ -696,6 +696,10 @@ impl Trait {
         db.trait_data(self)
     }
 
+    pub fn trait_ref(self, db: &impl HirDatabase) -> TraitRef {
+        TraitRef::for_trait(db, self)
+    }
+
     pub(crate) fn resolver(&self, db: &impl DefDatabase) -> Resolver {
         let r = self.module(db).resolver(db);
         // add generic params, if present
diff --git a/crates/ra_hir/src/db.rs b/crates/ra_hir/src/db.rs
index 398e00c42..8aaf0375a 100644
--- a/crates/ra_hir/src/db.rs
+++ b/crates/ra_hir/src/db.rs
@@ -1,4 +1,4 @@
-use std::sync::Arc;
+use std::sync::{Arc, Mutex};
 
 use ra_syntax::{SyntaxNode, TreeArc, SourceFile, SmolStr, ast};
 use ra_db::{SourceDatabase, salsa};
@@ -8,16 +8,16 @@ use crate::{
     Function, FnSignature, ExprScopes, TypeAlias,
     Struct, Enum, StructField,
     Const, ConstSignature, Static,
-    DefWithBody,
+    DefWithBody, Trait,
+    ids,
     nameres::{Namespace, ImportSourceMap, RawItems, CrateDefMap},
-    ty::{InferenceResult, Ty, method_resolution::CrateImplBlocks, TypableDef, CallableDef, FnSig},
+    ty::{InferenceResult, Ty, method_resolution::CrateImplBlocks, TypableDef, CallableDef, FnSig, TypeCtor},
     adt::{StructData, EnumData},
-    impl_block::{ModuleImplBlocks, ImplSourceMap},
+    impl_block::{ModuleImplBlocks, ImplSourceMap, ImplBlock},
     generics::{GenericParams, GenericDef},
     type_ref::TypeRef,
-    traits::TraitData, Trait, ty::TraitRef,
+    traits::TraitData,
     lang_item::{LangItems, LangItemTarget},
-    ids
 };
 
 #[salsa::query_group(DefDatabaseStorage)]
@@ -39,6 +39,12 @@ pub trait DefDatabase: SourceDatabase {
     #[salsa::interned]
     fn intern_type_alias(&self, loc: ids::ItemLoc<ast::TypeAliasDef>) -> ids::TypeAliasId;
 
+    // Interned IDs for Chalk integration
+    #[salsa::interned]
+    fn intern_type_ctor(&self, type_ctor: TypeCtor) -> ids::TypeCtorId;
+    #[salsa::interned]
+    fn intern_impl_block(&self, impl_block: ImplBlock) -> ids::GlobalImplId;
+
     #[salsa::invoke(crate::ids::macro_def_query)]
     fn macro_def(&self, macro_id: MacroDefId) -> Option<Arc<mbe::MacroRules>>;
 
@@ -144,8 +150,17 @@ pub trait HirDatabase: DefDatabase {
     #[salsa::invoke(crate::ty::method_resolution::CrateImplBlocks::impls_in_crate_query)]
     fn impls_in_crate(&self, krate: Crate) -> Arc<CrateImplBlocks>;
 
-    #[salsa::invoke(crate::ty::traits::implements)]
-    fn implements(&self, trait_ref: TraitRef) -> Option<crate::ty::traits::Solution>;
+    #[salsa::invoke(crate::ty::traits::impls_for_trait)]
+    fn impls_for_trait(&self, krate: Crate, trait_: Trait) -> Arc<[ImplBlock]>;
+
+    /// This provides the Chalk trait solver instance. Because Chalk always
+    /// works from a specific crate, this query is keyed on the crate; and
+    /// because Chalk does its own internal caching, the solver is wrapped in a
+    /// Mutex and the query is marked volatile, to make sure the cached state is
+    /// thrown away when input facts change.
+    #[salsa::invoke(crate::ty::traits::solver)]
+    #[salsa::volatile]
+    fn solver(&self, krate: Crate) -> Arc<Mutex<crate::ty::traits::Solver>>;
 }
 
 #[test]
diff --git a/crates/ra_hir/src/generics.rs b/crates/ra_hir/src/generics.rs
index 1c71e21ea..2e52c5871 100644
--- a/crates/ra_hir/src/generics.rs
+++ b/crates/ra_hir/src/generics.rs
@@ -9,7 +9,7 @@ use ra_syntax::ast::{self, NameOwner, TypeParamsOwner, TypeBoundsOwner};
 
 use crate::{
     db::DefDatabase,
-    Name, AsName, Function, Struct, Enum, Trait, TypeAlias, ImplBlock, Container, path::Path, type_ref::TypeRef
+    Name, AsName, Function, Struct, Enum, Trait, TypeAlias, ImplBlock, Container, path::Path, type_ref::TypeRef, AdtDef
 };
 
 /// Data about a generic parameter (to a function, struct, impl, ...).
@@ -157,6 +157,15 @@ impl From<Container> for GenericDef {
     }
 }
 
+impl From<crate::adt::AdtDef> for GenericDef {
+    fn from(adt: crate::adt::AdtDef) -> Self {
+        match adt {
+            AdtDef::Struct(s) => s.into(),
+            AdtDef::Enum(e) => e.into(),
+        }
+    }
+}
+
 pub trait HasGenericParams {
     fn generic_params(self, db: &impl DefDatabase) -> Arc<GenericParams>;
 }
diff --git a/crates/ra_hir/src/ids.rs b/crates/ra_hir/src/ids.rs
index 4102951c9..ff4a81e59 100644
--- a/crates/ra_hir/src/ids.rs
+++ b/crates/ra_hir/src/ids.rs
@@ -354,3 +354,15 @@ impl MacroCallId {
         )
     }
 }
+
+/// This exists just for Chalk, because Chalk just has a single `StructId` where
+/// we have different kinds of ADTs, primitive types and special type
+/// constructors like tuples and function pointers.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
+pub struct TypeCtorId(salsa::InternId);
+impl_intern_key!(TypeCtorId);
+
+/// This exists just for Chalk, because our ImplIds are only unique per module.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
+pub struct GlobalImplId(salsa::InternId);
+impl_intern_key!(GlobalImplId);
diff --git a/crates/ra_hir/src/resolve.rs b/crates/ra_hir/src/resolve.rs
index bc9170cdc..707556ef8 100644
--- a/crates/ra_hir/src/resolve.rs
+++ b/crates/ra_hir/src/resolve.rs
@@ -6,7 +6,7 @@ use ra_syntax::ast;
 use rustc_hash::FxHashMap;
 
 use crate::{
-    ModuleDef,
+    ModuleDef, Trait,
     code_model_api::Crate,
     MacroCallId,
     MacroCallLoc,
@@ -18,7 +18,6 @@ use crate::{
     expr::{scope::{ExprScopes, ScopeId}, PatId},
     impl_block::ImplBlock,
     path::Path,
-    Trait,
 };
 
 #[derive(Debug, Clone, Default)]
diff --git a/crates/ra_hir/src/source_binder.rs b/crates/ra_hir/src/source_binder.rs
index 2959e3eca..2ec1a7692 100644
--- a/crates/ra_hir/src/source_binder.rs
+++ b/crates/ra_hir/src/source_binder.rs
@@ -350,7 +350,16 @@ impl SourceAnalyzer {
         name: Option<&Name>,
         callback: impl FnMut(&Ty, Function) -> Option<T>,
     ) -> Option<T> {
-        ty.iterate_method_candidates(db, &self.resolver, name, callback)
+        // There should be no inference vars in types passed here
+        // FIXME check that?
+        let canonical = crate::ty::Canonical { value: ty, num_vars: 0 };
+        crate::ty::method_resolution::iterate_method_candidates(
+            &canonical,
+            db,
+            &self.resolver,
+            name,
+            callback,
+        )
     }
 
     #[cfg(test)]
diff --git a/crates/ra_hir/src/ty.rs b/crates/ra_hir/src/ty.rs
index 12e10c751..f4eee835f 100644
--- a/crates/ra_hir/src/ty.rs
+++ b/crates/ra_hir/src/ty.rs
@@ -13,9 +13,10 @@ mod infer;
 pub(crate) mod display;
 
 use std::sync::Arc;
+use std::ops::Deref;
 use std::{fmt, mem};
 
-use crate::{Name, AdtDef, type_ref::Mutability, db::HirDatabase, Trait};
+use crate::{Name, AdtDef, type_ref::Mutability, db::HirDatabase, Trait, GenericParams};
 use display::{HirDisplay, HirFormatter};
 
 pub(crate) use lower::{TypableDef, type_for_def, type_for_field, callable_item_sig};
@@ -81,13 +82,13 @@ pub enum TypeCtor {
     /// fn foo() -> i32 { 1 }
     /// let bar: fn() -> i32 = foo;
     /// ```
-    FnPtr,
+    FnPtr { num_args: u16 },
 
     /// The never type `!`.
     Never,
 
     /// A tuple type.  For example, `(i32, bool)`.
-    Tuple,
+    Tuple { cardinality: u16 },
 }
 
 /// A nominal type with (maybe 0) type parameters. This might be a primitive
@@ -118,9 +119,14 @@ pub enum Ty {
         /// surrounding impl, then the current function).
         idx: u32,
         /// The name of the parameter, for displaying.
+        // FIXME get rid of this
         name: Name,
     },
 
+    /// A bound type variable. Only used during trait resolution to represent
+    /// Chalk variables.
+    Bound(u32),
+
     /// A type variable used during type checking. Not to be confused with a
     /// type parameter.
     Infer(InferTy),
@@ -150,14 +156,6 @@ impl Substs {
         Substs(self.0.iter().cloned().take(n).collect::<Vec<_>>().into())
     }
 
-    pub fn iter(&self) -> impl Iterator<Item = &Ty> {
-        self.0.iter()
-    }
-
-    pub fn len(&self) -> usize {
-        self.0.len()
-    }
-
     pub fn walk_mut(&mut self, f: &mut impl FnMut(&mut Ty)) {
         // Without an Arc::make_mut_slice, we can't avoid the clone here:
         let mut v: Vec<_> = self.0.iter().cloned().collect();
@@ -173,6 +171,30 @@ impl Substs {
         }
         &self.0[0]
     }
+
+    /// Return Substs that replace each parameter by itself (i.e. `Ty::Param`).
+    pub fn identity(generic_params: &GenericParams) -> Substs {
+        Substs(
+            generic_params
+                .params_including_parent()
+                .into_iter()
+                .map(|p| Ty::Param { idx: p.idx, name: p.name.clone() })
+                .collect::<Vec<_>>()
+                .into(),
+        )
+    }
+
+    /// Return Substs that replace each parameter by a bound variable.
+    pub fn bound_vars(generic_params: &GenericParams) -> Substs {
+        Substs(
+            generic_params
+                .params_including_parent()
+                .into_iter()
+                .map(|p| Ty::Bound(p.idx))
+                .collect::<Vec<_>>()
+                .into(),
+        )
+    }
 }
 
 impl From<Vec<Ty>> for Substs {
@@ -181,6 +203,14 @@ impl From<Vec<Ty>> for Substs {
     }
 }
 
+impl Deref for Substs {
+    type Target = [Ty];
+
+    fn deref(&self) -> &[Ty] {
+        &self.0
+    }
+}
+
 /// A trait with type parameters. This includes the `Self`, so this represents a concrete type implementing the trait.
 /// Name to be bikeshedded: TraitBound? TraitImplements?
 #[derive(Clone, PartialEq, Eq, Debug, Hash)]
@@ -192,10 +222,29 @@ pub struct TraitRef {
 
 impl TraitRef {
     pub fn self_ty(&self) -> &Ty {
-        &self.substs.0[0]
+        &self.substs[0]
+    }
+
+    pub fn subst(mut self, substs: &Substs) -> TraitRef {
+        self.substs.walk_mut(&mut |ty_mut| {
+            let ty = mem::replace(ty_mut, Ty::Unknown);
+            *ty_mut = ty.subst(substs);
+        });
+        self
     }
 }
 
+/// Basically a claim (currently not validated / checked) that the contained
+/// type / trait ref contains no inference variables; any inference variables it
+/// contained have been replaced by bound variables, and `num_vars` tells us how
+/// many there are. This is used to erase irrelevant differences between types
+/// before using them in queries.
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+pub(crate) struct Canonical<T> {
+    pub value: T,
+    pub num_vars: usize,
+}
+
 /// A function signature as seen by type inference: Several parameter types and
 /// one return type.
 #[derive(Clone, PartialEq, Eq, Debug)]
@@ -250,7 +299,7 @@ impl Ty {
         Ty::Apply(ApplicationTy { ctor, parameters })
     }
     pub fn unit() -> Self {
-        Ty::apply(TypeCtor::Tuple, Substs::empty())
+        Ty::apply(TypeCtor::Tuple { cardinality: 0 }, Substs::empty())
     }
 
     pub fn walk(&self, f: &mut impl FnMut(&Ty)) {
@@ -260,7 +309,7 @@ impl Ty {
                     t.walk(f);
                 }
             }
-            Ty::Param { .. } | Ty::Infer(_) | Ty::Unknown => {}
+            Ty::Param { .. } | Ty::Bound(_) | Ty::Infer(_) | Ty::Unknown => {}
         }
         f(self);
     }
@@ -270,7 +319,7 @@ impl Ty {
             Ty::Apply(a_ty) => {
                 a_ty.parameters.walk_mut(f);
             }
-            Ty::Param { .. } | Ty::Infer(_) | Ty::Unknown => {}
+            Ty::Param { .. } | Ty::Bound(_) | Ty::Infer(_) | Ty::Unknown => {}
         }
         f(self);
     }
@@ -303,7 +352,9 @@ impl Ty {
 
     pub fn as_tuple(&self) -> Option<&Substs> {
         match self {
-            Ty::Apply(ApplicationTy { ctor: TypeCtor::Tuple, parameters }) => Some(parameters),
+            Ty::Apply(ApplicationTy { ctor: TypeCtor::Tuple { .. }, parameters }) => {
+                Some(parameters)
+            }
             _ => None,
         }
     }
@@ -331,7 +382,7 @@ impl Ty {
     fn callable_sig(&self, db: &impl HirDatabase) -> Option<FnSig> {
         match self {
             Ty::Apply(a_ty) => match a_ty.ctor {
-                TypeCtor::FnPtr => Some(FnSig::from_fn_ptr_substs(&a_ty.parameters)),
+                TypeCtor::FnPtr { .. } => Some(FnSig::from_fn_ptr_substs(&a_ty.parameters)),
                 TypeCtor::FnDef(def) => {
                     let sig = db.callable_item_signature(def);
                     Some(sig.subst(&a_ty.parameters))
@@ -362,16 +413,20 @@ impl Ty {
     pub fn subst(self, substs: &Substs) -> Ty {
         self.fold(&mut |ty| match ty {
             Ty::Param { idx, name } => {
-                if (idx as usize) < substs.0.len() {
-                    substs.0[idx as usize].clone()
-                } else {
-                    Ty::Param { idx, name }
-                }
+                substs.get(idx as usize).cloned().unwrap_or(Ty::Param { idx, name })
             }
             ty => ty,
         })
     }
 
+    /// Substitutes `Ty::Bound` vars (as opposed to type parameters).
+    pub fn subst_bound_vars(self, substs: &Substs) -> Ty {
+        self.fold(&mut |ty| match ty {
+            Ty::Bound(idx) => substs.get(idx as usize).cloned().unwrap_or(Ty::Bound(idx)),
+            ty => ty,
+        })
+    }
+
     /// Returns the type parameters of this type if it has some (i.e. is an ADT
     /// or function); so if `self` is `Option<u32>`, this returns the `u32`.
     fn substs(&self) -> Option<Substs> {
@@ -413,17 +468,17 @@ impl HirDisplay for ApplicationTy {
                 write!(f, "&{}{}", m.as_keyword_for_ref(), t.display(f.db))?;
             }
             TypeCtor::Never => write!(f, "!")?,
-            TypeCtor::Tuple => {
+            TypeCtor::Tuple { .. } => {
                 let ts = &self.parameters;
-                if ts.0.len() == 1 {
-                    write!(f, "({},)", ts.0[0].display(f.db))?;
+                if ts.len() == 1 {
+                    write!(f, "({},)", ts[0].display(f.db))?;
                 } else {
                     write!(f, "(")?;
                     f.write_joined(&*ts.0, ", ")?;
                     write!(f, ")")?;
                 }
             }
-            TypeCtor::FnPtr => {
+            TypeCtor::FnPtr { .. } => {
                 let sig = FnSig::from_fn_ptr_substs(&self.parameters);
                 write!(f, "fn(")?;
                 f.write_joined(sig.params(), ", ")?;
@@ -440,7 +495,7 @@ impl HirDisplay for ApplicationTy {
                     CallableDef::Function(_) => write!(f, "fn {}", name)?,
                     CallableDef::Struct(_) | CallableDef::EnumVariant(_) => write!(f, "{}", name)?,
                 }
-                if self.parameters.0.len() > 0 {
+                if self.parameters.len() > 0 {
                     write!(f, "<")?;
                     f.write_joined(&*self.parameters.0, ", ")?;
                     write!(f, ">")?;
@@ -456,7 +511,7 @@ impl HirDisplay for ApplicationTy {
                 }
                 .unwrap_or_else(Name::missing);
                 write!(f, "{}", name)?;
-                if self.parameters.0.len() > 0 {
+                if self.parameters.len() > 0 {
                     write!(f, "<")?;
                     f.write_joined(&*self.parameters.0, ", ")?;
                     write!(f, ">")?;
@@ -472,6 +527,7 @@ impl HirDisplay for Ty {
         match self {
             Ty::Apply(a_ty) => a_ty.hir_fmt(f)?,
             Ty::Param { name, .. } => write!(f, "{}", name)?,
+            Ty::Bound(idx) => write!(f, "?{}", idx)?,
             Ty::Unknown => write!(f, "{{unknown}}")?,
             Ty::Infer(..) => write!(f, "_")?,
         }
diff --git a/crates/ra_hir/src/ty/infer.rs b/crates/ra_hir/src/ty/infer.rs
index c7772a7f6..edce1afe7 100644
--- a/crates/ra_hir/src/ty/infer.rs
+++ b/crates/ra_hir/src/ty/infer.rs
@@ -44,9 +44,12 @@ use crate::{
 };
 use super::{
     Ty, TypableDef, Substs, primitive, op, ApplicationTy, TypeCtor, CallableDef, TraitRef,
-    traits::{ Solution, Obligation, Guidance},
+    traits::{Solution, Obligation, Guidance},
+    method_resolution,
 };
 
+mod unify;
+
 /// The entry point of type inference.
 pub fn infer(db: &impl HirDatabase, def: DefWithBody) -> Arc<InferenceResult> {
     db.check_canceled();
@@ -321,30 +324,29 @@ impl<'a, D: HirDatabase> InferenceContext<'a, D> {
     fn resolve_obligations_as_possible(&mut self) {
         let obligations = mem::replace(&mut self.obligations, Vec::new());
         for obligation in obligations {
-            // FIXME resolve types in the obligation first
-            let (solution, var_mapping) = match &obligation {
+            let (solution, canonicalized) = match &obligation {
                 Obligation::Trait(tr) => {
-                    let (tr, var_mapping) = super::traits::canonicalize(tr.clone());
-                    (self.db.implements(tr), var_mapping)
+                    let canonicalized = self.canonicalizer().canonicalize_trait_ref(tr.clone());
+                    (
+                        super::traits::implements(
+                            self.db,
+                            self.resolver.krate().unwrap(),
+                            canonicalized.value.clone(),
+                        ),
+                        canonicalized,
+                    )
                 }
             };
             match solution {
                 Some(Solution::Unique(substs)) => {
-                    for (i, subst) in substs.0.iter().enumerate() {
-                        let uncanonical = var_mapping[i];
-                        // FIXME the subst may contain type variables, which would need to be mapped back as well
-                        self.unify(&Ty::Infer(InferTy::TypeVar(uncanonical)), subst);
-                    }
+                    canonicalized.apply_solution(self, substs.0);
                 }
                 Some(Solution::Ambig(Guidance::Definite(substs))) => {
-                    for (i, subst) in substs.0.iter().enumerate() {
-                        let uncanonical = var_mapping[i];
-                        // FIXME the subst may contain type variables, which would need to be mapped back as well
-                        self.unify(&Ty::Infer(InferTy::TypeVar(uncanonical)), subst);
-                    }
+                    canonicalized.apply_solution(self, substs.0);
                     self.obligations.push(obligation);
                 }
                 Some(_) => {
+                    // FIXME use this when trying to resolve everything at the end
                     self.obligations.push(obligation);
                 }
                 None => {
@@ -737,14 +739,14 @@ impl<'a, D: HirDatabase> InferenceContext<'a, D> {
                 };
                 let expectations_iter = expectations.iter().chain(repeat(&Ty::Unknown));
 
-                let inner_tys = args
+                let inner_tys: Substs = args
                     .iter()
                     .zip(expectations_iter)
                     .map(|(&pat, ty)| self.infer_pat(pat, ty, default_bm))
                     .collect::<Vec<_>>()
                     .into();
 
-                Ty::apply(TypeCtor::Tuple, Substs(inner_tys))
+                Ty::apply(TypeCtor::Tuple { cardinality: inner_tys.len() as u16 }, inner_tys)
             }
             Pat::Ref { pat, mutability } => {
                 let expectation = match expected.as_reference() {
@@ -877,9 +879,16 @@ impl<'a, D: HirDatabase> InferenceContext<'a, D> {
         generic_args: Option<&GenericArgs>,
     ) -> Ty {
         let receiver_ty = self.infer_expr(receiver, &Expectation::none());
-        let resolved = receiver_ty.clone().lookup_method(self.db, method_name, &self.resolver);
+        let canonicalized_receiver = self.canonicalizer().canonicalize_ty(receiver_ty.clone());
+        let resolved = method_resolution::lookup_method(
+            &canonicalized_receiver.value,
+            self.db,
+            method_name,
+            &self.resolver,
+        );
         let (derefed_receiver_ty, method_ty, def_generics) = match resolved {
             Some((ty, func)) => {
+                let ty = canonicalized_receiver.decanonicalize_ty(ty);
                 self.write_method_resolution(tgt_expr, func);
                 (
                     ty,
@@ -1064,7 +1073,7 @@ impl<'a, D: HirDatabase> InferenceContext<'a, D> {
                     .autoderef(self.db)
                     .find_map(|derefed_ty| match derefed_ty {
                         Ty::Apply(a_ty) => match a_ty.ctor {
-                            TypeCtor::Tuple => {
+                            TypeCtor::Tuple { .. } => {
                                 let i = name.to_string().parse::<usize>().ok();
                                 i.and_then(|i| a_ty.parameters.0.get(i).cloned())
                             }
@@ -1175,7 +1184,10 @@ impl<'a, D: HirDatabase> InferenceContext<'a, D> {
                     ty_vec.push(self.infer_expr(*arg, &Expectation::none()));
                 }
 
-                Ty::apply(TypeCtor::Tuple, Substs(ty_vec.into()))
+                Ty::apply(
+                    TypeCtor::Tuple { cardinality: ty_vec.len() as u16 },
+                    Substs(ty_vec.into()),
+                )
             }
             Expr::Array(array) => {
                 let elem_ty = match &expected.ty {
diff --git a/crates/ra_hir/src/ty/infer/unify.rs b/crates/ra_hir/src/ty/infer/unify.rs
new file mode 100644
index 000000000..8ca7e957d
--- /dev/null
+++ b/crates/ra_hir/src/ty/infer/unify.rs
@@ -0,0 +1,122 @@
+//! Unification and canonicalization logic.
+
+use crate::db::HirDatabase;
+use crate::ty::{Ty, Canonical, TraitRef, InferTy};
+use super::InferenceContext;
+
+impl<'a, D: HirDatabase> InferenceContext<'a, D> {
+    pub(super) fn canonicalizer<'b>(&'b mut self) -> Canonicalizer<'a, 'b, D>
+    where
+        'a: 'b,
+    {
+        Canonicalizer { ctx: self, free_vars: Vec::new(), var_stack: Vec::new() }
+    }
+}
+
+pub(super) struct Canonicalizer<'a, 'b, D: HirDatabase>
+where
+    'a: 'b,
+{
+    ctx: &'b mut InferenceContext<'a, D>,
+    free_vars: Vec<InferTy>,
+    /// 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<super::TypeVarId>,
+}
+
+pub(super) struct Canonicalized<T> {
+    pub value: Canonical<T>,
+    free_vars: Vec<InferTy>,
+}
+
+impl<'a, 'b, D: HirDatabase> Canonicalizer<'a, 'b, D>
+where
+    'a: 'b,
+{
+    fn add(&mut self, free_var: InferTy) -> 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);
+            next_index
+        })
+    }
+
+    fn do_canonicalize_ty(&mut self, ty: Ty) -> Ty {
+        ty.fold(&mut |ty| match ty {
+            Ty::Infer(tv) => {
+                let inner = tv.to_inner();
+                if self.var_stack.contains(&inner) {
+                    // recursive type
+                    return tv.fallback_value();
+                }
+                if let Some(known_ty) = self.ctx.var_unification_table.probe_value(inner).known() {
+                    self.var_stack.push(inner);
+                    let result = self.do_canonicalize_ty(known_ty.clone());
+                    self.var_stack.pop();
+                    result
+                } else {
+                    let free_var = InferTy::TypeVar(self.ctx.var_unification_table.find(inner));
+                    let position = self.add(free_var);
+                    Ty::Bound(position as u32)
+                }
+            }
+            _ => ty,
+        })
+    }
+
+    fn do_canonicalize_trait_ref(&mut self, trait_ref: TraitRef) -> TraitRef {
+        let substs = trait_ref
+            .substs
+            .iter()
+            .map(|ty| self.do_canonicalize_ty(ty.clone()))
+            .collect::<Vec<_>>();
+        TraitRef { trait_: trait_ref.trait_, substs: substs.into() }
+    }
+
+    fn into_canonicalized<T>(self, result: T) -> Canonicalized<T> {
+        Canonicalized {
+            value: Canonical { value: result, num_vars: self.free_vars.len() },
+            free_vars: self.free_vars,
+        }
+    }
+
+    pub fn canonicalize_ty(mut self, ty: Ty) -> Canonicalized<Ty> {
+        let result = self.do_canonicalize_ty(ty);
+        self.into_canonicalized(result)
+    }
+
+    pub fn canonicalize_trait_ref(mut self, trait_ref: TraitRef) -> Canonicalized<TraitRef> {
+        let result = self.do_canonicalize_trait_ref(trait_ref);
+        self.into_canonicalized(result)
+    }
+}
+
+impl<T> Canonicalized<T> {
+    pub fn decanonicalize_ty(&self, ty: Ty) -> Ty {
+        ty.fold(&mut |ty| match ty {
+            Ty::Bound(idx) => {
+                if (idx as usize) < self.free_vars.len() {
+                    Ty::Infer(self.free_vars[idx as usize].clone())
+                } else {
+                    Ty::Bound(idx)
+                }
+            }
+            ty => ty,
+        })
+    }
+
+    pub fn apply_solution(
+        &self,
+        ctx: &mut InferenceContext<'_, impl HirDatabase>,
+        solution: Canonical<Vec<Ty>>,
+    ) {
+        // the solution may contain new variables, which we need to convert to new inference vars
+        let new_vars =
+            (0..solution.num_vars).map(|_| ctx.new_type_var()).collect::<Vec<_>>().into();
+        for (i, ty) in solution.value.into_iter().enumerate() {
+            let var = self.free_vars[i].clone();
+            ctx.unify(&Ty::Infer(var), &ty.subst_bound_vars(&new_vars));
+        }
+    }
+}
diff --git a/crates/ra_hir/src/ty/lower.rs b/crates/ra_hir/src/ty/lower.rs
index 7fac084ce..8bab7e54b 100644
--- a/crates/ra_hir/src/ty/lower.rs
+++ b/crates/ra_hir/src/ty/lower.rs
@@ -29,7 +29,10 @@ impl Ty {
             TypeRef::Tuple(inner) => {
                 let inner_tys =
                     inner.iter().map(|tr| Ty::from_hir(db, resolver, tr)).collect::<Vec<_>>();
-                Ty::apply(TypeCtor::Tuple, Substs(inner_tys.into()))
+                Ty::apply(
+                    TypeCtor::Tuple { cardinality: inner_tys.len() as u16 },
+                    Substs(inner_tys.into()),
+                )
             }
             TypeRef::Path(path) => Ty::from_hir_path(db, resolver, path),
             TypeRef::RawPtr(inner, mutability) => {
@@ -53,7 +56,7 @@ impl Ty {
                 let inner_tys =
                     params.iter().map(|tr| Ty::from_hir(db, resolver, tr)).collect::<Vec<_>>();
                 let sig = Substs(inner_tys.into());
-                Ty::apply(TypeCtor::FnPtr, sig)
+                Ty::apply(TypeCtor::FnPtr { num_args: sig.len() as u16 - 1 }, sig)
             }
             TypeRef::Error => Ty::Unknown,
         }
@@ -238,6 +241,11 @@ impl TraitRef {
         let segment = path.segments.last().expect("path should have at least one segment");
         substs_from_path_segment(db, resolver, segment, &resolved.generic_params(db), true)
     }
+
+    pub(crate) fn for_trait(db: &impl HirDatabase, trait_: Trait) -> TraitRef {
+        let substs = Substs::identity(&trait_.generic_params(db));
+        TraitRef { trait_, substs }
+    }
 }
 
 /// Build the declared type of an item. This depends on the namespace; e.g. for
@@ -299,7 +307,7 @@ fn fn_sig_for_fn(db: &impl HirDatabase, def: Function) -> FnSig {
 /// function body.
 fn type_for_fn(db: &impl HirDatabase, def: Function) -> Ty {
     let generics = def.generic_params(db);
-    let substs = make_substs(&generics);
+    let substs = Substs::identity(&generics);
     Ty::apply(TypeCtor::FnDef(def.into()), substs)
 }
 
@@ -341,7 +349,7 @@ fn type_for_struct_constructor(db: &impl HirDatabase, def: Struct) -> Ty {
         return type_for_struct(db, def); // Unit struct
     }
     let generics = def.generic_params(db);
-    let substs = make_substs(&generics);
+    let substs = Substs::identity(&generics);
     Ty::apply(TypeCtor::FnDef(def.into()), substs)
 }
 
@@ -357,7 +365,7 @@ fn fn_sig_for_enum_variant_constructor(db: &impl HirDatabase, def: EnumVariant)
         .map(|(_, field)| Ty::from_hir(db, &resolver, &field.type_ref))
         .collect::<Vec<_>>();
     let generics = def.parent_enum(db).generic_params(db);
-    let substs = make_substs(&generics);
+    let substs = Substs::identity(&generics);
     let ret = type_for_enum(db, def.parent_enum(db)).subst(&substs);
     FnSig::from_params_and_return(params, ret)
 }
@@ -369,36 +377,25 @@ fn type_for_enum_variant_constructor(db: &impl HirDatabase, def: EnumVariant) ->
         return type_for_enum(db, def.parent_enum(db)); // Unit variant
     }
     let generics = def.parent_enum(db).generic_params(db);
-    let substs = make_substs(&generics);
+    let substs = Substs::identity(&generics);
     Ty::apply(TypeCtor::FnDef(def.into()), substs)
 }
 
-fn make_substs(generics: &GenericParams) -> Substs {
-    Substs(
-        generics
-            .params_including_parent()
-            .into_iter()
-            .map(|p| Ty::Param { idx: p.idx, name: p.name.clone() })
-            .collect::<Vec<_>>()
-            .into(),
-    )
-}
-
 fn type_for_struct(db: &impl HirDatabase, s: Struct) -> Ty {
     let generics = s.generic_params(db);
-    Ty::apply(TypeCtor::Adt(s.into()), make_substs(&generics))
+    Ty::apply(TypeCtor::Adt(s.into()), Substs::identity(&generics))
 }
 
 fn type_for_enum(db: &impl HirDatabase, s: Enum) -> Ty {
     let generics = s.generic_params(db);
-    Ty::apply(TypeCtor::Adt(s.into()), make_substs(&generics))
+    Ty::apply(TypeCtor::Adt(s.into()), Substs::identity(&generics))
 }
 
 fn type_for_type_alias(db: &impl HirDatabase, t: TypeAlias) -> Ty {
     let generics = t.generic_params(db);
     let resolver = t.resolver(db);
     let type_ref = t.type_ref(db);
-    let substs = make_substs(&generics);
+    let substs = Substs::identity(&generics);
     let inner = Ty::from_hir(db, &resolver, &type_ref);
     inner.subst(&substs)
 }
diff --git a/crates/ra_hir/src/ty/method_resolution.rs b/crates/ra_hir/src/ty/method_resolution.rs
index ea6e0dc0f..607e9ba79 100644
--- a/crates/ra_hir/src/ty/method_resolution.rs
+++ b/crates/ra_hir/src/ty/method_resolution.rs
@@ -16,7 +16,7 @@ use crate::{
     generics::HasGenericParams,
     ty::primitive::{UncertainIntTy, UncertainFloatTy}
 };
-use super::{TraitRef, Substs};
+use super::{TraitRef, Canonical};
 
 /// This is used as a key for indexing impls.
 #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
@@ -130,124 +130,122 @@ fn def_crate(db: &impl HirDatabase, cur_crate: Crate, ty: &Ty) -> Option<Crate>
     }
 }
 
-impl Ty {
-    /// Look up the method with the given name, returning the actual autoderefed
-    /// receiver type (but without autoref applied yet).
-    pub(crate) fn lookup_method(
-        self,
-        db: &impl HirDatabase,
-        name: &Name,
-        resolver: &Resolver,
-    ) -> Option<(Ty, Function)> {
-        self.iterate_method_candidates(db, resolver, Some(name), |ty, f| Some((ty.clone(), f)))
-    }
+/// Look up the method with the given name, returning the actual autoderefed
+/// receiver type (but without autoref applied yet).
+pub(crate) fn lookup_method(
+    ty: &Canonical<Ty>,
+    db: &impl HirDatabase,
+    name: &Name,
+    resolver: &Resolver,
+) -> Option<(Ty, Function)> {
+    iterate_method_candidates(ty, db, resolver, Some(name), |ty, f| Some((ty.clone(), f)))
+}
 
-    // This would be nicer if it just returned an iterator, but that runs into
-    // lifetime problems, because we need to borrow temp `CrateImplBlocks`.
-    pub(crate) fn iterate_method_candidates<T>(
-        self,
-        db: &impl HirDatabase,
-        resolver: &Resolver,
-        name: Option<&Name>,
-        mut callback: impl FnMut(&Ty, Function) -> Option<T>,
-    ) -> Option<T> {
-        // For method calls, rust first does any number of autoderef, and then one
-        // autoref (i.e. when the method takes &self or &mut self). We just ignore
-        // the autoref currently -- when we find a method matching the given name,
-        // we assume it fits.
+// This would be nicer if it just returned an iterator, but that runs into
+// lifetime problems, because we need to borrow temp `CrateImplBlocks`.
+pub(crate) fn iterate_method_candidates<T>(
+    ty: &Canonical<Ty>,
+    db: &impl HirDatabase,
+    resolver: &Resolver,
+    name: Option<&Name>,
+    mut callback: impl FnMut(&Ty, Function) -> Option<T>,
+) -> Option<T> {
+    // For method calls, rust first does any number of autoderef, and then one
+    // autoref (i.e. when the method takes &self or &mut self). We just ignore
+    // the autoref currently -- when we find a method matching the given name,
+    // we assume it fits.
 
-        // Also note that when we've got a receiver like &S, even if the method we
-        // find in the end takes &self, we still do the autoderef step (just as
-        // rustc does an autoderef and then autoref again).
+    // Also note that when we've got a receiver like &S, even if the method we
+    // find in the end takes &self, we still do the autoderef step (just as
+    // rustc does an autoderef and then autoref again).
 
-        let krate = resolver.krate()?;
-        for derefed_ty in self.autoderef(db) {
-            if let Some(result) =
-                derefed_ty.iterate_inherent_methods(db, name, krate, &mut callback)
-            {
-                return Some(result);
-            }
-            if let Some(result) =
-                derefed_ty.iterate_trait_method_candidates(db, resolver, name, &mut callback)
-            {
-                return Some(result);
-            }
+    let krate = resolver.krate()?;
+    for derefed_ty in ty.value.clone().autoderef(db) {
+        let derefed_ty = Canonical { value: derefed_ty, num_vars: ty.num_vars };
+        if let Some(result) = iterate_inherent_methods(&derefed_ty, db, name, krate, &mut callback)
+        {
+            return Some(result);
+        }
+        if let Some(result) =
+            iterate_trait_method_candidates(&derefed_ty, db, resolver, name, &mut callback)
+        {
+            return Some(result);
         }
-        None
     }
+    None
+}
 
-    fn iterate_trait_method_candidates<T>(
-        &self,
-        db: &impl HirDatabase,
-        resolver: &Resolver,
-        name: Option<&Name>,
-        mut callback: impl FnMut(&Ty, Function) -> Option<T>,
-    ) -> Option<T> {
-        'traits: for t in resolver.traits_in_scope() {
-            let data = t.trait_data(db);
-            // we'll be lazy about checking whether the type implements the
-            // trait, but if we find out it doesn't, we'll skip the rest of the
-            // iteration
-            let mut known_implemented = false;
-            for item in data.items() {
-                match item {
-                    &TraitItem::Function(m) => {
-                        let sig = m.signature(db);
-                        if name.map_or(true, |name| sig.name() == name) && sig.has_self_param() {
-                            if !known_implemented {
-                                let trait_ref = TraitRef {
-                                    trait_: t,
-                                    substs: fresh_substs_for_trait(db, t, self.clone()),
-                                };
-                                let (trait_ref, _) = super::traits::canonicalize(trait_ref);
-                                if db.implements(trait_ref).is_none() {
-                                    continue 'traits;
-                                }
-                            }
-                            known_implemented = true;
-                            if let Some(result) = callback(self, m) {
-                                return Some(result);
+fn iterate_trait_method_candidates<T>(
+    ty: &Canonical<Ty>,
+    db: &impl HirDatabase,
+    resolver: &Resolver,
+    name: Option<&Name>,
+    mut callback: impl FnMut(&Ty, Function) -> Option<T>,
+) -> Option<T> {
+    let krate = resolver.krate()?;
+    'traits: for t in resolver.traits_in_scope() {
+        let data = t.trait_data(db);
+        // we'll be lazy about checking whether the type implements the
+        // trait, but if we find out it doesn't, we'll skip the rest of the
+        // iteration
+        let mut known_implemented = false;
+        for item in data.items() {
+            match item {
+                &TraitItem::Function(m) => {
+                    let sig = m.signature(db);
+                    if name.map_or(true, |name| sig.name() == name) && sig.has_self_param() {
+                        if !known_implemented {
+                            let trait_ref = canonical_trait_ref(db, t, ty.clone());
+                            // FIXME cache this implements check (without solution) in a query?
+                            if super::traits::implements(db, krate, trait_ref).is_none() {
+                                continue 'traits;
                             }
                         }
+                        known_implemented = true;
+                        if let Some(result) = callback(&ty.value, m) {
+                            return Some(result);
+                        }
                     }
-                    _ => {}
                 }
+                _ => {}
             }
         }
-        None
     }
+    None
+}
 
-    fn iterate_inherent_methods<T>(
-        &self,
-        db: &impl HirDatabase,
-        name: Option<&Name>,
-        krate: Crate,
-        mut callback: impl FnMut(&Ty, Function) -> Option<T>,
-    ) -> Option<T> {
-        let krate = match def_crate(db, krate, self) {
-            Some(krate) => krate,
-            None => return None,
-        };
-        let impls = db.impls_in_crate(krate);
+fn iterate_inherent_methods<T>(
+    ty: &Canonical<Ty>,
+    db: &impl HirDatabase,
+    name: Option<&Name>,
+    krate: Crate,
+    mut callback: impl FnMut(&Ty, Function) -> Option<T>,
+) -> Option<T> {
+    let krate = match def_crate(db, krate, &ty.value) {
+        Some(krate) => krate,
+        None => return None,
+    };
+    let impls = db.impls_in_crate(krate);
 
-        for impl_block in impls.lookup_impl_blocks(self) {
-            for item in impl_block.items(db) {
-                match item {
-                    ImplItem::Method(f) => {
-                        let sig = f.signature(db);
-                        if name.map_or(true, |name| sig.name() == name) && sig.has_self_param() {
-                            if let Some(result) = callback(self, f) {
-                                return Some(result);
-                            }
+    for impl_block in impls.lookup_impl_blocks(&ty.value) {
+        for item in impl_block.items(db) {
+            match item {
+                ImplItem::Method(f) => {
+                    let sig = f.signature(db);
+                    if name.map_or(true, |name| sig.name() == name) && sig.has_self_param() {
+                        if let Some(result) = callback(&ty.value, f) {
+                            return Some(result);
                         }
                     }
-                    _ => {}
                 }
+                _ => {}
             }
         }
-        None
     }
+    None
+}
 
+impl Ty {
     // This would be nicer if it just returned an iterator, but that runs into
     // lifetime problems, because we need to borrow temp `CrateImplBlocks`.
     pub fn iterate_impl_items<T>(
@@ -271,15 +269,26 @@ impl Ty {
 }
 
 /// This creates Substs for a trait with the given Self type and type variables
-/// for all other parameters. This is kind of a hack since these aren't 'real'
-/// type variables; the resulting trait reference is just used for the
-/// preliminary method candidate check.
-fn fresh_substs_for_trait(db: &impl HirDatabase, tr: Trait, self_ty: Ty) -> Substs {
+/// for all other parameters, to query Chalk with it.
+fn canonical_trait_ref(
+    db: &impl HirDatabase,
+    trait_: Trait,
+    self_ty: Canonical<Ty>,
+) -> Canonical<TraitRef> {
     let mut substs = Vec::new();
-    let generics = tr.generic_params(db);
-    substs.push(self_ty);
-    substs.extend(generics.params_including_parent().into_iter().skip(1).enumerate().map(
-        |(i, _p)| Ty::Infer(super::infer::InferTy::TypeVar(super::infer::TypeVarId(i as u32))),
-    ));
-    substs.into()
+    let generics = trait_.generic_params(db);
+    let num_vars = self_ty.num_vars;
+    substs.push(self_ty.value);
+    substs.extend(
+        generics
+            .params_including_parent()
+            .into_iter()
+            .skip(1)
+            .enumerate()
+            .map(|(i, _p)| Ty::Bound((i + num_vars) as u32)),
+    );
+    Canonical {
+        num_vars: substs.len() - 1 + self_ty.num_vars,
+        value: TraitRef { trait_, substs: substs.into() },
+    }
 }
diff --git a/crates/ra_hir/src/ty/tests.rs b/crates/ra_hir/src/ty/tests.rs
index c76a5012f..0aecde37c 100644
--- a/crates/ra_hir/src/ty/tests.rs
+++ b/crates/ra_hir/src/ty/tests.rs
@@ -2140,7 +2140,7 @@ fn test() {
 [102; 127) '{     ...d(); }': ()
 [108; 109) 'S': S<u32>(T) -> S<T>
 [108; 115) 'S(1u32)': S<u32>
-[108; 124) 'S(1u32...thod()': {unknown}
+[108; 124) 'S(1u32...thod()': u32
 [110; 114) '1u32': u32"###
     );
 }
diff --git a/crates/ra_hir/src/ty/traits.rs b/crates/ra_hir/src/ty/traits.rs
index 06f483899..a1ed0c028 100644
--- a/crates/ra_hir/src/ty/traits.rs
+++ b/crates/ra_hir/src/ty/traits.rs
@@ -1,47 +1,65 @@
-//! Stuff that will probably mostly replaced by Chalk.
-use std::collections::HashMap;
+//! Trait solving using Chalk.
+use std::sync::{Arc, Mutex};
 
-use crate::{db::HirDatabase, generics::HasGenericParams};
-use super::{TraitRef, Substs, infer::{TypeVarId, InferTy}, Ty};
+use log::debug;
+use chalk_ir::cast::Cast;
 
-// Copied (and simplified) from Chalk
+use crate::{Crate, Trait, db::HirDatabase, ImplBlock};
+use super::{TraitRef, Ty, Canonical};
 
-#[derive(Clone, Debug, PartialEq, Eq)]
-/// A (possible) solution for a proposed goal. Usually packaged in a `Result`,
-/// where `Err` represents definite *failure* to prove a goal.
-pub enum Solution {
-    /// The goal indeed holds, and there is a unique value for all existential
-    /// variables.
-    Unique(Substs),
+use self::chalk::{ToChalk, from_chalk};
 
-    /// The goal may be provable in multiple ways, but regardless we may have some guidance
-    /// for type inference.
-    Ambig(Guidance),
+mod chalk;
+
+pub(crate) type Solver = chalk_solve::Solver;
+
+#[derive(Debug, Copy, Clone)]
+struct ChalkContext<'a, DB> {
+    db: &'a DB,
+    krate: Crate,
 }
 
-#[derive(Clone, Debug, PartialEq, Eq)]
-/// When a goal holds ambiguously (e.g., because there are multiple possible
-/// solutions), we issue a set of *guidance* back to type inference.
-pub enum Guidance {
-    /// The existential variables *must* have the given values if the goal is
-    /// ever to hold, but that alone isn't enough to guarantee the goal will
-    /// actually hold.
-    Definite(Substs),
+pub(crate) fn solver(_db: &impl HirDatabase, _krate: Crate) -> Arc<Mutex<Solver>> {
+    // krate parameter is just so we cache a unique solver per crate
+    let solver_choice = chalk_solve::SolverChoice::SLG { max_size: 10 };
+    Arc::new(Mutex::new(solver_choice.into_solver()))
+}
 
-    /// There are multiple plausible values for the existentials, but the ones
-    /// here are suggested as the preferred choice heuristically. These should
-    /// be used for inference fallback only.
-    Suggested(Substs),
+/// Collects impls for the given trait in the whole dependency tree of `krate`.
+pub(crate) fn impls_for_trait(
+    db: &impl HirDatabase,
+    krate: Crate,
+    trait_: Trait,
+) -> Arc<[ImplBlock]> {
+    let mut impls = Vec::new();
+    // We call the query recursively here. On the one hand, this means we can
+    // reuse results from queries for different crates; on the other hand, this
+    // will only ever get called for a few crates near the root of the tree (the
+    // ones the user is editing), so this may actually be a waste of memory. I'm
+    // doing it like this mainly for simplicity for now.
+    for dep in krate.dependencies(db) {
+        impls.extend(db.impls_for_trait(dep.krate, trait_).iter());
+    }
+    let crate_impl_blocks = db.impls_in_crate(krate);
+    impls.extend(crate_impl_blocks.lookup_impl_blocks_for_trait(&trait_));
+    impls.into()
+}
 
-    /// There's no useful information to feed back to type inference
-    Unknown,
+fn solve(
+    db: &impl HirDatabase,
+    krate: Crate,
+    goal: &chalk_ir::UCanonical<chalk_ir::InEnvironment<chalk_ir::Goal>>,
+) -> Option<chalk_solve::Solution> {
+    let context = ChalkContext { db, krate };
+    let solver = db.solver(krate);
+    let solution = solver.lock().unwrap().solve(&context, goal);
+    debug!("solve({:?}) => {:?}", goal, solution);
+    solution
 }
 
 /// Something that needs to be proven (by Chalk) during type checking, e.g. that
 /// a certain type implements a certain trait. Proving the Obligation might
 /// result in additional information about inference variables.
-///
-/// This might be handled by Chalk when we integrate it?
 #[derive(Clone, Debug, PartialEq, Eq)]
 pub enum Obligation {
     /// Prove that a certain type implements a trait (the type is the `Self` type
@@ -49,67 +67,94 @@ pub enum Obligation {
     Trait(TraitRef),
 }
 
-/// Rudimentary check whether an impl exists for a given type and trait; this
-/// will actually be done by chalk.
-pub(crate) fn implements(db: &impl HirDatabase, trait_ref: TraitRef) -> Option<Solution> {
-    // FIXME use all trait impls in the whole crate graph
-    let krate = trait_ref.trait_.module(db).krate(db);
-    let krate = match krate {
-        Some(krate) => krate,
-        None => return None,
-    };
-    let crate_impl_blocks = db.impls_in_crate(krate);
-    let mut impl_blocks = crate_impl_blocks
-        .lookup_impl_blocks_for_trait(&trait_ref.trait_)
-        // we don't handle where clauses at all, waiting for Chalk for that
-        .filter(|impl_block| impl_block.generic_params(db).where_predicates.is_empty());
-    impl_blocks
-        .find_map(|impl_block| unify_trait_refs(&trait_ref, &impl_block.target_trait_ref(db)?))
+/// Check using Chalk whether trait is implemented for given parameters including `Self` type.
+pub(crate) fn implements(
+    db: &impl HirDatabase,
+    krate: Crate,
+    trait_ref: Canonical<TraitRef>,
+) -> Option<Solution> {
+    let goal: chalk_ir::Goal = trait_ref.value.to_chalk(db).cast();
+    debug!("goal: {:?}", goal);
+    let env = chalk_ir::Environment::new();
+    let in_env = chalk_ir::InEnvironment::new(&env, goal);
+    let parameter = chalk_ir::ParameterKind::Ty(chalk_ir::UniverseIndex::ROOT);
+    let canonical =
+        chalk_ir::Canonical { value: in_env, binders: vec![parameter; trait_ref.num_vars] };
+    // We currently don't deal with universes (I think / hope they're not yet
+    // relevant for our use cases?)
+    let u_canonical = chalk_ir::UCanonical { canonical, universes: 1 };
+    let solution = solve(db, krate, &u_canonical);
+    solution.map(|solution| solution_from_chalk(db, solution))
 }
 
-pub(super) fn canonicalize(trait_ref: TraitRef) -> (TraitRef, Vec<TypeVarId>) {
-    let mut canonical = HashMap::new(); // mapping uncanonical -> canonical
-    let mut uncanonical = Vec::new(); // mapping canonical -> uncanonical (which is dense)
-    let mut substs = trait_ref.substs.0.to_vec();
-    for ty in &mut substs {
-        ty.walk_mut(&mut |ty| match ty {
-            Ty::Infer(InferTy::TypeVar(tv)) => {
-                let tv: &mut TypeVarId = tv;
-                *tv = *canonical.entry(*tv).or_insert_with(|| {
-                    let i = uncanonical.len();
-                    uncanonical.push(*tv);
-                    TypeVarId(i as u32)
-                });
-            }
-            _ => {}
-        });
+fn solution_from_chalk(db: &impl HirDatabase, solution: chalk_solve::Solution) -> Solution {
+    let convert_subst = |subst: chalk_ir::Canonical<chalk_ir::Substitution>| {
+        let value = subst
+            .value
+            .parameters
+            .into_iter()
+            .map(|p| {
+                let ty = match p {
+                    chalk_ir::Parameter(chalk_ir::ParameterKind::Ty(ty)) => from_chalk(db, ty),
+                    chalk_ir::Parameter(chalk_ir::ParameterKind::Lifetime(_)) => unimplemented!(),
+                };
+                ty
+            })
+            .collect();
+        let result = Canonical { value, num_vars: subst.binders.len() };
+        SolutionVariables(result)
+    };
+    match solution {
+        chalk_solve::Solution::Unique(constr_subst) => {
+            let subst = chalk_ir::Canonical {
+                value: constr_subst.value.subst,
+                binders: constr_subst.binders,
+            };
+            Solution::Unique(convert_subst(subst))
+        }
+        chalk_solve::Solution::Ambig(chalk_solve::Guidance::Definite(subst)) => {
+            Solution::Ambig(Guidance::Definite(convert_subst(subst)))
+        }
+        chalk_solve::Solution::Ambig(chalk_solve::Guidance::Suggested(subst)) => {
+            Solution::Ambig(Guidance::Suggested(convert_subst(subst)))
+        }
+        chalk_solve::Solution::Ambig(chalk_solve::Guidance::Unknown) => {
+            Solution::Ambig(Guidance::Unknown)
+        }
     }
-    (TraitRef { substs: substs.into(), ..trait_ref }, uncanonical)
 }
 
-fn unify_trait_refs(tr1: &TraitRef, tr2: &TraitRef) -> Option<Solution> {
-    if tr1.trait_ != tr2.trait_ {
-        return None;
-    }
-    let mut solution_substs = Vec::new();
-    for (t1, t2) in tr1.substs.0.iter().zip(tr2.substs.0.iter()) {
-        // this is very bad / hacky 'unification' logic, just enough to make the simple tests pass
-        match (t1, t2) {
-            (_, Ty::Infer(InferTy::TypeVar(_))) | (_, Ty::Unknown) | (_, Ty::Param { .. }) => {
-                // type variable (or similar) in the impl, we just assume it works
-            }
-            (Ty::Infer(InferTy::TypeVar(v1)), _) => {
-                // type variable in the query and fixed type in the impl, record its value
-                solution_substs.resize_with(v1.0 as usize + 1, || Ty::Unknown);
-                solution_substs[v1.0 as usize] = t2.clone();
-            }
-            _ => {
-                // check that they're equal (actually we'd have to recurse etc.)
-                if t1 != t2 {
-                    return None;
-                }
-            }
-        }
-    }
-    Some(Solution::Unique(solution_substs.into()))
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub(crate) struct SolutionVariables(pub Canonical<Vec<Ty>>);
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+/// A (possible) solution for a proposed goal.
+pub(crate) enum Solution {
+    /// The goal indeed holds, and there is a unique value for all existential
+    /// variables.
+    Unique(SolutionVariables),
+
+    /// The goal may be provable in multiple ways, but regardless we may have some guidance
+    /// for type inference. In this case, we don't return any lifetime
+    /// constraints, since we have not "committed" to any particular solution
+    /// yet.
+    Ambig(Guidance),
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+/// When a goal holds ambiguously (e.g., because there are multiple possible
+/// solutions), we issue a set of *guidance* back to type inference.
+pub(crate) enum Guidance {
+    /// The existential variables *must* have the given values if the goal is
+    /// ever to hold, but that alone isn't enough to guarantee the goal will
+    /// actually hold.
+    Definite(SolutionVariables),
+
+    /// There are multiple plausible values for the existentials, but the ones
+    /// here are suggested as the preferred choice heuristically. These should
+    /// be used for inference fallback only.
+    Suggested(SolutionVariables),
+
+    /// There's no useful information to feed back to type inference
+    Unknown,
 }
diff --git a/crates/ra_hir/src/ty/traits/chalk.rs b/crates/ra_hir/src/ty/traits/chalk.rs
new file mode 100644
index 000000000..8b77d21b4
--- /dev/null
+++ b/crates/ra_hir/src/ty/traits/chalk.rs
@@ -0,0 +1,333 @@
+//! Conversion code from/to Chalk.
+use std::sync::Arc;
+
+use log::debug;
+
+use chalk_ir::{TypeId, ImplId, TypeKindId, ProjectionTy, Parameter, Identifier, cast::Cast, PlaceholderIndex, UniverseIndex, TypeName};
+use chalk_rust_ir::{AssociatedTyDatum, TraitDatum, StructDatum, ImplDatum};
+
+use ra_db::salsa::{InternId, InternKey};
+
+use crate::{
+    Trait, HasGenericParams, ImplBlock,
+    db::HirDatabase,
+    ty::{TraitRef, Ty, ApplicationTy, TypeCtor, Substs},
+};
+use super::ChalkContext;
+
+pub(super) trait ToChalk {
+    type Chalk;
+    fn to_chalk(self, db: &impl HirDatabase) -> Self::Chalk;
+    fn from_chalk(db: &impl HirDatabase, chalk: Self::Chalk) -> Self;
+}
+
+pub(super) fn from_chalk<T, ChalkT>(db: &impl HirDatabase, chalk: ChalkT) -> T
+where
+    T: ToChalk<Chalk = ChalkT>,
+{
+    T::from_chalk(db, chalk)
+}
+
+impl ToChalk for Ty {
+    type Chalk = chalk_ir::Ty;
+    fn to_chalk(self, db: &impl HirDatabase) -> chalk_ir::Ty {
+        match self {
+            Ty::Apply(apply_ty) => {
+                let struct_id = apply_ty.ctor.to_chalk(db);
+                let name = TypeName::TypeKindId(struct_id.into());
+                let parameters = apply_ty.parameters.to_chalk(db);
+                chalk_ir::ApplicationTy { name, parameters }.cast()
+            }
+            Ty::Param { idx, .. } => {
+                PlaceholderIndex { ui: UniverseIndex::ROOT, idx: idx as usize }.to_ty()
+            }
+            Ty::Bound(idx) => chalk_ir::Ty::BoundVar(idx as usize),
+            Ty::Infer(_infer_ty) => panic!("uncanonicalized infer ty"),
+            // FIXME this is clearly incorrect, but probably not too incorrect
+            // and I'm not sure what to actually do with Ty::Unknown
+            Ty::Unknown => PlaceholderIndex { ui: UniverseIndex::ROOT, idx: 0 }.to_ty(),
+        }
+    }
+    fn from_chalk(db: &impl HirDatabase, chalk: chalk_ir::Ty) -> Self {
+        match chalk {
+            chalk_ir::Ty::Apply(apply_ty) => {
+                match apply_ty.name {
+                    TypeName::TypeKindId(TypeKindId::StructId(struct_id)) => {
+                        let ctor = from_chalk(db, struct_id);
+                        let parameters = from_chalk(db, apply_ty.parameters);
+                        Ty::Apply(ApplicationTy { ctor, parameters })
+                    }
+                    // FIXME handle TypeKindId::Trait/Type here
+                    TypeName::TypeKindId(_) => unimplemented!(),
+                    TypeName::AssociatedType(_) => unimplemented!(),
+                    TypeName::Placeholder(idx) => {
+                        assert_eq!(idx.ui, UniverseIndex::ROOT);
+                        Ty::Param { idx: idx.idx as u32, name: crate::Name::missing() }
+                    }
+                }
+            }
+            chalk_ir::Ty::Projection(_) => unimplemented!(),
+            chalk_ir::Ty::UnselectedProjection(_) => unimplemented!(),
+            chalk_ir::Ty::ForAll(_) => unimplemented!(),
+            chalk_ir::Ty::BoundVar(idx) => Ty::Bound(idx as u32),
+            chalk_ir::Ty::InferenceVar(_iv) => panic!("unexpected chalk infer ty"),
+        }
+    }
+}
+
+impl ToChalk for Substs {
+    type Chalk = Vec<chalk_ir::Parameter>;
+
+    fn to_chalk(self, db: &impl HirDatabase) -> Vec<Parameter> {
+        self.iter().map(|ty| ty.clone().to_chalk(db).cast()).collect()
+    }
+
+    fn from_chalk(db: &impl HirDatabase, parameters: Vec<chalk_ir::Parameter>) -> Substs {
+        parameters
+            .into_iter()
+            .map(|p| match p {
+                chalk_ir::Parameter(chalk_ir::ParameterKind::Ty(ty)) => from_chalk(db, ty),
+                chalk_ir::Parameter(chalk_ir::ParameterKind::Lifetime(_)) => unimplemented!(),
+            })
+            .collect::<Vec<_>>()
+            .into()
+    }
+}
+
+impl ToChalk for TraitRef {
+    type Chalk = chalk_ir::TraitRef;
+
+    fn to_chalk(self: TraitRef, db: &impl HirDatabase) -> chalk_ir::TraitRef {
+        let trait_id = self.trait_.to_chalk(db);
+        let parameters = self.substs.to_chalk(db);
+        chalk_ir::TraitRef { trait_id, parameters }
+    }
+
+    fn from_chalk(db: &impl HirDatabase, trait_ref: chalk_ir::TraitRef) -> Self {
+        let trait_ = from_chalk(db, trait_ref.trait_id);
+        let substs = from_chalk(db, trait_ref.parameters);
+        TraitRef { trait_, substs }
+    }
+}
+
+impl ToChalk for Trait {
+    type Chalk = chalk_ir::TraitId;
+
+    fn to_chalk(self, _db: &impl HirDatabase) -> chalk_ir::TraitId {
+        self.id.into()
+    }
+
+    fn from_chalk(_db: &impl HirDatabase, trait_id: chalk_ir::TraitId) -> Trait {
+        Trait { id: trait_id.into() }
+    }
+}
+
+impl ToChalk for TypeCtor {
+    type Chalk = chalk_ir::StructId;
+
+    fn to_chalk(self, db: &impl HirDatabase) -> chalk_ir::StructId {
+        db.intern_type_ctor(self).into()
+    }
+
+    fn from_chalk(db: &impl HirDatabase, struct_id: chalk_ir::StructId) -> TypeCtor {
+        db.lookup_intern_type_ctor(struct_id.into())
+    }
+}
+
+impl ToChalk for ImplBlock {
+    type Chalk = chalk_ir::ImplId;
+
+    fn to_chalk(self, db: &impl HirDatabase) -> chalk_ir::ImplId {
+        db.intern_impl_block(self).into()
+    }
+
+    fn from_chalk(db: &impl HirDatabase, impl_id: chalk_ir::ImplId) -> ImplBlock {
+        db.lookup_intern_impl_block(impl_id.into())
+    }
+}
+
+fn make_binders<T>(value: T, num_vars: usize) -> chalk_ir::Binders<T> {
+    chalk_ir::Binders {
+        value,
+        binders: std::iter::repeat(chalk_ir::ParameterKind::Ty(())).take(num_vars).collect(),
+    }
+}
+
+impl<'a, DB> chalk_solve::RustIrDatabase for ChalkContext<'a, DB>
+where
+    DB: HirDatabase,
+{
+    fn associated_ty_data(&self, _ty: TypeId) -> Arc<AssociatedTyDatum> {
+        unimplemented!()
+    }
+    fn trait_datum(&self, trait_id: chalk_ir::TraitId) -> Arc<TraitDatum> {
+        debug!("trait_datum {:?}", trait_id);
+        let trait_: Trait = from_chalk(self.db, trait_id);
+        let generic_params = trait_.generic_params(self.db);
+        let bound_vars = Substs::bound_vars(&generic_params);
+        let trait_ref = trait_.trait_ref(self.db).subst(&bound_vars).to_chalk(self.db);
+        let flags = chalk_rust_ir::TraitFlags {
+            // FIXME set these flags correctly
+            auto: false,
+            marker: false,
+            upstream: trait_.module(self.db).krate(self.db) != Some(self.krate),
+            fundamental: false,
+        };
+        let where_clauses = Vec::new(); // FIXME add where clauses
+        let associated_ty_ids = Vec::new(); // FIXME add associated tys
+        let trait_datum_bound =
+            chalk_rust_ir::TraitDatumBound { trait_ref, where_clauses, flags, associated_ty_ids };
+        let trait_datum = TraitDatum { binders: make_binders(trait_datum_bound, bound_vars.len()) };
+        Arc::new(trait_datum)
+    }
+    fn struct_datum(&self, struct_id: chalk_ir::StructId) -> Arc<StructDatum> {
+        debug!("struct_datum {:?}", struct_id);
+        let type_ctor = from_chalk(self.db, struct_id);
+        // FIXME might be nicer if we can create a fake GenericParams for the TypeCtor
+        // FIXME extract this to a method on Ty
+        let (num_params, upstream) = match type_ctor {
+            TypeCtor::Bool
+            | TypeCtor::Char
+            | TypeCtor::Int(_)
+            | TypeCtor::Float(_)
+            | TypeCtor::Never
+            | TypeCtor::Str => (0, true),
+            TypeCtor::Slice | TypeCtor::Array | TypeCtor::RawPtr(_) | TypeCtor::Ref(_) => (1, true),
+            TypeCtor::FnPtr { num_args } => (num_args as usize + 1, true),
+            TypeCtor::Tuple { cardinality } => (cardinality as usize, true),
+            TypeCtor::FnDef(_) => unimplemented!(),
+            TypeCtor::Adt(adt) => {
+                let generic_params = adt.generic_params(self.db);
+                (
+                    generic_params.count_params_including_parent(),
+                    adt.krate(self.db) != Some(self.krate),
+                )
+            }
+        };
+        let flags = chalk_rust_ir::StructFlags {
+            upstream,
+            // FIXME set fundamental flag correctly
+            fundamental: false,
+        };
+        let where_clauses = Vec::new(); // FIXME add where clauses
+        let self_ty = chalk_ir::ApplicationTy {
+            name: TypeName::TypeKindId(type_ctor.to_chalk(self.db).into()),
+            parameters: (0..num_params).map(|i| chalk_ir::Ty::BoundVar(i).cast()).collect(),
+        };
+        let struct_datum_bound = chalk_rust_ir::StructDatumBound {
+            self_ty,
+            fields: Vec::new(), // FIXME add fields (only relevant for auto traits)
+            where_clauses,
+            flags,
+        };
+        let struct_datum = StructDatum { binders: make_binders(struct_datum_bound, num_params) };
+        Arc::new(struct_datum)
+    }
+    fn impl_datum(&self, impl_id: ImplId) -> Arc<ImplDatum> {
+        debug!("impl_datum {:?}", impl_id);
+        let impl_block: ImplBlock = from_chalk(self.db, impl_id);
+        let generic_params = impl_block.generic_params(self.db);
+        let bound_vars = Substs::bound_vars(&generic_params);
+        let trait_ref = impl_block
+            .target_trait_ref(self.db)
+            .expect("FIXME handle unresolved impl block trait ref")
+            .subst(&bound_vars);
+        let impl_type = if impl_block.module().krate(self.db) == Some(self.krate) {
+            chalk_rust_ir::ImplType::Local
+        } else {
+            chalk_rust_ir::ImplType::External
+        };
+        let impl_datum_bound = chalk_rust_ir::ImplDatumBound {
+            // FIXME handle negative impls (impl !Sync for Foo)
+            trait_ref: chalk_rust_ir::PolarizedTraitRef::Positive(trait_ref.to_chalk(self.db)),
+            where_clauses: Vec::new(),        // FIXME add where clauses
+            associated_ty_values: Vec::new(), // FIXME add associated type values
+            impl_type,
+        };
+        let impl_datum = ImplDatum { binders: make_binders(impl_datum_bound, bound_vars.len()) };
+        Arc::new(impl_datum)
+    }
+    fn impls_for_trait(&self, trait_id: chalk_ir::TraitId) -> Vec<ImplId> {
+        debug!("impls_for_trait {:?}", trait_id);
+        let trait_ = from_chalk(self.db, trait_id);
+        self.db
+            .impls_for_trait(self.krate, trait_)
+            .iter()
+            // FIXME temporary hack -- as long as we're not lowering where clauses
+            // correctly, ignore impls with them completely so as to not treat
+            // impl<T> Trait for T where T: ... as a blanket impl on all types
+            .filter(|impl_block| impl_block.generic_params(self.db).where_predicates.is_empty())
+            .map(|impl_block| impl_block.to_chalk(self.db))
+            .collect()
+    }
+    fn impl_provided_for(
+        &self,
+        auto_trait_id: chalk_ir::TraitId,
+        struct_id: chalk_ir::StructId,
+    ) -> bool {
+        debug!("impl_provided_for {:?}, {:?}", auto_trait_id, struct_id);
+        false // FIXME
+    }
+    fn type_name(&self, _id: TypeKindId) -> Identifier {
+        unimplemented!()
+    }
+    fn split_projection<'p>(
+        &self,
+        projection: &'p ProjectionTy,
+    ) -> (Arc<AssociatedTyDatum>, &'p [Parameter], &'p [Parameter]) {
+        debug!("split_projection {:?}", projection);
+        unimplemented!()
+    }
+    fn custom_clauses(&self) -> Vec<chalk_ir::ProgramClause> {
+        debug!("custom_clauses");
+        vec![]
+    }
+    fn all_structs(&self) -> Vec<chalk_ir::StructId> {
+        debug!("all_structs");
+        // FIXME
+        vec![]
+    }
+}
+
+fn id_from_chalk<T: InternKey>(chalk_id: chalk_ir::RawId) -> T {
+    T::from_intern_id(InternId::from(chalk_id.index))
+}
+fn id_to_chalk<T: InternKey>(salsa_id: T) -> chalk_ir::RawId {
+    chalk_ir::RawId { index: salsa_id.as_intern_id().as_u32() }
+}
+
+impl From<chalk_ir::TraitId> for crate::ids::TraitId {
+    fn from(trait_id: chalk_ir::TraitId) -> Self {
+        id_from_chalk(trait_id.0)
+    }
+}
+
+impl From<crate::ids::TraitId> for chalk_ir::TraitId {
+    fn from(trait_id: crate::ids::TraitId) -> Self {
+        chalk_ir::TraitId(id_to_chalk(trait_id))
+    }
+}
+
+impl From<chalk_ir::StructId> for crate::ids::TypeCtorId {
+    fn from(struct_id: chalk_ir::StructId) -> Self {
+        id_from_chalk(struct_id.0)
+    }
+}
+
+impl From<crate::ids::TypeCtorId> for chalk_ir::StructId {
+    fn from(type_ctor_id: crate::ids::TypeCtorId) -> Self {
+        chalk_ir::StructId(id_to_chalk(type_ctor_id))
+    }
+}
+
+impl From<chalk_ir::ImplId> for crate::ids::GlobalImplId {
+    fn from(impl_id: chalk_ir::ImplId) -> Self {
+        id_from_chalk(impl_id.0)
+    }
+}
+
+impl From<crate::ids::GlobalImplId> for chalk_ir::ImplId {
+    fn from(impl_id: crate::ids::GlobalImplId) -> Self {
+        chalk_ir::ImplId(id_to_chalk(impl_id))
+    }
+}