Fun with TypeLits

{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators
  , ExistentialQuantification #-}
import GHC.TypeLits
import Data.Proxy

data Tree :: * -> Nat -> * where
  Leaf :: a -> Tree a 0
  Node :: Tree a n -> Tree a n -> Tree a (n + 1)

instance Show a => Show (Tree a b) where
  show t = case t of
    Leaf a -> "Leaf " ++ show a
    Node l r -> "(" ++ show l ++ ") (" ++ show r ++ ")"

instance Show a => Show (SomeTree a) where
  show (SomeTree t) = "SomeTree " ++ show t 

append :: Tree a n -> Tree a n -> Tree a (n+1)
append = Node

depth :: KnownNat n => Tree a n -> Int
depth = fromEnum . go Proxy
  where
  go :: KnownNat n => Proxy n -> Tree a n -> Integer
  go p _ = natVal p

-- Either these three lines, or the remaining lines must be commented out;
-- making both 'depth' and 'dynamically' work in the same program seems tricky.

-- data SomeTree a = forall depth. KnownNat depth => SomeTree (Tree a depth)
-- depth' :: SomeTree a -> Int
-- depth' (SomeTree t) = depth t

data SomeTree a = forall depth. SomeTree (Tree a depth)
withDepth :: Int -> a -> SomeTree a
withDepth 0 n = SomeTree $ Leaf n
withDepth x n = case withDepth (x-1) n of
            SomeTree x -> SomeTree $ Node x x

dynamically :: IO (SomeTree String)
dynamically = do
  depth <- readLn
  return $ withDepth depth "hi"