From 2ba2cda972f484771b763603bf09d555003861b7 Mon Sep 17 00:00:00 2001 From: Joey Hess Date: Tue, 2 Jul 2019 00:46:21 -0400 Subject: Revert "Revert "custom type error messages"" This reverts commit 665ea0d3d9e1b0e90278fd659dee0ef8642030da. --- debian/changelog | 25 +++- doc/todo/use_ghc_8.0_custom_compile_errors.mdwn | 22 +++- propellor.cabal | 6 + src/Propellor/EnsureProperty.hs | 41 +++++-- src/Propellor/PropAccum.hs | 17 ++- src/Propellor/Property/Aiccu.hs | 5 +- src/Propellor/Property/Atomic.hs | 12 +- src/Propellor/Property/Systemd.hs | 1 + src/Propellor/Property/Tor.hs | 30 ++--- src/Propellor/Types.hs | 36 ++++-- src/Propellor/Types/MetaTypes.hs | 148 ++++++++++++++++++------ stack.yaml | 3 + 12 files changed, 262 insertions(+), 84 deletions(-) diff --git a/debian/changelog b/debian/changelog index c263fc96..c74cd929 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,5 +1,26 @@ -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. + * Note that those changes made ghc 8.0.1 in a few cases unable to infer + types when ensureProperty or tightenTargets is used. Adding a type + annotation will work around this problem, if you cannot upgrade + to a newer ghc that handles them better. + * Use the type-errors library to detect when the type checker gets stuck + unable to reduce type-level operations on MetaTypes, and avoid + displaying massive error messages in such a case. + * But, since type-errors is a new library not available in eg Debian + yet, added a WithTypeErrors build flag. When the library is not + available, cabal will automatically disable that build flag, + and it will build without the type-errors library. + * 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 d21c92fe..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,7 +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. -> The `custom-error-types` branch has this implemented quite nicely. -> Unfortunately, it ran into a ghc bug +> 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. + +> 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/propellor.cabal b/propellor.cabal index 300313c0..71d3c578 100644 --- a/propellor.cabal +++ b/propellor.cabal @@ -35,6 +35,9 @@ Description: . It is configured using haskell. +Flag WithTypeErrors + Description: Build with type-errors library for better error messages + Library Default-Language: Haskell98 GHC-Options: -Wall -fno-warn-tabs -O0 @@ -47,6 +50,9 @@ Library directory, filepath, IfElse, process, bytestring, hslogger, split, unix, unix-compat, ansi-terminal, containers (>= 0.5), network, async, time, mtl, transformers, exceptions (>= 0.6), stm, text, hashable + if flag(WithTypeErrors) + Build-Depends: type-errors + CPP-Options: -DWITH_TYPE_ERRORS Exposed-Modules: Propellor diff --git a/src/Propellor/EnsureProperty.hs b/src/Propellor/EnsureProperty.hs index ab624706..5ed0325f 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,40 @@ 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 + (IfStuck (Targets outer) + (TypeError + ('Text "ensureProperty outer Property type is not able to be inferred here." + ':$$: 'Text "Consider adding a type annotation." + ) + ) + (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/Aiccu.hs b/src/Propellor/Property/Aiccu.hs index 1b28759c..8bf3f283 100644 --- a/src/Propellor/Property/Aiccu.hs +++ b/src/Propellor/Property/Aiccu.hs @@ -47,8 +47,7 @@ hasConfig :: TunnelId -> UserName -> Property (HasInfo + DebianLike) hasConfig t u = prop `onChange` restarted where prop :: Property (HasInfo + UnixLike) - prop = withSomePrivData [(Password (u++"/"++t)), (Password u)] (Context "aiccu") $ - property' "aiccu configured" . writeConfig - writeConfig getpassword w = getpassword $ ensureProperty w . go + prop = withSomePrivData [(Password (u++"/"++t)), (Password u)] (Context "aiccu") $ \getpassword -> + property' "aiccu configured" $ \w -> getpassword $ ensureProperty w . go go (Password u', p) = confPath `File.hasContentProtected` config u' t p go (f, _) = error $ "Unexpected type of privdata: " ++ show f 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/Property/Systemd.hs b/src/Propellor/Property/Systemd.hs index bfc0f9a5..5d597ac6 100644 --- a/src/Propellor/Property/Systemd.hs +++ b/src/Propellor/Property/Systemd.hs @@ -391,6 +391,7 @@ mungename = replace "/" "_" containerCfg :: String -> RevertableProperty (HasInfo + Linux) (HasInfo + Linux) containerCfg p = RevertableProperty (mk True) (mk False) where + mk :: Bool -> Property (HasInfo + Linux) mk b = tightenTargets $ pureInfoProperty desc $ mempty { _chrootCfg = SystemdNspawnCfg [(p', b)] } diff --git a/src/Propellor/Property/Tor.hs b/src/Propellor/Property/Tor.hs index 426d4209..862af983 100644 --- a/src/Propellor/Property/Tor.hs +++ b/src/Propellor/Property/Tor.hs @@ -172,20 +172,22 @@ hiddenServiceData hn context = combineProperties desc $ props where desc = unwords ["hidden service data available in", varLib hn] installonion :: FilePath -> Property (HasInfo + DebianLike) - installonion f = withPrivData (PrivFile $ varLib hn f) context $ \getcontent -> - property' desc $ \w -> getcontent $ install w $ varLib hn f - install w f privcontent = ifM (liftIO $ doesFileExist f) - ( noChange - , ensureProperty w $ propertyList desc $ toProps - [ property desc $ makeChange $ do - createDirectoryIfMissing True (takeDirectory f) - writeFileProtected f (unlines (privDataLines privcontent)) - , File.mode (takeDirectory f) $ combineModes - [ownerReadMode, ownerWriteMode, ownerExecuteMode] - , File.ownerGroup (takeDirectory f) user (userGroup user) - , File.ownerGroup f user (userGroup user) - ] - ) + installonion basef = + let f = varLib hn basef + in withPrivData (PrivFile f) context $ \getcontent -> + property' desc $ \w -> getcontent $ \privcontent -> + ifM (liftIO $ doesFileExist f) + ( noChange + , ensureProperty w $ propertyList desc $ toProps + [ property desc $ makeChange $ do + createDirectoryIfMissing True (takeDirectory f) + writeFileProtected f (unlines (privDataLines privcontent)) + , File.mode (takeDirectory f) $ combineModes + [ownerReadMode, ownerWriteMode, ownerExecuteMode] + , File.ownerGroup (takeDirectory f) user (userGroup user) + , File.ownerGroup f user (userGroup user) + ] + ) restarted :: Property DebianLike restarted = Service.restarted "tor" diff --git a/src/Propellor/Types.hs b/src/Propellor/Types.hs index 7052bf92..026babf0 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,31 @@ 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 + (IfStuck (Targets tightened) + (TypeError + ('Text "Unable to infer desired Property type in this use of tightenTargets." + ':$$: ('Text "Consider adding a type annotation.") + ) + ) + (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..567f533a 100644 --- a/src/Propellor/Types/MetaTypes.hs +++ b/src/Propellor/Types/MetaTypes.hs @@ -1,4 +1,5 @@ {-# LANGUAGE TypeOperators, PolyKinds, DataKinds, TypeFamilies, UndecidableInstances, FlexibleInstances, GADTs #-} +{-# LANGUAGE CPP #-} module Propellor.Types.MetaTypes ( MetaType(..), @@ -17,21 +18,33 @@ module Propellor.Types.MetaTypes ( IncludesInfo, Targets, NonTargets, - NotSuperset, + PrettyPrintMetaTypes, + IsSubset, Combine, - CheckCombine(..), CheckCombinable, + CheckCombinableNote, type (&&), Not, EqT, Union, + Intersect, + Difference, + IfStuck, ) where import Propellor.Types.Singletons import Propellor.Types.OS +import GHC.TypeLits hiding (type (+)) import Data.Type.Bool +#ifdef WITH_TYPE_ERRORS +import Type.Errors +#else +type family IfStuck (expr :: k) (b :: k1) (c :: k1) :: k1 where + IfStuck expr b c = c +#endif + data MetaType = Targeting TargetOS -- ^ A target OS of a Property | WithInfo -- ^ Indicates that a Property has associated Info @@ -113,41 +126,69 @@ type family Combine (list1 :: [a]) (list2 :: [a]) :: [a] where (Targets list1 `Intersect` Targets list2) ) --- | 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 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 +-- | 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))) --- | Every item in the subset must be in the superset. +-- | This (or CheckCombinableNote) should be used anywhere Combine is used, +-- as an additional constraint. For example: -- --- 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 + (CannotCombine list1 list2 'Nothing) + +-- | 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 + (CannotCombine list1 list2 + ('Just ('Text "(" ':<>: note ':<>: 'Text ")")) + ) + +-- Checking IfStuck is to avoid massive and useless error message leaking +-- type families from this module. +type family CannotCombine (list1 :: [a]) (list2 :: [a]) (note :: Maybe ErrorMessage) :: Bool where + CannotCombine list1 list2 note = + IfStuck list1 + (IfStuck list2 + (TypeError (CannotCombineMessage UnknownType UnknownType UnknownTypeNote)) + (TypeError (CannotCombineMessage UnknownType (PrettyPrintMetaTypes list2) UnknownTypeNote)) + ) + (IfStuck list2 + (TypeError (CannotCombineMessage (PrettyPrintMetaTypes list1) UnknownType UnknownTypeNote)) + (TypeError (CannotCombineMessage (PrettyPrintMetaTypes list1) (PrettyPrintMetaTypes list2) note)) + ) + +type family UnknownType :: ErrorMessage where + UnknownType = 'Text "" + +type family UnknownTypeNote :: Maybe ErrorMessage where + UnknownTypeNote = 'Just ('Text "(Property is often due to a partially applied Property constructor, or due to passing the wrong type to a Property constructor.)") + +type family CannotCombineMessage (a :: ErrorMessage) (b :: ErrorMessage) (note :: Maybe ErrorMessage) :: ErrorMessage where + CannotCombineMessage a b ('Just note) = + CannotCombineMessage a b 'Nothing + ':$$: note + CannotCombineMessage a b 'Nothing = + 'Text "Cannot combine Properties:" + ':$$: ('Text " Property " ':<>: a) + ':$$: ('Text " Property " ':<>: b) type family IsTarget (a :: t) :: Bool where IsTarget ('Targeting a) = 'True @@ -167,6 +208,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 +244,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 diff --git a/stack.yaml b/stack.yaml index eb243950..84dbf12e 100644 --- a/stack.yaml +++ b/stack.yaml @@ -2,3 +2,6 @@ resolver: lts-9.21 packages: - '.' +extra-deps: +- type-errors-0.1.0.0 +- first-class-families-0.5.0.0 -- cgit v1.2.3