{-# LANGUAGE CPP, DataKinds, PolyKinds, TypeOperators, TypeFamilies, GADTs, UndecidableInstances #-} -- | Simple implementation of singletons, portable back to ghc 7.6.3 module Propellor.Types.Singletons ( module Propellor.Types.Singletons, KProxy(..) ) where #if __GLASGOW_HASKELL__ > 707 import Data.Proxy (KProxy(..)) #else data KProxy (a :: *) = KProxy #endif -- | The data family of singleton types. data family Sing (x :: k) -- | A class used to pass singleton values implicitly. class SingI t where sing :: Sing t -- Lists of singletons data instance Sing (x :: [k]) where Nil :: Sing '[] Cons :: Sing x -> Sing xs -> Sing (x ': xs) instance (SingI x, SingI xs) => SingI (x ': xs) where sing = Cons sing sing instance SingI '[] where sing = Nil data instance Sing (x :: Bool) where TrueS :: Sing 'True FalseS :: Sing 'False instance SingI 'True where sing = TrueS instance SingI 'False where sing = FalseS class (kparam ~ 'KProxy) => SingKind (kparam :: KProxy k) where type DemoteRep kparam :: * -- | From singleton to value. fromSing :: Sing (a :: k) -> DemoteRep kparam instance SingKind ('KProxy :: KProxy a) => SingKind ('KProxy :: KProxy [a]) where type DemoteRep ('KProxy :: KProxy [a]) = [DemoteRep ('KProxy :: KProxy a)] fromSing Nil = [] fromSing (Cons x xs) = fromSing x : fromSing xs instance SingKind ('KProxy :: KProxy Bool) where type DemoteRep ('KProxy :: KProxy Bool) = Bool fromSing FalseS = False fromSing TrueS = True