{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
module Data.Some.Constraint where
import Data.Kind
type AllC :: forall k. [k -> Constraint] -> k -> Constraint
type family AllC cs k :: Constraint where
AllC '[] k = ()
AllC (c ': cs) k = (c k, AllC cs k)
data Somes cs where
Some :: forall
(cs :: [Type -> Constraint])
(a :: Type).
AllC cs a => a -> Somes cs
type Some c = Somes '[c]
data Somes1 csf csa where
Some1 :: forall
k
(csf :: [(k -> Type) -> Constraint])
(csa :: [k -> Constraint])
(f :: k -> Type)
(a :: k).
(AllC csf f, AllC csa a) => f a -> Somes1 csf csa
type Some1 ca cf = Somes1 '[ca] '[cf]