{-# LANGUAGE CPP, DataKinds, PolyKinds, TypeOperators, TypeFamilies, GADTs, FlexibleContexts #-}

-- | 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