-- 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://cs.brynmawr.edu/~rae/papers/2012/singletons/paper.pdf)
-- See also the paper published at Haskell Symposium, 2014, which
-- describes how promotion works in greater detail:
-- https://cs.brynmawr.edu/~rae/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.0). 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.0
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
getOptions :: OptionsMonad m => m Options
-- | A convenient implementation of the OptionsMonad class. Use by
-- calling withOptions.
data OptionsM m a
-- | Declare the Options that a TH computation should use.
withOptions :: Options -> OptionsM m a -> m a
instance Language.Haskell.TH.Desugar.Reify.DsMonad m => Language.Haskell.TH.Desugar.Reify.DsMonad (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 Control.Monad.Fail.MonadFail m => Control.Monad.Fail.MonadFail (Data.Singletons.TH.Options.OptionsM 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)
instance Control.Monad.Trans.Class.MonadTrans Data.Singletons.TH.Options.OptionsM
instance GHC.Base.Monad m => GHC.Base.Monad (Data.Singletons.TH.Options.OptionsM m)
instance GHC.Base.Applicative m => GHC.Base.Applicative (Data.Singletons.TH.Options.OptionsM m)
instance GHC.Base.Functor m => GHC.Base.Functor (Data.Singletons.TH.Options.OptionsM 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 m => Data.Singletons.TH.Options.OptionsMonad (Language.Haskell.TH.Desugar.Reify.DsM m)
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 => 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 (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)
-- | 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, TestEquality, and
-- TestCoercion for each type in the list.
singDecideInstances :: OptionsMonad q => [Name] -> q [Dec]
-- | Create instances of SDecide, 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
-- | The function cases 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.
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.
sCases :: OptionsMonad q => Name -> q Exp -> q Exp -> q Exp
-- | Members of the SDecide "kind" class support decidable equality.
-- Instances of this class are generated alongside singleton definitions
-- for datatypes that derive an Eq instance.
class SDecide k
-- | Compute a proof or disproof of equality, given two singletons.
(%~) :: forall (a :: k) (b :: k). SDecide k => Sing a -> Sing b -> Decision (a :~: b)
infix 4 %~
-- | 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
-- | Because we can never create a value of type Void, a function
-- that type-checks at a -> Void shows that objects of type
-- a can never exist. Thus, we say that a is
-- Refuted
type Refuted a = a -> Void
-- | A Decision about a type a is either a proof of
-- existence or a proof that a cannot exist.
data Decision a
-- | Witness for a
Proved :: a -> Decision a
-- | Proof that no a exists
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]