summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorJoey Hess2019-07-01 15:49:20 -0400
committerJoey Hess2019-07-01 16:20:51 -0400
commit14f6ae30809d8bbdb10b91cc59757e865a365df8 (patch)
treebe688e4685f05d6426cf30b0e0eff5a25cf003ee /src
parent70e71629b370349914e9fc89956a6756783296b0 (diff)
custom type error messages
* Avoid displaying an excessive amount of type error messages when many properties have been combined in a props list. * Added custom type error messages when Properties don't combine due to conflicting metatypes. * Added custom type error messages for ensureProperty and tightenTargets. * ensureProperty: The constraints have been simplified to EnsurePropertyAllowed. (API change) * ensureProperty: The contraints have been simplified to TightenTargetsAllowed. (API change) * CheckCombinable generates a Bool. (API change) This commit was sponsored by Jake Vosloo on Patreon.
Diffstat (limited to 'src')
-rw-r--r--src/Propellor/EnsureProperty.hs34
-rw-r--r--src/Propellor/PropAccum.hs17
-rw-r--r--src/Propellor/Property/Atomic.hs12
-rw-r--r--src/Propellor/Types.hs29
-rw-r--r--src/Propellor/Types/MetaTypes.hs124
5 files changed, 152 insertions, 64 deletions
diff --git a/src/Propellor/EnsureProperty.hs b/src/Propellor/EnsureProperty.hs
index ab624706..01203d04 100644
--- a/src/Propellor/EnsureProperty.hs
+++ b/src/Propellor/EnsureProperty.hs
@@ -8,7 +8,7 @@ module Propellor.EnsureProperty
( ensureProperty
, property'
, OuterMetaTypesWitness
- , Cannot_ensureProperty_WithInfo
+ , EnsurePropertyAllowed
) where
import Propellor.Types
@@ -16,6 +16,8 @@ import Propellor.Types.Core
import Propellor.Types.MetaTypes
import Propellor.Exception
+import GHC.TypeLits
+import Data.Type.Bool
import Data.Monoid
import Prelude
@@ -41,19 +43,33 @@ ensureProperty
-- -Wredundant-constraints is turned off because
-- this constraint appears redundant, but is actually
-- crucial.
- ( Cannot_ensureProperty_WithInfo inner ~ 'True
- , (Targets inner `NotSuperset` Targets outer) ~ 'CanCombine
- )
+ ( EnsurePropertyAllowed inner outer ~ 'True)
=> OuterMetaTypesWitness outer
-> Property (MetaTypes inner)
-> Propellor Result
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 where
- Cannot_ensureProperty_WithInfo '[] = 'True
- Cannot_ensureProperty_WithInfo (t ': ts) =
- Not (t `EqT` 'WithInfo) && Cannot_ensureProperty_WithInfo ts
+type family EnsurePropertyAllowed inner outer where
+ EnsurePropertyAllowed inner outer =
+ (EnsurePropertyNoInfo inner)
+ &&
+ (EnsurePropertyTargetOSMatches inner outer)
+
+type family EnsurePropertyNoInfo (l :: [a]) :: Bool where
+ EnsurePropertyNoInfo '[] = 'True
+ EnsurePropertyNoInfo (t ': ts) = If (Not (t `EqT` 'WithInfo))
+ (EnsurePropertyNoInfo ts)
+ (TypeError ('Text "Cannot use ensureProperty with a Property that HasInfo."))
+
+type family EnsurePropertyTargetOSMatches inner outer where
+ EnsurePropertyTargetOSMatches inner outer =
+ If (Targets outer `IsSubset` Targets inner)
+ 'True
+ ( TypeError
+ ( 'Text "ensureProperty inner Property is missing support for: "
+ ':$$: PrettyPrintMetaTypes (Difference (Targets outer) (Targets inner))
+ )
+ )
-- | Constructs a property, like `property`, but provides its
-- `OuterMetaTypesWitness`.
diff --git a/src/Propellor/PropAccum.hs b/src/Propellor/PropAccum.hs
index c60ced73..3fc83202 100644
--- a/src/Propellor/PropAccum.hs
+++ b/src/Propellor/PropAccum.hs
@@ -19,6 +19,7 @@ import Propellor.Types.MetaTypes
import Propellor.Types.Core
import Propellor.Property
+import GHC.TypeLits
import Data.Monoid
import Prelude
@@ -45,6 +46,16 @@ type family GetMetaTypes x where
GetMetaTypes (Property (MetaTypes t)) = MetaTypes t
GetMetaTypes (RevertableProperty (MetaTypes t) undo) = MetaTypes t
+-- When many properties are combined, ghc error message
+-- can include quite a lot of code, typically starting with
+-- `props and including all the properties up to and including the
+-- one that fails to combine. Point the user in the right direction.
+type family NoteFor symbol :: ErrorMessage where
+ NoteFor symbol =
+ 'Text "Probably the problem is with the last property added with "
+ ':<>: symbol
+ ':<>: 'Text " in the code excerpt below."
+
-- | Adds a property to a Props.
--
-- Can add Properties and RevertableProperties
@@ -55,7 +66,7 @@ type family GetMetaTypes x where
-- this constraint appears redundant, but is actually
-- crucial.
, MetaTypes y ~ GetMetaTypes p
- , CheckCombinable x y ~ 'CanCombine
+ , CheckCombinableNote x y (NoteFor ('Text "&")) ~ 'True
)
=> Props (MetaTypes x)
-> p
@@ -70,7 +81,7 @@ Props c & p = Props (c ++ [toChildProperty p])
-- this constraint appears redundant, but is actually
-- crucial.
, MetaTypes y ~ GetMetaTypes p
- , CheckCombinable x y ~ 'CanCombine
+ , CheckCombinableNote x y (NoteFor ('Text "&^")) ~ 'True
)
=> Props (MetaTypes x)
-> p
@@ -82,7 +93,7 @@ Props c &^ p = Props (toChildProperty p : c)
-- -Wredundant-constraints is turned off because
-- this constraint appears redundant, but is actually
-- crucial.
- :: (CheckCombinable x z ~ 'CanCombine)
+ :: (CheckCombinableNote x z (NoteFor ('Text "!")) ~ 'True)
=> Props (MetaTypes x)
-> RevertableProperty (MetaTypes y) (MetaTypes z)
-> Props (MetaTypes (Combine x z))
diff --git a/src/Propellor/Property/Atomic.hs b/src/Propellor/Property/Atomic.hs
index 8519048b..2c7433f6 100644
--- a/src/Propellor/Property/Atomic.hs
+++ b/src/Propellor/Property/Atomic.hs
@@ -46,10 +46,8 @@ type CheckAtomicResourcePair a = AtomicResourcePair a -> Propellor (AtomicResour
-- inactiveAtomicResource, and if it was successful,
-- atomically activating that resource.
atomicUpdate
- -- Constriaints inherited from ensureProperty.
- :: ( Cannot_ensureProperty_WithInfo t ~ 'True
- , (Targets t `NotSuperset` Targets t) ~ 'CanCombine
- )
+ -- Constriaint inherited from ensureProperty.
+ :: (EnsurePropertyAllowed t t ~ 'True)
=> SingI t
=> AtomicResourcePair a
-> CheckAtomicResourcePair a
@@ -92,10 +90,8 @@ atomicUpdate rbase rcheck rswap mkp = property' d $ \w -> do
-- children: a symlink with the name of the directory itself, and two copies
-- of the directory, with names suffixed with ".1" and ".2"
atomicDirUpdate
- -- Constriaints inherited from ensureProperty.
- :: ( Cannot_ensureProperty_WithInfo t ~ 'True
- , (Targets t `NotSuperset` Targets t) ~ 'CanCombine
- )
+ -- Constriaint inherited from ensureProperty.
+ :: (EnsurePropertyAllowed t t ~ 'True)
=> SingI t
=> FilePath
-> (FilePath -> Property (MetaTypes t))
diff --git a/src/Propellor/Types.hs b/src/Propellor/Types.hs
index 7052bf92..e8e92332 100644
--- a/src/Propellor/Types.hs
+++ b/src/Propellor/Types.hs
@@ -31,6 +31,7 @@ module Propellor.Types (
, HasInfo
, type (+)
, TightenTargets(..)
+ , TightenTargetsAllowed
-- * Combining and modifying properties
, Combines(..)
, CombinedType
@@ -44,6 +45,8 @@ module Propellor.Types (
, module Propellor.Types.ZFS
) where
+import GHC.TypeLits hiding (type (+))
+import Data.Type.Bool
import qualified Data.Semigroup as Sem
import Data.Monoid
import Control.Applicative
@@ -59,7 +62,7 @@ import Propellor.Types.MetaTypes
import Propellor.Types.ZFS
-- | The core data type of Propellor, this represents a property
--- that the system should have, with a descrition, and an action to ensure
+-- that the system should have, with a description, and an action to ensure
-- it has the property.
--
-- There are different types of properties that target different OS's,
@@ -185,17 +188,17 @@ class Combines x y where
-> y
-> CombinedType x y
-instance (CheckCombinable x y ~ 'CanCombine, SingI (Combine x y)) => Combines (Property (MetaTypes x)) (Property (MetaTypes y)) where
+instance (CheckCombinable x y ~ 'True, 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 (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
+instance (CheckCombinable x y ~ 'True, CheckCombinable x' y' ~ 'True, 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 (CheckCombinable x y ~ 'CanCombine, SingI (Combine x y)) => Combines (RevertableProperty (MetaTypes x) (MetaTypes x')) (Property (MetaTypes y)) where
+instance (CheckCombinable x y ~ 'True, 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 (CheckCombinable x y ~ 'CanCombine, SingI (Combine x y)) => Combines (Property (MetaTypes x)) (RevertableProperty (MetaTypes y) (MetaTypes y')) where
+instance (CheckCombinable x y ~ 'True, 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
class TightenTargets p where
@@ -209,14 +212,24 @@ class TightenTargets p where
-- > upgraded = tightenTargets $ cmdProperty "apt-get" ["upgrade"]
tightenTargets
::
- -- Note that this uses PolyKinds
- ( (Targets untightened `NotSuperset` Targets tightened) ~ 'CanCombine
- , (NonTargets tightened `NotSuperset` NonTargets untightened) ~ 'CanCombine
+ ( TightenTargetsAllowed untightened tightened ~ 'True
, SingI tightened
)
=> p (MetaTypes untightened)
-> p (MetaTypes tightened)
+-- Note that this uses PolyKinds
+type family TightenTargetsAllowed untightened tightened where
+ TightenTargetsAllowed untightened tightened =
+ If (Targets tightened `IsSubset` Targets untightened
+ && NonTargets untightened `IsSubset` NonTargets tightened)
+ 'True
+ ( TypeError
+ ( 'Text "This use of tightenTargets would widen, not narrow, adding: "
+ ':$$: PrettyPrintMetaTypes (Difference (Targets tightened) (Targets untightened))
+ )
+ )
+
instance TightenTargets Property where
tightenTargets (Property _ d a i c) = Property sing d a i c
diff --git a/src/Propellor/Types/MetaTypes.hs b/src/Propellor/Types/MetaTypes.hs
index 0c476e87..beb9ff61 100644
--- a/src/Propellor/Types/MetaTypes.hs
+++ b/src/Propellor/Types/MetaTypes.hs
@@ -17,19 +17,23 @@ module Propellor.Types.MetaTypes (
IncludesInfo,
Targets,
NonTargets,
- NotSuperset,
+ PrettyPrintMetaTypes,
+ IsSubset,
Combine,
- CheckCombine(..),
CheckCombinable,
+ CheckCombinableNote,
type (&&),
Not,
EqT,
Union,
+ Intersect,
+ Difference,
) where
import Propellor.Types.Singletons
import Propellor.Types.OS
+import GHC.TypeLits hiding (type (+))
import Data.Type.Bool
data MetaType
@@ -113,41 +117,52 @@ type family Combine (list1 :: [a]) (list2 :: [a]) :: [a] where
(Targets list1 `Intersect` Targets list2)
)
--- | Checks if two MetaTypes lists can be safely combined.
+-- | Checks if two MetaTypes lists can be safly combined;
+-- eg they have at least one Target in common.
+type family IsCombinable (list1 :: [a]) (list2 :: [a]) :: Bool where
+ -- As a special case, if either list is empty or only WithInfo,
+ -- 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
+ -- subsequent errors due to later CheckCombinable constraints.
+ IsCombinable '[] list2 = 'True
+ IsCombinable list1 '[] = 'True
+ IsCombinable ('WithInfo ': list1) list2 = IsCombinable list1 list2
+ IsCombinable list1 ('WithInfo ': list2) = IsCombinable list1 list2
+ IsCombinable list1 list2 =
+ Not (Null (Combine (Targets list1) (Targets list2)))
+
+-- | This (or CheckCombinableNote) should be used anywhere Combine is used,
+-- as an additional constraint. For example:
--
--- 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 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 where
- NotSuperset superset '[] = 'CanCombine
- NotSuperset superset (s ': rest) =
- If (Elem s superset)
- (NotSuperset superset rest)
- 'CannotCombineTargets
+-- > foo :: (CheckCombinable x y ~ 'True) => x -> y -> Combine x y
+type family CheckCombinable (list1 :: [a]) (list2 :: [a]) :: Bool where
+ CheckCombinable list1 list2 =
+ If (IsCombinable list1 list2)
+ 'True
+ ( TypeError (CannotCombine list1 list2)
+ )
+
+-- | Allows providing an additional note.
+type family CheckCombinableNote (list1 :: [a]) (list2 :: [a]) (note :: ErrorMessage) :: Bool where
+ CheckCombinableNote list1 list2 note =
+ If (IsCombinable list1 list2)
+ 'True
+ ( TypeError
+ ( CannotCombine list1 list2
+ ':$$: 'Text "("
+ ':<>: note
+ ':<>: 'Text ")"
+ )
+ )
+
+type family CannotCombine (list1 :: [a]) (list2 :: [a]) :: ErrorMessage where
+ CannotCombine list1 list2 =
+ 'Text "Cannot combine properties with MetaTypes"
+ ':$$: ('Text " " ':<>: PrettyPrintMetaTypes list1)
+ ':$$: 'Text " vs"
+ ':$$: ('Text " " ':<>: PrettyPrintMetaTypes list2)
type family IsTarget (a :: t) :: Bool where
IsTarget ('Targeting a) = 'True
@@ -167,6 +182,21 @@ type family NonTargets (l :: [a]) :: [a] where
(NonTargets xs)
(x ': NonTargets xs)
+-- | Pretty-prints a list of MetaTypes for display in a type error message.
+type family PrettyPrintMetaTypes (l :: [MetaType]) :: ErrorMessage where
+ PrettyPrintMetaTypes '[] = 'Text "<none>"
+ PrettyPrintMetaTypes (t ': '[]) = PrettyPrintMetaType t
+ PrettyPrintMetaTypes (t ': ts) =
+ PrettyPrintMetaType t ':<>: 'Text " + " ':<>: PrettyPrintMetaTypes ts
+
+type family PrettyPrintMetaType t :: ErrorMessage where
+ PrettyPrintMetaType 'WithInfo = 'ShowType HasInfo
+ PrettyPrintMetaType ('Targeting 'OSDebian) = 'ShowType Debian
+ PrettyPrintMetaType ('Targeting 'OSBuntish) = 'ShowType Buntish
+ PrettyPrintMetaType ('Targeting 'OSFreeBSD) = 'ShowType FreeBSD
+ PrettyPrintMetaType ('Targeting 'OSArchLinux) = 'ShowType ArchLinux
+ PrettyPrintMetaType ('Targeting t) = 'ShowType t
+
-- | Type level elem
type family Elem (a :: t) (list :: [t]) :: Bool where
Elem a '[] = 'False
@@ -188,6 +218,28 @@ type family Intersect (list1 :: [a]) (list2 :: [a]) :: [a] where
(a ': Intersect rest list2)
(Intersect rest list2)
+-- | Type level difference. Items that are in the first list, but not in
+-- the second.
+type family Difference (list1 :: [a]) (list2 :: [a]) :: [a] where
+ Difference '[] list2 = '[]
+ Difference (a ': rest) list2 =
+ If (Elem a list2)
+ (Difference rest list2)
+ (a ': Difference rest list2)
+
+-- | Every item in the subset must be in the superset.
+type family IsSubset (subset :: [a]) (superset :: [a]) :: Bool where
+ IsSubset '[] superset = 'True
+ IsSubset (s ': rest) superset =
+ If (Elem s superset)
+ (IsSubset rest superset)
+ 'False
+
+-- | Type level null.
+type family Null (list :: [a]) :: Bool where
+ Null '[] = 'True
+ Null l = 'False
+
-- | Type level equality of metatypes.
type family EqT (a :: MetaType) (b :: MetaType) where
EqT a a = 'True