Data.Singletons.TypeLits

Defines and exports singletons useful for the Nat and Symbol kinds.

Documentation

data Nat :: *

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

Instances

SNum Nat

Methods

(%:+) :: Sing Nat t -> Sing Nat t -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:+$) Nat) t) t)

(%:-) :: Sing Nat t -> Sing Nat t -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:-$) Nat) t) t)

(%:*) :: Sing Nat t -> Sing Nat t -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:*$) Nat) t) t)

sNegate :: Sing Nat t -> Sing Nat (Apply Nat Nat (NegateSym0 Nat) t)

sAbs :: Sing Nat t -> Sing Nat (Apply Nat Nat (AbsSym0 Nat) t)

sSignum :: Sing Nat t -> Sing Nat (Apply Nat Nat (SignumSym0 Nat) t)

sFromInteger :: Sing Nat t -> Sing Nat (Apply Nat Nat (FromIntegerSym0 Nat) t)

PNum Nat

Associated Types

type (Nat :+ (arg :: Nat)) (arg :: Nat) :: a

type (Nat :- (arg :: Nat)) (arg :: Nat) :: a

type (Nat :* (arg :: Nat)) (arg :: Nat) :: a

type Negate Nat (arg :: Nat) :: a

type Abs Nat (arg :: Nat) :: a

type Signum Nat (arg :: Nat) :: a

type FromInteger Nat (arg :: Nat) :: a

SEnum Nat

Methods

sSucc :: Sing Nat t -> Sing Nat (Apply Nat Nat (SuccSym0 Nat) t)

sPred :: Sing Nat t -> Sing Nat (Apply Nat Nat (PredSym0 Nat) t)

sToEnum :: Sing Nat t -> Sing Nat (Apply Nat Nat (ToEnumSym0 Nat) t)

sFromEnum :: Sing Nat t -> Sing Nat (Apply Nat Nat (FromEnumSym0 Nat) t)

sEnumFromTo :: Sing Nat t -> Sing Nat t -> Sing [Nat] (Apply Nat [Nat] (Apply Nat (TyFun Nat [Nat] -> Type) (EnumFromToSym0 Nat) t) t)

sEnumFromThenTo :: Sing Nat t -> Sing Nat t -> Sing Nat t -> Sing [Nat] (Apply Nat [Nat] (Apply Nat (TyFun Nat [Nat] -> Type) (Apply Nat (TyFun Nat (TyFun Nat [Nat] -> Type) -> Type) (EnumFromThenToSym0 Nat) t) t) t)

PEnum Nat

Associated Types

type Succ Nat (arg :: Nat) :: a

type Pred Nat (arg :: Nat) :: a

type ToEnum Nat (arg :: Nat) :: a

type FromEnum Nat (arg :: Nat) :: Nat

type EnumFromTo Nat (arg :: Nat) (arg :: Nat) :: [a]

type EnumFromThenTo Nat (arg :: Nat) (arg :: Nat) (arg :: Nat) :: [a]

SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:^$$)

Methods

suppressUnusedWarnings :: Proxy (:^$$) t -> ()

SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) (:^$)

Methods

suppressUnusedWarnings :: Proxy (:^$) t -> ()

SuppressUnusedWarnings (TyFun Nat Constraint -> *) KnownNatSym0

Methods

suppressUnusedWarnings :: Proxy KnownNatSym0 t -> ()

SuppressUnusedWarnings ((TyFun a6989586621679454869 Bool -> Type) -> TyFun [a6989586621679454869] [Nat] -> *) (FindIndicesSym1 a6989586621679454869)

Methods

suppressUnusedWarnings :: Proxy (FindIndicesSym1 a6989586621679454869) t -> ()

SuppressUnusedWarnings ((TyFun a6989586621679454870 Bool -> Type) -> TyFun [a6989586621679454870] (Maybe Nat) -> *) (FindIndexSym1 a6989586621679454870)

Methods

suppressUnusedWarnings :: Proxy (FindIndexSym1 a6989586621679454870) t -> ()

SuppressUnusedWarnings ([a6989586621679454843] -> TyFun Nat a6989586621679454843 -> *) ((:!!$$) a6989586621679454843)

Methods

suppressUnusedWarnings :: Proxy ((:!!$$) a6989586621679454843) t -> ()

SuppressUnusedWarnings (Nat -> TyFun [a6989586621679454860] [a6989586621679454860] -> *) (DropSym1 a6989586621679454860)

Methods

suppressUnusedWarnings :: Proxy (DropSym1 a6989586621679454860) t -> ()

SuppressUnusedWarnings (Nat -> TyFun [a6989586621679454861] [a6989586621679454861] -> *) (TakeSym1 a6989586621679454861)

Methods

suppressUnusedWarnings :: Proxy (TakeSym1 a6989586621679454861) t -> ()

SuppressUnusedWarnings (Nat -> TyFun [a6989586621679454859] ([a6989586621679454859], [a6989586621679454859]) -> *) (SplitAtSym1 a6989586621679454859)

Methods

suppressUnusedWarnings :: Proxy (SplitAtSym1 a6989586621679454859) t -> ()

SuppressUnusedWarnings (Nat -> TyFun a6989586621679454845 [a6989586621679454845] -> *) (ReplicateSym1 a6989586621679454845)

Methods

suppressUnusedWarnings :: Proxy (ReplicateSym1 a6989586621679454845) t -> ()

SuppressUnusedWarnings (Nat -> TyFun (NonEmpty a6989586621679726400) [a6989586621679726400] -> *) (TakeSym1 a6989586621679726400)

Methods

suppressUnusedWarnings :: Proxy (TakeSym1 a6989586621679726400) t -> ()

SuppressUnusedWarnings (Nat -> TyFun (NonEmpty a6989586621679726399) [a6989586621679726399] -> *) (DropSym1 a6989586621679726399)

Methods

suppressUnusedWarnings :: Proxy (DropSym1 a6989586621679726399) t -> ()

SuppressUnusedWarnings (Nat -> TyFun (NonEmpty a6989586621679726398) ([a6989586621679726398], [a6989586621679726398]) -> *) (SplitAtSym1 a6989586621679726398)

Methods

suppressUnusedWarnings :: Proxy (SplitAtSym1 a6989586621679726398) t -> ()

SuppressUnusedWarnings (a6989586621679454871 -> TyFun [a6989586621679454871] [Nat] -> *) (ElemIndicesSym1 a6989586621679454871)

Methods

suppressUnusedWarnings :: Proxy (ElemIndicesSym1 a6989586621679454871) t -> ()

SuppressUnusedWarnings (a6989586621679454872 -> TyFun [a6989586621679454872] (Maybe Nat) -> *) (ElemIndexSym1 a6989586621679454872)

Methods

suppressUnusedWarnings :: Proxy (ElemIndexSym1 a6989586621679454872) t -> ()

SuppressUnusedWarnings (NonEmpty a6989586621679726378 -> TyFun Nat a6989586621679726378 -> *) ((:!!$$) a6989586621679726378)

Methods

suppressUnusedWarnings :: Proxy ((:!!$$) a6989586621679726378) t -> ()

SuppressUnusedWarnings (TyFun (TyFun a6989586621679454869 Bool -> Type) (TyFun [a6989586621679454869] [Nat] -> Type) -> *) (FindIndicesSym0 a6989586621679454869)

Methods

suppressUnusedWarnings :: Proxy (FindIndicesSym0 a6989586621679454869) t -> ()

SuppressUnusedWarnings (TyFun (TyFun a6989586621679454870 Bool -> Type) (TyFun [a6989586621679454870] (Maybe Nat) -> Type) -> *) (FindIndexSym0 a6989586621679454870)

Methods

suppressUnusedWarnings :: Proxy (FindIndexSym0 a6989586621679454870) t -> ()

SuppressUnusedWarnings (TyFun [a6989586621679454843] (TyFun Nat a6989586621679454843 -> Type) -> *) ((:!!$) a6989586621679454843)

Methods

suppressUnusedWarnings :: Proxy ((:!!$) a6989586621679454843) t -> ()

SuppressUnusedWarnings (TyFun [a6989586621679454846] Nat -> *) (LengthSym0 a6989586621679454846)

Methods

suppressUnusedWarnings :: Proxy (LengthSym0 a6989586621679454846) t -> ()

SuppressUnusedWarnings (TyFun Nat (TyFun [a6989586621679454860] [a6989586621679454860] -> Type) -> *) (DropSym0 a6989586621679454860)

Methods

suppressUnusedWarnings :: Proxy (DropSym0 a6989586621679454860) t -> ()

SuppressUnusedWarnings (TyFun Nat (TyFun [a6989586621679454861] [a6989586621679454861] -> Type) -> *) (TakeSym0 a6989586621679454861)

Methods

suppressUnusedWarnings :: Proxy (TakeSym0 a6989586621679454861) t -> ()

SuppressUnusedWarnings (TyFun Nat (TyFun [a6989586621679454859] ([a6989586621679454859], [a6989586621679454859]) -> Type) -> *) (SplitAtSym0 a6989586621679454859)

Methods

suppressUnusedWarnings :: Proxy (SplitAtSym0 a6989586621679454859) t -> ()

SuppressUnusedWarnings (TyFun Nat (TyFun a6989586621679454845 [a6989586621679454845] -> Type) -> *) (ReplicateSym0 a6989586621679454845)

Methods

suppressUnusedWarnings :: Proxy (ReplicateSym0 a6989586621679454845) t -> ()

SuppressUnusedWarnings (TyFun Nat (TyFun (NonEmpty a6989586621679726400) [a6989586621679726400] -> Type) -> *) (TakeSym0 a6989586621679726400)

Methods

suppressUnusedWarnings :: Proxy (TakeSym0 a6989586621679726400) t -> ()

SuppressUnusedWarnings (TyFun Nat (TyFun (NonEmpty a6989586621679726399) [a6989586621679726399] -> Type) -> *) (DropSym0 a6989586621679726399)

Methods

suppressUnusedWarnings :: Proxy (DropSym0 a6989586621679726399) t -> ()

SuppressUnusedWarnings (TyFun Nat (TyFun (NonEmpty a6989586621679726398) ([a6989586621679726398], [a6989586621679726398]) -> Type) -> *) (SplitAtSym0 a6989586621679726398)

Methods

suppressUnusedWarnings :: Proxy (SplitAtSym0 a6989586621679726398) t -> ()

SuppressUnusedWarnings (TyFun Nat a6989586621679407276 -> *) (FromIntegerSym0 a6989586621679407276)

Methods

suppressUnusedWarnings :: Proxy (FromIntegerSym0 a6989586621679407276) t -> ()

SuppressUnusedWarnings (TyFun Nat a6989586621679805857 -> *) (ToEnumSym0 a6989586621679805857)

Methods

suppressUnusedWarnings :: Proxy (ToEnumSym0 a6989586621679805857) t -> ()

SuppressUnusedWarnings (TyFun a6989586621679454871 (TyFun [a6989586621679454871] [Nat] -> Type) -> *) (ElemIndicesSym0 a6989586621679454871)

Methods

suppressUnusedWarnings :: Proxy (ElemIndicesSym0 a6989586621679454871) t -> ()

SuppressUnusedWarnings (TyFun a6989586621679454872 (TyFun [a6989586621679454872] (Maybe Nat) -> Type) -> *) (ElemIndexSym0 a6989586621679454872)

Methods

suppressUnusedWarnings :: Proxy (ElemIndexSym0 a6989586621679454872) t -> ()

SuppressUnusedWarnings (TyFun a6989586621679805857 Nat -> *) (FromEnumSym0 a6989586621679805857)

Methods

suppressUnusedWarnings :: Proxy (FromEnumSym0 a6989586621679805857) t -> ()

SuppressUnusedWarnings (TyFun (NonEmpty a6989586621679726378) (TyFun Nat a6989586621679726378 -> Type) -> *) ((:!!$) a6989586621679726378)

Methods

suppressUnusedWarnings :: Proxy ((:!!$) a6989586621679726378) t -> ()

SuppressUnusedWarnings (TyFun (NonEmpty a6989586621679726431) Nat -> *) (LengthSym0 a6989586621679726431)

Methods

suppressUnusedWarnings :: Proxy (LengthSym0 a6989586621679726431) t -> ()

type Demote Nat

type Demote Nat = Integer

data Sing Nat

data Sing Nat where

• SNat :: Sing Nat n

type Negate Nat a

type Negate Nat a = Error Symbol Nat "Cannot negate a natural number"

type Abs Nat a

type Abs Nat a = a

type Signum Nat a

type Signum Nat a

type FromInteger Nat a

type FromInteger Nat a = a

type Succ Nat a

type Succ Nat a

type Pred Nat a

type Pred Nat a

type ToEnum Nat a

type ToEnum Nat a

type FromEnum Nat a

type FromEnum Nat a

type (==) Nat a b

type (==) Nat a b = EqNat a b

type (:==) Nat a b

type (:==) Nat a b = (==) Nat a b

type (:/=) Nat x y

type (:/=) Nat x y = Not ((:==) Nat x y)

type Compare Nat a b

type Compare Nat a b = CmpNat a b

type (:<) Nat arg1 arg2

type (:<) Nat arg1 arg2

type (:<=) Nat arg1 arg2

type (:<=) Nat arg1 arg2

type (:>) Nat arg1 arg2

type (:>) Nat arg1 arg2

type (:>=) Nat arg1 arg2

type (:>=) Nat arg1 arg2

type Max Nat arg1 arg2

type Max Nat arg1 arg2

type Min Nat arg1 arg2

type Min Nat arg1 arg2

type (:+) Nat a b

type (:+) Nat a b = (+) a b

type (:-) Nat a b

type (:-) Nat a b = (-) a b

type (:*) Nat a b

type (:*) Nat a b = * a b

type EnumFromTo Nat a1 a2

type EnumFromTo Nat a1 a2

type Apply Nat Constraint KnownNatSym0 l

type Apply Nat Constraint KnownNatSym0 l = KnownNat l

type EnumFromThenTo Nat a1 a2 a3

type EnumFromThenTo Nat a1 a2 a3

type Apply Nat Nat ((:^$$) l1) l2

type Apply Nat Nat ((:^$$) l1) l2 = (:^) l1 l2

type Apply Nat k2 (FromIntegerSym0 k2) l

type Apply Nat k2 (FromIntegerSym0 k2) l = FromInteger k2 l

type Apply Nat k2 (ToEnumSym0 k2) l

type Apply Nat k2 (ToEnumSym0 k2) l = ToEnum k2 l

type Apply a Nat (FromEnumSym0 a) l

type Apply a Nat (FromEnumSym0 a) l = FromEnum a l

type Apply Nat a ((:!!$$) a l1) l2

type Apply Nat a ((:!!$$) a l1) l2 = (:!!) a l1 l2

type Apply Nat a ((:!!$$) a l1) l2

type Apply Nat a ((:!!$$) a l1) l2 = (:!!) a l1 l2

type Apply Nat (TyFun Nat Nat -> *) (:^$) l

type Apply Nat (TyFun Nat Nat -> *) (:^$) l = (:^$$) l

type Apply Nat (TyFun [a6989586621679454860] [a6989586621679454860] -> Type) (DropSym0 a6989586621679454860) l

type Apply Nat (TyFun [a6989586621679454860] [a6989586621679454860] -> Type) (DropSym0 a6989586621679454860) l = DropSym1 a6989586621679454860 l

type Apply Nat (TyFun [a6989586621679454861] [a6989586621679454861] -> Type) (TakeSym0 a6989586621679454861) l

type Apply Nat (TyFun [a6989586621679454861] [a6989586621679454861] -> Type) (TakeSym0 a6989586621679454861) l = TakeSym1 a6989586621679454861 l

type Apply Nat (TyFun [a6989586621679454859] ([a6989586621679454859], [a6989586621679454859]) -> Type) (SplitAtSym0 a6989586621679454859) l

type Apply Nat (TyFun [a6989586621679454859] ([a6989586621679454859], [a6989586621679454859]) -> Type) (SplitAtSym0 a6989586621679454859) l = SplitAtSym1 a6989586621679454859 l

type Apply Nat (TyFun a6989586621679454845 [a6989586621679454845] -> Type) (ReplicateSym0 a6989586621679454845) l

type Apply Nat (TyFun a6989586621679454845 [a6989586621679454845] -> Type) (ReplicateSym0 a6989586621679454845) l = ReplicateSym1 a6989586621679454845 l

type Apply Nat (TyFun (NonEmpty a6989586621679726400) [a6989586621679726400] -> Type) (TakeSym0 a6989586621679726400) l

type Apply Nat (TyFun (NonEmpty a6989586621679726400) [a6989586621679726400] -> Type) (TakeSym0 a6989586621679726400) l = TakeSym1 a6989586621679726400 l

type Apply Nat (TyFun (NonEmpty a6989586621679726399) [a6989586621679726399] -> Type) (DropSym0 a6989586621679726399) l

type Apply Nat (TyFun (NonEmpty a6989586621679726399) [a6989586621679726399] -> Type) (DropSym0 a6989586621679726399) l = DropSym1 a6989586621679726399 l

type Apply Nat (TyFun (NonEmpty a6989586621679726398) ([a6989586621679726398], [a6989586621679726398]) -> Type) (SplitAtSym0 a6989586621679726398) l

type Apply Nat (TyFun (NonEmpty a6989586621679726398) ([a6989586621679726398], [a6989586621679726398]) -> Type) (SplitAtSym0 a6989586621679726398) l = SplitAtSym1 a6989586621679726398 l

type Apply a6989586621679454871 (TyFun [a6989586621679454871] [Nat] -> Type) (ElemIndicesSym0 a6989586621679454871) l

type Apply a6989586621679454871 (TyFun [a6989586621679454871] [Nat] -> Type) (ElemIndicesSym0 a6989586621679454871) l = ElemIndicesSym1 a6989586621679454871 l

type Apply a6989586621679454872 (TyFun [a6989586621679454872] (Maybe Nat) -> Type) (ElemIndexSym0 a6989586621679454872) l

type Apply a6989586621679454872 (TyFun [a6989586621679454872] (Maybe Nat) -> Type) (ElemIndexSym0 a6989586621679454872) l = ElemIndexSym1 a6989586621679454872 l

type Apply [a] Nat (LengthSym0 a) l

type Apply [a] Nat (LengthSym0 a) l = Length a l

type Apply (NonEmpty a) Nat (LengthSym0 a) l

type Apply (NonEmpty a) Nat (LengthSym0 a) l = Length a l

type Apply [a] [Nat] (FindIndicesSym1 a l1) l2

type Apply [a] [Nat] (FindIndicesSym1 a l1) l2 = FindIndices a l1 l2

type Apply [a] [Nat] (ElemIndicesSym1 a l1) l2

type Apply [a] [Nat] (ElemIndicesSym1 a l1) l2 = ElemIndices a l1 l2

type Apply [a] (Maybe Nat) (FindIndexSym1 a l1) l2

type Apply [a] (Maybe Nat) (FindIndexSym1 a l1) l2 = FindIndex a l1 l2

type Apply [a] (Maybe Nat) (ElemIndexSym1 a l1) l2

type Apply [a] (Maybe Nat) (ElemIndexSym1 a l1) l2 = ElemIndex a l1 l2

type Apply [a6989586621679454843] (TyFun Nat a6989586621679454843 -> Type) ((:!!$) a6989586621679454843) l

type Apply [a6989586621679454843] (TyFun Nat a6989586621679454843 -> Type) ((:!!$) a6989586621679454843) l = (:!!$$) a6989586621679454843 l

type Apply (NonEmpty a6989586621679726378) (TyFun Nat a6989586621679726378 -> Type) ((:!!$) a6989586621679726378) l

type Apply (NonEmpty a6989586621679726378) (TyFun Nat a6989586621679726378 -> Type) ((:!!$) a6989586621679726378) l = (:!!$$) a6989586621679726378 l

type Apply (TyFun a6989586621679454869 Bool -> Type) (TyFun [a6989586621679454869] [Nat] -> Type) (FindIndicesSym0 a6989586621679454869) l

type Apply (TyFun a6989586621679454869 Bool -> Type) (TyFun [a6989586621679454869] [Nat] -> Type) (FindIndicesSym0 a6989586621679454869) l = FindIndicesSym1 a6989586621679454869 l

type Apply (TyFun a6989586621679454870 Bool -> Type) (TyFun [a6989586621679454870] (Maybe Nat) -> Type) (FindIndexSym0 a6989586621679454870) l

type Apply (TyFun a6989586621679454870 Bool -> Type) (TyFun [a6989586621679454870] (Maybe Nat) -> Type) (FindIndexSym0 a6989586621679454870) l = FindIndexSym1 a6989586621679454870 l

data Symbol :: *

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

Instances

SingKind Symbol

Since: 4.9.0.0

Associated Types

type DemoteRep Symbol :: *

Methods

fromSing :: Sing Symbol a -> DemoteRep Symbol

KnownSymbol a => SingI Symbol a

Since: 4.9.0.0

Methods

sing :: Sing a a

SuppressUnusedWarnings (TyFun Symbol Constraint -> *) KnownSymbolSym0

Methods

suppressUnusedWarnings :: Proxy KnownSymbolSym0 t -> ()

data Sing Symbol

data Sing Symbol where

• SSym :: Sing Symbol s

type DemoteRep Symbol

type DemoteRep Symbol = String

type Demote Symbol

type Demote Symbol = Text

data Sing Symbol

data Sing Symbol where

• SSym :: Sing Symbol n

type (==) Symbol a b

type (==) Symbol a b = EqSymbol a b

type (:==) Symbol a b

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

type (:/=) Symbol x y

type (:/=) Symbol x y = Not ((:==) Symbol x y)

type Compare Symbol a b

type Compare Symbol a b = CmpSymbol a b

type (:<) Symbol arg1 arg2

type (:<) Symbol arg1 arg2

type (:<=) Symbol arg1 arg2

type (:<=) Symbol arg1 arg2

type (:>) Symbol arg1 arg2

type (:>) Symbol arg1 arg2

type (:>=) Symbol arg1 arg2

type (:>=) Symbol arg1 arg2

type Max Symbol arg1 arg2

type Max Symbol arg1 arg2

type Min Symbol arg1 arg2

type Min Symbol arg1 arg2

type Apply Symbol Constraint KnownSymbolSym0 l

type Apply Symbol Constraint KnownSymbolSym0 l = KnownSymbol l

data family Sing (a :: k)

The singleton kind-indexed data family.

Instances

data Sing Bool

data Sing Bool where

• SFalse :: Sing Bool z
• STrue :: Sing Bool z

data Sing Ordering

data Sing Ordering where

• SLT :: Sing Ordering z
• SEQ :: Sing Ordering z
• SGT :: Sing Ordering z

data Sing *

data Sing * where

• STypeRep :: Sing * a

data Sing Nat

data Sing Nat where

• SNat :: Sing Nat n

data Sing Symbol

data Sing Symbol where

• SSym :: Sing Symbol n

data Sing ()

data Sing () where

• STuple0 :: Sing () z

data Sing [a]

data Sing [a] where

• SNil :: Sing [a] z
• SCons :: Sing [a] z

data Sing (Maybe a)

data Sing (Maybe a) where

• SNothing :: Sing (Maybe a) z
• SJust :: Sing (Maybe a) z

data Sing (NonEmpty a)

data Sing (NonEmpty a) where

• (:%|) :: Sing (NonEmpty a) z

data Sing (Either a b)

data Sing (Either a b) where

• SLeft :: Sing (Either a b) z
• SRight :: Sing (Either a b) z

data Sing (a, b)

data Sing (a, b) where

• STuple2 :: Sing (a, b) z

data Sing ((~>) k1 k2)

data Sing ((~>) k1 k2) = SLambda {

• applySing :: forall (t :: k1). Sing k1 t -> Sing k2 ((@@) k1 k2 f t)

}

data Sing (a, b, c)

data Sing (a, b, c) where

• STuple3 :: Sing (a, b, c) z

data Sing (a, b, c, d)

data Sing (a, b, c, d) where

• STuple4 :: Sing (a, b, c, d) z

data Sing (a, b, c, d, e)

data Sing (a, b, c, d, e) where

• STuple5 :: Sing (a, b, c, d, e) z

data Sing (a, b, c, d, e, f)

data Sing (a, b, c, d, e, f) where

• STuple6 :: Sing (a, b, c, d, e, f) z

data Sing (a, b, c, d, e, f, g)

data Sing (a, b, c, d, e, f, g) where

• STuple7 :: Sing (a, b, c, d, e, f, g) z

type SNat (x :: Nat) = Sing x

Kind-restricted synonym for Sing for Nats

type SSymbol (x :: Symbol) = Sing x

Kind-restricted synonym for Sing for Symbols

withKnownNat :: Sing n -> (KnownNat n => r) -> r

Given a singleton for Nat, call something requiring a KnownNat instance.

withKnownSymbol :: Sing n -> (KnownSymbol n => r) -> r

Given a singleton for Symbol, call something requiring a KnownSymbol instance.

type family Error (str :: k0) :: k

The promotion of error. This version is more poly-kinded for easier use.

data ErrorSym0 (l :: TyFun k06989586621679399311 k6989586621679399313)

Instances

SuppressUnusedWarnings (TyFun k06989586621679399311 k6989586621679399313 -> *) (ErrorSym0 k06989586621679399311 k6989586621679399313)

Methods

suppressUnusedWarnings :: Proxy (ErrorSym0 k06989586621679399311 k6989586621679399313) t -> ()

type Apply k0 k2 (ErrorSym0 k0 k2) l

type Apply k0 k2 (ErrorSym0 k0 k2) l = Error k0 k2 l

type ErrorSym1 (t :: k06989586621679399311) = Error t

sError :: Sing (str :: Symbol) -> a

The singleton for error

class KnownNat (n :: Nat)

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: 4.7.0.0

Minimal complete definition

natSing

data KnownNatSym0 (l :: TyFun Nat Constraint)

Instances

SuppressUnusedWarnings (TyFun Nat Constraint -> *) KnownNatSym0

Methods

suppressUnusedWarnings :: Proxy KnownNatSym0 t -> ()

type Apply Nat Constraint KnownNatSym0 l

type Apply Nat Constraint KnownNatSym0 l = KnownNat l

type KnownNatSym1 (t :: Nat) = KnownNat t

natVal :: KnownNat n => proxy n -> Integer

Since: 4.7.0.0

class KnownSymbol (n :: Symbol)

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

Since: 4.7.0.0

Minimal complete definition

symbolSing

data KnownSymbolSym0 (l :: TyFun Symbol Constraint)

Instances

SuppressUnusedWarnings (TyFun Symbol Constraint -> *) KnownSymbolSym0

Methods

suppressUnusedWarnings :: Proxy KnownSymbolSym0 t -> ()

type Apply Symbol Constraint KnownSymbolSym0 l

type Apply Symbol Constraint KnownSymbolSym0 l = KnownSymbol l

type KnownSymbolSym1 (t :: Symbol) = KnownSymbol t

symbolVal :: KnownSymbol n => proxy n -> String

Since: 4.7.0.0

type (:^) a b = a ^ b infixr 8

data (:^$) l

Instances

SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) (:^$)

Methods

suppressUnusedWarnings :: Proxy (:^$) t -> ()

type Apply Nat (TyFun Nat Nat -> *) (:^$) l

type Apply Nat (TyFun Nat Nat -> *) (:^$) l = (:^$$) l

data (l :: Nat) :^$$ l

Instances

SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:^$$)

Methods

suppressUnusedWarnings :: Proxy (:^$$) t -> ()

type Apply Nat Nat ((:^$$) l1) l2

type Apply Nat Nat ((:^$$) l1) l2 = (:^) l1 l2

type (:^$$$) (t :: Nat) (t :: Nat) = (:^) t t

Orphan instances

Eq Nat

Methods

(==) :: Nat -> Nat -> Bool

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

Eq Symbol

This bogus instance is helpful for people who want to define functions over Symbols that will only be used at the type level or as singletons.

Methods

(==) :: Symbol -> Symbol -> Bool

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

Num Nat

This bogus Num instance is helpful for people who want to define functions over Nats that will only be used at the type level or as singletons. A correct SNum instance for Nat singletons exists.

Methods

(+) :: Nat -> Nat -> Nat

(-) :: Nat -> Nat -> Nat

(*) :: Nat -> Nat -> Nat

negate :: Nat -> Nat

abs :: Nat -> Nat

signum :: Nat -> Nat

fromInteger :: Integer -> Nat

Ord Nat

Methods

compare :: Nat -> Nat -> Ordering

(<) :: Nat -> Nat -> Bool

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

(>) :: Nat -> Nat -> Bool

(>=) :: Nat -> Nat -> Bool

max :: Nat -> Nat -> Nat

min :: Nat -> Nat -> Nat

Ord Symbol

Methods

compare :: Symbol -> Symbol -> Ordering

(<) :: Symbol -> Symbol -> Bool

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

(>) :: Symbol -> Symbol -> Bool

(>=) :: Symbol -> Symbol -> Bool

max :: Symbol -> Symbol -> Symbol

min :: Symbol -> Symbol -> Symbol