singletonsth
A framework for generating singleton types
http://www.github.com/goldfirere/singletons
LTS Haskell 22.12:  3.2 
Stackage Nightly 20240226:  3.3 
Latest on Hackage:  3.3 
singletonsth3.3@sha256:5c064361b26ed0f4f02ff8c6f903672542a8fb7e6817a401e167fdb6dbb9e6bc,4648
Module documentation for 3.3
singletonsth
singletonsth
defines Template Haskell functionality that allows
promotion of termlevel functions to typelevel equivalents and
singling functions to dependently typed equivalents. This library was
originally presented in
Dependently Typed Programming with Singletons,
published at the Haskell Symposium, 2012. See also
the paper published at Haskell Symposium, 2014,
which describes how promotion works in greater detail.
singletonsth
generates code that relies on bleedingedge GHC language
extensions. As such, singletonsth
only supports the latest major version
of GHC (currently GHC 9.8). For more information,
consult the singletons
README
.
You may also be interested in the following related libraries:
 The
singletons
library is a small, foundational library that defines basic singletonrelated types and definitions.  The
singletonsbase
library usessingletonsth
to define promoted and singled functions from thebase
library, including thePrelude
.
Changes
Changelog for the singletonsth
project
3.3 [2023.10.13]

Require building with GHC 9.8.

Singled data types with derived
Eq
orOrd
instances now generateEq
orOrd
instances for the singleton type itself, e.g.,instance Eq (SExample a) where _ == _ = True instance Ord (SExample a) where compare _ _ = EQ

singletonsth
now makes an effort to promote definitions that use scoped type variables. See the “Scoped type variables” section of theREADME
for more information about whatsingletonsth
can (and can’t) do. 
singletonsth
now supports singling typelevel definitions that useTypeAbstractions
. 
Fix a bug in which data types using visible dependent quantification would generate illscoped code when singled.

Fix a bug in which singling a local variable that shadows a toplevel definition would fail to typecheck in some circumstances.

Fix a bug in which
singletonsth
would incorrectly promote/single records to toplevel field selectors whenNoFieldSelectors
was active.
3.2 [2023.03.12]
 Require building with GHC 9.6.
 Derived
POrd
andSOrd
instances (arising from a use ofderiving Ord
) now use(<>) @Ordering
in their implementations instead of the customthenCmp :: Ordering > Ordering > Ordering
function. While most code will likely continue to work after this change, this may break code that attempts to prove properties about the implementation of a derivedPOrd
/SOrd
instance.  Fix a bug in which the
singDecideInstances
andshowSingInstances
, as well asderiving Show
declarations, would not respect custompromotedDataTypeOrConName
options.  Allow building with
mtl2.3.*
.
3.1.1 [2022.08.23]
 Require building with GHC 9.4.
 Improve error messages when attempting to promote a partial application of
a function arrow
(>)
, which is not currently supported.
3.1 [2021.10.30]
 Require building with GHC 9.2.
 Allow promoting and singling type applications in data constructor patterns.
 Make the Template Haskell machinery generate
SingI1
andSingI2
instances when possible.  Make
genDefunSymbols
and related functions less likely to trigger GHC#19743.
3.0 [2021.03.12]

The
singletons
library has been split into three libraries: The new
singletons
library is now a minimal library that only providesData.Singletons
,Data.Singletons.Decide
,Data.Singletons.Sigma
, andData.Singletons.ShowSing
(if compiled with GHC 8.6 or later).singletons
now supports building GHCs back to GHC 8.0, as well as GHCJS.  The
singletonsth
library defines Template Haskell functionality for promoting and singling termlevel definitions, but but nothing else. This library continues to require the latest stable release of GHC.  The
singletonsbase
library defines promoted and singled versions of definitions from thebase
library, including thePrelude
. This library continues to require the latest stable release of GHC.
Consult the changelogs for
singletons
andsingletonsbase
for changes specific to those libraries. For more information on this split, see the relevant GitHub discussion.  The new

Require building with GHC 9.0.

Data.Singletons.CustomStar
andData.Singletons.SuppressUnusedWarnings
have been renamed toData.Singletons.TH.CustomStar
andData.Singletons.SuppressUnusedWarnings
, respectively, to give every module insingletonsth
a consistent module prefix. 
Due to the
singletons
package split, thesingletonsth
modulesData.Singletons.TH
andData.Singletons.TH.CustomStar
(formerly known asData.Singletons.CustomStar
) no longer reexport any definitions from thesingletonsbase
modulePrelude.Singletons
(formerly known asData.Singletons.Prelude
). Thesingletonsbase
library now provides versions of these modules—Data.Singletons.Base.CustomStar
andData.Singletons.Base.TH
, respectively—that do reexport definitions fromPrelude.Singletons
. 
“Fully saturated” defunctionalization symbols (e.g.,
IdSym1
) are now defined as type families instead of type synonyms. This has two notable benefits: Fully saturated defunctionalization symbols can now be given standalone kind signatures, which ensures that the order of kind variables is the same as the user originally declared them.
 This fixes a minor regression in
singletons2.7
in which the quality of:kind!
output in GHCi would become worse when using promoted type families generated by Template Haskell.
Under certain circumstances, this can be a breaking change:

Since more THgenerated promoted functions now have type families on their righthand sides, some programs will now require
UndecidableInstances
where they didn’t before. 
Certain definitions that made use of overlapping patterns, such as
natMinus
below, will no longer typecheck:$(singletons [d data Nat = Z  S Nat natMinus :: Nat > Nat > Nat natMinus Z _ = Z natMinus (S a) (S b) = natMinus a b natMinus a Z = a ])
This can be worked around by avoiding the use of overlapping patterns. In the case of
natMinus
, this amounts to changing the third equation to match on its first argument:$(singletons [d natMinus :: Nat > Nat > Nat natMinus Z _ = Z natMinus (S a) (S b) = natMinus a b natMinus a@(S _) Z = a ])

The specification for how
singletons
deals with record selectors has been simplified. Previously,singletons
would try to avoid promoting socalled “naughty” selectors (those whose types mention existential type variables that do not appear in the constructor’s return type) to toplevel functions. Determing if a selector is naughty is quite challenging in practice, as determining if a type variable is existential or not in the context of Template Haskell is difficult in the general case. As a result,singletons
now adopts the dumbbutpredictable approach of always promoting record selectors to toplevel functions, naughty or not.This means that attempting to promote code with a naughty record selector, like in the example below, will no longer work:
$(promote [d data Some :: (Type > Type) > Type where MkSome :: { getSome :: f a } > Some f  getSome is naughty due to mentioning the type variable `a` ])
Please open an issue if you find this restriction burdensome in practice.

The
singEqInstanceOnly
andsingEqInstancesOnly
functions, which generateSEq
(but notPEq
) instances, have been removed. There is not much point in keeping these functions around now thatPEq
now longer has a special default implementation. UsesingEqInstance{s}
instead. 
The Template Haskell machinery will no longer promote
TypeRep
toType
, as this special case never worked properly in the first place. 
The Template Haskell machinery will now preserve strict fields in data types when generating their singled counterparts.

Introduce a new
promotedDataTypeOrConName
option toData.Singletons.TH.Options
. Overriding this option can be useful in situations where one wishes to promote types such asNat
,Symbol
, or data types built on top of them. See the “Arrows,Nat
,Symbol
, and literals” section of theREADME
for more information. 
Define a
Quote
instance forOptionsM
. A notable benefit of this instance is that it avoids the need to explicitlylift
TH quotes intoOptionsM
. Before, you would have to do this:import Control.Monad.Trans.Class (lift) withOptions defaultOptions $ singletons $ lift [d data T = MkT ]
But now, it suffices to simply do this:
withOptions defaultOptions $ singletons [d data T = MkT ]