This module is an internal GHC module. It declares the constants used in the implementation of type-level natural numbers. The programmer interface for working with type-level naturals should be defined in a separate library.
(Kind) This is the kind of type-level natural numbers.
(Kind) This is the kind of type-level symbols. Declared here because class IP needs it
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.
This class gives the string associated with a type-level symbol. There are instances of the class for every concrete literal: "hello", etc.
This type represents unknown type-level natural numbers.
This type represents unknown type-level symbols.
Convert an integer into an unknown type-level natural.
Convert a string into an unknown type-level symbol.
We either get evidence that this function was instantiated with the same type-level numbers, or
We either get evidence that this function was instantiated with the same type-level symbols, or
Comparison of type-level naturals, as a constraint.
Comparison of type-level naturals, as a function. NOTE: The functionality for this function should be subsumed by
CmpNat, so this might go away in the future. Please let us know, if you encounter discrepancies between the two.
Addition of type-level naturals.
Multiplication of type-level naturals.
Exponentiation of type-level naturals.
Subtraction of type-level naturals.
Comparison of type-level naturals, as a function.
Comparison of type-level symbols, as a function.
The type-level equivalent of
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-existant instance,
-- in a context instance TypeError (Text "Cannot
Showfunctions." :$$: 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.")
A description of a custom type error.
© The University of Glasgow and others
Licensed under a BSD-style license (see top of the page).