singletons: A framework for generating singleton types
This library generates singleton types, promoted functions, and singleton functions using Template Haskell. It is useful for programmers who wish to use dependently typed programming techniques. The library was originally presented in Dependently Typed Programming with Singletons, published at the Haskell Symposium, 2012. (https://cs.brynmawr.edu/~rae/papers/2012/singletons/paper.pdf)
Version 1.0 and onwards works a lot harder to promote functions. See the paper published at Haskell Symposium, 2014: https://cs.brynmawr.edu/~rae/papers/2014/promotion/promotion.pdf.
[Skip to Readme]
Versions [faq]  0.8, 0.8.1, 0.8.2, 0.8.3, 0.8.4, 0.8.5, 0.8.6, 0.9.0, 0.9.1, 0.9.2, 0.9.3, 0.10.0, 1.0, 1.1, 1.1.1, 1.1.2, 1.1.2.1, 2.0, 2.0.0.1, 2.0.0.2, 2.0.1, 2.1, 2.2, 2.3, 2.3.1, 2.4, 2.4.1, 2.5, 2.5.1, 2.6, 2.7 

Change log  CHANGES.md 
Dependencies  base (==4.14.*), containers (>=0.5), ghcbootth, mtl (>=2.2.1), pretty, syb (>=0.4), templatehaskell, text (>=1.2), thdesugar (==1.11.*), transformers (>=0.5.2) [details] 
License  BSD3Clause 
Author  Richard Eisenberg <rae@cs.brynmawr.edu>, Jan Stolarek <jan.stolarek@p.lodz.pl> 
Maintainer  Ryan Scott <ryan.gl.scott@gmail.com> 
Revised  Revision 1 made by ryanglscott at 20200326T15:56:54Z 
Category  Dependent Types 
Home page  http://www.github.com/goldfirere/singletons 
Bug tracker  https://github.com/goldfirere/singletons/issues 
Source repo  this: git clone https://github.com/goldfirere/singletons.git(tag v2.7) head: git clone https://github.com/goldfirere/singletons.git b master 
Uploaded  by ryanglscott at 20200325T15:33:33Z 
Distributions  Arch:2.7, Debian:2.4.1, LTSHaskell:2.5.1, NixOS:2.7, Stackage:2.5.1 
Downloads  36972 total (718 in the last 30 days) 
Rating  2.75 (votes: 9) [estimated by Bayesian average] 
Your Rating 

Status  Docs uploaded by user [build log] All reported builds failed as of 20200325 [all 3 reports] 
Modules
[Index] [Quick Jump]
 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.Proxy
 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
Downloads
 singletons2.7.tar.gz [browse] (Cabal source package)
 Package description (revised from the package)
Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.
Readme for singletons2.7
[back to package description]singletons 2.7
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) and
Ryan Scott (ryan.gl.scott@gmail.com). 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 the 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 and singling functions to dependently typed equivalents.
Accordingly, it exports a Prelude of promoted and singled
functions, mirroring functions and datatypes found in the 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.10.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
NoCUSKs
NoStarIsType
PolyKinds
RankNTypes
ScopedTypeVariables
StandaloneKindSignatures
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 to consider toggling various warning flags:
Wnoredundantconstraints
. The code thatsingletons
generates uses redundant constraints, and there seems to be no way, without a large library redesign, to avoid this.fenablethsplicewarnings
. By default, GHC does not run patternmatch coverage checker warnings on code inside of Template Haskell quotes. This is an extremely common thing to do insingletons
, so you may consider opting in to these warnings.
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 promoted and
singled equivalents of functions from the real Prelude
.
Note that not all functions from original Prelude
could be promoted or
singled.
Data.Singletons.Prelude.*
modules provide promoted and singled equivalents of
definitions found in several commonly used base
library modules, including
(but not limited to) Data.Bool
, Data.Maybe
, Data.Either
, Data.List
,
Data.Tuple
, Data.Void
and GHC.Base
. We also provide promoted and singled
versions of common type classes, including (but not limited to) Eq
, Ord
,
Show
, Enum
, and Bounded
.
Data.Singletons.Decide
exports type classes for propositional equality.
Data.Singletons.TypeLits
exports definitions for working with GHC.TypeLits
.
Functions to generate singletons
The toplevel functions used to generate promoted or singled definitions 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]
This function 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 Sing :: k > Type
type family Sing
The type family of singleton types. A new instance of this type family is generated for every new singleton type.
class SingI a where
sing :: Sing a
A class used to pass singleton values implicitly. The sing
method produces
an explicit singleton value.
type SomeSing :: Type > Type
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
.
type SingKind :: Type > Constraint
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
.
type SingInstance :: k > Type
data SingInstance a 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
(==)
(in thePEq
class) and the(%==
) method (in theSEq
class). 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 :: Type > Constraint
type ShowSing k = (forall z. Show (Sing (z :: k))  Approximately
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 Error :: a > k type family Error str 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. These include (but are not limited to):
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 the "Supported Haskell constructs" section of this README for a full list.
Promoted definitions are usually generated by calling the 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 defunctionalization symbols. These are required to represent partial application at the type level. For more information, refer to the "Promotion and partial application" section below.
Users also have access to Data.Singletons.Prelude
and its submodules (e.g.,
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.
Promotion and partial application
Promoting higherorder functions proves to be surprisingly tricky. Consider this example:
$(promote [d
map :: (a > b) > [a] > [b]
map _ [] = []
map f (x:xs) = f x : map f xs
])
A naïve attempt to promote map
would be:
type Map :: (a > b) > [a] > [b]
type family Map f xs where
Map _ '[] = '[]
Map f (x:xs) = f x : Map f xs
While this compiles, it is much less useful than we would like. In particular,
common idioms like Map Id xs
will not typecheck, since GHC requires that all
invocations of type families be fully saturated. That is, the use of Id
in
Map Id xs
is rejected since it is not applied to one argument, which the
number of arguments that Id
was defined with. For more information on this
point, refer to the promotion paper.
Not having the ability to partially apply functions at the type level is rather
painful, so we do the next best thing: we defunctionalize all promoted
functions so that we can emulate partial application. For example, if one were
to promote the id
function:
$(promote [d
id :: a > a
id x = x
]
Then in addition to generating the promoted Id
type family, two
defunctionalization symbols will be generated:
type IdSym0 :: a ~> a
type IdSym0 x = x
type IdSym1 (x :: a) = Id a
In general, a function that accepts N arguments generates N+1 defunctionalization symbols when promoted.
IdSym1
is a fully saturated defunctionalization symbol and is usually only
needed when generating code through the Template Haskell machinery. IdSym0
is more interesting: it has the kind a ~> a
, which has a special arrow type
(~>)
. Defunctionalization symbols using the (~>)
kind are typelevel
constants that can be "applied" using a special Apply
type family:
type Apply :: (a ~> b) > a > b
type family Apply f x
Every defunctionalization symbol comes with a corresponding Apply
instance
(except for fully saturated defunctionalization symbols). For instance, here
is the Apply
instance for IdSym0
:
type instance Apply IdSym0 x = IdSym1 x
The (~>)
kind is used when promoting higherorder functions so that partially
applied arguments can be passed to them. For instance, here is our final attempt
at promoting map
:
type Map :: (a ~> b) > [a] > [b]
type family Map f xs where
Map _ '[] = '[]
Map f (x:xs) = Apply f x : Map f xs
Now map id xs
can be promoted to Map IdSym0 xs
, which typechecks without issue.
Defunctionalizing existing type families
The most common way to defunctionalize functions is by promoting them with the
Template Haskell machinery. One can also defunctionalize existing type families,
however, by using genDefunSymbols
. For example:
type MyTypeFamily :: Nat > Bool
type family MyTypeFamily n
$(genDefunSymbols [''MyTypeFamily])
This can be especially useful if MyTypeFamily
needs to be implemented by
hand. Be aware of the following design limitations of genDefunSymbols
:
genDefunSymbols
only works for typelevel declarations. Namely, it only works when given the names of type classes, type families, type synonyms, or data types. Attempting to pass the name of a term level function, class method, data constructor, or record selector will throw an error. Passing the name of a data type to
genDefunSymbols
will cause its data constructors to be defunctionalized but not its record selectors.  Passing the name of a type class to
genDefunSymbols
will cause the class itself to be defunctionalized, but /not/ its associated type families or methods.
Note that the limitations above reflect the current design of
genDefunSymbols
. As a result, they are subject to change in the future.
Defunctionalization and visible dependent quantification
Unlike most other parts of singletons
, which disallow visible dependent
quantification (VDQ), genDefunSymbols
has limited support for VDQ.
Consider this example:
type MyProxy :: forall (k :: Type) > k > Type
type family MyProxy k (a :: k) :: Type where
MyProxy k (a :: k) = Proxy a
$(genDefunSymbols [''MyProxy])
This will generate the following defunctionalization symbols:
type MyProxySym0 :: Type ~> k ~> Type
type MyProxySym1 :: forall (k :: Type) > k ~> Type
type MyProxySym2 k (a :: k) = MyProxy k a
Note that MyProxySym0
is a bit more general than it ought to be, since
there is no dependency between the first kind (Type
) and the second kind
(k
). But this would require the ability to write something like this:
type MyProxySym0 :: forall (k :: Type) ~> k ~> Type
This currently isn't possible. So for the time being, the kind of
MyProxySym0
will be slightly more general, which means that under rare
circumstances, you may have to provide extra type signatures if you write
code which exploits the dependency in MyProxy
's kind.
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 singled 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.
If desired, you can pick your own naming conventions by using the
Data.Singletons.TH.Options
module. Here is an example of how this module can
be used to prefix a singled data constructor with MyS
instead of S
:
import Control.Monad.Trans.Class
import Data.Singletons.TH
import Data.Singletons.TH.Options
import Language.Haskell.TH (Name, mkName, nameBase)
$(let myPrefix :: Name > Name
myPrefix name = mkName ("MyS" ++ nameBase name) in
withOptions defaultOptions{singledDataConName = myPrefix} $
singletons $ lift [d data T = MkT ])
Supported Haskell constructs
Full support
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
 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)
 pattern guards
 case
 let
 lambda expressions
!
and~
patterns (silently but successfully ignored during promotion) class and instance declarations
 signatures (e.g.,
(x :: Maybe a)
) in expressions InstanceSigs
Partial support
The following constructs are partially supported:
deriving
 finite arithmetic sequences
 records
 signatures (e.g.,
(x :: Maybe a)
) in patterns  functional dependencies
 type families
See the following sections for more details.
deriving
singletons
is slightly more conservative with respect to deriving
than GHC is.
The only classes that singletons
can derive without an explicit deriving
strategy are the following stock classes:
Eq
Ord
Show
Bounded
Enum
Functor
Foldable
Traversable
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
or via
strategies,
as there is no equivalent of coerce
at the type level.
Finite arithmetic sequences
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.
Records
Record selectors are promoted to toplevel functions, as there is no record
syntax at the type level. Record selectors are also singled to toplevel
functions because embedding records directly into singleton data constructors
can result in surprising behavior (see
this bug report for more
details on this point). THgenerated code is not affected by this limitation
since singletons
desugars away most uses of record syntax. On the other hand,
it is not possible to write out code like
SIdentity { sRunIdentity = SIdentity STrue }
by hand.
Signatures in patterns
singletons
can promote basic pattern signatures, such as in the following
examples:
f :: forall a. a > a
f (x :: a) = (x :: a)
g :: forall a. a > a
g (x :: b) = (x :: b)  b is the same as a
What does /not/ work are more advanced uses of pattern signatures that take advantage of the fact that type variables in pattern signatures can alias other types. Here are some examples of functions that one cannot promote:
h :: a > a > a h (x :: a) (_ :: b) = x
This typechecks by virtue of the fact that
b
aliasesa
. However, the same trick does not work whenh
is promoted to a type family, as a type family would considera
andb
to be distinct type variables.i :: Bool > Bool i (x :: a) = x
This typechecks by virtue of the fact that
a
aliasesBool
. Again, this would not work at the type level, as a type family would considera
to be a separate type fromBool
.
Functional dependencies
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.
Type families
Promoting functions with types that contain type families is likely to fail due to GHC#12564. Note that promoting type family declarations is fine (and often desired, since that produces defunctionalization symbols for them).
Support for promotion, but not singling
The following constructs are supported for promotion but not singleton generation:
 data constructors with contexts
 overlapping patterns
GADTs
 instances of polykinded type classes
See the following sections for more details.
Data constructors with contexts
For example, the following datatype does not single:
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 for SingKind
(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 single 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 with pred 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.
GADTs
Singling GADTs is likely to fail due to the generated SingKind
instances
not typechecking. (See
#150).
However, one can often work around the issue by suppressing the generation
of SingKind
instances by using custom Options
. See the T150
test case
for an example.
Instances of polykinded type classes
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 the C []
is sufficient
to work around the issue, though:
instance C [] where
method :: [a]
method = []
Little to no support
The following constructs are either unsupported or almost never work:
 scoped type variables
 datatypes that store arrows,
Nat
, orSymbol
 rankn types
 promoting
TypeRep
s TypeApplications
See the following sections for more details.
Scoped type variables
Promoting functions that rely on the behavior of ScopedTypeVariables
is very
tricky—see
this GitHub issue for an
extended discussion on the topic. This is not to say that promoting functions
that rely on ScopedTypeVariables
is guaranteed to fail, but it is rather
fragile. To demonstrate how fragile this is, note that the following function
will promote successfully:
f :: forall a. a > a
f x = id x :: a
But this one will not:
g :: forall a. a > a
g x = id (x :: a)
There are usually workarounds one can use instead of ScopedTypeVariables
:
Use pattern signatures:
g :: forall a. a > a g (x :: a) = id (x :: a)
Use local definitions:
g :: forall a. a > a g x = id' a where id' :: a > a id' x = x
Arrows, Nat
, Symbol
, and literals
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. Functions
working over 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.
Rankn types
singletons
does not support type signatures that have higherrank types.
More precisely, the only types that can be promoted or singled are
vanilla types, where a vanilla function type is a type that:
Only uses a
forall
at the top level, if used at all. That is to say, it does not contain any nested or higherrankforall
s.Only uses a context (e.g.,
c => ...
) at the top level, if used at all, and only after the toplevelforall
if one is present. That is to say, it does not contain any nested or higherrank contexts.Contains no visible dependent quantification.
Promoting TypeRep
s
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.
TypeApplications
singletons
currently cannot handle promoting or singling code that uses
TypeApplications
syntax, so singletons
will simply drop any visible type
applications. For example, id @Bool True
will be promoted to Id True
and
singled to sId STrue
. See
#378 for a discussion
of how singletons
may support TypeApplications
in the future.
On the other hand, singletons
does make an effort to preserve the order of
type variables when promoting and singling certain constructors. These include:
 Kind signatures of promoted toplevel functions
 Type signatures of singled toplevel functions
 Kind signatures of singled data type declarations
 Type signatures of singled data constructors
 Kind signatures of singled class declarations
 Type signatures of singled class methods
For example, consider this type signature:
const2 :: forall b a. a > b > a
The promoted version of const
will have the following kind signature:
type Const2 :: forall b a. a > b > a
The singled version of const2
will have the following type signature:
sConst2 :: forall b a (x :: a) (y :: a). Sing x > Sing y > Sing (Const x y)
Therefore, writing const2 @T1 @T2
works just as well as writing
Const2 @T1 @T2
or sConst2 @T1 @T2
, since the signatures for const2
, Const2
,
and sConst2
all begin with forall b a.
, in that order. Again, it is worth
emphasizing that the TH machinery does not support promoting or singling
const2 @T1 @T2
directly, but you can write the type applications by hand if
you so choose.
singletons
also has limited support for preserving the order of type variables
for the following constructs:
Kind signatures of defunctionalization symbols. The order of type variables is only guaranteed to be preserved if:
 The thing being defunctionalized has a standalone type (or kind) signature.
 The type (or kind) signature of the thing being defunctionalized is a vanilla type. (See the "Rankn types" section above for what "vanilla" means.)
If either of these conditions do not hold,
singletons
will fall back to a slightly different approach to generating defunctionalization symbols that does not guarantee the order of type variables. As an example, consider the following example:data T (x :: a) :: forall b. b > Type $(genDefunSymbols [''T])
The kind of
T
isforall a. a > forall b. b > Type
, which is not vanilla. Currently,singletons
will generate the following defunctionalization symbols forT
:data TSym0 :: a ~> b ~> Type data TSym1 (x :: a) :: b ~> Type
In both symbols, the kind starts with
forall a b.
rather than quantifying theb
after the visible argument of kinda
. These symbols can still be useful even with this flaw, sosingletons
permits generating them regardless. Be aware of this drawback if you try doing something similar yourself!Kind signatures of promoted class methods. The order of type variables will often "just work" by happy coincidence, but there are some situations where this does not happen. Consider the following class:
class C (b :: Type) where m :: forall a. a > b > a
The full type of
m
isforall b. C b => forall a. a > b > a
, which bindsb
beforea
. This order is preserved when singlingm
, but not when promotingm
. This is because theC
class is promoted as follows:class PC (b :: Type) where type M (x :: a) (y :: b) :: a
Due to the way GHC kindchecks associated type families, the kind of
M
isforall a b. a > b > a
, which bindsb
aftera
. Moreover, theStandaloneKindSignatures
extension does not provide a way to explicitly declare the full kind of an associated type family, so this limitation is not easy to work around.The defunctionalization symbols for
M
will also follow a similar order of type variables:type MSym0 :: forall a b. a ~> b ~> a type MSym1 :: forall a b. a > b ~> a