diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,11 @@
+# 0.4.1 [2018.05.02]
+* Add a `Num Nat` instance.
+* Implement `signum` in the `PNum`/`SNum` instances for `Nat`.
+* Define defunctionalization symbols for `Lit`.
+* Define `someNatVal`.
+
+# 0.4.0.4 [2018.01.09]
+* Allow `singletons-2.4`.
+
+# 0.4.0.3 [2017.11.03]
+* Allow `singletons-2.3`.
diff --git a/Data/Nat.hs b/Data/Nat.hs
--- a/Data/Nat.hs
+++ b/Data/Nat.hs
@@ -11,24 +11,28 @@
   , NatMul
   , NatMinus
   , NatAbs
+  , NatSignum
   , natPlus
   , natMul
   , natMinus
   , natAbs
+  , natSignum
+  , someNatVal
   , SNat
   , Data.Singletons.Prelude.Sing(SS, SZ)
   , Data.Singletons.Prelude.PNum
   , Data.Singletons.Prelude.SNum
   , SSym0(..)
-  , SSym1(..)
-  , ZSym0(..)
+  , SSym1
+  , ZSym0
   , Lit
+  , LitSym0(..)
+  , LitSym1
   , SLit
   , sLit) where
 
 import Data.Singletons.TH
 import Data.Singletons.Prelude
-import Unsafe.Coerce
 import qualified GHC.TypeLits as Lit
 
 $(singletons [d|
@@ -39,16 +43,31 @@
   natPlus (S a) b = S (natPlus a b)
 
   natMul :: Nat -> Nat -> Nat
-  natMul Z     b = Z
+  natMul Z     _ = Z
   natMul (S a) b = natPlus b (natMul a b)
 
   natMinus :: Nat -> Nat -> Nat
-  natMinus Z     b     = Z
+  natMinus Z     _     = Z
   natMinus (S a) (S b) = natMinus a b
   natMinus a     Z     = a
 
   natAbs :: Nat -> Nat
   natAbs n = n
+
+  natSignum :: Nat -> Nat
+  natSignum Z     = Z
+  natSignum (S _) = S Z
+
+  instance Num Nat where
+    (+) = natPlus
+    (-) = natMinus
+    (*) = natMul
+    abs = natAbs
+    signum = natSignum
+    fromInteger n
+      = if n == 0
+           then Z
+           else S (fromInteger (n - 1))
   |])
 
 #if !(MIN_VERSION_singletons(2,4,0))
@@ -61,58 +80,11 @@
 instance Ord (SNat n) where
   compare _ _ = EQ
 
-#if MIN_VERSION_singletons(2,3,0)
-instance PNum Nat where
-#else
-instance PNum ('Proxy :: Proxy Nat) where
-#endif
-#if MIN_VERSION_singletons(2,4,0)
-  type a + b = NatPlus a b
-  type a - b = NatMinus a b
-  type a * b = NatMul a b
-#else
-  type a :+ b = NatPlus a b
-  type a :- b = NatMinus a b
-  type a :* b = NatMul a b
-#endif
-  type Abs a = NatAbs a
-  type Signum (a :: Nat) = Error "Data.Nat: signum not implemented"
-  type FromInteger (a :: Lit.Nat) = Lit a
-
-instance SNum Nat where
-#if MIN_VERSION_singletons(2,4,0)
-  (%+) = sNatPlus
-  (%*) = sNatMul
-  (%-) = sNatMinus
-#else
-  (%:+) = sNatPlus
-  (%:*) = sNatMul
-  (%:-) = sNatMinus
-#endif
-  sAbs  = sNatAbs
-  sSignum = case toSing "Data.Nat: signum not implemented" of
-    SomeSing s -> sError s
-  sFromInteger n = case n 
-#if MIN_VERSION_singletons(2,4,0)
-                          %==
-#else
-                          %:==
-#endif
-                               (sing :: Sing 0) of
-    STrue  -> unsafeCoerce SZ
-    SFalse -> unsafeCoerce (SS (sFromInteger (n
-#if MIN_VERSION_singletons(2,4,0)
-                                                %-
-#else
-                                                %:-
-#endif
-                                                    (sing :: Sing 1))))
-
 {-| Converts a runtime 'Integer' to an existentially wrapped 'Nat'. Returns 'Nothing' if
 the argument is negative -}
 someNatVal :: Integer -> Maybe (SomeSing Nat)
 someNatVal n = case Lit.someNatVal n of
-  Just (Lit.SomeNat (pn :: Proxy n)) -> Just (SomeSing (sFromInteger (sing :: Sing n)))
+  Just (Lit.SomeNat (_ :: Proxy n)) -> Just (SomeSing (sFromInteger (sing :: Sing n)))
   Nothing -> Nothing
 
 {-| Provides a shorthand for 'Nat'-s using "GHC.TypeLits", for example:
@@ -125,6 +97,7 @@
 type family Lit n where
   Lit 0 = Z
   Lit n = S (Lit (n Lit.- 1))
+$(genDefunSymbols [''Lit])
 
 type SLit n = Sing (Lit n)
 
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,5 @@
+# singleton-nats
+
+[![Hackage](https://img.shields.io/hackage/v/singleton-nats.svg)](https://hackage.haskell.org/package/singleton-nats) [![Build Status](https://secure.travis-ci.org/AndrasKovacs/singleton-nats.svg)](http://travis-ci.org/AndrasKovacs/singleton-nats)
+
+Unary natural numbers relying on the singletons infrastructure.
diff --git a/singleton-nats.cabal b/singleton-nats.cabal
--- a/singleton-nats.cabal
+++ b/singleton-nats.cabal
@@ -1,6 +1,5 @@
-
 name:                singleton-nats
-version:             0.4.0.4
+version:             0.4.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
@@ -14,7 +13,8 @@
 
 build-type:          Simple
 cabal-version:       >=1.10
-tested-with:         GHC == 8.0.1, GHC == 8.2.1, GHC == 8.4.1
+tested-with:         GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.2
+extra-source-files:  CHANGELOG.md, README.md
 
 source-repository head
   type: git
@@ -29,3 +29,4 @@
     singletons >= 2.2 && < 2.5
 
   default-language:    Haskell2010
+  ghc-options:         -Wall -Wno-unticked-promoted-constructors