title: Equality for GADTs which erase type parameter
body: <p>I cannot implement an instance of <code>Eq</code> for the following typesafe DSL for expressions implemented with GADTs.</p>
  <pre><code>data Expr a where
    Num :: Int -&gt; Expr Int
    Bool :: Bool -&gt; Expr Bool
    Plus :: Expr Int -&gt; Expr Int -&gt; Expr Int
    If :: Expr Bool -&gt; Expr a -&gt; Expr a -&gt; Expr a
    Equal :: Eq a =&gt; Expr a -&gt; Expr a -&gt; Expr Bool
  </code></pre>
  <p>Expressions can be either of type <code>Bool</code> or <code>Int</code>. There are constructors for literals <code>Bool</code> and <code>Num</code> which have the corresponding types. Only <code>Int</code> expressions can be added up (constructor <code>Plus</code>). The condition in the <code>If</code> expression should have type <code>Bool</code> while both branches should have the same type. There is also an equality expression <code>Equal</code> whose operands should have the same type, and the type of the equality expression is <code>Bool</code>.</p>
  <p>I have no problems implementing the interpreter <code>eval</code> for this DSL. It compiles and works like a charm:</p>
  <pre><code>eval :: Expr a -&gt; a
  eval (Num x) = x
  eval (Bool x) = x
  eval (Plus x y) = eval x + eval y
  eval (If c t e) = if eval c then eval t else eval e
  eval (Equal x y) = eval x == eval y
  </code></pre>
  <p>However, I struggle to implement an instance of <code>Eq</code> for the DSL. I tried the simple syntactic equality:</p>
  <pre><code>instance Eq a =&gt; Eq (Expr a) where
    Num x == Num y = x == y
    Bool x == Bool y = x == y
    Plus x y == Plus x' y' = x == x' &amp;&amp; y == y'
    If c t e == If c' t' e' = c == c' &amp;&amp; t == t' &amp;&amp; e == e'
    Equal x y == Equal x' y' = x == x' &amp;&amp; y == y'
    _ == _ = False
  </code></pre>
  <p>It does not typecheck (with <code>ghc 8.6.5</code>), the error is the following:</p>
  <pre><code>[1 of 1] Compiling Main             ( Main.hs, Main.o )
  
  Main.hs:17:35: error:
      • Could not deduce: a2 ~ a1
        from the context: (a ~ Bool, Eq a1)
          bound by a pattern with constructor:
                     Equal :: forall a. Eq a =&gt; Expr a -&gt; Expr a -&gt; Expr Bool,
                   in an equation for ‘==’
          at Main.hs:17:3-11
        ‘a2’ is a rigid type variable bound by
          a pattern with constructor:
            Equal :: forall a. Eq a =&gt; Expr a -&gt; Expr a -&gt; Expr Bool,
          in an equation for ‘==’
          at Main.hs:17:16-26
        ‘a1’ is a rigid type variable bound by
          a pattern with constructor:
            Equal :: forall a. Eq a =&gt; Expr a -&gt; Expr a -&gt; Expr Bool,
          in an equation for ‘==’
          at Main.hs:17:3-11
        Expected type: Expr a1
          Actual type: Expr a2
      • In the second argument of ‘(==)’, namely ‘x'’
        In the first argument of ‘(&amp;&amp;)’, namely ‘x == x'’
        In the expression: x == x' &amp;&amp; y == y'
      • Relevant bindings include
          y' :: Expr a2 (bound at Main.hs:17:25)
          x' :: Expr a2 (bound at Main.hs:17:22)
          y :: Expr a1 (bound at Main.hs:17:11)
          x :: Expr a1 (bound at Main.hs:17:9)
     |
  17 |   Equal x y == Equal x' y' = x == x' &amp;&amp; y == y'
     |  
  </code></pre>
  <p>I believe the reason is that the constructor <code>Equal</code> &quot;forgets&quot; the value of the type parameter <code>a</code> of its subexpressions and there is no way for the typechecker to ensure subexpressions <code>x</code> and <code>y</code> both have the same type <code>Expr a</code>.</p>
  <p>I tried adding one more type parameter to <code>Expr a</code> to keep track of the type of subexpressions:</p>
  <pre><code>data Expr a b where
    Num :: Int -&gt; Expr Int b
    Bool :: Bool -&gt; Expr Bool b
    Plus :: Expr Int b -&gt; Expr Int b -&gt; Expr Int b
    If :: Expr Bool b -&gt; Expr a b -&gt; Expr a b -&gt; Expr a b
    Equal :: Eq a =&gt; Expr a a -&gt; Expr a a -&gt; Expr Bool a
  
  instance Eq a =&gt; Eq (Expr a b) where
    -- same implementation
  
  eval :: Expr a b -&gt; a
    -- same implementation
  </code></pre>
  <p>This approach does not seem scalable to me, once more constructors with subexpressions of different types are added.</p>
  <p>All this makes me think that I do use GADTs incorrectly to implement this kind of DSL. Is there a way to implement <code>Eq</code> for this type? If not, what is the idiomatic way to express this kind of type constraint on the expressions?</p>
  <p>Complete code:</p>
  <pre><code>{-# LANGUAGE GADTs #-}
   
  module Main where
  
  data Expr a where
    Num :: Int -&gt; Expr Int
    Bool :: Bool -&gt; Expr Bool
    Plus :: Expr Int -&gt; Expr Int -&gt; Expr Int
    If :: Expr Bool -&gt; Expr a -&gt; Expr a -&gt; Expr a
    Equal :: Eq a =&gt; Expr a -&gt; Expr a -&gt; Expr Bool
  
  instance Eq a =&gt; Eq (Expr a) where
    Num x == Num y = x == y
    Bool x == Bool y = x == y
    Plus x y == Plus x' y' = x == x' &amp;&amp; y == y'
    If c t e == If c' t' e' = c == c' &amp;&amp; t == t' &amp;&amp; e == e'
    Equal x y == Equal x' y' = x == x' &amp;&amp; y == y'
    _ == _ = False
  
  eval :: Expr a -&gt; a
  eval (Num x) = x
  eval (Bool x) = x
  eval (Plus x y) = eval x + eval y
  eval (If c t e) = if eval c then eval t else eval e
  eval (Equal x y) = eval x == eval y
  
  main :: IO ()
  main = do
    let expr1 = If (Equal (Num 13) (Num 42)) (Bool True) (Bool False)
    let expr2 = If (Equal (Num 13) (Num 42)) (Num 42) (Num 777)
    print (eval expr1)
    print (eval expr2)
    print (expr1 == expr1)
  </code></pre>