{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

-- | generic types and type families used in some of the modules
module Data.HTree.Families
  ( All
  , AllC
  , AllInv
  , Both
  , Not
  , Top
  , type (++)
  , type (||)
  )
where

import Data.Kind (Constraint)

-- | like 'Prelude.(++)' on the value level but on the type level
type (++) :: forall k. [k] -> [k] -> [k]
type family xs ++ ys where
  '[] ++ ys = ys
  (x : xs) ++ ys = x : xs ++ ys

-- | typelevel Or
type (||) :: Bool -> Bool -> Bool
type family a || b where
  'True || b = 'True
  'False || b = b

-- | like All but can be partially applied
type AllC :: forall k. (k -> Constraint) -> [k] -> Constraint
class All c xs => AllC c xs

instance All c xs => AllC c xs

-- | for all elements of a list, a contraint holds
type All :: forall k. (k -> Constraint) -> [k] -> Constraint
type family All c xs where
  All c '[] = ()
  All c (x : xs) = (c x, All c xs)

-- | the class that every type has an instance for
type Top :: k -> Constraint
class Top k

instance Top k

-- | like 'not' but on the type level
type Not :: Bool -> Bool
type family Not a where
  Not 'True = 'False
  Not 'False = 'True

infixr 5 ++

-- | 'All' but inversed: holds if all constraints in the list hold
type AllInv :: [k -> Constraint] -> k -> Constraint
class AllInv l k

instance AllInv '[] k

instance (c k, AllInv cs k) => AllInv (c ': cs) k

-- | product of two classes
type Both :: (k -> Constraint) -> (k -> Constraint) -> k -> Constraint
class (c1 a, c2 a) => Both c1 c2 a

instance (c1 a, c2 a) => Both c1 c2 a