Challenge 2: Extending the Expr a GADT With If and eval — Possible Solution
====================================================================

Main.hs:

{-# LANGUAGE GADTs #-}

data Expr a where
  IntLit  :: Int -> Expr Int
  BoolLit :: Bool -> Expr Bool
  Add     :: Expr Int -> Expr Int -> Expr Int
  If      :: Expr Bool -> Expr a -> Expr a -> Expr a

eval :: Expr a -> a
eval (IntLit n)      = n
eval (BoolLit b)      = b
eval (Add e1 e2)      = eval e1 + eval e2
eval (If cond t f)    = if eval cond then eval t else eval f

main :: IO ()
main = do
  print (eval (Add (IntLit 3) (IntLit 4)))
  print (eval (If (BoolLit True) (IntLit 10) (IntLit 20)))

Output:

    7
    10

Explanation:
eval's own type, Expr a -> a, is only possible BECAUSE Expr is a GADT
-- each pattern match can return a genuinely different concrete type
(Int for IntLit/Add, Bool for BoolLit, whatever `a` the branches of
If share), and the compiler tracks exactly which type applies at each
point using the specific return type each constructor declared. If's
own constructor requires its condition to specifically be Expr Bool
and its two branches to both be the SAME Expr a -- attempting
`If (IntLit 1) (IntLit 2) (IntLit 3)` (a non-Bool condition) would be
rejected at compile time, the same type-safety the chapter's own
Add (IntLit 5) (BoolLit True) example demonstrates.

WHY THIS WORKS AS AN ANSWER
------------------------------
This extends the chapter's own Expr a GADT with a new constructor
following the same per-constructor-return-type pattern, and writes a
real, correctly-typed eval function that only compiles because of the
GADT's own precise typing, tested against two genuinely different
expression shapes.