summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--propellor.cabal3
-rw-r--r--src/Propellor/Types.hs294
-rw-r--r--src/Propellor/Types/MetaTypes.hs276
-rw-r--r--src/Propellor/Types/OS.hs2
4 files changed, 396 insertions, 179 deletions
diff --git a/propellor.cabal b/propellor.cabal
index dc322e88..a631f262 100644
--- a/propellor.cabal
+++ b/propellor.cabal
@@ -146,16 +146,17 @@ Library
Propellor.Exception
Propellor.Types
Propellor.Types.Chroot
+ Propellor.Types.CmdLine
Propellor.Types.Container
Propellor.Types.Docker
Propellor.Types.Dns
Propellor.Types.Empty
Propellor.Types.Info
+ Propellor.Types.MetaTypes
Propellor.Types.OS
Propellor.Types.PrivData
Propellor.Types.Result
Propellor.Types.ResultCheck
- Propellor.Types.CmdLine
Propellor.Types.ZFS
Other-Modules:
Propellor.Bootstrap
diff --git a/src/Propellor/Types.hs b/src/Propellor/Types.hs
index 542a1f66..6c1412c1 100644
--- a/src/Propellor/Types.hs
+++ b/src/Propellor/Types.hs
@@ -7,23 +7,29 @@
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE PolyKinds #-}
module Propellor.Types
( Host(..)
, Property
, Info
- , HasInfo
- , NoInfo
- , CInfo
, Desc
- , infoProperty
- , simpleProperty
+ , mkProperty
+ , MetaType(..)
+ , OS(..)
+ , UnixLike
+ , Debian
+ , Buntish
+ , FreeBSD
+ , HasInfo
+ , type (+)
+ , addInfoProperty
, adjustPropertySatisfy
, propertyInfo
, propertyDesc
, propertyChildren
, RevertableProperty(..)
- , MkRevertableProperty(..)
, IsProp(..)
, Combines(..)
, CombinedType
@@ -36,7 +42,6 @@ module Propellor.Types
, module Propellor.Types.Result
, module Propellor.Types.ZFS
, propertySatisfy
- , ignoreInfo
) where
import Data.Monoid
@@ -50,13 +55,14 @@ import Propellor.Types.Info
import Propellor.Types.OS
import Propellor.Types.Dns
import Propellor.Types.Result
+import Propellor.Types.MetaTypes
import Propellor.Types.ZFS
-- | Everything Propellor knows about a system: Its hostname,
-- properties and their collected info.
data Host = Host
{ hostName :: HostName
- , hostProperties :: [Property HasInfo]
+ , hostProperties :: [ChildProperty]
, hostInfo :: Info
}
deriving (Show, Typeable)
@@ -103,162 +109,154 @@ data EndAction = EndAction Desc (Result -> Propellor Result)
type Desc = String
-- | The core data type of Propellor, this represents a property
--- that the system should have, and an action to ensure it has the
--- property.
+-- that the system should have, with a descrition, an action to ensure
+-- it has the property, and perhaps some Info that can be added to Hosts
+-- that have the property.
--
--- A property can have associated `Info` or not. This is tracked at the
--- type level with Property `NoInfo` and Property `HasInfo`.
+-- A property has a list of `[MetaType]`, which is part of its type.
--
-- There are many instances and type families, which are mostly used
-- internally, so you needn't worry about them.
-data Property i where
- IProperty :: Desc -> Propellor Result -> Info -> [Property HasInfo] -> Property HasInfo
- SProperty :: Desc -> Propellor Result -> [Property NoInfo] -> Property NoInfo
-
--- | Indicates that a Property has associated Info.
-data HasInfo
--- | Indicates that a Property does not have Info.
-data NoInfo
-
--- | Type level calculation of the combination of HasInfo and/or NoInfo
-type family CInfo x y
-type instance CInfo HasInfo HasInfo = HasInfo
-type instance CInfo HasInfo NoInfo = HasInfo
-type instance CInfo NoInfo HasInfo = HasInfo
-type instance CInfo NoInfo NoInfo = NoInfo
-
--- | Constructs a Property with associated Info.
-infoProperty
- :: Desc -- ^ description of the property
- -> Propellor Result -- ^ action to run to satisfy the property (must be idempotent; may run repeatedly)
- -> Info -- ^ info associated with the property
- -> [Property i] -- ^ child properties
- -> Property HasInfo
-infoProperty d a i cs = IProperty d a i (map toIProperty cs)
-
--- | Constructs a Property with no Info.
-simpleProperty :: Desc -> Propellor Result -> [Property NoInfo] -> Property NoInfo
-simpleProperty = SProperty
-
-toIProperty :: Property i -> Property HasInfo
-toIProperty p@(IProperty {}) = p
-toIProperty (SProperty d s cs) = IProperty d s mempty (map toIProperty cs)
-
-toSProperty :: Property i -> Property NoInfo
-toSProperty (IProperty d s _ cs) = SProperty d s (map toSProperty cs)
-toSProperty p@(SProperty {}) = p
+data Property metatypes = Property metatypes Desc (Propellor Result) Info [ChildProperty]
+
+-- | Since there are many different types of Properties, they cannot be put
+-- into a list. The simplified ChildProperty can be put into a list.
+data ChildProperty = ChildProperty Desc (Propellor Result) Info [ChildProperty]
+
+instance Show ChildProperty where
+ show (ChildProperty desc _ _ _) = desc
+
+-- | Constructs a Property.
+--
+-- You can specify any metatypes that make sense to indicate what OS
+-- the property targets, etc.
+--
+-- For example:
+--
+-- > foo :: Property Debian
+-- > foo = mkProperty "foo" (...)
+--
+-- Note that using this needs LANGUAGE PolyKinds.
+mkProperty
+ :: SingI metatypes
+ => Desc
+ -> Propellor Result
+ -> Property (Sing metatypes)
+mkProperty d a = Property sing d a mempty mempty
+
+-- | Adds info to a Property.
+--
+-- The new Property will include HasInfo in its metatypes.
+addInfoProperty
+ :: (metatypes' ~ (+) HasInfo metatypes, SingI metatypes')
+ => Property metatypes
+ -> Info
+ -> Property (Sing metatypes')
+addInfoProperty (Property metatypes d a i c) newi = Property sing d a (i <> newi) c
+
+{-
-- | Makes a version of a Proprty without its Info.
-- Use with caution!
-ignoreInfo :: Property i -> Property NoInfo
-ignoreInfo = toSProperty
+ignoreInfo
+ :: (metatypes' ~
+ => Property metatypes
+ -> Property (Sing metatypes')
+ignoreInfo =
+
+-}
-- | Gets the action that can be run to satisfy a Property.
-- You should never run this action directly. Use
-- 'Propellor.Engine.ensureProperty` instead.
-propertySatisfy :: Property i -> Propellor Result
-propertySatisfy (IProperty _ a _ _) = a
-propertySatisfy (SProperty _ a _) = a
+propertySatisfy :: Property metatypes -> Propellor Result
+propertySatisfy (Property _ _ a _ _) = a
-- | Changes the action that is performed to satisfy a property.
-adjustPropertySatisfy :: Property i -> (Propellor Result -> Propellor Result) -> Property i
-adjustPropertySatisfy (IProperty d s i cs) f = IProperty d (f s) i cs
-adjustPropertySatisfy (SProperty d s cs) f = SProperty d (f s) cs
+adjustPropertySatisfy :: Property metatypes -> (Propellor Result -> Propellor Result) -> Property metatypes
+adjustPropertySatisfy (Property t d s i c) f = Property t d (f s) i c
-propertyInfo :: Property i -> Info
-propertyInfo (IProperty _ _ i _) = i
-propertyInfo (SProperty {}) = mempty
+propertyInfo :: Property metatypes -> Info
+propertyInfo (Property _ _ _ i _) = i
-propertyDesc :: Property i -> Desc
-propertyDesc (IProperty d _ _ _) = d
-propertyDesc (SProperty d _ _) = d
+propertyDesc :: Property metatypes -> Desc
+propertyDesc (Property _ d _ _ _) = d
-instance Show (Property i) where
+instance Show (Property metatypes) where
show p = "property " ++ show (propertyDesc p)
-- | A Property can include a list of child properties that it also
-- satisfies. This allows them to be introspected to collect their info, etc.
-propertyChildren :: Property i -> [Property i]
-propertyChildren (IProperty _ _ _ cs) = cs
-propertyChildren (SProperty _ _ cs) = cs
+propertyChildren :: Property metatypes -> [ChildProperty]
+propertyChildren (Property _ _ _ _ c) = c
-- | A property that can be reverted. The first Property is run
-- normally and the second is run when it's reverted.
-data RevertableProperty i = RevertableProperty
- { setupRevertableProperty :: Property i
- , undoRevertableProperty :: Property i
+data RevertableProperty setupmetatypes undometatypes = RevertableProperty
+ { setupRevertableProperty :: Property setupmetatypes
+ , undoRevertableProperty :: Property undometatypes
}
-instance Show (RevertableProperty i) where
+instance Show (RevertableProperty setupmetatypes undometatypes) where
show (RevertableProperty p _) = show p
-class MkRevertableProperty i1 i2 where
- -- | Shorthand to construct a revertable property.
- (<!>) :: Property i1 -> Property i2 -> RevertableProperty (CInfo i1 i2)
-
-instance MkRevertableProperty HasInfo HasInfo where
- x <!> y = RevertableProperty x y
-instance MkRevertableProperty NoInfo NoInfo where
- x <!> y = RevertableProperty x y
-instance MkRevertableProperty NoInfo HasInfo where
- x <!> y = RevertableProperty (toProp x) y
-instance MkRevertableProperty HasInfo NoInfo where
- x <!> y = RevertableProperty x (toProp y)
+-- | Shorthand to construct a revertable property from any two Properties.
+(<!>)
+ :: Property setupmetatypes
+ -> Property undometatypes
+ -> RevertableProperty setupmetatypes undometatypes
+setup <!> undo = RevertableProperty setup undo
-- | Class of types that can be used as properties of a host.
class IsProp p where
setDesc :: p -> Desc -> p
- toProp :: p -> Property HasInfo
+ -- toProp :: p -> Property HasInfo
getDesc :: p -> Desc
-- | Gets the info of the property, combined with all info
-- of all children properties.
getInfoRecursive :: p -> Info
-instance IsProp (Property HasInfo) where
- setDesc (IProperty _ a i cs) d = IProperty d a i cs
- toProp = id
+instance IsProp (Property metatypes) where
+ setDesc (Property t _ a i c) d = Property t d a i c
+ -- toProp = id
getDesc = propertyDesc
- getInfoRecursive (IProperty _ _ i cs) =
- i <> mconcat (map getInfoRecursive cs)
-instance IsProp (Property NoInfo) where
- setDesc (SProperty _ a cs) d = SProperty d a cs
- toProp = toIProperty
- getDesc = propertyDesc
- getInfoRecursive _ = mempty
+ getInfoRecursive (Property _ _ _ i c) =
+ i <> mconcat (map getInfoRecursive c)
+
+instance IsProp ChildProperty where
+ setDesc (ChildProperty _ a i c) d = ChildProperty d a i c
+ getDesc (ChildProperty d _ _ _) = d
+ getInfoRecursive (ChildProperty _ _ i c) =
+ i <> mconcat (map getInfoRecursive c)
-instance IsProp (RevertableProperty HasInfo) where
+instance IsProp (RevertableProperty setupmetatypes undometatypes) where
setDesc = setDescR
getDesc (RevertableProperty p1 _) = getDesc p1
- toProp (RevertableProperty p1 _) = p1
+ -- toProp (RevertableProperty p1 _) = p1
-- | Return the Info of the currently active side.
getInfoRecursive (RevertableProperty p1 _p2) = getInfoRecursive p1
-instance IsProp (RevertableProperty NoInfo) where
- setDesc = setDescR
- getDesc (RevertableProperty p1 _) = getDesc p1
- toProp (RevertableProperty p1 _) = toProp p1
- getInfoRecursive (RevertableProperty _ _) = mempty
-- | Sets the description of both sides.
-setDescR :: IsProp (Property i) => RevertableProperty i -> Desc -> RevertableProperty i
+setDescR :: IsProp (Property setupmetatypes) => RevertableProperty setupmetatypes undometatypes -> Desc -> RevertableProperty setupmetatypes undometatypes
setDescR (RevertableProperty p1 p2) d =
RevertableProperty (setDesc p1 d) (setDesc p2 ("not " ++ d))
-- | Type level calculation of the type that results from combining two
-- types of properties.
type family CombinedType x y
-type instance CombinedType (Property x) (Property y) = Property (CInfo x y)
-type instance CombinedType (RevertableProperty x) (RevertableProperty y) = RevertableProperty (CInfo x y)
+type instance CombinedType (Property (Sing x)) (Property (Sing y)) = Property (Sing (Union x y))
+type instance CombinedType (RevertableProperty (Sing x) (Sing x')) (RevertableProperty (Sing y) (Sing y')) = RevertableProperty (Sing (Union x y)) (Sing (Union x' y'))
-- When only one of the properties is revertable, the combined property is
-- not fully revertable, so is not a RevertableProperty.
-type instance CombinedType (RevertableProperty x) (Property y) = Property (CInfo x y)
-type instance CombinedType (Property x) (RevertableProperty y) = Property (CInfo x y)
+type instance CombinedType (RevertableProperty (Sing x) (Sing x')) (Property (Sing y)) = Property (Sing (Union x y))
+type instance CombinedType (Property (Sing x)) (RevertableProperty (Sing y) (Sing y')) = Property (Sing (Union x y))
type ResultCombiner = Propellor Result -> Propellor Result -> Propellor Result
class Combines x y where
-- | Combines together two properties, yielding a property that
- -- has the description and info of the first, and that has the second
- -- property as a child.
+ -- has the description and info of the first, and that has the
+ -- second property as a child property.
combineWith
:: ResultCombiner
-- ^ How to combine the actions to satisfy the properties.
@@ -269,73 +267,15 @@ class Combines x y where
-> y
-> CombinedType x y
-instance Combines (Property HasInfo) (Property HasInfo) where
- combineWith f _ (IProperty d1 a1 i1 cs1) y@(IProperty _d2 a2 _i2 _cs2) =
- IProperty d1 (f a1 a2) i1 (y : cs1)
-
-instance Combines (Property HasInfo) (Property NoInfo) where
- combineWith f _ (IProperty d1 a1 i1 cs1) y@(SProperty _d2 a2 _cs2) =
- IProperty d1 (f a1 a2) i1 (toIProperty y : cs1)
-
-instance Combines (Property NoInfo) (Property HasInfo) where
- combineWith f _ (SProperty d1 a1 cs1) y@(IProperty _d2 a2 _i2 _cs2) =
- IProperty d1 (f a1 a2) mempty (y : map toIProperty cs1)
-
-instance Combines (Property NoInfo) (Property NoInfo) where
- combineWith f _ (SProperty d1 a1 cs1) y@(SProperty _d2 a2 _cs2) =
- SProperty d1 (f a1 a2) (y : cs1)
-
-instance Combines (RevertableProperty NoInfo) (RevertableProperty NoInfo) where
- combineWith = combineWithRR
-instance Combines (RevertableProperty HasInfo) (RevertableProperty HasInfo) where
- combineWith = combineWithRR
-instance Combines (RevertableProperty HasInfo) (RevertableProperty NoInfo) where
- combineWith = combineWithRR
-instance Combines (RevertableProperty NoInfo) (RevertableProperty HasInfo) where
- combineWith = combineWithRR
-instance Combines (RevertableProperty NoInfo) (Property HasInfo) where
- combineWith = combineWithRP
-instance Combines (RevertableProperty NoInfo) (Property NoInfo) where
- combineWith = combineWithRP
-instance Combines (RevertableProperty HasInfo) (Property HasInfo) where
- combineWith = combineWithRP
-instance Combines (RevertableProperty HasInfo) (Property NoInfo) where
- combineWith = combineWithRP
-instance Combines (Property HasInfo) (RevertableProperty NoInfo) where
- combineWith = combineWithPR
-instance Combines (Property NoInfo) (RevertableProperty NoInfo) where
- combineWith = combineWithPR
-instance Combines (Property HasInfo) (RevertableProperty HasInfo) where
- combineWith = combineWithPR
-instance Combines (Property NoInfo) (RevertableProperty HasInfo) where
- combineWith = combineWithPR
-
-combineWithRR
- :: Combines (Property x) (Property y)
- => ResultCombiner
- -> ResultCombiner
- -> RevertableProperty x
- -> RevertableProperty y
- -> RevertableProperty (CInfo x y)
-combineWithRR sf tf (RevertableProperty s1 t1) (RevertableProperty s2 t2) =
- RevertableProperty
- (combineWith sf tf s1 s2)
- (combineWith tf sf t1 t2)
-
-combineWithRP
- :: Combines (Property i) y
- => (Propellor Result -> Propellor Result -> Propellor Result)
- -> (Propellor Result -> Propellor Result -> Propellor Result)
- -> RevertableProperty i
- -> y
- -> CombinedType (Property i) y
-combineWithRP sf tf (RevertableProperty x _) y = combineWith sf tf x y
-
-combineWithPR
- :: Combines x (Property i)
- => (Propellor Result -> Propellor Result -> Propellor Result)
- -> (Propellor Result -> Propellor Result -> Propellor Result)
- -> x
- -> RevertableProperty i
- -> CombinedType x (Property i)
-combineWithPR sf tf x (RevertableProperty y _) = combineWith sf tf x y
+instance (CombinedType (Property (Sing x)) (Property (Sing y)) ~ Property (Sing (Union x y)), SingI (Union x y)) => Combines (Property (Sing x)) (Property (Sing y)) where
+ combineWith f _ (Property t1 d1 a1 i1 c1) (Property _t2 d2 a2 i2 c2) =
+ Property sing d1 (f a1 a2) i1 (ChildProperty d2 a2 i2 c2 : c1)
+instance (CombinedType (RevertableProperty (Sing x) (Sing x')) (RevertableProperty (Sing y) (Sing y')) ~ RevertableProperty (Sing (Union x y)) (Sing (Union x' y')), SingI (Union x y), SingI (Union x' y')) => Combines (RevertableProperty (Sing x) (Sing x')) (RevertableProperty (Sing y) (Sing y')) where
+ combineWith sf tf (RevertableProperty s1 t1) (RevertableProperty s2 t2) =
+ RevertableProperty
+ (combineWith sf tf s1 s2)
+ (combineWith tf sf t1 t2)
+instance (CombinedType (RevertableProperty (Sing x) (Sing x')) (Property (Sing y)) ~ Property (Sing (Union x y)), SingI (Union x y)) => Combines (RevertableProperty (Sing x) (Sing x')) (Property (Sing y)) where
+ combineWith sf tf (RevertableProperty x _) y = combineWith sf tf x y
+instance (CombinedType (Property (Sing x)) (RevertableProperty (Sing y) (Sing y')) ~ Property (Sing (Union x y)), SingI (Union x y)) => Combines (Property (Sing x)) (RevertableProperty (Sing y) (Sing y')) where
+ combineWith sf tf x (RevertableProperty y _) = combineWith sf tf x y
diff --git a/src/Propellor/Types/MetaTypes.hs b/src/Propellor/Types/MetaTypes.hs
new file mode 100644
index 00000000..b6d72dcd
--- /dev/null
+++ b/src/Propellor/Types/MetaTypes.hs
@@ -0,0 +1,276 @@
+{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, TypeFamilies, UndecidableInstances, FlexibleInstances, GADTs #-}
+
+module Propellor.Types.MetaTypes (
+ MetaType(..),
+ OS(..),
+ UnixLike,
+ Debian,
+ Buntish,
+ FreeBSD,
+ HasInfo,
+ type (+),
+ OuterMetaTypes,
+ ensureProperty,
+ tightenTargets,
+ pickOS,
+ Sing,
+ sing,
+ SingI,
+ Union,
+) where
+
+----- DEMO ----------
+
+foo :: Property (HasInfo + FreeBSD)
+foo = mkProperty' $ \t -> do
+ ensureProperty t jail
+
+bar :: Property (Debian + FreeBSD)
+bar = aptinstall `pickOS` jail
+
+aptinstall :: Property Debian
+aptinstall = mkProperty $ do
+ return ()
+
+jail :: Property FreeBSD
+jail = mkProperty $ do
+ return ()
+
+----- END DEMO ----------
+
+data Property metatypes = Property metatypes (IO ())
+
+mkProperty :: SingI l => IO () -> Property (Sing l)
+mkProperty = mkProperty' . const
+
+mkProperty' :: SingI l => (OuterMetaTypes l -> IO ()) -> Property (Sing l)
+mkProperty' a =
+ let p = Property sing (a (outerMetaTypes p))
+ in p
+
+data MetaType
+ = Targeting OS -- ^ A target OS of a Property
+ | WithInfo -- ^ Indicates that a Property has associated Info
+
+data OS
+ = OSDebian
+ | OSBuntish -- ^ A well-known Debian derivative founded by a space tourist. The actual name of this distribution is not used in Propellor per <http://joeyh.name/blog/entry/trademark_nonsense/>
+ | OSFreeBSD
+ deriving (Show, Eq)
+
+-- | Any unix-like system
+type UnixLike = Sing '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish, 'Targeting 'OSFreeBSD ]
+type Debian = Sing '[ 'Targeting 'OSDebian ]
+type Buntish = Sing '[ 'Targeting 'OSBuntish ]
+type FreeBSD = Sing '[ 'Targeting 'OSFreeBSD ]
+
+-- | Used to indicate that a Property adds Info to the Host where it's used.
+type HasInfo = Sing '[ 'WithInfo ]
+
+-- | 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
+ OSDebianS :: Sing ('Targeting 'OSDebian)
+ OSBuntishS :: Sing ('Targeting 'OSBuntish)
+ OSFreeBSDS :: Sing ('Targeting 'OSFreeBSD)
+ WithInfoS :: Sing 'WithInfo
+instance SingI ('Targeting 'OSDebian) where sing = OSDebianS
+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 `Sing` lists.
+--
+-- For example:
+--
+-- > HasInfo + Debian
+--
+-- Which is shorthand for this type:
+--
+-- > Sing '[WithInfo, Targeting OSDebian]
+type family a + b :: ab
+type instance (Sing a) + (Sing b) = Sing (Concat a b)
+
+type family Concat (list1 :: [a]) (list2 :: [a]) :: [a]
+type instance Concat '[] bs = bs
+type instance Concat (a ': as) bs = a ': (Concat as bs)
+
+newtype OuterMetaTypes l = OuterMetaTypes (Sing l)
+
+outerMetaTypes :: Property (Sing l) -> OuterMetaTypes l
+outerMetaTypes (Property metatypes _) = OuterMetaTypes metatypes
+
+-- | Use `mkProperty''` to get the `OuterMetaTypes`. For example:
+--
+-- > foo = Property Debian
+-- > foo = mkProperty' $ \t -> do
+-- > ensureProperty t (aptInstall "foo")
+--
+-- The type checker will prevent using ensureProperty with a property
+-- that does not support the target OSes needed by the OuterMetaTypes.
+-- In the example above, aptInstall must support Debian.
+--
+-- The type checker will also prevent using ensureProperty with a property
+-- with HasInfo in its MetaTypes. Doing so would cause the info associated
+-- with the property to be lost.
+ensureProperty
+ ::
+ ( (Targets inner `NotSuperset` Targets outer) ~ 'CanCombineTargets
+ , CannotUseEnsurePropertyWithInfo inner ~ 'True
+ )
+ => OuterMetaTypes outer
+ -> Property (Sing inner)
+ -> IO ()
+ensureProperty (OuterMetaTypes outermetatypes) (Property innermetatypes a) = a
+
+-- The name of this was chosen to make type errors a more understandable.
+type family CannotUseEnsurePropertyWithInfo (l :: [a]) :: Bool
+type instance CannotUseEnsurePropertyWithInfo '[] = 'True
+type instance CannotUseEnsurePropertyWithInfo (t ': ts) = Not (t `EqT` 'WithInfo) && CannotUseEnsurePropertyWithInfo ts
+
+-- | Tightens the MetaType list of a Property, to contain fewer targets.
+--
+-- Anything else in the MetaType list is passed through unchanged.
+tightenTargets
+ ::
+ ( combined ~ Concat (NonTargets old) (Intersect (Targets old) (Targets new))
+ , CannotCombineTargets old new combined ~ 'CanCombineTargets
+ , SingI combined
+ )
+ => Sing new
+ -> Property (Sing old)
+ -> Property (Sing combined)
+tightenTargets _ (Property old a) = Property sing a
+
+-- | Picks one of the two input properties to use,
+-- depending on the targeted OS.
+--
+-- If both input properties support the targeted OS, then the
+-- first will be used.
+pickOS
+ ::
+ ( combined ~ Union a b
+ , SingI combined
+ )
+ => Property (Sing a)
+ -> Property (Sing b)
+ -> Property (Sing combined)
+pickOS a@(Property ta ioa) b@(Property tb iob) = Property sing io
+ where
+ -- TODO pick with of ioa or iob to use based on final OS of
+ -- system being run on.
+ io = undefined
+
+data CheckCombineTargets = CannotCombineTargets | CanCombineTargets
+
+-- | Detect intersection of two lists that don't have any common targets.
+--
+-- The name of this was chosen to make type errors a more understandable.
+type family CannotCombineTargets (list1 :: [a]) (list2 :: [a]) (listr :: [a]) :: CheckCombineTargets
+type instance CannotCombineTargets l1 l2 '[] = 'CannotCombineTargets
+type instance CannotCombineTargets l1 l2 (a ': rest) = 'CanCombineTargets
+
+-- | Every item in the subset must be in the superset.
+--
+-- The name of this was chosen to make type errors a more understandable.
+type family NotSuperset (superset :: [a]) (subset :: [a]) :: CheckCombineTargets
+type instance NotSuperset superset '[] = 'CanCombineTargets
+type instance NotSuperset superset (s ': rest) =
+ If (Elem s superset)
+ (NotSuperset superset rest)
+ 'CannotCombineTargets
+
+type family IsTarget (a :: t) :: Bool
+type instance IsTarget ('Targeting a) = 'True
+type instance IsTarget 'WithInfo = 'False
+
+type family Targets (l :: [a]) :: [a]
+type instance Targets '[] = '[]
+type instance Targets (x ': xs) =
+ If (IsTarget x)
+ (x ': Targets xs)
+ (Targets xs)
+
+type family NonTargets (l :: [a]) :: [a]
+type instance NonTargets '[] = '[]
+type instance NonTargets (x ': xs) =
+ If (IsTarget x)
+ (Targets xs)
+ (x ': Targets xs)
+
+-- | Type level elem
+type family Elem (a :: t) (list :: [t]) :: Bool
+type instance Elem a '[] = 'False
+type instance Elem a (b ': bs) = EqT a b || Elem a bs
+
+-- | Type level union.
+type family Union (list1 :: [a]) (list2 :: [a]) :: [a]
+type instance Union '[] list2 = list2
+type instance Union (a ': rest) list2 =
+ If (Elem a list2 || Elem a rest)
+ (Union rest list2)
+ (a ': Union rest list2)
+
+-- | Type level intersection. Duplicate list items are eliminated.
+type family Intersect (list1 :: [a]) (list2 :: [a]) :: [a]
+type instance Intersect '[] list2 = '[]
+type instance Intersect (a ': rest) list2 =
+ If (Elem a list2 && Not (Elem a rest))
+ (a ': Intersect rest list2)
+ (Intersect rest list2)
+
+-- | Type level equality
+--
+-- This is a very clumsy implmentation, but it works back to ghc 7.6.
+type family EqT (a :: t) (b :: t) :: Bool
+type instance EqT ('Targeting a) ('Targeting b) = EqT a b
+type instance EqT 'WithInfo 'WithInfo = 'True
+type instance EqT 'WithInfo ('Targeting b) = 'False
+type instance EqT ('Targeting a) 'WithInfo = 'False
+type instance EqT 'OSDebian 'OSDebian = 'True
+type instance EqT 'OSBuntish 'OSBuntish = 'True
+type instance EqT 'OSFreeBSD 'OSFreeBSD = 'True
+type instance EqT 'OSDebian 'OSBuntish = 'False
+type instance EqT 'OSDebian 'OSFreeBSD = 'False
+type instance EqT 'OSBuntish 'OSDebian = 'False
+type instance EqT 'OSBuntish 'OSFreeBSD = 'False
+type instance EqT 'OSFreeBSD 'OSDebian = 'False
+type instance EqT 'OSFreeBSD 'OSBuntish = 'False
+-- More modern version if the combinatiorial explosion gets too bad later:
+--
+-- type family Eq (a :: MetaType) (b :: MetaType) where
+-- Eq a a = True
+-- Eq a b = False
+
+-- | An equivilant to the following is in Data.Type.Bool in
+-- modern versions of ghc, but is included here to support ghc 7.6.
+type family If (cond :: Bool) (tru :: a) (fls :: a) :: a
+type instance If 'True tru fls = tru
+type instance If 'False tru fls = fls
+type family (a :: Bool) || (b :: Bool) :: Bool
+type instance 'False || 'False = 'False
+type instance 'True || 'True = 'True
+type instance 'True || 'False = 'True
+type instance 'False || 'True = 'True
+type family (a :: Bool) && (b :: Bool) :: Bool
+type instance 'False && 'False = 'False
+type instance 'True && 'True = 'True
+type instance 'True && 'False = 'False
+type instance 'False && 'True = 'False
+type family Not (a :: Bool) :: Bool
+type instance Not 'False = 'True
+type instance Not 'True = 'False
+
diff --git a/src/Propellor/Types/OS.hs b/src/Propellor/Types/OS.hs
index a1ba14d4..94a37936 100644
--- a/src/Propellor/Types/OS.hs
+++ b/src/Propellor/Types/OS.hs
@@ -28,7 +28,7 @@ data System = System Distribution Architecture
data Distribution
= Debian DebianSuite
- | Buntish Release -- ^ A well-known Debian derivative founded by a space tourist. The actual name of this distribution is not used in Propellor per <http://joeyh.name/blog/entry/trademark_nonsense/>)
+ | Buntish Release -- ^ A well-known Debian derivative founded by a space tourist. The actual name of this distribution is not used in Propellor per <http://joeyh.name/blog/entry/trademark_nonsense/>
| FreeBSD FreeBSDRelease
deriving (Show, Eq)