Copyright | (C) 2014 Richard Eisenberg |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Ryan Scott |
Stability | experimental |
Portability | non-portable |
Safe Haskell | Safe-Inferred |
Language | GHC2021 |
Defines and exports singletons useful for the Natural, Symbol, and Char kinds.
Synopsis
- data Natural
- data Symbol
- data Char
- type family Sing :: k -> Type
- data SNat (n :: Nat)
- pattern SNat :: () => KnownNat n => SNat n
- data SSymbol (s :: Symbol)
- pattern SSymbol :: () => KnownSymbol s => SSymbol s
- pattern SSym :: forall s. () => KnownSymbol s => SSymbol s
- data SChar (s :: Char)
- pattern SChar :: () => KnownChar c => SChar c
- withKnownNat :: forall (n :: Nat) (rep :: RuntimeRep) (r :: TYPE rep). SNat n -> (KnownNat n => r) -> r
- withKnownSymbol :: forall (s :: Symbol) (rep :: RuntimeRep) (r :: TYPE rep). SSymbol s -> (KnownSymbol s => r) -> r
- withKnownChar :: forall (c :: Char) (rep :: RuntimeRep) (r :: TYPE rep). SChar c -> (KnownChar c => r) -> r
- type family Error (str :: Symbol) :: a where ...
- sError :: HasCallStack => Sing (str :: Symbol) -> a
- type family ErrorWithoutStackTrace (str :: Symbol) :: a where ...
- sErrorWithoutStackTrace :: Sing (str :: Symbol) -> a
- type family Undefined :: a where ...
- sUndefined :: HasCallStack => a
- class KnownNat (n :: Nat)
- natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Natural
- class KnownSymbol (n :: Symbol)
- symbolVal :: forall (n :: Symbol) proxy. KnownSymbol n => proxy n -> String
- class KnownChar (n :: Char)
- charVal :: forall (n :: Char) proxy. KnownChar n => proxy n -> Char
- type family (a :: Natural) ^ (b :: Natural) :: Natural where ...
- (%^) :: Sing a -> Sing b -> Sing (a ^ b)
- type (<=?) (m :: k) (n :: k) = OrdCond (Compare m n) 'True 'True 'False
- (%<=?) :: forall (a :: Natural) (b :: Natural). Sing a -> Sing b -> Sing (a <=? b)
- type family Log2 (a :: Natural) :: Natural where ...
- sLog2 :: Sing x -> Sing (Log2 x)
- type family Div (a :: Natural) (b :: Natural) :: Natural where ...
- sDiv :: Sing x -> Sing y -> Sing (Div x y)
- type family Mod (a :: Natural) (b :: Natural) :: Natural where ...
- sMod :: Sing x -> Sing y -> Sing (Mod x y)
- type family DivMod (a :: Natural) (a :: Natural) :: (Natural, Natural) where ...
- sDivMod :: Sing x -> Sing y -> Sing (DivMod x y)
- type family Quot (a :: Natural) (a :: Natural) :: Natural where ...
- sQuot :: Sing x -> Sing y -> Sing (Quot x y)
- type family Rem (a :: Natural) (a :: Natural) :: Natural where ...
- sRem :: Sing x -> Sing y -> Sing (Rem x y)
- type family QuotRem (a :: Natural) (a :: Natural) :: (Natural, Natural) where ...
- sQuotRem :: Sing x -> Sing y -> Sing (QuotRem x y)
- consSymbol :: Char -> String -> String
- type family ConsSymbol (a :: Char) (b :: Symbol) :: Symbol where ...
- sConsSymbol :: Sing x -> Sing y -> Sing (ConsSymbol x y)
- unconsSymbol :: String -> Maybe (Char, String)
- type family UnconsSymbol (a :: Symbol) :: Maybe (Char, Symbol) where ...
- sUnconsSymbol :: Sing x -> Sing (UnconsSymbol x)
- charToNat :: Char -> Natural
- type family CharToNat (a :: Char) :: Natural where ...
- sCharToNat :: Sing x -> Sing (CharToNat x)
- natToChar :: Natural -> Char
- type family NatToChar (a :: Natural) :: Char where ...
- sNatToChar :: Sing x -> Sing (NatToChar x)
- data ErrorSym0 :: (~>) Symbol a
- type family ErrorSym1 (a6989586621679450964 :: Symbol) :: a where ...
- data ErrorWithoutStackTraceSym0 :: (~>) Symbol a
- type family ErrorWithoutStackTraceSym1 (a6989586621679451222 :: Symbol) :: a where ...
- type family UndefinedSym0 :: a where ...
- data KnownNatSym0 :: (~>) Nat Constraint
- type family KnownNatSym1 (a6989586621679457769 :: Nat) :: Constraint where ...
- data KnownSymbolSym0 :: (~>) Symbol Constraint
- type family KnownSymbolSym1 (a6989586621679457771 :: Symbol) :: Constraint where ...
- data KnownCharSym0 :: (~>) Char Constraint
- type family KnownCharSym1 (a6989586621679457773 :: Char) :: Constraint where ...
- data (^@#@$) :: (~>) Natural ((~>) Natural Natural)
- data (^@#@$$) (a6989586621679451915 :: Natural) :: (~>) Natural Natural
- type family (a6989586621679451915 :: Natural) ^@#@$$$ (a6989586621679451916 :: Natural) :: Natural where ...
- data (<=?@#@$) :: (~>) k ((~>) k Bool)
- data (<=?@#@$$) (a6989586621679452355 :: k) :: (~>) k Bool
- type family (a6989586621679452355 :: k) <=?@#@$$$ (a6989586621679452356 :: k) :: Bool where ...
- data Log2Sym0 :: (~>) Natural Natural
- type family Log2Sym1 (a6989586621679458358 :: Natural) :: Natural where ...
- data DivSym0 :: (~>) Natural ((~>) Natural Natural)
- data DivSym1 (a6989586621679458584 :: Natural) :: (~>) Natural Natural
- type family DivSym2 (a6989586621679458584 :: Natural) (a6989586621679458585 :: Natural) :: Natural where ...
- data ModSym0 :: (~>) Natural ((~>) Natural Natural)
- data ModSym1 (a6989586621679459025 :: Natural) :: (~>) Natural Natural
- type family ModSym2 (a6989586621679459025 :: Natural) (a6989586621679459026 :: Natural) :: Natural where ...
- data DivModSym0 :: (~>) Natural ((~>) Natural (Natural, Natural))
- data DivModSym1 (a6989586621679459645 :: Natural) :: (~>) Natural (Natural, Natural)
- type family DivModSym2 (a6989586621679459645 :: Natural) (a6989586621679459646 :: Natural) :: (Natural, Natural) where ...
- data QuotSym0 :: (~>) Natural ((~>) Natural Natural)
- data QuotSym1 (a6989586621679459627 :: Natural) :: (~>) Natural Natural
- type family QuotSym2 (a6989586621679459627 :: Natural) (a6989586621679459628 :: Natural) :: Natural where ...
- data RemSym0 :: (~>) Natural ((~>) Natural Natural)
- data RemSym1 (a6989586621679459616 :: Natural) :: (~>) Natural Natural
- type family RemSym2 (a6989586621679459616 :: Natural) (a6989586621679459617 :: Natural) :: Natural where ...
- data QuotRemSym0 :: (~>) Natural ((~>) Natural (Natural, Natural))
- data QuotRemSym1 (a6989586621679459638 :: Natural) :: (~>) Natural (Natural, Natural)
- type family QuotRemSym2 (a6989586621679459638 :: Natural) (a6989586621679459639 :: Natural) :: (Natural, Natural) where ...
- data ConsSymbolSym0 :: (~>) Char ((~>) Symbol Symbol)
- data ConsSymbolSym1 (a6989586621679460905 :: Char) :: (~>) Symbol Symbol
- type family ConsSymbolSym2 (a6989586621679460905 :: Char) (a6989586621679460906 :: Symbol) :: Symbol where ...
- data UnconsSymbolSym0 :: (~>) Symbol (Maybe (Char, Symbol))
- type family UnconsSymbolSym1 (a6989586621679461421 :: Symbol) :: Maybe (Char, Symbol) where ...
- data CharToNatSym0 :: (~>) Char Natural
- type family CharToNatSym1 (a6989586621679461637 :: Char) :: Natural where ...
- data NatToCharSym0 :: (~>) Natural Char
- type family NatToCharSym1 (a6989586621679461858 :: Natural) :: Char where ...
Documentation
Instances
Instances
Instances
Bounded Char | |
Enum Char | |
Ix Char | |
Read Char | |
Show Char | |
NFData Char | |
Defined in Control.DeepSeq | |
Eq Char | |
Ord Char | |
SingKind Char Source # | |
SDecide Char Source # | |
PEq Char Source # | |
SEq Char Source # | |
POrd Char Source # | |
SOrd Char Source # | |
Defined in GHC.TypeLits.Singletons.Internal sCompare :: forall (t1 :: Char) (t2 :: Char). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) Source # (%<) :: forall (t1 :: Char) (t2 :: Char). Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) Source # (%<=) :: forall (t1 :: Char) (t2 :: Char). Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) Source # (%>) :: forall (t1 :: Char) (t2 :: Char). Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) Source # (%>=) :: forall (t1 :: Char) (t2 :: Char). Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) Source # sMax :: forall (t1 :: Char) (t2 :: Char). Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) Source # sMin :: forall (t1 :: Char) (t2 :: Char). Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) Source # | |
PBounded Char Source # | |
PEnum Char Source # | |
SBounded Char Source # | |
Defined in Data.Singletons.Base.Enum | |
SEnum Char Source # | |
Defined in Data.Singletons.Base.Enum sSucc :: forall (t :: Char). Sing t -> Sing (Apply SuccSym0 t) Source # sPred :: forall (t :: Char). Sing t -> Sing (Apply PredSym0 t) Source # sToEnum :: forall (t :: Natural). Sing t -> Sing (Apply ToEnumSym0 t) Source # sFromEnum :: forall (t :: Char). Sing t -> Sing (Apply FromEnumSym0 t) Source # sEnumFromTo :: forall (t1 :: Char) (t2 :: Char). Sing t1 -> Sing t2 -> Sing (Apply (Apply EnumFromToSym0 t1) t2) Source # sEnumFromThenTo :: forall (t1 :: Char) (t2 :: Char) (t3 :: Char). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t1) t2) t3) Source # | |
PShow Char Source # | |
SShow Char Source # | |
Defined in Text.Show.Singletons sShowsPrec :: forall (t1 :: Natural) (t2 :: Char) (t3 :: Symbol). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3) Source # sShow_ :: forall (t :: Char). Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: forall (t1 :: [Char]) (t2 :: Symbol). Sing t1 -> Sing t2 -> Sing (Apply (Apply ShowListSym0 t1) t2) Source # | |
TestCoercion SChar | |
Defined in GHC.TypeLits testCoercion :: forall (a :: k) (b :: k). SChar a -> SChar b -> Maybe (Coercion a b) | |
TestEquality SChar | |
Defined in GHC.TypeLits testEquality :: forall (a :: k) (b :: k). SChar a -> SChar b -> Maybe (a :~: b) | |
KnownChar c => SingI (c :: Char) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
Lift Char | |
Generic1 (URec Char :: k -> Type) | |
SingI1 ShowCharSym1 Source # | |
Defined in Text.Show.Singletons liftSing :: forall (x :: k1). Sing x -> Sing (ShowCharSym1 x) # | |
SingI1 ConsSymbolSym1 Source # | |
Defined in GHC.TypeLits.Singletons liftSing :: forall (x :: k1). Sing x -> Sing (ConsSymbolSym1 x) # | |
Foldable (UChar :: Type -> Type) | |
Defined in Data.Foldable fold :: Monoid m => UChar m -> m foldMap :: Monoid m => (a -> m) -> UChar a -> m foldMap' :: Monoid m => (a -> m) -> UChar a -> m foldr :: (a -> b -> b) -> b -> UChar a -> b foldr' :: (a -> b -> b) -> b -> UChar a -> b foldl :: (b -> a -> b) -> b -> UChar a -> b foldl' :: (b -> a -> b) -> b -> UChar a -> b foldr1 :: (a -> a -> a) -> UChar a -> a foldl1 :: (a -> a -> a) -> UChar a -> a toList :: UChar a -> [a] null :: UChar a -> Bool length :: UChar a -> Int elem :: Eq a => a -> UChar a -> Bool maximum :: Ord a => UChar a -> a minimum :: Ord a => UChar a -> a sum :: Num a => UChar a -> a product :: Num a => UChar a -> a | |
Traversable (UChar :: Type -> Type) | |
Defined in Data.Traversable | |
Functor (URec Char :: Type -> Type) | |
SingI ShowCharSym0 Source # | |
Defined in Text.Show.Singletons sing :: Sing ShowCharSym0 # | |
SingI NatToCharSym0 Source # | |
Defined in GHC.TypeLits.Singletons sing :: Sing NatToCharSym0 # | |
SingI ConsSymbolSym0 Source # | |
Defined in GHC.TypeLits.Singletons sing :: Sing ConsSymbolSym0 # | |
SingI CharToNatSym0 Source # | |
Defined in GHC.TypeLits.Singletons sing :: Sing CharToNatSym0 # | |
SingI UnconsSymbolSym0 Source # | |
Defined in GHC.TypeLits.Singletons | |
SuppressUnusedWarnings NatToCharSym0 Source # | |
Defined in GHC.TypeLits.Singletons suppressUnusedWarnings :: () # | |
SuppressUnusedWarnings ConsSymbolSym0 Source # | |
Defined in GHC.TypeLits.Singletons suppressUnusedWarnings :: () # | |
SuppressUnusedWarnings ShowCharSym0 Source # | |
Defined in Text.Show.Singletons suppressUnusedWarnings :: () # | |
SuppressUnusedWarnings CharToNatSym0 Source # | |
Defined in GHC.TypeLits.Singletons suppressUnusedWarnings :: () # | |
SuppressUnusedWarnings KnownCharSym0 Source # | |
Defined in GHC.TypeLits.Singletons suppressUnusedWarnings :: () # | |
SuppressUnusedWarnings UnconsSymbolSym0 Source # | |
Defined in GHC.TypeLits.Singletons suppressUnusedWarnings :: () # | |
SMonadFail m => SingI (FailSym0 :: TyFun [Char] (m a) -> Type) Source # | |
Defined in Control.Monad.Fail.Singletons | |
SuppressUnusedWarnings (FailSym0 :: TyFun [Char] (m a) -> Type) Source # | |
Defined in Control.Monad.Fail.Singletons suppressUnusedWarnings :: () # | |
Generic (URec Char p) | |
Show (URec Char p) | |
Eq (URec Char p) | |
Ord (URec Char p) | |
type Demote Char Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
type Sing Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
type MaxBound Source # | |
Defined in Data.Singletons.Base.Enum type MaxBound | |
type MinBound Source # | |
Defined in Data.Singletons.Base.Enum type MinBound | |
data URec Char (p :: k) | |
Defined in GHC.Generics | |
type FromEnum (a :: Char) Source # | |
Defined in Data.Singletons.Base.Enum | |
type Pred (arg :: Char) Source # | |
Defined in Data.Singletons.Base.Enum | |
type Succ (arg :: Char) Source # | |
Defined in Data.Singletons.Base.Enum | |
type ToEnum a Source # | |
Defined in Data.Singletons.Base.Enum type ToEnum a | |
type Show_ (arg :: Char) Source # | |
Defined in Text.Show.Singletons | |
type Compare (a :: Char) (b :: Char) | |
Defined in Data.Type.Ord | |
type (arg :: Char) /= (arg1 :: Char) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
type (x :: Char) == (y :: Char) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
type (arg :: Char) < (arg1 :: Char) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
type (arg :: Char) <= (arg1 :: Char) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
type (arg :: Char) > (arg1 :: Char) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
type (arg :: Char) >= (arg1 :: Char) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
type Compare (a :: Char) (b :: Char) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
type Max (arg :: Char) (arg1 :: Char) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
type Min (arg :: Char) (arg1 :: Char) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
type EnumFromTo (arg1 :: Char) (arg2 :: Char) Source # | |
Defined in Data.Singletons.Base.Enum | |
type ShowList (cs :: [Char]) x Source # | |
Defined in Text.Show.Singletons | |
type Apply NatToCharSym0 (a6989586621679461858 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons | |
type Apply CharToNatSym0 (a6989586621679461637 :: Char) Source # | |
Defined in GHC.TypeLits.Singletons | |
type Apply KnownCharSym0 (a6989586621679457773 :: Char) Source # | |
Defined in GHC.TypeLits.Singletons | |
type EnumFromThenTo (arg1 :: Char) (arg2 :: Char) (arg3 :: Char) Source # | |
Defined in Data.Singletons.Base.Enum | |
type ShowsPrec p (c :: Char) x Source # | |
Defined in Text.Show.Singletons | |
type Apply UnconsSymbolSym0 (a6989586621679461421 :: Symbol) Source # | |
Defined in GHC.TypeLits.Singletons | |
type Rep1 (URec Char :: k -> Type) | |
Defined in GHC.Generics type Rep1 (URec Char :: k -> Type) = D1 ('MetaData "URec" "GHC.Generics" "base" 'False) (C1 ('MetaCons "UChar" 'PrefixI 'True) (S1 ('MetaSel ('Just "uChar#") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (UChar :: k -> Type))) | |
type Apply ConsSymbolSym0 (a6989586621679460905 :: Char) Source # | |
Defined in GHC.TypeLits.Singletons | |
type Apply ShowCharSym0 (a6989586621679965708 :: Char) Source # | |
Defined in Text.Show.Singletons | |
type Apply (FailSym0 :: TyFun [Char] (m a) -> Type) (a6989586621679444078 :: [Char]) Source # | |
type Rep (URec Char p) | |
Defined in GHC.Generics type Rep (URec Char p) = D1 ('MetaData "URec" "GHC.Generics" "base" 'False) (C1 ('MetaCons "UChar" 'PrefixI 'True) (S1 ('MetaSel ('Just "uChar#") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (UChar :: Type -> Type))) |
type family Sing :: k -> Type #
The singleton kind-indexed type family.
Instances
Instances
TestCoercion SNat | |
Defined in GHC.TypeNats testCoercion :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (Coercion a b) | |
TestEquality SNat | |
Defined in GHC.TypeNats testEquality :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b) | |
Show (SNat n) | |
Instances
TestCoercion SSymbol | |
Defined in GHC.TypeLits testCoercion :: forall (a :: k) (b :: k). SSymbol a -> SSymbol b -> Maybe (Coercion a b) | |
TestEquality SSymbol | |
Defined in GHC.TypeLits testEquality :: forall (a :: k) (b :: k). SSymbol a -> SSymbol b -> Maybe (a :~: b) | |
Show (SSymbol s) | |
pattern SSymbol :: () => KnownSymbol s => SSymbol s #
pattern SSym :: forall s. () => KnownSymbol s => SSymbol s Source #
An alias for the SSymbol
pattern synonym.
Instances
TestCoercion SChar | |
Defined in GHC.TypeLits testCoercion :: forall (a :: k) (b :: k). SChar a -> SChar b -> Maybe (Coercion a b) | |
TestEquality SChar | |
Defined in GHC.TypeLits testEquality :: forall (a :: k) (b :: k). SChar a -> SChar b -> Maybe (a :~: b) | |
Show (SChar c) | |
withKnownNat :: forall (n :: Nat) (rep :: RuntimeRep) (r :: TYPE rep). SNat n -> (KnownNat n => r) -> r #
withKnownSymbol :: forall (s :: Symbol) (rep :: RuntimeRep) (r :: TYPE rep). SSymbol s -> (KnownSymbol s => r) -> r #
withKnownChar :: forall (c :: Char) (rep :: RuntimeRep) (r :: TYPE rep). SChar c -> (KnownChar c => r) -> r #
type family Error (str :: Symbol) :: a where ... Source #
A promoted version of error
. This implements Error
as a stuck type
family with a Symbol
argument. Depending on your needs, you might also
consider the following alternatives:
- Data.Singletons.Base.PolyError provides
PolyError
, which generalizes the argument to be kind-polymorphic. This allows passing additional information to the error besides rawSymbol
s. - Data.Singletons.Base.TypeError provides
TypeError
, a slightly modified version of the custom type error machinery found in GHC.TypeLits. This allows emitting error messages as compiler errors rather than as stuck type families.
type family ErrorWithoutStackTrace (str :: Symbol) :: a where ... Source #
The promotion of errorWithoutStackTrace
.
sErrorWithoutStackTrace :: Sing (str :: Symbol) -> a Source #
The singleton for errorWithoutStackTrace
.
sUndefined :: HasCallStack => a Source #
The singleton for undefined
.
class KnownSymbol (n :: Symbol) #
symbolSing
symbolVal :: forall (n :: Symbol) proxy. KnownSymbol n => proxy n -> String #
(%<=?) :: forall (a :: Natural) (b :: Natural). Sing a -> Sing b -> Sing (a <=? b) infix 4 Source #
The singleton analogue of <=?
Note that, because of historical reasons in GHC's Natural
API, <=?
is incompatible (unification-wise) with <=
and the PEq
, SEq
,
POrd
, and SOrd
instances for Natural
. (a
does not
imply anything about <=?
b) ~ 'Truea
or any other <=
bPEq
/ POrd
relationships.
(Be aware that <=
in the paragraph above refers to <=
from the
POrd
typeclass, exported from Data.Ord.Singletons, and not
the <=
from GHC.TypeNats. The latter is simply a type alias for
(a
.)<=?
b) ~ 'True
This is provided here for the sake of completeness and for compatibility
with libraries with APIs built around <=?
. New code should use
CmpNat
, exposed through this library through the POrd
and SOrd
instances for Natural
.
type family QuotRem (a :: Natural) (a :: Natural) :: (Natural, Natural) where ... Source #
QuotRem a_6989586621679459631 a_6989586621679459633 = Apply (Apply DivModSym0 a_6989586621679459631) a_6989586621679459633 |
consSymbol :: Char -> String -> String Source #
type family ConsSymbol (a :: Char) (b :: Symbol) :: Symbol where ... #
sConsSymbol :: Sing x -> Sing y -> Sing (ConsSymbol x y) Source #
unconsSymbol :: String -> Maybe (Char, String) Source #
type family UnconsSymbol (a :: Symbol) :: Maybe (Char, Symbol) where ... #
sUnconsSymbol :: Sing x -> Sing (UnconsSymbol x) Source #
Defunctionalization symbols
data ErrorSym0 :: (~>) Symbol a Source #
Instances
SingI (ErrorSym0 :: TyFun Symbol a -> Type) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
SuppressUnusedWarnings (ErrorSym0 :: TyFun Symbol a -> Type) Source # | |
Defined in GHC.TypeLits.Singletons.Internal suppressUnusedWarnings :: () # | |
type Apply (ErrorSym0 :: TyFun Symbol k2 -> Type) (a6989586621679450964 :: Symbol) Source # | |
data ErrorWithoutStackTraceSym0 :: (~>) Symbol a Source #
Instances
SingI (ErrorWithoutStackTraceSym0 :: TyFun Symbol a -> Type) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
SuppressUnusedWarnings (ErrorWithoutStackTraceSym0 :: TyFun Symbol a -> Type) Source # | |
Defined in GHC.TypeLits.Singletons.Internal suppressUnusedWarnings :: () # | |
type Apply (ErrorWithoutStackTraceSym0 :: TyFun Symbol k2 -> Type) (a6989586621679451222 :: Symbol) Source # | |
Defined in GHC.TypeLits.Singletons.Internal type Apply (ErrorWithoutStackTraceSym0 :: TyFun Symbol k2 -> Type) (a6989586621679451222 :: Symbol) = ErrorWithoutStackTrace a6989586621679451222 :: k2 |
type family ErrorWithoutStackTraceSym1 (a6989586621679451222 :: Symbol) :: a where ... Source #
ErrorWithoutStackTraceSym1 a6989586621679451222 = ErrorWithoutStackTrace a6989586621679451222 |
type family UndefinedSym0 :: a where ... Source #
data KnownNatSym0 :: (~>) Nat Constraint Source #
Instances
SuppressUnusedWarnings KnownNatSym0 Source # | |
Defined in GHC.TypeLits.Singletons suppressUnusedWarnings :: () # | |
type Apply KnownNatSym0 (a6989586621679457769 :: Nat) Source # | |
Defined in GHC.TypeLits.Singletons |
type family KnownNatSym1 (a6989586621679457769 :: Nat) :: Constraint where ... Source #
KnownNatSym1 a6989586621679457769 = KnownNat a6989586621679457769 |
data KnownSymbolSym0 :: (~>) Symbol Constraint Source #
Instances
SuppressUnusedWarnings KnownSymbolSym0 Source # | |
Defined in GHC.TypeLits.Singletons suppressUnusedWarnings :: () # | |
type Apply KnownSymbolSym0 (a6989586621679457771 :: Symbol) Source # | |
Defined in GHC.TypeLits.Singletons |
type family KnownSymbolSym1 (a6989586621679457771 :: Symbol) :: Constraint where ... Source #
KnownSymbolSym1 a6989586621679457771 = KnownSymbol a6989586621679457771 |
data KnownCharSym0 :: (~>) Char Constraint Source #
Instances
SuppressUnusedWarnings KnownCharSym0 Source # | |
Defined in GHC.TypeLits.Singletons suppressUnusedWarnings :: () # | |
type Apply KnownCharSym0 (a6989586621679457773 :: Char) Source # | |
Defined in GHC.TypeLits.Singletons |
type family KnownCharSym1 (a6989586621679457773 :: Char) :: Constraint where ... Source #
KnownCharSym1 a6989586621679457773 = KnownChar a6989586621679457773 |
data (^@#@$) :: (~>) Natural ((~>) Natural Natural) infixr 8 Source #
Instances
SingI (^@#@$) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
SuppressUnusedWarnings (^@#@$) Source # | |
Defined in GHC.TypeLits.Singletons.Internal suppressUnusedWarnings :: () # | |
type Apply (^@#@$) (a6989586621679451915 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons.Internal |
data (^@#@$$) (a6989586621679451915 :: Natural) :: (~>) Natural Natural infixr 8 Source #
Instances
SingI1 (^@#@$$) Source # | |
SingI x => SingI ((^@#@$$) x :: TyFun Natural Natural -> Type) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
SuppressUnusedWarnings ((^@#@$$) a6989586621679451915 :: TyFun Natural Natural -> Type) Source # | |
Defined in GHC.TypeLits.Singletons.Internal suppressUnusedWarnings :: () # | |
type Apply ((^@#@$$) a6989586621679451915 :: TyFun Natural Natural -> Type) (a6989586621679451916 :: Natural) Source # | |
type family (a6989586621679451915 :: Natural) ^@#@$$$ (a6989586621679451916 :: Natural) :: Natural where ... infixr 8 Source #
data (<=?@#@$) :: (~>) k ((~>) k Bool) infix 4 Source #
Instances
SingI ((<=?@#@$) :: TyFun Natural (Natural ~> Bool) -> Type) Source # | |
Defined in GHC.TypeLits.Singletons.Internal | |
SuppressUnusedWarnings ((<=?@#@$) :: TyFun k (k ~> Bool) -> Type) Source # | |
Defined in GHC.TypeLits.Singletons.Internal suppressUnusedWarnings :: () # | |
type Apply ((<=?@#@$) :: TyFun k (k ~> Bool) -> Type) (a6989586621679452355 :: k) Source # | |
Defined in GHC.TypeLits.Singletons.Internal type Apply ((<=?@#@$) :: TyFun k (k ~> Bool) -> Type) (a6989586621679452355 :: k) = (<=?@#@$$) a6989586621679452355 |
data (<=?@#@$$) (a6989586621679452355 :: k) :: (~>) k Bool infix 4 Source #
Instances
SingI1 ((<=?@#@$$) :: Natural -> TyFun Natural Bool -> Type) Source # | |
Defined in GHC.TypeLits.Singletons.Internal liftSing :: forall (x :: k1). Sing x -> Sing ((<=?@#@$$) x) # | |
SingI x => SingI ((<=?@#@$$) x :: TyFun Natural Bool -> Type) Source # | |
Defined in GHC.TypeLits.Singletons.Internal sing :: Sing ((<=?@#@$$) x) # | |
SuppressUnusedWarnings ((<=?@#@$$) a6989586621679452355 :: TyFun k Bool -> Type) Source # | |
Defined in GHC.TypeLits.Singletons.Internal suppressUnusedWarnings :: () # | |
type Apply ((<=?@#@$$) a6989586621679452355 :: TyFun k Bool -> Type) (a6989586621679452356 :: k) Source # | |
Defined in GHC.TypeLits.Singletons.Internal type Apply ((<=?@#@$$) a6989586621679452355 :: TyFun k Bool -> Type) (a6989586621679452356 :: k) = a6989586621679452355 <=? a6989586621679452356 |
type family (a6989586621679452355 :: k) <=?@#@$$$ (a6989586621679452356 :: k) :: Bool where ... infix 4 Source #
data Log2Sym0 :: (~>) Natural Natural Source #
Instances
SingI Log2Sym0 Source # | |
Defined in GHC.TypeLits.Singletons | |
SuppressUnusedWarnings Log2Sym0 Source # | |
Defined in GHC.TypeLits.Singletons suppressUnusedWarnings :: () # | |
type Apply Log2Sym0 (a6989586621679458358 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons |
data DivSym0 :: (~>) Natural ((~>) Natural Natural) infixl 7 Source #
Instances
SingI DivSym0 Source # | |
Defined in GHC.TypeLits.Singletons | |
SuppressUnusedWarnings DivSym0 Source # | |
Defined in GHC.TypeLits.Singletons suppressUnusedWarnings :: () # | |
type Apply DivSym0 (a6989586621679458584 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons |
data DivSym1 (a6989586621679458584 :: Natural) :: (~>) Natural Natural infixl 7 Source #
Instances
SingI1 DivSym1 Source # | |
SingI x => SingI (DivSym1 x :: TyFun Natural Natural -> Type) Source # | |
Defined in GHC.TypeLits.Singletons | |
SuppressUnusedWarnings (DivSym1 a6989586621679458584 :: TyFun Natural Natural -> Type) Source # | |
Defined in GHC.TypeLits.Singletons suppressUnusedWarnings :: () # | |
type Apply (DivSym1 a6989586621679458584 :: TyFun Natural Natural -> Type) (a6989586621679458585 :: Natural) Source # | |
type family DivSym2 (a6989586621679458584 :: Natural) (a6989586621679458585 :: Natural) :: Natural where ... infixl 7 Source #
data ModSym0 :: (~>) Natural ((~>) Natural Natural) infixl 7 Source #
Instances
SingI ModSym0 Source # | |
Defined in GHC.TypeLits.Singletons | |
SuppressUnusedWarnings ModSym0 Source # | |
Defined in GHC.TypeLits.Singletons suppressUnusedWarnings :: () # | |
type Apply ModSym0 (a6989586621679459025 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons |
data ModSym1 (a6989586621679459025 :: Natural) :: (~>) Natural Natural infixl 7 Source #
Instances
SingI1 ModSym1 Source # | |
SingI x => SingI (ModSym1 x :: TyFun Natural Natural -> Type) Source # | |
Defined in GHC.TypeLits.Singletons | |
SuppressUnusedWarnings (ModSym1 a6989586621679459025 :: TyFun Natural Natural -> Type) Source # | |
Defined in GHC.TypeLits.Singletons suppressUnusedWarnings :: () # | |
type Apply (ModSym1 a6989586621679459025 :: TyFun Natural Natural -> Type) (a6989586621679459026 :: Natural) Source # | |
type family ModSym2 (a6989586621679459025 :: Natural) (a6989586621679459026 :: Natural) :: Natural where ... infixl 7 Source #
data DivModSym0 :: (~>) Natural ((~>) Natural (Natural, Natural)) Source #
Instances
SuppressUnusedWarnings DivModSym0 Source # | |
Defined in GHC.TypeLits.Singletons suppressUnusedWarnings :: () # | |
type Apply DivModSym0 (a6989586621679459645 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons |
data DivModSym1 (a6989586621679459645 :: Natural) :: (~>) Natural (Natural, Natural) Source #
Instances
SuppressUnusedWarnings (DivModSym1 a6989586621679459645 :: TyFun Natural (Natural, Natural) -> Type) Source # | |
Defined in GHC.TypeLits.Singletons suppressUnusedWarnings :: () # | |
type Apply (DivModSym1 a6989586621679459645 :: TyFun Natural (Natural, Natural) -> Type) (a6989586621679459646 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons |
type family DivModSym2 (a6989586621679459645 :: Natural) (a6989586621679459646 :: Natural) :: (Natural, Natural) where ... Source #
DivModSym2 a6989586621679459645 a6989586621679459646 = DivMod a6989586621679459645 a6989586621679459646 |
data QuotSym0 :: (~>) Natural ((~>) Natural Natural) infixl 7 Source #
Instances
SuppressUnusedWarnings QuotSym0 Source # | |
Defined in GHC.TypeLits.Singletons suppressUnusedWarnings :: () # | |
type Apply QuotSym0 (a6989586621679459627 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons |
data QuotSym1 (a6989586621679459627 :: Natural) :: (~>) Natural Natural infixl 7 Source #
type family QuotSym2 (a6989586621679459627 :: Natural) (a6989586621679459628 :: Natural) :: Natural where ... infixl 7 Source #
data RemSym0 :: (~>) Natural ((~>) Natural Natural) infixl 7 Source #
Instances
SuppressUnusedWarnings RemSym0 Source # | |
Defined in GHC.TypeLits.Singletons suppressUnusedWarnings :: () # | |
type Apply RemSym0 (a6989586621679459616 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons |
data RemSym1 (a6989586621679459616 :: Natural) :: (~>) Natural Natural infixl 7 Source #
type family RemSym2 (a6989586621679459616 :: Natural) (a6989586621679459617 :: Natural) :: Natural where ... infixl 7 Source #
data QuotRemSym0 :: (~>) Natural ((~>) Natural (Natural, Natural)) Source #
Instances
SuppressUnusedWarnings QuotRemSym0 Source # | |
Defined in GHC.TypeLits.Singletons suppressUnusedWarnings :: () # | |
type Apply QuotRemSym0 (a6989586621679459638 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons |
data QuotRemSym1 (a6989586621679459638 :: Natural) :: (~>) Natural (Natural, Natural) Source #
Instances
SuppressUnusedWarnings (QuotRemSym1 a6989586621679459638 :: TyFun Natural (Natural, Natural) -> Type) Source # | |
Defined in GHC.TypeLits.Singletons suppressUnusedWarnings :: () # | |
type Apply (QuotRemSym1 a6989586621679459638 :: TyFun Natural (Natural, Natural) -> Type) (a6989586621679459639 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons |
type family QuotRemSym2 (a6989586621679459638 :: Natural) (a6989586621679459639 :: Natural) :: (Natural, Natural) where ... Source #
QuotRemSym2 a6989586621679459638 a6989586621679459639 = QuotRem a6989586621679459638 a6989586621679459639 |
data ConsSymbolSym0 :: (~>) Char ((~>) Symbol Symbol) Source #
Instances
SingI ConsSymbolSym0 Source # | |
Defined in GHC.TypeLits.Singletons sing :: Sing ConsSymbolSym0 # | |
SuppressUnusedWarnings ConsSymbolSym0 Source # | |
Defined in GHC.TypeLits.Singletons suppressUnusedWarnings :: () # | |
type Apply ConsSymbolSym0 (a6989586621679460905 :: Char) Source # | |
Defined in GHC.TypeLits.Singletons |
data ConsSymbolSym1 (a6989586621679460905 :: Char) :: (~>) Symbol Symbol Source #
Instances
SingI1 ConsSymbolSym1 Source # | |
Defined in GHC.TypeLits.Singletons liftSing :: forall (x :: k1). Sing x -> Sing (ConsSymbolSym1 x) # | |
SingI x => SingI (ConsSymbolSym1 x :: TyFun Symbol Symbol -> Type) Source # | |
Defined in GHC.TypeLits.Singletons sing :: Sing (ConsSymbolSym1 x) # | |
SuppressUnusedWarnings (ConsSymbolSym1 a6989586621679460905 :: TyFun Symbol Symbol -> Type) Source # | |
Defined in GHC.TypeLits.Singletons suppressUnusedWarnings :: () # | |
type Apply (ConsSymbolSym1 a6989586621679460905 :: TyFun Symbol Symbol -> Type) (a6989586621679460906 :: Symbol) Source # | |
Defined in GHC.TypeLits.Singletons type Apply (ConsSymbolSym1 a6989586621679460905 :: TyFun Symbol Symbol -> Type) (a6989586621679460906 :: Symbol) = ConsSymbol a6989586621679460905 a6989586621679460906 |
type family ConsSymbolSym2 (a6989586621679460905 :: Char) (a6989586621679460906 :: Symbol) :: Symbol where ... Source #
ConsSymbolSym2 a6989586621679460905 a6989586621679460906 = ConsSymbol a6989586621679460905 a6989586621679460906 |
data UnconsSymbolSym0 :: (~>) Symbol (Maybe (Char, Symbol)) Source #
Instances
SingI UnconsSymbolSym0 Source # | |
Defined in GHC.TypeLits.Singletons | |
SuppressUnusedWarnings UnconsSymbolSym0 Source # | |
Defined in GHC.TypeLits.Singletons suppressUnusedWarnings :: () # | |
type Apply UnconsSymbolSym0 (a6989586621679461421 :: Symbol) Source # | |
Defined in GHC.TypeLits.Singletons |
type family UnconsSymbolSym1 (a6989586621679461421 :: Symbol) :: Maybe (Char, Symbol) where ... Source #
UnconsSymbolSym1 a6989586621679461421 = UnconsSymbol a6989586621679461421 |
data CharToNatSym0 :: (~>) Char Natural Source #
Instances
SingI CharToNatSym0 Source # | |
Defined in GHC.TypeLits.Singletons sing :: Sing CharToNatSym0 # | |
SuppressUnusedWarnings CharToNatSym0 Source # | |
Defined in GHC.TypeLits.Singletons suppressUnusedWarnings :: () # | |
type Apply CharToNatSym0 (a6989586621679461637 :: Char) Source # | |
Defined in GHC.TypeLits.Singletons |
type family CharToNatSym1 (a6989586621679461637 :: Char) :: Natural where ... Source #
CharToNatSym1 a6989586621679461637 = CharToNat a6989586621679461637 |
data NatToCharSym0 :: (~>) Natural Char Source #
Instances
SingI NatToCharSym0 Source # | |
Defined in GHC.TypeLits.Singletons sing :: Sing NatToCharSym0 # | |
SuppressUnusedWarnings NatToCharSym0 Source # | |
Defined in GHC.TypeLits.Singletons suppressUnusedWarnings :: () # | |
type Apply NatToCharSym0 (a6989586621679461858 :: Natural) Source # | |
Defined in GHC.TypeLits.Singletons |
type family NatToCharSym1 (a6989586621679461858 :: Natural) :: Char where ... Source #
NatToCharSym1 a6989586621679461858 = NatToChar a6989586621679461858 |
Orphan instances
IsString Symbol Source # | |
fromString :: String -> Symbol | |
Monoid Symbol Source # | |
Semigroup Symbol Source # | |
Show Symbol Source # | |
Eq Symbol Source # | 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. |
Ord Symbol Source # | |