{-# LANGUAGE TypeInType #-}
module Data.Singletons where
import Data.Kind
import GHC.TypeLits
import Data.Typeable
type family Sing :: k -> Type
class SingI a where
sing :: Sing a
data SNat (n :: Nat) = KnownNat n => SNat
type instance Sing = SNat
instance KnownNat a => SingI (a :: Nat) where
sing = SNat
data SSymbol (n :: Symbol) = KnownSymbol n => SSym
type instance Sing = SSymbol
instance KnownSymbol a => SingI (a :: Symbol) where
sing = SSym
withKnownNat :: Sing n -> (KnownNat n => r) -> r
withKnownNat SNat f = f
withKnownSymbol :: Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol SSym f = f
data SList :: [k] -> Type where
SNil :: SList '[]
SCons :: forall k (h :: k) (t :: [k]). Sing h -> SList t -> SList (h ': t)
type instance Sing = SList
instance SingI ('[] :: [k]) where
sing = SNil
instance (SingI x, SingI xs) => SingI ( (x ': xs) :: [k]) where
sing = SCons sing sing
data STuple2 (a :: (k1, k2)) where
STuple2 :: Sing x -> Sing y -> STuple2 '(x, y)
instance (SingI x, SingI y) => SingI ( '(x, y) :: (k1, k2)) where
sing = STuple2 sing sing
type instance Sing = STuple2
data STypeRep :: Type -> Type where
STypeRep :: forall (t :: Type). Typeable t => STypeRep t
type instance Sing = STypeRep
instance Typeable a => SingI (a :: Type) where
sing = STypeRep