Data.Singletons.TH

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.

Primary Template Haskell generation functions

singletons :: OptionsMonad q => q [Dec] -> q [Dec]

Make promoted and singled versions of all declarations given, retaining the original declarations. See the README for further explanation.

singletonsOnly :: 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.

genSingletons :: OptionsMonad q => [Name] -> 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.

promote :: OptionsMonad q => q [Dec] -> q [Dec]

Promote every declaration given to the type level, retaining the originals. See the README for further explanation.

promoteOnly :: 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.

genDefunSymbols :: OptionsMonad q => [Name] -> 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.

genPromotions :: OptionsMonad q => [Name] -> q [Dec]

Generate promoted definitions for each of the provided type-level declaration Names. This is generally only useful with classes.

Functions to generate equality instances

promoteEqInstances :: OptionsMonad q => [Name] -> q [Dec]

Produce instances for PEq from the given types

promoteEqInstance :: OptionsMonad q => Name -> q [Dec]

Produce an instance for PEq from the given type

singEqInstances :: OptionsMonad q => [Name] -> q [Dec]

Create instances of SEq for the given types

singEqInstance :: OptionsMonad q => Name -> q [Dec]

Create instance of SEq for the given type

singDecideInstances :: OptionsMonad q => [Name] -> q [Dec]

Create instances of SDecide, TestEquality, and TestCoercion for each type in the list.

singDecideInstance :: OptionsMonad q => Name -> q [Dec]

Create instances of SDecide, TestEquality, and TestCoercion for the given type.

Functions to generate Ord instances

promoteOrdInstances :: OptionsMonad q => [Name] -> q [Dec]

Produce instances for POrd from the given types

promoteOrdInstance :: OptionsMonad q => Name -> q [Dec]

Produce an instance for POrd from the given type

singOrdInstances :: OptionsMonad q => [Name] -> q [Dec]

Create instances of SOrd for the given types

singOrdInstance :: OptionsMonad q => Name -> q [Dec]

Create instance of SOrd for the given type

Functions to generate Bounded instances

promoteBoundedInstances :: OptionsMonad q => [Name] -> q [Dec]

Produce instances for PBounded from the given types

promoteBoundedInstance :: OptionsMonad q => Name -> q [Dec]

Produce an instance for PBounded from the given type

singBoundedInstances :: OptionsMonad q => [Name] -> q [Dec]

Create instances of SBounded for the given types

singBoundedInstance :: OptionsMonad q => Name -> q [Dec]

Create instance of SBounded for the given type

Functions to generate Enum instances

promoteEnumInstances :: OptionsMonad q => [Name] -> q [Dec]

Produce instances for PEnum from the given types

promoteEnumInstance :: OptionsMonad q => Name -> q [Dec]

Produce an instance for PEnum from the given type

singEnumInstances :: OptionsMonad q => [Name] -> q [Dec]

Create instances of SEnum for the given types

singEnumInstance :: OptionsMonad q => Name -> q [Dec]

Create instance of SEnum for the given type

Functions to generate Show instances

promoteShowInstances :: OptionsMonad q => [Name] -> q [Dec]

Produce instances for PShow from the given types

promoteShowInstance :: OptionsMonad q => Name -> q [Dec]

Produce an instance for PShow from the given type

singShowInstances :: OptionsMonad q => [Name] -> q [Dec]

Create instances of SShow for the given types

(Not to be confused with showSingInstances.)

singShowInstance :: OptionsMonad q => Name -> q [Dec]

Create instance of SShow for the given type

(Not to be confused with showShowInstance.)

showSingInstances :: OptionsMonad q => [Name] -> q [Dec]

Create instances of Show for the given singleton types

(Not to be confused with singShowInstances.)

showSingInstance :: OptionsMonad q => Name -> q [Dec]

Create instance of Show for the given singleton type

(Not to be confused with singShowInstance.)

Utility functions

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

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.

cases

Arguments

:: DsMonad q

=> Name

The head of the type of the scrutinee. (Like ''Maybe or ''Bool.)

-> q Exp

The scrutinee, in a Template Haskell quote

-> q Exp

The body, in a Template Haskell quote

-> q Exp

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.

sCases

Arguments

:: OptionsMonad q

=> Name

The head of the type the scrutinee's type is based on. (Like ''Maybe or ''Bool.)

-> q Exp

The scrutinee, in a Template Haskell quote

-> q Exp

The body, in a Template Haskell quote

-> 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.

Basic singleton definitions

Auxiliary definitions

class SDecide k where

Methods

(%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)

data (a :: k) :~: (b :: k) where 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.

Since: base-4.7.0.0

Constructors

Refl :: forall {k} (a :: k). a :~: a

Instances

Category ((:~:) :: k -> k -> Type)

Since: base-4.7.0.0

Defined in Control.Category

Methods

id :: forall (a :: k0). a :~: a

(.) :: forall (b :: k0) (c :: k0) (a :: k0). (b :~: c) -> (a :~: b) -> a :~: c

TestCoercion ((:~:) a :: k -> Type)

Since: base-4.7.0.0

Defined in Data.Type.Coercion

Methods

testCoercion :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b)

TestEquality ((:~:) a :: k -> Type)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

testEquality :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b)

NFData2 ((:~:) :: Type -> Type -> Type)

Since: deepseq-1.4.3.0

Defined in Control.DeepSeq

Methods

liftRnf2 :: (a -> ()) -> (b -> ()) -> (a :~: b) -> ()

NFData1 ((:~:) a)

Since: deepseq-1.4.3.0

Defined in Control.DeepSeq

Methods

liftRnf :: (a0 -> ()) -> (a :~: a0) -> ()

(a ~ b, Data a) => Data (a :~: b)

Since: base-4.7.0.0

Defined in Data.Data

Methods

gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~: b) -> c (a :~: b)

gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b)

toConstr :: (a :~: b) -> Constr

dataTypeOf :: (a :~: b) -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b))

gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r

gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b)

a ~ b => Bounded (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

minBound :: a :~: b

maxBound :: a :~: b

a ~ b => Enum (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

succ :: (a :~: b) -> a :~: b

pred :: (a :~: b) -> a :~: b

toEnum :: Int -> a :~: b

fromEnum :: (a :~: b) -> Int

enumFrom :: (a :~: b) -> [a :~: b]

enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b]

enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b]

enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b]

a ~ b => Read (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

readsPrec :: Int -> ReadS (a :~: b)

readList :: ReadS [a :~: b]

readPrec :: ReadPrec (a :~: b)

readListPrec :: ReadPrec [a :~: b]

Show (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

showsPrec :: Int -> (a :~: b) -> ShowS

show :: (a :~: b) -> String

showList :: [a :~: b] -> ShowS

NFData (a :~: b)

Since: deepseq-1.4.3.0

Defined in Control.DeepSeq

Methods

rnf :: (a :~: b) -> ()

Eq (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

(==) :: (a :~: b) -> (a :~: b) -> Bool

(/=) :: (a :~: b) -> (a :~: b) -> Bool

Ord (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

compare :: (a :~: b) -> (a :~: b) -> Ordering

(<) :: (a :~: b) -> (a :~: b) -> Bool

(<=) :: (a :~: b) -> (a :~: b) -> Bool

(>) :: (a :~: b) -> (a :~: b) -> Bool

(>=) :: (a :~: b) -> (a :~: b) -> Bool

max :: (a :~: b) -> (a :~: b) -> a :~: b

min :: (a :~: b) -> (a :~: b) -> a :~: b

data Void

Uninhabited data type

Since: base-4.8.0.0

Instances

Data Void

Since: base-4.8.0.0

Defined in Data.Void

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Void -> c Void

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Void

toConstr :: Void -> Constr

dataTypeOf :: Void -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Void)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Void)

gmapT :: (forall b. Data b => b -> b) -> Void -> Void

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Void -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Void -> r

gmapQ :: (forall d. Data d => d -> u) -> Void -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Void -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Void -> m Void

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Void -> m Void

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Void -> m Void

Semigroup Void

Since: base-4.9.0.0

Defined in Data.Void

Methods

(<>) :: Void -> Void -> Void

sconcat :: NonEmpty Void -> Void

stimes :: Integral b => b -> Void -> Void

Exception Void

Since: base-4.8.0.0

Defined in Data.Void

Methods

toException :: Void -> SomeException

fromException :: SomeException -> Maybe Void

displayException :: Void -> String

Generic Void

Defined in Data.Void

Associated Types

type Rep Void :: Type -> Type

Methods

from :: Void -> Rep Void x

to :: Rep Void x -> Void

Ix Void

Since: base-4.8.0.0

Defined in Data.Void

Methods

range :: (Void, Void) -> [Void]

index :: (Void, Void) -> Void -> Int

unsafeIndex :: (Void, Void) -> Void -> Int

inRange :: (Void, Void) -> Void -> Bool

rangeSize :: (Void, Void) -> Int

unsafeRangeSize :: (Void, Void) -> Int

Read Void

Reading a Void value is always a parse error, considering Void as a data type with no constructors.

Since: base-4.8.0.0

Defined in Data.Void

Methods

readsPrec :: Int -> ReadS Void

readList :: ReadS [Void]

readPrec :: ReadPrec Void

readListPrec :: ReadPrec [Void]

Show Void

Since: base-4.8.0.0

Defined in Data.Void

Methods

showsPrec :: Int -> Void -> ShowS

show :: Void -> String

showList :: [Void] -> ShowS

NFData Void

Defined as rnf = absurd.

Since: deepseq-1.4.0.0

Defined in Control.DeepSeq

Methods

rnf :: Void -> ()

Eq Void

Since: base-4.8.0.0

Defined in Data.Void

Methods

(==) :: Void -> Void -> Bool

(/=) :: Void -> Void -> Bool

Ord Void

Since: base-4.8.0.0

Defined in Data.Void

Methods

compare :: Void -> Void -> Ordering

(<) :: Void -> Void -> Bool

(<=) :: Void -> Void -> Bool

(>) :: Void -> Void -> Bool

(>=) :: Void -> Void -> Bool

max :: Void -> Void -> Void

min :: Void -> Void -> Void

Lift Void

Since: template-haskell-2.15.0.0

Defined in Language.Haskell.TH.Syntax

Methods

lift :: Quote m => Void -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => Void -> Code m Void

type Rep Void

Since: base-4.8.0.0

Defined in Data.Void

type Rep Void = D1 ('MetaData "Void" "Data.Void" "base" 'False) (V1 :: Type -> Type)

type Refuted a = a -> Void

data Decision a

Constructors

Proved a

Disproved (Refuted a)

class SuppressUnusedWarnings (t :: k) where

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.

Methods

suppressUnusedWarnings :: ()