From a7560c9677485dbecd7283aedf977c4653cfacb4 Mon Sep 17 00:00:00 2001 From: Joey Hess Date: Fri, 25 Mar 2016 13:10:33 -0400 Subject: fix CheckCombinable Was wrong when there was a non-target in the MetaTypes list. Also, rework to improve type checker errors. --- src/Propellor/EnsureProperty.hs | 2 +- src/Propellor/Types.hs | 8 +++---- src/Propellor/Types/MetaTypes.hs | 51 ++++++++++++++++++++++++---------------- 3 files changed, 36 insertions(+), 25 deletions(-) (limited to 'src') 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) -- cgit v1.2.3