GHC.TypeLits

Kinds

data Nat

data Symbol

Linking type and value level

data family Sing n

class SingI a

class SingE kparam

class SingRep a

singByProxy

data SomeSing

class ToSing kp

type SomeNat

type SomeSymbol

Working with singletons

withSing

singThat

Functions on type nats

class m (<=) n

type family m (<=?) n :: Bool

type family m (+) n :: Nat

type family m (*) n :: Nat

type family m (^) n :: Nat

type family m (-) n :: Nat

Comparing for equality

data :~:

eqSingNat

eqSingSym

Destructing type-nat singletons.

isZero

data IsZero

Matching on type-nats

data Nat1

type family FromNat1 n :: Nat

Kind parameters

data KindIs a

type Demote a

type KindOf a