Fiddling with GADTs during http://matthew.brecknell.net/post/btree-gadt/ at Lambda Jam 2013.

gadt_lambdajam_2013.hs

-- Easiest way to run this with ghci:
--
-- ghci -XDataKinds -XGADTs -XEmptyDataDecls -XKindSignatures -XScopedTypeVariables -XTemplateHaskell

-- Natural numbers, e.g.
-- 0 == Z
-- 1 == S Z
-- 2 == S (S Z)
-- 3 == S (S (S Z))
-- etc

data Nat = Z | S Nat

-- My GADT with two constructors. One would normally
-- write
-- 
-- data T n = T0 ... | Tm ...
--
-- but here we want to specify the *types* of the constructors.

data T n where
    T0 :: T Z
    Tm :: T n -> T (S n)

-- Calculate the 'n' component, recursing on the definition of Tm.
depth :: T n -> Int
depth T0 = 0
depth (Tm a) = 1 + (depth a)

-- Takes two parameters of type T n, so they must be
-- of the same depth.
twoOfSameDepth :: T n -> T n -> Int
twoOfSameDepth x _ = depth x

-- Takes two parameters T n and T m, and enforces
-- that S n ~ m, in other words the second parameter
-- is one plus the first parameter.
secondIsPlusOne :: forall n m. (S n ~ m) => T n -> T m -> Bool
secondIsPlusOne _ _ = True