(Kind) This is the kind of type-level natural numbers.

This class gives the integer associated with a type-level natural. There are instances of the class for every concrete literal: 0, 1, 2, etc.

Since: base-4.7.0.0

Since: base-4.7.0.0

Since: base-4.8.0.0

This type represents unknown type-level natural numbers.

Since: base-4.10.0.0

Convert an integer into an unknown type-level natural.

Since: base-4.7.0.0

We either get evidence that this function was instantiated with the same type-level numbers, or Nothing.

Since: base-4.7.0.0

(Kind) An integer that may be negative.

This class gives the (value-level) integer associated with a type-level integer. There are instances of this class for every concrete natural: 0, 1, 2, etc. There are also instances of this class for every negated natural, such as Neg 1.

Get the value associated with a type-level integer

Get the value associated with a type-level integer. The difference between this function and intVal is that it takes a Proxy# parameter, which has zero runtime representation and so is entirely free.

This type represents unknown type-level integers.

Since: 0.1.1

Convert an integer into an unknown type-level integer.

Since: 0.1.1

Type constructor for a rational

This class gives the (value-level) rational associated with a type-level rational. There are instances of this class for every combination of a concrete integer and concrete natural.

Get the value associated with a type-level rational

Get the value associated with a type-level rational. The difference between this function and ratVal is that it takes a Proxy# parameter, which has zero runtime representation and so is entirely free.

This type represents unknown type-level integers.

Since: 0.1.1

Convert a rational into an unknown type-level rational.

Since: 0.1.1

Boolean type-level equals. Useful for e.g. If (x ==? 0)

Boolean type-level not-equals.

Boolean comparison of two type-level numbers

Equality constraint, used as e.g. (x == 3) => _

Not-equal constraint

The sum of two type-level numbers

The difference of two type-level numbers

The product of two type-level numbers.

Due to changes in GHC 8.6, using this operator infix and unqualified requires the NoStarIsType language extension to be active. See the GHC 8.6.x migration guide for details: https://ghc.haskell.org/trac/ghc/wiki/Migration/8.6

Exponentiation of type-level naturals.

Since: base-4.7.0.0

(Kind) This is the kind of type-level symbols. Declared here because class IP needs it

Concatenation of type-level symbols.

Since: base-4.10.0.0

Comparison of type-level symbols, as a function.

Since: base-4.7.0.0

This class gives the string associated with a type-level symbol. There are instances of the class for every concrete literal: "hello", etc.

Since: base-4.7.0.0

Since: base-4.7.0.0

Since: base-4.8.0.0

This type represents unknown type-level symbols.

Convert a string into an unknown type-level symbol.

Since: base-4.7.0.0

We either get evidence that this function was instantiated with the same type-level symbols, or Nothing.

Since: base-4.7.0.0

The type-level equivalent of error.

The polymorphic kind of this type allows it to be used in several settings. For instance, it can be used as a constraint, e.g. to provide a better error message for a non-existent instance,

-- in a context
instance TypeError (Text "Cannot Show functions." :$$:
                    Text "Perhaps there is a missing argument?")
      => Show (a -> b) where
    showsPrec = error "unreachable"

It can also be placed on the right-hand side of a type-level function to provide an error for an invalid case,

type family ByteSize x where
   ByteSize Word16   = 2
   ByteSize Word8    = 1
   ByteSize a        = TypeError (Text "The type " :<>: ShowType a :<>:
                                  Text " is not exportable.")

Since: base-4.9.0.0

A description of a custom type error.