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

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

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.

Create instance of SDecide for the given type.

Produce instances for POrd from the given types

Produce an instance for POrd from the given type

Create instances of SOrd for the given types

Create instance of SOrd for the given type

Produce instances for PBounded from the given types

Produce an instance for PBounded from the given type

Create instances of SBounded for the given types

Create instance of SBounded for the given type

Produce instances for PEnum from the given types

Produce an instance for PEnum from the given type

Create instances of SEnum for the given types

Create instance of SEnum for 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 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.

The singleton kind-indexed data family.

The promoted analogue of Eq. If you supply no definition for '(:==)', 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 *))

Above, we print kinds explicitly, as if with -fprint-explicit-kinds.

Note that Any is kind polymorphic; its kind is thus forall 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

Uninhabited data type

Since: 4.8.0.0

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 version is more poly-kinded for easier use.

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.