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 a6989586621679475569 Bool -> Type) -> TyFun [a6989586621679475569] [Nat] -> *) (FindIndicesSym1 a6989586621679475569) #
Methods suppressUnusedWarnings :: Proxy (FindIndicesSym1 a6989586621679475569) t -> () #
SuppressUnusedWarnings ((TyFun a6989586621679475570 Bool -> Type) -> TyFun [a6989586621679475570] (Maybe Nat) -> *) (FindIndexSym1 a6989586621679475570) #
Methods suppressUnusedWarnings :: Proxy (FindIndexSym1 a6989586621679475570) t -> () #
SuppressUnusedWarnings ([a6989586621679475543] -> TyFun Nat a6989586621679475543 -> *) ((:!!$$) a6989586621679475543) #
Methods suppressUnusedWarnings :: Proxy ((:!!$$) a6989586621679475543) t -> () #
SuppressUnusedWarnings (Nat -> TyFun [a6989586621679475560] [a6989586621679475560] -> *) (DropSym1 a6989586621679475560) #
Methods suppressUnusedWarnings :: Proxy (DropSym1 a6989586621679475560) t -> () #
SuppressUnusedWarnings (Nat -> TyFun [a6989586621679475561] [a6989586621679475561] -> *) (TakeSym1 a6989586621679475561) #
Methods suppressUnusedWarnings :: Proxy (TakeSym1 a6989586621679475561) t -> () #
SuppressUnusedWarnings (Nat -> TyFun [a6989586621679475559] ([a6989586621679475559], [a6989586621679475559]) -> *) (SplitAtSym1 a6989586621679475559) #
Methods suppressUnusedWarnings :: Proxy (SplitAtSym1 a6989586621679475559) t -> () #
SuppressUnusedWarnings (Nat -> TyFun a6989586621679475545 [a6989586621679475545] -> *) (ReplicateSym1 a6989586621679475545) #
Methods suppressUnusedWarnings :: Proxy (ReplicateSym1 a6989586621679475545) t -> () #
SuppressUnusedWarnings (Nat -> TyFun (NonEmpty a6989586621679753510) [a6989586621679753510] -> *) (TakeSym1 a6989586621679753510) #
Methods suppressUnusedWarnings :: Proxy (TakeSym1 a6989586621679753510) t -> () #
SuppressUnusedWarnings (Nat -> TyFun (NonEmpty a6989586621679753509) [a6989586621679753509] -> *) (DropSym1 a6989586621679753509) #
Methods suppressUnusedWarnings :: Proxy (DropSym1 a6989586621679753509) t -> () #
SuppressUnusedWarnings (Nat -> TyFun (NonEmpty a6989586621679753508) ([a6989586621679753508], [a6989586621679753508]) -> *) (SplitAtSym1 a6989586621679753508) #
Methods suppressUnusedWarnings :: Proxy (SplitAtSym1 a6989586621679753508) t -> () #
SuppressUnusedWarnings (a6989586621679475571 -> TyFun [a6989586621679475571] [Nat] -> *) (ElemIndicesSym1 a6989586621679475571) #
Methods suppressUnusedWarnings :: Proxy (ElemIndicesSym1 a6989586621679475571) t -> () #
SuppressUnusedWarnings (a6989586621679475572 -> TyFun [a6989586621679475572] (Maybe Nat) -> *) (ElemIndexSym1 a6989586621679475572) #
Methods suppressUnusedWarnings :: Proxy (ElemIndexSym1 a6989586621679475572) t -> () #
SuppressUnusedWarnings (NonEmpty a6989586621679753488 -> TyFun Nat a6989586621679753488 -> *) ((:!!$$) a6989586621679753488) #
Methods suppressUnusedWarnings :: Proxy ((:!!$$) a6989586621679753488) t -> () #
SuppressUnusedWarnings (TyFun (TyFun a6989586621679475569 Bool -> Type) (TyFun [a6989586621679475569] [Nat] -> Type) -> *) (FindIndicesSym0 a6989586621679475569) #
Methods suppressUnusedWarnings :: Proxy (FindIndicesSym0 a6989586621679475569) t -> () #
SuppressUnusedWarnings (TyFun (TyFun a6989586621679475570 Bool -> Type) (TyFun [a6989586621679475570] (Maybe Nat) -> Type) -> *) (FindIndexSym0 a6989586621679475570) #
Methods suppressUnusedWarnings :: Proxy (FindIndexSym0 a6989586621679475570) t -> () #
SuppressUnusedWarnings (TyFun [a6989586621679475543] (TyFun Nat a6989586621679475543 -> Type) -> *) ((:!!$) a6989586621679475543) #
Methods suppressUnusedWarnings :: Proxy ((:!!$) a6989586621679475543) t -> () #
SuppressUnusedWarnings (TyFun [a6989586621679475546] Nat -> *) (LengthSym0 a6989586621679475546) #
Methods suppressUnusedWarnings :: Proxy (LengthSym0 a6989586621679475546) t -> () #
SuppressUnusedWarnings (TyFun Nat (TyFun [a6989586621679475560] [a6989586621679475560] -> Type) -> *) (DropSym0 a6989586621679475560) #
Methods suppressUnusedWarnings :: Proxy (DropSym0 a6989586621679475560) t -> () #
SuppressUnusedWarnings (TyFun Nat (TyFun [a6989586621679475561] [a6989586621679475561] -> Type) -> *) (TakeSym0 a6989586621679475561) #
Methods suppressUnusedWarnings :: Proxy (TakeSym0 a6989586621679475561) t -> () #
SuppressUnusedWarnings (TyFun Nat (TyFun [a6989586621679475559] ([a6989586621679475559], [a6989586621679475559]) -> Type) -> *) (SplitAtSym0 a6989586621679475559) #
Methods suppressUnusedWarnings :: Proxy (SplitAtSym0 a6989586621679475559) t -> () #
SuppressUnusedWarnings (TyFun Nat (TyFun a6989586621679475545 [a6989586621679475545] -> Type) -> *) (ReplicateSym0 a6989586621679475545) #
Methods suppressUnusedWarnings :: Proxy (ReplicateSym0 a6989586621679475545) t -> () #
SuppressUnusedWarnings (TyFun Nat (TyFun (NonEmpty a6989586621679753510) [a6989586621679753510] -> Type) -> *) (TakeSym0 a6989586621679753510) #
Methods suppressUnusedWarnings :: Proxy (TakeSym0 a6989586621679753510) t -> () #
SuppressUnusedWarnings (TyFun Nat (TyFun (NonEmpty a6989586621679753509) [a6989586621679753509] -> Type) -> *) (DropSym0 a6989586621679753509) #
Methods suppressUnusedWarnings :: Proxy (DropSym0 a6989586621679753509) t -> () #
SuppressUnusedWarnings (TyFun Nat (TyFun (NonEmpty a6989586621679753508) ([a6989586621679753508], [a6989586621679753508]) -> Type) -> *) (SplitAtSym0 a6989586621679753508) #
Methods suppressUnusedWarnings :: Proxy (SplitAtSym0 a6989586621679753508) t -> () #
SuppressUnusedWarnings (TyFun Nat a6989586621679427063 -> *) (FromIntegerSym0 a6989586621679427063) #
Methods suppressUnusedWarnings :: Proxy (FromIntegerSym0 a6989586621679427063) t -> () #
SuppressUnusedWarnings (TyFun Nat a6989586621679834780 -> *) (ToEnumSym0 a6989586621679834780) #
Methods suppressUnusedWarnings :: Proxy (ToEnumSym0 a6989586621679834780) t -> () #
SuppressUnusedWarnings (TyFun a6989586621679475571 (TyFun [a6989586621679475571] [Nat] -> Type) -> *) (ElemIndicesSym0 a6989586621679475571) #
Methods suppressUnusedWarnings :: Proxy (ElemIndicesSym0 a6989586621679475571) t -> () #
SuppressUnusedWarnings (TyFun a6989586621679475572 (TyFun [a6989586621679475572] (Maybe Nat) -> Type) -> *) (ElemIndexSym0 a6989586621679475572) #
Methods suppressUnusedWarnings :: Proxy (ElemIndexSym0 a6989586621679475572) t -> () #
SuppressUnusedWarnings (TyFun a6989586621679834780 Nat -> *) (FromEnumSym0 a6989586621679834780) #
Methods suppressUnusedWarnings :: Proxy (FromEnumSym0 a6989586621679834780) t -> () #
SuppressUnusedWarnings (TyFun (NonEmpty a6989586621679753488) (TyFun Nat a6989586621679753488 -> Type) -> *) ((:!!$) a6989586621679753488) #
Methods suppressUnusedWarnings :: Proxy ((:!!$) a6989586621679753488) t -> () #
SuppressUnusedWarnings (TyFun (NonEmpty a6989586621679753541) Nat -> *) (LengthSym0 a6989586621679753541) #
Methods suppressUnusedWarnings :: Proxy (LengthSym0 a6989586621679753541) 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 [a6989586621679475560] [a6989586621679475560] -> Type) (DropSym0 a6989586621679475560) l #
type Apply Nat (TyFun [a6989586621679475560] [a6989586621679475560] -> Type) (DropSym0 a6989586621679475560) l = DropSym1 a6989586621679475560 l
type Apply Nat (TyFun [a6989586621679475561] [a6989586621679475561] -> Type) (TakeSym0 a6989586621679475561) l #
type Apply Nat (TyFun [a6989586621679475561] [a6989586621679475561] -> Type) (TakeSym0 a6989586621679475561) l = TakeSym1 a6989586621679475561 l
type Apply Nat (TyFun [a6989586621679475559] ([a6989586621679475559], [a6989586621679475559]) -> Type) (SplitAtSym0 a6989586621679475559) l #
type Apply Nat (TyFun [a6989586621679475559] ([a6989586621679475559], [a6989586621679475559]) -> Type) (SplitAtSym0 a6989586621679475559) l = SplitAtSym1 a6989586621679475559 l
type Apply Nat (TyFun a6989586621679475545 [a6989586621679475545] -> Type) (ReplicateSym0 a6989586621679475545) l #
type Apply Nat (TyFun a6989586621679475545 [a6989586621679475545] -> Type) (ReplicateSym0 a6989586621679475545) l = ReplicateSym1 a6989586621679475545 l
type Apply Nat (TyFun (NonEmpty a6989586621679753510) [a6989586621679753510] -> Type) (TakeSym0 a6989586621679753510) l #
type Apply Nat (TyFun (NonEmpty a6989586621679753510) [a6989586621679753510] -> Type) (TakeSym0 a6989586621679753510) l = TakeSym1 a6989586621679753510 l
type Apply Nat (TyFun (NonEmpty a6989586621679753509) [a6989586621679753509] -> Type) (DropSym0 a6989586621679753509) l #
type Apply Nat (TyFun (NonEmpty a6989586621679753509) [a6989586621679753509] -> Type) (DropSym0 a6989586621679753509) l = DropSym1 a6989586621679753509 l
type Apply Nat (TyFun (NonEmpty a6989586621679753508) ([a6989586621679753508], [a6989586621679753508]) -> Type) (SplitAtSym0 a6989586621679753508) l #
type Apply Nat (TyFun (NonEmpty a6989586621679753508) ([a6989586621679753508], [a6989586621679753508]) -> Type) (SplitAtSym0 a6989586621679753508) l = SplitAtSym1 a6989586621679753508 l
type Apply a6989586621679475571 (TyFun [a6989586621679475571] [Nat] -> Type) (ElemIndicesSym0 a6989586621679475571) l #
type Apply a6989586621679475571 (TyFun [a6989586621679475571] [Nat] -> Type) (ElemIndicesSym0 a6989586621679475571) l = ElemIndicesSym1 a6989586621679475571 l
type Apply a6989586621679475572 (TyFun [a6989586621679475572] (Maybe Nat) -> Type) (ElemIndexSym0 a6989586621679475572) l #
type Apply a6989586621679475572 (TyFun [a6989586621679475572] (Maybe Nat) -> Type) (ElemIndexSym0 a6989586621679475572) l = ElemIndexSym1 a6989586621679475572 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 [a6989586621679475543] (TyFun Nat a6989586621679475543 -> Type) ((:!!$) a6989586621679475543) l #
type Apply [a6989586621679475543] (TyFun Nat a6989586621679475543 -> Type) ((:!!$) a6989586621679475543) l = (:!!$$) a6989586621679475543 l
type Apply (NonEmpty a6989586621679753488) (TyFun Nat a6989586621679753488 -> Type) ((:!!$) a6989586621679753488) l #
type Apply (NonEmpty a6989586621679753488) (TyFun Nat a6989586621679753488 -> Type) ((:!!$) a6989586621679753488) l = (:!!$$) a6989586621679753488 l
type Apply (TyFun a6989586621679475569 Bool -> Type) (TyFun [a6989586621679475569] [Nat] -> Type) (FindIndicesSym0 a6989586621679475569) l #
type Apply (TyFun a6989586621679475569 Bool -> Type) (TyFun [a6989586621679475569] [Nat] -> Type) (FindIndicesSym0 a6989586621679475569) l = FindIndicesSym1 a6989586621679475569 l
type Apply (TyFun a6989586621679475570 Bool -> Type) (TyFun [a6989586621679475570] (Maybe Nat) -> Type) (FindIndexSym0 a6989586621679475570) l #
type Apply (TyFun a6989586621679475570 Bool -> Type) (TyFun [a6989586621679475570] (Maybe Nat) -> Type) (FindIndexSym0 a6989586621679475570) l = FindIndexSym1 a6989586621679475570 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 k06989586621679418718 k6989586621679418720) #

Instances

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

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