From 67f4a35f08caff9efd5ec930943a02217188cc79 Mon Sep 17 00:00:00 2001 From: Joey Hess Date: Mon, 28 Mar 2016 02:28:08 -0400 Subject: implemented pickOS Fell down the fromSing rabbit hole, followed by the OMH ghc doesh't work rabbit hole. Suboptimal. --- src/Propellor/Types/Singletons.hs | 36 ++++++++++++++++++++++++++++++++++-- 1 file changed, 34 insertions(+), 2 deletions(-) (limited to 'src/Propellor/Types/Singletons.hs') diff --git a/src/Propellor/Types/Singletons.hs b/src/Propellor/Types/Singletons.hs index be777ecb..f2089ee8 100644 --- a/src/Propellor/Types/Singletons.hs +++ b/src/Propellor/Types/Singletons.hs @@ -1,6 +1,17 @@ -{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies, GADTs #-} +{-# LANGUAGE CPP, DataKinds, PolyKinds, TypeOperators, TypeFamilies, GADTs, UndecidableInstances #-} -module Propellor.Types.Singletons where +-- | 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) @@ -15,3 +26,24 @@ data instance Sing (x :: [k]) where 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 -- cgit v1.2.3