singletons 2.7

Hackage Build Status

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 ([email protected]) and with significant contributions by Jan Stolarek ([email protected]) and Ryan Scott ([email protected]). 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 follow-up paper, Promoting Functions to Type Families in Haskell, is available here and will be referenced in this documentation as the “promotion paper”.

Ryan Scott ([email protected]) 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 term-level functions to type-level 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:

  • -Wno-redundant-constraints. The code that singletons generates uses redundant constraints, and there seems to be no way, without a large library redesign, to avoid this.
  • -fenable-th-splice-warnings. By default, GHC does not run pattern-match coverage checker warnings on code inside of Template Haskell quotes. This is an extremely common thing to do in singletons, 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 re-exports 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 top-level 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 in-depth 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 existentially-quantified 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 existentially-quantified singleton, wrapped up in a SomeSing. The Demote associated kind-indexed 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 the PEq class) and the (%==) method (in the SEq class). See the Data.Singletons.Prelude.Eq module for more information.

  • Propositional equality is implemented through the constraint (~), the type (:~:), and the class SDecide. See modules Data.Type.Equality and Data.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 Shows? 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 value-level 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 value-level Show instance for String. On the value level, showing Strings escapes special characters (such as double quotes), but implementing this requires pattern-matching on character literals, something which is currently impossible at the type level. As a consequence, the type-level Show instance for Symbols does not do any character escaping.

Errors

The singletons library provides two different ways to handle errors:

  • The Error type family, from Data.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 to Error "This is an error message" appears in error messages.

  • The TypeError type family, from Data.Singletons.TypeError. This is a drop-in replacement for TypeError from GHC.TypeLits which can be used at both the type level and the value level (via the typeError function).

    Unlike Error, TypeError will result in an actual compile-time error message, which may be more desirable depending on the use case.

Pre-defined 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 type-level equivalents of term-level 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 so-called 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 higher-order 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 type-level 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 higher-order 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 type-level 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 type-checking 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:

  1. original datatype: Nat

    promoted kind: Nat

    singleton type: SNat (which is really a synonym for Sing)

  2. original datatype: /\

    promoted kind: /\

    singleton type: %/\

  3. original constructor: Succ

    promoted type: 'Succ (you can use Succ when unambiguous)

    singleton constructor: SSucc

    symbols: SuccSym0, SuccSym1

  4. original constructor: :+:

    promoted type: ':+:

    singleton constructor: :%+:

    symbols: :+:@#@$, :+:@#@$$, :+:@#@$$$

  5. original value: pred

    promoted type: Pred

    singleton value: sPred

    symbols: PredSym0, PredSym1

  6. original value: +

    promoted type: +

    singleton value: %+

    symbols: +@#@$, +@#@$$, +@#@$$$

  7. original class: Num

    promoted class: PNum

    singleton class: SNum

  8. original class: ~>

    promoted class: #~>

    singleton class: %~>

Special names

There are some special cases, listed below (with asterisks* denoting special treatment):

  1. original datatype: []

    promoted kind: []

    singleton type*: SList

  2. original constructor: []

    promoted type: '[]

    singleton constructor*: SNil

    symbols*: NilSym0

  3. original constructor: :

    promoted type: ':

    singleton constructor*: SCons

    symbols: :@#@$, :@#@$$, :@#@$$$

  4. original datatype: (,)

    promoted kind: (,)

    singleton type*: STuple2

  5. original constructor: (,)

    promoted type: '(,)

    singleton constructor*: STuple2

    symbols*: Tuple2Sym0, Tuple2Sym1, Tuple2Sym2

    All tuples (including the 0-tuple, unit) are treated similarly.

  6. 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, and case)
  • literals (for Nat and Symbol), 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 top-level functions, as there is no record syntax at the type level. Record selectors are also singled to top-level functions because embedding records directly into singleton data constructors can result in surprising behavior (see this bug report for more details on this point). TH-generated 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 aliases a. However, the same trick does not work when h is promoted to a type family, as a type family would consider a and b to be distinct type variables.

  • i :: Bool -> Bool
    i (x :: a) = x
    

    This typechecks by virtue of the fact that a aliases Bool. Again, this would not work at the type level, as a type family would consider a to be a separate type from Bool.

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 poly-kinded 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 catch-all guard, which is always true and thus overlaps with pred x guard.

Another non-obvious 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 catch-all 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 poly-kinded type classes

Singling instances of poly-kinded 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, or Symbol
  • rank-n types
  • promoting TypeReps
  • 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:

  1. Use pattern signatures:

    g :: forall a. a -> a
    g (x :: a) = id (x :: a)
    
  2. 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 built-in 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, term-level 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.

Rank-n types

singletons does not support type signatures that have higher-rank types. More precisely, the only types that can be promoted or singled are vanilla types, where a vanilla function type is a type that:

  1. Only uses a forall at the top level, if used at all. That is to say, it does not contain any nested or higher-rank foralls.

  2. Only uses a context (e.g., c => ...) at the top level, if used at all, and only after the top-level forall if one is present. That is to say, it does not contain any nested or higher-rank contexts.

  3. Contains no visible dependent quantification.

Promoting TypeReps

The built-in 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:

  1. The module Data.Singletons.TypeRepTYPE has all the definitions possible for making * the promoted version of TypeRep, as TypeRep is currently implemented. The singleton associated with TypeRep has one constructor:

    type instance Sing @(TYPE rep) = TypeRep
    

    (Recall that type * = TYPE LiftedRep.) Note that any datatypes that store TypeReps will not generally work as expected; the built-in promotion mechanism will not promote TypeRep to *.

  2. The module Data.Singletons.CustomStar allows the programmer to define a subset of types with which to work. See the Haddock documentation for the function singletonStar 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 top-level functions
  • Type signatures of singled top-level 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:

    1. The thing being defunctionalized has a standalone type (or kind) signature.
    2. The type (or kind) signature of the thing being defunctionalized is a vanilla type. (See the “Rank-n 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 is forall a. a -> forall b. b -> Type, which is not vanilla. Currently, singletons will generate the following defunctionalization symbols for T:

    data TSym0 :: a ~> b ~> Type
    data TSym1 (x :: a) :: b ~> Type
    

    In both symbols, the kind starts with forall a b. rather than quantifying the b after the visible argument of kind a. These symbols can still be useful even with this flaw, so singletons 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 is forall b. C b => forall a. a -> b -> a, which binds b before a. This order is preserved when singling m, but not when promoting m. This is because the C class is promoted as follows:

    class PC (b :: Type) where
      type M (x :: a) (y :: b) :: a
    

    Due to the way GHC kind-checks associated type families, the kind of M is forall a b. a -> b -> a, which binds b after a. Moreover, the StandaloneKindSignatures 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
    

Changes

Changelog for singletons project

2.7

  • Require GHC 8.10.

  • Record selectors are now singled as top-level functions. For instance, $(singletons [d| data T = MkT { unT :: Bool } |]) will now generate this:

    data ST :: T -> Type where
      SMkT :: Sing b -> Sing (MkT b)
    
    sUnT :: Sing (t :: T) -> Sing (UnT t :: Bool)
    sUnT (SMkT sb) = sb
    
    ...
    

    Instead of this:

    data ST :: T -> Type where
      SMkT :: { sUnT :: Sing b } -> Sing (MkT b)
    

    Note that the new type of sUnT is more general than the previous type (Sing (MkT b) -> Sing b).

    There are two primary reasons for this change:

    1. Singling record selectors as top-level functions is consistent with how promoting records works (note that MkT is also a top-level function). As
    2. Embedding record selectors directly into a singleton data constructor can result in surprising behavior. This can range from simple code using a record selector not typechecking to the inability to define multiple constructors that share the same record name.

    See this GitHub issue for an extended discussion on the motivation behind this change.

  • The Template Haskell machinery now supports fine-grained configuration in the way of an Options data type, which lives in the new Data.Singletons.TH.Options module. Besides Options, this module also contains:

    • Options’ record selectors. Currently, these include options to toggle generating quoted declarations, toggle generating SingKind instances, and configure how singletons generates the names of promoted or singled types. In the future, there may be additional options.
    • A defaultOptions value.
    • An mtl-like OptionsMonad class for monads that support carrying Options. This includes Q, which uses defaultOptions if it is the top of the monad transformer stack.
    • An OptionM monad transformer that turns any DsMonad into an OptionsMonad.
    • A withOptions function which allows passing Options to TH functions (e.g., promote or singletons). See the README for a full example of how to use withOptions. Most TH functions are now polymorphic over OptionsMonad instead of DsMonad.
  • singletons now does a much better job of preserving the order of type variables in type signatures during promotion and singling. See the Support for TypeApplications section of the README for more details.

    When generating type-level declarations in particular (e.g., promoted type families or defunctionalization symbols), singletons will likely also generate standalone kind signatures to preserve type variable order. As a result, most singletons code that uses Template Haskell will require the use of the StandaloneKindSignatures extension (and, by extension, the NoCUSKs extension) to work.

  • singletons now does a more much thorough job of rejecting higher-rank types during promotion or singling, as singletons cannot support them. (Previously, singletons would sometimes accept them, often changing rank-2 types to rank-1 types incorrectly in the process.)

  • Add the Data.Singletons.Prelude.Proxy module.

  • Remove the promoted versions of genericTake, genericDrop, genericSplitAt, genericIndex, and genericReplicate from Data.Singletons.Prelude.List. These definitions were subtly wrong since (1) they claim to work over any Integral type i, but in practice would only work on Nats, and (2) wouldn’t even typecheck if they were singled.

  • Export ApplyTyConAux1, ApplyTyConAux2, as well as the record pattern synonyms selector applySing2, applySing3, etc. from Data.Singletons. These were unintentionally left out in previous releases.

  • Export promoted and singled versions of the getDown record selector in Data.Singletons.Prelude.Ord.

  • Fix a slew of bugs related to fixity declarations:

    • Fixity declarations for data types are no longer singled, as fixity declarations do not serve any purpose for singled data type constructors, which always have exactly one argument.
    • singletons now promotes fixity declarations for class names. genPromotions/genSingletons now also handle fixity declarations for classes, class methods, data types, and record selectors correctly.
    • singletons will no longer erroneously try to single fixity declarations for type synonym or type family names.
    • A bug that caused fixity declarations for certain defunctionalization symbols not to be generated has been fixed.
    • promoteOnly and singletonsOnly will now produce fixity declarations for values with infix names.

2.6

  • Require GHC 8.8.

  • Sing has switched from a data family to a type family. This GitHub issue comment provides a detailed explanation for the motivation behind this change.

    This has a number of consequences:

    • Names like SBool, SMaybe, etc. are no longer type synonyms for particular instantiations of Sing but are instead the names of the singleton data types themselves. In other words, previous versions of singletons would provide this:

      data instance Sing :: Bool -> Type where
        SFalse :: Sing False
        STrue  :: Sing True
      type SBool = (Sing :: Bool -> Type)
      

      Whereas with Sing-as-a-type-family, singletons now provides this:

      data SBool :: Bool -> Type where
        SFalse :: SBool False
        STrue  :: SBool True
      type instance Sing @Bool = SBool
      
    • The Sing instance for TYPE rep in Data.Singletons.TypeRepTYPE is now directly defined as type 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 with Sing-as-a-type-family. One notable consequence of this is that Show 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 for ShowSing' in Data.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, a WrappedSing data type (which is a newtype around Sing) was introduced so that one can hang instances off of it.

      This had one noticeable effect in singletons itself: there are no longer TestEquality Sing or TestCoercion Sing instances. Instead, singletons now generates a separate TestEquality/TestCoercion instance for every data type that singles a derived Eq instance. In addition, the Data.Singletons.Decide module now provides top-level decideEquality/decideCoercion functions which provide the behavior of testEquality/testCoercion, but monomorphized to Sing. Finally, TestEquality/TestCoercion instances are provided for WrappedSing.

  • 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 on singletons’ 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 kind-generalizes sLoop (whereas it did not previously), explaining why the error message mentions a mysterious kind variable k1 that only appeared after kind generalization. The solution is to give loop 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 the TypeApplications extension. (The generated code was always using TypeApplications under the hood, but it’s only now that GHC is detecting it.)

  • Data.Singletons now defines a family of SingI instances for TyCon1 through TyCon8:

    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 for SingI instances for applications of TyCon{N} to particular type constructors, as they have been superseded by the instances above.

  • Changes to Data.Singletons.Sigma:

    • SSigma, the singleton type for Sigma, is now defined.

    • New functions fstSigma, sndSigma, FstSigma, SndSigma, currySigma, and uncurrySigma have been added. A Show instance for Sigma has also been added.

    • projSigma1 has been redefined to use continuation-passing style to more closely resemble its cousin projSigma2. The new type signature of projSigma1 is:

      projSigma1 :: (forall (fst :: s). Sing fst -> r) -> Sigma s t -> r
      

      The old type signature of projSigma1 can be found in the fstSigma function.

    • Σ has been redefined such that it is now a partial application of Sigma, 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 base-4.13, the Fail/sFail methods of {P,S}Monad have been removed in favor of new {P,S}MonadFail classes introduced in the Data.Singletons.Prelude.Monad.Fail module. These classes are also re-exported from Data.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 for SomeSing now uses more efficient implementations of enumFromTo and enumFromThenTo that no longer require a SingKind constraint.

2.5.1

  • ShowSing is now a type class (with a single instance) instead of a type synonym. This was changed because defining ShowSing 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 for SomeSing.

2.5

  • The Data.Promotion.Prelude.* namespace has been removed. Use the corresponding modules in the Data.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 in PEq 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 that a == a reduces to True for any a. (As a result, the previous version of singletons regressed in terms of type inference for the PEq instances for Nat and Symbol, which used that default.) On the other hand, DefaultEq a a does reduce to True for all a.

  • Add Enum Nat, Show Nat, and Show Symbol instances to Data.Singletons.TypeLits.

  • Template Haskell-generated code may require DataKinds and PolyKinds in scenarios which did not previously require it:

    • singletons now explicitly quantifies all kind variables used in explicit foralls.
    • singletons now generates a ~> b instead of TyFun a b -> Type whenever possible.
  • Since th-desugar now desugars all data types to GADT syntax, Template Haskell-generated code may require GADTs in situations that didn’t require it before.

  • Overhaul the way derived Show instances for singleton types works. Before, there was an awkward ShowSing class (which was essentially a cargo-culted version of Show specialized for Sing) that one had to create instances for separately. Now that GHC has QuantifiedConstraints, we can scrap this whole class and turn ShowSing into a simple type synonym:

    type ShowSing k = forall z. Show (Sing (z :: k))
    

    Now, instead of generating a hand-written ShowSing and Show instance for each singleton type, we only generate a single (derived!) Show instance. As a result of this change, you will likely need to enable QuantifiedConstraints and StandaloneDeriving if you single any derived Show instances in your code.

  • The kind of the type parameter to SingI is no longer specified. This only affects you if you were using the sing method with TypeApplications. For instance, if you were using sing @Bool @True before, then you will now need to now use sing @Bool instead.

  • singletons now generates SingI instances for defunctionalization symbols through Template Haskell. As a result, you may need to enable FlexibleInstances 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 to Data.Singletons.TypeRepTYPE, and generalize the Sing :: Type -> Type instance to Sing :: TYPE rep -> Type, allowing it to work over more open kinds. Also rename SomeTypeRepStar to SomeTypeRepTYPE, 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 (<=?) from GHC.TypeNats, as well as defunctionalization symbols for (<=?), to Data.Singletons.TypeLits.

  • Add Data.Singletons.Prelude.{Semigroup,Monoid}, which define promoted and singled versions of the Semigroup and Monoid type classes, as well as various newtype modifiers.

    Symbol is now has promoted Semigroup and Monoid instances as well. As a consequence, Data.Singletons.TypeLits no longer exports (<>) or (%<>), as they are superseded by the corresponding methods from PSemigroup and SSemigroup.

  • Add promoted and singled versions of the Functor, Foldable, Traversable, Applicative, Alternative, Monad, MonadPlus, and MonadZip classes. Among other things, this grants the ability to promote or single do-notation and list comprehensions.

    • Data.Singletons.Prelude.List now reexports more general Foldable/Traversable functions wherever possible, just as Data.List does.
  • Add Data.Singletons.Prelude.{Const,Identity}, which define promoted and singled version of the Const and Identity data types, respectively.

  • Promote and single the Down newtype in Data.Singletons.Prelude.Ord.

  • To match the base library, the promoted/singled versions of comparing and thenCmp are no longer exported from Data.Singletons.Prelude. (They continue to live in Data.Singletons.Prelude.Ord.)

  • Permit singling of expression and pattern signatures.

  • Permit promotion and singling of InstanceSigs.

  • sError and sUndefined now have HasCallStack constraints, like their counterparts error and undefined. The promoted and singled counterparts to errorWithoutStackTrace have also been added in case you do not want this behavior.

  • Add Data.Singletons.TypeError, which provides a drop-in replacement for GHC.TypeLits.TypeError which can be used at both the value- and type-level.

2.4.1

  • Restore the TyCon1, TyCon2, etc. types. It turns out that the new TyCon doesn’t work with kind-polymorphic tycons.

2.4

  • Require GHC 8.4.

  • Demote Nat is now Natural (from Numeric.Natural) instead of Integer. In accordance with this change, Data.Singletons.TypeLits now exposes GHC.TypeNats.natVal (which returns a Natural) instead of GHC.TypeLits.natVal (which returns an Integer).

  • 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 of undefined would be promoted to GHC.Exts.Any and singled to undefined. Now, there is a proper Undefined type family and sUndefined singleton function.

  • As a consequence of not promoting undefined to Any, there is no need to have a special any_ function to distinguish the function on lists. The corresponding promoted type, singleton function, and defunctionalization symbols are now named Any, sAny, and AnySym{0,1,2}.

  • Rework the treatment of empty data types:

    • Generated SingKind instances for empty data types now use EmptyCase instead of simply erroring.
    • Derived PEq instances for empty data types now return True instead of False. Derived SEq instances now return True instead of erroring.
    • Derived SDecide instances for empty data types now return Proved bottom, where bottom is a divergent computation, instead of erroring.
  • Add Data.Singletons.Prelude.IsString and Data.Promotion.Prelude.IsString modules. IsString.fromString is now used when promoting or singling string literals when the -XOverloadedStrings extension is enabled (similarly to how Num.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, and quotRem to Data.Singletons.TypeLits that utilize the efficient Div and Mod type families from GHC.TypeNats. Also add sLog2 and defunctionalization symbols for Log2 from GHC.TypeNats.

  • Add (<>) and (%<>), the promoted and singled versions of AppendSymbol from GHC.TypeLits.

  • Add (%^), the singleton version of GHC.TypeLits.^.

  • Add unlines and unwords to Data.Singletons.Prelude.List.

  • Add promoted and singled versions of Show, including deriving support.

  • Add a ShowSing class, which facilitates the ability to write Show instances for Sing instances.

  • Permit derived Ord instances for empty datatypes.

  • Permit standalone deriving declarations.

  • Permit DeriveAnyClass (through the anyclass keyword of DerivingStrategies)

  • Add a value-level (@@), which is a synonym for applySing.

  • Add Eq, Ord, Num, Enum, and Bounded instances for SomeSing, which leverage the SEq, SOrd, SNum, SEnum, and SBounded instances, respectively, for the underlying Sing.

  • Rework the Sing (a :: *) instance in Data.Singletons.TypeRepStar such that it now uses type-indexed Typeable. The new Sing 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 on TypeReps whose kind is of kind *. The previous implementation did not enforce this, which could lead to segfaults if used carelessly.

  • Instead of erroring, the toSing implementation in the SingKind (k1 ~> k2) instance now works as one would expect (provided the user adheres to some common-sense SingKind laws, which are now documented).

  • Add a demote function, which is a convenient shorthand for fromSing sing.

  • Add a Data.Singletons.Sigma module with a Sigma (dependent pair) data type.

  • Export defunctionalization symbols for Demote, SameKind, KindOf, (~>), Apply, and (@@)fromData.Singletons`.

  • Add an explicitly bidirectional pattern synonym Sing. Pattern matching on Sing brings a SingI ty constraint into scope from a singleton Sing 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 term-level Haskell function on singletons.

  • Remove the family of TyCon1, TyCon2, …, in favor of just TyCon. GHC 8.4’s type system is powerful enough to allow this nice simplification.

2.3

  • Documentation clarifiation in Data.Singletons.TypeLits, thanks to @ivan-m.

  • Demote was no longer a convenient way of calling DemoteRep and has been removed. DemoteRep has been renamed Demote.

  • DemoteRep is now injective.

  • Demoting a Symbol now gives Text. This is motivated by making DemoteRep injective. (If Symbol demoted to String, then there would be a conflict between demoting [Char] and Symbol.)

  • Generating singletons also now generates fixity declarations for the singletonized definitions, thanks to @int-index.

  • Though more an implementation detail: singletons no longer uses kind-level proxies anywhere, thanks again to @int-index.

  • Support for promoting higher-kinded type variables, thanks for @int-index.

  • Data.Singletons.TypeLits now exports defunctionalization symbols for KnownNat and KnownSymbol.

  • Better type inference support around constraints, as tracked in Issue #176.

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

  • Show instances for SNat and SSymbol, thanks to @cumber.

  • The singFun and unSingFun functions no longer use proxies, preferring TypeApplications.

2.2

  • With TypeInType, we no longer kind KProxy. @int-index has very helpfully removed the use of KProxy from singletons.

  • 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 th-desugar >= 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 as Bounded.

  • Deriving Enum is also now supported.

  • Ditto for Num, which includes an instance for Nat, naturally.

  • Promoting a literal number now uses overloaded literals at the type level, using a type-level FromInteger in the type-level Num class.

  • Better support for dealing with constraints. Some previously-unsingletonizable 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 locally-declared 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 th-desugar-1.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 th-desugar-1.5. Some types changed (using th-desugar’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, partially-applied functions, and anonymous functions, where, sections, among others.

  • Classes and instances can be promoted (but not singletonized).

  • Derivation of promoted instances for Ord and Bounded.

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