diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,7 @@
+- 0.1.5
+    - Add `discreteBool :: Dec (a :~: b)` (GHC-7.8+)
+    - Add `Show`, `Eq`, `Ord` `SBool b` instances.
+
 - 0.1.4
     - Add `fromSBool` and `withSomeSBool`.
 
diff --git a/singleton-bool.cabal b/singleton-bool.cabal
--- a/singleton-bool.cabal
+++ b/singleton-bool.cabal
@@ -1,44 +1,44 @@
-name:           singleton-bool
-version:        0.1.4
-synopsis:       Type level booleans
-description:    Type level booleans.
-                .
-                @singletons@ package provides similar functionality,
-                but it has tight dependency constraints.
-category:       Web
-homepage:       https://github.com/phadej/singleton-bool#readme
-bug-reports:    https://github.com/phadej/singleton-bool/issues
-author:         Oleg Grenrus <oleg.grenrus@iki.fi>
-maintainer:     Oleg Grenrus <oleg.grenrus@iki.fi>
-license:        BSD3
-license-file:   LICENSE
-build-type:     Simple
-cabal-version:  >= 1.10
+cabal-version:      >=1.10
+name:               singleton-bool
+version:            0.1.5
+synopsis:           Type level booleans
+description:
+  Type level booleans.
+  .
+  @singletons@ package provides similar functionality,
+  but it has tight dependency constraints.
+
+category:           Web
+homepage:           https://github.com/phadej/singleton-bool#readme
+bug-reports:        https://github.com/phadej/singleton-bool/issues
+author:             Oleg Grenrus <oleg.grenrus@iki.fi>
+maintainer:         Oleg Grenrus <oleg.grenrus@iki.fi>
+license:            BSD3
+license-file:       LICENSE
+build-type:         Simple
 tested-with:
-  GHC==7.6.3,
-  GHC==7.8.4,
-  GHC==7.10.3,
-  GHC==8.0.2,
-  GHC==8.2.2,
-  GHC==8.4.1
+  GHC ==8.8.1 || ==8.6.5 || ==8.4.4 || ==8.2.2 || ==8.0.2 || ==7.10.3 || ==7.8.4 || ==7.6.3
 
 extra-source-files:
   CHANGELOG.md
   README.md
 
 source-repository head
-  type: git
+  type:     git
   location: https://github.com/phadej/singleton-bool
 
 library
-  hs-source-dirs:
-    src
-  ghc-options: -Wall
+  hs-source-dirs:   src
+  ghc-options:      -Wall
   build-depends:
-    base        >=4.6 && <4.12
-  exposed-modules:
-    Data.Singletons.Bool
+      base  >=4.6   && <4.13
+
+  if impl(ghc >= 7.8)
+    build-depends:
+      dec   >=0.0.3 && <0.1
+
+  exposed-modules:  Data.Singletons.Bool
   default-language: Haskell2010
 
-  if !impl(ghc >= 7.8)
-    build-depends: tagged >= 0.8.5 && <0.9
+  if !impl(ghc >=7.8)
+    build-depends: tagged >=0.8.5 && <0.9
diff --git a/src/Data/Singletons/Bool.hs b/src/Data/Singletons/Bool.hs
--- a/src/Data/Singletons/Bool.hs
+++ b/src/Data/Singletons/Bool.hs
@@ -10,6 +10,7 @@
 {-# OPTIONS_GHC -Wno-redundant-constraints #-}
 #endif
 #if MIN_VERSION_base(4,7,0)
+{-# LANGUAGE EmptyCase        #-}
 {-# LANGUAGE FlexibleContexts #-}
 #endif
 -- | Additions to "Data.Type.Bool".
@@ -20,6 +21,11 @@
     withSomeSBool,
     reflectBool,
     reifyBool,
+    -- * Data.Type.Dec
+#if MIN_VERSION_base(4,7,0)
+    -- | 'discreteBool' is available with @base >= 4.7@ (GHC-7.8)
+    discreteBool,
+#endif
     -- * Data.Type.Bool and .Equality
     -- | These are only defined with @base >= 4.7@
 #if MIN_VERSION_base(4,7,0)
@@ -31,12 +37,17 @@
 
 #if MIN_VERSION_base(4,7,0)
 import           Data.Type.Bool
+import           Data.Type.Dec      (Dec (..))
 import           Data.Type.Equality
 import           Unsafe.Coerce      (unsafeCoerce)
 #endif
 
 import Data.Proxy (Proxy (..))
 
+-- $setup
+-- >>> :set -XDataKinds -XTypeOperators
+-- >>> import Data.Type.Dec (decShow)
+
 data SBool (b :: Bool) where
     STrue  :: SBool 'True
     SFalse :: SBool 'False
@@ -45,13 +56,26 @@
 instance SBoolI 'True       where sbool = STrue
 instance SBoolI 'False      where sbool = SFalse
 
+-- | @since 0.1.5
+instance Show (SBool b) where
+    showsPrec _ STrue  = showString "STrue"
+    showsPrec _ SFalse = showString "SFalse"
+
+-- | @since 0.1.5
+instance Eq (SBool b) where
+    _ == _ = True
+
+-- | @since 0.1.5
+instance Ord (SBool b) where
+    compare _ _ = EQ
+
 -------------------------------------------------------------------------------
 -- conversion to and from explicit SBool values
 -------------------------------------------------------------------------------
 
 -- | Convert an 'SBool' to the corresponding 'Bool'.
 --
--- @since next
+-- @since 0.1.4
 fromSBool :: SBool b -> Bool
 fromSBool STrue  = True
 fromSBool SFalse = False
@@ -61,7 +85,7 @@
 -- >>> withSomeSBool True fromSBool
 -- True
 --
--- @since next
+-- @since 0.1.4
 withSomeSBool :: Bool -> (forall b. SBool b -> r) -> r
 withSomeSBool True  f = f STrue
 withSomeSBool False f = f SFalse
@@ -70,7 +94,7 @@
 -- reify & reflect
 -------------------------------------------------------------------------------
 
--- | Reify 'Bool'.
+-- | Reify 'Bool' to type-level.
 --
 -- >>> reifyBool True reflectBool
 -- True
@@ -79,16 +103,39 @@
 reifyBool True  f = f (Proxy :: Proxy 'True)
 reifyBool False f = f (Proxy :: Proxy 'False)
 
+-- | Reflect to term-level.
+--
+-- >>> reflectBool (Proxy :: Proxy 'True)
+-- True
 reflectBool :: forall b proxy. SBoolI b => proxy b -> Bool
-reflectBool _ = case sbool :: SBool b of
-    STrue  -> True
-    SFalse -> False
+reflectBool _ = fromSBool (sbool :: SBool b)
 
 -------------------------------------------------------------------------------
+-- Discrete
+-------------------------------------------------------------------------------
+
+#if MIN_VERSION_base(4,7,0)
+-- | Decidable equality.
+--
+-- >>> decShow (discreteBool :: Dec ('True :~: 'True))
+-- "Yes Refl"
+--
+-- @since 0.1.5
+discreteBool :: forall a b. (SBoolI a, SBoolI b) => Dec (a :~: b)
+discreteBool = case (sbool :: SBool a, sbool :: SBool b) of
+    (STrue,  STrue)  -> Yes Refl
+    (STrue,  SFalse) -> No $ \p  -> case p of {}
+    (SFalse, STrue)  -> No $ \p  -> case p of {}
+    (SFalse, SFalse) -> Yes Refl
+#endif
+
+-------------------------------------------------------------------------------
 -- Witnesses
 -------------------------------------------------------------------------------
 
 #if MIN_VERSION_base(4,7,0)
+-- | >>> sboolAnd STrue SFalse
+-- SFalse
 sboolAnd :: SBool a -> SBool b -> SBool (a && b)
 sboolAnd SFalse _ = SFalse
 sboolAnd STrue  b = b
@@ -113,10 +160,22 @@
 trivialRefl :: () :~: ()
 trivialRefl = Refl
 
+-- GHC 8.10+ requires that all kind variables be explicitly quantified after
+-- a `forall`. Technically, GHC has had the ability to do this since GHC 8.0,
+-- but GHC 8.0-8.4 require enabling TypeInType to do. To avoid having to faff
+-- around with CPP to enable TypeInType on certain GHC versions, we only
+-- explicitly quantify kind variables on GHC 8.6 or later, since those versions
+-- do not require TypeInType, only PolyKinds.
+# if __GLASGOW_HASKELL__ >= 806
+#  define KVS(kvs) kvs
+# else
+#  define KVS(kvs)
+# endif
+
 -- | Useful combination of 'sbool' and 'eqToRefl'
 --
 -- @since 0.1.2.0
-sboolEqRefl :: forall (a :: k) (b :: k). SBoolI (a == b) => Maybe (a :~: b)
+sboolEqRefl :: forall KVS(k) (a :: k) (b :: k). SBoolI (a == b) => Maybe (a :~: b)
 sboolEqRefl = case sbool :: SBool (a == b) of
     STrue  -> Just eqToRefl
     SFalse -> Nothing