Introduce QuantifiedWhereClause and DynTy analogous to Chalk

This introduces a bunch of new binders in lots of places, which we have
to be careful about, but we had to add them at some point.

6 files changed, 197 insertions, 98 deletions

diff --git a/crates/hir_ty/src/display.rs b/crates/hir_ty/src/display.rs
index 9d3b79be3..372671405 100644
--- a/crates/hir_ty/src/display.rs
+++ b/crates/hir_ty/src/display.rs
@@ -1,6 +1,6 @@
 //! FIXME: write short doc here
 
-use std::{borrow::Cow, fmt};
+use std::fmt;
 
 use arrayvec::ArrayVec;
 use chalk_ir::Mutability;
@@ -20,7 +20,7 @@ use crate::{
     db::HirDatabase, from_assoc_type_id, from_foreign_def_id, from_placeholder_idx, primitive,
     to_assoc_type_id, traits::chalk::from_chalk, utils::generics, AdtId, AliasEq, AliasTy,
     CallableDefId, CallableSig, DomainGoal, ImplTraitId, Interner, Lifetime, OpaqueTy,
-    ProjectionTy, Scalar, Substitution, TraitRef, Ty, TyKind, WhereClause,
+    ProjectionTy, QuantifiedWhereClause, Scalar, Substitution, TraitRef, Ty, TyKind, WhereClause,
 };
 
 pub struct HirFormatter<'a> {
@@ -328,9 +328,9 @@ impl HirDisplay for Ty {
 
                 // FIXME: all this just to decide whether to use parentheses...
                 let datas;
-                let predicates = match t.interned(&Interner) {
-                    TyKind::Dyn(predicates) if predicates.len() > 1 => {
-                        Cow::Borrowed(predicates.as_ref())
+                let predicates: Vec<_> = match t.interned(&Interner) {
+                    TyKind::Dyn(dyn_ty) if dyn_ty.bounds.skip_binders().interned().len() > 1 => {
+                        dyn_ty.bounds.skip_binders().interned().iter().cloned().collect()
                     }
                     &TyKind::Alias(AliasTy::Opaque(OpaqueTy {
                         opaque_ty_id,
@@ -345,17 +345,21 @@ impl HirDisplay for Ty {
                                 .as_ref()
                                 .map(|rpit| rpit.impl_traits[idx as usize].bounds.clone());
                             let bounds = data.subst(parameters);
-                            Cow::Owned(bounds.value)
+                            bounds.value
                         } else {
-                            Cow::Borrowed(&[][..])
+                            Vec::new()
                         }
                     }
-                    _ => Cow::Borrowed(&[][..]),
+                    _ => Vec::new(),
                 };
 
-                if let [WhereClause::Implemented(trait_ref), _] = predicates.as_ref() {
+                if let Some(WhereClause::Implemented(trait_ref)) =
+                    predicates.get(0).map(|b| b.skip_binders())
+                {
                     let trait_ = trait_ref.hir_trait_id();
-                    if fn_traits(f.db.upcast(), trait_).any(|it| it == trait_) {
+                    if fn_traits(f.db.upcast(), trait_).any(|it| it == trait_)
+                        && predicates.len() <= 2
+                    {
                         return write!(f, "{}", ty_display);
                     }
                 }
@@ -586,13 +590,25 @@ impl HirDisplay for Ty {
                                 _ => false,
                             })
                             .collect::<Vec<_>>();
-                        write_bounds_like_dyn_trait_with_prefix("impl", &bounds, f)?;
+                        write_bounds_like_dyn_trait_with_prefix(
+                            "impl",
+                            &bounds
+                                .iter()
+                                .cloned()
+                                .map(crate::Binders::wrap_empty)
+                                .collect::<Vec<_>>(),
+                            f,
+                        )?;
                     }
                 }
             }
             TyKind::BoundVar(idx) => write!(f, "?{}.{}", idx.debruijn.depth(), idx.index)?,
-            TyKind::Dyn(predicates) => {
-                write_bounds_like_dyn_trait_with_prefix("dyn", predicates, f)?;
+            TyKind::Dyn(dyn_ty) => {
+                write_bounds_like_dyn_trait_with_prefix(
+                    "dyn",
+                    dyn_ty.bounds.skip_binders().interned(),
+                    f,
+                )?;
             }
             TyKind::Alias(AliasTy::Projection(p_ty)) => p_ty.hir_fmt(f)?,
             TyKind::Alias(AliasTy::Opaque(opaque_ty)) => {
@@ -661,7 +677,7 @@ fn fn_traits(db: &dyn DefDatabase, trait_: TraitId) -> impl Iterator<Item = Trai
 
 pub fn write_bounds_like_dyn_trait_with_prefix(
     prefix: &str,
-    predicates: &[WhereClause],
+    predicates: &[QuantifiedWhereClause],
     f: &mut HirFormatter,
 ) -> Result<(), HirDisplayError> {
     write!(f, "{}", prefix)?;
@@ -674,7 +690,7 @@ pub fn write_bounds_like_dyn_trait_with_prefix(
 }
 
 fn write_bounds_like_dyn_trait(
-    predicates: &[WhereClause],
+    predicates: &[QuantifiedWhereClause],
     f: &mut HirFormatter,
 ) -> Result<(), HirDisplayError> {
     // Note: This code is written to produce nice results (i.e.
@@ -687,7 +703,7 @@ fn write_bounds_like_dyn_trait(
     let mut angle_open = false;
     let mut is_fn_trait = false;
     for p in predicates.iter() {
-        match p {
+        match p.skip_binders() {
             WhereClause::Implemented(trait_ref) => {
                 let trait_ = trait_ref.hir_trait_id();
                 if !is_fn_trait {
diff --git a/crates/hir_ty/src/infer/unify.rs b/crates/hir_ty/src/infer/unify.rs
index 1fc03c8f4..35b0a2059 100644
--- a/crates/hir_ty/src/infer/unify.rs
+++ b/crates/hir_ty/src/infer/unify.rs
@@ -310,9 +310,18 @@ impl InferenceTable {
 
             (TyKind::Placeholder(p1), TyKind::Placeholder(p2)) if *p1 == *p2 => true,
 
-            (TyKind::Dyn(dyn1), TyKind::Dyn(dyn2)) if dyn1.len() == dyn2.len() => {
-                for (pred1, pred2) in dyn1.iter().zip(dyn2.iter()) {
-                    if !self.unify_preds(pred1, pred2, depth + 1) {
+            (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;
                     }
                 }
diff --git a/crates/hir_ty/src/lib.rs b/crates/hir_ty/src/lib.rs
index ad908f957..e4b1f92e4 100644
--- a/crates/hir_ty/src/lib.rs
+++ b/crates/hir_ty/src/lib.rs
@@ -132,6 +132,12 @@ impl TypeWalk for ProjectionTy {
     }
 }
 
+#[derive(Clone, PartialEq, Eq, Debug, Hash)]
+pub struct DynTy {
+    /// The unknown self type.
+    pub bounds: Binders<QuantifiedWhereClauses>,
+}
+
 pub type FnSig = chalk_ir::FnSig<Interner>;
 
 #[derive(Clone, PartialEq, Eq, Debug, Hash)]
@@ -283,7 +289,7 @@ pub enum TyKind {
     /// represents the `Self` type inside the bounds. This is currently
     /// implicit; Chalk has the `Binders` struct to make it explicit, but it
     /// didn't seem worth the overhead yet.
-    Dyn(Arc<[WhereClause]>),
+    Dyn(DynTy),
 
     /// A placeholder for a type which could not be computed; this is propagated
     /// to avoid useless error messages. Doubles as a placeholder where type
@@ -490,6 +496,13 @@ impl<T> Binders<T> {
         Self { num_binders, value }
     }
 
+    pub fn wrap_empty(value: T) -> Self
+    where
+        T: TypeWalk,
+    {
+        Self { num_binders: 0, value: value.shift_bound_vars(DebruijnIndex::ONE) }
+    }
+
     pub fn as_ref(&self) -> Binders<&T> {
         Binders { num_binders: self.num_binders, value: &self.value }
     }
@@ -501,6 +514,10 @@ impl<T> Binders<T> {
     pub fn filter_map<U>(self, f: impl FnOnce(T) -> Option<U>) -> Option<Binders<U>> {
         Some(Binders { num_binders: self.num_binders, value: f(self.value)? })
     }
+
+    pub fn skip_binders(&self) -> &T {
+        &self.value
+    }
 }
 
 impl<T: Clone> Binders<&T> {
@@ -614,6 +631,24 @@ impl TypeWalk for WhereClause {
     }
 }
 
+pub type QuantifiedWhereClause = Binders<WhereClause>;
+
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+pub struct QuantifiedWhereClauses(Arc<[QuantifiedWhereClause]>);
+
+impl QuantifiedWhereClauses {
+    pub fn from_iter(
+        _interner: &Interner,
+        elements: impl IntoIterator<Item = QuantifiedWhereClause>,
+    ) -> Self {
+        QuantifiedWhereClauses(elements.into_iter().collect())
+    }
+
+    pub fn interned(&self) -> &Arc<[QuantifiedWhereClause]> {
+        &self.0
+    }
+}
+
 /// 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 `kinds` tells us how
@@ -810,12 +845,14 @@ impl Ty {
     }
 
     /// If this is a `dyn Trait` type, this returns the `Trait` part.
-    pub fn dyn_trait_ref(&self) -> Option<&TraitRef> {
+    fn dyn_trait_ref(&self) -> Option<&TraitRef> {
         match self.interned(&Interner) {
-            TyKind::Dyn(bounds) => bounds.get(0).and_then(|b| match b {
-                WhereClause::Implemented(trait_ref) => Some(trait_ref),
-                _ => None,
-            }),
+            TyKind::Dyn(dyn_ty) => {
+                dyn_ty.bounds.value.interned().get(0).and_then(|b| match b.skip_binders() {
+                    WhereClause::Implemented(trait_ref) => Some(trait_ref),
+                    _ => None,
+                })
+            }
             _ => None,
         }
     }
@@ -892,7 +929,7 @@ impl Ty {
         }
     }
 
-    pub fn impl_trait_bounds(&self, db: &dyn HirDatabase) -> Option<Vec<WhereClause>> {
+    pub fn impl_trait_bounds(&self, db: &dyn HirDatabase) -> Option<Vec<QuantifiedWhereClause>> {
         match self.interned(&Interner) {
             TyKind::OpaqueType(opaque_ty_id, ..) => {
                 match db.lookup_intern_impl_trait_id((*opaque_ty_id).into()) {
@@ -905,10 +942,13 @@ impl Ty {
                             // This is only used by type walking.
                             // Parameters will be walked outside, and projection predicate is not used.
                             // So just provide the Future trait.
-                            let impl_bound = WhereClause::Implemented(TraitRef {
-                                trait_id: to_chalk_trait_id(future_trait),
-                                substitution: Substitution::empty(),
-                            });
+                            let impl_bound = Binders::new(
+                                0,
+                                WhereClause::Implemented(TraitRef {
+                                    trait_id: to_chalk_trait_id(future_trait),
+                                    substitution: Substitution::empty(),
+                                }),
+                            );
                             Some(vec![impl_bound])
                         } else {
                             None
@@ -953,6 +993,7 @@ impl Ty {
                                 }) => proj.self_type_parameter() == self,
                                 _ => false,
                             })
+                            .map(Binders::wrap_empty)
                             .collect_vec();
 
                         Some(predicates)
@@ -1094,8 +1135,8 @@ impl TypeWalk for Ty {
                     t.walk(f);
                 }
             }
-            TyKind::Dyn(predicates) => {
-                for p in predicates.iter() {
+            TyKind::Dyn(dyn_ty) => {
+                for p in dyn_ty.bounds.value.interned().iter() {
                     p.walk(f);
                 }
             }
@@ -1122,8 +1163,8 @@ impl TypeWalk for Ty {
             TyKind::Alias(AliasTy::Projection(p_ty)) => {
                 p_ty.substitution.walk_mut_binders(f, binders);
             }
-            TyKind::Dyn(predicates) => {
-                for p in make_mut_slice(predicates) {
+            TyKind::Dyn(dyn_ty) => {
+                for p in make_mut_slice(&mut dyn_ty.bounds.value.0) {
                     p.walk_mut_binders(f, binders.shifted_in());
                 }
             }
@@ -1173,7 +1214,7 @@ pub struct ReturnTypeImplTraits {
 
 #[derive(Clone, PartialEq, Eq, Debug, Hash)]
 pub(crate) struct ReturnTypeImplTrait {
-    pub(crate) bounds: Binders<Vec<WhereClause>>,
+    pub(crate) bounds: Binders<Vec<QuantifiedWhereClause>>,
 }
 
 pub fn to_foreign_def_id(id: TypeAliasId) -> ForeignDefId {
diff --git a/crates/hir_ty/src/lower.rs b/crates/hir_ty/src/lower.rs
index fd451a823..45591e920 100644
--- a/crates/hir_ty/src/lower.rs
+++ b/crates/hir_ty/src/lower.rs
@@ -33,9 +33,10 @@ use crate::{
         all_super_trait_refs, associated_type_by_name_including_super_traits, generics,
         variant_data,
     },
-    AliasEq, AliasTy, Binders, BoundVar, CallableSig, DebruijnIndex, FnPointer, FnSig, ImplTraitId,
-    OpaqueTy, PolyFnSig, ProjectionTy, ReturnTypeImplTrait, ReturnTypeImplTraits, Substitution,
-    TraitEnvironment, TraitRef, Ty, TyKind, TypeWalk, WhereClause,
+    AliasEq, AliasTy, Binders, BoundVar, CallableSig, DebruijnIndex, DynTy, FnPointer, FnSig,
+    ImplTraitId, OpaqueTy, PolyFnSig, ProjectionTy, QuantifiedWhereClause, QuantifiedWhereClauses,
+    ReturnTypeImplTrait, ReturnTypeImplTraits, Substitution, TraitEnvironment, TraitRef, Ty,
+    TyKind, TypeWalk, WhereClause,
 };
 
 #[derive(Debug)]
@@ -188,13 +189,14 @@ impl<'a> TyLoweringContext<'a> {
             TypeRef::DynTrait(bounds) => {
                 let self_ty =
                     TyKind::BoundVar(BoundVar::new(DebruijnIndex::INNERMOST, 0)).intern(&Interner);
-                let predicates = self.with_shifted_in(DebruijnIndex::ONE, |ctx| {
-                    bounds
-                        .iter()
-                        .flat_map(|b| ctx.lower_type_bound(b, self_ty.clone(), false))
-                        .collect()
+                let bounds = self.with_shifted_in(DebruijnIndex::ONE, |ctx| {
+                    QuantifiedWhereClauses::from_iter(
+                        &Interner,
+                        bounds.iter().flat_map(|b| ctx.lower_type_bound(b, self_ty.clone(), false)),
+                    )
                 });
-                TyKind::Dyn(predicates).intern(&Interner)
+                let bounds = Binders::new(1, bounds);
+                TyKind::Dyn(DynTy { bounds }).intern(&Interner)
             }
             TypeRef::ImplTrait(bounds) => {
                 match self.impl_trait_mode {
@@ -376,7 +378,16 @@ impl<'a> TyLoweringContext<'a> {
                     // FIXME report error (ambiguous associated type)
                     TyKind::Unknown.intern(&Interner)
                 } else {
-                    TyKind::Dyn(Arc::new([WhereClause::Implemented(trait_ref)])).intern(&Interner)
+                    let dyn_ty = DynTy {
+                        bounds: Binders::new(
+                            1,
+                            QuantifiedWhereClauses::from_iter(
+                                &Interner,
+                                Some(Binders::wrap_empty(WhereClause::Implemented(trait_ref))),
+                            ),
+                        ),
+                    };
+                    TyKind::Dyn(dyn_ty).intern(&Interner)
                 };
                 return (ty, None);
             }
@@ -670,7 +681,7 @@ impl<'a> TyLoweringContext<'a> {
         &'a self,
         where_predicate: &'a WherePredicate,
         ignore_bindings: bool,
-    ) -> impl Iterator<Item = WhereClause> + 'a {
+    ) -> impl Iterator<Item = QuantifiedWhereClause> + 'a {
         match where_predicate {
             WherePredicate::ForLifetime { target, bound, .. }
             | WherePredicate::TypeBound { target, bound } => {
@@ -705,12 +716,12 @@ impl<'a> TyLoweringContext<'a> {
         bound: &'a TypeBound,
         self_ty: Ty,
         ignore_bindings: bool,
-    ) -> impl Iterator<Item = WhereClause> + 'a {
+    ) -> impl Iterator<Item = QuantifiedWhereClause> + 'a {
         let mut bindings = None;
         let trait_ref = match bound {
             TypeBound::Path(path) => {
                 bindings = self.lower_trait_ref_from_path(path, Some(self_ty));
-                bindings.clone().map(WhereClause::Implemented)
+                bindings.clone().map(WhereClause::Implemented).map(|b| Binders::wrap_empty(b))
             }
             TypeBound::Lifetime(_) => None,
             TypeBound::Error => None,
@@ -727,7 +738,7 @@ impl<'a> TyLoweringContext<'a> {
         &'a self,
         bound: &'a TypeBound,
         trait_ref: TraitRef,
-    ) -> impl Iterator<Item = WhereClause> + 'a {
+    ) -> impl Iterator<Item = QuantifiedWhereClause> + 'a {
         let last_segment = match bound {
             TypeBound::Path(path) => path.segments().last(),
             TypeBound::Error | TypeBound::Lifetime(_) => None,
@@ -743,7 +754,7 @@ impl<'a> TyLoweringContext<'a> {
                     &binding.name,
                 );
                 let (super_trait_ref, associated_ty) = match found {
-                    None => return SmallVec::<[WhereClause; 1]>::new(),
+                    None => return SmallVec::<[QuantifiedWhereClause; 1]>::new(),
                     Some(t) => t,
                 };
                 let projection_ty = ProjectionTy {
@@ -757,7 +768,7 @@ impl<'a> TyLoweringContext<'a> {
                     let ty = self.lower_ty(type_ref);
                     let alias_eq =
                         AliasEq { alias: AliasTy::Projection(projection_ty.clone()), ty };
-                    preds.push(WhereClause::AliasEq(alias_eq));
+                    preds.push(Binders::wrap_empty(WhereClause::AliasEq(alias_eq)));
                 }
                 for bound in &binding.bounds {
                     preds.extend(self.lower_type_bound(
@@ -888,6 +899,9 @@ pub(crate) fn generic_predicates_for_param_query(
     db: &dyn HirDatabase,
     param_id: TypeParamId,
 ) -> Arc<[Binders<WhereClause>]> {
+    // FIXME: these binders are for the type parameters of the def. We need to
+    // introduce another level of binders for quantified where clauses (for<'a>
+    // ...)
     let resolver = param_id.parent.resolver(db.upcast());
     let ctx =
         TyLoweringContext::new(db, &resolver).with_type_param_mode(TypeParamLoweringMode::Variable);
@@ -906,7 +920,7 @@ pub(crate) fn generic_predicates_for_param_query(
             WherePredicate::Lifetime { .. } => false,
         })
         .flat_map(|pred| {
-            ctx.lower_where_predicate(pred, true).map(|p| Binders::new(generics.len(), p))
+            ctx.lower_where_predicate(pred, true).map(|p| Binders::new(generics.len(), p.value))
         })
         .collect()
 }
@@ -930,7 +944,7 @@ pub(crate) fn trait_environment_query(
     let mut clauses = Vec::new();
     for pred in resolver.where_predicates_in_scope() {
         for pred in ctx.lower_where_predicate(pred, false) {
-            if let WhereClause::Implemented(tr) = &pred {
+            if let WhereClause::Implemented(tr) = &pred.skip_binders() {
                 traits_in_scope.push((tr.self_type_parameter().clone(), tr.hir_trait_id()));
             }
             let program_clause: chalk_ir::ProgramClause<Interner> =
@@ -971,6 +985,9 @@ pub(crate) fn generic_predicates_query(
     db: &dyn HirDatabase,
     def: GenericDefId,
 ) -> Arc<[Binders<WhereClause>]> {
+    // FIXME: these binders are for the type parameters of the def. We need to
+    // introduce another level of binders for quantified where clauses (for<'a>
+    // ...)
     let resolver = def.resolver(db.upcast());
     let ctx =
         TyLoweringContext::new(db, &resolver).with_type_param_mode(TypeParamLoweringMode::Variable);
@@ -978,7 +995,7 @@ pub(crate) fn generic_predicates_query(
     resolver
         .where_predicates_in_scope()
         .flat_map(|pred| {
-            ctx.lower_where_predicate(pred, false).map(|p| Binders::new(generics.len(), p))
+            ctx.lower_where_predicate(pred, false).map(|p| Binders::new(generics.len(), p.value))
         })
         .collect()
 }
diff --git a/crates/hir_ty/src/traits/chalk.rs b/crates/hir_ty/src/traits/chalk.rs
index 944145603..4019fdf17 100644
--- a/crates/hir_ty/src/traits/chalk.rs
+++ b/crates/hir_ty/src/traits/chalk.rs
@@ -238,7 +238,10 @@ impl<'a> chalk_solve::RustIrDatabase<Interner> for ChalkContext<'a> {
                     });
                     let bound = OpaqueTyDatumBound {
                         bounds: make_binders(
-                            vec![impl_bound.to_chalk(self.db), proj_bound.to_chalk(self.db)],
+                            vec![
+                                wrap_in_empty_binders(impl_bound).to_chalk(self.db),
+                                wrap_in_empty_binders(proj_bound).to_chalk(self.db),
+                            ],
                             1,
                         ),
                         where_clauses: make_binders(vec![], 0),
@@ -397,7 +400,6 @@ pub(crate) fn associated_ty_data_query(
         .iter()
         .flat_map(|bound| ctx.lower_type_bound(bound, self_ty.clone(), false))
         .filter_map(|pred| generic_predicate_to_inline_bound(db, &pred, &self_ty))
-        .map(|bound| make_binders(bound.shifted_in(&Interner), 0))
         .collect();
 
     let where_clauses = convert_where_clauses(db, type_alias.into(), &bound_vars);
@@ -720,3 +722,7 @@ impl From<crate::db::InternedClosureId> for chalk_ir::ClosureId<Interner> {
         chalk_ir::ClosureId(id.as_intern_id())
     }
 }
+
+fn wrap_in_empty_binders<T: crate::TypeWalk>(value: T) -> crate::Binders<T> {
+    crate::Binders::wrap_empty(value)
+}
diff --git a/crates/hir_ty/src/traits/chalk/mapping.rs b/crates/hir_ty/src/traits/chalk/mapping.rs
index 65feb82e5..5b9c7e831 100644
--- a/crates/hir_ty/src/traits/chalk/mapping.rs
+++ b/crates/hir_ty/src/traits/chalk/mapping.rs
@@ -7,15 +7,14 @@ use chalk_ir::{cast::Cast, fold::shift::Shift, interner::HasInterner, LifetimeDa
 use chalk_solve::rust_ir;
 
 use base_db::salsa::InternKey;
-use hir_def::{AssocContainerId, GenericDefId, Lookup, TypeAliasId};
+use hir_def::{GenericDefId, TypeAliasId};
 
 use crate::{
     db::HirDatabase,
-    from_assoc_type_id,
     primitive::UintTy,
     traits::{Canonical, DomainGoal},
-    AliasTy, CallableDefId, FnPointer, InEnvironment, OpaqueTy, ProjectionTy, Scalar, Substitution,
-    TraitRef, Ty, WhereClause,
+    AliasTy, CallableDefId, FnPointer, InEnvironment, OpaqueTy, ProjectionTy,
+    QuantifiedWhereClause, Scalar, Substitution, TraitRef, Ty, TypeWalk, WhereClause,
 };
 
 use super::interner::*;
@@ -95,10 +94,10 @@ impl ToChalk for Ty {
             TyKind::Placeholder(idx) => idx.to_ty::<Interner>(&Interner),
             TyKind::BoundVar(idx) => chalk_ir::TyKind::BoundVar(idx).intern(&Interner),
             TyKind::InferenceVar(..) => panic!("uncanonicalized infer ty"),
-            TyKind::Dyn(predicates) => {
+            TyKind::Dyn(dyn_ty) => {
                 let where_clauses = chalk_ir::QuantifiedWhereClauses::from_iter(
                     &Interner,
-                    predicates.iter().cloned().map(|p| p.to_chalk(db)),
+                    dyn_ty.bounds.value.interned().iter().cloned().map(|p| p.to_chalk(db)),
                 );
                 let bounded_ty = chalk_ir::DynTy {
                     bounds: make_binders(where_clauses, 1),
@@ -144,13 +143,17 @@ impl ToChalk for Ty {
             chalk_ir::TyKind::InferenceVar(_iv, _kind) => TyKind::Unknown,
             chalk_ir::TyKind::Dyn(where_clauses) => {
                 assert_eq!(where_clauses.bounds.binders.len(&Interner), 1);
-                let predicates = where_clauses
+                let bounds = where_clauses
                     .bounds
                     .skip_binders()
                     .iter(&Interner)
-                    .map(|c| from_chalk(db, c.clone()))
-                    .collect();
-                TyKind::Dyn(predicates)
+                    .map(|c| from_chalk(db, c.clone()));
+                TyKind::Dyn(crate::DynTy {
+                    bounds: crate::Binders::new(
+                        1,
+                        crate::QuantifiedWhereClauses::from_iter(&Interner, bounds),
+                    ),
+                })
             }
 
             chalk_ir::TyKind::Adt(adt_id, subst) => TyKind::Adt(adt_id, from_chalk(db, subst)),
@@ -305,33 +308,22 @@ impl ToChalk for TypeAliasAsValue {
 }
 
 impl ToChalk for WhereClause {
-    type Chalk = chalk_ir::QuantifiedWhereClause<Interner>;
+    type Chalk = chalk_ir::WhereClause<Interner>;
 
-    fn to_chalk(self, db: &dyn HirDatabase) -> chalk_ir::QuantifiedWhereClause<Interner> {
+    fn to_chalk(self, db: &dyn HirDatabase) -> chalk_ir::WhereClause<Interner> {
         match self {
             WhereClause::Implemented(trait_ref) => {
-                let chalk_trait_ref = trait_ref.to_chalk(db);
-                let chalk_trait_ref = chalk_trait_ref.shifted_in(&Interner);
-                make_binders(chalk_ir::WhereClause::Implemented(chalk_trait_ref), 0)
+                chalk_ir::WhereClause::Implemented(trait_ref.to_chalk(db))
             }
-            WhereClause::AliasEq(alias_eq) => make_binders(
-                chalk_ir::WhereClause::AliasEq(alias_eq.to_chalk(db).shifted_in(&Interner)),
-                0,
-            ),
+            WhereClause::AliasEq(alias_eq) => chalk_ir::WhereClause::AliasEq(alias_eq.to_chalk(db)),
         }
     }
 
     fn from_chalk(
         db: &dyn HirDatabase,
-        where_clause: chalk_ir::QuantifiedWhereClause<Interner>,
+        where_clause: chalk_ir::WhereClause<Interner>,
     ) -> WhereClause {
-        // we don't produce any where clauses with binders and can't currently deal with them
-        match where_clause
-            .skip_binders()
-            .clone()
-            .shifted_out(&Interner)
-            .expect("unexpected bound vars in where clause")
-        {
+        match where_clause {
             chalk_ir::WhereClause::Implemented(tr) => WhereClause::Implemented(from_chalk(db, tr)),
             chalk_ir::WhereClause::AliasEq(alias_eq) => {
                 WhereClause::AliasEq(from_chalk(db, alias_eq))
@@ -500,6 +492,29 @@ where
     }
 }
 
+impl<T: ToChalk> ToChalk for crate::Binders<T>
+where
+    T::Chalk: chalk_ir::interner::HasInterner<Interner = Interner>,
+{
+    type Chalk = chalk_ir::Binders<T::Chalk>;
+
+    fn to_chalk(self, db: &dyn HirDatabase) -> chalk_ir::Binders<T::Chalk> {
+        chalk_ir::Binders::new(
+            chalk_ir::VariableKinds::from_iter(
+                &Interner,
+                std::iter::repeat(chalk_ir::VariableKind::Ty(chalk_ir::TyVariableKind::General))
+                    .take(self.num_binders),
+            ),
+            self.value.to_chalk(db),
+        )
+    }
+
+    fn from_chalk(db: &dyn HirDatabase, binders: chalk_ir::Binders<T::Chalk>) -> crate::Binders<T> {
+        let (v, b) = binders.into_value_and_skipped_binders();
+        crate::Binders::new(b.len(&Interner), from_chalk(db, v))
+    }
+}
+
 pub(super) fn make_binders<T>(value: T, num_vars: usize) -> chalk_ir::Binders<T>
 where
     T: HasInterner<Interner = Interner>,
@@ -522,21 +537,22 @@ pub(super) fn convert_where_clauses(
     let generic_predicates = db.generic_predicates(def);
     let mut result = Vec::with_capacity(generic_predicates.len());
     for pred in generic_predicates.iter() {
-        result.push(pred.clone().subst(substs).to_chalk(db));
+        result.push(crate::Binders::wrap_empty(pred.clone().subst(substs)).to_chalk(db));
     }
     result
 }
 
 pub(super) fn generic_predicate_to_inline_bound(
     db: &dyn HirDatabase,
-    pred: &WhereClause,
+    pred: &QuantifiedWhereClause,
     self_ty: &Ty,
-) -> Option<rust_ir::InlineBound<Interner>> {
+) -> Option<chalk_ir::Binders<rust_ir::InlineBound<Interner>>> {
     // An InlineBound is like a GenericPredicate, except the self type is left out.
     // We don't have a special type for this, but Chalk does.
-    match pred {
+    let self_ty_shifted_in = self_ty.clone().shift_bound_vars(DebruijnIndex::ONE);
+    match &pred.value {
         WhereClause::Implemented(trait_ref) => {
-            if &trait_ref.substitution[0] != self_ty {
+            if trait_ref.self_type_parameter() != &self_ty_shifted_in {
                 // we can only convert predicates back to type bounds if they
                 // have the expected self type
                 return None;
@@ -546,19 +562,13 @@ pub(super) fn generic_predicate_to_inline_bound(
                 .map(|ty| ty.clone().to_chalk(db).cast(&Interner))
                 .collect();
             let trait_bound = rust_ir::TraitBound { trait_id: trait_ref.trait_id, args_no_self };
-            Some(rust_ir::InlineBound::TraitBound(trait_bound))
+            Some(make_binders(rust_ir::InlineBound::TraitBound(trait_bound), pred.num_binders))
         }
         WhereClause::AliasEq(AliasEq { alias: AliasTy::Projection(projection_ty), ty }) => {
-            if &projection_ty.substitution[0] != self_ty {
+            if projection_ty.self_type_parameter() != &self_ty_shifted_in {
                 return None;
             }
-            let trait_ = match from_assoc_type_id(projection_ty.associated_ty_id)
-                .lookup(db.upcast())
-                .container
-            {
-                AssocContainerId::TraitId(t) => t,
-                _ => panic!("associated type not in trait"),
-            };
+            let trait_ = projection_ty.trait_(db);
             let args_no_self = projection_ty.substitution[1..]
                 .iter()
                 .map(|ty| ty.clone().to_chalk(db).cast(&Interner))
@@ -569,7 +579,7 @@ pub(super) fn generic_predicate_to_inline_bound(
                 associated_ty_id: projection_ty.associated_ty_id,
                 parameters: Vec::new(), // FIXME we don't support generic associated types yet
             };
-            Some(rust_ir::InlineBound::AliasEqBound(alias_eq_bound))
+            Some(make_binders(rust_ir::InlineBound::AliasEqBound(alias_eq_bound), pred.num_binders))
         }
         _ => None,
     }