module Data.Singletons.Eq (
SEq(..),
type (==), (:==), (:/=)
) where
import Data.Singletons.Util
import Data.Singletons.Bool
import Data.Singletons.Singletons
import Data.Singletons.Core
import GHC.TypeLits ( Nat, Symbol )
import Unsafe.Coerce
#if __GLASGOW_HASKELL__ >= 707
import Data.Proxy
import Data.Type.Equality
type a :== b = a == b
#else
import Data.Singletons.Types
import Data.Singletons.Promote
type family (a :: k) :== (b :: k) :: Bool
type a == b = a :== b
#endif
type a :/= b = Not (a :== b)
class (kparam ~ 'KProxy) => SEq (kparam :: KProxy k) where
(%:==) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :== b)
(%:/=) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :/= b)
a %:/= b = sNot (a %:== b)
#if __GLASGOW_HASKELL__ < 707
$(promoteEqInstances basicTypes)
#endif
$(singEqInstancesOnly basicTypes)
instance SEq ('KProxy :: KProxy Nat) where
(SNat a) %:== (SNat b)
| a == b = unsafeCoerce STrue
| otherwise = unsafeCoerce SFalse
instance SEq ('KProxy :: KProxy Symbol) where
(SSym a) %:== (SSym b)
| a == b = unsafeCoerce STrue
| otherwise = unsafeCoerce SFalse