{- Data/Singletons/Single/Data.hs

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

Singletonizes constructors.
-}

{-# LANGUAGE ParallelListComp, TupleSections, LambdaCase #-}

module Data.Singletons.Single.Data where

import Language.Haskell.TH.Desugar
import Language.Haskell.TH.Syntax
import Data.Singletons.Single.Defun
import Data.Singletons.Single.Monad
import Data.Singletons.Single.Type
import Data.Singletons.Single.Fixity
import Data.Singletons.Promote.Type
import Data.Singletons.Util
import Data.Singletons.Names
import Data.Singletons.Syntax
import Data.Singletons.TH.Options
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 Name
name [DTyVarBndr]
tvbs [DCon]
ctors) = do
  Options
opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  let tvbNames :: [Name]
tvbNames      = (DTyVarBndr -> Name) -> [DTyVarBndr] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndr -> Name
extractTvbName [DTyVarBndr]
tvbs
      ctor_names :: [Name]
ctor_names    = (DCon -> Name) -> [DCon] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DCon -> Name
extractName [DCon]
ctors
      rec_sel_names :: [Name]
rec_sel_names = (DCon -> [Name]) -> [DCon] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DCon -> [Name]
extractRecSelNames [DCon]
ctors
  DKind
k <- DKind -> SgM DKind
forall (m :: * -> *). MonadFail m => DKind -> m DKind
promoteType (DKind -> [DKind] -> DKind
foldType (Name -> DKind
DConT Name
name) ((Name -> DKind) -> [Name] -> [DKind]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DKind
DVarT [Name]
tvbNames))
  Maybe DKind
mb_data_sak <- Name -> SgM (Maybe DKind)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DKind)
dsReifyType Name
name
  [DCon]
ctors' <- (DCon -> SgM DCon) -> [DCon] -> SgM [DCon]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name -> DCon -> SgM DCon
singCtor Name
name) [DCon]
ctors
  [DDec]
fixityDecs <- [Name] -> SgM [DDec]
forall (q :: * -> *). OptionsMonad q => [Name] -> q [DDec]
singReifiedInfixDecls ([Name] -> SgM [DDec]) -> [Name] -> SgM [DDec]
forall a b. (a -> b) -> a -> b
$ [Name]
ctor_names [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
rec_sel_names
  -- instance for SingKind
  [DClause]
fromSingClauses     <- (DCon -> SgM DClause) -> [DCon] -> SgM [DClause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM DCon -> SgM DClause
mkFromSingClause [DCon]
ctors
  DClause
emptyFromSingClause <- SgM DClause
mkEmptyFromSingClause
  [DClause]
toSingClauses       <- (DCon -> SgM DClause) -> [DCon] -> SgM [DClause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM DCon -> SgM DClause
mkToSingClause [DCon]
ctors
  DClause
emptyToSingClause   <- SgM DClause
mkEmptyToSingClause
  let singKindInst :: DDec
singKindInst =
        Maybe Overlap
-> Maybe [DTyVarBndr] -> [DKind] -> DKind -> [DDec] -> DDec
DInstanceD Maybe Overlap
forall a. Maybe a
Nothing Maybe [DTyVarBndr]
forall a. Maybe a
Nothing
                   ((Name -> DKind) -> [Name] -> [DKind]
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]
tvbNames)
                   (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 [DTyVarBndr] -> DKind -> DKind -> DTySynEqn
DTySynEqn Maybe [DTyVarBndr]
forall a. Maybe a
Nothing
                      (Name -> DKind
DConT Name
demoteName DKind -> DKind -> DKind
`DAppT` DKind
k)
                      (DKind -> [DKind] -> DKind
foldType (Name -> DKind
DConT Name
name)
                        ((Name -> DKind) -> [Name] -> [DKind]
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]
tvbNames))
                   , 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 :: Name
singDataName = Options -> Name -> Name
singledDataTypeName Options
opts Name
name
      -- e.g. type instance Sing @Nat = SNat
      singSynInst :: DDec
singSynInst =
        DTySynEqn -> DDec
DTySynInstD (DTySynEqn -> DDec) -> DTySynEqn -> DDec
forall a b. (a -> b) -> a -> b
$ Maybe [DTyVarBndr] -> DKind -> DKind -> DTySynEqn
DTySynEqn Maybe [DTyVarBndr]
forall a. Maybe a
Nothing
                                (Name -> DKind
DConT Name
singFamilyName DKind -> DKind -> DKind
`DAppKindT` DKind
k)
                                (Name -> DKind
DConT Name
singDataName)

      mk_data_dec :: [DTyVarBndr] -> Maybe DKind -> DDec
mk_data_dec [DTyVarBndr]
tvbs' Maybe DKind
mb_kind =
        NewOrData
-> [DKind]
-> Name
-> [DTyVarBndr]
-> Maybe DKind
-> [DCon]
-> [DDerivClause]
-> DDec
DDataD NewOrData
Data [] Name
singDataName [DTyVarBndr]
tvbs' Maybe DKind
mb_kind [DCon]
ctors' []

  [DDec]
data_decs <-
    case Maybe DKind
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
        DKind
ki <- DKind -> SgM DKind
forall (m :: * -> *). MonadFail m => DKind -> m DKind
promoteType (DKind -> SgM DKind) -> DKind -> SgM DKind
forall a b. (a -> b) -> a -> b
$ DKind -> [DKind] -> DKind
foldType (Name -> DKind
DConT Name
name) ((DTyVarBndr -> DKind) -> [DTyVarBndr] -> [DKind]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndr -> DKind
dTyVarBndrToDType [DTyVarBndr]
tvbs)
        let sing_tvbs :: [DTyVarBndr]
sing_tvbs = [DKind] -> [DTyVarBndr]
toposortTyVarsOf [DKind
k]
            kinded_sing_ty :: DKind
kinded_sing_ty = ForallVisFlag -> [DTyVarBndr] -> DKind -> DKind
DForallT ForallVisFlag
ForallInvis [DTyVarBndr]
sing_tvbs (DKind -> DKind) -> DKind -> DKind
forall a b. (a -> b) -> a -> b
$
                             DKind
DArrowT DKind -> DKind -> DKind
`DAppT` DKind
ki DKind -> DKind -> DKind
`DAppT` Name -> DKind
DConT Name
typeKindName
        [DDec] -> SgM [DDec]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [[DTyVarBndr] -> Maybe DKind -> DDec
mk_data_dec [] (DKind -> Maybe DKind
forall a. a -> Maybe a
Just 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
        let (DFunArgs
args, DKind
_)  = DKind -> (DFunArgs, DKind)
unravelDType DKind
data_sak
            vis_args :: [DVisFunArg]
vis_args   = DFunArgs -> [DVisFunArg]
filterDVisFunArgs DFunArgs
args
            invis_tvbs :: [DTyVarBndr]
invis_tvbs = DFunArgs -> [DTyVarBndr]
filterInvisTvbArgs DFunArgs
args
            vis_tvbs :: [DTyVarBndr]
vis_tvbs   = (DVisFunArg -> DTyVarBndr -> DTyVarBndr)
-> [DVisFunArg] -> [DTyVarBndr] -> [DTyVarBndr]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith DVisFunArg -> DTyVarBndr -> DTyVarBndr
replaceTvbKind [DVisFunArg]
vis_args [DTyVarBndr]
tvbs
        DKind
ki <- DKind -> SgM DKind
forall (m :: * -> *). MonadFail m => DKind -> m DKind
promoteType (DKind -> SgM DKind) -> DKind -> SgM DKind
forall a b. (a -> b) -> a -> b
$ DKind -> [DKind] -> DKind
foldType (Name -> DKind
DConT Name
name) ((DTyVarBndr -> DKind) -> [DTyVarBndr] -> [DKind]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndr -> DKind
dTyVarBndrToDType [DTyVarBndr]
vis_tvbs)
        Name
z  <- String -> SgM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"z"
        let sing_data_sak :: DKind
sing_data_sak = ForallVisFlag -> [DTyVarBndr] -> DKind -> DKind
DForallT ForallVisFlag
ForallInvis ([DTyVarBndr]
invis_tvbs [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
forall a. [a] -> [a] -> [a]
++ [DTyVarBndr]
vis_tvbs) (DKind -> DKind) -> DKind -> DKind
forall a b. (a -> b) -> a -> b
$
                            DKind
DArrowT DKind -> DKind -> DKind
`DAppT` DKind
ki DKind -> DKind -> DKind
`DAppT` Name -> DKind
DConT Name
typeKindName
        [DDec] -> SgM [DDec]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ Name -> DKind -> DDec
DKiSigD Name
singDataName DKind
sing_data_sak
             , [DTyVarBndr] -> Maybe DKind -> DDec
mk_data_dec [Name -> DTyVarBndr
DPlainTV Name
z] Maybe DKind
forall a. Maybe a
Nothing
             ]

  [DDec] -> SgM [DDec]
forall (m :: * -> *) a. Monad m => a -> m a
return ([DDec] -> SgM [DDec]) -> [DDec] -> SgM [DDec]
forall a b. (a -> b) -> a -> b
$ [DDec]
data_decs [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++
           DDec
singSynInst DDec -> [DDec] -> [DDec]
forall a. a -> [a] -> [a]
:
           [DDec
singKindInst | Options -> Bool
genSingKindInsts Options
opts] [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++
           [DDec]
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 (m :: * -> *). Quasi m => String -> m 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 (m :: * -> *) a. Monad m => a -> m a
return

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

        mkToSingClause :: DCon -> SgM DClause
        mkToSingClause :: DCon -> SgM DClause
mkToSingClause (DCon [DTyVarBndr]
_tvbs [DKind]
_cxt Name
cname DConFields
fields DKind
_rty) = do
          Options
opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
          let types :: [DKind]
types = DConFields -> [DKind]
tysOfConFields DConFields
fields
          [Name]
varNames  <- (DKind -> SgM Name) -> [DKind] -> SgM [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SgM Name -> DKind -> SgM Name
forall a b. a -> b -> a
const (SgM Name -> DKind -> SgM Name) -> SgM Name -> DKind -> SgM Name
forall a b. (a -> b) -> a -> b
$ String -> SgM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"b") [DKind]
types
          [Name]
svarNames <- (DKind -> SgM Name) -> [DKind] -> SgM [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SgM Name -> DKind -> SgM Name
forall a b. a -> b -> a
const (SgM Name -> DKind -> SgM Name) -> SgM Name -> DKind -> SgM Name
forall a b. (a -> b) -> a -> b
$ String -> SgM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"c") [DKind]
types
          [DKind]
promoted  <- (DKind -> SgM DKind) -> [DKind] -> SgM [DKind]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM DKind -> SgM DKind
forall (m :: * -> *). MonadFail m => DKind -> m DKind
promoteType [DKind]
types
          Name
cname' <- Name -> SgM Name
mkConName Name
cname
          let varPats :: [DPat]
varPats        = (Name -> DKind -> DPat) -> [Name] -> [DKind] -> [DPat]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> DKind -> DPat
mkToSingVarPat [Name]
varNames [DKind]
promoted
              recursiveCalls :: [DExp]
recursiveCalls = (Name -> DKind -> DExp) -> [Name] -> [DKind] -> [DExp]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> DKind -> DExp
mkRecursiveCall [Name]
varNames [DKind]
promoted
          DClause -> SgM DClause
forall (m :: * -> *) a. Monad m => a -> m a
return (DClause -> SgM DClause) -> DClause -> SgM DClause
forall a b. (a -> b) -> a -> b
$
            [DPat] -> DExp -> DClause
DClause [Name -> [DPat] -> DPat
DConP Name
cname' [DPat]
varPats]
                    ([DExp] -> [DPat] -> DExp -> DExp
multiCase [DExp]
recursiveCalls
                               ((Name -> DPat) -> [Name] -> [DPat]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> [DPat] -> DPat
DConP Name
someSingDataName ([DPat] -> DPat) -> (Name -> [DPat]) -> Name -> DPat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DPat -> [DPat]
forall a. a -> [a]
listify (DPat -> [DPat]) -> (Name -> DPat) -> Name -> [DPat]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> DPat
DVarP)
                                    [Name]
svarNames)
                               (DExp -> DExp -> DExp
DAppE (Name -> DExp
DConE Name
someSingDataName)
                                         (DExp -> [DExp] -> DExp
foldExp (Name -> DExp
DConE (Options -> Name -> Name
singledDataConName Options
opts Name
cname))
                                                  ((Name -> DExp) -> [Name] -> [DExp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DExp
DVarE [Name]
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
          Name
x <- String -> SgM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"x"
          DClause -> SgM DClause
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DClause -> SgM DClause) -> DClause -> SgM DClause
forall a b. (a -> b) -> a -> b
$ [DPat] -> DExp -> DClause
DClause [Name -> DPat
DVarP Name
x]
               (DExp -> DClause) -> DExp -> DClause
forall a b. (a -> b) -> a -> b
$ DExp -> [DMatch] -> DExp
DCaseE (Name -> DExp
DVarE Name
x) []

        mkEmptyToSingClause :: SgM DClause
        mkEmptyToSingClause :: SgM DClause
mkEmptyToSingClause = do
          Name
x <- String -> SgM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"x"
          DClause -> SgM DClause
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DClause -> SgM DClause) -> DClause -> SgM DClause
forall a b. (a -> b) -> a -> b
$ [DPat] -> DExp -> DClause
DClause [Name -> DPat
DVarP Name
x]
               (DExp -> DClause) -> DExp -> DClause
forall a b. (a -> b) -> a -> b
$ Name -> DExp
DConE Name
someSingDataName DExp -> DExp -> DExp
`DAppE` DExp -> [DMatch] -> DExp
DCaseE (Name -> DExp
DVarE Name
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]
con_tvbs [DKind]
cxt Name
name DConFields
fields DKind
rty)
  | Bool -> Bool
not ([DKind] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DKind]
cxt)
  = String -> SgM DCon
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Singling of constrained constructors not yet supported"
  | Bool
otherwise
  = do
  Options
opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  let types :: [DKind]
types = DConFields -> [DKind]
tysOfConFields DConFields
fields
      sName :: Name
sName = Options -> Name -> Name
singledDataConName Options
opts Name
name
      sCon :: DExp
sCon = Name -> DExp
DConE Name
sName
      pCon :: DKind
pCon = Name -> DKind
DConT Name
name
  DKind -> SgM ()
forall (m :: * -> *). MonadFail m => DKind -> m ()
checkVanillaDType (DKind -> SgM ()) -> DKind -> SgM ()
forall a b. (a -> b) -> a -> b
$ [DTyVarBndr] -> [DKind] -> [DKind] -> DKind -> DKind
ravelVanillaDType [DTyVarBndr]
con_tvbs [] [DKind]
types DKind
rty
  [Name]
indexNames <- (DKind -> SgM Name) -> [DKind] -> SgM [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SgM Name -> DKind -> SgM Name
forall a b. a -> b -> a
const (SgM Name -> DKind -> SgM Name) -> SgM Name -> DKind -> SgM Name
forall a b. (a -> b) -> a -> b
$ String -> SgM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"n") [DKind]
types
  [DKind]
kinds <- (DKind -> SgM DKind) -> [DKind] -> SgM [DKind]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM DKind -> SgM DKind
forall (m :: * -> *). MonadFail m => DKind -> m DKind
promoteType_NC [DKind]
types
  DKind
rty' <- DKind -> SgM DKind
forall (m :: * -> *). MonadFail m => DKind -> m DKind
promoteType_NC DKind
rty
  let indices :: [DKind]
indices = (Name -> DKind) -> [Name] -> [DKind]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DKind
DVarT [Name]
indexNames
      kindedIndices :: [DKind]
kindedIndices = (DKind -> DKind -> DKind) -> [DKind] -> [DKind] -> [DKind]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith DKind -> DKind -> DKind
DSigT [DKind]
indices [DKind]
kinds
      kvbs :: [DTyVarBndr]
kvbs = [DTyVarBndr]
-> [DKind] -> [DKind] -> DKind -> OSet Name -> [DTyVarBndr]
singTypeKVBs [DTyVarBndr]
con_tvbs [DKind]
kinds [] DKind
rty' OSet Name
forall a. Monoid a => a
mempty
      all_tvbs :: [DTyVarBndr]
all_tvbs = [DTyVarBndr]
kvbs [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
forall a. [a] -> [a] -> [a]
++ (Name -> DKind -> DTyVarBndr) -> [Name] -> [DKind] -> [DTyVarBndr]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> DKind -> DTyVarBndr
DKindedTV [Name]
indexNames [DKind]
kinds

  -- SingI instance for data constructor
  [DDec] -> SgM ()
forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
emitDecs
    [Maybe Overlap
-> Maybe [DTyVarBndr] -> [DKind] -> DKind -> [DDec] -> DDec
DInstanceD Maybe Overlap
forall a. Maybe a
Nothing Maybe [DTyVarBndr]
forall a. Maybe a
Nothing
                ((DKind -> DKind) -> [DKind] -> [DKind]
forall a b. (a -> b) -> [a] -> [b]
map (DKind -> DKind -> DKind
DAppT (Name -> DKind
DConT Name
singIName)) [DKind]
indices)
                (DKind -> DKind -> DKind
DAppT (Name -> DKind
DConT Name
singIName)
                       (DKind -> [DKind] -> DKind
foldType DKind
pCon [DKind]
kindedIndices))
                [DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ DPat -> DExp -> DLetDec
DValD (Name -> DPat
DVarP Name
singMethName)
                       (DExp -> [DExp] -> DExp
foldExp DExp
sCon ((DKind -> DExp) -> [DKind] -> [DExp]
forall a b. (a -> b) -> [a] -> [b]
map (DExp -> DKind -> DExp
forall a b. a -> b -> a
const (DExp -> DKind -> DExp) -> DExp -> DKind -> DExp
forall a b. (a -> b) -> a -> b
$ Name -> DExp
DVarE Name
singMethName) [DKind]
types))]]
  -- 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 ().
  [DDec] -> SgM ()
forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
emitDecs ([DDec] -> SgM ()) -> SgM [DDec] -> SgM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Name
-> NameSpace
-> [DKind]
-> [Maybe DKind]
-> Maybe DKind
-> SgM [DDec]
singDefuns Name
name NameSpace
DataName [] ((DKind -> Maybe DKind) -> [DKind] -> [Maybe DKind]
forall a b. (a -> b) -> [a] -> [b]
map DKind -> Maybe DKind
forall a. a -> Maybe a
Just [DKind]
kinds) (DKind -> Maybe DKind
forall a. a -> Maybe a
Just DKind
rty')

  let noBang :: Bang
noBang    = SourceUnpackedness -> SourceStrictness -> Bang
Bang SourceUnpackedness
NoSourceUnpackedness SourceStrictness
NoSourceStrictness
      args :: [(Bang, DKind)]
args      = (DKind -> (Bang, DKind)) -> [DKind] -> [(Bang, DKind)]
forall a b. (a -> b) -> [a] -> [b]
map ((Bang
noBang,) (DKind -> (Bang, DKind))
-> (DKind -> DKind) -> DKind -> (Bang, DKind)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DKind -> DKind -> DKind
DAppT DKind
singFamily) [DKind]
indices
      conFields :: DConFields
conFields = case DConFields
fields of
                    DNormalC Bool
dInfix [(Bang, DKind)]
_ -> Bool -> [(Bang, DKind)] -> DConFields
DNormalC Bool
dInfix [(Bang, DKind)]
args
                    DRecC [DVarBangType]
_           -> Bool -> [(Bang, DKind)] -> DConFields
DNormalC Bool
False  [(Bang, DKind)]
args
                      -- Don't bother looking at record selectors, as they are
                      -- handled separately in singTopLevelDecs.
                      -- See Note [singletons and record selectors]
  DCon -> SgM DCon
forall (m :: * -> *) a. Monad m => a -> m a
return (DCon -> SgM DCon) -> DCon -> SgM DCon
forall a b. (a -> b) -> a -> b
$ [DTyVarBndr] -> [DKind] -> Name -> DConFields -> DKind -> DCon
DCon [DTyVarBndr]
all_tvbs [] Name
sName DConFields
conFields
                (Name -> DKind
DConT (Options -> Name -> Name
singledDataTypeName Options
opts Name
dataName) DKind -> DKind -> DKind
`DAppT`
                  (DKind -> [DKind] -> DKind
foldType DKind
pCon [DKind]
indices DKind -> DKind -> DKind
`DSigT` DKind
rty'))
                  -- Make sure to include an explicit `rty'` kind annotation.
                  -- See Note [Preserve the order of type variables during singling],
                  -- wrinkle 3, in D.S.Single.Type.

{-
Note [singletons and record selectors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Record selectors are annoying to deal with in singletons 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 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.Promote.promoteDecs and
D.S.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 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.
-}