I am working at reimplementing the library Unbound to understand how it works. One issue I have come up with is that an equation that I thought held true doesn't. The equation is: Forall e::Rebind a b, e `aeq` (uncurry rebind . unrebind $ e) => True. That is that spliting the binding of a rebind and then adding it back should be the identity. The issue is that Rebind does not freshen its pattern variables on unrebind, because it assumes that a higher level unbind already did that if required. But I believe this is not sufficient as there is not necesarily a higher level Bind to be ubound as shown by this program: {-# LANGUAGE TemplateHaskell, UndecidableInstances, FlexibleInstances, MultiParamTypeClasses #-} module Main where import Unbound.LocallyNameless data Exp = Var (Name Exp) deriving Show $(derive [''Exp]) instance Alpha Exp instance Subst Exp Exp where isvar (Var x) = Just (SubstName x) x :: Name Exp x = string2Name "x" y :: Name Exp y = string2Name "y" rebindPass :: Alpha a => Rebind Exp a -> Rebind Exp a rebindPass = (uncurry rebind . unrebind) main :: IO () main = do let rebound = (rebind (Var y) (Embed (Var x))) print $ rebound let substed = subst x (Var y) rebound print $ substed print $ unrebind substed print $ rebindPass substed Which outputs: <<Var y>> {Var x} <<Var y>> {Var y} (Var y,{Var y}) <<Var y>> {Var 0@0} If the equation holds true then the second and fourth lines should be identical but they are not. Can someone explain why this is the correct behavior or if the implementation is incorrect?