I just extended the original example to support safe polymorphic Eq operation. It seems there’s this implicit transition:

1
ADT -> Phantom types -> GADT

Complete code example:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}

module GADT where

import Data.Function (on)

data Expr a where
  I   :: Int  -> Expr Int
  B   :: Bool -> Expr Bool
  Bop :: Bop t a -> Expr t -> Expr t -> Expr a

data Bop :: * -> * -> * where
  Add :: Bop Int Int
  Mul :: Bop Int Int
  Eq :: Eq a => Bop a Bool

evalBop :: Bop t a -> Expr t -> Expr t -> a
evalBop Add x y = ((+) `on` eval) x y
evalBop Mul x y = ((*) `on` eval) x y
evalBop Eq x y = ((==) `on` eval) x y

eval :: Expr a -> a
eval (I n) = n
eval (B b) = b
eval (Bop op x y) = evalBop op x y

x = I 3
y = I 2
r = [Bop Add x y, Bop Mul x y]

main = do
  mapM_ (print . eval) r
  print . eval $ Bop Eq x y
  print . eval $ Bop Eq (B True) (B False)

§Reference