diff --git a/Data/Type/Ordinal.hs b/Data/Type/Ordinal.hs
--- a/Data/Type/Ordinal.hs
+++ b/Data/Type/Ordinal.hs
@@ -1,7 +1,11 @@
+{-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE CPP, DataKinds, EmptyDataDecls, FlexibleContexts         #-}
 {-# LANGUAGE FlexibleInstances, GADTs, KindSignatures, PolyKinds      #-}
 {-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TemplateHaskell #-}
 {-# LANGUAGE TypeFamilies, TypeOperators                              #-}
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
+{-# LANGUAGE EmptyCase, LambdaCase #-}
+#endif
 -- | Set-theoretic ordinal arithmetic
 module Data.Type.Ordinal
        ( -- * Data-types
@@ -12,7 +16,9 @@
          unsafeFromInt, inclusion, inclusion',
          -- * Ordinal arithmetics
          (@+), enumOrdinal,
-         -- * Quasi Quote
+         -- * Elimination rules for @'Ordinal' 'Z'@.
+         absurdOrd, vacuousOrd, vacuousOrdM,
+         -- * Quasi Quoter
          od
        ) where
 import Data.Constraint
@@ -24,7 +30,9 @@
 import Unsafe.Coerce
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
 import Data.Singletons.Prelude
+import Data.Typeable (Typeable)
 #endif
+import Control.Monad (liftM)
 
 -- | Set-theoretic (finite) ordinals:
 --
@@ -35,6 +43,10 @@
   OZ :: Ordinal (S n)
   OS :: Ordinal n -> Ordinal (S n)
 
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
+-- | Since 0.2.3.0  
+deriving instance Typeable Ordinal
+#endif
 -- | Parsing always fails, because there are no inhabitant.
 instance Read (Ordinal Z) where
   readsPrec _ _ = []
@@ -85,7 +97,7 @@
 unsafeFromInt n =
     case (promote n :: Monomorphic (Sing :: Nat -> *)) of
       Monomorphic sn ->
-        case sS sn %:<<= (sing :: SNat n) of
+        case SS sn %:<<= (sing :: SNat n) of
           STrue -> sNatToOrd' (sing :: SNat n) sn
           SFalse -> error "Bound over!"
 
@@ -104,10 +116,10 @@
 
 -- | Convert @Ordinal n@ into @SNat m@ with the proof of @S m :<<= n@.
 ordToSNat' :: Ordinal n -> CastedOrdinal n
-ordToSNat' OZ = CastedOrdinal sZ
+ordToSNat' OZ = CastedOrdinal SZ
 ordToSNat' (OS on) =
   case ordToSNat' on of
-    CastedOrdinal m -> CastedOrdinal (sS m)
+    CastedOrdinal m -> CastedOrdinal (SS m)
 
 -- | Convert @Ordinal n@ into monomorphic @SNat@
 ordToSNat :: Ordinal n -> Monomorphic (Sing :: Nat -> *)
@@ -132,7 +144,7 @@
 inclusion' :: (n :<<= m) ~ True => SNat m -> Ordinal n -> Ordinal m
 inclusion' (SS SZ) OZ = OZ
 inclusion' (SS (SS _)) OZ = OZ
-inclusion' (SS (SS n)) (OS m) = OS $ inclusion' (sS n) m
+inclusion' (SS (SS n)) (OS m) = OS $ inclusion' (SS n) m
 inclusion' _ _ = bugInGHC
 -}
 
@@ -152,6 +164,30 @@
   case sing :: SNat n of
     SS sn -> case singInstance sn of SingInstance -> OS $ n @+ m
     _ -> bugInGHC
+
+-- | Since @Ordinal Z@ is logically not inhabited, we can coerce it to any value.
+--
+-- Since 0.2.3.0
+absurdOrd :: Ordinal Z -> a
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
+absurdOrd cs = case cs of {}
+#else
+absurdOrd _ = error "Impossible!"
+#endif
+
+-- | 'absurdOrd' for the value in 'Functor'.
+-- 
+--   Since 0.2.3.0
+vacuousOrd :: Functor f => f (Ordinal Z) -> f a
+vacuousOrd = fmap absurdOrd
+
+-- | 'absurdOrd' for the value in 'Monad'.
+--   This function will become uneccesary once 'Applicative' (and hence 'Functor')
+--   become the superclass of 'Monad'.
+-- 
+--   Since 0.2.3.0
+vacuousOrdM :: Monad m => m (Ordinal Z) -> m a
+vacuousOrdM = liftM absurdOrd
 
 -- | Quasiquoter for ordinals
 od :: QuasiQuoter
diff --git a/type-natural.cabal b/type-natural.cabal
--- a/type-natural.cabal
+++ b/type-natural.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                type-natural
-version:             0.2.2.0
+version:             0.2.3.0
 synopsis:            Type-level natural and proofs of their properties.
 description:         Type-level natural numbers and proofs of their properties.
 homepage:            https://github.com/konn/type-natural