#if __GLASGOW_HASKELL__ >= 707
#else
#endif
module Data.Singletons.Core where
import Data.Singletons.Util
import Data.Singletons.Singletons
import GHC.TypeLits (Nat, Symbol)
import Data.Singletons.Types
import Unsafe.Coerce
#if __GLASGOW_HASKELL__ >= 707
import GHC.TypeLits (KnownNat, KnownSymbol, natVal, symbolVal)
import Data.Proxy
import Data.Type.Equality
#else
import qualified GHC.TypeLits as TypeLits
#endif
type KindOf (a :: k) = ('KProxy :: KProxy k)
data family Sing (a :: k)
class SingI (a :: k) where
sing :: Sing a
class (kparam ~ 'KProxy) => SingKind (kparam :: KProxy k) where
type DemoteRep kparam :: *
fromSing :: Sing (a :: k) -> DemoteRep kparam
toSing :: DemoteRep kparam -> SomeSing kparam
type Demote (a :: k) = DemoteRep ('KProxy :: KProxy k)
data SomeSing (kproxy :: KProxy k) where
SomeSing :: Sing (a :: k) -> SomeSing ('KProxy :: KProxy k)
$(genSingletons basicTypes)
newtype instance Sing (n :: Nat) = SNat Integer
#if __GLASGOW_HASKELL__ >= 707
instance KnownNat n => SingI n where
sing = SNat (natVal (Proxy :: Proxy n))
#else
instance TypeLits.SingRep n Integer => SingI (n :: Nat) where
sing = SNat (TypeLits.fromSing (TypeLits.sing :: TypeLits.Sing n))
#endif
instance SingKind ('KProxy :: KProxy Nat) where
type DemoteRep ('KProxy :: KProxy Nat) = Integer
fromSing (SNat n) = n
toSing n = SomeSing (SNat n)
newtype instance Sing (n :: Symbol) = SSym String
#if __GLASGOW_HASKELL__ >= 707
instance KnownSymbol n => SingI n where
sing = SSym (symbolVal (Proxy :: Proxy n))
#else
instance TypeLits.SingRep n String => SingI (n :: Symbol) where
sing = SSym (TypeLits.fromSing (TypeLits.sing :: TypeLits.Sing n))
#endif
instance SingKind ('KProxy :: KProxy Symbol) where
type DemoteRep ('KProxy :: KProxy Symbol) = String
fromSing (SSym n) = n
toSing s = SomeSing (SSym s)
class (kparam ~ 'KProxy) => SDecide (kparam :: KProxy k) where
(%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
$(singDecideInstances basicTypes)
instance SDecide ('KProxy :: KProxy Nat) where
(SNat n) %~ (SNat m)
| n == m = Proved $ unsafeCoerce Refl
| otherwise = Disproved (\_ -> error errStr)
where errStr = "Broken Nat singletons"
instance SDecide ('KProxy :: KProxy Symbol) where
(SSym n) %~ (SSym m)
| n == m = Proved $ unsafeCoerce Refl
| otherwise = Disproved (\_ -> error errStr)
where errStr = "Broken Symbol singletons"
instance SDecide ('KProxy :: KProxy k) => TestEquality (Sing :: k -> *) where
testEquality a b =
case a %~ b of
Proved Refl -> Just Refl
Disproved _ -> Nothing