summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJoey Hess2018-05-18 10:31:18 -0400
committerJoey Hess2018-05-18 10:40:13 -0400
commit13beb3a02e5c59eb8c2c481f79535fb4469392d3 (patch)
treef7d516cdfdf4dd25291685461a38af718e37ea77
parentf4ac700c77869ed017fc85dc86984a3c72d3440a (diff)
modernized and simplified the MetaTypes implementation
now that compatability with ghc 7 is no longer needed. Data.Type.Bool contains effectively the same stuff that was implemented here, so removed my code. Tried to use Data.Type.Equality instead of my EqT, but it seems to be some other type of (type level) equality, and didn't compile. Instead went with the simpler EqT implementation that newer ghc versions allow. The rest of the changes are simply better syntax for defining type families. And upon using that syntax, ghc noticed that `type family a + b` does not have kind "ab" like I wrote before, but is kind *. Tested on debian stable with ghc 8.0.1. This commit was sponsored by John Pellman on Patreon.
-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