diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,2 +1,6 @@
+- 0.1.2.0
+    - Enable `PolyKinds` on GHC >= 7.6
+    - Add `sboolEqRefl :: SBoolI (a == b) => Maybe (a :~: b)`
+
 - 0.1.1.0
     - Add `eqToRefl`, `eqCast`, `trivialRefl`
diff --git a/singleton-bool.cabal b/singleton-bool.cabal
--- a/singleton-bool.cabal
+++ b/singleton-bool.cabal
@@ -1,9 +1,9 @@
--- This file has been generated from package.yaml by hpack version 0.14.0.
+-- This file has been generated from package.yaml by hpack version 0.14.1.
 --
 -- see: https://github.com/sol/hpack
 
 name:           singleton-bool
-version:        0.1.1.0
+version:        0.1.2.0
 synopsis:       Type level booleans
 description:    Type level booleans.
                 .
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
@@ -4,9 +4,15 @@
 {-# LANGUAGE KindSignatures      #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators       #-}
+#if __GLASGOW_HASKELL__ >= 706
+{-# LANGUAGE PolyKinds           #-}
+#endif
 #if __GLASGOW_HASKELL__ >= 800
 {-# OPTIONS_GHC -Wno-redundant-constraints #-}
 #endif
+#if MIN_VERSION_base(4,7,0)
+{-# LANGUAGE FlexibleContexts #-}
+#endif
 module Data.Singletons.Bool (
     SBool(..),
     SBoolI(..),
@@ -14,7 +20,8 @@
     -- | These are only defined with @base >= 4.7@
 #if MIN_VERSION_base(4,7,0)
     sboolAnd, sboolOr, sboolNot,
-    eqToRefl, eqCast, trivialRefl,
+    eqToRefl, eqCast, sboolEqRefl,
+    trivialRefl,
 #endif
     ) where
 
@@ -60,4 +67,12 @@
 -- | @since 0.1.1.0
 trivialRefl :: () :~: ()
 trivialRefl = Refl
+
+-- | Useful combination of 'sbool' and 'eqToRefl'
+--
+-- @since 0.1.2.0
+sboolEqRefl :: forall (a :: k) (b :: k). SBoolI (a == b) => Maybe (a :~: b)
+sboolEqRefl = case sbool :: SBool (a == b) of
+    STrue  -> Just eqToRefl
+    SFalse -> Nothing
 #endif