diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,6 @@
+### 0.4.1 [2018.02.13]
+* Add `elimVoid` to `Data.Eliminator`.
+
 ## 0.4 [2018.01.09]
 * Require `singletons-2.4` and GHC 8.4.
 
diff --git a/eliminators.cabal b/eliminators.cabal
--- a/eliminators.cabal
+++ b/eliminators.cabal
@@ -1,5 +1,5 @@
 name:                eliminators
-version:             0.4
+version:             0.4.1
 synopsis:            Dependently typed elimination functions using singletons
 description:         This library provides eliminators for inductive data types,
                      leveraging the power of the @singletons@ library to allow
@@ -28,8 +28,8 @@
                        Data.Eliminator.TypeNats
   build-depends:       base             >= 4.11    && < 4.12
                      , extra            >= 1.4.2   && < 1.7
-                     , singletons       >= 2.4     && < 2.5
-                     , singleton-nats   >= 0.4.0.3 && < 0.5
+                     , singletons       >= 2.4.1   && < 2.5
+                     , singleton-nats   >= 0.4.0.4 && < 0.5
                      , template-haskell >= 2.13    && < 2.14
                      , th-abstraction   >= 0.2.3   && < 0.3
                      , th-desugar       >= 1.8     && < 1.9
@@ -51,8 +51,8 @@
   build-depends:       base           >= 4.11    && < 4.12
                      , eliminators
                      , hspec          >= 2       && < 3
-                     , singletons     >= 2.4     && < 2.5
-                     , singleton-nats >= 0.4.0.3 && < 0.5
+                     , singletons     >= 2.4.1   && < 2.5
+                     , singleton-nats >= 0.4.0.4 && < 0.5
   build-tool-depends:  hspec-discover:hspec-discover
   hs-source-dirs:      tests
   default-language:    Haskell2010
diff --git a/src/Data/Eliminator.hs b/src/Data/Eliminator.hs
--- a/src/Data/Eliminator.hs
+++ b/src/Data/Eliminator.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE EmptyCase #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
@@ -37,6 +38,7 @@
   , elimTuple5
   , elimTuple6
   , elimTuple7
+  , elimVoid
   ) where
 
 import Control.Monad.Extra
@@ -46,6 +48,7 @@
 import Data.Nat
 import Data.Singletons.Prelude
 import Data.Singletons.Prelude.List.NonEmpty (Sing(..))
+import Data.Void (Void)
 
 import Language.Haskell.TH.Desugar (tupleNameDegree_maybe)
 
@@ -65,7 +68,7 @@
   with @~>@ prepended.
 -}
 
-$(concatMapM deriveElim [''Bool, ''Either, ''Maybe, ''Nat, ''NonEmpty, ''Ordering])
+$(concatMapM deriveElim [''Bool, ''Either, ''Maybe, ''Nat, ''NonEmpty, ''Ordering, ''Void])
 $(deriveElimNamed "elimList" ''[])
 $(concatMapM (\n -> let Just deg = tupleNameDegree_maybe n
                     in deriveElimNamed ("elimTuple" ++ show deg) n)