{-# LANGUAGE PolyKinds #-} -- | Constraints for indexed datatypes. -- -- This module contains code that helps to specify that all -- elements of an indexed structure must satisfy a particular -- constraint. -- module Generics.SOP.Constraint ( module Generics.SOP.Constraint , Constraint ) where import GHC.Exts (Constraint) import Generics.SOP.Sing -- | Require a constraint for every element of a list. -- -- If you have a datatype that is indexed over a type-level -- list, then you can use 'All' to indicate that all elements -- of that type-level list must satisfy a given constraint. -- -- /Example:/ The constraint -- -- > All Eq '[ Int, Bool, Char ] -- -- is equivalent to the constraint -- -- > (Eq Int, Eq Bool, Eq Char) -- -- /Example:/ A type signature such as -- -- > f :: All Eq xs => NP I xs -> ... -- -- means that 'f' can assume that all elements of the n-ary -- product satisfy 'Eq'. -- type family All (c :: k -> Constraint) (xs :: [k]) :: Constraint type instance All c '[] = () type instance All c (x ': xs) = (c x, All c xs) -- | Require a constraint for every element of a list of lists. -- -- If you have a datatype that is indexed over a type-level -- list of lists, then you can use 'All2' to indicate that all -- elements of the innert lists must satisfy a given constraint. -- -- /Example:/ The constraint -- -- > All2 Eq '[ '[ Int ], '[ Bool, Char ] ] -- -- is equivalent to the constraint -- -- > (Eq Int, Eq Bool, Eq Char) -- -- /Example:/ A type signature such as -- -- > f :: All2 Eq xss => SOP I xs -> ... -- -- means that 'f' can assume that all elements of the sum -- of product satisfy 'Eq'. -- type family All2 (c :: k -> Constraint) (xs :: [[k]]) :: Constraint type instance All2 c '[] = () type instance All2 c (x ': xs) = (All c x, All2 c xs) -- | A type-level 'map'. type family Map (f :: k -> l) (xs :: [k]) :: [l] type instance Map f '[] = '[] type instance Map f (x ': xs) = f x ': Map f xs -- | A generalization of 'All' and 'All2'. -- -- The family 'AllMap' expands to 'All' or 'All2' depending on whether -- the argument is indexed by a list or a list of lists. -- type family AllMap (h :: (k -> *) -> (l -> *)) (c :: k -> Constraint) (xs :: l) :: Constraint -- | Dictionary for a constraint for all elements of a type-level list. -- -- A value of type @'AllDict' c xs@ captures the constraint @'All' c xs@. -- data AllDict (c :: k -> Constraint) (xs :: [k]) where AllDictC :: (SingI xs, All c xs) => AllDict c xs