{- Data/Singletons/TH/Single/Data.hs

(c) Richard Eisenberg 2013
rae@cs.brynmawr.edu

Singletonizes constructors.
-}

module Data.Singletons.TH.Single.Data
  ( singDataD
  , singCtor
  ) where

import Language.Haskell.TH.Desugar as Desugar
import Language.Haskell.TH.Syntax
import Data.Maybe
import Data.Singletons.TH.Names
import Data.Singletons.TH.Options
import Data.Singletons.TH.Promote.Type
import Data.Singletons.TH.Single.Defun
import Data.Singletons.TH.Single.Fixity
import Data.Singletons.TH.Single.Monad
import Data.Singletons.TH.Syntax
import Data.Singletons.TH.Util
import Control.Monad

-- We wish to consider the promotion of "Rep" to be *
-- not a promoted data constructor.
singDataD :: DataDecl -> SgM [DDec]
singDataD :: DataDecl -> SgM [DDec]
singDataD (DataDecl DataFlavor
df Name
name [DTyVarBndrVis]
tvbs [DCon]
ctors) = do
  opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  let reqTvbNames   = (DTyVarBndrVis -> Name) -> [DTyVarBndrVis] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrVis -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName ([DTyVarBndrVis] -> [Name]) -> [DTyVarBndrVis] -> [Name]
forall a b. (a -> b) -> a -> b
$
                      (DTyVarBndrVis -> Bool) -> [DTyVarBndrVis] -> [DTyVarBndrVis]
forall a. (a -> Bool) -> [a] -> [a]
filter (\DTyVarBndrVis
tvb -> DTyVarBndrVis -> BndrVis
forall flag. DTyVarBndr flag -> flag
extractTvbFlag DTyVarBndrVis
tvb BndrVis -> BndrVis -> Bool
forall a. Eq a => a -> a -> Bool
== BndrVis
BndrReq) [DTyVarBndrVis]
tvbs
      ctor_names    = (DCon -> Name) -> [DCon] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DCon -> Name
extractName [DCon]
ctors
      rec_sel_names = (DCon -> [Name]) -> [DCon] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DCon -> [Name]
extractRecSelNames [DCon]
ctors
  k <- promoteType (foldTypeTvbs (DConT name) tvbs)
  mb_data_sak <- dsReifyType name
  ctors' <- mapM (singCtor name) ctors
  fixityDecs <- singReifiedInfixDecls $ ctor_names ++ rec_sel_names
  -- instance for SingKind
  fromSingClauses     <- mapM mkFromSingClause ctors
  emptyFromSingClause <- mkEmptyFromSingClause
  toSingClauses       <- mapM mkToSingClause ctors
  emptyToSingClause   <- mkEmptyToSingClause
  let singKindInst =
        Maybe Overlap
-> Maybe [DTyVarBndrUnit] -> DCxt -> DKind -> [DDec] -> DDec
DInstanceD Maybe Overlap
forall a. Maybe a
Nothing Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing
                   ((Name -> DKind) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map (DKind -> DKind
singKindConstraint (DKind -> DKind) -> (Name -> DKind) -> Name -> DKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> DKind
DVarT) [Name]
reqTvbNames)
                   (DKind -> DKind -> DKind
DAppT (Name -> DKind
DConT Name
singKindClassName) DKind
k)
                   [ DTySynEqn -> DDec
DTySynInstD (DTySynEqn -> DDec) -> DTySynEqn -> DDec
forall a b. (a -> b) -> a -> b
$ Maybe [DTyVarBndrUnit] -> DKind -> DKind -> DTySynEqn
DTySynEqn Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing
                      (Name -> DKind
DConT Name
demoteName DKind -> DKind -> DKind
`DAppT` DKind
k)
                      (DKind -> DCxt -> DKind
foldType (Name -> DKind
DConT Name
name)
                        ((Name -> DKind) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map (DKind -> DKind -> DKind
DAppT DKind
demote (DKind -> DKind) -> (Name -> DKind) -> Name -> DKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> DKind
DVarT) [Name]
reqTvbNames))
                   , DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ Name -> [DClause] -> DLetDec
DFunD Name
fromSingName
                               ([DClause]
fromSingClauses [DClause] -> [DClause] -> [DClause]
forall a. [a] -> [a] -> [a]
`orIfEmpty` [DClause
emptyFromSingClause])
                   , DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ Name -> [DClause] -> DLetDec
DFunD Name
toSingName
                               ([DClause]
toSingClauses   [DClause] -> [DClause] -> [DClause]
forall a. [a] -> [a] -> [a]
`orIfEmpty` [DClause
emptyToSingClause]) ]

  let singDataName = Options -> Name -> Name
singledDataTypeName Options
opts Name
name
      -- e.g. type instance Sing @Nat = SNat
      singSynInst =
        DTySynEqn -> DDec
DTySynInstD (DTySynEqn -> DDec) -> DTySynEqn -> DDec
forall a b. (a -> b) -> a -> b
$ Maybe [DTyVarBndrUnit] -> DKind -> DKind -> DTySynEqn
DTySynEqn Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing
                                (Name -> DKind
DConT Name
singFamilyName DKind -> DKind -> DKind
`DAppKindT` DKind
k)
                                (Name -> DKind
DConT Name
singDataName)

      -- Note that we always include an explicit result kind in the body of the
      -- singleton data type declaration, even if it has a standalone kind
      -- signature that would make this explicit result kind redudant.
      -- See Note [Keep redundant kind information for Haddocks]
      -- in D.S.TH.Promote.
      mk_data_dec DKind
kind =
        DataFlavor
-> DCxt
-> Name
-> [DTyVarBndrVis]
-> Maybe DKind
-> [DCon]
-> [DDerivClause]
-> DDec
DDataD DataFlavor
Data [] Name
singDataName [] (DKind -> Maybe DKind
forall a. a -> Maybe a
Just DKind
kind) [DCon]
ctors' []

  data_decs <- case mb_data_sak of
    -- No standalone kind signature. Try to figure out the order of kind
    -- variables on a best-effort basis.
    Maybe DKind
Nothing -> do
      let sing_tvbs :: [DTyVarBndr Specificity]
sing_tvbs = Specificity -> [DTyVarBndrUnit] -> [DTyVarBndr Specificity]
forall newFlag oldFlag.
newFlag -> [DTyVarBndr oldFlag] -> [DTyVarBndr newFlag]
changeDTVFlags Specificity
SpecifiedSpec ([DTyVarBndrUnit] -> [DTyVarBndr Specificity])
-> [DTyVarBndrUnit] -> [DTyVarBndr Specificity]
forall a b. (a -> b) -> a -> b
$
                      DCxt -> [DTyVarBndrUnit]
toposortTyVarsOf (DCxt -> [DTyVarBndrUnit]) -> DCxt -> [DTyVarBndrUnit]
forall a b. (a -> b) -> a -> b
$ (DTyVarBndrVis -> DKind) -> [DTyVarBndrVis] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrVis -> DKind
forall flag. DTyVarBndr flag -> DKind
dTyVarBndrToDType [DTyVarBndrVis]
tvbs
          kinded_sing_ty :: DKind
kinded_sing_ty = DForallTelescope -> DKind -> DKind
DForallT ([DTyVarBndr Specificity] -> DForallTelescope
DForallInvis [DTyVarBndr Specificity]
sing_tvbs) (DKind -> DKind) -> DKind -> DKind
forall a b. (a -> b) -> a -> b
$
                           DKind
DArrowT DKind -> DKind -> DKind
`DAppT` DKind
k DKind -> DKind -> DKind
`DAppT` Name -> DKind
DConT Name
typeKindName
      [DDec] -> SgM [DDec]
forall a. a -> SgM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [DKind -> DDec
mk_data_dec DKind
kinded_sing_ty]

    -- A standalone kind signature is provided, so use that to determine the
    -- order of kind variables.
    Just DKind
data_sak -> do
      sing_data_sak <- DKind -> [DTyVarBndrVis] -> DKind -> SgM DKind
forall (q :: * -> *).
MonadFail q =>
DKind -> [DTyVarBndrVis] -> DKind -> q DKind
singDataSAK DKind
data_sak [DTyVarBndrVis]
tvbs DKind
k
      pure [ DKiSigD singDataName sing_data_sak
           , mk_data_dec sing_data_sak
           ]

  return $ data_decs ++
           singSynInst :
           [ singKindInst | genSingKindInsts opts
                          , -- `type data` data constructors only exist at the
                            -- type level. As such, we cannot define SingKind
                            -- instances for them, as they require term-level
                            -- data constructors to implement.
                            df /= Desugar.TypeData
                          ] ++
           fixityDecs
  where -- in the Rep case, the names of the constructors are in the wrong scope
        -- (they're types, not datacons), so we have to reinterpret them.
        mkConName :: Name -> SgM Name
        mkConName :: Name -> SgM Name
mkConName
          | Name -> String
nameBase Name
name String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> String
nameBase Name
repName = String -> SgM Name
forall (q :: * -> *). Quasi q => String -> q Name
mkDataName (String -> SgM Name) -> (Name -> String) -> Name -> SgM Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
nameBase
          | Bool
otherwise                         = Name -> SgM Name
forall a. a -> SgM a
forall (m :: * -> *) a. Monad m => a -> m a
return

        mkFromSingClause :: DCon -> SgM DClause
        mkFromSingClause :: DCon -> SgM DClause
mkFromSingClause DCon
c = do
          opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
          let (cname, numArgs) = extractNameArgs c
          cname' <- mkConName cname
          varNames <- replicateM numArgs (qNewName "b")
          return $ DClause [DConP (singledDataConName opts cname) [] (map DVarP varNames)]
                           (foldExp
                              (DConE cname')
                              (map (DAppE (DVarE fromSingName) . DVarE) varNames))

        mkToSingClause :: DCon -> SgM DClause
        mkToSingClause :: DCon -> SgM DClause
mkToSingClause (DCon [DTyVarBndr Specificity]
_tvbs DCxt
_cxt Name
cname DConFields
fields DKind
_rty) = do
          opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
          let types = DConFields -> DCxt
tysOfConFields DConFields
fields
          varNames  <- mapM (const $ qNewName "b") types
          svarNames <- mapM (const $ qNewName "c") types
          promoted  <- mapM promoteType types
          cname' <- mkConName cname
          let varPats        = (Name -> DKind -> DPat) -> [Name] -> DCxt -> [DPat]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> DKind -> DPat
mkToSingVarPat [Name]
varNames DCxt
promoted
              recursiveCalls = (Name -> DKind -> DExp) -> [Name] -> DCxt -> [DExp]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> DKind -> DExp
mkRecursiveCall [Name]
varNames DCxt
promoted
          return $
            DClause [DConP cname' [] varPats]
                    (multiCase recursiveCalls
                               (map (DConP someSingDataName [] . listify . DVarP)
                                    svarNames)
                               (DAppE (DConE someSingDataName)
                                         (foldExp (DConE (singledDataConName opts cname))
                                                  (map DVarE svarNames))))

        mkToSingVarPat :: Name -> DKind -> DPat
        mkToSingVarPat :: Name -> DKind -> DPat
mkToSingVarPat Name
varName DKind
ki =
          DPat -> DKind -> DPat
DSigP (Name -> DPat
DVarP Name
varName) (DKind -> DKind -> DKind
DAppT (Name -> DKind
DConT Name
demoteName) DKind
ki)

        mkRecursiveCall :: Name -> DKind -> DExp
        mkRecursiveCall :: Name -> DKind -> DExp
mkRecursiveCall Name
var_name DKind
ki =
          DExp -> DKind -> DExp
DSigE (DExp -> DExp -> DExp
DAppE (Name -> DExp
DVarE Name
toSingName) (Name -> DExp
DVarE Name
var_name))
                (DKind -> DKind -> DKind
DAppT (Name -> DKind
DConT Name
someSingTypeName) DKind
ki)

        mkEmptyFromSingClause :: SgM DClause
        mkEmptyFromSingClause :: SgM DClause
mkEmptyFromSingClause = do
          x <- String -> SgM Name
forall (q :: * -> *). Quasi q => String -> q Name
qNewName String
"x"
          pure $ DClause [DVarP x]
               $ dCaseE (DVarE x) []

        mkEmptyToSingClause :: SgM DClause
        mkEmptyToSingClause :: SgM DClause
mkEmptyToSingClause = do
          x <- String -> SgM Name
forall (q :: * -> *). Quasi q => String -> q Name
qNewName String
"x"
          pure $ DClause [DVarP x]
               $ DConE someSingDataName `DAppE` dCaseE (DVarE x) []

-- Single a constructor.
singCtor :: Name -> DCon -> SgM DCon
 -- polymorphic constructors are handled just
 -- like monomorphic ones -- the polymorphism in
 -- the kind is automatic
singCtor :: Name -> DCon -> SgM DCon
singCtor Name
dataName (DCon [DTyVarBndr Specificity]
con_tvbs DCxt
cxt Name
name DConFields
fields DKind
rty)
  | Bool -> Bool
not (DCxt -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null DCxt
cxt)
  = String -> SgM DCon
forall a. String -> SgM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Singling of constrained constructors not yet supported"
  | Bool
otherwise
  = do
  opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  let types = DConFields -> DCxt
tysOfConFields DConFields
fields
      numTypes = DCxt -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length DCxt
types
      sName = Options -> Name -> Name
singledDataConName Options
opts Name
name
      sCon = Name -> DExp
DConE Name
sName
      pCon = Name -> DKind
DConT (Name -> DKind) -> Name -> DKind
forall a b. (a -> b) -> a -> b
$ Options -> Name -> Name
promotedDataTypeOrConName Options
opts Name
name
  checkVanillaDType $ ravelVanillaDType con_tvbs [] types rty
  indexNames <- mapM (const $ qNewName "n") types
  kinds <- mapM promoteType_NC types
  rty' <- promoteType_NC rty
  let indices = (Name -> DKind) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DKind
DVarT [Name]
indexNames
      kindedIndices = (DKind -> DKind -> DKind) -> DCxt -> DCxt -> DCxt
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith DKind -> DKind -> DKind
DSigT DCxt
indices DCxt
kinds
      -- The approach we use for singling data constructor types differs
      -- slightly from the approach taken in D.S.TH.Single.Type.singType in that
      -- we always explicitly quantify all type variables in a singled data
      -- constructor, regardless of whether the original data constructor
      -- explicitly quantified them or not. This explains the use of
      -- toposortTyVarsOf below.
      -- See Note [Preserve the order of type variables during singling]
      -- (wrinkle 1) in D.S.TH.Single.Type.
      kvbs | [DTyVarBndr Specificity] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DTyVarBndr Specificity]
con_tvbs
           = Specificity -> [DTyVarBndrUnit] -> [DTyVarBndr Specificity]
forall newFlag oldFlag.
newFlag -> [DTyVarBndr oldFlag] -> [DTyVarBndr newFlag]
changeDTVFlags Specificity
SpecifiedSpec (DCxt -> [DTyVarBndrUnit]
toposortTyVarsOf (DCxt
kinds DCxt -> DCxt -> DCxt
forall a. [a] -> [a] -> [a]
++ [DKind
rty'])) [DTyVarBndr Specificity]
-> [DTyVarBndr Specificity] -> [DTyVarBndr Specificity]
forall a. [a] -> [a] -> [a]
++
             [DTyVarBndr Specificity]
con_tvbs
           | Bool
otherwise
           = [DTyVarBndr Specificity]
con_tvbs
      all_tvbs = [DTyVarBndr Specificity]
kvbs [DTyVarBndr Specificity]
-> [DTyVarBndr Specificity] -> [DTyVarBndr Specificity]
forall a. [a] -> [a] -> [a]
++ (Name -> DKind -> DTyVarBndr Specificity)
-> [Name] -> DCxt -> [DTyVarBndr Specificity]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Name -> Specificity -> DKind -> DTyVarBndr Specificity
forall flag. Name -> flag -> DKind -> DTyVarBndr flag
`DKindedTV` Specificity
SpecifiedSpec) [Name]
indexNames DCxt
kinds

  -- @mb_SingI_dec k@ returns 'Just' an instance of @SingI<k>@ if @k@ is
  -- less than or equal to the number of fields in the data constructor.
  -- Otherwise, it returns 'Nothing'.
  let mb_SingI_dec :: Int -> Maybe DDec
      mb_SingI_dec Int
k
        | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
numTypes
        = let take_until_k :: [a] -> [a]
take_until_k = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take (Int
numTypes Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k) in
          DDec -> Maybe DDec
forall a. a -> Maybe a
Just (DDec -> Maybe DDec) -> DDec -> Maybe DDec
forall a b. (a -> b) -> a -> b
$ Maybe Overlap
-> Maybe [DTyVarBndrUnit] -> DCxt -> DKind -> [DDec] -> DDec
DInstanceD Maybe Overlap
forall a. Maybe a
Nothing Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing
                   ((DKind -> DKind) -> DCxt -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map (DKind -> DKind -> DKind
DAppT (Name -> DKind
DConT Name
singIName)) (DCxt -> DCxt
forall {a}. [a] -> [a]
take_until_k DCxt
indices))
                   (DKind -> DKind -> DKind
DAppT (Name -> DKind
DConT (Int -> Name
mkSingIName Int
k))
                          (DKind -> DCxt -> DKind
foldType DKind
pCon (DCxt -> DCxt
forall {a}. [a] -> [a]
take_until_k DCxt
kindedIndices)))
                   [DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ DPat -> DExp -> DLetDec
DValD (Name -> DPat
DVarP (Int -> Name
mkSingMethName Int
k))
                          (DExp -> [DExp] -> DExp
foldExp DExp
sCon (Int -> DExp -> [DExp]
forall a. Int -> a -> [a]
replicate (Int
numTypes Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k) (Name -> DExp
DVarE Name
singMethName)))]
        | Bool
otherwise
        = Maybe DDec
forall a. Maybe a
Nothing

  -- SingI instance for data constructor
  emitDecs $ mapMaybe mb_SingI_dec [0, 1, 2]
  -- SingI instances for defunctionalization symbols. Note that we don't
  -- support contexts in constructors at the moment, so it's fine for now to
  -- just assume that the context is always ().
  emitDecs =<< singDefuns name DataName [] (map Just kinds) (Just rty')

  conFields <- case fields of
    DNormalC Bool
dInfix [DBangType]
bts -> Bool -> [DBangType] -> DConFields
DNormalC Bool
dInfix ([DBangType] -> DConFields) -> SgM [DBangType] -> SgM DConFields
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                           (DBangType -> DKind -> SgM DBangType)
-> [DBangType] -> DCxt -> SgM [DBangType]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (\(Bang
b, DKind
_) DKind
index -> Bang -> DKind -> SgM DBangType
mk_bang_type Bang
b DKind
index)
                                    [DBangType]
bts DCxt
indices
    DRecC [DVarBangType]
vbts          -> Bool -> [DBangType] -> DConFields
DNormalC Bool
False ([DBangType] -> DConFields) -> SgM [DBangType] -> SgM DConFields
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                           (DVarBangType -> DKind -> SgM DBangType)
-> [DVarBangType] -> DCxt -> SgM [DBangType]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (\(Name
_, Bang
b, DKind
_) DKind
index -> Bang -> DKind -> SgM DBangType
mk_bang_type Bang
b DKind
index)
                                    [DVarBangType]
vbts DCxt
indices
                      -- Don't bother looking at record selectors, as they are
                      -- handled separately in singTopLevelDecs.
                      -- See Note [singletons-th and record selectors]
  return $ DCon all_tvbs [] sName conFields
                (DConT (singledDataTypeName opts dataName) `DAppT`
                  (foldType pCon indices `DSigT` rty'))
                  -- Make sure to include an explicit `rty'` kind annotation.
                  -- See Note [Preserve the order of type variables during singling],
                  -- wrinkle 2, in D.S.TH.Single.Type.
  where
    mk_source_unpackedness :: SourceUnpackedness -> SgM SourceUnpackedness
    mk_source_unpackedness :: SourceUnpackedness -> SgM SourceUnpackedness
mk_source_unpackedness SourceUnpackedness
su = case SourceUnpackedness
su of
      SourceUnpackedness
NoSourceUnpackedness -> SourceUnpackedness -> SgM SourceUnpackedness
forall a. a -> SgM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceUnpackedness
su
      SourceUnpackedness
SourceNoUnpack       -> SourceUnpackedness -> SgM SourceUnpackedness
forall a. a -> SgM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceUnpackedness
su
      SourceUnpackedness
SourceUnpack         -> do
        -- {-# UNPACK #-} is essentially useless in a singletons setting, since
        -- all singled data types are GADTs. See GHC#10016.
        String -> SgM ()
forall (q :: * -> *). Quasi q => String -> q ()
qReportWarning String
"{-# UNPACK #-} pragmas are ignored by `singletons-th`."
        SourceUnpackedness -> SgM SourceUnpackedness
forall a. a -> SgM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceUnpackedness
NoSourceUnpackedness

    mk_bang :: Bang -> SgM Bang
    mk_bang :: Bang -> SgM Bang
mk_bang (Bang SourceUnpackedness
su SourceStrictness
ss) = do su' <- SourceUnpackedness -> SgM SourceUnpackedness
mk_source_unpackedness SourceUnpackedness
su
                              pure $ Bang su' ss

    mk_bang_type :: Bang -> DType -> SgM DBangType
    mk_bang_type :: Bang -> DKind -> SgM DBangType
mk_bang_type Bang
b DKind
index = do b' <- Bang -> SgM Bang
mk_bang Bang
b
                              pure (b', DAppT singFamily index)

-- @'singDataSAK' sak data_bndrs@ produces a standalone kind signature for a
-- singled data declaration, using the original data type's standalone kind
-- signature (@sak@) and its user-written binders (@data_bndrs@) as a template.
-- For this example:
--
-- @
-- type D :: forall j k. k -> j -> Type
-- data D @j @l (a :: l) b = ...
-- @
--
-- We would produce the following standalone kind signature:
--
-- @
-- type SD :: forall j l (a :: l) (b :: j). D @j @l (a :: l) b -> Type
-- @
--
-- Note that the order of the invisible quantifiers is preserved, so both
-- @D \@Bool \@Ordering@ and @SD \@Bool \@Ordering@ will work the way you would
-- expect it to.
--
-- See also the Haddocks for 'dMatchUpSAKWithDecl' function, which also apply
-- here.
singDataSAK ::
     MonadFail q
  => DKind
     -- ^ The standalone kind signature for the original data type
  -> [DTyVarBndrVis]
     -- ^ The user-written binders for the original data type
  -> DKind
     -- ^ The original data type, promoted to a kind
  -> q DKind
     -- ^ The standalone kind signature for the singled data type
singDataSAK :: forall (q :: * -> *).
MonadFail q =>
DKind -> [DTyVarBndrVis] -> DKind -> q DKind
singDataSAK DKind
data_sak [DTyVarBndrVis]
data_bndrs DKind
data_k = do
  sing_sak_tvbs <- DKind -> [DTyVarBndrVis] -> q [DTyVarBndr ForAllTyFlag]
forall (q :: * -> *).
MonadFail q =>
DKind -> [DTyVarBndrVis] -> q [DTyVarBndr ForAllTyFlag]
dMatchUpSAKWithDecl DKind
data_sak [DTyVarBndrVis]
data_bndrs
  let sing_sak_tvbs' = [DTyVarBndr ForAllTyFlag] -> [DTyVarBndr Specificity]
dtvbForAllTyFlagsToSpecs [DTyVarBndr ForAllTyFlag]
sing_sak_tvbs
  pure $ DForallT (DForallInvis sing_sak_tvbs')
       $ DArrowT `DAppT` data_k `DAppT` DConT typeKindName

{-
Note [singletons-th and record selectors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Record selectors are annoying to deal with in singletons-th for various reasons:

1. There is no record syntax at the type level, so promoting code that involves
   records in some way is not straightforward.
2. One can define record selectors for singled data types, but they're rife
   with peril. Some pitfalls include:

   * Singling record updates often produces code that does not typecheck. For
     example, this works:

       let i = Identity True in i { runIdentity = False }

     But this does /not/ work:

       let si = SIdentity STrue in si { sRunIdentity = SFalse }

       error:
           • Record update for insufficiently polymorphic field:
               sRunIdentity :: Sing n
           • In the expression: si {sRunIdentity = SFalse}
             In the expression:
               let si = SIdentity STrue in si {sRunIdentity = SFalse}

     Ugh. See GHC#16501.

   * Singling a data type with multiple constructors that share a record
     selector name will /also/ not typecheck. While this works:

       data X = X1 {y :: Bool} | X2 {y :: Bool}

     This does not:

       data SX :: X -> Type where
         SX1 :: { sY :: Sing n } -> SX ('X1 n)
         SY1 :: { sY :: Sing n } -> SX ('X2 n)

       error:
           • Constructors SX1 and SX2 have a common field ‘sY’,
               but have different result types
           • In the data type declaration for ‘SX’

     Double ugh. See GHC#8673/GHC#12159.

   * Even if a data type only has a single constructor with record selectors,
     singling it can induce headaches. One might be tempted to single this type:

       newtype Unit = MkUnit { runUnit :: () }

     With this code:

       data SUnit :: Unit -> Type where
         SMkUnit :: { sRunUnit :: Sing u } -> SUnit (MkUnit u)

     Somewhat surprisingly, the type of sRunUnit:

       sRunUnit :: Sing (MkUnit u) -> Sing u

     Is not general enough to handle common uses of record selectors. For
     example, if you try to single this function:

       f :: Unit -> ()
       f = runUnit

     Then the resulting code:

       sF :: Sing (x :: Unit) -> Sing (F x :: ())
       sF = sRunUnit

     Will not typecheck. Note that sRunUnit expects an argument of type
     `Sing (MkUnit u)`, but there is no way to know a priori that the `x` in
     `Sing (x :: Unit)` is `MkUnit u` without pattern-matching on SMkUnit.

Hopefully I have convinced you that handling records in singletons-th is a bit of
a nightmare. Thankfully, there is a simple trick to avoid most of the pitfalls
above: just desugar code (using th-desugar) to avoid records!
In more concrete terms, we do the following:

* A record constructions desugars to a normal constructor application. For example:

    MkT{a = x, b = y}

      ==>

    MkT x y

  Something similar occurs for record syntax in patterns.

* A record update desugars to a case expression. For example:

    t{a = x}

      ==>

    case t of MkT _ y => MkT x y

We can't easily desugar away all uses of records, however. After all, records
can be used as ordinary functions as well. We leave such uses of records alone
when desugaring and accommodate them during promotion and singling by generating
"manual" record selectors. As a running example, consider the earlier Unit example:

  newtype Unit = MkUnit { runUnit :: () }

When singling Unit, we do not give SMkUnit a record selector:

  data SUnit :: Unit -> Type where
    SMkUnit :: Sing u -> SUnit (MkUnit u)

Instead, we generate a top-level function that behaves equivalently to runUnit.
This function then gets promoted and singled (in D.S.TH.Promote.promoteDecs and
D.S.TH.Single.singTopLevelDecs):

  type family RunUnit (x :: Unit) :: () where
    RunUnit (MkUnit x) = x

  sRunUnit :: Sing (x :: Unit) -> Sing (RunUnit x :: ())
  sRunUnit (SMkUnit sx) = sx

Now promoting/singling uses of runUnit as an ordinary function work as expected
since the types of RunUnit/sRunUnit are sufficiently general. This technique also
scales up to data types with multiple constructors sharing a record selector name.
For instance, in the earlier X example:

  data X = X1 {y :: Bool} | X2 {y :: Bool}

We would promote/single `y` like so:

  type family Y (x :: X) :: Bool where
    Y (X1 y) = y
    Y (X2 y) = y

  sY :: Sing (x :: X) -> Sing (Y x :: Bool)
  sY (SX1 sy) = sy
  sY (SX2 sy) = sy

Manual record selectors cannot be used in record constructions or updates, but
for most use cases this won't be an issue, since singletons-th makes an effort to
desugar away fancy uses of records anyway. The only time this would bite is if
you wanted to use record syntax in hand-written singletons code.
-}