-- 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

Check the depth of the structure:

*Main> depth T0
0
*Main> depth (Tm T0)
1
*Main> depth (Tm (Tm (Tm (Tm T0))))
4

The function twoOfSameDepth expects both parameters to be of the same depth. If not, you get a type error.

*Main> :t twoOfSameDepth T0 T0
twoOfSameDepth T0 T0 :: Int
*Main> :t twoOfSameDepth T0 (Tm T0)

:1:20:
    Couldn't match expected type `'Z' with actual type `S n0'
    Expected type: T 'Z
      Actual type: T (S n0)
    In the return type of a call of `Tm'
    In the second argument of `twoOfSameDepth', namely `(Tm T0)'

The function secondIsPlusOne expects the second parameter to be of depth one more than the first parameter:

*Main> :t secondIsPlusOne T0 (Tm T0)
secondIsPlusOne T0 (Tm T0) :: Bool
*Main> :t secondIsPlusOne T0 (Tm (Tm T0))

:1:25:
    Couldn't match expected type `'Z' with actual type `S n0'
    Expected type: T 'Z
      Actual type: T (S n0)
    In the return type of a call of `Tm'
    In the first argument of `Tm', namely `(Tm T0)'
*Main>

In Matt’s LambdaJam talk/jam you can see how this idea can be used to help with implementing a b-tree data structure.