Deriving a trivial Eq class from a GADT

I thought GADTs were great until I tried putting any of the "expressions with GADTs" examples scattered around the internet to use.

Traditional ADTs kindly provide definitional equality in the guise of Eq for free. In GADTs for this code:

data Expr a where
  (:+:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr a
  (:-:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr a
  (:*:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr a
  (:/:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr a
  (:=:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr Bool
  (:<:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr Bool
  (:>:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr Bool
  (:>=:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr Bool
  (:<=:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr Bool
  (:<>:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr Bool
  EOr :: Expr Bool -> Expr Bool -> Expr Bool
  EAnd :: Expr Bool -> Expr Bool -> Expr Bool
  ENot :: Expr Bool -> Expr Bool
  ESymbol :: (Show a, Eq a) => String -> Expr a
  ELiteral :: (Show a, Eq a) => a -> Expr a
  EFunction :: (Show a, Eq a) => String -> [Expr a] -> Expr a
  deriving (Eq)

I get (very understandably):

    • Can't make a derived instance of ‘Eq (Expr a)’:
        Constructor ‘:+:’ has existentials or constraints in its type
        Constructor ‘:-:’ has existentials or constraints in its type
        Constructor ‘:*:’ has existentials or constraints in its type
        Constructor ‘:/:’ has existentials or constraints in its type
        Constructor ‘:=:’ has existentials or constraints in its type
        Constructor ‘:<:’ has existentials or constraints in its type
        Constructor ‘:>:’ has existentials or constraints in its type
        Constructor ‘:>=:’ has existentials or constraints in its type
        Constructor ‘:<=:’ has existentials or constraints in its type
        Constructor ‘:<>:’ has existentials or constraints in its type
        Constructor ‘EOr’ has existentials or constraints in its type
        Constructor ‘EAnd’ has existentials or constraints in its type
        Constructor ‘ENot’ has existentials or constraints in its type
        Constructor ‘ESymbol’ has existentials or constraints in its type
        Constructor ‘ELiteral’ has existentials or constraints in its type
        Constructor ‘EFunction’ has existentials or constraints in its type
        Possible fix: use a standalone deriving declaration instead
    • In the data declaration for ‘Expr’

Which would be understandable if I hadn't the Eq restriction for each constructor but now I have to write trivial equality rules for all these constructors.

I feel like there is better way to go about this than I have

Solution

Traditional deriving can't handle GADT constraints. Standalone deriving can, in principle:

{-# LANGUAGE GADTs, StandaloneDeriving #-}
data Expr a where
  (:+:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr a
  ...
deriving instance Eq (Expr a)

However, that doesn't help you because that Eq instance is just not possible. How will you compare

(1 :<: (2 :: Expr Int)) == (pi :<: (sqrt 2 :: Expr Double))

It's just not possible; the GADT constraint

  (:<:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr Bool

only enforces that both values compared in that Expr have the same type and are Eq, but it doesn't tell you anything about the types of different expressions.