Data.Singletons.TH

This module contains everything you need to derive your own singletons via Template Haskell.

TURN ON -XScopedTypeVariables IN YOUR MODULE IF YOU WANT THIS TO WORK.

Primary Template Haskell generation functions

singletons :: Quasi q => q [Dec] -> q [Dec]

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.

singletonsOnly :: Quasi q => q [Dec] -> q [Dec]

Make promoted and singleton versions of all declarations given, discarding the original declarations.

genSingletons :: Quasi q => [Name] -> q [Dec]

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 :: Quasi q => q [Dec] -> q [Dec]

Promote every declaration given to the type level, retaining the originals.

promoteOnly :: Quasi q => q [Dec] -> q [Dec]

Promote each declaration, discarding the originals.

Functions to generate equality instances

promoteEqInstances :: Quasi q => [Name] -> q [Dec]

Produce instances for '(:==)' (type-level equality) from the given types

promoteEqInstance :: Quasi q => Name -> q [Dec]

Produce an instance for '(:==)' (type-level equality) from the given type

singEqInstances :: Quasi q => [Name] -> q [Dec]

Create instances of SEq and type-level '(:==)' for each type in the list

singEqInstance :: Quasi q => Name -> q [Dec]

Create instance of SEq and type-level '(:==)' for the given type

singEqInstancesOnly :: Quasi q => [Name] -> q [Dec]

Create instances of SEq (only -- no instance for '(:==)', which SEq generally relies on) for each type in the list

singEqInstanceOnly :: Quasi q => Name -> q [Dec]

Create instances of SEq (only -- no instance for '(:==)', which SEq generally relies on) for the given type

singDecideInstances :: Quasi q => [Name] -> q [Dec]

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.

singDecideInstance :: Quasi q => Name -> q [Dec]

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.

Utility function

cases

Arguments

:: Quasi q

=> Name

The head of the type of the scrutinee. (Like ''Maybe or ''Bool.)

-> q Exp

The scrutinee, in a Template Haskell quote

-> q Exp

The body, in a Template Haskell quote

-> q Exp

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.

Basic singleton definitions

data family Sing a

The singleton kind-indexed data family.

Instances

TestCoercion * (Sing *)

SDecide k (KProxy k) => TestEquality k (Sing k)

data Sing Bool where

• SFalse :: (~) Bool z False => Sing Bool z
• STrue :: (~) Bool z True => Sing Bool z

data Sing Ordering where

• SLT :: (~) Ordering z LT => Sing Ordering z
• SEQ :: (~) Ordering z EQ => Sing Ordering z
• SGT :: (~) Ordering z GT => Sing Ordering z

data Sing * where

• STypeRep :: Typeable * a => Sing * a

data Sing Nat where

• SNat :: KnownNat n => Sing Nat n

data Sing Symbol where

• SSym :: KnownSymbol n => Sing Symbol n

data Sing () where

• STuple0 :: (~) () z () => Sing () z

data Sing [a0] where

• SNil :: (~) [a] z ([] a) => Sing [a] z
• SCons :: (~) [a] z ((:) a n n) => Sing a n -> Sing [a] n -> Sing [a] z

data Sing (Maybe a0) where

• SNothing :: (~) (Maybe a) z (Nothing a) => Sing (Maybe a) z
• SJust :: (~) (Maybe a) z (Just a n) => Sing a n -> Sing (Maybe a) z

data Sing (Either a0 b0) where

• SLeft :: (~) (Either a b) z (Left a b n) => Sing a n -> Sing (Either a b) z
• SRight :: (~) (Either a b) z (Right a b n) => Sing b n -> Sing (Either a b) z

data Sing ((,) a0 b0) where

• STuple2 :: (~) ((,) a b) z ((,) a b n n) => Sing a n -> Sing b n -> Sing ((,) a b) z

data Sing ((,,) a0 b0 c0) where

• STuple3 :: (~) ((,,) a b c) z ((,,) a b c n n n) => Sing a n -> Sing b n -> Sing c n -> Sing ((,,) a b c) z

data Sing ((,,,) a0 b0 c0 d0) where

• STuple4 :: (~) ((,,,) a b c d) z ((,,,) a b c d n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing ((,,,) a b c d) z

data Sing ((,,,,) a0 b0 c0 d0 e0) where

• STuple5 :: (~) ((,,,,) a b c d e) z ((,,,,) a b c d e n n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing e n -> Sing ((,,,,) a b c d e) z

data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where

• STuple6 :: (~) ((,,,,,) a b c d e f) z ((,,,,,) a b c d e f n n n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing e n -> Sing f n -> Sing ((,,,,,) a b c d e f) z

data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where

• STuple7 :: (~) ((,,,,,,) a b c d e f g) z ((,,,,,,) a b c d e f g n n n n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing e n -> Sing f n -> Sing g n -> Sing ((,,,,,,) a b c d e f g) z

class SingI a where

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

Methods

sing :: Sing a

Produce the singleton explicitly. You will likely need the ScopedTypeVariables extension to use this method the way you want.

Instances

SingI Bool False

SingI Bool True

SingI Ordering LT

SingI Ordering EQ

SingI Ordering GT

Typeable * a => SingI * a

KnownNat n => SingI Nat n

KnownSymbol n => SingI Symbol n

SingI () ()

SingI [k] ([] k)

SingI (Maybe k) (Nothing k)

SingI a0 n0 => SingI (Maybe a) (Just a n)

(SingI a0 n0, SingI [a0] n1) => SingI [a] ((:) a n n)

SingI b0 n0 => SingI (Either k b) (Right k b n)

SingI a0 n0 => SingI (Either a k) (Left a k n)

(SingI a0 n0, SingI b0 n1) => SingI ((,) a b) ((,) a b n n)

(SingI a0 n0, SingI b0 n1, SingI c0 n2) => SingI ((,,) a b c) ((,,) a b c n n n)

(SingI a0 n0, SingI b0 n1, SingI c0 n2, SingI d0 n3) => SingI ((,,,) a b c d) ((,,,) a b c d n n n n)

(SingI a0 n0, SingI b0 n1, SingI c0 n2, SingI d0 n3, SingI e0 n4) => SingI ((,,,,) a b c d e) ((,,,,) a b c d e n n n n n)

(SingI a0 n0, SingI b0 n1, SingI c0 n2, SingI d0 n3, SingI e0 n4, SingI f0 n5) => SingI ((,,,,,) a b c d e f) ((,,,,,) a b c d e f n n n n n n)

(SingI a0 n0, SingI b0 n1, SingI c0 n2, SingI d0 n3, SingI e0 n4, SingI f0 n5, SingI g0 n6) => SingI ((,,,,,,) a b c d e f g) ((,,,,,,) a b c d e f g n n n n n n n)

class (kparam ~ KProxy) => SingKind kparam where

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.

Associated Types

type DemoteRep kparam :: *

Get a base type from a proxy for the promoted kind. For example, DemoteRep ('KProxy :: KProxy Bool) will be the type Bool.

Methods

fromSing :: Sing (a :: k) -> DemoteRep kparam

Convert a singleton to its unrefined version.

toSing :: DemoteRep kparam -> SomeSing kparam

Convert an unrefined type to an existentially-quantified singleton type.

Instances

SingKind Bool (KProxy Bool)

SingKind Ordering (KProxy Ordering)

SingKind * (KProxy *)

SingKind Nat (KProxy Nat)

SingKind Symbol (KProxy Symbol)

SingKind () (KProxy ())

SingKind a0 (KProxy a0) => SingKind [a] (KProxy [a])

SingKind a0 (KProxy a0) => SingKind (Maybe a) (KProxy (Maybe a))

(SingKind a0 (KProxy a0), SingKind b0 (KProxy b0)) => SingKind (Either a b) (KProxy (Either a b))

(SingKind a0 (KProxy a0), SingKind b0 (KProxy b0)) => SingKind ((,) a b) (KProxy ((,) a b))

(SingKind a0 (KProxy a0), SingKind b0 (KProxy b0), SingKind c0 (KProxy c0)) => SingKind ((,,) a b c) (KProxy ((,,) a b c))

(SingKind a0 (KProxy a0), SingKind b0 (KProxy b0), SingKind c0 (KProxy c0), SingKind d0 (KProxy d0)) => SingKind ((,,,) a b c d) (KProxy ((,,,) a b c d))

(SingKind a0 (KProxy a0), SingKind b0 (KProxy b0), SingKind c0 (KProxy c0), SingKind d0 (KProxy d0), SingKind e0 (KProxy e0)) => SingKind ((,,,,) a b c d e) (KProxy ((,,,,) a b c d e))

(SingKind a0 (KProxy a0), SingKind b0 (KProxy b0), SingKind c0 (KProxy c0), SingKind d0 (KProxy d0), SingKind e0 (KProxy e0), SingKind f0 (KProxy f0)) => SingKind ((,,,,,) a b c d e f) (KProxy ((,,,,,) a b c d e f))

(SingKind a0 (KProxy a0), SingKind b0 (KProxy b0), SingKind c0 (KProxy c0), SingKind d0 (KProxy d0), SingKind e0 (KProxy e0), SingKind f0 (KProxy f0), SingKind g0 (KProxy g0)) => SingKind ((,,,,,,) a b c d e f g) (KProxy ((,,,,,,) a b c d e f g))

type KindOf a = (KProxy :: KProxy k)

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

type Demote a = DemoteRep (KProxy :: KProxy k)

Convenient abbreviation for DemoteRep: type Demote (a :: k) = DemoteRep ('KProxy :: KProxy k)

Auxiliary definitions

These definitions might be mentioned in code generated by Template Haskell, so they must be in scope.

type family a == b :: Bool

A type family to compute Boolean equality. Instances are provided only for open kinds, such as * and function kinds. Instances are also provided for datatypes exported from base. A poly-kinded instance is not provided, as a recursive definition for algebraic kinds is generally more useful.

Instances

type (==) Bool a b = EqBool a b

type (==) Ordering a b = EqOrdering a b

type (==) * a b = EqStar a b

type (==) Nat a b = EqNat a b

type (==) Symbol a b = EqSymbol a b

type (==) () a b = EqUnit a b

type (==) [k] a b = EqList k a b

type (==) (Maybe k) a b = EqMaybe k a b

type (==) (k -> k1) a b = EqArrow k k1 a b

type (==) (Either k k1) a b = EqEither k k1 a b

type (==) ((,) k k1) a b = Eq2 k k1 a b

type (==) ((,,) k k1 k2) a b = Eq3 k k1 k2 a b

type (==) ((,,,) k k1 k2 k3) a b = Eq4 k k1 k2 k3 a b

type (==) ((,,,,) k k1 k2 k3 k4) a b = Eq5 k k1 k2 k3 k4 a b

type (==) ((,,,,,) k k1 k2 k3 k4 k5) a b = Eq6 k k1 k2 k3 k4 k5 a b

type (==) ((,,,,,,) k k1 k2 k3 k4 k5 k6) a b = Eq7 k k1 k2 k3 k4 k5 k6 a b

type (==) ((,,,,,,,) k k1 k2 k3 k4 k5 k6 k7) a b = Eq8 k k1 k2 k3 k4 k5 k6 k7 a b

type (==) ((,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8) a b = Eq9 k k1 k2 k3 k4 k5 k6 k7 k8 a b

type (==) ((,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9) a b = Eq10 k k1 k2 k3 k4 k5 k6 k7 k8 k9 a b

type (==) ((,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10) a b = Eq11 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 a b

type (==) ((,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11) a b = Eq12 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 a b

type (==) ((,,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12) a b = Eq13 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 a b

type (==) ((,,,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13) a b = Eq14 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13 a b

type (==) ((,,,,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13 k14) a b = Eq15 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13 k14 a b

type (:==) a b = a == b

A re-export of the type-level (==) that conforms to the singletons naming convention.

type family If cond tru fls :: k

Type-level If. If True a b ==> a; If False a b ==> b

Equations

If k True tru fls = tru

If k False tru fls = fls

sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)

Conditional over singletons

type (:&&) a b = a && b

class (kparam ~ KProxy) => SEq kparam where

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 '(%:/=)'.

Methods

(%:==) :: forall a b. Sing a -> Sing b -> Sing (a :== b)

Boolean equality on singletons

(%:/=) :: forall a b. Sing a -> Sing b -> Sing (a :/= b)

Boolean disequality on singletons

Instances

SEq Bool (KProxy Bool)

SEq Ordering (KProxy Ordering)

SEq * (KProxy *)

SEq Nat (KProxy Nat)

SEq Symbol (KProxy Symbol)

SEq () (KProxy ())

SEq a0 (KProxy a0) => SEq [a] (KProxy [a])

SEq a0 (KProxy a0) => SEq (Maybe a) (KProxy (Maybe a))

(SEq a0 (KProxy a0), SEq b0 (KProxy b0)) => SEq (Either a b) (KProxy (Either a b))

(SEq a0 (KProxy a0), SEq b0 (KProxy b0)) => SEq ((,) a b) (KProxy ((,) a b))

(SEq a0 (KProxy a0), SEq b0 (KProxy b0), SEq c0 (KProxy c0)) => SEq ((,,) a b c) (KProxy ((,,) a b c))

(SEq a0 (KProxy a0), SEq b0 (KProxy b0), SEq c0 (KProxy c0), SEq d0 (KProxy d0)) => SEq ((,,,) a b c d) (KProxy ((,,,) a b c d))

(SEq a0 (KProxy a0), SEq b0 (KProxy b0), SEq c0 (KProxy c0), SEq d0 (KProxy d0), SEq e0 (KProxy e0)) => SEq ((,,,,) a b c d e) (KProxy ((,,,,) a b c d e))

(SEq a0 (KProxy a0), SEq b0 (KProxy b0), SEq c0 (KProxy c0), SEq d0 (KProxy d0), SEq e0 (KProxy e0), SEq f0 (KProxy f0)) => SEq ((,,,,,) a b c d e f) (KProxy ((,,,,,) a b c d e f))

(SEq a0 (KProxy a0), SEq b0 (KProxy b0), SEq c0 (KProxy c0), SEq d0 (KProxy d0), SEq e0 (KProxy e0), SEq f0 (KProxy f0), SEq g0 (KProxy g0)) => SEq ((,,,,,,) a b c d e f g) (KProxy ((,,,,,,) a b c d e f g))

data Any

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.

class (kparam ~ KProxy) => SDecide kparam where

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.

Methods

(%~) :: forall a b. Sing a -> Sing b -> Decision (a :~: b)

Compute a proof or disproof of equality, given two singletons.

Instances

SDecide Bool (KProxy Bool)

SDecide Ordering (KProxy Ordering)

SDecide * (KProxy *)

SDecide Nat (KProxy Nat)

SDecide Symbol (KProxy Symbol)

SDecide () (KProxy ())

SDecide a0 (KProxy a0) => SDecide [a] (KProxy [a])

SDecide a0 (KProxy a0) => SDecide (Maybe a) (KProxy (Maybe a))

(SDecide a0 (KProxy a0), SDecide b0 (KProxy b0)) => SDecide (Either a b) (KProxy (Either a b))

(SDecide a0 (KProxy a0), SDecide b0 (KProxy b0)) => SDecide ((,) a b) (KProxy ((,) a b))

(SDecide a0 (KProxy a0), SDecide b0 (KProxy b0), SDecide c0 (KProxy c0)) => SDecide ((,,) a b c) (KProxy ((,,) a b c))

(SDecide a0 (KProxy a0), SDecide b0 (KProxy b0), SDecide c0 (KProxy c0), SDecide d0 (KProxy d0)) => SDecide ((,,,) a b c d) (KProxy ((,,,) a b c d))

(SDecide a0 (KProxy a0), SDecide b0 (KProxy b0), SDecide c0 (KProxy c0), SDecide d0 (KProxy d0), SDecide e0 (KProxy e0)) => SDecide ((,,,,) a b c d e) (KProxy ((,,,,) a b c d e))

(SDecide a0 (KProxy a0), SDecide b0 (KProxy b0), SDecide c0 (KProxy c0), SDecide d0 (KProxy d0), SDecide e0 (KProxy e0), SDecide f0 (KProxy f0)) => SDecide ((,,,,,) a b c d e f) (KProxy ((,,,,,) a b c d e f))

(SDecide a0 (KProxy a0), SDecide b0 (KProxy b0), SDecide c0 (KProxy c0), SDecide d0 (KProxy d0), SDecide e0 (KProxy e0), SDecide f0 (KProxy f0), SDecide g0 (KProxy g0)) => SDecide ((,,,,,,) a b c d e f g) (KProxy ((,,,,,,) a b c d e f g))

data a :~: b where

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

Constructors

Refl :: (:~:) k a1 a1

Instances

TestCoercion k ((:~:) k a)

TestEquality k ((:~:) k a)

Typeable (k -> k -> *) ((:~:) k)

(~) k a b => Bounded ((:~:) k a b)

(~) k a b => Enum ((:~:) k a b)

Eq ((:~:) k a b)

((~) * a b, Data a) => Data ((:~:) * a b)

Ord ((:~:) k a b)

(~) k a b => Read ((:~:) k a b)

Show ((:~:) k a b)

data Void

A logically uninhabited data type.

Instances

Eq Void

Data Void

Ord Void

Read Void

Reading a Void value is always a parse error, considering Void as a data type with no constructors.

Show Void

Ix Void

Generic Void

Exception Void

Typeable * Void

type Rep Void = D1 D1Void (C1 C1_0Void (S1 NoSelector (Rec0 Void)))

type Refuted a = a -> Void

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

data Decision a

A Decision about a type a is either a proof of existence or a proof that a cannot exist.

Constructors

Proved a

Witness for a

Disproved (Refuted a)

Proof that no a exists

data KProxy t

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

Constructors

KProxy

data SomeSing kproxy where

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.

Constructors

SomeSing :: Sing (a :: k) -> SomeSing (KProxy :: KProxy k)