GHC.TypeLits

A description of a custom type error.

Natural number

Invariant: numbers <= 0xffffffffffffffff use the NS constructor

Exponentiation of type-level naturals.

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.")

Multiplication of type-level naturals.

Addition of type-level naturals.

Comparison (<=) of comparable types, as a constraint.

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

Subtraction of type-level naturals.

A type synonym for Natural.

Previously, this was an opaque data type, but it was changed to a type synonym.

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.

Log base 2 (round down) of natural numbers. Log 0 is undefined (i.e., it cannot be reduced).

Modulus of natural numbers. Mod x 0 is undefined (i.e., it cannot be reduced).

Division (round down) of natural numbers. Div x 0 is undefined (i.e., it cannot be reduced).

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

Convert a Unicode code point to a character (cf. chr)

Convert a character to its Unicode code point (cf. ord)

This type family yields type-level Just storing the first character of a symbol and its tail if it is defined and Nothing otherwise.

Extending a type-level symbol with a type-level character

Concatenation of type-level symbols.

A value-level witness for a type-level natural number. This is commonly referred to as a singleton type, as for each n, there is a single value that inhabits the type SNat n (aside from bottom).

The definition of SNat is intentionally left abstract. To obtain an SNat value, use one of the following:

1. The natSing method of KnownNat.

2. The SNat pattern synonym.

3. The withSomeSNat function, which creates an SNat from a Natural number.

A explicitly bidirectional pattern synonym relating an SNat to a KnownNat constraint.

As an expression: Constructs an explicit SNat n value from an implicit KnownNat n constraint:

SNat @n :: KnownNat n => SNat n

As a pattern: Matches on an explicit SNat n value bringing an implicit KnownNat n constraint into scope:

f :: SNat n -> ..
f SNat = {- KnownNat n in scope -}

Like sameNat, but if the numbers aren't equal, this additionally provides proof of LT or GT.

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

Return the Integer corresponding to n in an SNat n value. The returned Integer is always non-negative.

For a version of this function that returns a Natural instead of an Integer, see fromSNat in GHC.TypeNats.

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

Convert an integer into an unknown type-level natural.

Convert an explicit SNat n value into an implicit KnownNat n constraint.

Attempt to convert an Integer into an SNat n value, where n is a fresh type-level natural number. If the Integer argument is non-negative, invoke the continuation with Just sn, where sn is the SNat n value. If the Integer argument is negative, invoke the continuation with Nothing.

For a version of this function where the continuation uses 'SNat n instead of Maybe (SNat n)@, see withSomeSNat in GHC.TypeNats.

Comparison (<=) of comparable types, as a function.

This type represents unknown type-level natural numbers.

Comparison of type-level naturals, as a function.

Ordering data type for type literals that provides proof of their ordering.

A value-level witness for a type-level character. This is commonly referred to as a singleton type, as for each c, there is a single value that inhabits the type SChar c (aside from bottom).

The definition of SChar is intentionally left abstract. To obtain an SChar value, use one of the following:

1. The charSing method of KnownChar.

2. The SChar pattern synonym.

3. The withSomeSChar function, which creates an SChar from a Char.

A explicitly bidirectional pattern synonym relating an SChar to a KnownChar constraint.

As an expression: Constructs an explicit SChar c value from an implicit KnownChar c constraint:

SChar @c :: KnownChar c => SChar c

As a pattern: Matches on an explicit SChar c value bringing an implicit KnownChar c constraint into scope:

f :: SChar c -> ..
f SChar = {- KnownChar c in scope -}

A value-level witness for a type-level symbol. This is commonly referred to as a singleton type, as for each s, there is a single value that inhabits the type SSymbol s (aside from bottom).

The definition of SSymbol is intentionally left abstract. To obtain an SSymbol value, use one of the following:

1. The symbolSing method of KnownSymbol.

2. The SSymbol pattern synonym.

3. The withSomeSSymbol function, which creates an SSymbol from a String.

A explicitly bidirectional pattern synonym relating an SSymbol to a KnownSymbol constraint.

As an expression: Constructs an explicit SSymbol s value from an implicit KnownSymbol s constraint:

SSymbol @s :: KnownSymbol s => SSymbol s

As a pattern: Matches on an explicit SSymbol s value bringing an implicit KnownSymbol s constraint into scope:

f :: SSymbol s -> ..
f SSymbol = {- KnownSymbol s in scope -}

Like sameChar, but if the Chars aren't equal, this additionally provides proof of LT or GT.

Like sameSymbol, but if the symbols aren't equal, this additionally provides proof of LT or GT.

We either get evidence that this function was instantiated with the same type-level characters, or that the type-level characters are distinct.

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

Return the Char corresponding to c in an SChar c value.

Return the String corresponding to s in an SSymbol s value.

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

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

Convert a character into an unknown type-level char.

Convert a string into an unknown type-level symbol.

Convert an explicit SChar c value into an implicit KnownChar c constraint.

Convert an explicit SSymbol s value into an implicit KnownSymbol s constraint.

Convert a Char into an SChar c value, where c is a fresh type-level character.

Convert a String into an SSymbol s value, where s is a fresh type-level symbol.

This type represents unknown type-level symbols.

Comparison of type-level characters.

Comparison of type-level symbols, as a function.