split out singletons lib

2 files changed, 18 insertions, 13 deletions

diff --git a/src/Propellor/Types/MetaTypes.hs b/src/Propellor/Types/MetaTypes.hs
index 3e89e28d..39d6e725 100644
--- a/src/Propellor/Types/MetaTypes.hs
+++ b/src/Propellor/Types/MetaTypes.hs
@@ -25,6 +25,7 @@ module Propellor.Types.MetaTypes (
 	EqT,
 ) where
 
+import Propellor.Types.Singletons
 import Propellor.Types.OS
 
 data MetaType
@@ -49,13 +50,6 @@ type instance IncludesInfo (MetaTypes l) = Elem 'WithInfo l
 
 type MetaTypes = Sing
 
--- | 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
-
 -- This boilerplatw would not be needed if the singletons library were
 -- used. However, we're targeting too old a version of ghc to use it yet.
 data instance Sing (x :: MetaType) where
@@ -68,12 +62,6 @@ instance SingI ('Targeting 'OSBuntish) where sing = OSBuntishS
 instance SingI ('Targeting 'OSFreeBSD) where sing = OSFreeBSDS
 instance SingI 'WithInfo where sing = WithInfoS
 
-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
-
 -- | Convenience type operator to combine two `MetaTypes` lists.
 --
 -- For example:
diff --git a/src/Propellor/Types/Singletons.hs b/src/Propellor/Types/Singletons.hs
new file mode 100644
index 00000000..be777ecb
--- /dev/null
+++ b/src/Propellor/Types/Singletons.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies, GADTs #-}
+
+module Propellor.Types.Singletons where
+
+-- | 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