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

    -- | Simple implementation of singletons, portable back to ghc 8.0.1

    module Propellor.Types.Singletons (
    	module Propellor.Types.Singletons,
    	KProxy(..)
    ) where

    import Data.Kind (Type)
    import Data.Proxy (KProxy(..))

    -- | 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 :: Sing (x : xs)
    sing = Sing x -> Sing xs -> Sing (x : xs)
    forall {k} (x :: k) (xs :: [k]). Sing x -> Sing xs -> Sing (x : xs)
    Cons Sing x
    forall {k} (t :: k). SingI t => Sing t
    sing Sing xs
    forall {k} (t :: k). SingI t => Sing t
    sing
    instance SingI '[] where sing :: Sing '[]
    sing = Sing '[]
    forall k. Sing '[]
    Nil

    data instance Sing (x :: Bool) where
    	TrueS :: Sing 'True
    	FalseS :: Sing 'False
    instance SingI 'True where sing :: Sing 'True
    sing = Sing 'True
    TrueS
    instance SingI 'False where sing :: Sing 'False
    sing = Sing 'False
    FalseS

    class (kparam ~ 'KProxy) => SingKind (kparam :: KProxy k) where
    	type DemoteRep kparam :: Type
    	-- | 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 :: forall (a :: [a]). Sing a -> DemoteRep 'KProxy
    fromSing Sing a
    R:Sing[]x a a
    Nil = []
    	fromSing (Cons Sing x
    x Sing xs
    xs) = Sing x -> DemoteRep 'KProxy
    forall (a :: a). Sing a -> DemoteRep 'KProxy
    forall k (kparam :: KProxy k) (a :: k).
    SingKind kparam =>
    Sing a -> DemoteRep kparam
    fromSing Sing x
    x DemoteRep 'KProxy -> [DemoteRep 'KProxy] -> [DemoteRep 'KProxy]
    forall a. a -> [a] -> [a]
    : Sing xs -> DemoteRep 'KProxy
    forall (a :: [a]). Sing a -> DemoteRep 'KProxy
    forall k (kparam :: KProxy k) (a :: k).
    SingKind kparam =>
    Sing a -> DemoteRep kparam
    fromSing Sing xs
    xs

    instance SingKind ('KProxy :: KProxy Bool) where
    	type DemoteRep ('KProxy :: KProxy Bool) = Bool
    	fromSing :: forall (a :: Bool). Sing a -> DemoteRep 'KProxy
    fromSing Sing a
    R:SingBoolx a
    FalseS = Bool
    DemoteRep 'KProxy
    False
    	fromSing Sing a
    R:SingBoolx a
    TrueS = Bool
    DemoteRep 'KProxy
    True