singletons
A framework for generating singleton types
http://www.github.com/goldfirere/singletons
Version on this page:  2.6 
LTS Haskell 16.23:  2.6 
Stackage Nightly 20201123:  2.7@rev:1 
Latest on Hackage:  2.7@rev:1 
singletons2.6@sha256:e8e9cea442e37f565fab8604fe54f78c776421e54ed67ac6b4c454e11991db0b,7167
Module documentation for 2.6
 Data
 Data.Singletons
 Data.Singletons.CustomStar
 Data.Singletons.Decide
 Data.Singletons.Prelude
 Data.Singletons.Prelude.Applicative
 Data.Singletons.Prelude.Base
 Data.Singletons.Prelude.Bool
 Data.Singletons.Prelude.Const
 Data.Singletons.Prelude.Either
 Data.Singletons.Prelude.Enum
 Data.Singletons.Prelude.Eq
 Data.Singletons.Prelude.Foldable
 Data.Singletons.Prelude.Function
 Data.Singletons.Prelude.Functor
 Data.Singletons.Prelude.Identity
 Data.Singletons.Prelude.IsString
 Data.Singletons.Prelude.List
 Data.Singletons.Prelude.Maybe
 Data.Singletons.Prelude.Monad
 Data.Singletons.Prelude.Monoid
 Data.Singletons.Prelude.Num
 Data.Singletons.Prelude.Ord
 Data.Singletons.Prelude.Semigroup
 Data.Singletons.Prelude.Show
 Data.Singletons.Prelude.Traversable
 Data.Singletons.Prelude.Tuple
 Data.Singletons.Prelude.Void
 Data.Singletons.ShowSing
 Data.Singletons.Sigma
 Data.Singletons.SuppressUnusedWarnings
 Data.Singletons.TH
 Data.Singletons.TypeError
 Data.Singletons.TypeLits
 Data.Singletons.TypeRepTYPE
 Data.Singletons
singletons 2.6
This is the README file for the singletons library. This file contains all the documentation for the definitions and functions in the library.
The singletons library was written by Richard Eisenberg, rae@cs.brynmawr.edu, and with significant contributions by Jan Stolarek, jan.stolarek@p.lodz.pl. There are two papers that describe the library. Original one, Dependently typed programming with singletons, is available here and will be referenced in this documentation as the “singletons paper”. A followup paper, Promoting Functions to Type Families in Haskell, is available here and will be referenced in this documentation as the “promotion paper”.
Ryan Scott, ryan.gl.scott@gmail.com, is an active maintainer.
Purpose of the singletons library
The library contains a definition of singleton types, which allow programmers to use dependently typed techniques to enforce rich constraints among the types in their programs. See the singletons paper for a more thorough introduction.
The package also allows promotion of termlevel functions to typelevel
equivalents. Accordingly, it exports a Prelude of promoted and singletonized
functions, mirroring functions and datatypes found in Prelude, Data.Bool
,
Data.Maybe
, Data.Either
, Data.Tuple
and Data.List
. See the promotion
paper for a more thorough introduction.
This blog series, authored by Justin Le, offers a tutorial for this library that assumes no knowledge of dependent types.
Compatibility
The singletons library requires GHC 8.8.1 or greater. Any code that uses the singleton generation primitives needs to enable a long list of GHC extensions. This list includes, but is not necessarily limited to, the following:
DataKinds
DefaultSignatures
EmptyCase
ExistentialQuantification
FlexibleContexts
FlexibleInstances
GADTs
InstanceSigs
KindSignatures
NoStarIsType
PolyKinds
RankNTypes
ScopedTypeVariables
TemplateHaskell
TypeApplications
TypeFamilies
TypeOperators
UndecidableInstances
In particular, NoStarIsType
is needed to use the *
type family from the
PNum
class because with StarIsType
enabled, GHC thinks *
is a synonym
for Type
.
You may also want
Wnoredundantconstraints
as the code that singletons
generates uses redundant constraints, and there
seems to be no way, without a large library redesign, to avoid this.
Modules for singleton types
Data.Singletons
exports all the basic singletons definitions. Import this
module if you are not using Template Haskell and wish only to define your
own singletons.
Data.Singletons.TH
exports all the definitions needed to use the Template
Haskell code to generate new singletons.
Data.Singletons.Prelude
reexports Data.Singletons
along with singleton
definitions for various Prelude types. This module provides a singletonized
equivalent of the real Prelude
. Note that not all functions from original
Prelude
could be turned into singletons.
Data.Singletons.Prelude.*
modules provide singletonized equivalents of
definitions found in the following base
library modules: Data.Bool
,
Data.Maybe
, Data.Either
, Data.List
, Data.Tuple
, Data.Void
and
GHC.Base
. We also provide singletonized Eq
, Ord
, Show
, Enum
, and
Bounded
typeclasses.
Data.Singletons.Decide
exports type classes for propositional equality.
Data.Singletons.TypeLits
exports definitions for working with GHC.TypeLits
.
Modules for function promotion
Modules in Data.Promotion
namespace provide functionality required for
function promotion. They mostly reexport a subset of definitions from
respective Data.Singletons
modules.
Data.Promotion.TH
exports all the definitions needed to use the Template
Haskell code to generate promoted definitions.
Data.Promotion.Prelude
and Data.Promotion.Prelude.*
modules reexport all
promoted definitions from respective Data.Singletons.Prelude
modules. Data.Promotion.Prelude.List
adds a significant amount of functions
that couldn’t be singletonized but can be promoted. Some functions still don’t
promote  these are documented in the source code of the module. There is also
Data.Promotion.Prelude.Bounded
module that provides promoted PBounded
typeclass.
Functions to generate singletons
The toplevel functions used to generate singletons are documented in the
Data.Singletons.TH
module. The most common case is just calling singletons
,
which I’ll describe here:
singletons :: Q [Dec] > Q [Dec]
Generates singletons from the definitions given. Because singleton generation requires promotion, this also promotes all of the definitions given to the type level.
Usage example:
$(singletons [d
data Nat = Zero  Succ Nat
pred :: Nat > Nat
pred Zero = Zero
pred (Succ n) = n
])
Definitions used to support singletons
Please refer to the singletons paper for a more indepth explanation of these definitions. Many of the definitions were developed in tandem with Iavor Diatchki.
type family Sing :: k > Type
The type family of singleton types. A new instance of this type family is generated for every new singleton type.
class SingI (a :: k) where
sing :: Sing a
A class used to pass singleton values implicitly. The sing
method produces
an explicit singleton value.
data SomeSing k where
SomeSing :: Sing (a :: k) > SomeSing k
The SomeSing
type wraps up an existentiallyquantified singleton. Note that
the type parameter a
does not appear in the SomeSing
type. Thus, this type
can be used when you have a singleton, but you don’t know at compile time what
it will be. SomeSing Thing
is isomorphic to Thing
.
class SingKind k where
type Demote k :: *
fromSing :: Sing (a :: k) > Demote k
toSing :: Demote k > SomeSing k
This class is used to convert a singleton value back to a value in the
original, unrefined ADT. The fromSing
method converts, say, a
singleton Nat
back to an ordinary Nat
. The toSing
method produces
an existentiallyquantified singleton, wrapped up in a SomeSing
.
The Demote
associated
kindindexed type family maps the kind Nat
back to the type Nat
.
data SingInstance (a :: k) where
SingInstance :: SingI a => SingInstance a
singInstance :: Sing a > SingInstance a
Sometimes you have an explicit singleton (a Sing
) where you need an implicit
one (a dictionary for SingI
). The SingInstance
type simply wraps a SingI
dictionary, and the singInstance
function produces this dictionary from an
explicit singleton. The singInstance
function runs in constant time, using
a little magic.
Equality classes
There are two different notions of equality applicable to singletons: Boolean equality and propositional equality.

Boolean equality is implemented in the type family
(:==)
(which is actually a synonym for the type family(==)
fromData.Type.Equality
) and the classSEq
. See theData.Singletons.Prelude.Eq
module for more information. 
Propositional equality is implemented through the constraint
(~)
, the type(:~:)
, and the classSDecide
. See modulesData.Type.Equality
andData.Singletons.Decide
for more information.
Which one do you need? That depends on your application. Boolean equality has the advantage that your program can take action when two types do not equal, while propositional equality has the advantage that GHC can use the equality of types during type inference.
Instances of SEq
, SDecide
, TestEquality
, and TestCoercion
are generated
when singletons
is called on a datatype that has deriving Eq
. You can also
generate these instances directly through functions exported from
Data.Singletons.TH
.
Show
classes
Promoted and singled versions of the Show
class (PShow
and SShow
,
respectively) are provided in the Data.Singletons.Prelude.Show
module. In
addition, there is a ShowSing
constraint synonym provided in the
Data.Singletons.ShowSing
module:
type ShowSing k = (forall z. Show (Sing (z :: k))
This facilitates the ability to write Show
instances for Sing
instances.
What distinguishes all of these Show
s? Let’s use the False
constructor as
an example. If you used the PShow Bool
instance, then the output of calling
Show_
on False
is "False"
, much like the valuelevel Show Bool
instance
(similarly for the SShow Bool
instance). However, the Show (Sing (z :: Bool))
instance (i.e., ShowSing Bool
) is intended for printing the value of the
singleton constructor SFalse
, so calling show SFalse
yields "SFalse"
.
Instance of PShow
, SShow
, and Show
(for the singleton type) are generated
when singletons
is called on a datatype that has deriving Show
. You can also
generate these instances directly through functions exported from
Data.Singletons.TH
.
A promoted and singled Show
instance is provided for Symbol
, but it is only
a crude approximation of the valuelevel Show
instance for String
. On the
value level, showing String
s escapes special characters (such as double
quotes), but implementing this requires patternmatching on character literals,
something which is currently impossible at the type level. As a consequence, the
typelevel Show
instance for Symbol
s does not do any character escaping.
Errors
The singletons
library provides two different ways to handle errors:

The
Error
type family, fromData.Singletons.TypeLits
:type family Error (str :: a) :: k where {}
This is simply an empty, closed type family, which means that it will fail to reduce regardless of its input. The typical use case is giving it a
Symbol
as an argument, so that something akin toError "This is an error message"
appears in error messages. 
The
TypeError
type family, fromData.Singletons.TypeError
. This is a dropin replacement forTypeError
fromGHC.TypeLits
which can be used at both the type level and the value level (via thetypeError
function).Unlike
Error
,TypeError
will result in an actual compiletime error message, which may be more desirable depending on the use case.
Predefined singletons
The singletons library defines a number of singleton types and functions by default:
Bool
Maybe
Either
Ordering
()
 tuples up to length 7
 lists
These are all available through Data.Singletons.Prelude
. Functions that
operate on these singletons are available from modules such as Data.Singletons.Bool
and Data.Singletons.Maybe
.
Promoting functions
Function promotion allows to generate typelevel equivalents of termlevel definitions. Almost all Haskell source constructs are supported – see last section of this README for a full list.
Promoted definitions are usually generated by calling promote
function:
$(promote [d
data Nat = Zero  Succ Nat
pred :: Nat > Nat
pred Zero = Zero
pred (Succ n) = n
])
Every promoted function and data constructor definition comes with a set of
socalled “symbols”. These are required to represent partial application at the
type level. Each function gets N+1 symbols, where N is the arity. Symbols
represent application of between 0 to N arguments. When calling any of the
promoted definitions it is important refer to it using their symbol
name. Moreover, there is new function application at the type level represented
by Apply
type family. Symbol representing arity X can have X arguments passed
in using normal function application. All other parameters must be passed by
calling Apply
.
Users also have access to Data.Promotion.Prelude
and its submodules (Base
,
Bool
, Either
, List
, Maybe
and Tuple
). These provide promoted versions
of function found in GHC’s base library.
Note that GHC resolves variable names in Template Haskell quotes. You cannot then use an undefined identifier in a quote, making idioms like this not work:
type family Foo a where ...
$(promote [d ... foo x ... ])
In this example, foo
would be out of scope.
Refer to the promotion paper for more details on function promotion.
Classes and instances
This is best understood by example. Let’s look at a stripped down Ord
:
class Eq a => Ord a where
compare :: a > a > Ordering
(<) :: a > a > Bool
x < y = case x `compare` y of
LT > True
EQ > False
GT > False
This class gets promoted to a “kind class” thus:
class PEq a => POrd a where
type Compare (x :: a) (y :: a) :: Ordering
type (:<) (x :: a) (y :: a) :: Bool
type x :< y = ...  promoting `case` is yucky.
Note that default method definitions become default associated type family instances. This works out quite nicely.
We also get this singleton class:
class SEq a => SOrd a where
sCompare :: forall (x :: a) (y :: a). Sing x > Sing y > Sing (Compare x y)
(%:<) :: forall (x :: a) (y :: a). Sing x > Sing y > Sing (x :< y)
default (%:<) :: forall (x :: a) (y :: a).
((x :< y) ~ { RHS from (:<) above })
=> Sing x > Sing y > Sing (x :< y)
x %:< y = ...  this is a bit yucky too
Note that a singletonized class needs to use default
signatures, because
typechecking the default body requires that the default associated type
family instance was used in the promoted class. The extra equality constraint
on the default signature asserts this fact to the type checker.
Instances work roughly similarly.
instance Ord Bool where
compare False False = EQ
compare False True = LT
compare True False = GT
compare True True = EQ
instance POrd Bool where
type Compare 'False 'False = 'EQ
type Compare 'False 'True = 'LT
type Compare 'True 'False = 'GT
type Compare 'True 'True = 'EQ
instance SOrd Bool where
sCompare :: forall (x :: a) (y :: a). Sing x > Sing y > Sing (Compare x y)
sCompare SFalse SFalse = SEQ
sCompare SFalse STrue = SLT
sCompare STrue SFalse = SGT
sCompare STrue STrue = SEQ
The only interesting bit here is the instance signature. It’s not necessary in such a simple scenario, but more complicated functions need to refer to scoped type variables, which the instance signature can bring into scope. The defaults all just work.
On names
The singletons library has to produce new names for the new constructs it generates. Here are some examples showing how this is done:

original datatype:
Nat
promoted kind:
Nat
singleton type:
SNat
(which is really a synonym forSing
) 
original datatype:
/\
promoted kind:
/\
singleton type:
%/\

original constructor:
Succ
promoted type:
'Succ
(you can useSucc
when unambiguous)singleton constructor:
SSucc
symbols:
SuccSym0
,SuccSym1

original constructor:
:+:
promoted type:
':+:
singleton constructor:
:%+:
symbols:
:+:@#@$
,:+:@#@$$
,:+:@#@$$$

original value:
pred
promoted type:
Pred
singleton value:
sPred
symbols:
PredSym0
,PredSym1

original value:
+
promoted type:
+
singleton value:
%+
symbols:
+@#@$
,+@#@$$
,+@#@$$$

original class:
Num
promoted class:
PNum
singleton class:
SNum

original class:
~>
promoted class:
#~>
singleton class:
%~>
Special names
There are some special cases, listed below (with asterisks* denoting special treatment):

original datatype:
[]
promoted kind:
[]
singleton type*:
SList

original constructor:
[]
promoted type:
'[]
singleton constructor*:
SNil
symbols*:
NilSym0

original constructor:
:
promoted type:
':
singleton constructor*:
SCons
symbols:
:@#@$
,:@#@$$
,:@#@$$$

original datatype:
(,)
promoted kind:
(,)
singleton type*:
STuple2

original constructor:
(,)
promoted type:
'(,)
singleton constructor*:
STuple2
symbols*:
Tuple2Sym0
,Tuple2Sym1
,Tuple2Sym2
All tuples (including the 0tuple, unit) are treated similarly.

original value:
___foo
promoted type*:
US___foo
(”US
” stands for “underscore”)singleton value*:
___sfoo
symbols*:
US___fooSym0
All functions that begin with leading underscores are treated similarly.
Supported Haskell constructs
The following constructs are fully supported:
 variables
 tuples
 constructors
 if statements
 infix expressions and types
_
patterns aliased patterns
 lists (including list comprehensions)
do
notation sections
 undefined
 error
 deriving
Eq
,Ord
,Show
,Bounded
,Enum
,Functor
,Foldable
, andTraversable
, as well as thestock
andanyclass
deriving strategies  class constraints (though these sometimes fail with
let
,lambda
, andcase
)  literals (for
Nat
andSymbol
), including overloaded number literals  unboxed tuples (which are treated as normal tuples)
 records
 pattern guards
 case
 let
 lambda expressions
!
and~
patterns (silently but successfully ignored during promotion) class and instance declarations
 scoped type variables
 signatures (e.g.,
(x :: Maybe a)
) in expressions and patterns InstanceSigs
 higherkinded type variables (see below)
 finite arithmetic sequences (see below)
 functional dependencies (with limitations – see below)
 type families (with limitations – see below)
Higherkinded type variables in class
/data
declarations must be annotated
explicitly. This is due to GHC’s handling of complete
userspecified kind signatures, or CUSKs.
Briefly, singletons
has a hard
time conforming to the precise rules that GHC imposes around CUSKs and so
needs a little help around kind inference here. See
this pull request for more
background.
singletons
is slightly more conservative with respect to deriving
than GHC is.
The stock classes listed above (Eq
, Ord
, Show
, Bounded
, Enum
, Functor
,
Foldable
, and Traversable
) are the only ones that singletons
will derive
without an explicit deriving strategy. To do anything more exotic, one must
explicitly indicate one’s intentions by using the DerivingStrategies
extension.
singletons
fully supports the anyclass
strategy as well as the stock
strategy
(at least, for the classes listed above). singletons
does not support the
newtype
strategy, as there is not an equivalent of coerce
at the type level.
singletons
has partial support for arithmetic sequences (which desugar to
methods from the Enum
class under the hood). Finite sequences (e.g.,
[0..42]) are fully supported. However, infinite sequences (e.g., [0..]),
which desugar to calls to enumFromTo
or enumFromThenTo
, are not supported,
as these would require using infinite lists at the type level.
The following constructs are supported for promotion but not singleton generation:

datatypes with constructors which have contexts. For example, the following datatype does not singletonize:
data T a where MkT :: Show a => a > T a
Constructors like these do not interact well with the current design of the
SingKind
class. But see this bug report, which proposes a redesign forSingKind
(in a future version of GHC with certain bugfixes) which could permit constructors with equality constraints. 
overlapping patterns. Note that overlapping patterns are sometimes not obvious. For example, the
filter
function does not singletonize due to overlapping patterns:filter :: (a > Bool) > [a] > [a] filter _pred [] = [] filter pred (x:xs)  pred x = x : filter pred xs  otherwise = filter pred xs
Overlap is caused by
otherwise
catchall guard, which is always true and thus overlaps withpred x
guard.Another nonobvious source of overlapping patterns comes from partial pattern matches in
do
notation. For example:f :: [()] f = do Just () < [Nothing] return ()
This has overlap because the partial pattern match desugars to the following:
f :: [()] f = case [Nothing] of Just () > return () _ > fail "Partial pattern match in do notation"
Here, it is more evident that the catchall pattern
_
overlaps with the one above it.
The following constructs are not supported:
 datatypes that store arrows,
Nat
, orSymbol
 literals (limited support)
Why are these out of reach?
As described in the promotion paper, promotion of datatypes that store arrows is currently impossible. So if you have a declaration such as
data Foo = Bar (Bool > Maybe Bool)
you will quickly run into errors.
Literals are problematic because we rely on GHC’s builtin support, which
currently is limited. Functions that operate on strings will not work because
type level strings are no longer considered lists of characters. Function
working on integer literals can be promoted by rewriting them to use
Nat
. Since Nat
does not exist at the term level it will only be possible to
use the promoted definition, but not the original, termlevel one.
This is the same line of reasoning that forbids the use of Nat
or Symbol
in datatype definitions. But, see this bug
report for a workaround.
Support for *
The builtin Haskell promotion mechanism does not yet have a full story around
the kind *
(the kind of types that have values). Ideally, promoting some form
of TypeRep
would yield *
, but the implementation of TypeRep
would have to
be updated for this to really work out. In the meantime, users who wish to
experiment with this feature have two options:

The module
Data.Singletons.TypeRepTYPE
has all the definitions possible for making*
the promoted version ofTypeRep
, asTypeRep
is currently implemented. The singleton associated withTypeRep
has one constructor:type instance Sing @(TYPE rep) = TypeRep
(Recall that
type * = TYPE LiftedRep
.) Note that any datatypes that storeTypeRep
s will not generally work as expected; the builtin promotion mechanism will not promoteTypeRep
to*
. 
The module
Data.Singletons.CustomStar
allows the programmer to define a subset of types with which to work. See the Haddock documentation for the functionsingletonStar
for more info.
Known bugs

Record updates don’t singletonize

Inference dependent on functional dependencies is unpredictably bad. The problem is that a use of an associated type family tied to a class with fundeps doesn’t provoke the fundep to kick in. This is GHC’s problem, in the end.

Singled code that contains uses type families is likely to fail due to GHC Trac #12564. Note that singling type family declarations themselves is fine (and often desired, since that produces defunctionalization symbols for them).

Singling instances of polykinded type classes is likely to fail due to #358. However, one can often work around the issue by using
InstanceSigs
. For instance, the following code will not single:class C (f :: k > Type) where method :: f a instance C [] where method = []
Adding a type signature for
method
in theC []
is sufficient to work around the issue, though:instance C [] where method :: [a] method = []
Changes
Changelog for singletons project
2.6

Require GHC 8.8.

Sing
has switched from a data family to a type family. This has a number of consequences:
Names like
SBool
,SMaybe
, etc. are no longer type synonyms for particular instantiations ofSing
but are instead the names of the singleton data types themselves. In other words, previous versions ofsingletons
would provide this:data instance Sing :: Bool > Type where SFalse :: Sing False STrue :: Sing True type SBool = (Sing :: Bool > Type)
Whereas with
Sing
asatypefamily,singletons
now provides this:data SBool :: Bool > Type where SFalse :: SBool False STrue :: SBool True type instance Sing @Bool = SBool

The
Sing
instance forTYPE rep
inData.Singletons.TypeRepTYPE
is now directly defined astype instance Sing @(TYPE rep) = TypeRep
, without the use of an intermediate newtype as before. 
Due to limitations in the ways that quantified constraints and type families can interact (see this GHC issue), the internals of
ShowSing
has to be tweaked in order to continue to work withSing
asatypefamily. One notable consequence of this is thatShow
instances for singleton types can no longer be derived—they must be written by hand in order to work around this GHC bug. This is unlikely to affect you unless you define ‘Show’ instances for singleton types by hand. For more information, refer to the Haddocks forShowSing'
inData.Singletons.ShowSing
. 
GHC does not permit type class instances to mention type families, which means that it is no longer possible to define instances that mention the
Sing
type constructor. For this reason, aWrappedSing
data type (which is a newtype aroundSing
) was introduced so that one can hang instances off of it.This had one noticeable effect in
singletons
itself: there are no longerTestEquality Sing
orTestCoercion Sing
instances. Instead,singletons
now generates a separateTestEquality
/TestCoercion
instance for every data type that singles a derivedEq
instance. In addition, theData.Singletons.Decide
module now provides topleveldecideEquality
/decideCoercion
functions which provide the behavior oftestEquality
/testCoercion
, but monomorphized toSing
. Finally,TestEquality
/TestCoercion
instances are provided forWrappedSing
.


GHC’s behavior surrounding kind inference for local definitions has changed in 8.8, and certain code that
singletons
generates for local definitions may no longer typecheck as a result. While we have taken measures to mitigate the issue onsingletons
’ end, there still exists code that must be patched on the users’ end in order to continue compiling. For instance, here is an example of code that stopped compiling with the switch to GHC 8.8:replicateM_ :: (Applicative m) => Nat > m a > m () replicateM_ cnt0 f = loop cnt0 where loop cnt  cnt <= 0 = pure ()  otherwise = f *> loop (cnt  1)
This produces errors to the effect of:
• Could not deduce (SNum k1) arising from a use of ‘sFromInteger’ from the context: SApplicative m ... • Could not deduce (SOrd k1) arising from a use of ‘%<=’ from the context: SApplicative m ...
The issue is that GHC 8.8 now kindgeneralizes
sLoop
(whereas it did not previously), explaining why the error message mentions a mysterious kind variablek1
that only appeared after kind generalization. The solution is to giveloop
an explicit type signature like so:replicateM_ :: (Applicative m) => Nat > m a > m () +replicateM_ :: forall m a. (Applicative m) => Nat > m a > m () replicateM_ cnt0 f = loop cnt0 where + loop :: Nat > m () loop cnt  cnt <= 0 = pure ()  otherwise = f *> loop (cnt  1)
This general approach should be sufficient to fix any type inference regressions that were introduced between GHC 8.6 and 8.8. If this isn’t the case, please file an issue.

Due to GHC Trac #16133 being fixed,
singletons
generated code now requires explicitly enabling theTypeApplications
extension. (The generated code was always usingTypeApplications
under the hood, but it’s only now that GHC is detecting it.) 
Data.Singletons
now defines a family ofSingI
instances forTyCon1
throughTyCon8
:instance (forall a. SingI a => SingI (f a), ...) => SingI (TyCon1 f) instance (forall a b. (SingI a, SingI b) => SingI (f a b), ...) => SingI (TyCon2 f) ...
As a result,
singletons
no longer generates instances forSingI
instances for applications ofTyCon{N}
to particular type constructors, as they have been superseded by the instances above. 
Changes to
Data.Singletons.Sigma
:
SSigma
, the singleton type forSigma
, is now defined. 
New functions
fstSigma
,sndSigma
,FstSigma
,SndSigma
,currySigma
, anduncurrySigma
have been added. AShow
instance forSigma
has also been added. 
projSigma1
has been redefined to use continuationpassing style to more closely resemble its cousinprojSigma2
. The new type signature ofprojSigma1
is:projSigma1 :: (forall (fst :: s). Sing fst > r) > Sigma s t > r
The old type signature of
projSigma1
can be found in thefstSigma
function. 
Σ
has been redefined such that it is now a partial application ofSigma
, like so:type Σ = Sigma
One benefit of this change is that one no longer needs defunctionalization symbols in order to partially apply
Σ
. As a result,ΣSym0
,ΣSym1
, andΣSym2
have been removed.


In line with corresponding changes in
base4.13
, theFail
/sFail
methods of{P,S}Monad
have been removed in favor of new{P,S}MonadFail
classes introduced in theData.Singletons.Prelude.Monad.Fail
module. These classes are also reexported fromData.Singletons.Prelude
. 
Fix a bug where expressions with explicit signatures involving function types would fail to single.

The infix names
(.)
and(!)
are no longer mapped to(:.)
and(:!)
, as GHC 8.8 learned to parse them at the type level. 
The
Enum
instance forSomeSing
now uses more efficient implementations ofenumFromTo
andenumFromThenTo
that no longer require aSingKind
constraint.
2.5.1
ShowSing
is now a type class (with a single instance) instead of a type synonym. This was changed because definingShowSing
as a type synonym prevents it from working well with recursive types due to an unfortunate GHC bug. For more information, see issue #371. Add an
IsString
instance forSomeSing
.
2.5

The
Data.Promotion.Prelude.*
namespace has been removed. Use the corresponding modules in theData.Singletons.Prelude.*
namespace instead. 
Fix a regression in which certain infix type families, such as
(++)
,($)
,(+)
, and others, did not have the correct fixities. 
The default implementation of the
(==)
type inPEq
was changed from(Data.Type.Equality.==)
to a custom type family,DefaultEq
. The reason for this change is that(Data.Type.Equality.==)
is unable to conclude thata == a
reduces toTrue
for anya
. (As a result, the previous version ofsingletons
regressed in terms of type inference for thePEq
instances forNat
andSymbol
, which used that default.) On the other hand,DefaultEq a a
does reduce toTrue
for alla
. 
Add
Enum Nat
,Show Nat
, andShow Symbol
instances toData.Singletons.TypeLits
. 
Template Haskellgenerated code may require
DataKinds
andPolyKinds
in scenarios which did not previously require it:singletons
now explicitly quantifies all kind variables used in explicitforall
s.singletons
now generatesa ~> b
instead ofTyFun a b > Type
whenever possible.

Since
thdesugar
now desugars all data types to GADT syntax, Template Haskellgenerated code may requireGADTs
in situations that didn’t require it before. 
Overhaul the way derived
Show
instances for singleton types works. Before, there was an awkwardShowSing
class (which was essentially a cargoculted version ofShow
specialized forSing
) that one had to create instances for separately. Now that GHC hasQuantifiedConstraints
, we can scrap this whole class and turnShowSing
into a simple type synonym:type ShowSing k = forall z. Show (Sing (z :: k))
Now, instead of generating a handwritten
ShowSing
andShow
instance for each singleton type, we only generate a single (derived!)Show
instance. As a result of this change, you will likely need to enableQuantifiedConstraints
andStandaloneDeriving
if you single any derivedShow
instances in your code. 
The kind of the type parameter to
SingI
is no longer specified. This only affects you if you were using thesing
method withTypeApplications
. For instance, if you were usingsing @Bool @True
before, then you will now need to now usesing @Bool
instead. 
singletons
now generatesSingI
instances for defunctionalization symbols through Template Haskell. As a result, you may need to enableFlexibleInstances
in more places. 
genDefunSymbols
is now more robust with respect to types that use dependent quantification, such as:type family MyProxy k (a :: k) :: Type where MyProxy k (a :: k) = Proxy a
See the documentation for
genDefunSymbols
for limitations to this. 
Rename
Data.Singletons.TypeRepStar
toData.Singletons.TypeRepTYPE
, and generalize theSing :: Type > Type
instance toSing :: TYPE rep > Type
, allowing it to work over more open kinds. Also renameSomeTypeRepStar
toSomeTypeRepTYPE
, and change its definition accordingly. 
Promoting or singling a type synonym or type family declaration now produces defunctionalization symbols for it. (Previously, promoting or singling a type synonym did nothing whatsoever, and promoting or singling a type family produced an error.)

singletons
now produces fixity declarations for defunctionalization symbols when appropriate. 
Add
(%<=?)
, a singled version of(<=?)
fromGHC.TypeNats
, as well as defunctionalization symbols for(<=?)
, toData.Singletons.TypeLits
. 
Add
Data.Singletons.Prelude.{Semigroup,Monoid}
, which define promoted and singled versions of theSemigroup
andMonoid
type classes, as well as various newtype modifiers.Symbol
is now has promotedSemigroup
andMonoid
instances as well. As a consequence,Data.Singletons.TypeLits
no longer exports(<>)
or(%<>)
, as they are superseded by the corresponding methods fromPSemigroup
andSSemigroup
. 
Add promoted and singled versions of the
Functor
,Foldable
,Traversable
,Applicative
,Alternative
,Monad
,MonadPlus
, andMonadZip
classes. Among other things, this grants the ability to promote or singledo
notation and list comprehensions.Data.Singletons.Prelude.List
now reexports more generalFoldable
/Traversable
functions wherever possible, just asData.List
does.

Add
Data.Singletons.Prelude.{Const,Identity}
, which define promoted and singled version of theConst
andIdentity
data types, respectively. 
Promote and single the
Down
newtype inData.Singletons.Prelude.Ord
. 
To match the
base
library, the promoted/singled versions ofcomparing
andthenCmp
are no longer exported fromData.Singletons.Prelude
. (They continue to live inData.Singletons.Prelude.Ord
.) 
Permit singling of expression and pattern signatures.

Permit promotion and singling of
InstanceSigs
. 
sError
andsUndefined
now haveHasCallStack
constraints, like their counterpartserror
andundefined
. The promoted and singled counterparts toerrorWithoutStackTrace
have also been added in case you do not want this behavior. 
Add
Data.Singletons.TypeError
, which provides a dropin replacement forGHC.TypeLits.TypeError
which can be used at both the value and typelevel.
2.4.1
 Restore the
TyCon1
,TyCon2
, etc. types. It turns out that the newTyCon
doesn’t work with kindpolymorphic tycons.
2.4

Require GHC 8.4.

Demote Nat
is nowNatural
(fromNumeric.Natural
) instead ofInteger
. In accordance with this change,Data.Singletons.TypeLits
now exposesGHC.TypeNats.natVal
(which returns aNatural
) instead ofGHC.TypeLits.natVal
(which returns anInteger
). 
The naming conventions for infix identifiers (e.g.,
(&*)
) have been overhauled.
Infix functions (that are not constructors) are no longer prepended with a colon when promoted to type families. For instance, the promoted version of
(&*)
is now called(&*)
as well, instead of(:&*)
as before.There is one exception to this rule: the
(.)
function, which is promoted as(:.)
. The reason is that one cannot write(.)
at the type level. 
Singletons for infix functions are now always prepended with
%
instead of%:
. 
Singletons for infix classes are now always prepended with
%
instead of:%
. 
Singletons for infix datatypes are now always prepended with a
%
.(Before, there was an unspoken requirement that singling an infix datatype required that name to begin with a colon, and the singleton type would begin with
:%
. But now that infix datatype names can be things like(+)
, this requirement became obsolete.)
The upshot is that most infix names can now be promoted using the same name, and singled by simply prepending the name with
%
. 

The suffix for defunctionalized names of symbolic functions (e.g.,
(+)
) has changed. Before, the promoted type name would be suffixed with some number of dollar signs (e.g.,(+$)
and(+$$)
) to indicate defunctionalization symbols. Now, the promoted type name is first suffixed with@#@
and then followed by dollar signs (e.g.,(+@#@$)
and(+@#@$$)
). Adopting this conventional eliminates naming conflicts that could arise for functions that consisted of solely$
symbols. 
The treatment of
undefined
is less magical. Before, all uses ofundefined
would be promoted toGHC.Exts.Any
and singled toundefined
. Now, there is a properUndefined
type family andsUndefined
singleton function. 
As a consequence of not promoting
undefined
toAny
, there is no need to have a specialany_
function to distinguish the function on lists. The corresponding promoted type, singleton function, and defunctionalization symbols are now namedAny
,sAny
, andAnySym{0,1,2}
. 
Rework the treatment of empty data types:
 Generated
SingKind
instances for empty data types now useEmptyCase
instead of simplyerror
ing.  Derived
PEq
instances for empty data types now returnTrue
instead ofFalse
. DerivedSEq
instances now returnTrue
instead oferror
ing.  Derived
SDecide
instances for empty data types now returnProved bottom
, wherebottom
is a divergent computation, instead oferror
ing.
 Generated

Add
Data.Singletons.Prelude.IsString
andData.Promotion.Prelude.IsString
modules.IsString.fromString
is now used when promoting or singling string literals when theXOverloadedStrings
extension is enabled (similarly to howNum.fromInteger
is currently used when promoting or singling numeric literals). 
Add
Data.Singletons.Prelude.Void
. 
Add promoted and singled versions of
div
,mod
,divMod
,quot
,rem
, andquotRem
toData.Singletons.TypeLits
that utilize the efficientDiv
andMod
type families fromGHC.TypeNats
. Also addsLog2
and defunctionalization symbols forLog2
fromGHC.TypeNats
. 
Add
(<>)
and(%<>)
, the promoted and singled versions ofAppendSymbol
fromGHC.TypeLits
. 
Add
(%^)
, the singleton version ofGHC.TypeLits.^
. 
Add
unlines
andunwords
toData.Singletons.Prelude.List
. 
Add promoted and singled versions of
Show
, includingderiving
support. 
Add a
ShowSing
class, which facilitates the ability to writeShow
instances forSing
instances. 
Permit derived
Ord
instances for empty datatypes. 
Permit standalone
deriving
declarations. 
Permit
DeriveAnyClass
(through theanyclass
keyword ofDerivingStrategies
) 
Add a valuelevel
(@@)
, which is a synonym forapplySing
. 
Add
Eq
,Ord
,Num
,Enum
, andBounded
instances forSomeSing
, which leverage theSEq
,SOrd
,SNum
,SEnum
, andSBounded
instances, respectively, for the underlyingSing
. 
Rework the
Sing (a :: *)
instance inData.Singletons.TypeRepStar
such that it now uses typeindexedTypeable
. The newSing
instance is now:newtype instance Sing :: Type > Type where STypeRep :: TypeRep a > Sing a
Accordingly, the
SingKind
instance has also been changed:instance SingKind Type where type Demote Type = SomeTypeRepStar ... data SomeTypeRepStar where SomeTypeRepStar :: forall (a :: *). !(TypeRep a) > SomeTypeRepStar
Aside from cleaning up some implementation details, this change assures that
toSing
can only be called onTypeRep
s whose kind is of kind*
. The previous implementation did not enforce this, which could lead to segfaults if used carelessly. 
Instead of
error
ing, thetoSing
implementation in theSingKind (k1 ~> k2)
instance now works as one would expect (provided the user adheres to some commonsenseSingKind
laws, which are now documented). 
Add a
demote
function, which is a convenient shorthand forfromSing sing
. 
Add a
Data.Singletons.Sigma
module with aSigma
(dependent pair) data type. 
Export defunctionalization symbols for
Demote
,SameKind,
KindOf,
(~>),
Apply, and
(@@)from
Data.Singletons`. 
Add an explicitly bidirectional pattern synonym
Sing
. Pattern matching onSing
brings aSingI ty
constraint into scope from a singletonSing ty
. 
Add an explicitly bidirectional pattern synonym
FromSing
. Pattern matching on any demoted (base) type gives us the corresponding singleton. 
Add explicitly bidirectional pattern synonyms
SLambda{2..8}
. Pattern matching on any defunctionalized singleton yields a termlevel Haskell function on singletons. 
Remove the family of
TyCon1
,TyCon2
, …, in favor of justTyCon
. GHC 8.4’s type system is powerful enough to allow this nice simplification.
2.3

Documentation clarifiation in
Data.Singletons.TypeLits
, thanks to @ivanm. 
Demote
was no longer a convenient way of callingDemoteRep
and has been removed.DemoteRep
has been renamedDemote
. 
DemoteRep
is now injective. 
Demoting a
Symbol
now givesText
. This is motivated by makingDemoteRep
injective. (IfSymbol
demoted toString
, then there would be a conflict between demoting[Char]
andSymbol
.) 
Generating singletons also now generates fixity declarations for the singletonized definitions, thanks to @intindex.

Though more an implementation detail: singletons no longer uses kindlevel proxies anywhere, thanks again to @intindex.

Support for promoting higherkinded type variables, thanks for @intindex.

Data.Singletons.TypeLits
now exports defunctionalization symbols forKnownNat
andKnownSymbol
. 
Better type inference support around constraints, as tracked in Issue #176.

Type synonym definitions are now ignored, as they should be.

Show
instances forSNat
andSSymbol
, thanks to @cumber. 
The
singFun
andunSingFun
functions no longer use proxies, preferringTypeApplications
.
2.2

With
TypeInType
, we no longer kindKProxy
. @intindex has very helpfully removed the use ofKProxy
fromsingletons
. 
Drop support for GHC 7.x.

Remove
bugInGHC
. That function was intended to work around GHC’s difficulty in detecting exhaustiveness of GADT pattern matches. GHC 8 comes with a much better exhaustiveness checker, and so this function is no longer necessary.
2.1

Require
thdesugar
>= 1.6 
Work with GHC 8. GHC 8 gives the opportunity to simplify some pieces of singletons, but these opportunities are not yet fully realized. For example, injective type families means that we no longer need
Sing
to be a data family; it could be a type family. This might drastically simplify the way functions are singletonized. But not yet! 
singletons
now outputs a few more type/kind annotations to help GHC do type inference. There may be a few more programs accepted than before. (This is the fix for #136.)
2.0.1
 Lots more functions in
Data.Singletons.Prelude.List
:filter
,find
,elemIndex
,elemIndices
,findIndex
,findIndices
,intersect
,intersectBy
,takeWhile
,dropWhile
,dropWhileEnd
,span
,break
,take
,drop
,splitAt
,group
,maximum
,minimum
,insert
,sort
,groupBy
,lookup
,partition
,sum
,product
,length
,replicate
,transpose
,(!!)
,nub
,nubBy
,unionBy
,union
,genericLength
2.0.0.2
 Fix fixity of
*
.
2.0.0.1
 Make haddock work.
2.0

Instance promotion now works properly – it was quite buggy in 1.0.

Classes and instances can now be singletonized.

Limited support for functional dependencies.

We now have promoted and singletonized versions of
Enum
, as well asBounded
. 
Deriving
Enum
is also now supported. 
Ditto for
Num
, which includes an instance forNat
, naturally. 
Promoting a literal number now uses overloaded literals at the type level, using a typelevel
FromInteger
in the typelevelNum
class. 
Better support for dealing with constraints. Some previouslyunsingletonizable functions that have constrained parameters now work.

No more orphan
Quasi
instances! 
Support for functions of arity 8 (instead of the old limit, 7).

Full support for fixity declarations.

A raft of bugfixes.

Drop support for GHC 7.8. You must have GHC 7.10.2.
1.1.2.1
Fix bug #116, thus allowing locallydeclared symbols to be used in GHC 7.10.
1.1.2
 No more GHC 7.8.2 support – you must have GHC 7.8.3.
1.1.1
Update testsuite to work with thdesugar1.5.2. No functional changes.
1.1
This is a maintenance release to support building (but not testing, due to
GHC bug #10058) with 7.10. This release also targets thdesugar1.5. Some
types changed (using thdesugar’s new DsMonad
instead of Quasi
), but
clients generally won’t need to make any changes, unless they, too, generalize
over Quasi
.
1.0
This is a complete rewrite of the package.

A much wider array of surface syntax is now accepted for promotion and singletonization, including
let
,case
, partiallyapplied functions, and anonymous functions,where
, sections, among others. 
Classes and instances can be promoted (but not singletonized).

Derivation of promoted instances for
Ord
andBounded
.
This release can be seen as a “technology preview”. More features are coming soon.
This version drops GHC 7.6 support.
0.10.0
Template Haskell names are now more hygienic. In other words, singletons
won’t try to gobble up something happened to be named Sing
in your project.
(Note that the Template Haskell names are not completely hygienic; names
generated during singleton generation can still cause conflicts.)
If a function to be promoted or singletonized is missing a type signature, that is now an error, not a warning.
Added a new external module Data.Singletons.TypeLits, which contain the singletons for GHC.TypeLits. Some convenience functions are also provided.
The extension EmptyCase
is no longer needed. This caused pain when trying
to support both GHC 7.6.3 and 7.8.
0.9.3
Fix export list of Data.Singletons.TH, again again.
Add SEq
instances for Nat
and Symbol
.
0.9.2
Fix export list of Data.Singletons.TH, again.
0.9.1
Fix export list of Data.Singletons.TH.
0.9.0
Make compatible with GHC HEAD, but HEAD reports core lint errors sometimes.
Change module structure significantly. If you want to derive your own
singletons, you should import Data.Singletons.TH
. The module
Data.Singletons
now exports functions only for the use of singletons.
New modules Data.Singletons.Bool
, ...Maybe
, ...Either
, and ...List
are just like their equivalents from Data.
, except for List
, which is
quite lacking in features.
For singleton equality, use Data.Singletons.Eq
.
For propositional singleton equality, use Data.Singletons.Decide
.
New module Data.Singletons.Prelude
is meant to mirror the Haskell Prelude,
but with singleton definitions.
Streamline representation of singletons, resulting in exponential speedup at execution. (This has not been rigorously measured, but the data structures are now exponentially smaller.)
Add internal support for TypeLits, because the TypeLits module no longer exports singleton definitions.
Add support for existential singletons, through the toSing
method of
SingKind
.
Remove the SingE
class, bundling its functionality into SingKind
.
Thus, the SingRep
synonym has also been removed.
Name change: KindIs
becomes KProxy
.
Add support for singletonizing calls to error
.
Add support for singletonizing empty data definitions.
0.8.6
Make compatible with GHC HEAD, but HEAD reports core lint errors sometimes.
0.8.5
Bug fix to make singletons compatible with GHC 7.6.1.
Added git info to cabal file.
0.8.4
Update to work with latest version of GHC (7.7.20130114).
Now use branched type family instances to allow for promotion of functions with overlapping patterns.
Permit promotion of functions with constraints by omitting constraints.
0.8.3
Update to work with latest version of GHC (7.7.20121031).
Removed use of Any to simulate kind classes; now using KindOf and OfKind from GHC.TypeLits.
Made compatible with GHC.TypeLits.
0.8.2
Added this changelog
Update to work with latest version of GHC (7.6.1). (There was a change to Template Haskell).
Moved library into Data.Singletons.
0.8.1
Update to work with latest version of GHC. (There was a change to Template Haskell).
Updated dependencies in cabal to include the newer version of TH.
0.8
Initial public release