split out singletons lib

4 files changed, 21 insertions, 15 deletions

diff --git a/debian/changelog b/debian/changelog
index fc499c86..af2f5c2b 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -39,10 +39,10 @@ propellor (3.0.0) UNRELEASED; urgency=medium
 		go = property "foo" (return NoChange)
       To fix, specify the type of go:
 	  	go :: Property UnixLike
-    - `ensureProperty` now needs to be passed information about the
+    - `ensureProperty` now needs to be passed a witness to the type of the 
       property it's used in.
       change this:  foo = property desc $ ... ensureProperty bar
-      to this:      foo = property' desc $ \o -> ... ensureProperty o bar
+      to this:      foo = property' desc $ \w -> ... ensureProperty w bar
     - General purpose properties like cmdProperty have type "Property UnixLike".
       When using that to run a command only available on Debian, you can
       tighten the type to only the OS that your more specific property works on.
diff --git a/propellor.cabal b/propellor.cabal
index 4a7739d3..f11d2afe 100644
--- a/propellor.cabal
+++ b/propellor.cabal
@@ -162,6 +162,7 @@ Library
     Propellor.Types.PrivData
     Propellor.Types.Result
     Propellor.Types.ResultCheck
+    Propellor.Types.Singletons
     Propellor.Types.ZFS
   Other-Modules:
     Propellor.Bootstrap
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