diff --git a/Data/Nat.hs b/Data/Nat.hs
--- a/Data/Nat.hs
+++ b/Data/Nat.hs
@@ -1,7 +1,8 @@
 {-# LANGUAGE
   UndecidableInstances, ScopedTypeVariables, DataKinds,
   FlexibleInstances, GADTs, TypeFamilies, TemplateHaskell,
-  InstanceSigs, TypeOperators, PolyKinds #-}
+  InstanceSigs, TypeOperators, PolyKinds, StandaloneDeriving,
+  FlexibleContexts, AllowAmbiguousTypes #-}
 
 module Data.Nat (
     Nat(..)
@@ -21,7 +22,8 @@
   , SSym1(..)
   , ZSym0(..)
   , Lit
-  , SLit ) where
+  , SLit
+  , sLit) where
 
 import Data.Singletons.TH
 import Data.Singletons.Prelude
@@ -46,9 +48,17 @@
 
   natAbs :: Nat -> Nat
   natAbs n = n
-  |])                                
+  |])
 
-instance PNum ('KProxy :: KProxy Nat) where
+deriving instance Show (SNat n)
+
+instance Eq (SNat n) where
+  (==) _ _ = True
+
+instance Ord (SNat n) where
+  compare _ _ = EQ
+
+instance PNum ('Proxy :: Proxy Nat) where
   type a :+ b = NatPlus a b
   type a :- b = NatMinus a b
   type a :* b = NatMul a b
@@ -56,7 +66,7 @@
   type Signum (a :: Nat) = Error "Data.Nat: signum not implemented"
   type FromInteger (a :: Lit.Nat) = Lit a
 
-instance SNum ('KProxy :: KProxy Nat) where  
+instance SNum Nat where  
   (%:+) = sNatPlus
   (%:*) = sNatMul
   (%:-) = sNatMinus
@@ -69,7 +79,7 @@
 
 {-| Converts a runtime 'Integer' to an existentially wrapped 'Nat'. Returns 'Nothing' if
 the argument is negative -}
-someNatVal :: Integer -> Maybe (SomeSing (KindOf Z))
+someNatVal :: Integer -> Maybe (SomeSing Nat)
 someNatVal n = case Lit.someNatVal n of
   Just (Lit.SomeNat (pn :: Proxy n)) -> Just (SomeSing (sFromInteger (sing :: Sing n)))
   Nothing -> Nothing
@@ -86,4 +96,15 @@
   Lit n = S (Lit (n Lit.- 1))
 
 type SLit n = Sing (Lit n)
+
+{-| Shorthand for 'SNat' literals using `TypeApplications`.
+
+>>> :set -XTypeApplications
+>>> sLit @5
+SS (SS (SS (SS (SS SZ))))
+
+-}
+
+sLit :: forall (n :: Lit.Nat). SingI (Lit n) => Sing (Lit n)
+sLit = sing
 
diff --git a/singleton-nats.cabal b/singleton-nats.cabal
--- a/singleton-nats.cabal
+++ b/singleton-nats.cabal
@@ -1,31 +1,31 @@
-
-name:                singleton-nats
-version:             0.4.0.1
-synopsis:            Unary natural numbers relying on the singletons infrastructure.
-description:         Unary natural number relying on the <https://hackage.haskell.org/package/singletons singletons> infrastructure. More information about the general usage of singletons can be found on the <https://github.com/goldfirere/singletons singletons github> page.                           
-category:            Data, Dependent Types
-homepage:            https://github.com/AndrasKovacs/singleton-nats
-bug-reports:         https://github.com/AndrasKovacs/singleton-nats/issues
-license:             BSD3
-license-file:        LICENSE
-author:              András Kovács
-maintainer:          puttamalac@gmail.com
-copyright:           2015 András Kovács
-
-build-type:          Simple
-cabal-version:       >=1.10
-tested-with:         GHC == 7.10.2
-
-source-repository head
-  type: git
-  location: https://github.com/AndrasKovacs/singleton-nats.git
-
-library
-  exposed-modules:
-    Data.Nat
-
-  build-depends:
-    base >=4.8.1.0 && <4.9,
-    singletons >= 2.0.1
-
+
+name:                singleton-nats
+version:             0.4.0.2
+synopsis:            Unary natural numbers relying on the singletons infrastructure.
+description:         Unary natural number relying on the <https://hackage.haskell.org/package/singletons singletons> infrastructure. More information about the general usage of singletons can be found on the <https://github.com/goldfirere/singletons singletons github> page.                           
+category:            Data, Dependent Types
+homepage:            https://github.com/AndrasKovacs/singleton-nats
+bug-reports:         https://github.com/AndrasKovacs/singleton-nats/issues
+license:             BSD3
+license-file:        LICENSE
+author:              András Kovács
+maintainer:          puttamalac@gmail.com
+copyright:           2015 András Kovács
+
+build-type:          Simple
+cabal-version:       >=1.10
+tested-with:         GHC == 8.0.1
+
+source-repository head
+  type: git
+  location: https://github.com/AndrasKovacs/singleton-nats.git
+
+library
+  exposed-modules:
+    Data.Nat
+
+  build-depends:
+    base >=4.8.1.0 && <5,
+    singletons >= 2.2 && < 2.3
+
   default-language:    Haskell2010