Copyright	(C) 2014 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Richard Eisenberg (rae@cs.brynmawr.edu)
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Singletons.TypeLits

Contents

Orphan instances

Description

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

Synopsis

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 a1627856109 Bool -> Type) -> TyFun [a1627856109] [Nat] -> *) (FindIndicesSym1 a1627856109) #
Methods suppressUnusedWarnings :: Proxy (FindIndicesSym1 a1627856109) t -> () #
SuppressUnusedWarnings ((TyFun a1627856110 Bool -> Type) -> TyFun [a1627856110] (Maybe Nat) -> *) (FindIndexSym1 a1627856110) #
Methods suppressUnusedWarnings :: Proxy (FindIndexSym1 a1627856110) t -> () #
SuppressUnusedWarnings ([a1627856083] -> TyFun Nat a1627856083 -> *) ((:!!$$) a1627856083) #
Methods suppressUnusedWarnings :: Proxy ((:!!$$) a1627856083) t -> () #
SuppressUnusedWarnings (Nat -> TyFun [a1627856100] [a1627856100] -> *) (DropSym1 a1627856100) #
Methods suppressUnusedWarnings :: Proxy (DropSym1 a1627856100) t -> () #
SuppressUnusedWarnings (Nat -> TyFun [a1627856101] [a1627856101] -> *) (TakeSym1 a1627856101) #
Methods suppressUnusedWarnings :: Proxy (TakeSym1 a1627856101) t -> () #
SuppressUnusedWarnings (Nat -> TyFun [a1627856099] ([a1627856099], [a1627856099]) -> *) (SplitAtSym1 a1627856099) #
Methods suppressUnusedWarnings :: Proxy (SplitAtSym1 a1627856099) t -> () #
SuppressUnusedWarnings (Nat -> TyFun a1627856085 [a1627856085] -> *) (ReplicateSym1 a1627856085) #
Methods suppressUnusedWarnings :: Proxy (ReplicateSym1 a1627856085) t -> () #
SuppressUnusedWarnings (Nat -> TyFun (NonEmpty a1628135958) [a1628135958] -> *) (TakeSym1 a1628135958) #
Methods suppressUnusedWarnings :: Proxy (TakeSym1 a1628135958) t -> () #
SuppressUnusedWarnings (Nat -> TyFun (NonEmpty a1628135957) [a1628135957] -> *) (DropSym1 a1628135957) #
Methods suppressUnusedWarnings :: Proxy (DropSym1 a1628135957) t -> () #
SuppressUnusedWarnings (Nat -> TyFun (NonEmpty a1628135956) ([a1628135956], [a1628135956]) -> *) (SplitAtSym1 a1628135956) #
Methods suppressUnusedWarnings :: Proxy (SplitAtSym1 a1628135956) t -> () #
SuppressUnusedWarnings (a1627856111 -> TyFun [a1627856111] [Nat] -> *) (ElemIndicesSym1 a1627856111) #
Methods suppressUnusedWarnings :: Proxy (ElemIndicesSym1 a1627856111) t -> () #
SuppressUnusedWarnings (a1627856112 -> TyFun [a1627856112] (Maybe Nat) -> *) (ElemIndexSym1 a1627856112) #
Methods suppressUnusedWarnings :: Proxy (ElemIndexSym1 a1627856112) t -> () #
SuppressUnusedWarnings (NonEmpty a1628135936 -> TyFun Nat a1628135936 -> *) ((:!!$$) a1628135936) #
Methods suppressUnusedWarnings :: Proxy ((:!!$$) a1628135936) t -> () #
SuppressUnusedWarnings (TyFun (TyFun a1627856109 Bool -> Type) (TyFun [a1627856109] [Nat] -> Type) -> *) (FindIndicesSym0 a1627856109) #
Methods suppressUnusedWarnings :: Proxy (FindIndicesSym0 a1627856109) t -> () #
SuppressUnusedWarnings (TyFun (TyFun a1627856110 Bool -> Type) (TyFun [a1627856110] (Maybe Nat) -> Type) -> *) (FindIndexSym0 a1627856110) #
Methods suppressUnusedWarnings :: Proxy (FindIndexSym0 a1627856110) t -> () #
SuppressUnusedWarnings (TyFun [a1627856083] (TyFun Nat a1627856083 -> Type) -> *) ((:!!$) a1627856083) #
Methods suppressUnusedWarnings :: Proxy ((:!!$) a1627856083) t -> () #
SuppressUnusedWarnings (TyFun [a1627856086] Nat -> *) (LengthSym0 a1627856086) #
Methods suppressUnusedWarnings :: Proxy (LengthSym0 a1627856086) t -> () #
SuppressUnusedWarnings (TyFun Nat (TyFun [a1627856100] [a1627856100] -> Type) -> *) (DropSym0 a1627856100) #
Methods suppressUnusedWarnings :: Proxy (DropSym0 a1627856100) t -> () #
SuppressUnusedWarnings (TyFun Nat (TyFun [a1627856101] [a1627856101] -> Type) -> *) (TakeSym0 a1627856101) #
Methods suppressUnusedWarnings :: Proxy (TakeSym0 a1627856101) t -> () #
SuppressUnusedWarnings (TyFun Nat (TyFun [a1627856099] ([a1627856099], [a1627856099]) -> Type) -> *) (SplitAtSym0 a1627856099) #
Methods suppressUnusedWarnings :: Proxy (SplitAtSym0 a1627856099) t -> () #
SuppressUnusedWarnings (TyFun Nat (TyFun a1627856085 [a1627856085] -> Type) -> *) (ReplicateSym0 a1627856085) #
Methods suppressUnusedWarnings :: Proxy (ReplicateSym0 a1627856085) t -> () #
SuppressUnusedWarnings (TyFun Nat (TyFun (NonEmpty a1628135958) [a1628135958] -> Type) -> *) (TakeSym0 a1628135958) #
Methods suppressUnusedWarnings :: Proxy (TakeSym0 a1628135958) t -> () #
SuppressUnusedWarnings (TyFun Nat (TyFun (NonEmpty a1628135957) [a1628135957] -> Type) -> *) (DropSym0 a1628135957) #
Methods suppressUnusedWarnings :: Proxy (DropSym0 a1628135957) t -> () #
SuppressUnusedWarnings (TyFun Nat (TyFun (NonEmpty a1628135956) ([a1628135956], [a1628135956]) -> Type) -> *) (SplitAtSym0 a1628135956) #
Methods suppressUnusedWarnings :: Proxy (SplitAtSym0 a1628135956) t -> () #
SuppressUnusedWarnings (TyFun Nat a1627807374 -> *) (FromIntegerSym0 a1627807374) #
Methods suppressUnusedWarnings :: Proxy (FromIntegerSym0 a1627807374) t -> () #
SuppressUnusedWarnings (TyFun Nat a1628217981 -> *) (ToEnumSym0 a1628217981) #
Methods suppressUnusedWarnings :: Proxy (ToEnumSym0 a1628217981) t -> () #
SuppressUnusedWarnings (TyFun a1627856111 (TyFun [a1627856111] [Nat] -> Type) -> *) (ElemIndicesSym0 a1627856111) #
Methods suppressUnusedWarnings :: Proxy (ElemIndicesSym0 a1627856111) t -> () #
SuppressUnusedWarnings (TyFun a1627856112 (TyFun [a1627856112] (Maybe Nat) -> Type) -> *) (ElemIndexSym0 a1627856112) #
Methods suppressUnusedWarnings :: Proxy (ElemIndexSym0 a1627856112) t -> () #
SuppressUnusedWarnings (TyFun a1628217981 Nat -> *) (FromEnumSym0 a1628217981) #
Methods suppressUnusedWarnings :: Proxy (FromEnumSym0 a1628217981) t -> () #
SuppressUnusedWarnings (TyFun (NonEmpty a1628135936) (TyFun Nat a1628135936 -> Type) -> *) ((:!!$) a1628135936) #
Methods suppressUnusedWarnings :: Proxy ((:!!$) a1628135936) t -> () #
SuppressUnusedWarnings (TyFun (NonEmpty a1628135989) Nat -> *) (LengthSym0 a1628135989) #
Methods suppressUnusedWarnings :: Proxy (LengthSym0 a1628135989) 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 [a1627856100] [a1627856100] -> Type) (DropSym0 a1627856100) l #
type Apply Nat (TyFun [a1627856100] [a1627856100] -> Type) (DropSym0 a1627856100) l = DropSym1 a1627856100 l
type Apply Nat (TyFun [a1627856101] [a1627856101] -> Type) (TakeSym0 a1627856101) l #
type Apply Nat (TyFun [a1627856101] [a1627856101] -> Type) (TakeSym0 a1627856101) l = TakeSym1 a1627856101 l
type Apply Nat (TyFun [a1627856099] ([a1627856099], [a1627856099]) -> Type) (SplitAtSym0 a1627856099) l #
type Apply Nat (TyFun [a1627856099] ([a1627856099], [a1627856099]) -> Type) (SplitAtSym0 a1627856099) l = SplitAtSym1 a1627856099 l
type Apply Nat (TyFun a1627856085 [a1627856085] -> Type) (ReplicateSym0 a1627856085) l #
type Apply Nat (TyFun a1627856085 [a1627856085] -> Type) (ReplicateSym0 a1627856085) l = ReplicateSym1 a1627856085 l
type Apply Nat (TyFun (NonEmpty a1628135958) [a1628135958] -> Type) (TakeSym0 a1628135958) l #
type Apply Nat (TyFun (NonEmpty a1628135958) [a1628135958] -> Type) (TakeSym0 a1628135958) l = TakeSym1 a1628135958 l
type Apply Nat (TyFun (NonEmpty a1628135957) [a1628135957] -> Type) (DropSym0 a1628135957) l #
type Apply Nat (TyFun (NonEmpty a1628135957) [a1628135957] -> Type) (DropSym0 a1628135957) l = DropSym1 a1628135957 l
type Apply Nat (TyFun (NonEmpty a1628135956) ([a1628135956], [a1628135956]) -> Type) (SplitAtSym0 a1628135956) l #
type Apply Nat (TyFun (NonEmpty a1628135956) ([a1628135956], [a1628135956]) -> Type) (SplitAtSym0 a1628135956) l = SplitAtSym1 a1628135956 l
type Apply a1627856111 (TyFun [a1627856111] [Nat] -> Type) (ElemIndicesSym0 a1627856111) l #
type Apply a1627856111 (TyFun [a1627856111] [Nat] -> Type) (ElemIndicesSym0 a1627856111) l = ElemIndicesSym1 a1627856111 l
type Apply a1627856112 (TyFun [a1627856112] (Maybe Nat) -> Type) (ElemIndexSym0 a1627856112) l #
type Apply a1627856112 (TyFun [a1627856112] (Maybe Nat) -> Type) (ElemIndexSym0 a1627856112) l = ElemIndexSym1 a1627856112 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 [a1627856083] (TyFun Nat a1627856083 -> Type) ((:!!$) a1627856083) l #
type Apply [a1627856083] (TyFun Nat a1627856083 -> Type) ((:!!$) a1627856083) l = (:!!$$) a1627856083 l
type Apply (NonEmpty a1628135936) (TyFun Nat a1628135936 -> Type) ((:!!$) a1628135936) l #
type Apply (NonEmpty a1628135936) (TyFun Nat a1628135936 -> Type) ((:!!$) a1628135936) l = (:!!$$) a1628135936 l
type Apply (TyFun a1627856109 Bool -> Type) (TyFun [a1627856109] [Nat] -> Type) (FindIndicesSym0 a1627856109) l #
type Apply (TyFun a1627856109 Bool -> Type) (TyFun [a1627856109] [Nat] -> Type) (FindIndicesSym0 a1627856109) l = FindIndicesSym1 a1627856109 l
type Apply (TyFun a1627856110 Bool -> Type) (TyFun [a1627856110] (Maybe Nat) -> Type) (FindIndexSym0 a1627856110) l #
type Apply (TyFun a1627856110 Bool -> Type) (TyFun [a1627856110] (Maybe Nat) -> Type) (FindIndexSym0 a1627856110) l = FindIndexSym1 a1627856110 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 k01627798799 k1627798801) #

Instances

SuppressUnusedWarnings (TyFun k01627798799 k1627798801 -> *) (ErrorSym0 k01627798799 k1627798801) #
Methods suppressUnusedWarnings :: Proxy (ErrorSym0 k01627798799 k1627798801) t -> () #
type Apply k0 k2 (ErrorSym0 k0 k2) l #
type Apply k0 k2 (ErrorSym0 k0 k2) l = Error k0 k2 l

type ErrorSym1 (t :: k01627798799) = 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 #