GHC.TypeLits

GHC's DataKinds language extension lifts data constructors, natural numbers, and strings to the type level. This module provides the primitives needed for working with type-level numbers (the Nat kind), strings (the Symbol kind), and characters (the Char kind). It also defines the TypeError type family, a feature that makes use of type-level strings to support user defined type errors.

For now, this module is the API for working with type-level literals. However, please note that it is a work in progress and is subject to change. Once the design of the DataKinds feature is more stable, this will be considered only an internal GHC module, and the programmer interface for working with type-level data will be defined in a separate library.

Since: base-4.6.0.0

Kinds

data Natural

Instances

PrintfArg Natural

Since: base-4.8.0.0

Defined in Text.Printf

Methods

formatArg :: Natural -> FieldFormatter

parseFormat :: Natural -> ModifierParser

Bits Natural

Since: base-4.8.0

Defined in GHC.Internal.Bits

Methods

(.&.) :: Natural -> Natural -> Natural

(.|.) :: Natural -> Natural -> Natural

xor :: Natural -> Natural -> Natural

complement :: Natural -> Natural

shift :: Natural -> Int -> Natural

rotate :: Natural -> Int -> Natural

zeroBits :: Natural

bit :: Int -> Natural

setBit :: Natural -> Int -> Natural

clearBit :: Natural -> Int -> Natural

complementBit :: Natural -> Int -> Natural

testBit :: Natural -> Int -> Bool

bitSizeMaybe :: Natural -> Maybe Int

bitSize :: Natural -> Int

isSigned :: Natural -> Bool

shiftL :: Natural -> Int -> Natural

unsafeShiftL :: Natural -> Int -> Natural

shiftR :: Natural -> Int -> Natural

unsafeShiftR :: Natural -> Int -> Natural

rotateL :: Natural -> Int -> Natural

rotateR :: Natural -> Int -> Natural

popCount :: Natural -> Int

Data Natural

Since: base-4.8.0.0

Defined in GHC.Internal.Data.Data

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Natural -> c Natural

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Natural

toConstr :: Natural -> Constr

dataTypeOf :: Natural -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Natural)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Natural)

gmapT :: (forall b. Data b => b -> b) -> Natural -> Natural

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Natural -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Natural -> r

gmapQ :: (forall d. Data d => d -> u) -> Natural -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Natural -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Natural -> m Natural

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Natural -> m Natural

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Natural -> m Natural

Enum Natural

Since: base-4.8.0.0

Defined in GHC.Internal.Enum

Methods

succ :: Natural -> Natural

pred :: Natural -> Natural

toEnum :: Int -> Natural

fromEnum :: Natural -> Int

enumFrom :: Natural -> [Natural]

enumFromThen :: Natural -> Natural -> [Natural]

enumFromTo :: Natural -> Natural -> [Natural]

enumFromThenTo :: Natural -> Natural -> Natural -> [Natural]

Ix Natural

Since: base-4.8.0.0

Defined in GHC.Internal.Ix

Methods

range :: (Natural, Natural) -> [Natural]

index :: (Natural, Natural) -> Natural -> Int

unsafeIndex :: (Natural, Natural) -> Natural -> Int

inRange :: (Natural, Natural) -> Natural -> Bool

rangeSize :: (Natural, Natural) -> Int

unsafeRangeSize :: (Natural, Natural) -> Int

Num Natural

Note that Natural's Num instance isn't a ring: no element but 0 has an additive inverse. It is a semiring though.

Since: base-4.8.0.0

Defined in GHC.Internal.Num

Methods

(+) :: Natural -> Natural -> Natural

(-) :: Natural -> Natural -> Natural

(*) :: Natural -> Natural -> Natural

negate :: Natural -> Natural

abs :: Natural -> Natural

signum :: Natural -> Natural

fromInteger :: Integer -> Natural

Read Natural

Since: base-4.8.0.0

Defined in GHC.Internal.Read

Methods

readsPrec :: Int -> ReadS Natural

readList :: ReadS [Natural]

readPrec :: ReadPrec Natural

readListPrec :: ReadPrec [Natural]

Integral Natural

Since: base-4.8.0.0

Defined in GHC.Internal.Real

Methods

quot :: Natural -> Natural -> Natural

rem :: Natural -> Natural -> Natural

div :: Natural -> Natural -> Natural

mod :: Natural -> Natural -> Natural

quotRem :: Natural -> Natural -> (Natural, Natural)

divMod :: Natural -> Natural -> (Natural, Natural)

toInteger :: Natural -> Integer

Real Natural

Since: base-4.8.0.0

Defined in GHC.Internal.Real

Methods

toRational :: Natural -> Rational

Show Natural

Since: base-4.8.0.0

Defined in GHC.Internal.Show

Methods

showsPrec :: Int -> Natural -> ShowS

show :: Natural -> String

showList :: [Natural] -> ShowS

Eq Natural

Defined in GHC.Num.Natural

Methods

(==) :: Natural -> Natural -> Bool

(/=) :: Natural -> Natural -> Bool

Ord Natural

Defined in GHC.Num.Natural

Methods

compare :: Natural -> Natural -> Ordering

(<) :: Natural -> Natural -> Bool

(<=) :: Natural -> Natural -> Bool

(>) :: Natural -> Natural -> Bool

(>=) :: Natural -> Natural -> Bool

max :: Natural -> Natural -> Natural

min :: Natural -> Natural -> Natural

KnownNat n => HasResolution (n :: Nat)

For example, Fixed 1000 will give you a Fixed with a resolution of 1000.

Defined in Data.Fixed

Methods

resolution :: p n -> Integer

TestCoercion SNat

Since: base-4.18.0.0

Defined in GHC.Internal.TypeNats

Methods

testCoercion :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (Coercion a b)

TestEquality SNat

Since: base-4.18.0.0

Defined in GHC.Internal.TypeNats

Methods

testEquality :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b)

Lift Natural

Defined in GHC.Internal.TH.Lift

Methods

lift :: Quote m => Natural -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => Natural -> Code m Natural

type Compare (a :: Natural) (b :: Natural)

Defined in GHC.Internal.Data.Type.Ord

type Compare (a :: Natural) (b :: Natural) = CmpNat a b

type Nat = Natural

A type synonym for Natural.

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

Since: base-4.16.0.0

data Symbol

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

Instances

SingKind Symbol

Since: base-4.9.0.0

Defined in GHC.Internal.Generics

Associated Types

type DemoteRep Symbol

Defined in GHC.Internal.Generics

type DemoteRep Symbol = String

Methods

fromSing :: forall (a :: Symbol). Sing a -> DemoteRep Symbol

TestCoercion SSymbol

Since: base-4.18.0.0

Defined in GHC.Internal.TypeLits

Methods

testCoercion :: forall (a :: Symbol) (b :: Symbol). SSymbol a -> SSymbol b -> Maybe (Coercion a b)

TestEquality SSymbol

Since: base-4.18.0.0

Defined in GHC.Internal.TypeLits

Methods

testEquality :: forall (a :: Symbol) (b :: Symbol). SSymbol a -> SSymbol b -> Maybe (a :~: b)

KnownSymbol a => SingI (a :: Symbol)

Since: base-4.9.0.0

Defined in GHC.Internal.Generics

Methods

sing :: Sing a

type DemoteRep Symbol

Defined in GHC.Internal.Generics

type DemoteRep Symbol = String

data Sing (s :: Symbol)

Defined in GHC.Internal.Generics

data Sing (s :: Symbol) where

• SSym :: forall (s :: Symbol). KnownSymbol s => Sing s

type Compare (a :: Symbol) (b :: Symbol)

Defined in GHC.Internal.Data.Type.Ord

type Compare (a :: Symbol) (b :: Symbol) = CmpSymbol a b

Linking type and value level

class KnownNat (n :: Nat) where

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

Methods

natSing :: SNat n

natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Integer

Since: base-4.7.0.0

natVal' :: forall (n :: Nat). KnownNat n => Proxy# n -> Integer

Since: base-4.8.0.0

class KnownSymbol (n :: Symbol) where

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

Methods

symbolSing :: SSymbol n

symbolVal :: forall (n :: Symbol) proxy. KnownSymbol n => proxy n -> String

Since: base-4.7.0.0

symbolVal' :: forall (n :: Symbol). KnownSymbol n => Proxy# n -> String

Since: base-4.8.0.0

class KnownChar (n :: Char) where

Since: base-4.16.0.0

Methods

charSing :: SChar n

charVal :: forall (n :: Char) proxy. KnownChar n => proxy n -> Char

charVal' :: forall (n :: Char). KnownChar n => Proxy# n -> Char

data SomeNat

This type represents unknown type-level natural numbers.

Since: base-4.10.0.0

Constructors

KnownNat n => SomeNat (Proxy n)

Instances

Read SomeNat

Since: base-4.7.0.0

Defined in GHC.Internal.TypeNats

Methods

readsPrec :: Int -> ReadS SomeNat

readList :: ReadS [SomeNat]

readPrec :: ReadPrec SomeNat

readListPrec :: ReadPrec [SomeNat]

Show SomeNat

Since: base-4.7.0.0

Defined in GHC.Internal.TypeNats

Methods

showsPrec :: Int -> SomeNat -> ShowS

show :: SomeNat -> String

showList :: [SomeNat] -> ShowS

Eq SomeNat

Since: base-4.7.0.0

Defined in GHC.Internal.TypeNats

Methods

(==) :: SomeNat -> SomeNat -> Bool

(/=) :: SomeNat -> SomeNat -> Bool

Ord SomeNat

Since: base-4.7.0.0

Defined in GHC.Internal.TypeNats

Methods

compare :: SomeNat -> SomeNat -> Ordering

(<) :: SomeNat -> SomeNat -> Bool

(<=) :: SomeNat -> SomeNat -> Bool

(>) :: SomeNat -> SomeNat -> Bool

(>=) :: SomeNat -> SomeNat -> Bool

max :: SomeNat -> SomeNat -> SomeNat

min :: SomeNat -> SomeNat -> SomeNat

data SomeSymbol

This type represents unknown type-level symbols.

Constructors

KnownSymbol n => SomeSymbol (Proxy n)

Since: base-4.7.0.0

Instances

Read SomeSymbol

Since: base-4.7.0.0

Defined in GHC.Internal.TypeLits

Methods

readsPrec :: Int -> ReadS SomeSymbol

readList :: ReadS [SomeSymbol]

readPrec :: ReadPrec SomeSymbol

readListPrec :: ReadPrec [SomeSymbol]

Show SomeSymbol

Since: base-4.7.0.0

Defined in GHC.Internal.TypeLits

Methods

showsPrec :: Int -> SomeSymbol -> ShowS

show :: SomeSymbol -> String

showList :: [SomeSymbol] -> ShowS

Eq SomeSymbol

Since: base-4.7.0.0

Defined in GHC.Internal.TypeLits

Methods

(==) :: SomeSymbol -> SomeSymbol -> Bool

(/=) :: SomeSymbol -> SomeSymbol -> Bool

Ord SomeSymbol

Since: base-4.7.0.0

Defined in GHC.Internal.TypeLits

Methods

compare :: SomeSymbol -> SomeSymbol -> Ordering

(<) :: SomeSymbol -> SomeSymbol -> Bool

(<=) :: SomeSymbol -> SomeSymbol -> Bool

(>) :: SomeSymbol -> SomeSymbol -> Bool

(>=) :: SomeSymbol -> SomeSymbol -> Bool

max :: SomeSymbol -> SomeSymbol -> SomeSymbol

min :: SomeSymbol -> SomeSymbol -> SomeSymbol

data SomeChar

Constructors

KnownChar n => SomeChar (Proxy n)

Instances

Read SomeChar

Defined in GHC.Internal.TypeLits

Methods

readsPrec :: Int -> ReadS SomeChar

readList :: ReadS [SomeChar]

readPrec :: ReadPrec SomeChar

readListPrec :: ReadPrec [SomeChar]

Show SomeChar

Defined in GHC.Internal.TypeLits

Methods

showsPrec :: Int -> SomeChar -> ShowS

show :: SomeChar -> String

showList :: [SomeChar] -> ShowS

Eq SomeChar

Defined in GHC.Internal.TypeLits

Methods

(==) :: SomeChar -> SomeChar -> Bool

(/=) :: SomeChar -> SomeChar -> Bool

Ord SomeChar

Defined in GHC.Internal.TypeLits

Methods

compare :: SomeChar -> SomeChar -> Ordering

(<) :: SomeChar -> SomeChar -> Bool

(<=) :: SomeChar -> SomeChar -> Bool

(>) :: SomeChar -> SomeChar -> Bool

(>=) :: SomeChar -> SomeChar -> Bool

max :: SomeChar -> SomeChar -> SomeChar

min :: SomeChar -> SomeChar -> SomeChar

someNatVal :: Integer -> Maybe SomeNat

Convert an integer into an unknown type-level natural.

Since: base-4.7.0.0

someSymbolVal :: String -> SomeSymbol

Convert a string into an unknown type-level symbol.

Since: base-4.7.0.0

someCharVal :: Char -> SomeChar

Convert a character into an unknown type-level char.

Since: base-4.16.0.0

sameNat :: forall (a :: Nat) (b :: Nat) proxy1 proxy2. (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> Maybe (a :~: b)

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

Since: base-4.7.0.0

sameSymbol :: forall (a :: Symbol) (b :: Symbol) proxy1 proxy2. (KnownSymbol a, KnownSymbol b) => proxy1 a -> proxy2 b -> Maybe (a :~: b)

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

Since: base-4.7.0.0

sameChar :: forall (a :: Char) (b :: Char) proxy1 proxy2. (KnownChar a, KnownChar b) => proxy1 a -> proxy2 b -> Maybe (a :~: b)

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

Since: base-4.16.0.0

decideNat :: forall (a :: Nat) (b :: Nat) proxy1 proxy2. (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> Either ((a :~: b) -> Void) (a :~: b)

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

Since: base-4.19.0.0

decideSymbol :: forall (a :: Symbol) (b :: Symbol) proxy1 proxy2. (KnownSymbol a, KnownSymbol b) => proxy1 a -> proxy2 b -> Either ((a :~: b) -> Void) (a :~: b)

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

Since: base-4.19.0.0

decideChar :: forall (a :: Char) (b :: Char) proxy1 proxy2. (KnownChar a, KnownChar b) => proxy1 a -> proxy2 b -> Either ((a :~: b) -> Void) (a :~: b)

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

Since: base-4.19.0.0

data OrderingI (a :: k) (b :: k) where

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

Since: base-4.16.0.0

Constructors

LTI :: forall {k} (a :: k) (b :: k). Compare a b ~ 'LT => OrderingI a b

EQI :: forall {k} (a :: k). Compare a a ~ 'EQ => OrderingI a a

GTI :: forall {k} (a :: k) (b :: k). Compare a b ~ 'GT => OrderingI a b

Instances

Show (OrderingI a b)

Defined in GHC.Internal.Data.Type.Ord

Methods

showsPrec :: Int -> OrderingI a b -> ShowS

show :: OrderingI a b -> String

showList :: [OrderingI a b] -> ShowS

Eq (OrderingI a b)

Defined in GHC.Internal.Data.Type.Ord

Methods

(==) :: OrderingI a b -> OrderingI a b -> Bool

(/=) :: OrderingI a b -> OrderingI a b -> Bool

cmpNat :: forall (a :: Nat) (b :: Nat) proxy1 proxy2. (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> OrderingI a b

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

Since: base-4.16.0.0

cmpSymbol :: forall (a :: Symbol) (b :: Symbol) proxy1 proxy2. (KnownSymbol a, KnownSymbol b) => proxy1 a -> proxy2 b -> OrderingI a b

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

Since: base-4.16.0.0

cmpChar :: forall (a :: Char) (b :: Char) proxy1 proxy2. (KnownChar a, KnownChar b) => proxy1 a -> proxy2 b -> OrderingI a b

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

Since: base-4.16.0.0

Singleton values

data SNat (n :: Nat)

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.

Since: base-4.18.0.0

Instances

TestCoercion SNat

Since: base-4.18.0.0

Defined in GHC.Internal.TypeNats

Methods

testCoercion :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (Coercion a b)

TestEquality SNat

Since: base-4.18.0.0

Defined in GHC.Internal.TypeNats

Methods

testEquality :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b)

Show (SNat n)

Since: base-4.18.0.0

Defined in GHC.Internal.TypeNats

Methods

showsPrec :: Int -> SNat n -> ShowS

show :: SNat n -> String

showList :: [SNat n] -> ShowS

Eq (SNat n)

Since: base-4.19.0.0

Defined in GHC.Internal.TypeNats

Methods

(==) :: SNat n -> SNat n -> Bool

(/=) :: SNat n -> SNat n -> Bool

Ord (SNat n)

Since: base-4.19.0.0

Defined in GHC.Internal.TypeNats

Methods

compare :: SNat n -> SNat n -> Ordering

(<) :: SNat n -> SNat n -> Bool

(<=) :: SNat n -> SNat n -> Bool

(>) :: SNat n -> SNat n -> Bool

(>=) :: SNat n -> SNat n -> Bool

max :: SNat n -> SNat n -> SNat n

min :: SNat n -> SNat n -> SNat n

data SSymbol (s :: Symbol)

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.

Since: base-4.18.0.0

Instances

TestCoercion SSymbol

Since: base-4.18.0.0

Defined in GHC.Internal.TypeLits

Methods

testCoercion :: forall (a :: Symbol) (b :: Symbol). SSymbol a -> SSymbol b -> Maybe (Coercion a b)

TestEquality SSymbol

Since: base-4.18.0.0

Defined in GHC.Internal.TypeLits

Methods

testEquality :: forall (a :: Symbol) (b :: Symbol). SSymbol a -> SSymbol b -> Maybe (a :~: b)

Show (SSymbol s)

Since: base-4.18.0.0

Defined in GHC.Internal.TypeLits

Methods

showsPrec :: Int -> SSymbol s -> ShowS

show :: SSymbol s -> String

showList :: [SSymbol s] -> ShowS

Eq (SSymbol s)

Since: base-4.19.0.0

Defined in GHC.Internal.TypeLits

Methods

(==) :: SSymbol s -> SSymbol s -> Bool

(/=) :: SSymbol s -> SSymbol s -> Bool

Ord (SSymbol s)

Since: base-4.19.0.0

Defined in GHC.Internal.TypeLits

Methods

compare :: SSymbol s -> SSymbol s -> Ordering

(<) :: SSymbol s -> SSymbol s -> Bool

(<=) :: SSymbol s -> SSymbol s -> Bool

(>) :: SSymbol s -> SSymbol s -> Bool

(>=) :: SSymbol s -> SSymbol s -> Bool

max :: SSymbol s -> SSymbol s -> SSymbol s

min :: SSymbol s -> SSymbol s -> SSymbol s

data SChar (s :: Char)

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.

Since: base-4.18.0.0

Instances

TestCoercion SChar

Since: base-4.18.0.0

Defined in GHC.Internal.TypeLits

Methods

testCoercion :: forall (a :: Char) (b :: Char). SChar a -> SChar b -> Maybe (Coercion a b)

TestEquality SChar

Since: base-4.18.0.0

Defined in GHC.Internal.TypeLits

Methods

testEquality :: forall (a :: Char) (b :: Char). SChar a -> SChar b -> Maybe (a :~: b)

Show (SChar c)

Since: base-4.18.0.0

Defined in GHC.Internal.TypeLits

Methods

showsPrec :: Int -> SChar c -> ShowS

show :: SChar c -> String

showList :: [SChar c] -> ShowS

Eq (SChar c)

Since: base-4.19.0.0

Defined in GHC.Internal.TypeLits

Methods

(==) :: SChar c -> SChar c -> Bool

(/=) :: SChar c -> SChar c -> Bool

Ord (SChar c)

Since: base-4.19.0.0

Defined in GHC.Internal.TypeLits

Methods

compare :: SChar c -> SChar c -> Ordering

(<) :: SChar c -> SChar c -> Bool

(<=) :: SChar c -> SChar c -> Bool

(>) :: SChar c -> SChar c -> Bool

(>=) :: SChar c -> SChar c -> Bool

max :: SChar c -> SChar c -> SChar c

min :: SChar c -> SChar c -> SChar c

pattern SNat :: () => KnownNat n => SNat n

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 -}

Since: base-4.18.0.0

pattern SSymbol :: () => KnownSymbol s => SSymbol s

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 -}

Since: base-4.18.0.0

pattern SChar :: () => KnownChar c => SChar c

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 -}

Since: base-4.18.0.0

fromSNat :: forall (n :: Nat). SNat n -> Integer

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.

Since: base-4.18.0.0

fromSSymbol :: forall (s :: Symbol). SSymbol s -> String

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

Since: base-4.18.0.0

fromSChar :: forall (c :: Char). SChar c -> Char

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

Since: base-4.18.0.0

withSomeSNat :: Integer -> (forall (n :: Nat). Maybe (SNat n) -> r) -> r

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.

Since: base-4.18.0.0

withSomeSSymbol :: String -> (forall (s :: Symbol). SSymbol s -> r) -> r

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

Since: base-4.18.0.0

withSomeSChar :: Char -> (forall (c :: Char). SChar c -> r) -> r

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

Since: base-4.18.0.0

withKnownNat :: forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r

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

Since: base-4.18.0.0

withKnownSymbol :: forall (s :: Symbol) r. SSymbol s -> (KnownSymbol s => r) -> r

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

Since: base-4.18.0.0

withKnownChar :: forall (c :: Char) r. SChar c -> (KnownChar c => r) -> r

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

Since: base-4.18.0.0

Functions on type literals

type (<=) (x :: t) (y :: t) = Assert (x <=? y) (LeErrMsg x y :: Constraint) infix 4

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

Since: base-4.16.0.0

type (<=?) (m :: k) (n :: k) = OrdCond (Compare m n) 'True 'True 'False infix 4

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

Since: base-4.16.0.0

type family (a :: Natural) + (b :: Natural) :: Natural where ... infixl 6

Addition of type-level naturals.

Since: base-4.7.0.0

type family (a :: Natural) * (b :: Natural) :: Natural where ... infixl 7

Multiplication of type-level naturals.

Since: base-4.7.0.0

type family (a :: Natural) ^ (b :: Natural) :: Natural where ... infixr 8

Exponentiation of type-level naturals.

Since: base-4.7.0.0

type family (a :: Natural) - (b :: Natural) :: Natural where ... infixl 6

Subtraction of type-level naturals.

Since: base-4.7.0.0

type family Div (a :: Natural) (b :: Natural) :: Natural where ... infixl 7

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

Since: base-4.11.0.0

type family Mod (a :: Natural) (b :: Natural) :: Natural where ... infixl 7

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

Since: base-4.11.0.0

type family Log2 (a :: Natural) :: Natural where ...

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

Since: base-4.11.0.0

type family AppendSymbol (a :: Symbol) (b :: Symbol) :: Symbol where ...

Concatenation of type-level symbols.

Since: base-4.10.0.0

type family CmpNat (a :: Natural) (b :: Natural) :: Ordering where ...

Comparison of type-level naturals, as a function.

Since: base-4.7.0.0

type family CmpSymbol (a :: Symbol) (b :: Symbol) :: Ordering where ...

Comparison of type-level symbols, as a function.

Since: base-4.7.0.0

type family CmpChar (a :: Char) (b :: Char) :: Ordering where ...

Comparison of type-level characters.

Since: base-4.16.0.0

type family ConsSymbol (a :: Char) (b :: Symbol) :: Symbol where ...

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

Since: base-4.16.0.0

type family UnconsSymbol (a :: Symbol) :: Maybe (Char, Symbol) where ...

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

Since: base-4.16.0.0

type family CharToNat (a :: Char) :: Natural where ...

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

Since: base-4.16.0.0

type family NatToChar (a :: Natural) :: Char where ...

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

Since: base-4.16.0.0

User-defined type errors

type family TypeError (a :: ErrorMessage) :: b where ...

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

data ErrorMessage

A description of a custom type error.

Constructors

Text Symbol

Show the text as is.

ShowType t

Pretty print the type. ShowType :: k -> ErrorMessage

ErrorMessage :<>: ErrorMessage infixl 6

Put two pieces of error message next to each other.

ErrorMessage :$$: ErrorMessage infixl 5

Stack two pieces of error message on top of each other.