-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | A framework for generating singleton types
--
-- singletons-th defines Template Haskell functionality that
-- allows promotion of term-level functions to type-level
-- equivalents and singling functions to dependently typed
-- equivalents. This library was originally presented in Dependently
-- Typed Programming with Singletons, published at the Haskell
-- Symposium, 2012.
-- (https://richarde.dev/papers/2012/singletons/paper.pdf) See
-- also the paper published at Haskell Symposium, 2014, which describes
-- how promotion works in greater detail:
-- https://richarde.dev/papers/2014/promotion/promotion.pdf.
--
-- singletons-th generates code that relies on bleeding-edge GHC
-- language extensions. As such, singletons-th only supports the
-- latest major version of GHC (currently GHC 9.8). For more information,
-- consult the singletons README.
--
-- You may also be interested in the following related libraries:
--
--
-- - The singletons library is a small, foundational library
-- that defines basic singleton-related types and definitions.
-- - The singletons-base library uses singletons-th
-- to define promoted and singled functions from the base
-- library, including the Prelude.
--
@package singletons-th
@version 3.3
module Data.Singletons.TH.SuppressUnusedWarnings
-- | This class (which users should never see) is to be instantiated in
-- order to use an otherwise-unused data constructor, such as the
-- "kind-inference" data constructor for defunctionalization symbols.
class SuppressUnusedWarnings (t :: k)
suppressUnusedWarnings :: SuppressUnusedWarnings t => ()
-- | This module defines Options that control finer details of how
-- the Template Haskell machinery works, as well as an mtl-like
-- OptionsMonad class and an OptionsM monad transformer.
module Data.Singletons.TH.Options
-- | Options that control the finer details of how singletons-th's
-- Template Haskell machinery works.
data Options
-- | Sensible default Options.
--
-- genQuotedDecs defaults to True. That is, quoted
-- declarations are generated alongside their promoted and singled
-- counterparts.
--
-- genSingKindInsts defaults to True. That is,
-- SingKind instances are generated.
--
-- The default behaviors for promotedClassName,
-- promotedValueNamePrefix, singledDataTypeName,
-- singledClassName, singledDataConName,
-- singledValueName, and defunctionalizedName are described
-- in the "On names" section of the singletons
-- README.
defaultOptions :: Options
-- | If True, then quoted declarations will be generated alongside
-- their promoted and singled counterparts. If False, then quoted
-- declarations will be discarded.
genQuotedDecs :: Options -> Bool
-- | If True, then SingKind instances will be generated. If
-- False, they will be omitted entirely. This can be useful in
-- scenarios where TH-generated SingKind instances do not
-- typecheck (for instance, when generating singletons for GADTs).
genSingKindInsts :: Options -> Bool
-- | Given the name of the original data type or data constructor, produces
-- the name of the promoted equivalent. Unlike the singling-related
-- options, in which there are separate singledDataTypeName and
-- singledDataConName functions, we combine the handling of
-- promoted data types and data constructors into a single option. This
-- is because the names of promoted data types and data constructors can
-- be difficult to distinguish in certain contexts without expensive
-- compile-time checks.
--
-- Because of the DataKinds extension, most data type and data
-- constructor names can be used in promoted contexts without any
-- changes. As a result, this option will act like the identity function
-- 99% of the time. There are some situations where it can be useful to
-- override this option, however, as it can be used to promote primitive
-- data types that do not have proper type-level equivalents, such as
-- Natural and Text. See the "Arrows, Nat,
-- Symbol, and literals" section of the singletons
-- README for more details.
promotedDataTypeOrConName :: Options -> Name -> Name
-- | Given the name of the original, unrefined class, produces the name of
-- the promoted equivalent of the class.
promotedClassName :: Options -> Name -> Name
-- | Given the name of the original, unrefined value, produces the name of
-- the promoted equivalent of the value. This is used for both top-level
-- and let-bound names, and the difference is encoded in the
-- Maybe Uniq argument. If promoting a top-level
-- name, the argument is Nothing. If promoting a
-- let-bound name, the argument is Just uniq, where
-- uniq is a globally unique number that can be used to
-- distinguish the name from other local definitions of the same name
-- (e.g., if two functions both use let x = ... in x).
promotedValueName :: Options -> Name -> Maybe Uniq -> Name
-- | Given the name of the original, unrefined data type, produces the name
-- of the corresponding singleton type.
singledDataTypeName :: Options -> Name -> Name
-- | Given the name of the original, unrefined class, produces the name of
-- the singled equivalent of the class.
singledClassName :: Options -> Name -> Name
-- | Given the name of the original, unrefined data constructor, produces
-- the name of the corresponding singleton data constructor.
singledDataConName :: Options -> Name -> Name
-- | Given the name of the original, unrefined value, produces the name of
-- the singled equivalent of the value.
singledValueName :: Options -> Name -> Name
-- | Given the original name and the number of parameters it is applied to
-- (the Int argument), produces a type-level function name that
-- can be partially applied when given the same number of parameters.
--
-- Note that defunctionalization works over both term-level names
-- (producing symbols for the promoted name) and type-level names
-- (producing symbols directly for the name itself). As a result, this
-- callback is used for names in both the term and type namespaces.
defunctionalizedName :: Options -> Name -> Int -> Name
-- | Given the name of the original, unrefined, top-level value, produces
-- the name of the promoted equivalent of the value.
promotedTopLevelValueName :: Options -> Name -> Name
-- | Given the name of the original, unrefined, let-bound value
-- and its globally unique number, produces the name of the promoted
-- equivalent of the value.
promotedLetBoundValueName :: Options -> Name -> Uniq -> Name
-- | Given the original name of a function (term- or type-level), produces
-- a type-level function name that can be partially applied even without
-- being given any arguments (i.e., 0 arguments).
defunctionalizedName0 :: Options -> Name -> Name
-- | Class that describes monads that contain Options.
class DsMonad m => OptionsMonad (m :: Type -> Type)
getOptions :: OptionsMonad m => m Options
-- | A convenient implementation of the OptionsMonad class. Use by
-- calling withOptions.
data OptionsM (m :: Type -> Type) a
-- | Declare the Options that a TH computation should use.
withOptions :: Options -> OptionsM m a -> m a
instance GHC.Base.Applicative m => GHC.Base.Applicative (Data.Singletons.TH.Options.OptionsM m)
instance Language.Haskell.TH.Desugar.Reify.DsMonad m => Language.Haskell.TH.Desugar.Reify.DsMonad (Data.Singletons.TH.Options.OptionsM m)
instance GHC.Base.Functor m => GHC.Base.Functor (Data.Singletons.TH.Options.OptionsM m)
instance Control.Monad.Fail.MonadFail m => Control.Monad.Fail.MonadFail (Data.Singletons.TH.Options.OptionsM m)
instance Control.Monad.IO.Class.MonadIO m => Control.Monad.IO.Class.MonadIO (Data.Singletons.TH.Options.OptionsM m)
instance GHC.Base.Monad m => GHC.Base.Monad (Data.Singletons.TH.Options.OptionsM m)
instance Control.Monad.Trans.Class.MonadTrans Data.Singletons.TH.Options.OptionsM
instance Data.Singletons.TH.Options.OptionsMonad m => Data.Singletons.TH.Options.OptionsMonad (Language.Haskell.TH.Desugar.Reify.DsM m)
instance Language.Haskell.TH.Desugar.Reify.DsMonad m => Data.Singletons.TH.Options.OptionsMonad (Data.Singletons.TH.Options.OptionsM m)
instance Data.Singletons.TH.Options.OptionsMonad Language.Haskell.TH.Syntax.Q
instance (Data.Singletons.TH.Options.OptionsMonad q, GHC.Base.Monoid m) => Data.Singletons.TH.Options.OptionsMonad (Data.Singletons.TH.Util.QWithAux m q)
instance (Data.Singletons.TH.Options.OptionsMonad m, GHC.Base.Monoid w) => Data.Singletons.TH.Options.OptionsMonad (Control.Monad.Trans.RWS.Lazy.RWST r w s m)
instance Data.Singletons.TH.Options.OptionsMonad m => Data.Singletons.TH.Options.OptionsMonad (Control.Monad.Trans.Reader.ReaderT r m)
instance Data.Singletons.TH.Options.OptionsMonad m => Data.Singletons.TH.Options.OptionsMonad (Control.Monad.Trans.State.Lazy.StateT s m)
instance (Data.Singletons.TH.Options.OptionsMonad m, GHC.Base.Monoid w) => Data.Singletons.TH.Options.OptionsMonad (Control.Monad.Trans.Writer.Lazy.WriterT w m)
instance Language.Haskell.TH.Syntax.Quasi m => Language.Haskell.TH.Syntax.Quasi (Data.Singletons.TH.Options.OptionsM m)
instance Language.Haskell.TH.Syntax.Quote m => Language.Haskell.TH.Syntax.Quote (Data.Singletons.TH.Options.OptionsM m)
-- | This module contains basic functionality for deriving your own
-- singletons via Template Haskell. Note that this module does not define
-- any singled definitions on its own. For a version of this module that
-- comes pre-equipped with several singled definitions based on the
-- Prelude, see Data.Singletons.Base.TH from the
-- singletons-base library.
module Data.Singletons.TH
-- | Make promoted and singled versions of all declarations given,
-- retaining the original declarations. See the README
-- for further explanation.
singletons :: OptionsMonad q => q [Dec] -> q [Dec]
-- | Make promoted and singled versions of all declarations given,
-- discarding the original declarations. Note that a singleton based on a
-- datatype needs the original datatype, so this will fail if it sees any
-- datatype declarations. Classes, instances, and functions are all fine.
singletonsOnly :: OptionsMonad q => q [Dec] -> q [Dec]
-- | Generate singled definitions for each of the provided type-level
-- declaration Names. For example, the singletons-th package
-- itself uses
--
--
-- $(genSingletons [''Bool, ''Maybe, ''Either, ''[]])
--
--
-- to generate singletons for Prelude types.
genSingletons :: OptionsMonad q => [Name] -> q [Dec]
-- | Promote every declaration given to the type level, retaining the
-- originals. See the README for further explanation.
promote :: OptionsMonad q => q [Dec] -> q [Dec]
-- | Promote each declaration, discarding the originals. Note that a
-- promoted datatype uses the same definition as an original datatype, so
-- this will not work with datatypes. Classes, instances, and functions
-- are all fine.
promoteOnly :: OptionsMonad q => q [Dec] -> q [Dec]
-- | Generate defunctionalization symbols for each of the provided
-- type-level declaration Names. See the "Promotion and partial
-- application" section of the singletons README
-- for further explanation.
genDefunSymbols :: OptionsMonad q => [Name] -> q [Dec]
-- | Generate promoted definitions for each of the provided type-level
-- declaration Names. This is generally only useful with classes.
genPromotions :: OptionsMonad q => [Name] -> q [Dec]
-- | Produce instances for PEq from the given types
promoteEqInstances :: OptionsMonad q => [Name] -> q [Dec]
-- | Produce an instance for PEq from the given type
promoteEqInstance :: OptionsMonad q => Name -> q [Dec]
-- | Create instances of SEq for the given types
singEqInstances :: OptionsMonad q => [Name] -> q [Dec]
-- | Create instance of SEq for the given type
singEqInstance :: OptionsMonad q => Name -> q [Dec]
-- | Create instances of SDecide, Eq, TestEquality,
-- and TestCoercion for each type in the list.
singDecideInstances :: OptionsMonad q => [Name] -> q [Dec]
-- | Create instances of SDecide, Eq, TestEquality,
-- and TestCoercion for the given type.
singDecideInstance :: OptionsMonad q => Name -> q [Dec]
-- | Produce instances for POrd from the given types
promoteOrdInstances :: OptionsMonad q => [Name] -> q [Dec]
-- | Produce an instance for POrd from the given type
promoteOrdInstance :: OptionsMonad q => Name -> q [Dec]
-- | Create instances of SOrd for the given types
singOrdInstances :: OptionsMonad q => [Name] -> q [Dec]
-- | Create instance of SOrd for the given type
singOrdInstance :: OptionsMonad q => Name -> q [Dec]
-- | Produce instances for PBounded from the given types
promoteBoundedInstances :: OptionsMonad q => [Name] -> q [Dec]
-- | Produce an instance for PBounded from the given type
promoteBoundedInstance :: OptionsMonad q => Name -> q [Dec]
-- | Create instances of SBounded for the given types
singBoundedInstances :: OptionsMonad q => [Name] -> q [Dec]
-- | Create instance of SBounded for the given type
singBoundedInstance :: OptionsMonad q => Name -> q [Dec]
-- | Produce instances for PEnum from the given types
promoteEnumInstances :: OptionsMonad q => [Name] -> q [Dec]
-- | Produce an instance for PEnum from the given type
promoteEnumInstance :: OptionsMonad q => Name -> q [Dec]
-- | Create instances of SEnum for the given types
singEnumInstances :: OptionsMonad q => [Name] -> q [Dec]
-- | Create instance of SEnum for the given type
singEnumInstance :: OptionsMonad q => Name -> q [Dec]
-- | Produce instances for PShow from the given types
promoteShowInstances :: OptionsMonad q => [Name] -> q [Dec]
-- | Produce an instance for PShow from the given type
promoteShowInstance :: OptionsMonad q => Name -> q [Dec]
-- | Create instances of SShow for the given types
--
-- (Not to be confused with showSingInstances.)
singShowInstances :: OptionsMonad q => [Name] -> q [Dec]
-- | Create instance of SShow for the given type
--
-- (Not to be confused with showShowInstance.)
singShowInstance :: OptionsMonad q => Name -> q [Dec]
-- | Create instances of Show for the given singleton types
--
-- (Not to be confused with singShowInstances.)
showSingInstances :: OptionsMonad q => [Name] -> q [Dec]
-- | Create instance of Show for the given singleton type
--
-- (Not to be confused with singShowInstance.)
showSingInstance :: OptionsMonad q => Name -> q [Dec]
-- | Create an instance for SingI TyCon{N}, where
-- N is the positive number provided as an argument.
--
-- Note that the generated code requires the use of the
-- QuantifiedConstraints language extension.
singITyConInstances :: DsMonad q => [Int] -> q [Dec]
-- | Create an instance for SingI TyCon{N}, where
-- N is the positive number provided as an argument.
--
-- Note that the generated code requires the use of the
-- QuantifiedConstraints language extension.
singITyConInstance :: DsMonad q => Int -> q Dec
cases :: DsMonad q => Name -> q Exp -> q Exp -> q Exp
-- | The function sCases generates a case expression where each
-- right-hand side is identical. This may be useful if the type-checker
-- requires knowledge of which constructor is used to satisfy equality or
-- type-class constraints, but where each constructor is treated the
-- same.
--
-- For sCases, unlike cases, the scrutinee is a singleton.
-- But make sure to pass in the name of the original datatype,
-- preferring ''Maybe over ''SMaybe. In other words,
-- sCases ''Maybe is equivalent to cases
-- ''SMaybe.
sCases :: OptionsMonad q => Name -> q Exp -> q Exp -> q Exp
data family TyCon :: k1 -> k2 -> unmatchable_fun
-- | Proxy is a type that holds no data, but has a phantom parameter
-- of arbitrary type (or even kind). Its use is to provide type
-- information, even though there is no value available of that type (or
-- it may be too costly to create one).
--
-- Historically, Proxy :: Proxy a is a safer
-- alternative to the undefined :: a idiom.
--
--
-- >>> Proxy :: Proxy (Void, Int -> Int)
-- Proxy
--
--
-- Proxy can even hold types of higher kinds,
--
--
-- >>> Proxy :: Proxy Either
-- Proxy
--
--
--
-- >>> Proxy :: Proxy Functor
-- Proxy
--
--
--
-- >>> Proxy :: Proxy complicatedStructure
-- Proxy
--
data Proxy (t :: k)
Proxy :: Proxy (t :: k)
class SingKind k where {
type Demote k = (r :: Type) | r -> k;
}
fromSing :: forall (a :: k). SingKind k => Sing a -> Demote k
toSing :: SingKind k => Demote k -> SomeSing k
class SingI (a :: k)
sing :: SingI a => Sing a
type family Sing :: k -> Type
pattern Sing :: forall k (a :: k). () => SingI a => Sing a
type a ~> b = TyFun a b -> Type
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
type family ApplyTyCon :: k1 -> k2 -> TyFun k1 unmatchable_fun -> Type
data ApplyTyConAux1 (a :: k1 -> k2) (b :: TyFun k1 k2)
class forall (x :: k1). SingI x => SingI f x => SingI1 (f :: k1 -> k2)
liftSing :: forall (x :: k1). SingI1 f => Sing x -> Sing (f x)
class forall (x :: k1) (y :: k2). (SingI x, SingI y) => SingI f x y => SingI2 (f :: k1 -> k2 -> k3)
liftSing2 :: forall (x :: k1) (y :: k2). SingI2 f => Sing x -> Sing y -> Sing (f x y)
type family Demote k = (r :: Type) | r -> k
withSingI :: forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
data SomeSing k
[SomeSing] :: forall k (a :: k). Sing a -> SomeSing k
newtype SLambda (f :: k1 ~> k2)
SLambda :: (forall (t :: k1). () => Sing t -> Sing (f @@ t)) -> SLambda (f :: k1 ~> k2)
[applySing] :: SLambda (f :: k1 ~> k2) -> forall (t :: k1). () => Sing t -> Sing (f @@ t)
type SameKind (a :: k) (b :: k) = ()
demote :: forall {k} (a :: k). (SingKind k, SingI a) => Demote k
type (a :: k1 ~> k2) @@ (b :: k1) = Apply a b
(@@) :: forall k1 k2 (f :: k1 ~> k2) (t :: k1). Sing f -> Sing t -> Sing (f @@ t)
data (a1 :: TyFun a ~> b a ~> b) @@@#@$
data (a1 :: a ~> b) @@@#@$$ (b1 :: TyFun a b)
type (f :: a ~> b) @@@#@$$$ (x :: a) = f @@ x
data (a :: TyFun Type Type ~> Type) ~>@#@$
data a ~>@#@$$ (b :: TyFun Type Type)
type x ~>@#@$$$ y = x ~> y
pattern FromSing :: forall k (a :: k). SingKind k => Sing a -> Demote k
pattern SLambda2 :: forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)). SingFunction2 f -> Sing f
pattern SLambda3 :: forall {a1} {a2} {a3} {b} (f :: a1 ~> (a2 ~> (a3 ~> b))). SingFunction3 f -> Sing f
pattern SLambda4 :: forall {a1} {a2} {a3} {a4} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))). SingFunction4 f -> Sing f
pattern SLambda5 :: forall {a1} {a2} {a3} {a4} {a5} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))). SingFunction5 f -> Sing f
pattern SLambda6 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))). SingFunction6 f -> Sing f
pattern SLambda7 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))). SingFunction7 f -> Sing f
pattern SLambda8 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {a8} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> (a8 ~> b)))))))). SingFunction8 f -> Sing f
applySing2 :: forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)). Sing f -> SingFunction2 f
applySing3 :: forall {a1} {a2} {a3} {b} (f :: a1 ~> (a2 ~> (a3 ~> b))). Sing f -> SingFunction3 f
applySing4 :: forall {a1} {a2} {a3} {a4} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))). Sing f -> SingFunction4 f
applySing5 :: forall {a1} {a2} {a3} {a4} {a5} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))). Sing f -> SingFunction5 f
applySing6 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))). Sing f -> SingFunction6 f
applySing7 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))). Sing f -> SingFunction7 f
applySing8 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {a8} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> (a8 ~> b)))))))). Sing f -> SingFunction8 f
demote1 :: forall {k1} {k2} (f :: k1 -> k2) (x :: k1). (SingKind k2, SingI1 f, SingI x) => Demote k2
demote2 :: forall {k1} {k2} {k3} (f :: k1 -> k2 -> k3) (x :: k1) (y :: k2). (SingKind k3, SingI2 f, SingI x, SingI y) => Demote k3
sing1 :: forall {k1} {k} (f :: k1 -> k) (x :: k1). (SingI1 f, SingI x) => Sing (f x)
sing2 :: forall {k1} {k2} {k} (f :: k1 -> k2 -> k) (x :: k1) (y :: k2). (SingI2 f, SingI x, SingI y) => Sing (f x y)
singByProxy :: forall {k} (a :: k) proxy. SingI a => proxy a -> Sing a
singByProxy# :: forall {k} (a :: k). SingI a => Proxy# a -> Sing a
singByProxy1 :: forall {k1} {k} (f :: k1 -> k) (x :: k1) proxy. (SingI1 f, SingI x) => proxy (f x) -> Sing (f x)
singByProxy1# :: forall {k1} {k} (f :: k1 -> k) (x :: k1). (SingI1 f, SingI x) => Proxy# (f x) -> Sing (f x)
singByProxy2 :: forall {k1} {k2} {k} (f :: k1 -> k2 -> k) (x :: k1) (y :: k2) proxy. (SingI2 f, SingI x, SingI y) => proxy (f x y) -> Sing (f x y)
singByProxy2# :: forall {k1} {k2} {k} (f :: k1 -> k2 -> k) (x :: k1) (y :: k2). (SingI2 f, SingI x, SingI y) => Proxy# (f x y) -> Sing (f x y)
singFun1 :: forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun2 :: forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)). SingFunction2 f -> Sing f
singFun3 :: forall {a1} {a2} {a3} {b} (f :: a1 ~> (a2 ~> (a3 ~> b))). SingFunction3 f -> Sing f
singFun4 :: forall {a1} {a2} {a3} {a4} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))). SingFunction4 f -> Sing f
singFun5 :: forall {a1} {a2} {a3} {a4} {a5} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))). SingFunction5 f -> Sing f
singFun6 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))). SingFunction6 f -> Sing f
singFun7 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))). SingFunction7 f -> Sing f
singFun8 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {a8} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> (a8 ~> b)))))))). SingFunction8 f -> Sing f
singInstance :: forall k (a :: k). Sing a -> SingInstance a
singThat :: forall k (a :: k). (SingKind k, SingI a) => (Demote k -> Bool) -> Maybe (Sing a)
singThat1 :: forall k1 k2 (f :: k1 -> k2) (x :: k1). (SingKind k2, SingI1 f, SingI x) => (Demote k2 -> Bool) -> Maybe (Sing (f x))
singThat2 :: forall k1 k2 k3 (f :: k1 -> k2 -> k3) (x :: k1) (y :: k2). (SingKind k3, SingI2 f, SingI x, SingI y) => (Demote k3 -> Bool) -> Maybe (Sing (f x y))
unSingFun1 :: forall {a1} {b} (f :: a1 ~> b). Sing f -> SingFunction1 f
unSingFun2 :: forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)). Sing f -> SingFunction2 f
unSingFun3 :: forall {a1} {a2} {a3} {b} (f :: a1 ~> (a2 ~> (a3 ~> b))). Sing f -> SingFunction3 f
unSingFun4 :: forall {a1} {a2} {a3} {a4} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))). Sing f -> SingFunction4 f
unSingFun5 :: forall {a1} {a2} {a3} {a4} {a5} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))). Sing f -> SingFunction5 f
unSingFun6 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))). Sing f -> SingFunction6 f
unSingFun7 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))). Sing f -> SingFunction7 f
unSingFun8 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {a8} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> (a8 ~> b)))))))). Sing f -> SingFunction8 f
usingSingI1 :: forall {k1} {k} (f :: k1 -> k) (x :: k1) r. (SingI1 f, SingI x) => (SingI (f x) => r) -> r
usingSingI2 :: forall {k1} {k2} {k} (f :: k1 -> k2 -> k) (x :: k1) (y :: k2) r. (SingI2 f, SingI x, SingI y) => (SingI (f x y) => r) -> r
withSing :: forall {k} (a :: k) b. SingI a => (Sing a -> b) -> b
withSing1 :: forall {k1} {k} (f :: k1 -> k) (x :: k1) b. (SingI1 f, SingI x) => (Sing (f x) -> b) -> b
withSing2 :: forall {k1} {k2} {k} (f :: k1 -> k2 -> k) (x :: k1) (y :: k2) b. (SingI2 f, SingI x, SingI y) => (Sing (f x y) -> b) -> b
withSomeSing :: SingKind k => Demote k -> (forall (a :: k). () => Sing a -> r) -> r
data ApplySym0 (a1 :: TyFun a ~> b a ~> b)
data ApplySym1 (a1 :: a ~> b) (b1 :: TyFun a b)
type ApplySym2 (f :: a ~> b) (x :: a) = Apply f x
data ApplyTyConAux2 (a :: k1 -> k2 -> k3) (b :: TyFun k1 unmatchable_fun)
data DemoteSym0 (a :: TyFun Type Type)
type DemoteSym1 x = Demote x
type KindOf (a :: k) = k
data KindOfSym0 (a :: TyFun k Type)
type KindOfSym1 (x :: k) = KindOf x
newtype SWrappedSing (a1 :: WrappedSing a)
[SWrapSing] :: forall k (a :: k) (a1 :: WrappedSing a). Sing a -> SWrappedSing a1
data SameKindSym0 (a :: TyFun k k ~> Constraint)
data SameKindSym1 (a :: k) (b :: TyFun k Constraint)
type SameKindSym2 (x :: k) (y :: k) = SameKind x y
type SingFunction1 (f :: a1 ~> b) = forall (t :: a1). () => Sing t -> Sing f @@ t
type SingFunction2 (f :: a1 ~> a2 ~> b) = forall (t1 :: a1) (t2 :: a2). () => Sing t1 -> Sing t2 -> Sing f @@ t1 @@ t2
type SingFunction3 (f :: a1 ~> a2 ~> a3 ~> b) = forall (t1 :: a1) (t2 :: a2) (t3 :: a3). () => Sing t1 -> Sing t2 -> Sing t3 -> Sing f @@ t1 @@ t2 @@ t3
type SingFunction4 (f :: a1 ~> a2 ~> a3 ~> a4 ~> b) = forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4). () => Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing f @@ t1 @@ t2 @@ t3 @@ t4
type SingFunction5 (f :: a1 ~> a2 ~> a3 ~> a4 ~> a5 ~> b) = forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4) (t5 :: a5). () => Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing f @@ t1 @@ t2 @@ t3 @@ t4 @@ t5
type SingFunction6 (f :: a1 ~> a2 ~> a3 ~> a4 ~> a5 ~> a6 ~> b) = forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4) (t5 :: a5) (t6 :: a6). () => Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing t6 -> Sing f @@ t1 @@ t2 @@ t3 @@ t4 @@ t5 @@ t6
type SingFunction7 (f :: a1 ~> a2 ~> a3 ~> a4 ~> a5 ~> a6 ~> a7 ~> b) = forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4) (t5 :: a5) (t6 :: a6) (t7 :: a7). () => Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing t6 -> Sing t7 -> Sing f @@ t1 @@ t2 @@ t3 @@ t4 @@ t5 @@ t6 @@ t7
type SingFunction8 (f :: a1 ~> a2 ~> a3 ~> a4 ~> a5 ~> a6 ~> a7 ~> a8 ~> b) = forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4) (t5 :: a5) (t6 :: a6) (t7 :: a7) (t8 :: a8). () => Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing t6 -> Sing t7 -> Sing t8 -> Sing f @@ t1 @@ t2 @@ t3 @@ t4 @@ t5 @@ t6 @@ t7 @@ t8
data SingInstance (a :: k)
[SingInstance] :: forall {k} (a :: k). SingI a => SingInstance a
type TyCon1 = TyCon :: k1 -> k2 -> k1 ~> k2
type TyCon2 = TyCon :: k1 -> k2 -> k3 -> k1 ~> k2 ~> k3
type TyCon3 = TyCon :: k1 -> k2 -> k3 -> k4 -> k1 ~> k2 ~> k3 ~> k4
type TyCon4 = TyCon :: k1 -> k2 -> k3 -> k4 -> k5 -> k1 ~> k2 ~> k3 ~> k4 ~> k5
type TyCon5 = TyCon :: k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6
type TyCon6 = TyCon :: k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7
type TyCon7 = TyCon :: k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7 ~> k8
type TyCon8 = TyCon :: k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> k9 -> k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7 ~> k8 ~> k9
data TyFun a b
type family UnwrapSing (ws :: WrappedSing a) :: Sing a
newtype WrappedSing (a :: k)
[WrapSing] :: forall k (a :: k). Sing a -> WrappedSing a
class SDecide k
(%~) :: forall (a :: k) (b :: k). SDecide k => Sing a -> Sing b -> Decision (a :~: b)
-- | Propositional equality. If a :~: b is inhabited by some
-- terminating value, then the type a is the same as the type
-- b. To use this equality in practice, pattern-match on the
-- a :~: b to get out the Refl constructor; in the body
-- of the pattern-match, the compiler knows that a ~ b.
data (a :: k) :~: (b :: k)
[Refl] :: forall {k} (a :: k). a :~: a
infix 4 :~:
-- | Uninhabited data type
data Void
type Refuted a = a -> Void
data Decision a
Proved :: a -> Decision a
Disproved :: Refuted a -> Decision a
-- | This class (which users should never see) is to be instantiated in
-- order to use an otherwise-unused data constructor, such as the
-- "kind-inference" data constructor for defunctionalization symbols.
class SuppressUnusedWarnings (t :: k)
suppressUnusedWarnings :: SuppressUnusedWarnings t => ()
-- | This file implements singletonStar, which generates a datatype
-- Rep and associated singleton from a list of types. The
-- promoted version of Rep is kind * and the Haskell
-- types themselves. This is still very experimental, so expect unusual
-- results!
--
-- See also Data.Singletons.Base.CustomStar from
-- singletons-base, a variant of this module that also
-- re-exports related definitions from Prelude.Singletons.
module Data.Singletons.TH.CustomStar
-- | Produce a representation and singleton for the collection of types
-- given.
--
-- A datatype Rep is created, with one constructor per type in
-- the declared universe. When this type is promoted by the
-- singletons-th library, the constructors become full types in
-- *, not just promoted data constructors.
--
-- For example,
--
--
-- $(singletonStar [''Nat, ''Bool, ''Maybe])
--
--
-- generates the following:
--
--
-- data Rep = Nat | Bool | Maybe Rep deriving (Eq, Ord, Read, Show)
--
--
-- and its singleton. However, because Rep is promoted to
-- *, the singleton is perhaps slightly unexpected:
--
--
-- data SRep (a :: *) where
-- SNat :: Sing Nat
-- SBool :: Sing Bool
-- SMaybe :: Sing a -> Sing (Maybe a)
-- type instance Sing = SRep
--
--
-- The unexpected part is that Nat, Bool, and
-- Maybe above are the real Nat, Bool, and
-- Maybe, not just promoted data constructors.
--
-- Please note that this function is very experimental. Use at
-- your own risk.
singletonStar :: OptionsMonad q => [Name] -> q [Dec]