ghc-internal-9.1001.0: Basic libraries
Safe HaskellTrustworthy
LanguageHaskell2010

GHC.Internal.TypeLits

Description

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

Synopsis

Kinds

data Natural Source #

Natural number

Invariant: numbers <= 0xffffffffffffffff use the NS constructor

Instances

Instances details
Bits Natural Source #

@since base-4.8.0

Instance details

Defined in GHC.Internal.Bits

Data Natural Source #

@since base-4.8.0.0

Instance details

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 Source #

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

toConstr :: Natural -> Constr Source #

dataTypeOf :: Natural -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Enum Natural Source #

@since base-4.8.0.0

Instance details

Defined in GHC.Internal.Enum

Ix Natural Source #

@since base-4.8.0.0

Instance details

Defined in GHC.Internal.Ix

Num Natural Source #

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

Instance details

Defined in GHC.Internal.Num

Read Natural Source #

@since base-4.8.0.0

Instance details

Defined in GHC.Internal.Read

Integral Natural Source #

@since base-4.8.0.0

Instance details

Defined in GHC.Internal.Real

Real Natural Source #

@since base-4.8.0.0

Instance details

Defined in GHC.Internal.Real

Show Natural Source #

@since base-4.8.0.0

Instance details

Defined in GHC.Internal.Show

Eq Natural 
Instance details

Defined in GHC.Num.Natural

Ord Natural 
Instance details

Defined in GHC.Num.Natural

TestCoercion SNat Source #

@since base-4.18.0.0

Instance details

Defined in GHC.Internal.TypeNats

Methods

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

TestEquality SNat Source #

@since base-4.18.0.0

Instance details

Defined in GHC.Internal.TypeNats

Methods

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

type Compare (a :: Natural) (b :: Natural) Source # 
Instance details

Defined in GHC.Internal.Data.Type.Ord

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

type Nat = Natural Source #

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 Source #

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

Instances

Instances details
TestCoercion SSymbol Source #

@since base-4.18.0.0

Instance details

Defined in GHC.Internal.TypeLits

Methods

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

TestEquality SSymbol Source #

@since base-4.18.0.0

Instance details

Defined in GHC.Internal.TypeLits

Methods

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

type Compare (a :: Symbol) (b :: Symbol) Source # 
Instance details

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 Source #

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 Source #

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

@since base-4.7.0.0

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

@since base-4.8.0.0

class KnownSymbol (n :: Symbol) where Source #

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

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

@since base-4.7.0.0

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

@since base-4.8.0.0

class KnownChar (n :: Char) where Source #

@since base-4.16.0.0

Methods

charSing :: SChar n Source #

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

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

data SomeNat Source #

This type represents unknown type-level natural numbers.

@since base-4.10.0.0

Constructors

KnownNat n => SomeNat (Proxy n) 

Instances

Instances details
Read SomeNat Source #

@since base-4.7.0.0

Instance details

Defined in GHC.Internal.TypeNats

Show SomeNat Source #

@since base-4.7.0.0

Instance details

Defined in GHC.Internal.TypeNats

Eq SomeNat Source #

@since base-4.7.0.0

Instance details

Defined in GHC.Internal.TypeNats

Ord SomeNat Source #

@since base-4.7.0.0

Instance details

Defined in GHC.Internal.TypeNats

data SomeSymbol Source #

This type represents unknown type-level symbols.

Constructors

KnownSymbol n => SomeSymbol (Proxy n)

@since base-4.7.0.0

someNatVal :: Integer -> Maybe SomeNat Source #

Convert an integer into an unknown type-level natural.

@since base-4.7.0.0

someSymbolVal :: String -> SomeSymbol Source #

Convert a string into an unknown type-level symbol.

@since base-4.7.0.0

someCharVal :: Char -> SomeChar Source #

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) Source #

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) Source #

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) Source #

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) Source #

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) Source #

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) Source #

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 Source #

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

Instances details
Show (OrderingI a b) Source # 
Instance details

Defined in GHC.Internal.Data.Type.Ord

Eq (OrderingI a b) Source # 
Instance details

Defined in GHC.Internal.Data.Type.Ord

Methods

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

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

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

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 Source #

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 Source #

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) Source #

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

Instances details
TestCoercion SNat Source #

@since base-4.18.0.0

Instance details

Defined in GHC.Internal.TypeNats

Methods

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

TestEquality SNat Source #

@since base-4.18.0.0

Instance details

Defined in GHC.Internal.TypeNats

Methods

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

Show (SNat n) Source #

@since base-4.18.0.0

Instance details

Defined in GHC.Internal.TypeNats

Methods

showsPrec :: Int -> SNat n -> ShowS Source #

show :: SNat n -> String Source #

showList :: [SNat n] -> ShowS Source #

Eq (SNat n) Source #

@since base-4.19.0.0

Instance details

Defined in GHC.Internal.TypeNats

Methods

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

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

Ord (SNat n) Source #

@since base-4.19.0.0

Instance details

Defined in GHC.Internal.TypeNats

Methods

compare :: SNat n -> SNat n -> Ordering Source #

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

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

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

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

max :: SNat n -> SNat n -> SNat n Source #

min :: SNat n -> SNat n -> SNat n Source #

data SSymbol (s :: Symbol) Source #

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

Instances details
TestCoercion SSymbol Source #

@since base-4.18.0.0

Instance details

Defined in GHC.Internal.TypeLits

Methods

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

TestEquality SSymbol Source #

@since base-4.18.0.0

Instance details

Defined in GHC.Internal.TypeLits

Methods

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

Show (SSymbol s) Source #

@since base-4.18.0.0

Instance details

Defined in GHC.Internal.TypeLits

Eq (SSymbol s) Source #

@since base-4.19.0.0

Instance details

Defined in GHC.Internal.TypeLits

Methods

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

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

Ord (SSymbol s) Source #

@since base-4.19.0.0

Instance details

Defined in GHC.Internal.TypeLits

data SChar (s :: Char) Source #

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

Instances details
TestCoercion SChar Source #

@since base-4.18.0.0

Instance details

Defined in GHC.Internal.TypeLits

Methods

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

TestEquality SChar Source #

@since base-4.18.0.0

Instance details

Defined in GHC.Internal.TypeLits

Methods

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

Show (SChar c) Source #

@since base-4.18.0.0

Instance details

Defined in GHC.Internal.TypeLits

Eq (SChar c) Source #

@since base-4.19.0.0

Instance details

Defined in GHC.Internal.TypeLits

Methods

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

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

Ord (SChar c) Source #

@since base-4.19.0.0

Instance details

Defined in GHC.Internal.TypeLits

Methods

compare :: SChar c -> SChar c -> Ordering Source #

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

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

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

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

max :: SChar c -> SChar c -> SChar c Source #

min :: SChar c -> SChar c -> SChar c Source #

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

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 Source #

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 Source #

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 Source #

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 Source #

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

@since base-4.18.0.0

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

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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

@since base-4.16.0.0

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

Addition of type-level naturals.

@since base-4.7.0.0

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

Multiplication of type-level naturals.

@since base-4.7.0.0

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

Exponentiation of type-level naturals.

@since base-4.7.0.0

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

Subtraction of type-level naturals.

@since base-4.7.0.0

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

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 Source #

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 ... Source #

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 ... Source #

Concatenation of type-level symbols.

@since base-4.10.0.0

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

Comparison of type-level naturals, as a function.

@since base-4.7.0.0

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

Comparison of type-level symbols, as a function.

@since base-4.7.0.0

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

Comparison of type-level characters.

@since base-4.16.0.0

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

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 ... Source #

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 ... Source #

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

@since base-4.16.0.0

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

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 ... Source #

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 Source #

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.