Make Sing a type family

This fixes #318 by switching `Sing` from a data family to a type
family. There are several knock-on changes as a result of this
switch—refer to `CHANGES.md` for an overview.

CHANGES.md

@@ -4,6 +4,50 @@ Changelog for singletons project
 2.6
 ---
 * Require GHC 8.8.
+* `Sing` has switched from a data family to a type family. This has a number of
+  consequences:
+  * Names like `SBool`, `SMaybe`, etc. are no longer type synonyms for
+    particular instantiations of `Sing` but are instead the names of the
+    singleton data types themselves. In other words, previous versions of
+    `singletons` would provide this:
+
+    ```haskell
+    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:
+
+    ```haskell
+    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](https://gitlab.haskell.org/ghc/ghc/issues/14860)),
+    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](https://gitlab.haskell.org/ghc/ghc/issues/16365).
+    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`.
+  * It is no longer possible to define a single `TestEquality` and
+    `TestCoercion` instance that covers all `Sing`s, as one cannot put type
+    families inside of instance heads. Instead, `singletons` now generates a
+    separate `TestEquality`/`TestCoercion` instance for every data type that
+    singletons 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`.
 * 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

README.md

@@ -58,7 +58,6 @@ following:
 * `PolyKinds`
 * `RankNTypes`
 * `ScopedTypeVariables`
-* `StandaloneDeriving`
 * `TemplateHaskell`
 * `TypeApplications`
 * `TypeFamilies`
@@ -152,10 +151,10 @@ 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.
 
 ```haskell
-data family Sing (a :: k)
+type family Sing :: k -> Type
 ```
 
-The data family of singleton types. A new instance of this data family is
+The type family of singleton types. A new instance of this type family is
 generated for every new singleton type.
 
 ```haskell
@@ -222,9 +221,10 @@ 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 both `SEq` and `SDecide` 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`.
+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
@@ -692,23 +692,21 @@ Support for `*`
 
 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
+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:
 
     ```haskell
-    newtype instance Sing :: forall (rep :: RuntimeRep). TYPE rep -> Type where
-      STypeRep :: forall (rep :: RuntimeRep) (a :: TYPE rep). TypeRep a -> Sing a
+    type instance Sing @(TYPE rep) = TypeRep
     ```
 
-   (Recall that `type * = TYPE LiftedRep`.) Thus, a `TypeRep` is stored in the
-singleton constructor. However, any datatypes that store `TypeRep`s will not
-generally work as expected; the built-in promotion mechanism will not promote
-`TypeRep` to `*`.
+    (Recall that `type * = TYPE LiftedRep`.) Note that any datatypes that store
+`TypeRep`s 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

src/Data/Singletons.hs

@@ -7,6 +7,7 @@
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeApplications #-}
@@ -38,7 +39,7 @@
 module Data.Singletons (
   -- * Main singleton definitions
 
-  Sing(SLambda, applySing), (@@),
+  Sing, SLambda(..), (@@),
 
   SingI(..), SingKind(..),
 
@@ -77,6 +78,7 @@ module Data.Singletons (
   Proxy(..),
 
   -- * Defunctionalization symbols
+  SingSym0, SingSym1,
   DemoteSym0, DemoteSym1,
   SameKindSym0, SameKindSym1, SameKindSym2,
   KindOfSym0, KindOfSym1,
@@ -150,7 +152,10 @@ instance SNum k => Num (SomeSing k) where
   signum (SomeSing a) = SomeSing (sSignum a)
   fromInteger n = withSomeSing (fromIntegral n) (SomeSing . sFromInteger)
 
-deriving instance ShowSing k => Show (SomeSing k)
+instance ShowSing k => Show (SomeSing k) where
+  showsPrec p (SomeSing (s :: Sing a)) =
+    showParen (p > 10) $ showString "SomeSing " . showsPrec 11 s
+      :: ShowSing' a => ShowS
 
 instance SSemigroup k => Semigroup (SomeSing k) where
   SomeSing a <> SomeSing b = SomeSing (a %<> b)
@@ -165,8 +170,8 @@ instance SIsString k => IsString (SomeSing k) where
 ---- Defunctionalization symbols -------------------------------------
 ----------------------------------------------------------------------
 
-$(genDefunSymbols [''Demote, ''SameKind, ''KindOf, ''(~>), ''Apply, ''(@@)])
--- SingFunction1 et al. are not defunctionalizable at the moment due to #198
+$(genDefunSymbols [''Sing, ''Demote, ''SameKind, ''KindOf, ''(~>), ''Apply, ''(@@)])
+-- SingFunction1 et al. are not defunctionalizable at the moment due to Trac #9269
 
 {- $SLambdaPatternSynonyms
 

src/Data/Singletons/CustomStar.hs

@@ -60,10 +60,11 @@ import Data.Singletons.Prelude.Bool
 -- and its singleton. However, because @Rep@ is promoted to @*@, the singleton
 -- is perhaps slightly unexpected:
 --
--- > data instance Sing (a :: *) where
+-- > data SRep (a :: *) where
 -- >   SNat :: Sing Nat
 -- >   SBool :: Sing Bool
 -- >   SMaybe :: Sing a -> Sing (Maybe a)
+-- > type instance Sing = SRep
 --
 -- The unexpected part is that @Nat@, @Bool@, and @Maybe@ above are the real @Nat@,
 -- @Bool@, and @Maybe@, not just promoted data constructors.
@@ -87,9 +88,9 @@ singletonStar names = do
     -- We opt to infer the constraints for the Eq instance here so that when it's
     -- promoted, Rep will be promoted to Type.
     dataDeclEqCxt <- inferConstraints (DConT ''Eq) (DConT repName) fakeCtors
-    let dataDeclEqInst = DerivedDecl (Just dataDeclEqCxt) (DConT repName) dataDecl
+    let dataDeclEqInst = DerivedDecl (Just dataDeclEqCxt) (DConT repName) repName dataDecl
     ordInst  <- mkOrdInstance Nothing (DConT repName) dataDecl
-    showInst <- mkShowInstance Nothing (DConT repName) dataDecl
+    showInst <- mkShowInstance ForPromotion Nothing (DConT repName) dataDecl
     (pInsts, promDecls) <- promoteM [] $ do promoteDataDec dataDecl
                                             promoteDerivedEqDec dataDeclEqInst
                                             traverse (promoteInstanceDec mempty)

src/Data/Singletons/Decide.hs

@@ -20,10 +20,10 @@ module Data.Singletons.Decide (
   SDecide(..),
 
   -- * Supporting definitions
-  (:~:)(..), Void, Refuted, Decision(..)
+  (:~:)(..), Void, Refuted, Decision(..),
+  decideEquality, decideCoercion
   ) where
 
-import Data.Kind (Type)
 import Data.Singletons.Internal
 import Data.Type.Coercion
 import Data.Type.Equality
@@ -51,14 +51,20 @@ class SDecide k where
   (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
   infix 4 %~
 
-instance SDecide k => TestEquality (Sing :: k -> Type) where
-  testEquality a b =
-    case a %~ b of
-      Proved Refl -> Just Refl
-      Disproved _ -> Nothing
+-- | A suitable default implementation for 'testEquality' that leverages
+-- 'SDecide'.
+decideEquality :: forall k (a :: k) (b :: k). SDecide k
+               => Sing a -> Sing b -> Maybe (a :~: b)
+decideEquality a b =
+  case a %~ b of
+    Proved Refl -> Just Refl
+    Disproved _ -> Nothing
 
-instance SDecide k => TestCoercion (Sing :: k -> Type) where
-  testCoercion a b =
-    case a %~ b of
-      Proved Refl -> Just Coercion
-      Disproved _ -> Nothing
+-- | A suitable default implementation for 'testCoercion' that leverages
+-- 'SDecide'.
+decideCoercion :: forall k (a :: k) (b :: k). SDecide k
+               => Sing a -> Sing b -> Maybe (Coercion a b)
+decideCoercion a b =
+  case a %~ b of
+    Proved Refl -> Just Coercion
+    Disproved _ -> Nothing