Single record selectors as top-level functions (#436)

`singletons` has traditionally singled record selectors "in-place".
For example, `data T = MkT { unT :: Bool }` would be singled as
`data ST :: T -> Type where SMkT :: { sUnT :: Sing b } -> ST (MkT b)`.
This may seem like a sensible choice, but it has some unfortunate
consequences:

* This function will not typecheck when singled:

  ```hs
  f :: T -> Bool
  f = unT
  ```

  This is because the type of `sUnT` is `Sing (MkT b) -> b`, which
  is not general enough for the type of `sF`, which is
  `Sing (t :: T) -> Sing (F t :: Bool)`.
* It is impossible to single a data type with multiple constructors
  that share a record name, since each occurrence of a record
  selector in a data type is required to have the same type.

For these reasons and more discussed in
`Note [singletons and record selectors]` in `D.S.Single.Data`, we
have decided in #364 to single record selectors as simple top-level
functions. That is, we would generate the following for `sUnT`:

```hs
data ST :: T -> Type where
  SMkT :: Sing b -> ST (MkT b)

sUnT :: Sing (t :: T) -> Sing (UnT t :: Bool)
sUnT (MkT x) = x
```

This brings the treatment of singled record selectors in line with
promoted record selectors (note that `UnT` is also a top-level type
family) and avoids the drawbacks mentioned above. The drawback is
that it is no longer possible to use record syntax in combination
with `SMkT`, although record selectors for singleton data constructors
are already quite buggy (see
#364 (comment)),
so this is arguably not that huge of a loss.

This change allows `D.S.Prelude.*` to single code that is much closer
to the original code found in `base`. As one example, the changes in
`D.S.Prelude.Foldable` should give a pretty good idea of the kind of
code that can now be singled.

Fixes #364.

CHANGES.md

@@ -4,6 +4,40 @@ 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:
+
+  ```hs
+  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:
+
+  ```hs
+  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](https://github.com/goldfirere/singletons/issues/364)
+  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
@@ -37,22 +71,24 @@ Changelog for singletons project
   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.)
-* 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.
 * 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 `Nat`s, 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 and class methods correctly.
+    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

README.md

@@ -592,7 +592,6 @@ The following constructs are fully supported:
 * 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)
-* records
 * pattern guards
 * case
 * let
@@ -604,6 +603,7 @@ The following constructs are fully supported:
 * `InstanceSigs`
 * higher-kinded type variables (see below)
 * finite arithmetic sequences (see below)
+* records (with limitations -- see below)
 * functional dependencies (with limitations -- see below)
 * type families (with limitations -- see below)
 
@@ -623,6 +623,16 @@ methods from the `Enum` class under the hood). _Finite_ sequences (e.g.,
 which desugar to calls to `enumFromTo` or `enumFromThenTo`, are not supported,
 as these would require using infinite lists at the type level.
 
+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](https://github.com/goldfirere/singletons/issues/364) 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.
+
 The following constructs are supported for promotion but not singleton generation:
 
 * datatypes with constructors which have contexts. For example, the following
@@ -864,7 +874,6 @@ for the following constructs:
 Known bugs
 ----------
 
-* Record updates don't singletonize
 * Inference dependent on functional dependencies is unpredictably bad. The
   problem is that a use of an associated type family tied to a class with
   fundeps doesn't provoke the fundep to kick in. This is GHC's problem, in

src/Data/Singletons/CustomStar.hs

@@ -92,7 +92,7 @@ singletonStar names = do
     let dataDeclEqInst = DerivedDecl (Just dataDeclEqCxt) (DConT repName) repName dataDecl
     ordInst  <- mkOrdInstance Nothing (DConT repName) dataDecl
     showInst <- mkShowInstance ForPromotion Nothing (DConT repName) dataDecl
-    (pInsts, promDecls) <- promoteM [] $ do promoteDataDec dataDecl
+    (pInsts, promDecls) <- promoteM [] $ do _ <- promoteDataDec dataDecl
                                             promoteDerivedEqDec dataDeclEqInst
                                             traverse (promoteInstanceDec mempty mempty)
                                               [ordInst, showInst]

src/Data/Singletons/Prelude/Applicative.hs

@@ -29,7 +29,7 @@
 module Data.Singletons.Prelude.Applicative (
   PApplicative(..), SApplicative(..),
   PAlternative(..), SAlternative(..),
-  Sing, SConst(..), Const, GetConst,
+  Sing, SConst(..), Const, GetConst, sGetConst,
   type (<$>), (%<$>), type (<$), (%<$), type (<**>), (%<**>),
   LiftA, sLiftA, LiftA3, sLiftA3, Optional, sOptional,
 

src/Data/Singletons/Prelude/Const.hs

@@ -27,7 +27,7 @@
 
 module Data.Singletons.Prelude.Const (
   -- * The 'Const' singleton
-  Sing, SConst(..), GetConst,
+  Sing, SConst(..), GetConst, sGetConst,
 
   -- * Defunctionalization symbols
   ConstSym0, ConstSym1,
@@ -73,7 +73,7 @@ hand.
 -}
 type SConst :: Const a b -> Type
 data SConst c where
-  SConst :: { sGetConst :: Sing a } -> SConst ('Const a)
+  SConst :: Sing a -> SConst ('Const a)
 type instance Sing = SConst
 instance SingKind a => SingKind (Const a b) where
   type Demote (Const a b) = Const (Demote a) b
@@ -86,13 +86,10 @@ $(genDefunSymbols [''Const])
 instance SingI ConstSym0 where
   sing = singFun1 SConst
 
-$(singletons [d|
-  type GetConst :: Const a b -> a
-  type family GetConst x where
-    GetConst ('Const x) = x
-  |])
-
 $(singletonsOnly [d|
+  getConst :: Const a b -> a
+  getConst (Const x) = x
+
   deriving instance Bounded a => Bounded (Const a b)
   deriving instance Eq      a => Eq      (Const a b)
   deriving instance Ord     a => Ord     (Const a b)