Single record selectors as top-level functions

[RyanGlScott]

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:

  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:

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.

[RyanGlScott]

Ideally, I would have written this:

      maximum = fromMaybe (errorWithoutStackTrace "maximum: empty structure") .
       getMaxInternal . foldMap (MaxInternal . (Just :: a -> Maybe))

As that is closer to how maximum is actually defined in base. Sadly, this won't work in singletons due to #433.

[goldfirere]

Otherwise, looks good!