The singleton kind-indexed type family.

An infix synonym for applySing

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

A version of the SingI class lifted to unary type constructors.

Produce a singleton explicitly using implicit SingI1 and SingI constraints. You will likely need the ScopedTypeVariables extension to use this method the way you want.

A version of the SingI class lifted to binary type constructors.

Produce a singleton explicitly using implicit SingI2 and SingI constraints. You will likely need the ScopedTypeVariables extension to use this method the way you want.

The SingKind class is 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.

For a SingKind instance to be well behaved, it should obey the following laws:

toSing . fromSing ≡ SomeSing
(\x -> withSomeSing x fromSing) ≡ id

The final law can also be expressed in terms of the FromSing pattern synonym:

(\(FromSing sing) -> FromSing sing) ≡ id

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

Force GHC to unify the kinds of a and b. Note that SameKind a b is different from KindOf a ~ KindOf b in that the former makes the kinds unify immediately, whereas the latter is a proposition that GHC considers as possibly false.

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.

An explicitly bidirectional pattern synonym for implicit singletons.

As an expression: Constructs a singleton Sing a given a implicit singleton constraint SingI a.

As a pattern: Matches on an explicit Sing a witness bringing an implicit SingI a constraint into scope.

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.

An explicitly bidirectional pattern synonym for going between a singleton and the corresponding demoted term.

As an expression: this takes a singleton to its demoted (base) type.

>>> :t FromSing \@Bool
FromSing \@Bool :: Sing a -> Bool
>>> FromSing SFalse
False

As a pattern: It extracts a singleton from its demoted (base) type.

singAnd :: Bool -> Bool -> SomeSing Bool
singAnd (FromSing singBool1) (FromSing singBool2) =
  SomeSing (singBool1 %&& singBool2)

instead of writing it with withSomeSing:

singAnd bool1 bool2 =
  withSomeSing bool1 $ singBool1 ->
    withSomeSing bool2 $ singBool2 ->
      SomeSing (singBool1 %&& singBool2)

Convert a group of SingI1 and SingI constraints (representing a function to apply and its argument, respectively) into a single SingI constraint representing the application. You will likely need the ScopedTypeVariables extension to use this method the way you want.

Convert a group of SingI2 and SingI constraints (representing a function to apply and its arguments, respectively) into a single SingI constraint representing the application. You will likely need the ScopedTypeVariables extension to use this method the way you want.

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

Allows creation of a singleton for a unary type constructor when a proxy is at hand.

Allows creation of a singleton for a binary type constructor when a proxy is at hand.

A convenience function that takes a type as input and demotes it to its value-level counterpart as output. This uses SingKind and SingI behind the scenes, so demote = fromSing sing.

This function is intended to be used with TypeApplications. For example:

>>> demote @True
True

>>> demote @(Nothing :: Maybe Ordering)
Nothing

>>> demote @(Just EQ)
Just EQ

>>> demote @'(True,EQ)
(True,EQ)

A convenience function that takes a unary type constructor and its argument as input, applies them, and demotes the result to its value-level counterpart as output. This uses SingKind, SingI1, and SingI behind the scenes, so demote1 = fromSing sing1.

This function is intended to be used with TypeApplications. For example:

>>> demote1 @Just @EQ
Just EQ

>>> demote1 @('(,) True) @EQ
(True,EQ)

A convenience function that takes a binary type constructor and its arguments as input, applies them, and demotes the result to its value-level counterpart as output. This uses SingKind, SingI2, and SingI behind the scenes, so demote2 = fromSing sing2.

This function is intended to be used with TypeApplications. For example:

>>> demote2 @'(,) @True @EQ
(True,EQ)

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

Allows creation of a singleton for a unary type constructor when a proxy# is at hand.

Allows creation of a singleton for a binary type constructor 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 useful when we need to name a singleton value for a unary type constructor multiple times. Without this function, each use of sing1 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 useful when we need to name a singleton value for a binary type constructor multiple times. Without this function, each use of sing1 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.

A convenience function that names a singleton for a unary type constructor 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.

A convenience function that names a singleton for a binary type constructor 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.

A newtype around Sing.

Since Sing is a type family, it cannot be used directly in type class instances. As one example, one cannot write a catch-all instance SDecide k => TestEquality (Sing k). On the other hand, WrappedSing is a perfectly ordinary data type, which means that it is quite possible to define an instance SDecide k => TestEquality (WrappedSing k).

The singleton for WrappedSings. Informally, this is the singleton type for other singletons.

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.

Something of kind a ~> b is a defunctionalized type function that is not necessarily generative or injective. Defunctionalized type functions (also called "defunctionalization symbols") can be partially applied, even if the original type function cannot be. For more information on how this works, see the "Promotion and partial application" section of the README.

Normal type-level arrows (->) can be converted into defunctionalization arrows (~>) by the use of the TyCon family of types. (Refer to the Haddocks for TyCon1 to see an example of this in practice.) For this reason, we do not make an effort to define defunctionalization symbols for most type constructors of kind a -> b, as they can be used in defunctionalized settings by simply applying TyCon{N} with an appropriate N.

This includes the (->) type constructor itself, which is of kind Type -> Type -> Type. One can turn it into something of kind Type ~> Type ~> Type by writing TyCon2 (->), or something of kind Type -> Type ~> Type by writing TyCon1 ((->) t) (where t :: Type).

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

data Nat = Zero | Succ Nat
type family Map (a :: 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

An infix synonym for Apply

Workhorse for the TyCon1, etc., types. This can be used directly in place of any of the TyConN types, but it will work only with monomorphic types. When GHC#14645 is fixed, this should fully supersede the TyConN types.

Note that this is only defined on GHC 8.6 or later. Prior to GHC 8.6, TyCon1 et al. were defined as separate data types.

An "internal" definition used primary in the Apply instance for TyCon.

Note that this only defined on GHC 8.6 or later.

An "internal" defunctionalization symbol used primarily in the definition of ApplyTyCon, as well as the SingI instances for TyCon1, TyCon2, etc.

Note that this is only defined on GHC 8.6 or later.

An "internal" defunctionalization symbol used primarily in the definition of ApplyTyCon.

Note that this is only defined on GHC 8.6 or later.

Use this function when passing a function on singletons as a higher-order function. You will need visible type application to get this to work. For example:

falses = sMap (singFun1 @NotSym0 sNot)
              (STrue `SCons` STrue `SCons` SNil)

There are a family of singFun... functions, keyed by the number of parameters of the function.

This is the inverse of singFun1, and likewise for the other unSingFun... functions.

Proxy is a type that holds no data, but has a phantom parameter of arbitrary type (or even kind). Its use is to provide type information, even though there is no value available of that type (or it may be too costly to create one).

Historically, Proxy :: Proxy a is a safer alternative to the undefined :: a idiom.

>>> Proxy :: Proxy (Void, Int -> Int)
Proxy

Proxy can even hold types of higher kinds,

>>> Proxy :: Proxy Either
Proxy

>>> Proxy :: Proxy Functor
Proxy

>>> Proxy :: Proxy complicatedStructure
Proxy