[commit: base] type-reasoning: Include Richard Eisenberg's suggestion for decidable type equality (functionality not complete yet). (ce431e6)

[Gabor Greif]

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

On branch  : type-reasoning

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

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

commit ce431e62cbdec6ea747e9f9f681df7001bbf0ecb
Author: Gabor Greif <ggreif at gmail.com>
Date:   Wed Feb 6 18:58:46 2013 +0100

    Include Richard Eisenberg's suggestion for decidable type equality (functionality not complete yet).

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

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

diff --git a/GHC/TypeLits.hs b/GHC/TypeLits.hs
index 5546a5a..7715a32 100644
--- a/GHC/TypeLits.hs
+++ b/GHC/TypeLits.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE TypeFamilies #-}           -- for declaring operators + sing family
 {-# LANGUAGE TypeOperators #-}          -- for declaring operator
 {-# LANGUAGE EmptyDataDecls #-}         -- for declaring the kinds
+{-# LANGUAGE EmptyCase #-}              -- for absurd
 {-# LANGUAGE GADTs #-}                  -- for examining type nats
 {-# LANGUAGE PolyKinds #-}              -- for Sing family
 {-# LANGUAGE FlexibleContexts #-}
@@ -56,6 +57,7 @@ import Unsafe.Coerce(unsafeCoerce)
 -- import Data.Bits(testBit,shiftR)
 import Data.Maybe(Maybe(..))
 import Data.List((++))
+import Data.Either(Either (..))
 import Control.Monad (guard, return, (>>))
 
 -- | (Kind) A kind useful for passing kinds as parameters.
@@ -138,6 +140,10 @@ class (kparam ~ KindParam, SingE (kparam :: OfKind k)) => SingEquality (kparam :
   type SameSing kparam :: k -> k -> *
   type SameSing kparam = (:~:)
   sameSing :: Sing a -> Sing b -> Maybe (SameSing kparam a b)
+  sameSing a b = case decideSing a b of
+                 Right witness -> Just witness
+                 otherwise -> Nothing
+  decideSing :: Sing a -> Sing b -> Decision (SameSing kparam a b)
 
 instance SingE (KindParam :: OfKind Nat) where
   type DemoteRep (KindParam :: OfKind Nat) = Integer
@@ -149,9 +155,13 @@ instance SingE (KindParam :: OfKind Symbol) where
 
 instance SingEquality (KindParam :: OfKind Nat) where
   sameSing = eqSingNat
+  decideSing a b = case eqSingNat a b of
+                   Just witness -> Right witness
 
 instance SingEquality (KindParam :: OfKind Symbol) where
   sameSing = eqSingSym
+  decideSing a b = case eqSingSym a b of
+                   Just witness -> Right witness
 
 {- | A convenient name for the type used to representing the values
 for a particular singleton family.  For example, @Demote 2 ~ Integer@,
@@ -248,6 +258,18 @@ data (:~:) :: k -> k -> * where
 instance Show (a :~: b) where
   show Refl = "Refl"
 
+
+-- | A type that has no inhabitants.
+data Void
+
+-- | Anything follow from falseness.
+absurd :: Void -> a
+absurd x = case x of {}
+
+type Refuted a = a -> Void
+
+type Decision a = Either (Refuted a) a
+
 {- | Check if two type-natural singletons of potentially different types
 are indeed the same, by comparing their runtime representations.