{-# LANGUAGE GADTs, KindSignatures #-}
{-# OPTIONS -Wall #-}
module GADTNonExhaustive where

data Expr :: * -> * where
  Const :: Const a -> Expr a
  Pair  :: Expr a -> Expr b -> Expr (a, b)
  Fst   :: Expr (a, b) -> Expr a
  Snd   :: Expr (a, b) -> Expr b

data Const :: * -> * where
  ConstInt :: Int -> Const Int
  ConstFloat :: Float -> Const Float

eval :: Expr a -> a
eval expr =
  case expr of
    Const c -> evalConst c
    Pair l r -> evalPair l r
    Fst e -> evalFst e
    Snd e -> evalSnd e

evalConst :: Const a -> a
evalConst c =
  case c of
    ConstInt i -> i
    ConstFloat f -> f

evalPair :: Expr a -> Expr b -> (a, b)
evalPair l r = (eval l, eval r)

evalFst :: Expr (a, b) -> a
evalFst expr =
  case expr of
    -- The `Const' case is in fact impossible, as any Const
    -- constructor matched against is type-incorrect.  However, GHC
    -- warns about non-exhaustive pattern matches if the following
    -- line is commented.  This behavior is observed with 6.10.4,
    -- 6.12.1, 6.12.2, and 6.12.3.  I have not tested other versions.
    Const _c -> error "Impossible!"
    Pair l _r -> eval l
    Fst e -> fst $ evalFst e
    Snd e -> fst $ evalSnd e

evalSnd :: Expr (a, b) -> b
evalSnd expr =
  case expr of
    -- Same deal here as in evalFst.
    Const _c -> error "Impossible!"
    Pair _l r -> eval r
    Fst e -> snd $ evalFst e
    Snd e -> snd $ evalSnd e