From 1c12b89a671152d7da4630b41b48815eefc8c2fe Mon Sep 17 00:00:00 2001 From: Joey Hess Date: Tue, 2 Jul 2019 14:39:51 -0400 Subject: use ConstraintKinds This is just a bit prettier code than manually needing to use constraint ~ True --- src/Propellor/EnsureProperty.hs | 12 +++++++----- src/Propellor/PropAccum.hs | 6 +++--- src/Propellor/Property/Atomic.hs | 4 ++-- src/Propellor/Types.hs | 16 +++++++++------- src/Propellor/Types/MetaTypes.hs | 16 +++++++++------- 5 files changed, 30 insertions(+), 24 deletions(-) (limited to 'src') diff --git a/src/Propellor/EnsureProperty.hs b/src/Propellor/EnsureProperty.hs index 4b70ffb7..9f3d0a19 100644 --- 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 #-} @@ -17,6 +18,7 @@ import Propellor.Types.MetaTypes import Propellor.Exception import GHC.TypeLits +import GHC.Exts (Constraint) import Data.Type.Bool import Data.Monoid import Prelude @@ -43,17 +45,17 @@ ensureProperty -- -Wredundant-constraints is turned off because -- this constraint appears redundant, but is actually -- crucial. - ( EnsurePropertyAllowed inner outer ~ 'True) + ( EnsurePropertyAllowed inner outer) => OuterMetaTypesWitness outer -> Property (MetaTypes inner) -> Propellor Result ensureProperty _ = maybe (return NoChange) catchPropellor . getSatisfy -type family EnsurePropertyAllowed inner outer where - EnsurePropertyAllowed inner outer = - (EnsurePropertyNoInfo inner) +type family EnsurePropertyAllowed inner outer :: Constraint where + EnsurePropertyAllowed inner outer = 'True ~ + ((EnsurePropertyNoInfo inner) && - (EnsurePropertyTargetOSMatches inner outer) + (EnsurePropertyTargetOSMatches inner outer)) type family EnsurePropertyNoInfo (l :: [a]) :: Bool where EnsurePropertyNoInfo '[] = 'True diff --git a/src/Propellor/PropAccum.hs b/src/Propellor/PropAccum.hs index 3fc83202..ea85f04f 100644 --- a/src/Propellor/PropAccum.hs +++ b/src/Propellor/PropAccum.hs @@ -66,7 +66,7 @@ type family NoteFor symbol :: ErrorMessage where -- this constraint appears redundant, but is actually -- crucial. , MetaTypes y ~ GetMetaTypes p - , CheckCombinableNote x y (NoteFor ('Text "&")) ~ 'True + , CheckCombinableNote x y (NoteFor ('Text "&")) ) => Props (MetaTypes x) -> p @@ -81,7 +81,7 @@ Props c & p = Props (c ++ [toChildProperty p]) -- this constraint appears redundant, but is actually -- crucial. , MetaTypes y ~ GetMetaTypes p - , CheckCombinableNote x y (NoteFor ('Text "&^")) ~ 'True + , CheckCombinableNote x y (NoteFor ('Text "&^")) ) => Props (MetaTypes x) -> p @@ -93,7 +93,7 @@ Props c &^ p = Props (toChildProperty p : c) -- -Wredundant-constraints is turned off because -- this constraint appears redundant, but is actually -- crucial. - :: (CheckCombinableNote x z (NoteFor ('Text "!")) ~ 'True) + :: CheckCombinableNote x z (NoteFor ('Text "!")) => 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 2c7433f6..8f2ef1d3 100644 --- a/src/Propellor/Property/Atomic.hs +++ b/src/Propellor/Property/Atomic.hs @@ -47,7 +47,7 @@ type CheckAtomicResourcePair a = AtomicResourcePair a -> Propellor (AtomicResour -- atomically activating that resource. atomicUpdate -- Constriaint inherited from ensureProperty. - :: (EnsurePropertyAllowed t t ~ 'True) + :: EnsurePropertyAllowed t t => SingI t => AtomicResourcePair a -> CheckAtomicResourcePair a @@ -91,7 +91,7 @@ atomicUpdate rbase rcheck rswap mkp = property' d $ \w -> do -- of the directory, with names suffixed with ".1" and ".2" atomicDirUpdate -- Constriaint inherited from ensureProperty. - :: (EnsurePropertyAllowed t t ~ 'True) + :: EnsurePropertyAllowed t t => SingI t => FilePath -> (FilePath -> Property (MetaTypes t)) diff --git a/src/Propellor/Types.hs b/src/Propellor/Types.hs index 0a3dd122..0d9b3d6b 100644 --- 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 #-} @@ -46,6 +47,7 @@ module Propellor.Types ( ) where import GHC.TypeLits hiding (type (+)) +import GHC.Exts (Constraint) import Data.Type.Bool import qualified Data.Semigroup as Sem import Data.Monoid @@ -188,17 +190,17 @@ class Combines x y where -> y -> CombinedType x y -instance (CheckCombinable x y ~ 'True, 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 ~ '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 +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 ~ 'True, 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 ~ 'True, 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 @@ -212,18 +214,18 @@ class TightenTargets p where -- > upgraded = tightenTargets $ cmdProperty "apt-get" ["upgrade"] tightenTargets :: - ( TightenTargetsAllowed untightened tightened ~ 'True + ( TightenTargetsAllowed untightened tightened , SingI tightened ) => p (MetaTypes untightened) -> p (MetaTypes tightened) -- Note that this uses PolyKinds -type family TightenTargetsAllowed untightened tightened where +type family TightenTargetsAllowed untightened tightened :: Constraint where TightenTargetsAllowed untightened tightened = If (Targets tightened `IsSubset` Targets untightened && NonTargets untightened `IsSubset` NonTargets tightened) - 'True + ('True ~ 'True) (IfStuck (Targets tightened) (DelayError ('Text "Unable to infer desired Property type in this use of tightenTargets." diff --git a/src/Propellor/Types/MetaTypes.hs b/src/Propellor/Types/MetaTypes.hs index 68b3503d..055338af 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 TypeOperators, PolyKinds, DataKinds, ConstraintKinds #-} +{-# LANGUAGE TypeFamilies, UndecidableInstances, FlexibleInstances, GADTs #-} {-# LANGUAGE CPP #-} module Propellor.Types.MetaTypes ( @@ -38,6 +39,7 @@ 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 @@ -151,25 +153,25 @@ type family IsCombinable (list1 :: [a]) (list2 :: [a]) :: Bool where -- | This (or CheckCombinableNote) should be used anywhere Combine is used, -- as an additional constraint. For example: -- --- > foo :: (CheckCombinable x y ~ 'True) => x -> y -> Combine x y -type family CheckCombinable (list1 :: [a]) (list2 :: [a]) :: Bool where +-- > 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 ~ 'True) (CannotCombine list1 list2 'Nothing) -- | Allows providing an additional note. -type family CheckCombinableNote (list1 :: [a]) (list2 :: [a]) (note :: ErrorMessage) :: Bool where +type family CheckCombinableNote (list1 :: [a]) (list2 :: [a]) (note :: ErrorMessage) :: Constraint where CheckCombinableNote list1 list2 note = If (IsCombinable list1 list2) - 'True + ('True ~ '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 +type family CannotCombine (list1 :: [a]) (list2 :: [a]) (note :: Maybe ErrorMessage) :: Constraint where CannotCombine list1 list2 note = IfStuck list1 (IfStuck list2 -- cgit v1.2.3