summaryrefslogtreecommitdiff
path: root/src/Propellor
diff options
context:
space:
mode:
Diffstat (limited to 'src/Propellor')
-rw-r--r--src/Propellor/EnsureProperty.hs12
-rw-r--r--src/Propellor/PropAccum.hs6
-rw-r--r--src/Propellor/Property/Atomic.hs4
-rw-r--r--src/Propellor/Types.hs16
-rw-r--r--src/Propellor/Types/MetaTypes.hs16
5 files changed, 30 insertions, 24 deletions
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