+module Data.HList.Number
+ ( HNat
+
+ , HZero
+ , hZero
+
+ , HSucc
+ , hSucc
+ , hPred
+
+ , hNatLiteralT
+ , hNatLiteralE
+ , hNatLiteralP
+ )
+ where
+
+import Language.Haskell.TH
+
+
+-- HNat
+class HNat n
+
+-- HZero
+data HZero = HZero deriving Show
+
+instance HNat HZero
+
+hZero :: HZero
+hZero = HZero
+
+-- HSucc
+data HSucc n = HSucc n deriving Show
+
+instance HNat n => HNat (HSucc n)
+
+hSucc :: HNat n => n -> HSucc n
+hSucc = HSucc
+
+hPred :: HNat n => HSucc n -> n
+hPred (HSucc n) = n
+
+-- TH
+hNatLiteralT :: Integral n => n -> Q Type
+hNatLiteralT n
+ | n == 0 = conT (mkName "HZero")
+ | otherwise = appT (conT (mkName "HSucc"))
+ (hNatLiteralT (n - 1))
+
+hNatLiteralE :: Integral n => n -> Q Exp
+hNatLiteralE n
+ | n == 0 = varE (mkName "hZero")
+ | otherwise = appE (varE (mkName "hSucc"))
+ (hNatLiteralE (n - 1))
+
+hNatLiteralP :: Integral n => n -> Q Pat
+hNatLiteralP n
+ | n == 0 = varP (mkName "HZero")
+ | otherwise = conP (mkName "HSucc") [hNatLiteralP n]