11 files changed, 215 insertions, 113 deletions

diff --git a/crates/hir/src/lib.rs b/crates/hir/src/lib.rs
index e3ac37e4c..a325b6691 100644
--- a/crates/hir/src/lib.rs
+++ b/crates/hir/src/lib.rs
@@ -57,8 +57,8 @@ use hir_ty::{
     to_assoc_type_id,
     traits::{FnTrait, Solution, SolutionVariables},
     AliasEq, AliasTy, BoundVar, CallableDefId, CallableSig, Canonical, Cast, DebruijnIndex,
-    InEnvironment, Interner, ProjectionTy, Scalar, Substitution, Ty, TyDefId, TyKind,
-    TyVariableKind, WhereClause,
+    InEnvironment, Interner, ProjectionTy, QuantifiedWhereClause, Scalar, Substitution, Ty,
+    TyDefId, TyKind, TyVariableKind, WhereClause,
 };
 use itertools::Itertools;
 use rustc_hash::FxHashSet;
@@ -1460,7 +1460,7 @@ impl TypeParam {
     pub fn trait_bounds(self, db: &dyn HirDatabase) -> Vec<Trait> {
         db.generic_predicates_for_param(self.id)
             .into_iter()
-            .filter_map(|pred| match &pred.value {
+            .filter_map(|pred| match &pred.skip_binders().skip_binders() {
                 hir_ty::WhereClause::Implemented(trait_ref) => {
                     Some(Trait::from(trait_ref.hir_trait_id()))
                 }
@@ -2022,7 +2022,7 @@ impl Type {
     pub fn as_impl_traits(&self, db: &dyn HirDatabase) -> Option<Vec<Trait>> {
         self.ty.value.impl_trait_bounds(db).map(|it| {
             it.into_iter()
-                .filter_map(|pred| match pred {
+                .filter_map(|pred| match pred.skip_binders() {
                     hir_ty::WhereClause::Implemented(trait_ref) => {
                         Some(Trait::from(trait_ref.hir_trait_id()))
                     }
@@ -2061,11 +2061,11 @@ impl Type {
         fn walk_bounds(
             db: &dyn HirDatabase,
             type_: &Type,
-            bounds: &[WhereClause],
+            bounds: &[QuantifiedWhereClause],
             cb: &mut impl FnMut(Type),
         ) {
             for pred in bounds {
-                match pred {
+                match pred.skip_binders() {
                     WhereClause::Implemented(trait_ref) => {
                         cb(type_.clone());
                         // skip the self type. it's likely the type we just got the bounds from
@@ -2107,7 +2107,12 @@ impl Type {
                     }
                 }
                 TyKind::Dyn(bounds) => {
-                    walk_bounds(db, &type_.derived(ty.clone()), bounds.as_ref(), cb);
+                    walk_bounds(
+                        db,
+                        &type_.derived(ty.clone()),
+                        bounds.bounds.skip_binders().interned(),
+                        cb,
+                    );
                 }
 
                 TyKind::Ref(_, ty) | TyKind::Raw(_, ty) | TyKind::Array(ty) | TyKind::Slice(ty) => {
diff --git a/crates/hir_ty/src/db.rs b/crates/hir_ty/src/db.rs
index 91a2e0b5b..58e4247c6 100644
--- a/crates/hir_ty/src/db.rs
+++ b/crates/hir_ty/src/db.rs
@@ -12,8 +12,8 @@ use la_arena::ArenaMap;
 use crate::{
     method_resolution::{InherentImpls, TraitImpls},
     traits::chalk,
-    Binders, CallableDefId, FnDefId, ImplTraitId, InferenceResult, PolyFnSig, ReturnTypeImplTraits,
-    TraitRef, Ty, TyDefId, ValueTyDefId, WhereClause,
+    Binders, CallableDefId, FnDefId, ImplTraitId, InferenceResult, PolyFnSig,
+    QuantifiedWhereClause, ReturnTypeImplTraits, TraitRef, Ty, TyDefId, ValueTyDefId,
 };
 use hir_expand::name::Name;
 
@@ -57,10 +57,13 @@ pub trait HirDatabase: DefDatabase + Upcast<dyn DefDatabase> {
 
     #[salsa::invoke(crate::lower::generic_predicates_for_param_query)]
     #[salsa::cycle(crate::lower::generic_predicates_for_param_recover)]
-    fn generic_predicates_for_param(&self, param_id: TypeParamId) -> Arc<[Binders<WhereClause>]>;
+    fn generic_predicates_for_param(
+        &self,
+        param_id: TypeParamId,
+    ) -> Arc<[Binders<QuantifiedWhereClause>]>;
 
     #[salsa::invoke(crate::lower::generic_predicates_query)]
-    fn generic_predicates(&self, def: GenericDefId) -> Arc<[Binders<WhereClause>]>;
+    fn generic_predicates(&self, def: GenericDefId) -> Arc<[Binders<QuantifiedWhereClause>]>;
 
     #[salsa::invoke(crate::lower::trait_environment_query)]
     fn trait_environment(&self, def: GenericDefId) -> Arc<crate::TraitEnvironment>;
diff --git a/crates/hir_ty/src/display.rs b/crates/hir_ty/src/display.rs
index 9d3b79be3..cc6b93d37 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);
                     }
                 }
@@ -577,7 +581,7 @@ impl HirDisplay for Ty {
                             .generic_predicates(id.parent)
                             .into_iter()
                             .map(|pred| pred.clone().subst(&substs))
-                            .filter(|wc| match &wc {
+                            .filter(|wc| match &wc.skip_binders() {
                                 WhereClause::Implemented(tr) => tr.self_type_parameter() == self,
                                 WhereClause::AliasEq(AliasEq {
                                     alias: AliasTy::Projection(proj),
@@ -591,8 +595,12 @@ impl HirDisplay for Ty {
                 }
             }
             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 +669,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 +682,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 +695,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/expr.rs b/crates/hir_ty/src/infer/expr.rs
index 24deff707..05cbde4e3 100644
--- a/crates/hir_ty/src/infer/expr.rs
+++ b/crates/hir_ty/src/infer/expr.rs
@@ -11,6 +11,7 @@ use hir_def::{
     AssocContainerId, FieldId, Lookup,
 };
 use hir_expand::name::{name, Name};
+use stdx::always;
 use syntax::ast::RangeOp;
 
 use crate::{
@@ -936,7 +937,9 @@ impl<'a> InferenceContext<'a> {
             let def: CallableDefId = from_chalk(self.db, *fn_def);
             let generic_predicates = self.db.generic_predicates(def.into());
             for predicate in generic_predicates.iter() {
-                let predicate = predicate.clone().subst(parameters);
+                let (predicate, binders) =
+                    predicate.clone().subst(parameters).into_value_and_skipped_binders();
+                always!(binders == 0); // quantified where clauses not yet handled
                 self.obligations.push(predicate.cast(&Interner));
             }
             // add obligation for trait implementation, if this is a trait method
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..90b5b17e2 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,14 @@ 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
+    }
+
+    pub fn into_value_and_skipped_binders(self) -> (T, usize) {
+        (self.value, self.num_binders)
+    }
 }
 
 impl<T: Clone> Binders<&T> {
@@ -614,6 +635,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 +849,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 +933,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 +946,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
@@ -945,7 +989,7 @@ impl Ty {
                             .generic_predicates(id.parent)
                             .into_iter()
                             .map(|pred| pred.clone().subst(&substs))
-                            .filter(|wc| match &wc {
+                            .filter(|wc| match &wc.skip_binders() {
                                 WhereClause::Implemented(tr) => tr.self_type_parameter() == self,
                                 WhereClause::AliasEq(AliasEq {
                                     alias: AliasTy::Projection(proj),
@@ -1094,8 +1138,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 +1166,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 +1217,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..f60cec649 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(
@@ -814,7 +825,7 @@ pub fn associated_type_shorthand_candidates<R>(
             let predicates = db.generic_predicates_for_param(param_id);
             let mut traits_: Vec<_> = predicates
                 .iter()
-                .filter_map(|pred| match &pred.value {
+                .filter_map(|pred| match &pred.value.value {
                     WhereClause::Implemented(tr) => Some(tr.clone()),
                     _ => None,
                 })
@@ -887,7 +898,7 @@ pub(crate) fn field_types_query(
 pub(crate) fn generic_predicates_for_param_query(
     db: &dyn HirDatabase,
     param_id: TypeParamId,
-) -> Arc<[Binders<WhereClause>]> {
+) -> Arc<[Binders<QuantifiedWhereClause>]> {
     let resolver = param_id.parent.resolver(db.upcast());
     let ctx =
         TyLoweringContext::new(db, &resolver).with_type_param_mode(TypeParamLoweringMode::Variable);
@@ -915,7 +926,7 @@ pub(crate) fn generic_predicates_for_param_recover(
     _db: &dyn HirDatabase,
     _cycle: &[String],
     _param_id: &TypeParamId,
-) -> Arc<[Binders<WhereClause>]> {
+) -> Arc<[Binders<QuantifiedWhereClause>]> {
     Arc::new([])
 }
 
@@ -930,7 +941,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> =
@@ -970,7 +981,7 @@ pub(crate) fn trait_environment_query(
 pub(crate) fn generic_predicates_query(
     db: &dyn HirDatabase,
     def: GenericDefId,
-) -> Arc<[Binders<WhereClause>]> {
+) -> Arc<[Binders<QuantifiedWhereClause>]> {
     let resolver = def.resolver(db.upcast());
     let ctx =
         TyLoweringContext::new(db, &resolver).with_type_param_mode(TypeParamLoweringMode::Variable);
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..7209dd14e 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>,
@@ -529,14 +544,15 @@ pub(super) fn convert_where_clauses(
 
 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,
     }
diff --git a/crates/hir_ty/src/utils.rs b/crates/hir_ty/src/utils.rs
index 1ec1ecd43..19874e42b 100644
--- a/crates/hir_ty/src/utils.rs
+++ b/crates/hir_ty/src/utils.rs
@@ -63,7 +63,7 @@ fn direct_super_trait_refs(db: &dyn HirDatabase, trait_ref: &TraitRef) -> Vec<Tr
     db.generic_predicates_for_param(trait_self)
         .iter()
         .filter_map(|pred| {
-            pred.as_ref().filter_map(|pred| match pred {
+            pred.as_ref().filter_map(|pred| match pred.skip_binders() {
                 WhereClause::Implemented(tr) => Some(tr.clone()),
                 _ => None,
             })
diff --git a/docs/dev/README.md b/docs/dev/README.md
index b91013f13..57162a47d 100644
--- a/docs/dev/README.md
+++ b/docs/dev/README.md
@@ -226,6 +226,9 @@ If the GitHub Actions release fails because of a transient problem like a timeou
 If it fails because of something that needs to be fixed, remove the release tag (if needed), fix the problem, then start over.
 Make sure to remove the new changelog post created when running `cargo xtask release` a second time.
 
+We release "nightly" every night automatically and promote the latest nightly to "stable" manually, every week.
+We don't do "patch" releases, unless something truly egregious comes up.
+
 # Permissions
 
 There are three sets of people with extra permissions: