{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Propellor.EnsureProperty
( ensureProperty
, property'
, OuterMetaTypesWitness(..)
, Cannot_ensureProperty_WithInfo
) where
import Propellor.Types
import Propellor.Types.Core
import Propellor.Types.MetaTypes
import Propellor.Exception
import Data.Monoid
import Prelude
ensureProperty
::
( Cannot_ensureProperty_WithInfo inner ~ 'True
, (Targets inner `NotSuperset` Targets outer) ~ 'CanCombine
)
=> OuterMetaTypesWitness outer
-> Property (MetaTypes inner)
-> Propellor Result
ensureProperty _ = maybe (return NoChange) catchPropellor . getSatisfy
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
property'
:: SingI metatypes
=> Desc
-> (OuterMetaTypesWitness metatypes -> Propellor Result)
-> Property (MetaTypes metatypes)
property' d a =
let p = Property sing d (Just (a (outerMetaTypesWitness p))) mempty mempty
in p
newtype OuterMetaTypesWitness metatypes = OuterMetaTypesWitness (MetaTypes metatypes)
outerMetaTypesWitness :: Property (MetaTypes l) -> OuterMetaTypesWitness l
outerMetaTypesWitness (Property metatypes _ _ _ _) = OuterMetaTypesWitness metatypes