summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--debian/changelog7
-rw-r--r--src/Propellor/EnsureProperty.hs8
-rw-r--r--src/Propellor/PropAccum.hs6
-rw-r--r--src/Propellor/Types.hs20
-rw-r--r--src/Propellor/Types/MetaTypes.hs195
5 files changed, 103 insertions, 133 deletions
diff --git a/debian/changelog b/debian/changelog
index ae97e9db..bf4df720 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,10 @@
+propellor (5.4.1) UNRELEASED; urgency=medium
+
+ * Modernized and simplified the MetaTypes implementation now that
+ compatability with ghc 7 is no longer needed.
+
+ -- Joey Hess <id@joeyh.name> Fri, 18 May 2018 10:25:05 -0400
+
propellor (5.4.0) unstable; urgency=medium
[ Sean Whitton ]
diff --git a/src/Propellor/EnsureProperty.hs b/src/Propellor/EnsureProperty.hs
index 5a07107c..6c720e2b 100644
--- a/src/Propellor/EnsureProperty.hs
+++ b/src/Propellor/EnsureProperty.hs
@@ -50,10 +50,10 @@ ensureProperty
ensureProperty _ = maybe (return NoChange) catchPropellor . getSatisfy
-- The name of this was chosen to make type errors a bit more understandable.
-type family Cannot_ensureProperty_WithInfo (l :: [a]) :: Bool
-type instance Cannot_ensureProperty_WithInfo '[] = 'True
-type instance Cannot_ensureProperty_WithInfo (t ': ts) =
- Not (t `EqT` 'WithInfo) && Cannot_ensureProperty_WithInfo ts
+type family Cannot_ensureProperty_WithInfo (l :: [a]) :: Bool where
+ Cannot_ensureProperty_WithInfo '[] = 'True
+ Cannot_ensureProperty_WithInfo (t ': ts) =
+ Not (t `EqT` 'WithInfo) && Cannot_ensureProperty_WithInfo ts
-- | Constructs a property, like `property`, but provides its
-- `OuterMetaTypesWitness`.
diff --git a/src/Propellor/PropAccum.hs b/src/Propellor/PropAccum.hs
index 5d1d3afb..c60ced73 100644
--- a/src/Propellor/PropAccum.hs
+++ b/src/Propellor/PropAccum.hs
@@ -41,9 +41,9 @@ infixl 1 &
infixl 1 &^
infixl 1 !
-type family GetMetaTypes x
-type instance GetMetaTypes (Property (MetaTypes t)) = MetaTypes t
-type instance GetMetaTypes (RevertableProperty (MetaTypes t) undo) = MetaTypes t
+type family GetMetaTypes x where
+ GetMetaTypes (Property (MetaTypes t)) = MetaTypes t
+ GetMetaTypes (RevertableProperty (MetaTypes t) undo) = MetaTypes t
-- | Adds a property to a Props.
--
diff --git a/src/Propellor/Types.hs b/src/Propellor/Types.hs
index 7cbe9f13..e10e0f5b 100644
--- a/src/Propellor/Types.hs
+++ b/src/Propellor/Types.hs
@@ -154,13 +154,19 @@ instance IsProp (RevertableProperty setupmetatypes undometatypes) where
-- | Type level calculation of the type that results from combining two
-- types of properties.
-type family CombinedType x y
-type instance CombinedType (Property (MetaTypes x)) (Property (MetaTypes y)) = Property (MetaTypes (Combine x y))
-type instance CombinedType (RevertableProperty (MetaTypes x) (MetaTypes x')) (RevertableProperty (MetaTypes y) (MetaTypes y')) = RevertableProperty (MetaTypes (Combine x y)) (MetaTypes (Combine 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 (MetaTypes x) (MetaTypes x')) (Property (MetaTypes y)) = Property (MetaTypes (Combine x y))
-type instance CombinedType (Property (MetaTypes x)) (RevertableProperty (MetaTypes y) (MetaTypes y')) = Property (MetaTypes (Combine x y))
+type family CombinedType x y where
+ CombinedType (Property (MetaTypes x)) (Property (MetaTypes y)) =
+ Property (MetaTypes (Combine x y))
+ CombinedType
+ (RevertableProperty (MetaTypes x) (MetaTypes x'))
+ (RevertableProperty (MetaTypes y) (MetaTypes y')) =
+ RevertableProperty (MetaTypes (Combine x y)) (MetaTypes (Combine x' y'))
+ -- When only one of the properties is revertable, the combined
+ -- property is not fully revertable, so is not a RevertableProperty.
+ CombinedType (RevertableProperty (MetaTypes x) (MetaTypes x')) (Property (MetaTypes y)) =
+ Property (MetaTypes (Combine x y))
+ CombinedType (Property (MetaTypes x)) (RevertableProperty (MetaTypes y) (MetaTypes y')) =
+ Property (MetaTypes (Combine x y))
type ResultCombiner = Maybe (Propellor Result) -> Maybe (Propellor Result) -> Maybe (Propellor Result)
diff --git a/src/Propellor/Types/MetaTypes.hs b/src/Propellor/Types/MetaTypes.hs
index 4e4472eb..0c476e87 100644
--- a/src/Propellor/Types/MetaTypes.hs
+++ b/src/Propellor/Types/MetaTypes.hs
@@ -30,6 +30,8 @@ module Propellor.Types.MetaTypes (
import Propellor.Types.Singletons
import Propellor.Types.OS
+import Data.Type.Bool
+
data MetaType
= Targeting TargetOS -- ^ A target OS of a Property
| WithInfo -- ^ Indicates that a Property has associated Info
@@ -60,8 +62,8 @@ type ArchLinux = MetaTypes '[ 'Targeting 'OSArchLinux ]
-- | Used to indicate that a Property adds Info to the Host where it's used.
type HasInfo = MetaTypes '[ 'WithInfo ]
-type family IncludesInfo t :: Bool
-type instance IncludesInfo (MetaTypes l) = Elem 'WithInfo l
+type family IncludesInfo t :: Bool where
+ IncludesInfo (MetaTypes l) = Elem 'WithInfo l
type MetaTypes = Sing
@@ -95,21 +97,21 @@ instance SingKind ('KProxy :: KProxy MetaType) where
-- Which is shorthand for this type:
--
-- > MetaTypes '[WithInfo, Targeting OSDebian]
-type family a + b :: ab
-type instance (MetaTypes a) + (MetaTypes b) = MetaTypes (Concat a b)
+type family a + b :: * where
+ (MetaTypes a) + (MetaTypes b) = MetaTypes (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)
+type family Concat (list1 :: [a]) (list2 :: [a]) :: [a] where
+ Concat '[] bs = bs
+ Concat (a ': as) bs = a ': (Concat as bs)
-- | Combine two MetaTypes lists, yielding a list
-- that has targets present in both, and nontargets present in either.
-type family Combine (list1 :: [a]) (list2 :: [a]) :: [a]
-type instance Combine (list1 :: [a]) (list2 :: [a]) =
- (Concat
- (NonTargets list1 `Union` NonTargets list2)
- (Targets list1 `Intersect` Targets list2)
- )
+type family Combine (list1 :: [a]) (list2 :: [a]) :: [a] where
+ Combine (list1 :: [a]) (list2 :: [a]) =
+ (Concat
+ (NonTargets list1 `Union` NonTargets list2)
+ (Targets list1 `Intersect` Targets list2)
+ )
-- | Checks if two MetaTypes lists can be safely combined.
--
@@ -117,121 +119,76 @@ type instance Combine (list1 :: [a]) (list2 :: [a]) =
-- constraint. For example:
--
-- > foo :: (CheckCombinable x y ~ 'CanCombine) => x -> y -> Combine x y
-type family CheckCombinable (list1 :: [a]) (list2 :: [a]) :: CheckCombine
--- As a special case, if either list is empty, let it be combined with the
--- other. This relies on MetaTypes list always containing at least
--- one target, so can only happen if there's already been a type error.
--- This special case lets the type checker show only the original type
--- error, and not an extra error due to a later CheckCombinable constraint.
-type instance CheckCombinable '[] list2 = 'CanCombine
-type instance CheckCombinable list1 '[] = 'CanCombine
-type instance CheckCombinable (l1 ': list1) (l2 ': list2) =
- CheckCombinable' (Combine (l1 ': list1) (l2 ': list2))
-type family CheckCombinable' (combinedlist :: [a]) :: CheckCombine
-type instance CheckCombinable' '[] = 'CannotCombineTargets
-type instance CheckCombinable' (a ': rest)
- = If (IsTarget a)
- 'CanCombine
- (CheckCombinable' rest)
+type family CheckCombinable (list1 :: [a]) (list2 :: [a]) :: CheckCombine where
+ -- As a special case, if either list is empty, let it be combined
+ -- with the other. This relies on MetaTypes list always containing
+ -- at least one target, so can only happen if there's already been
+ -- a type error. This special case lets the type checker show only
+ -- the original type error, and not an extra error due to a later
+ -- CheckCombinable constraint.
+ CheckCombinable '[] list2 = 'CanCombine
+ CheckCombinable list1 '[] = 'CanCombine
+ CheckCombinable (l1 ': list1) (l2 ': list2) =
+ CheckCombinable' (Combine (l1 ': list1) (l2 ': list2))
+type family CheckCombinable' (combinedlist :: [a]) :: CheckCombine where
+ CheckCombinable' '[] = 'CannotCombineTargets
+ CheckCombinable' (a ': rest)
+ = If (IsTarget a)
+ 'CanCombine
+ (CheckCombinable' rest)
data CheckCombine = CannotCombineTargets | CanCombine
-- | Every item in the subset must be in the superset.
--
-- The name of this was chosen to make type errors more understandable.
-type family NotSuperset (superset :: [a]) (subset :: [a]) :: CheckCombine
-type instance NotSuperset superset '[] = 'CanCombine
-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)
- (NonTargets xs)
- (x ': NonTargets xs)
+type family NotSuperset (superset :: [a]) (subset :: [a]) :: CheckCombine where
+ NotSuperset superset '[] = 'CanCombine
+ NotSuperset superset (s ': rest) =
+ If (Elem s superset)
+ (NotSuperset superset rest)
+ 'CannotCombineTargets
+
+type family IsTarget (a :: t) :: Bool where
+ IsTarget ('Targeting a) = 'True
+ IsTarget 'WithInfo = 'False
+
+type family Targets (l :: [a]) :: [a] where
+ Targets '[] = '[]
+ Targets (x ': xs) =
+ If (IsTarget x)
+ (x ': Targets xs)
+ (Targets xs)
+
+type family NonTargets (l :: [a]) :: [a] where
+ NonTargets '[] = '[]
+ NonTargets (x ': xs) =
+ If (IsTarget x)
+ (NonTargets xs)
+ (x ': NonTargets 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 family Elem (a :: t) (list :: [t]) :: Bool where
+ Elem a '[] = 'False
+ 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 family Union (list1 :: [a]) (list2 :: [a]) :: [a] where
+ Union '[] list2 = list2
+ 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
-type instance EqT 'OSArchLinux 'OSArchLinux = 'True
-type instance EqT 'OSArchLinux 'OSDebian = 'False
-type instance EqT 'OSArchLinux 'OSBuntish = 'False
-type instance EqT 'OSArchLinux 'OSFreeBSD = 'False
-type instance EqT 'OSDebian 'OSArchLinux = 'False
-type instance EqT 'OSBuntish 'OSArchLinux = 'False
-type instance EqT 'OSFreeBSD 'OSArchLinux = '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
-
+type family Intersect (list1 :: [a]) (list2 :: [a]) :: [a] where
+ Intersect '[] list2 = '[]
+ Intersect (a ': rest) list2 =
+ If (Elem a list2 && Not (Elem a rest))
+ (a ': Intersect rest list2)
+ (Intersect rest list2)
+
+-- | Type level equality of metatypes.
+type family EqT (a :: MetaType) (b :: MetaType) where
+ EqT a a = 'True
+ EqT a b = 'False