From 14f6ae30809d8bbdb10b91cc59757e865a365df8 Mon Sep 17 00:00:00 2001 From: Joey Hess Date: Mon, 1 Jul 2019 15:49:20 -0400 Subject: 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. --- debian/changelog | 14 ++- doc/todo/use_ghc_8.0_custom_compile_errors.mdwn | 36 ++++--- src/Propellor/EnsureProperty.hs | 34 +++++-- src/Propellor/PropAccum.hs | 17 +++- src/Propellor/Property/Atomic.hs | 12 +-- src/Propellor/Types.hs | 29 ++++-- src/Propellor/Types/MetaTypes.hs | 124 +++++++++++++++++------- 7 files changed, 181 insertions(+), 85 deletions(-) diff --git a/debian/changelog b/debian/changelog index c263fc96..8944ff8f 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,5 +1,15 @@ -propellor (5.8.1) UNRELEASED; urgency=medium - +propellor (5.9.0) UNRELEASED; urgency=medium + + * 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) * Libvirt.installed: install libvirt-daemon-system Thanks, David Bremner diff --git a/doc/todo/use_ghc_8.0_custom_compile_errors.mdwn b/doc/todo/use_ghc_8.0_custom_compile_errors.mdwn index 95f86143..8c2ed77a 100644 --- a/doc/todo/use_ghc_8.0_custom_compile_errors.mdwn +++ b/doc/todo/use_ghc_8.0_custom_compile_errors.mdwn @@ -6,27 +6,25 @@ For example, a RevertableProperty is sometimes used where only a regular Property is accepted. In this case, the error could suggest that the user apply `setupRevertableProperty` to extract the setup side of the RevertableProperty. +> I tried this, it didn't seem worth the complication however. --[[Joey]] + And, when a Property HasInfo is provided to ensureProperty, propellor could explain, in the compile error, why it can't let the user do that. -Custom errors need a type class to be used. So, could do something like this: - - class NeedsProperty a where - withProperty :: (Property metatype -> b) -> b - - instance NeedsProperty (Property metatype) where withProperty = id - - instance TypeError (Text "Use setupRevertableProperty ...") - => NeedsProperty RevertableProperty where - withProperty = error "unreachable" - -(While propellor needs to be buildable with older versions of ghc, -the `instance TypeError` can just be wrapped in an ifdef to make it only be -used by the new ghc.) - -> The new type-errors library builds a lot of stuff on top of this. -> Its ability to detect "stuckness" seems like it may be able to catch -> the very long type errors that we sometimes see when using propellor, and -> whittle them down to a more useful error. --[[Joey]] +> Done this and also used custom errors when properties' types don't let +> them be combined. --[[Joey]] + +The new type-errors library builds a lot of stuff on top of this. +Its ability to detect "stuckness" seems like it may be able to catch +the very long type errors that we sometimes see when using propellor, and +whittle them down to a more useful error. --[[Joey]] + +> > Actually I think the stuckness would not help with that, though it +> > could help with other mistakes. In particular, forgetting to provide +> > a parameter to a property constructor can lead to a massive +> > error message that leaks type family stuff from MetaTypes, due to +> > the type checker getting stuck. Detecting that and replacing it with +> > a simpler error would be a big improvement. Such large error messages +> > can make ghc use an excessive amount of memory. --[[Joey]] [[!tag user/joey]] 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 "" + 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 -- cgit v1.2.3