WIP: Single record selectors as top-level functions

TODO RGS: Say the magic words about 364

`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.

[ci skip]

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
@@ -34,13 +68,15 @@ Changelog for singletons project
 * 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

@@ -584,7 +584,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
@@ -596,6 +595,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)
 
@@ -624,6 +624,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
@@ -768,7 +778,6 @@ of how this may be fixed in the future.
 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

@@ -28,7 +28,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

@@ -26,7 +26,7 @@
 
 module Data.Singletons.Prelude.Const (
   -- * The 'Const' singleton
-  Sing, SConst(..), GetConst,
+  Sing, SConst(..), GetConst, sGetConst,
 
   -- * Defunctionalization symbols
   ConstSym0, ConstSym1,
@@ -71,7 +71,7 @@ poly-kinded Sing instances (see #150), we simply write the Sing instance by
 hand.
 -}
 data SConst :: forall (k :: Type) (a :: Type) (b :: k). Const a b -> Type 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
@@ -84,12 +84,10 @@ $(genDefunSymbols [''Const])
 instance SingI ConstSym0 where
   sing = singFun1 SConst
 
-$(singletons [d|
-  type family GetConst (x :: Const a b) :: a 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)

src/Data/Singletons/Prelude/Foldable.hs

@@ -101,7 +101,7 @@ import Control.Monad
 import Data.Kind
 import Data.List.NonEmpty (NonEmpty(..))
 import Data.Monoid hiding (All(..), Any(..), Endo(..), Product(..), Sum(..))
-import qualified Data.Monoid as Monoid (All(..), Any(..), Product(..), Sum(..))
+import qualified Data.Monoid as Monoid (Product(..), Sum(..))
 import Data.Singletons.Internal
 import Data.Singletons.Prelude.Base
   hiding (Foldr, FoldrSym0, FoldrSym1, FoldrSym2, FoldrSym3, sFoldr)
@@ -126,11 +126,11 @@ import Data.Singletons.Prelude.Semigroup.Internal
   hiding ( AllSym0(..),     AllSym1,     SAll
          , AnySym0(..),     AnySym1,     SAny
          , FirstSym0,       FirstSym1,   SFirst
+         , GetFirstSym0,    sGetFirst
          , LastSym0,        LastSym1,    SLast
          , ProductSym0(..), ProductSym1, SProduct
          , SumSym0(..),     SumSym1,     SSum )
 import Data.Singletons.Prelude.Semigroup.Internal.Disambiguation
-import Data.Singletons.Promote
 import Data.Singletons.Single
 import Data.Singletons.TypeLits.Internal
 
@@ -142,24 +142,20 @@ data EndoSym0 :: forall a. (a ~> a) ~> Endo a
 type instance Apply EndoSym0 x = 'Endo x
 
 $(singletonsOnly [d|
+  appEndo :: Endo a -> (a -> a)
+  appEndo (Endo x) = x
+
   instance Semigroup (Endo a) where
           Endo x <> Endo y = Endo (x . y)
 
   instance Monoid (Endo a) where
           mempty = Endo id
   |])
 
-newtype MaxInternal a = MaxInternal (Maybe a)
-data SMaxInternal :: forall a. MaxInternal a -> Type where
-  SMaxInternal :: Sing x -> SMaxInternal ('MaxInternal x)
-type instance Sing = SMaxInternal
-$(genDefunSymbols [''MaxInternal])
-
-newtype MinInternal a = MinInternal (Maybe a)
-data SMinInternal :: forall a. MinInternal a -> Type where
-  SMinInternal :: Sing x -> SMinInternal ('MinInternal x)
-type instance Sing = SMinInternal
-$(genDefunSymbols [''MinInternal])
+$(singletons [d|
+  newtype MaxInternal a = MaxInternal { getMaxInternal :: Maybe a }
+  newtype MinInternal a = MinInternal { getMinInternal :: Maybe a }
+  |])
 
 $(singletonsOnly [d|
   instance Ord a => Semigroup (MaxInternal a) where
@@ -258,8 +254,7 @@ $(singletonsOnly [d|
       -- @foldr f z = 'List.foldr' f z . 'toList'@
       --
       foldr :: (a -> b -> b) -> b -> t a -> b
-      foldr f z t = case foldMap (Endo . f) t of
-                      Endo g -> g z
+      foldr f z t = appEndo (foldMap (Endo . f) t) z
 
       -- -| Right-associative fold of a structure, but with strict application of
       -- the operator.
@@ -294,8 +289,7 @@ $(singletonsOnly [d|
       -- @foldl f z = 'List.foldl' f z . 'toList'@
       --
       foldl :: (b -> a -> b) -> b -> t a -> b
-      foldl f z t = case foldMap (Dual . Endo . flip f) t of
-                      Dual (Endo g) -> g z
+      foldl f z t = appEndo (getDual (foldMap (Dual . Endo . flip f) t)) z
       -- There's no point mucking around with coercions here,
       -- because flip forces us to build a new function anyway.
 
@@ -362,26 +356,28 @@ $(singletonsOnly [d|
 
       -- -| The largest element of a non-empty structure.
       maximum :: forall a . Ord a => t a -> a
-      maximum x =
-        case foldMap (MaxInternal . Just) x of
-          MaxInternal y -> fromMaybe (errorWithoutStackTrace "maximum: empty structure") y
+      maximum = fromMaybe (errorWithoutStackTrace "maximum: empty structure") .
+       getMaxInternal . foldMap (MaxInternal . mkJust)
+        where
+          mkJust :: a -> Maybe a
+          mkJust = Just
 
       -- -| The least element of a non-empty structure.
       minimum :: forall a . Ord a => t a -> a
-      minimum x =
-        case foldMap (MinInternal . Just) x of
-          MinInternal y -> fromMaybe (errorWithoutStackTrace "minimum: empty structure") y
+      minimum = fromMaybe (errorWithoutStackTrace "minimum: empty structure") .
+       getMinInternal . foldMap (MinInternal . mkJust)
+        where
+          mkJust :: a -> Maybe a
+          mkJust = Just
 
       -- -| The 'sum' function computes the sum of the numbers of a structure.
       sum :: Num a => t a -> a
-      sum x = case foldMap sum_ x of
-                Monoid.Sum y -> y
+      sum = getSum . foldMap sum_
 
       -- -| The 'product' function computes the product of the numbers of a
       -- structure.
       product :: Num a => t a -> a
-      product x = case foldMap product_ x of
-                    Monoid.Product y -> y
+      product = getProduct . foldMap product_
 
   -- instances for Prelude types
 
@@ -449,55 +445,55 @@ $(singletonsOnly [d|
   instance Foldable Dual where
       foldMap f (Dual x)  = f x
 
-      elem x (Dual y)     = x == y
+      elem                = (. getDual) . (==)
       foldl f z (Dual x)  = f z x
       foldl' f z (Dual x) = f z x
-      foldl1 _ (Dual x)   = x
+      foldl1 _            = getDual
       foldr f z (Dual x)  = f x z
       foldr'              = foldr
-      foldr1 _ (Dual x)   = x
+      foldr1 _            = getDual
       length _            = 1
-      maximum (Dual x)    = x
-      minimum (Dual x)    = x
+      maximum             = getDual
+      minimum             = getDual
       null _              = False
-      product (Dual x)    = x
-      sum (Dual x)        = x
+      product             = getDual
+      sum                 = getDual
       toList (Dual x)     = [x]
 
   instance Foldable Monoid.Sum where
       foldMap f (Monoid.Sum x)  = f x
 
-      elem x (Monoid.Sum y)     = x == y
+      elem                      = (. getSum) . (==)
       foldl f z (Monoid.Sum x)  = f z x
       foldl' f z (Monoid.Sum x) = f z x
-      foldl1 _ (Monoid.Sum x)   = x
+      foldl1 _                  = getSum
       foldr f z (Monoid.Sum x)  = f x z
       foldr'                    = foldr
-      foldr1 _ (Monoid.Sum x)   = x
+      foldr1 _                  = getSum
       length _                  = 1
-      maximum (Monoid.Sum x)    = x
-      minimum (Monoid.Sum x)    = x
+      maximum                   = getSum
+      minimum                   = getSum
       null _                    = False
-      product (Monoid.Sum x)    = x
-      sum (Monoid.Sum x)        = x
+      product                   = getSum
+      sum                       = getSum
       toList (Monoid.Sum x)     = [x]
 
   instance Foldable Monoid.Product where
       foldMap f (Monoid.Product x)  = f x
 
-      elem x (Monoid.Product y)     = x == y
+      elem                          = (. getProduct) . (==)
       foldl f z (Monoid.Product x)  = f z x
       foldl' f z (Monoid.Product x) = f z x
-      foldl1 _ (Monoid.Product x)   = x
+      foldl1 _                      = getProduct
       foldr f z (Monoid.Product x)  = f x z
-      foldr'              = foldr
-      foldr1 _ (Monoid.Product x)   = x
-      length _            = 1
-      maximum (Monoid.Product x)    = x
-      minimum (Monoid.Product x)    = x
-      null _              = False
-      product (Monoid.Product x)    = x
-      sum (Monoid.Product x)        = x
+      foldr'                        = foldr
+      foldr1 _                      = getProduct
+      length _                      = 1
+      maximum                       = getProduct
+      minimum                       = getProduct
+      null _                        = False
+      product                       = getProduct
+      sum                           = getProduct
       toList (Monoid.Product x)     = [x]
 
   -- -| Monadic fold over the elements of a structure,
@@ -588,25 +584,21 @@ $(singletonsOnly [d|
   -- result to be 'True', the container must be finite; 'False', however,
   -- results from a 'False' value finitely far from the left end.
   and :: Foldable t => t Bool -> Bool
-  and x = case foldMap all_ x of
-            Monoid.All y -> y
+  and = getAll . foldMap all_
 
   -- -| 'or' returns the disjunction of a container of Bools.  For the
   -- result to be 'False', the container must be finite; 'True', however,
   -- results from a 'True' value finitely far from the left end.
   or :: Foldable t => t Bool -> Bool
-  or x = case foldMap any_ x of
-           Monoid.Any y -> y
+  or = getAny . foldMap any_
 
   -- -| Determines whether any element of the structure satisfies the predicate.
   any :: Foldable t => (a -> Bool) -> t a -> Bool
-  any p x = case foldMap (any_ . p) x of
-              Monoid.Any y -> y
+  any p = getAny . foldMap (any_ . p)
 
   -- -| Determines whether all elements of the structure satisfy the predicate.
   all :: Foldable t => (a -> Bool) -> t a -> Bool
-  all p x = case foldMap (all_ . p) x of
-              Monoid.All y -> y
+  all p = getAll . foldMap (all_ . p)
 
   -- -| The largest element of a non-empty structure with respect to the
   -- given comparison function.
@@ -638,8 +630,7 @@ $(singletonsOnly [d|
   -- the leftmost element of the structure matching the predicate, or
   -- 'Nothing' if there is no such element.
   find :: Foldable t => (a -> Bool) -> t a -> Maybe a
-  find p y = case foldMap (\ x -> First (if p x then Just x else Nothing)) y of
-               First z -> z
+  find p = getFirst . foldMap (\ x -> First (if p x then Just x else Nothing))
   |])
 
 $(singletonsOnly [d|

src/Data/Singletons/Prelude/Identity.hs

@@ -26,7 +26,7 @@
 
 module Data.Singletons.Prelude.Identity (
   -- * The 'Identity' singleton
-  Sing, SIdentity(..), RunIdentity,
+  Sing, SIdentity(..), RunIdentity, sRunIdentity,
 
   -- * Defunctionalization symbols
   IdentitySym0, IdentitySym1,