[commit: base] master: Add functions that compare singletons for equality (with evidence) (85bda3d)

[Iavor Diatchki]

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

On branch  : master

http://hackage.haskell.org/trac/ghc/changeset/85bda3d6e36fb8b3d7121ccc01c8ccfc3942431f

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

commit 85bda3d6e36fb8b3d7121ccc01c8ccfc3942431f
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Sat Dec 22 15:22:43 2012 -0800

    Add functions that compare singletons for equality (with evidence)

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

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

diff --git a/GHC/TypeLits.hs b/GHC/TypeLits.hs
index 50a5c86..ed1f205 100644
--- a/GHC/TypeLits.hs
+++ b/GHC/TypeLits.hs
@@ -29,10 +29,14 @@ module GHC.TypeLits
   , type (<=), type (<=?), type (+), type (*), type (^)
   , type (-)
 
+    -- * Comparing for equality
+  , type (:~:) (..), eqSingNat, eqSingSym
+
     -- * Destructing type-nat singletons.
   , isZero, IsZero(..)
   , isEven, IsEven(..)
 
+
     -- * Matching on type-nats
   , Nat1(..), FromNat1
 
@@ -215,4 +219,40 @@ type family FromNat1 (n :: Nat1) :: Nat
 type instance FromNat1 Zero     = 0
 type instance FromNat1 (Succ n) = 1 + FromNat1 n
 
+--------------------------------------------------------------------------------
+
+-- | A type that provides evidence for equality between two types.
+data (:~:) :: k -> k -> * where
+  Refl :: a :~: a
+
+instance Show (a :~: b) where
+  show Refl = "Refl"
+
+{- | Check if two type-natural singletons of potentially different types
+are indeed the same, by comparing their runtime representations.
+
+WARNING: in combination with `unsafeSingNat` this may lead to unsoudness:
+
+> eqSingNat (sing :: Sing 1) (unsafeSingNat 1 :: Sing 2)
+> == Just (Refl :: 1 :~: 2)
+-}
+
+eqSingNat :: Sing (m :: Nat) -> Sing (n :: Nat) -> Maybe (m :~: n)
+eqSingNat x y
+  | fromSing x == fromSing y  = Just (unsafeCoerce Refl)
+  | otherwise                 = Nothing
+
+
+{- | Check if two symbol singletons of potentially different types
+are indeed the same, by comparing their runtime representations.
+WARNING: in combination with `unsafeSingSymbol` this may lead to unsoudness
+(see `eqSingNat` for an example).
+-}
+
+eqSingSym:: Sing (m :: Symbol) -> Sing (n :: Symbol) -> Maybe (m :~: n)
+eqSingSym x y
+  | fromSing x == fromSing y  = Just (unsafeCoerce Refl)
+  | otherwise                 = Nothing
+
+