{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
module Options.Harg.Het.All where

import Data.Kind (Type, Constraint)

-- | @All c xs@ returns a constraint which is constructed by
-- applying @c@ to all the types in @xs@.
type family All
    (c :: k -> Constraint)
    (xs :: [k])
    :: Constraint where
  All _ '[]       = ()
  All c (x ': xs) = (c x, All c xs)

-- | @AllF c xs f@ is similar to 'All', but types in @xs@ have the kind @(Type
-- -> Type) -> Type@ so they require an extra @f :: Type -> Type@ in order to
-- be of fully saturated.
type family AllF
    (c :: k -> Constraint)
    (xs :: [(Type -> Type) -> Type])
    (f :: Type -> Type)
    :: Constraint where
  AllF _ '[] _       = ()
  AllF c (x ': xs) f = (c (x f), AllF c xs f)