    {-# LANGUAGE TypeOperators, PolyKinds, DataKinds, TypeFamilies, UndecidableInstances, FlexibleInstances, GADTs #-}

    module Propellor.Types.MetaTypes (
    	MetaType(..),
    	UnixLike,
    	Linux,
    	DebianLike,
    	Debian,
    	Buntish,
    	ArchLinux,
    	FreeBSD,
    	HasInfo,
    	MetaTypes,
    	type (+),
    	sing,
    	SingI,
    	IncludesInfo,
    	Targets,
    	NonTargets,
    	NotSuperset,
    	Combine,
    	CheckCombine(..),
    	CheckCombinable,
    	type (&&),
    	Not,
    	EqT,
    	Union,
    ) where

    import Propellor.Types.Singletons
    import Propellor.Types.OS

    data MetaType
    	= Targeting TargetOS -- ^ A target OS of a Property
    	| WithInfo           -- ^ Indicates that a Property has associated Info
    	deriving (Show, Eq, Ord)

    -- | Any unix-like system
    type UnixLike = MetaTypes
    	'[ 'Targeting 'OSDebian
    	, 'Targeting 'OSBuntish
    	, 'Targeting 'OSArchLinux
    	, 'Targeting 'OSFreeBSD
    	]

    -- | Any linux system
    type Linux = MetaTypes
    	'[ 'Targeting 'OSDebian
    	, 'Targeting 'OSBuntish
    	, 'Targeting 'OSArchLinux
    	]

    -- | Debian and derivatives.
    type DebianLike = MetaTypes '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish ]
    type Debian = MetaTypes '[ 'Targeting 'OSDebian ]
    type Buntish = MetaTypes '[ 'Targeting 'OSBuntish ]
    type FreeBSD = MetaTypes '[ 'Targeting 'OSFreeBSD ]
    type ArchLinux = MetaTypes '[ 'Targeting 'OSArchLinux ]

    -- | Used to indicate that a Property adds Info to the Host where it's used.
    type HasInfo = MetaTypes '[ 'WithInfo ]

    type family IncludesInfo t :: Bool
    type instance IncludesInfo (MetaTypes l) = Elem 'WithInfo l

    type MetaTypes = Sing

    -- This boilerplate would not be needed if the singletons library were
    -- used. However, we're targeting too old a version of ghc to use it yet.
    data instance Sing (x :: MetaType) where
    	OSDebianS :: Sing ('Targeting 'OSDebian)
    	OSBuntishS :: Sing ('Targeting 'OSBuntish)
    	OSFreeBSDS :: Sing ('Targeting 'OSFreeBSD)
    	OSArchLinuxS :: Sing ('Targeting 'OSArchLinux)
    	WithInfoS :: Sing 'WithInfo
    instance SingI ('Targeting 'OSDebian) where sing = OSDebianS
    instance SingI ('Targeting 'OSBuntish) where sing = OSBuntishS
    instance SingI ('Targeting 'OSFreeBSD) where sing = OSFreeBSDS
    instance SingI ('Targeting 'OSArchLinux) where sing = OSArchLinuxS
    instance SingI 'WithInfo where sing = WithInfoS
    instance SingKind ('KProxy :: KProxy MetaType) where
    	type DemoteRep ('KProxy :: KProxy MetaType) = MetaType
    	fromSing OSDebianS = Targeting OSDebian
    	fromSing OSBuntishS = Targeting OSBuntish
    	fromSing OSFreeBSDS = Targeting OSFreeBSD
    	fromSing OSArchLinuxS = Targeting OSArchLinux
    	fromSing WithInfoS = WithInfo

    -- | Convenience type operator to combine two `MetaTypes` lists.
    --
    -- For example:
    --
    -- > HasInfo + Debian
    --
    -- Which is shorthand for this type:
    --
    -- > MetaTypes '[WithInfo, Targeting OSDebian]
    type family a + b :: ab
    type instance (MetaTypes a) + (MetaTypes b) = MetaTypes (Concat a b)

    type family Concat (list1 :: [a]) (list2 :: [a]) :: [a]
    type instance Concat '[] bs = bs
    type instance Concat (a ': as) bs = a ': (Concat as bs)

    -- | Combine two MetaTypes lists, yielding a list
    -- that has targets present in both, and nontargets present in either.
    type family Combine (list1 :: [a]) (list2 :: [a]) :: [a]
    type instance Combine (list1 :: [a]) (list2 :: [a]) =
    	(Concat
    		(NonTargets list1 `Union` NonTargets list2)
    		(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:
    --
    -- > foo :: (CheckCombinable x y ~ 'CanCombine) => x -> y -> Combine x y
    type family CheckCombinable (list1 :: [a]) (list2 :: [a]) :: CheckCombine
    -- 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.
    type instance CheckCombinable '[] list2 = 'CanCombine
    type instance CheckCombinable list1 '[] = 'CanCombine
    type instance CheckCombinable (l1 ': list1) (l2 ': list2) =
    	CheckCombinable' (Combine (l1 ': list1) (l2 ': list2))
    type family CheckCombinable' (combinedlist :: [a]) :: CheckCombine
    type instance CheckCombinable' '[] = 'CannotCombineTargets
    type instance CheckCombinable' (a ': rest)
    	= If (IsTarget a)
    		'CanCombine
    		(CheckCombinable' rest)

    data CheckCombine = CannotCombineTargets | CanCombine

    -- | 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
    type instance NotSuperset superset '[] = 'CanCombine
    type instance NotSuperset superset (s ': rest) =
    	If (Elem s superset)
    		(NotSuperset superset rest)
    		'CannotCombineTargets

    type family IsTarget (a :: t) :: Bool
    type instance IsTarget ('Targeting a) = 'True
    type instance IsTarget 'WithInfo = 'False

    type family Targets (l :: [a]) :: [a]
    type instance Targets '[] = '[]
    type instance Targets (x ': xs) =
    	If (IsTarget x)
    		(x ': Targets xs)
    		(Targets xs)

    type family NonTargets (l :: [a]) :: [a]
    type instance NonTargets '[] = '[]
    type instance NonTargets (x ': xs) =
    	If (IsTarget x)
    		(NonTargets xs)
    		(x ': NonTargets xs)

    -- | Type level elem
    type family Elem (a :: t) (list :: [t]) :: Bool
    type instance Elem a '[] = 'False
    type instance Elem a (b ': bs) = EqT a b || Elem a bs

    -- | Type level union.
    type family Union (list1 :: [a]) (list2 :: [a]) :: [a]
    type instance Union '[] list2 = list2
    type instance Union (a ': rest) list2 =
    	If (Elem a list2 || Elem a rest)
    		(Union rest list2)
    		(a ': Union rest list2)

    -- | Type level intersection. Duplicate list items are eliminated.
    type family Intersect (list1 :: [a]) (list2 :: [a]) :: [a]
    type instance Intersect '[] list2 = '[]
    type instance Intersect (a ': rest) list2 =
    	If (Elem a list2 && Not (Elem a rest))
    		(a ': Intersect rest list2)
    		(Intersect rest list2)

    -- | Type level equality
    --
    -- This is a very clumsy implmentation, but it works back to ghc 7.6.
    type family EqT (a :: t) (b :: t) :: Bool
    type instance EqT ('Targeting a) ('Targeting b)  = EqT a b
    type instance EqT 'WithInfo      'WithInfo       = 'True
    type instance EqT 'WithInfo      ('Targeting b)  = 'False
    type instance EqT ('Targeting a) 'WithInfo       = 'False
    type instance EqT 'OSDebian  'OSDebian  = 'True
    type instance EqT 'OSBuntish 'OSBuntish = 'True
    type instance EqT 'OSFreeBSD 'OSFreeBSD = 'True
    type instance EqT 'OSDebian  'OSBuntish = 'False
    type instance EqT 'OSDebian  'OSFreeBSD = 'False
    type instance EqT 'OSBuntish 'OSDebian  = 'False
    type instance EqT 'OSBuntish 'OSFreeBSD = 'False
    type instance EqT 'OSFreeBSD 'OSDebian  = 'False
    type instance EqT 'OSFreeBSD 'OSBuntish = 'False
    type instance EqT 'OSArchLinux 'OSArchLinux = 'True
    type instance EqT 'OSArchLinux 'OSDebian    = 'False
    type instance EqT 'OSArchLinux 'OSBuntish   = 'False
    type instance EqT 'OSArchLinux 'OSFreeBSD   = 'False
    type instance EqT 'OSDebian    'OSArchLinux = 'False
    type instance EqT 'OSBuntish   'OSArchLinux = 'False
    type instance EqT 'OSFreeBSD   'OSArchLinux = 'False

    -- More modern version if the combinatiorial explosion gets too bad later:
    --
    -- type family Eq (a :: MetaType) (b :: MetaType) where
    -- 	Eq a a = True
    -- 	Eq a b = False

    -- | An equivilant to the following is in Data.Type.Bool in
    -- modern versions of ghc, but is included here to support ghc 7.6.
    type family If (cond :: Bool) (tru :: a) (fls :: a) :: a
    type instance If 'True  tru fls = tru
    type instance If 'False tru fls = fls
    type family (a :: Bool) || (b :: Bool) :: Bool
    type instance    'False || 'False = 'False
    type instance    'True  || 'True  = 'True
    type instance    'True  || 'False = 'True
    type instance    'False || 'True  = 'True
    type family (a :: Bool) && (b :: Bool) :: Bool
    type instance    'False && 'False = 'False
    type instance    'True  && 'True  = 'True
    type instance    'True  && 'False = 'False
    type instance    'False && 'True  = 'False
    type family Not (a :: Bool) :: Bool
    type instance Not 'False = 'True
    type instance Not 'True = 'False