[commit: base] type-reasoning: Introduce the SingEquality class (ad97c40)

[Gabor Greif]

Repository : ssh://darcs.haskell.org//srv/darcs/packages/base

On branch  : type-reasoning

http://hackage.haskell.org/trac/ghc/changeset/ad97c40764fab97f87d1739983c77cc12427b2e4

>---------------------------------------------------------------

commit ad97c40764fab97f87d1739983c77cc12427b2e4
Author: Gabor Greif <ggreif at gmail.com>
Date:   Fri Nov 30 12:23:28 2012 +0100

    Introduce the SingEquality class
    with customizable witness type
    and a sameSing method that may
    produce the latter.

>---------------------------------------------------------------

 GHC/TypeLits.hs |   14 +++++++++++++-
 1 files changed, 13 insertions(+), 1 deletions(-)

diff --git a/GHC/TypeLits.hs b/GHC/TypeLits.hs
index f8b759e..5546a5a 100644
--- a/GHC/TypeLits.hs
+++ b/GHC/TypeLits.hs
@@ -30,7 +30,7 @@ module GHC.TypeLits
   , type (-)
 
     -- * Comparing for equality
-  , type (:~:) (..), eqSingNat, eqSingSym
+  , type (:~:) (..), eqSingNat, eqSingSym, SingEquality (..)
 
     -- * Destructing type-nat singletons.
   , isZero, IsZero(..)
@@ -56,6 +56,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
@@ -133,6 +134,11 @@ class (kparam ~ KindParam) => SingE (kparam :: OfKind k) where
   type DemoteRep kparam :: *
   fromSing :: Sing (a :: k) -> DemoteRep kparam
 
+class (kparam ~ KindParam, SingE (kparam :: OfKind k)) => SingEquality (kparam :: OfKind k) where
+  type SameSing kparam :: k -> k -> *
+  type SameSing kparam = (:~:)
+  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
@@ -141,6 +147,12 @@ instance SingE (KindParam :: OfKind Symbol) where
   type DemoteRep (KindParam :: OfKind Symbol) = String
   fromSing (SSym s) = s
 
+instance SingEquality (KindParam :: OfKind Nat) where
+  sameSing = eqSingNat
+
+instance SingEquality (KindParam :: OfKind Symbol) where
+  sameSing = eqSingSym
+
 {- | A convenient name for the type used to representing the values
 for a particular singleton family.  For example, @Demote 2 ~ Integer@,
 and also @Demote 3 ~ Integer@, but @Demote "Hello" ~ String at . -}