diff --git a/crates/hir_ty/src/builder.rs b/crates/hir_ty/src/builder.rs
index 372621f7378..7b8603fd77e 100644
--- a/crates/hir_ty/src/builder.rs
+++ b/crates/hir_ty/src/builder.rs
@@ -194,7 +194,7 @@ impl TyBuilder<TypeAliasId> {
 
 impl<T: TypeWalk + HasInterner<Interner = Interner>> TyBuilder<Binders<T>> {
     fn subst_binders(b: Binders<T>) -> Self {
-        let param_count = b.num_binders;
+        let param_count = b.binders.len(&Interner);
         TyBuilder::new(b, param_count)
     }
 
diff --git a/crates/hir_ty/src/infer/expr.rs b/crates/hir_ty/src/infer/expr.rs
index ccaae53e983..d61ef65f258 100644
--- a/crates/hir_ty/src/infer/expr.rs
+++ b/crates/hir_ty/src/infer/expr.rs
@@ -849,7 +849,7 @@ impl<'a> InferenceContext<'a> {
                 self.write_method_resolution(tgt_expr, func);
                 (ty, self.db.value_ty(func.into()), Some(generics(self.db.upcast(), func.into())))
             }
-            None => (receiver_ty, Binders::new(0, self.err_ty()), None),
+            None => (receiver_ty, Binders::empty(&Interner, self.err_ty()), None),
         };
         let substs = self.substs_for_method_call(def_generics, generic_args, &derefed_receiver_ty);
         let method_ty = method_ty.subst(&substs);
@@ -951,7 +951,7 @@ impl<'a> InferenceContext<'a> {
             for predicate in generic_predicates.iter() {
                 let (predicate, binders) =
                     predicate.clone().subst(parameters).into_value_and_skipped_binders();
-                always!(binders == 0); // quantified where clauses not yet handled
+                always!(binders.len(&Interner) == 0); // quantified where clauses not yet handled
                 self.push_obligation(predicate.cast(&Interner));
             }
             // add obligation for trait implementation, if this is a trait method
diff --git a/crates/hir_ty/src/lib.rs b/crates/hir_ty/src/lib.rs
index 61b5cf269af..86973c7ed11 100644
--- a/crates/hir_ty/src/lib.rs
+++ b/crates/hir_ty/src/lib.rs
@@ -66,6 +66,8 @@ pub type ClosureId = chalk_ir::ClosureId<Interner>;
 pub type OpaqueTyId = chalk_ir::OpaqueTyId<Interner>;
 pub type PlaceholderIndex = chalk_ir::PlaceholderIndex;
 
+pub type VariableKind = chalk_ir::VariableKind<Interner>;
+pub type VariableKinds = chalk_ir::VariableKinds<Interner>;
 pub type CanonicalVarKinds = chalk_ir::CanonicalVarKinds<Interner>;
 
 pub type ChalkTraitId = chalk_ir::TraitId<Interner>;
@@ -126,22 +128,26 @@ impl<T> Binders<T> {
     }
 }
 
-impl<T: Clone> Binders<&T> {
-    pub fn cloned(&self) -> Binders<T> {
-        let (value, binders) = self.into_value_and_skipped_binders();
-        Binders::new(binders, value.clone())
-    }
-}
-
 impl<T: TypeWalk> Binders<T> {
     /// Substitutes all variables.
     pub fn subst(self, subst: &Substitution) -> T {
         let (value, binders) = self.into_value_and_skipped_binders();
-        assert_eq!(subst.len(&Interner), binders);
+        assert_eq!(subst.len(&Interner), binders.len(&Interner));
         value.subst_bound_vars(subst)
     }
 }
 
+pub fn make_only_type_binders<T>(num_vars: usize, value: T) -> Binders<T> {
+    Binders::new(
+        VariableKinds::from_iter(
+            &Interner,
+            std::iter::repeat(chalk_ir::VariableKind::Ty(chalk_ir::TyVariableKind::General))
+                .take(num_vars),
+        ),
+        value,
+    )
+}
+
 impl TraitRef {
     pub fn self_type_parameter(&self, interner: &Interner) -> &Ty {
         &self.substitution.at(interner, 0).assert_ty_ref(interner)
@@ -407,8 +413,8 @@ 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 = Binders::new(
-                                0,
+                            let impl_bound = Binders::empty(
+                                &Interner,
                                 WhereClause::Implemented(TraitRef {
                                     trait_id: to_chalk_trait_id(future_trait),
                                     substitution: Substitution::empty(&Interner),
diff --git a/crates/hir_ty/src/lower.rs b/crates/hir_ty/src/lower.rs
index 19465b2ed08..59d2a157fb5 100644
--- a/crates/hir_ty/src/lower.rs
+++ b/crates/hir_ty/src/lower.rs
@@ -31,7 +31,7 @@ use crate::{
     traits::chalk::{Interner, ToChalk},
     utils::{
         all_super_trait_refs, associated_type_by_name_including_super_traits, generics,
-        variant_data,
+        variant_data, Generics,
     },
     AliasEq, AliasTy, Binders, BoundVar, CallableSig, DebruijnIndex, DynTy, FnPointer, FnSig,
     ImplTraitId, OpaqueTy, PolyFnSig, ProjectionTy, QuantifiedWhereClause, QuantifiedWhereClauses,
@@ -196,7 +196,7 @@ impl<'a> TyLoweringContext<'a> {
                         bounds.iter().flat_map(|b| ctx.lower_type_bound(b, self_ty.clone(), false)),
                     )
                 });
-                let bounds = Binders::new(1, bounds);
+                let bounds = crate::make_only_type_binders(1, bounds);
                 TyKind::Dyn(DynTy { bounds }).intern(&Interner)
             }
             TypeRef::ImplTrait(bounds) => {
@@ -209,9 +209,9 @@ impl<'a> TyLoweringContext<'a> {
                         // this dance is to make sure the data is in the right
                         // place even if we encounter more opaque types while
                         // lowering the bounds
-                        self.opaque_type_data
-                            .borrow_mut()
-                            .push(ReturnTypeImplTrait { bounds: Binders::new(1, Vec::new()) });
+                        self.opaque_type_data.borrow_mut().push(ReturnTypeImplTrait {
+                            bounds: crate::make_only_type_binders(1, Vec::new()),
+                        });
                         // We don't want to lower the bounds inside the binders
                         // we're currently in, because they don't end up inside
                         // those binders. E.g. when we have `impl Trait<impl
@@ -380,7 +380,7 @@ impl<'a> TyLoweringContext<'a> {
                     TyKind::Error.intern(&Interner)
                 } else {
                     let dyn_ty = DynTy {
-                        bounds: Binders::new(
+                        bounds: crate::make_only_type_binders(
                             1,
                             QuantifiedWhereClauses::from_iter(
                                 &Interner,
@@ -787,7 +787,7 @@ impl<'a> TyLoweringContext<'a> {
         let predicates = self.with_shifted_in(DebruijnIndex::ONE, |ctx| {
             bounds.iter().flat_map(|b| ctx.lower_type_bound(b, self_ty.clone(), false)).collect()
         });
-        ReturnTypeImplTrait { bounds: Binders::new(1, predicates) }
+        ReturnTypeImplTrait { bounds: crate::make_only_type_binders(1, predicates) }
     }
 }
 
@@ -884,7 +884,7 @@ pub(crate) fn field_types_query(
     let ctx =
         TyLoweringContext::new(db, &resolver).with_type_param_mode(TypeParamLoweringMode::Variable);
     for (field_id, field_data) in var_data.fields().iter() {
-        res.insert(field_id, Binders::new(generics.len(), ctx.lower_ty(&field_data.type_ref)))
+        res.insert(field_id, make_binders(&generics, ctx.lower_ty(&field_data.type_ref)))
     }
     Arc::new(res)
 }
@@ -918,9 +918,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))
-        })
+        .flat_map(|pred| ctx.lower_where_predicate(pred, true).map(|p| make_binders(&generics, p)))
         .collect()
 }
 
@@ -991,9 +989,7 @@ pub(crate) fn generic_predicates_query(
     let generics = generics(db.upcast(), def);
     resolver
         .where_predicates_in_scope()
-        .flat_map(|pred| {
-            ctx.lower_where_predicate(pred, false).map(|p| Binders::new(generics.len(), p))
-        })
+        .flat_map(|pred| ctx.lower_where_predicate(pred, false).map(|p| make_binders(&generics, p)))
         .collect()
 }
 
@@ -1030,7 +1026,7 @@ pub(crate) fn generic_defaults_query(
                 DebruijnIndex::INNERMOST,
             );
 
-            Binders::new(idx, ty)
+            crate::make_only_type_binders(idx, ty)
         })
         .collect();
 
@@ -1043,14 +1039,13 @@ fn fn_sig_for_fn(db: &dyn HirDatabase, def: FunctionId) -> PolyFnSig {
     let ctx_params = TyLoweringContext::new(db, &resolver)
         .with_impl_trait_mode(ImplTraitLoweringMode::Variable)
         .with_type_param_mode(TypeParamLoweringMode::Variable);
-    let params = data.params.iter().map(|tr| (&ctx_params).lower_ty(tr)).collect::<Vec<_>>();
+    let params = data.params.iter().map(|tr| ctx_params.lower_ty(tr)).collect::<Vec<_>>();
     let ctx_ret = TyLoweringContext::new(db, &resolver)
         .with_impl_trait_mode(ImplTraitLoweringMode::Opaque)
         .with_type_param_mode(TypeParamLoweringMode::Variable);
-    let ret = (&ctx_ret).lower_ty(&data.ret_type);
+    let ret = ctx_ret.lower_ty(&data.ret_type);
     let generics = generics(db.upcast(), def.into());
-    let num_binders = generics.len();
-    Binders::new(num_binders, CallableSig::from_params_and_return(params, ret, data.is_varargs()))
+    make_binders(&generics, CallableSig::from_params_and_return(params, ret, data.is_varargs()))
 }
 
 /// Build the declared type of a function. This should not need to look at the
@@ -1058,8 +1053,8 @@ fn fn_sig_for_fn(db: &dyn HirDatabase, def: FunctionId) -> PolyFnSig {
 fn type_for_fn(db: &dyn HirDatabase, def: FunctionId) -> Binders<Ty> {
     let generics = generics(db.upcast(), def.into());
     let substs = generics.bound_vars_subst(DebruijnIndex::INNERMOST);
-    Binders::new(
-        substs.len(&Interner),
+    make_binders(
+        &generics,
         TyKind::FnDef(CallableDefId::FunctionId(def).to_chalk(db), substs).intern(&Interner),
     )
 }
@@ -1072,7 +1067,7 @@ fn type_for_const(db: &dyn HirDatabase, def: ConstId) -> Binders<Ty> {
     let ctx =
         TyLoweringContext::new(db, &resolver).with_type_param_mode(TypeParamLoweringMode::Variable);
 
-    Binders::new(generics.len(), ctx.lower_ty(&data.type_ref))
+    make_binders(&generics, ctx.lower_ty(&data.type_ref))
 }
 
 /// Build the declared type of a static.
@@ -1081,7 +1076,7 @@ fn type_for_static(db: &dyn HirDatabase, def: StaticId) -> Binders<Ty> {
     let resolver = def.resolver(db.upcast());
     let ctx = TyLoweringContext::new(db, &resolver);
 
-    Binders::new(0, ctx.lower_ty(&data.type_ref))
+    Binders::empty(&Interner, ctx.lower_ty(&data.type_ref))
 }
 
 fn fn_sig_for_struct_constructor(db: &dyn HirDatabase, def: StructId) -> PolyFnSig {
@@ -1103,8 +1098,8 @@ fn type_for_struct_constructor(db: &dyn HirDatabase, def: StructId) -> Binders<T
     }
     let generics = generics(db.upcast(), def.into());
     let substs = generics.bound_vars_subst(DebruijnIndex::INNERMOST);
-    Binders::new(
-        substs.len(&Interner),
+    make_binders(
+        &generics,
         TyKind::FnDef(CallableDefId::StructId(def).to_chalk(db), substs).intern(&Interner),
     )
 }
@@ -1130,17 +1125,17 @@ fn type_for_enum_variant_constructor(db: &dyn HirDatabase, def: EnumVariantId) -
     }
     let generics = generics(db.upcast(), def.parent.into());
     let substs = generics.bound_vars_subst(DebruijnIndex::INNERMOST);
-    Binders::new(
-        substs.len(&Interner),
+    make_binders(
+        &generics,
         TyKind::FnDef(CallableDefId::EnumVariantId(def).to_chalk(db), substs).intern(&Interner),
     )
 }
 
 fn type_for_adt(db: &dyn HirDatabase, adt: AdtId) -> Binders<Ty> {
+    let generics = generics(db.upcast(), adt.into());
     let b = TyBuilder::adt(db, adt);
-    let num_binders = b.remaining();
     let ty = b.fill_with_bound_vars(DebruijnIndex::INNERMOST, 0).build();
-    Binders::new(num_binders, ty)
+    make_binders(&generics, ty)
 }
 
 fn type_for_type_alias(db: &dyn HirDatabase, t: TypeAliasId) -> Binders<Ty> {
@@ -1149,11 +1144,11 @@ fn type_for_type_alias(db: &dyn HirDatabase, t: TypeAliasId) -> Binders<Ty> {
     let ctx =
         TyLoweringContext::new(db, &resolver).with_type_param_mode(TypeParamLoweringMode::Variable);
     if db.type_alias_data(t).is_extern {
-        Binders::new(0, TyKind::Foreign(crate::to_foreign_def_id(t)).intern(&Interner))
+        Binders::empty(&Interner, TyKind::Foreign(crate::to_foreign_def_id(t)).intern(&Interner))
     } else {
         let type_ref = &db.type_alias_data(t).type_ref;
         let inner = ctx.lower_ty(type_ref.as_deref().unwrap_or(&TypeRef::Error));
-        Binders::new(generics.len(), inner)
+        make_binders(&generics, inner)
     }
 }
 
@@ -1212,19 +1207,21 @@ impl_from!(FunctionId, StructId, UnionId, EnumVariantId, ConstId, StaticId for V
 /// namespace.
 pub(crate) fn ty_query(db: &dyn HirDatabase, def: TyDefId) -> Binders<Ty> {
     match def {
-        TyDefId::BuiltinType(it) => Binders::new(0, TyBuilder::builtin(it)),
+        TyDefId::BuiltinType(it) => Binders::empty(&Interner, TyBuilder::builtin(it)),
         TyDefId::AdtId(it) => type_for_adt(db, it),
         TyDefId::TypeAliasId(it) => type_for_type_alias(db, it),
     }
 }
 
 pub(crate) fn ty_recover(db: &dyn HirDatabase, _cycle: &[String], def: &TyDefId) -> Binders<Ty> {
-    let num_binders = match *def {
-        TyDefId::BuiltinType(_) => 0,
-        TyDefId::AdtId(it) => generics(db.upcast(), it.into()).len(),
-        TyDefId::TypeAliasId(it) => generics(db.upcast(), it.into()).len(),
+    let generics = match *def {
+        TyDefId::BuiltinType(_) => {
+            return Binders::empty(&Interner, TyKind::Error.intern(&Interner))
+        }
+        TyDefId::AdtId(it) => generics(db.upcast(), it.into()),
+        TyDefId::TypeAliasId(it) => generics(db.upcast(), it.into()),
     };
-    Binders::new(num_binders, TyKind::Error.intern(&Interner))
+    make_binders(&generics, TyKind::Error.intern(&Interner))
 }
 
 pub(crate) fn value_ty_query(db: &dyn HirDatabase, def: ValueTyDefId) -> Binders<Ty> {
@@ -1244,7 +1241,7 @@ pub(crate) fn impl_self_ty_query(db: &dyn HirDatabase, impl_id: ImplId) -> Binde
     let generics = generics(db.upcast(), impl_id.into());
     let ctx =
         TyLoweringContext::new(db, &resolver).with_type_param_mode(TypeParamLoweringMode::Variable);
-    Binders::new(generics.len(), ctx.lower_ty(&impl_data.self_ty))
+    make_binders(&generics, ctx.lower_ty(&impl_data.self_ty))
 }
 
 pub(crate) fn const_param_ty_query(db: &dyn HirDatabase, def: ConstParamId) -> Ty {
@@ -1262,7 +1259,7 @@ pub(crate) fn impl_self_ty_recover(
     impl_id: &ImplId,
 ) -> Binders<Ty> {
     let generics = generics(db.upcast(), (*impl_id).into());
-    Binders::new(generics.len(), TyKind::Error.intern(&Interner))
+    make_binders(&generics, TyKind::Error.intern(&Interner))
 }
 
 pub(crate) fn impl_trait_query(db: &dyn HirDatabase, impl_id: ImplId) -> Option<Binders<TraitRef>> {
@@ -1287,13 +1284,12 @@ pub(crate) fn return_type_impl_traits(
         .with_type_param_mode(TypeParamLoweringMode::Variable);
     let _ret = (&ctx_ret).lower_ty(&data.ret_type);
     let generics = generics(db.upcast(), def.into());
-    let num_binders = generics.len();
     let return_type_impl_traits =
         ReturnTypeImplTraits { impl_traits: ctx_ret.opaque_type_data.into_inner() };
     if return_type_impl_traits.impl_traits.is_empty() {
         None
     } else {
-        Some(Arc::new(Binders::new(num_binders, return_type_impl_traits)))
+        Some(Arc::new(make_binders(&generics, return_type_impl_traits)))
     }
 }
 
@@ -1303,3 +1299,7 @@ pub(crate) fn lower_to_chalk_mutability(m: hir_def::type_ref::Mutability) -> Mut
         hir_def::type_ref::Mutability::Mut => Mutability::Mut,
     }
 }
+
+fn make_binders<T>(generics: &Generics, value: T) -> Binders<T> {
+    crate::make_only_type_binders(generics.len(), value)
+}
diff --git a/crates/hir_ty/src/traits/chalk.rs b/crates/hir_ty/src/traits/chalk.rs
index 47867f77e9a..dff87ef70e4 100644
--- a/crates/hir_ty/src/traits/chalk.rs
+++ b/crates/hir_ty/src/traits/chalk.rs
@@ -184,7 +184,8 @@ impl<'a> chalk_solve::RustIrDatabase<Interner> for ChalkContext<'a> {
                     .db
                     .return_type_impl_traits(func)
                     .expect("impl trait id without impl traits");
-                let data = &datas.skip_binders().impl_traits[idx as usize];
+                let (datas, binders) = (*datas).as_ref().into_value_and_skipped_binders();
+                let data = &datas.impl_traits[idx as usize];
                 let bound = OpaqueTyDatumBound {
                     bounds: make_binders(
                         data.bounds
@@ -197,8 +198,7 @@ impl<'a> chalk_solve::RustIrDatabase<Interner> for ChalkContext<'a> {
                     ),
                     where_clauses: make_binders(vec![], 0),
                 };
-                let num_vars = datas.num_binders;
-                make_binders(bound, num_vars)
+                chalk_ir::Binders::new(binders, bound)
             }
             crate::ImplTraitId::AsyncBlockTypeImplTrait(..) => {
                 if let Some((future_trait, future_output)) = self
@@ -626,7 +626,7 @@ fn type_alias_associated_ty_value(
     let value = rust_ir::AssociatedTyValue {
         impl_id: impl_id.to_chalk(db),
         associated_ty_id: to_assoc_type_id(assoc_ty),
-        value: make_binders(value_bound, binders),
+        value: chalk_ir::Binders::new(binders, value_bound),
     };
     Arc::new(value)
 }
@@ -656,7 +656,7 @@ pub(crate) fn fn_def_datum_query(
     let datum = FnDefDatum {
         id: fn_def_id,
         sig: chalk_ir::FnSig { abi: (), safety: chalk_ir::Safety::Safe, variadic: sig.is_varargs },
-        binders: make_binders(bound, binders),
+        binders: chalk_ir::Binders::new(binders, bound),
     };
     Arc::new(datum)
 }
diff --git a/crates/hir_ty/src/traits/chalk/mapping.rs b/crates/hir_ty/src/traits/chalk/mapping.rs
index 72458f367fa..2c7407c7ca8 100644
--- a/crates/hir_ty/src/traits/chalk/mapping.rs
+++ b/crates/hir_ty/src/traits/chalk/mapping.rs
@@ -99,7 +99,7 @@ impl ToChalk for Ty {
                     bounds.interned().iter().cloned().map(|p| p.to_chalk(db)),
                 );
                 let bounded_ty = chalk_ir::DynTy {
-                    bounds: make_binders(where_clauses, binders),
+                    bounds: chalk_ir::Binders::new(binders, where_clauses),
                     lifetime: LifetimeData::Static.intern(&Interner),
                 };
                 chalk_ir::TyKind::Dyn(bounded_ty).intern(&Interner)
@@ -149,7 +149,7 @@ impl ToChalk for Ty {
                     .map(|c| from_chalk(db, c.clone()));
                 TyKind::Dyn(crate::DynTy {
                     bounds: crate::Binders::new(
-                        1,
+                        where_clauses.bounds.binders.clone(),
                         crate::QuantifiedWhereClauses::from_iter(&Interner, bounds),
                     ),
                 })
@@ -488,19 +488,12 @@ where
 
     fn to_chalk(self, db: &dyn HirDatabase) -> chalk_ir::Binders<T::Chalk> {
         let (value, binders) = self.into_value_and_skipped_binders();
-        chalk_ir::Binders::new(
-            chalk_ir::VariableKinds::from_iter(
-                &Interner,
-                std::iter::repeat(chalk_ir::VariableKind::Ty(chalk_ir::TyVariableKind::General))
-                    .take(binders),
-            ),
-            value.to_chalk(db),
-        )
+        chalk_ir::Binders::new(binders, 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))
+        crate::Binders::new(b, from_chalk(db, v))
     }
 }
 
@@ -552,7 +545,7 @@ 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(make_binders(rust_ir::InlineBound::TraitBound(trait_bound), binders))
+            Some(chalk_ir::Binders::new(binders, rust_ir::InlineBound::TraitBound(trait_bound)))
         }
         WhereClause::AliasEq(AliasEq { alias: AliasTy::Projection(projection_ty), ty }) => {
             if projection_ty.self_type_parameter(&Interner) != &self_ty_shifted_in {
@@ -569,7 +562,10 @@ 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(make_binders(rust_ir::InlineBound::AliasEqBound(alias_eq_bound), binders))
+            Some(chalk_ir::Binders::new(
+                binders,
+                rust_ir::InlineBound::AliasEqBound(alias_eq_bound),
+            ))
         }
         _ => None,
     }
diff --git a/crates/hir_ty/src/types.rs b/crates/hir_ty/src/types.rs
index 0e3dd511f9d..59678b45b41 100644
--- a/crates/hir_ty/src/types.rs
+++ b/crates/hir_ty/src/types.rs
@@ -12,7 +12,7 @@ use smallvec::SmallVec;
 
 use crate::{
     AssocTypeId, CanonicalVarKinds, ChalkTraitId, ClosureId, FnDefId, FnSig, ForeignDefId,
-    InferenceVar, Interner, OpaqueTyId, PlaceholderIndex,
+    InferenceVar, Interner, OpaqueTyId, PlaceholderIndex, VariableKinds,
 };
 
 #[derive(Clone, PartialEq, Eq, Debug, Hash)]
@@ -286,7 +286,7 @@ impl Substitution {
         Substitution(elements.into_iter().casted(interner).collect())
     }
 
-    // We can hopefully add this to Chalk
+    // Temporary helper functions, to be removed
     pub fn intern(interned: SmallVec<[GenericArg; 2]>) -> Substitution {
         Substitution(interned)
     }
@@ -296,46 +296,67 @@ impl Substitution {
     }
 }
 
-#[derive(Copy, Clone, PartialEq, Eq, Debug, Hash)]
+#[derive(Clone, PartialEq, Eq, Hash)]
 pub struct Binders<T> {
-    pub num_binders: usize,
+    /// The binders that quantify over the value.
+    pub binders: VariableKinds,
     value: T,
 }
 
 impl<T> Binders<T> {
-    pub fn new(num_binders: usize, value: T) -> Self {
-        Self { num_binders, value }
+    pub fn new(binders: VariableKinds, value: T) -> Self {
+        Self { binders, value }
     }
 
     pub fn empty(_interner: &Interner, value: T) -> Self {
-        Self { num_binders: 0, value }
+        crate::make_only_type_binders(0, value)
     }
 
     pub fn as_ref(&self) -> Binders<&T> {
-        Binders { num_binders: self.num_binders, value: &self.value }
+        Binders { binders: self.binders.clone(), value: &self.value }
     }
 
     pub fn map<U>(self, f: impl FnOnce(T) -> U) -> Binders<U> {
-        Binders { num_binders: self.num_binders, value: f(self.value) }
+        Binders { binders: self.binders, value: f(self.value) }
     }
 
     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)? })
+        Some(Binders { binders: self.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)
+    pub fn into_value_and_skipped_binders(self) -> (T, VariableKinds) {
+        (self.value, self.binders)
     }
 
+    /// Returns the number of binders.
+    pub fn len(&self, interner: &Interner) -> usize {
+        self.binders.len(interner)
+    }
+
+    // Temporary helper function, to be removed
     pub fn skip_binders_mut(&mut self) -> &mut T {
         &mut self.value
     }
 }
 
+impl<T: Clone> Binders<&T> {
+    pub fn cloned(&self) -> Binders<T> {
+        Binders::new(self.binders.clone(), self.value.clone())
+    }
+}
+
+impl<T: std::fmt::Debug> std::fmt::Debug for Binders<T> {
+    fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> Result<(), std::fmt::Error> {
+        let Binders { ref binders, ref value } = *self;
+        write!(fmt, "for{:?} ", binders.inner_debug(&Interner))?;
+        std::fmt::Debug::fmt(value, fmt)
+    }
+}
+
 /// A trait with type parameters. This includes the `Self`, so this represents a concrete type implementing the trait.
 #[derive(Clone, PartialEq, Eq, Debug, Hash)]
 pub struct TraitRef {