derive_abstract breaks alpha equivalence

enolan commented 8 years ago

aeq always returns False when your term uses instances created with derive_abstract. This is extremely surprising behavior if you're not thinking about how the library needs to work internally. I guess it's not possible to do the right thing without access to the underlying representation, but derive_abstract should at least have a big warning.

{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses,
             TemplateHaskell, UndecidableInstances #-}
module Lib
     where

import Unbound.LocallyNameless

data Term = Word Word
  deriving Show

$(derive_abstract [''Word])
$(derive [''Term])
instance Alpha Word
instance Alpha Term

t1 :: Term
t1 = Word 5

wrong :: Bool
wrong = t1 `aeq` t1 -- False

sweirich commented 8 years ago

Thanks for the report. I've just pushed an update that calls 'error' on your code instead of returning False. Is this what you were expecting?

Either way, though, it would be good to document the behavior, but I'm not sure what the best place to do so would be. Is there a better place than https://github.com/sweirich/replib/blob/master/Unbound/examples/Abstract.hs?

enolan commented 8 years ago

Having it call error is reasonable. Honestly, I was expecting it to "Just Work" but letting me know it won't and how to fix it as soon as I make the mistake is the next best thing.

The Haddock for Alpha is probably the best place. I'm unlikely to look at the example unless I already know it's there, whereas I'll always be looking at the Haddock.

Thanks for the fast response!

sweirich commented 8 years ago

Ok, I've updated the Haddocks for Alpha to mention this issue. Closing now.

Thanks again!

sweirich / replib

derive_abstract breaks alpha equivalence #38