    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE ConstraintKinds #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE UndecidableInstances #-}

    module Propellor.EnsureProperty
    	( ensureProperty
    	, property'
    	, OuterMetaTypesWitness
    	, EnsurePropertyAllowed
    	) where

    import Propellor.Types
    import Propellor.Types.Core
    import Propellor.Types.MetaTypes
    import Propellor.Exception

    import GHC.TypeLits
    import GHC.Exts (Constraint)
    import Data.Type.Bool
    import Data.Monoid
    import Prelude

    -- | For when code running in the Propellor monad needs to ensure a
    -- Property.
    --
    -- Use `property'` to get the `OuterMetaTypesWithness`. For example:
    --
    -- > foo = Property Debian
    -- > foo = property' "my property" $ \w -> do
    -- > 	ensureProperty w (aptInstall "foo")
    --
    -- The type checker will prevent using ensureProperty with a property
    -- that does not support the target OSes needed by the OuterMetaTypesWitness.
    -- In the example above, aptInstall must support Debian, since foo
    -- is supposed to support Debian.
    --
    -- The type checker will also prevent using ensureProperty with a property
    -- with HasInfo in its MetaTypes. Doing so would cause the `Info` associated
    -- with the property to be lost.
    ensureProperty
    	::
    		-- -Wredundant-constraints is turned off because
    		-- this constraint appears redundant, but is actually
    		-- crucial.
    		( EnsurePropertyAllowed inner outer)
    	=> OuterMetaTypesWitness outer
    	-> Property (MetaTypes inner)
    	-> Propellor Result
    ensureProperty :: forall (inner :: [MetaType]) (outer :: [MetaType]).
    EnsurePropertyAllowed inner outer =>
    OuterMetaTypesWitness outer
    -> Property (MetaTypes inner) -> Propellor Result
    ensureProperty OuterMetaTypesWitness outer
    _ = Propellor Result
    -> (Propellor Result -> Propellor Result)
    -> Maybe (Propellor Result)
    -> Propellor Result
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (Result -> Propellor Result
    forall a. a -> Propellor a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    NoChange) Propellor Result -> Propellor Result
    forall (m :: * -> *).
    (MonadIO m, MonadCatch m) =>
    m Result -> m Result
    catchPropellor (Maybe (Propellor Result) -> Propellor Result)
    -> (Property (MetaTypes inner) -> Maybe (Propellor Result))
    -> Property (MetaTypes inner)
    -> Propellor Result
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Property (MetaTypes inner) -> Maybe (Propellor Result)
    forall p. IsProp p => p -> Maybe (Propellor Result)
    getSatisfy

    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`.
    property'
    	:: SingI metatypes
    	=> Desc
    	-> (OuterMetaTypesWitness metatypes -> Propellor Result)
    	-> Property (MetaTypes metatypes)
    property' :: forall {k} (metatypes :: k).
    SingI metatypes =>
    Desc
    -> (OuterMetaTypesWitness metatypes -> Propellor Result)
    -> Property (MetaTypes metatypes)
    property' Desc
    d OuterMetaTypesWitness metatypes -> Propellor Result
    a =
    	let p :: Property (Sing metatypes)
    p = Sing metatypes
    -> Desc
    -> Maybe (Propellor Result)
    -> Info
    -> [ChildProperty]
    -> Property (Sing metatypes)
    forall metatypes.
    metatypes
    -> Desc
    -> Maybe (Propellor Result)
    -> Info
    -> [ChildProperty]
    -> Property metatypes
    Property Sing metatypes
    forall {k} (t :: k). SingI t => Sing t
    sing Desc
    d (Propellor Result -> Maybe (Propellor Result)
    forall a. a -> Maybe a
    Just (OuterMetaTypesWitness metatypes -> Propellor Result
    a (Property (Sing metatypes) -> OuterMetaTypesWitness metatypes
    forall {k} (l :: k).
    Property (MetaTypes l) -> OuterMetaTypesWitness l
    outerMetaTypesWitness Property (Sing metatypes)
    p))) Info
    forall a. Monoid a => a
    mempty [ChildProperty]
    forall a. Monoid a => a
    mempty
    	in Property (Sing metatypes)
    p

    -- | Used to provide the metatypes of a Property to calls to
    -- 'ensureProperty` within it.
    newtype OuterMetaTypesWitness metatypes = OuterMetaTypesWitness (MetaTypes metatypes)

    outerMetaTypesWitness :: Property (MetaTypes l) -> OuterMetaTypesWitness l
    outerMetaTypesWitness :: forall {k} (l :: k).
    Property (MetaTypes l) -> OuterMetaTypesWitness l
    outerMetaTypesWitness (Property MetaTypes l
    metatypes Desc
    _ Maybe (Propellor Result)
    _ Info
    _ [ChildProperty]
    _) = MetaTypes l -> OuterMetaTypesWitness l
    forall {k} (metatypes :: k).
    MetaTypes metatypes -> OuterMetaTypesWitness metatypes
    OuterMetaTypesWitness MetaTypes l
    metatypes