Options.Harg.Het.All

Documentation

type family All (c :: k -> Constraint) (xs :: [k]) :: Constraint where ...

All c xs returns a constraint which is constructed by applying c to all the types in xs.

Equations

All _ '[] = ()

All c (x ': xs) = (c x, All c xs)

type family AllF (c :: k -> Constraint) (xs :: [(Type -> Type) -> Type]) (f :: Type -> Type) :: Constraint where ...

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.

Equations

AllF _ '[] _ = ()

AllF c (x ': xs) f = (c (x f), AllF c xs f)