diff --git a/GHC/TypeLits.hs b/GHC/TypeLits.hs
index 50a5c86..cf04658 100644
--- a/GHC/TypeLits.hs
+++ b/GHC/TypeLits.hs
@@ -25,6 +25,9 @@ module GHC.TypeLits
     -- * Working with singletons
   , withSing, singThat
 
+    -- * Singleton type equality witness
+  , SingEq(..)
+
     -- * Functions on type nats
   , type (<=), type (<=?), type (+), type (*), type (^)
   , type (-)
@@ -50,6 +53,7 @@ import Unsafe.Coerce(unsafeCoerce)
 import Data.Bits(testBit,shiftR)
 import Data.Maybe(Maybe(..))
 import Data.List((++))
+import Control.Monad (guard, return, (>>))
 
 -- | (Kind) A kind useful for passing kinds as parameters.
 data OfKind (a :: *) = KindParam
@@ -123,17 +127,27 @@ and not their type---all types of a given kind are processed by the
 same instances.
 -}
 
+data SingEq :: k -> k -> * where
+  SingEq :: SingEq s s
+
 class (kparam ~ KindParam) => SingE (kparam :: OfKind k) where
   type DemoteRep kparam :: *
   fromSing :: Sing (a :: k) -> DemoteRep kparam
+  type SameSing kparam :: k -> k -> *
+  type SameSing kparam = SingEq
+  sameSing :: Sing a -> Sing b -> Maybe (SameSing kparam a b)
 
 instance SingE (KindParam :: OfKind Nat) where
   type DemoteRep (KindParam :: OfKind Nat) = Integer
   fromSing (SNat n) = n
+  sameSing a b = do guard $ fromSing a == fromSing b
+                    return $ unsafeCoerce SingEq
 
 instance SingE (KindParam :: OfKind Symbol) where
   type DemoteRep (KindParam :: OfKind Symbol) = String
   fromSing (SSym s) = s
+  sameSing a b = do guard $ fromSing a == fromSing b
+                    return $ unsafeCoerce SingEq
 
 {- | A convenient name for the type used to representing the values
 for a particular singleton family.  For example, @Demote 2 ~ Integer@,