Frames.TypeLevel

Helpers for working with type-level lists.

Documentation

type family RDelete r rs

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

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

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

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

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)