summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorJoey Hess2016-03-25 13:10:33 -0400
committerJoey Hess2016-03-25 13:11:26 -0400
commita7560c9677485dbecd7283aedf977c4653cfacb4 (patch)
tree43774f4dc22be843e090566c9d3aabe490f76c93 /src
parentde3a9a722847685b267ce396166de9245cd0d566 (diff)
fix CheckCombinable
Was wrong when there was a non-target in the MetaTypes list. Also, rework to improve type checker errors.
Diffstat (limited to 'src')
-rw-r--r--src/Propellor/EnsureProperty.hs2
-rw-r--r--src/Propellor/Types.hs8
-rw-r--r--src/Propellor/Types/MetaTypes.hs51
3 files changed, 36 insertions, 25 deletions
diff --git a/src/Propellor/EnsureProperty.hs b/src/Propellor/EnsureProperty.hs
index f3e79ae5..f42003c0 100644
--- a/src/Propellor/EnsureProperty.hs
+++ b/src/Propellor/EnsureProperty.hs
@@ -33,7 +33,7 @@ import Propellor.Exception
-- with the property to be lost.
ensureProperty
::
- ( (Targets inner `NotSuperset` Targets outer) ~ 'CanCombineTargets
+ ( (Targets inner `NotSuperset` Targets outer) ~ 'CanCombine
, CannotUse_ensureProperty_WithInfo inner ~ 'True
)
=> OuterMetaTypes outer
diff --git a/src/Propellor/Types.hs b/src/Propellor/Types.hs
index 23716e58..42c12492 100644
--- a/src/Propellor/Types.hs
+++ b/src/Propellor/Types.hs
@@ -269,15 +269,15 @@ class Combines x y where
-> y
-> CombinedType x y
-instance (CannotCombineTargets x y (Combine x y) ~ 'CanCombineTargets, SingI (Combine x y)) => Combines (Property (MetaTypes x)) (Property (MetaTypes y)) where
+instance (CheckCombinable x y ~ 'CanCombine, SingI (Combine x y)) => Combines (Property (MetaTypes x)) (Property (MetaTypes y)) where
combineWith f _ (Property _ d1 a1 i1 c1) (Property _ d2 a2 i2 c2) =
Property sing d1 (f a1 a2) i1 (ChildProperty d2 a2 i2 c2 : c1)
-instance (CannotCombineTargets x y (Combine x y) ~ 'CanCombineTargets, CannotCombineTargets x' y' (Combine x' y') ~ 'CanCombineTargets, SingI (Combine x y), SingI (Combine x' y')) => Combines (RevertableProperty (MetaTypes x) (MetaTypes x')) (RevertableProperty (MetaTypes y) (MetaTypes y')) where
+instance (CheckCombinable x y ~ 'CanCombine, CheckCombinable x' y' ~ 'CanCombine, SingI (Combine x y), SingI (Combine x' y')) => Combines (RevertableProperty (MetaTypes x) (MetaTypes x')) (RevertableProperty (MetaTypes y) (MetaTypes y')) where
combineWith sf tf (RevertableProperty s1 t1) (RevertableProperty s2 t2) =
RevertableProperty
(combineWith sf tf s1 s2)
(combineWith tf sf t1 t2)
-instance (CannotCombineTargets x y (Combine x y) ~ 'CanCombineTargets, SingI (Combine x y)) => Combines (RevertableProperty (MetaTypes x) (MetaTypes x')) (Property (MetaTypes y)) where
+instance (CheckCombinable x y ~ 'CanCombine, SingI (Combine x y)) => Combines (RevertableProperty (MetaTypes x) (MetaTypes x')) (Property (MetaTypes y)) where
combineWith sf tf (RevertableProperty x _) y = combineWith sf tf x y
-instance (CannotCombineTargets x y (Combine x y) ~ 'CanCombineTargets, SingI (Combine x y)) => Combines (Property (MetaTypes x)) (RevertableProperty (MetaTypes y) (MetaTypes y')) where
+instance (CheckCombinable x y ~ 'CanCombine, SingI (Combine x y)) => Combines (Property (MetaTypes x)) (RevertableProperty (MetaTypes y) (MetaTypes 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
index 4006914e..80fa454e 100644
--- a/src/Propellor/Types/MetaTypes.hs
+++ b/src/Propellor/Types/MetaTypes.hs
@@ -17,9 +17,9 @@ module Propellor.Types.MetaTypes (
Targets,
NonTargets,
NotSuperset,
- CheckCombineTargets(..),
Combine,
- CannotCombineTargets,
+ CheckCombine(..),
+ CheckCombinable,
type (&&),
Not,
EqT,
@@ -46,6 +46,9 @@ type DebianLike = Debian + Buntish
-- | 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 MetaTypes = Sing
-- | The data family of singleton types.
@@ -98,28 +101,36 @@ type instance Combine (list1 :: [a]) (list2 :: [a]) =
(Targets list1 `Intersect` Targets list2)
)
-type family IncludesInfo t :: Bool
-type instance IncludesInfo (MetaTypes l) = Elem 'WithInfo l
-
--- 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
-
--- | 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
-
-data CheckCombineTargets = CannotCombineTargets | CanCombineTargets
+-- | Checks if two MetaTypes lists can be safely combined.
+--
+-- This should be used anywhere Combine is used, as an additional
+-- 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)
+
+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]) :: CheckCombineTargets
-type instance NotSuperset superset '[] = 'CanCombineTargets
+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)