Generate type in runtime using existential and GADTs.

type.hs

{-# LANGUAGE DataKinds, GADTs, TypeOperators, KindSignatures #-}

-- http://www.reddit.com/r/haskell/comments/1q93r2/haskell_the_language_most_likely_to_change_the/cdberll

data Nat = Z | S Nat deriving (Show)

data SNat n where
  Zero :: SNat Z
  Succ :: SNat n -> SNat (S n)

{-- We can't do this, because return type differs.
fromInt :: Integer -> SNat n
fromInt 0 = Zero                      -- SNat Z
fromInt n = Succ $ fromInt (n - 1)    -- SNat (S n)
--}

{-- Wrap SNat in  existential type --}
data SomeNat where
  SomeNat :: SNat n -> SomeNat

nextSN :: SomeNat -> SomeNat
nextSN (SomeNat n) = SomeNat (Succ n)

natify :: Integer -> SomeNat
natify 0 = SomeNat Zero
natify x | x >= 0 = nextSN . natify $ x - 1

-- Easier way to inspect type

toInt :: SNat n -> Int
toInt Zero = 0
toInt (Succ n) = 1 + toInt n

instance Show (SNat n) where
    show Zero = "SNat " ++ show (toInt Zero)
    show n@(Succ _) = "SNat (" ++  show (toInt n) ++ ")"

instance Show SomeNat where
    show (SomeNat n) = "SomeNat (" ++ show n ++ ")"

main = do
    n <- readLn
    print (natify n)

    SomeNat n' <- return . natify $ n
    print n'

    case natify n of
      SomeNat n' -> print n'

    -- My brain just exploded
    -- let SomeNat n' = natify n
    -- print n'