Haskellの依存型ムズカシネ

Exp.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE FunctionalDependencies #-}

-- 0/1/二項演算op2 だけしか無い式の構文で，
-- 0が高々1回しか表れないようなものを表現し，
-- Eqのインスタンスにしたい．

class ContainsZeroAtMostOne a where

data WithZero
instance ContainsZeroAtMostOne WithZero

data WithoutZero
instance ContainsZeroAtMostOne WithoutZero

class ExistZero2 a b c | a b -> c
instance ExistZero2 WithoutZero WithoutZero WithoutZero
instance ExistZero2 WithoutZero WithZero    WithZero
instance ExistZero2 WithZero    WithoutZero WithZero

data Exp a where
    ExpZero :: Exp WithZero
    ExpOne :: Exp WithoutZero
    ExpOp2 :: ( ContainsZeroAtMostOne b
              , ContainsZeroAtMostOne c
              , ExistZero2 b c d ) =>
              Exp b -> Exp c -> Exp d

instance ContainsZeroAtMostOne a => Eq (Exp a) where
    ExpZero == ExpZero = True
    ExpOne == ExpOne = True
    ExpOp2 a b == ExpOp2 c d = a == c && b == d -- ここどうにかなるか？
    _ == _ = False

instance ContainsZeroAtMostOne a => Show (Exp a) where
    show ExpZero = "0"
    show ExpOne = "1"
    show (ExpOp2 a b) = "(op2 "++shows a" "++shows b")"

e1 :: Exp WithZero
e1 = ExpOp2 ExpZero ExpOne

e2 :: Exp WithoutZero
e2 = ExpOp2 ExpOne ExpOne

-- 正しく型エラーになる
-- e3 = ExpOp2 ExpZero ExpZero

main :: IO ()
main = print (e1 == e1)