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.

Representation of the kind of a type-level function. The difference between term-level arrows and this type-level arrow is that at the term level applications can be unsaturated, whereas at the type level all applications have to be fully saturated.

Wrapper for converting the normal type-level arrow into a TyFun. For example, given:

data Nat = Zero | Succ Nat
type family Map (a :: TyFun a b -> *) (a :: [a]) :: [b]
  Map f '[] = '[]
  Map f (x ': xs) = Apply f x ': Map f xs

We can write:

Map (TyCon1 Succ) [Zero, Succ Zero]

Similar to TyCon1, but for two-parameter type constructors.

Type level function application