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.

Generate defunctionalization symbols for existing type family

Generate promoted definitions from a type that is already defined. This is generally only useful with classes.

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.

Produce instances for Compare from the given types

Produce an instance for Compare from the given type

Produce instances for MinBound and MaxBound from the given types

Produce an instance for MinBound and MaxBound from the given type

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.

The promoted analogue of Eq. If you supply no definition for '(:==)' under GHC 7.8+, then it defaults to a use of '(==)', from Data.Type.Equality.

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, poly-kinded proxy type

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.

The promotion of error

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.