Make promoted and singleton versions of all declarations given, retaining the original declarations. See http://www.cis.upenn.edu/~eir/packages/singletons/README.html for further explanation.

Make promoted and singleton versions of all declarations given, discarding the original declarations.

Generate singleton definitions from a type that is already defined. For example, the singletons package itself uses

$(genSingletons [''Bool, ''Maybe, ''Either, ''[]])

to generate singletons for Prelude types.

Promote every declaration given to the type level, retaining the originals.

Promote each declaration, discarding the originals.

Produce instances for '(:==)' (type-level equality) from the given types

Produce an instance for '(:==)' (type-level equality) from the given type

Create instances of SEq and type-level '(:==)' for each type in the list

Create instance of SEq and type-level '(:==)' for the given type

Create instances of SEq (only -- no instance for '(:==)', which SEq generally relies on) for each type in the list

Create instances of SEq (only -- no instance for '(:==)', which SEq generally relies on) for the given type

Create instances of SDecide for each type in the list.

Note that, due to a bug in GHC 7.6.3 (and lower) optimizing instances for SDecide can make GHC hang. You may want to put {-# OPTIONS_GHC -O0 #-} in your file.

Create instance of SDecide for the given type.

Note that, due to a bug in GHC 7.6.3 (and lower) optimizing instances for SDecide can make GHC hang. You may want to put {-# OPTIONS_GHC -O0 #-} in your file.

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.

The singleton kind-indexed data family.

A SingI constraint is essentially an implicitly-passed singleton. If you need to satisfy this constraint with an explicit singleton, please see withSingI.

The SingKind class is essentially a kind class. It classifies all kinds for which singletons are defined. The class supports converting between a singleton type and the base (unrefined) type which it is built from.

Convenient synonym to refer to the kind of a type variable: type KindOf (a :: k) = ('KProxy :: KProxy k)

Convenient abbreviation for DemoteRep: type Demote (a :: k) = DemoteRep ('KProxy :: KProxy k)

A type family to compute Boolean equality. Instances are provided only for open kinds, such as * and function kinds. Instances are also provided for datatypes exported from base. A poly-kinded instance is not provided, as a recursive definition for algebraic kinds is generally more useful.

A re-export of the type-level (==) that conforms to the singletons naming convention.

Type-level If. If True a b ==> a; If False a b ==> b

Conditional over singletons

The singleton analogue of Eq. Unlike the definition for Eq, it is required that instances define a body for '(%:==)'. You may also supply a body for '(%:/=)'.

The type constructor Any is type to which you can unsafely coerce any lifted type, and back.

• It is lifted, and hence represented by a pointer
• It does not claim to be a data type, and that's important for the code generator, because the code gen may enter a data value but never enters a function value.

It's also used to instantiate un-constrained type variables after type checking. For example, length has type

length :: forall a. [a] -> Int

and the list datacon for the empty list has type

[] :: forall a. [a]

In order to compose these two terms as length [] a type application is required, but there is no constraint on the choice. In this situation GHC uses Any:

length (Any *) ([] (Any *))

Note that Any is kind polymorphic, and takes a kind k as its first argument. The kind of Any is thus forall k. k -> k.

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.

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: 4.7.0.0

A logically uninhabited data type.

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

A Decision about a type a is either a proof of existence or a proof that a cannot exist.

A concrete, promotable proxy type, for use at the kind level There are no instances for this because it is intended at the kind level only

An existentially-quantified singleton. This type is useful when you want a singleton type, but there is no way of knowing, at compile-time, what the type index will be. To make use of this type, you will generally have to use a pattern-match:

foo :: Bool -> ...
foo b = case toSing b of
          SomeSing sb -> {- fancy dependently-typed code with sb -}

An example like the one above may be easier to write using withSomeSing.