Shows how to implement an `instance Eq` for a GADT wrapped in an existential type, in Haskell.

gadt-equality.hs

-- Shows how to implement an `instance Eq` for a GADT wrapped in an existential type.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeOperators #-}

import Data.Type.Equality

-- | A GADT. The example would also work if it had more than 1 type parameter.
data MyGadt a where
  G1 :: Int -> MyGadt Int
  G2 :: Bool -> MyGadt String

deriving instance Show (MyGadt a)
deriving instance Eq (MyGadt a)

-- | An existantial around the GADT.
data SomeMyGadt = forall a . SomeMyGadt (MyGadt a)

deriving instance Show SomeMyGadt


-- deriving instance Eq SomeMyGadt -- Doesn't work, can't work.


-- One way of doing it (direct way, cannot be reused for other instances):
{-
instance Eq SomeMyGadt where
  SomeMyGadt a@G1{} == SomeMyGadt b@G1{} = a == b
  SomeMyGadt a@G2{} == SomeMyGadt b@G2{} = a == b
  _                 == _                 = False
-}


-- A more general way of doing it is below, which can be reused:


-- | Tells whether two `MyGadt`s have are of the same type.
sameGadtType
  :: MyGadt a1
  -> MyGadt a2
  -> Maybe (MyGadt a1 :~: MyGadt a2)
sameGadtType a b = case a of

  -- Need to list all GADT constructors explicitly here.

  G1{} -> case b of
    G1{} -> Just Refl
    _ -> Nothing

  G2{} -> case b of
    G2{} -> Just Refl
    _ -> Nothing

  -- We take care to not have a wildcard `_ == _ = False`
  -- in the outer `case` to make sure to get an exhaustiveness
  -- check warning if somebody adds a new constructor to the GADT
  -- but forgets to add it to `sameGadtType`.


-- Then we can use `sameGadtType` to implement instances concisely:

instance Eq SomeMyGadt where
  SomeMyGadt a == SomeMyGadt b = case sameGadtType a b of
    Just Refl -> a == b  -- a == b typechecks here because `Refl` proves that their types are equal
    Nothing -> False     -- Type is different, so values can't be equal.


main :: IO ()
main = do
  print $ SomeMyGadt (G1 1) == SomeMyGadt (G1 1)
  print $ SomeMyGadt (G1 1) == SomeMyGadt (G2 False)

Regarding GADTs involving more than one parameter, I simply can't get it to work. Could you show how you would do it?

Also, how would you perform Eq instances with GADTs that have parameters in their type signature? i.e. G1 :: a -> MyGadt a