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 SingInstance wraps up a SingI instance for explicit handling.

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.

Get an implicit singleton (a SingI instance) from an explicit one.

Convenience function for creating a context with an implicit singleton available.

Convert a normal datatype (like Bool) to a singleton for that datatype, passing it into a continuation.

Allows creation of a singleton when a proxy is at hand.

Allows creation of a singleton when a proxy# is at hand.

A convenience function useful when we need to name a singleton value multiple times. Without this function, each use of sing could potentially refer to a different singleton, and one has to use type signatures (often with ScopedTypeVariables) to ensure that they are the same.

A convenience function that names a singleton satisfying a certain property. If the singleton does not satisfy the property, then the function returns Nothing. The property is expressed in terms of the underlying representation of the singleton.

GHC 7.8 sometimes warns about incomplete pattern matches when no such patterns are possible, due to GADT constraints. See the bug report at https://ghc.haskell.org/trac/ghc/ticket/3927. In such cases, it's useful to have a catch-all pattern that then has bugInGHC as its right-hand side.

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

A concrete, poly-kinded proxy type