[Haskell-cafe] Unbound: rebind and unrebind

[Eric Dobson]

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 at 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?