Binders in dependently-typed programming are especially important due to types such as Σ : (a : Type) -> (a -> Type) -> Type and Π : (a : Type) -> (a -> Type) -> Type. This work-in-progress in the Idris compiler aims to bring the ergonomic benefits of custom binders brought by arbitrary syntax extension, while keeping the grammar fixed in order to provide bespoke quality error messages.