Frames.TypeLevel

Helpers for working with type-level lists.

Documentation

type family RDelete r rs where ...

Remove the first occurence of a type from a type-level list.

Equations

RDelete r (r ': rs) = rs

RDelete r (s ': rs) = s ': RDelete r rs

type family LAll c ts :: Constraint where ...

A constraint on each element of a type-level list.

Equations

LAll c '[] = ()

LAll c (t ': ts) = (c t, LAll c ts)

type family AllAre a ts :: Constraint where ...

Constraint that every element of a promoted list is equal to a particular type. That is, the list of types is a single type repeated some number of times.

Equations

AllAre a '[] = ()

AllAre a (t ': ts) = (t ~ a, AllAre a ts)

type family HasInstances a cs :: Constraint where ...

Compound constraint that a type has an instance for each of a list of type classes.

Equations

HasInstances a '[] = ()

HasInstances a (c ': cs) = (c a, HasInstances a cs)

type family AllHave cs as :: Constraint where ...

Compound constraint that all types have instances for each of a list of type clasesses. AllHave classes types.

Equations

AllHave cs '[] = ()

AllHave cs (a ': as) = (HasInstances a cs, AllHave cs as)