diff --git a/CHANGELOG b/CHANGELOG --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,32 @@ +propellor (5.9.0) unstable; urgency=medium + + * 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, while later ghc + versions had no difficulty. If this affects building your properties, + adding a type annotation to the code will work around the problem. + * Added custom type error messages displayed when type inference + fails when using ensureProperty and tightenTargets, that suggest + adding a type annotation. + * 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. + * 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. + * EnsurePropertyAllowed, TightenTargetsAllowed, and CheckCombinable + types have changed to Constraint. + (API change) + * Try harder to avoid displaying an excessive amount of type error + messages when many properties have been combined in a props list. + * Libvirt.installed: install libvirt-daemon-system + Thanks, David Bremner + + -- Joey Hess Tue, 02 Jul 2019 16:27:07 -0400 + propellor (5.8.0) unstable; urgency=medium * Fix bug in File.containsShellSetting that replaced whole shell conffile diff --git a/debian/changelog b/debian/changelog --- a/debian/changelog +++ b/debian/changelog @@ -1,3 +1,32 @@ +propellor (5.9.0) unstable; urgency=medium + + * 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, while later ghc + versions had no difficulty. If this affects building your properties, + adding a type annotation to the code will work around the problem. + * Added custom type error messages displayed when type inference + fails when using ensureProperty and tightenTargets, that suggest + adding a type annotation. + * 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. + * 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. + * EnsurePropertyAllowed, TightenTargetsAllowed, and CheckCombinable + types have changed to Constraint. + (API change) + * Try harder to avoid displaying an excessive amount of type error + messages when many properties have been combined in a props list. + * Libvirt.installed: install libvirt-daemon-system + Thanks, David Bremner + + -- Joey Hess Tue, 02 Jul 2019 16:27:07 -0400 + propellor (5.8.0) unstable; urgency=medium * Fix bug in File.containsShellSetting that replaced whole shell conffile diff --git a/joeyconfig.hs b/joeyconfig.hs --- a/joeyconfig.hs +++ b/joeyconfig.hs @@ -417,7 +417,8 @@ & Apt.serviceInstalledRunning "swapspace" & Cron.runPropellor (Cron.Times "30 * * * *") & Apt.installed ["etckeeper", "sudo"] - & Apt.removed ["nfs-common", "exim4", "exim4-base", "exim4-daemon-light", "rsyslog", "acpid", "rpcbind", "at"] + & JoeySites.noExim + & Apt.removed ["nfs-common", "rsyslog", "acpid", "rpcbind", "at"] & User.hasSomePassword (User "root") & User.accountFor (User "joey") @@ -525,13 +526,14 @@ & Apt.installed ["vim", "screen", "less"] & Cron.runPropellor (Cron.Times "30 * * * *") -- I use postfix, or no MTA. - & Apt.removed ["exim4", "exim4-daemon-light", "exim4-config", "exim4-base"] - `onChange` Apt.autoRemove + & JoeySites.noExim -- This is my standard container setup, Featuring automatic upgrades. standardContainer :: DebianSuite -> Property (HasInfo + Debian) standardContainer suite = propertyList "standard container" $ props & osDebian suite X86_64 + -- Do not want to run mail daemon inside a random container.. + & JoeySites.noExim & Apt.stdSourcesList `onChange` Apt.upgrade & Apt.unattendedUpgrades & Apt.cacheCleaned diff --git a/propellor.cabal b/propellor.cabal --- a/propellor.cabal +++ b/propellor.cabal @@ -1,5 +1,5 @@ Name: propellor -Version: 5.8.0 +Version: 5.9.0 Cabal-Version: 1.20 License: BSD2 Maintainer: Joey Hess @@ -35,11 +35,12 @@ . 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 - if impl(ghc >= 8.0) - GHC-Options: -fno-warn-redundant-constraints Default-Extensions: TypeOperators Hs-Source-Dirs: src Build-Depends: @@ -49,6 +50,9 @@ 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 --- a/src/Propellor/EnsureProperty.hs +++ b/src/Propellor/EnsureProperty.hs @@ -1,6 +1,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} @@ -8,7 +9,7 @@ ( ensureProperty , property' , OuterMetaTypesWitness - , Cannot_ensureProperty_WithInfo + , EnsurePropertyAllowed ) where import Propellor.Types @@ -16,6 +17,9 @@ import Propellor.Types.MetaTypes import Propellor.Exception +import GHC.TypeLits +import GHC.Exts (Constraint) +import Data.Type.Bool import Data.Monoid import Prelude @@ -41,19 +45,40 @@ -- -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) => 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 :: Constraint where + EnsurePropertyAllowed inner outer = 'True ~ + ((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) + (DelayError + ('Text "ensureProperty outer Property type is not able to be inferred here." + ':$$: 'Text "Consider adding a type annotation." + ) + ) + (DelayErrorFcf + ('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 --- a/src/Propellor/PropAccum.hs +++ b/src/Propellor/PropAccum.hs @@ -19,6 +19,7 @@ import Propellor.Types.Core import Propellor.Property +import GHC.TypeLits import Data.Monoid import Prelude @@ -45,6 +46,16 @@ 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 @@ -- this constraint appears redundant, but is actually -- crucial. , MetaTypes y ~ GetMetaTypes p - , CheckCombinable x y ~ 'CanCombine + , CheckCombinableNote x y (NoteFor ('Text "&")) ) => Props (MetaTypes x) -> p @@ -70,7 +81,7 @@ -- this constraint appears redundant, but is actually -- crucial. , MetaTypes y ~ GetMetaTypes p - , CheckCombinable x y ~ 'CanCombine + , CheckCombinableNote x y (NoteFor ('Text "&^")) ) => Props (MetaTypes x) -> p @@ -82,7 +93,7 @@ -- -Wredundant-constraints is turned off because -- this constraint appears redundant, but is actually -- crucial. - :: (CheckCombinable x z ~ 'CanCombine) + :: CheckCombinableNote x z (NoteFor ('Text "!")) => 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 --- a/src/Propellor/Property/Aiccu.hs +++ b/src/Propellor/Property/Aiccu.hs @@ -47,8 +47,7 @@ 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 --- a/src/Propellor/Property/Atomic.hs +++ b/src/Propellor/Property/Atomic.hs @@ -46,10 +46,8 @@ -- 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 => SingI t => AtomicResourcePair a -> CheckAtomicResourcePair a @@ -92,10 +90,8 @@ -- 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 => SingI t => FilePath -> (FilePath -> Property (MetaTypes t)) diff --git a/src/Propellor/Property/Libvirt.hs b/src/Propellor/Property/Libvirt.hs --- a/src/Propellor/Property/Libvirt.hs +++ b/src/Propellor/Property/Libvirt.hs @@ -34,7 +34,7 @@ -- | Install basic libvirt components installed :: Property DebianLike -installed = Apt.installed ["libvirt-clients", "virtinst"] +installed = Apt.installed ["libvirt-clients", "virtinst", "libvirt-daemon", "libvirt-daemon-system"] -- | Ensure that the default libvirt network is set to autostart, and start it. -- diff --git a/src/Propellor/Property/SiteSpecific/JoeySites.hs b/src/Propellor/Property/SiteSpecific/JoeySites.hs --- a/src/Propellor/Property/SiteSpecific/JoeySites.hs +++ b/src/Propellor/Property/SiteSpecific/JoeySites.hs @@ -910,15 +910,16 @@ & Systemd.enabled setupservicename `requires` setupserviceinstalled `onChange` Systemd.started setupservicename - & Systemd.enabled watchdogservicename - `requires` watchdogserviceinstalled - `onChange` Systemd.started watchdogservicename & Systemd.enabled pollerservicename `requires` pollerserviceinstalled `onChange` Systemd.started pollerservicename & Systemd.enabled controllerservicename `requires` controllerserviceinstalled `onChange` Systemd.started controllerservicename + & Systemd.enabled watchdogservicename + `requires` watchdogserviceinstalled + `onChange` Systemd.started watchdogservicename + & Apt.serviceInstalledRunning "watchdog" & User.hasGroup user (Group "dialout") & Group.exists (Group "gpio") Nothing & User.hasGroup user (Group "gpio") @@ -1025,7 +1026,7 @@ ] -- Any changes to the rsync command will need my .authorized_keys -- rsync server command to be updated too. - rsynccommand = "rsync -e 'ssh -i" ++ sshkeyfile ++ "' -avz rrds/ joey@kitenet.net:/srv/web/house.joeyh.name/rrds/" + rsynccommand = "rsync -e 'ssh -i" ++ sshkeyfile ++ "' -avz rrds/ joey@kitenet.net:/srv/web/house.joeyh.name/rrds/ >/dev/null 2>&1" websitesymlink :: Property UnixLike websitesymlink = check (not . isSymbolicLink <$> getSymbolicLinkStatus "/var/www/html") @@ -1321,3 +1322,7 @@ where -- rsync.net has a newer borg here os' = Borg.UsesEnvVar ("BORG_REMOTE_PATH", "borg1") : os + +noExim :: Property DebianLike +noExim = Apt.removed ["exim4", "exim4-base", "exim4-daemon-light"] + `onChange` Apt.autoRemove diff --git a/src/Propellor/Property/Systemd.hs b/src/Propellor/Property/Systemd.hs --- a/src/Propellor/Property/Systemd.hs +++ b/src/Propellor/Property/Systemd.hs @@ -391,6 +391,7 @@ 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 --- a/src/Propellor/Property/Tor.hs +++ b/src/Propellor/Property/Tor.hs @@ -172,20 +172,22 @@ 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 --- a/src/Propellor/Types.hs +++ b/src/Propellor/Types.hs @@ -4,6 +4,7 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveDataTypeable #-} @@ -31,6 +32,7 @@ , HasInfo , type (+) , TightenTargets(..) + , TightenTargetsAllowed -- * Combining and modifying properties , Combines(..) , CombinedType @@ -44,6 +46,9 @@ , module Propellor.Types.ZFS ) where +import GHC.TypeLits hiding (type (+)) +import GHC.Exts (Constraint) +import Data.Type.Bool import qualified Data.Semigroup as Sem import Data.Monoid import Control.Applicative @@ -59,7 +64,7 @@ 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 +190,17 @@ -> 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, 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, CheckCombinable x' y', 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, 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, 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,13 +214,30 @@ -- > 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 , SingI tightened ) => p (MetaTypes untightened) -> p (MetaTypes tightened) + +-- Note that this uses PolyKinds +type family TightenTargetsAllowed untightened tightened :: Constraint where + TightenTargetsAllowed untightened tightened = + If (Targets tightened `IsSubset` Targets untightened + && NonTargets untightened `IsSubset` NonTargets tightened) + ('True ~ 'True) + (IfStuck (Targets tightened) + (DelayError + ('Text "Unable to infer desired Property type in this use of tightenTargets." + ':$$: ('Text "Consider adding a type annotation.") + ) + ) + (DelayErrorFcf + ('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 --- a/src/Propellor/Types/MetaTypes.hs +++ b/src/Propellor/Types/MetaTypes.hs @@ -1,4 +1,6 @@ -{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, TypeFamilies, UndecidableInstances, FlexibleInstances, GADTs #-} +{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, ConstraintKinds #-} +{-# LANGUAGE TypeFamilies, UndecidableInstances, FlexibleInstances, GADTs #-} +{-# LANGUAGE CPP #-} module Propellor.Types.MetaTypes ( MetaType(..), @@ -17,21 +19,40 @@ IncludesInfo, Targets, NonTargets, - NotSuperset, + PrettyPrintMetaTypes, + IsSubset, Combine, - CheckCombine(..), CheckCombinable, + CheckCombinableNote, type (&&), Not, EqT, Union, + Intersect, + Difference, + IfStuck, + DelayError, + DelayErrorFcf, ) where import Propellor.Types.Singletons import Propellor.Types.OS +import GHC.TypeLits hiding (type (+)) +import GHC.Exts (Constraint) 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 +type family DelayError msg where + DelayError msg = TypeError msg +type family DelayErrorFcf msg where + DelayErrorFcf msg = TypeError msg +#endif + data MetaType = Targeting TargetOS -- ^ A target OS of a Property | WithInfo -- ^ Indicates that a Property has associated Info @@ -113,42 +134,70 @@ (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: +-- | 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: -- --- > 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) +-- > foo :: CheckCombinable x y => x -> y -> Combine x y +type family CheckCombinable (list1 :: [a]) (list2 :: [a]) :: Constraint where + CheckCombinable list1 list2 = + If (IsCombinable list1 list2) + ('True ~ 'True) + (CannotCombine list1 list2 'Nothing) -data CheckCombine = CannotCombineTargets | CanCombine +-- | Allows providing an additional note. +type family CheckCombinableNote (list1 :: [a]) (list2 :: [a]) (note :: ErrorMessage) :: Constraint where + CheckCombinableNote list1 list2 note = + If (IsCombinable list1 list2) + ('True ~ 'True) + (CannotCombine list1 list2 + ('Just ('Text "(" ':<>: note ':<>: 'Text ")")) + ) --- | 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 +-- 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) :: Constraint where + CannotCombine list1 list2 note = + IfStuck list1 + (IfStuck list2 + (DelayError (CannotCombineMessage UnknownType UnknownType UnknownTypeNote)) + (DelayErrorFcf (CannotCombineMessage UnknownType (PrettyPrintMetaTypes list2) UnknownTypeNote)) + ) + (IfStuck list2 + (DelayError (CannotCombineMessage (PrettyPrintMetaTypes list1) UnknownType UnknownTypeNote)) + (DelayErrorFcf (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 caused by applying a Property constructor to the wrong number of arguments.)") + +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 IsTarget 'WithInfo = 'False @@ -167,6 +216,21 @@ (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 @@ -187,6 +251,28 @@ If (Elem a list2 && Not (Elem a rest)) (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 diff --git a/stack.yaml b/stack.yaml --- 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