    {- Data/Singletons/Single/Monad.hs

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

    This file defines the SgM monad and its operations, for use during singling.

    The SgM monad allows reading from a SgEnv environment and is wrapped around a Q.
    -}

    {-# LANGUAGE GeneralizedNewtypeDeriving, ParallelListComp, TemplateHaskell #-}

    module Data.Singletons.Single.Monad (
      SgM, bindLets, bindContext, askContext, lookupVarE, lookupConE,
      wrapSingFun, wrapUnSingFun,
      singM, singDecsM,
      emitDecs, emitDecsM
      ) where

    import Prelude hiding ( exp )
    import Data.Map ( Map )
    import qualified Data.Map as Map
    import Data.Singletons.Promote.Monad ( emitDecs, emitDecsM )
    import Data.Singletons.Names
    import Data.Singletons.Util
    import Data.Singletons.Internal
    import Language.Haskell.TH.Syntax hiding ( lift )
    import Language.Haskell.TH.Desugar
    import Control.Monad.Reader
    import Control.Monad.Writer
    import Control.Applicative

    -- environment during singling
    data SgEnv =
      SgEnv { SgEnv -> Map Name DExp
    sg_let_binds   :: Map Name DExp   -- from the *original* name
            , SgEnv -> DCxt
    sg_context     :: DCxt -- See Note [Tracking the current type signature context]
            , SgEnv -> [Dec]
    sg_local_decls :: [Dec]
            }

    emptySgEnv :: SgEnv
    emptySgEnv :: SgEnv
    emptySgEnv = SgEnv :: Map Name DExp -> DCxt -> [Dec] -> SgEnv
    SgEnv { sg_let_binds :: Map Name DExp
    sg_let_binds   = Map Name DExp
    forall k a. Map k a
    Map.empty
                       , sg_context :: DCxt
    sg_context     = []
                       , sg_local_decls :: [Dec]
    sg_local_decls = []
                       }

    -- the singling monad
    newtype SgM a = SgM (ReaderT SgEnv (WriterT [DDec] Q) a)
      deriving ( a -> SgM b -> SgM a
    (a -> b) -> SgM a -> SgM b
    (forall a b. (a -> b) -> SgM a -> SgM b)
    -> (forall a b. a -> SgM b -> SgM a) -> Functor SgM
    forall a b. a -> SgM b -> SgM a
    forall a b. (a -> b) -> SgM a -> SgM b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: a -> SgM b -> SgM a
    $c<$ :: forall a b. a -> SgM b -> SgM a
    fmap :: (a -> b) -> SgM a -> SgM b
    $cfmap :: forall a b. (a -> b) -> SgM a -> SgM b
    Functor, Functor SgM
    a -> SgM a
    Functor SgM =>
    (forall a. a -> SgM a)
    -> (forall a b. SgM (a -> b) -> SgM a -> SgM b)
    -> (forall a b c. (a -> b -> c) -> SgM a -> SgM b -> SgM c)
    -> (forall a b. SgM a -> SgM b -> SgM b)
    -> (forall a b. SgM a -> SgM b -> SgM a)
    -> Applicative SgM
    SgM a -> SgM b -> SgM b
    SgM a -> SgM b -> SgM a
    SgM (a -> b) -> SgM a -> SgM b
    (a -> b -> c) -> SgM a -> SgM b -> SgM c
    forall a. a -> SgM a
    forall a b. SgM a -> SgM b -> SgM a
    forall a b. SgM a -> SgM b -> SgM b
    forall a b. SgM (a -> b) -> SgM a -> SgM b
    forall a b c. (a -> b -> c) -> SgM a -> SgM b -> SgM c
    forall (f :: * -> *).
    Functor f =>
    (forall a. a -> f a)
    -> (forall a b. f (a -> b) -> f a -> f b)
    -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
    -> (forall a b. f a -> f b -> f b)
    -> (forall a b. f a -> f b -> f a)
    -> Applicative f
    <* :: SgM a -> SgM b -> SgM a
    $c<* :: forall a b. SgM a -> SgM b -> SgM a
    *> :: SgM a -> SgM b -> SgM b
    $c*> :: forall a b. SgM a -> SgM b -> SgM b
    liftA2 :: (a -> b -> c) -> SgM a -> SgM b -> SgM c
    $cliftA2 :: forall a b c. (a -> b -> c) -> SgM a -> SgM b -> SgM c
    <*> :: SgM (a -> b) -> SgM a -> SgM b
    $c<*> :: forall a b. SgM (a -> b) -> SgM a -> SgM b
    pure :: a -> SgM a
    $cpure :: forall a. a -> SgM a
    $cp1Applicative :: Functor SgM
    Applicative, Applicative SgM
    a -> SgM a
    Applicative SgM =>
    (forall a b. SgM a -> (a -> SgM b) -> SgM b)
    -> (forall a b. SgM a -> SgM b -> SgM b)
    -> (forall a. a -> SgM a)
    -> Monad SgM
    SgM a -> (a -> SgM b) -> SgM b
    SgM a -> SgM b -> SgM b
    forall a. a -> SgM a
    forall a b. SgM a -> SgM b -> SgM b
    forall a b. SgM a -> (a -> SgM b) -> SgM b
    forall (m :: * -> *).
    Applicative m =>
    (forall a b. m a -> (a -> m b) -> m b)
    -> (forall a b. m a -> m b -> m b)
    -> (forall a. a -> m a)
    -> Monad m
    return :: a -> SgM a
    $creturn :: forall a. a -> SgM a
    >> :: SgM a -> SgM b -> SgM b
    $c>> :: forall a b. SgM a -> SgM b -> SgM b
    >>= :: SgM a -> (a -> SgM b) -> SgM b
    $c>>= :: forall a b. SgM a -> (a -> SgM b) -> SgM b
    $cp1Monad :: Applicative SgM
    Monad
               , MonadReader SgEnv, MonadWriter [DDec]
               , Monad SgM
    Monad SgM => (forall a. String -> SgM a) -> MonadFail SgM
    String -> SgM a
    forall a. String -> SgM a
    forall (m :: * -> *).
    Monad m =>
    (forall a. String -> m a) -> MonadFail m
    fail :: String -> SgM a
    $cfail :: forall a. String -> SgM a
    $cp1MonadFail :: Monad SgM
    MonadFail, Monad SgM
    Monad SgM => (forall a. IO a -> SgM a) -> MonadIO SgM
    IO a -> SgM a
    forall a. IO a -> SgM a
    forall (m :: * -> *).
    Monad m =>
    (forall a. IO a -> m a) -> MonadIO m
    liftIO :: IO a -> SgM a
    $cliftIO :: forall a. IO a -> SgM a
    $cp1MonadIO :: Monad SgM
    MonadIO )

    liftSgM :: Q a -> SgM a
    liftSgM :: Q a -> SgM a
    liftSgM = ReaderT SgEnv (WriterT [DDec] Q) a -> SgM a
    forall a. ReaderT SgEnv (WriterT [DDec] Q) a -> SgM a
    SgM (ReaderT SgEnv (WriterT [DDec] Q) a -> SgM a)
    -> (Q a -> ReaderT SgEnv (WriterT [DDec] Q) a) -> Q a -> SgM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WriterT [DDec] Q a -> ReaderT SgEnv (WriterT [DDec] Q) a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (WriterT [DDec] Q a -> ReaderT SgEnv (WriterT [DDec] Q) a)
    -> (Q a -> WriterT [DDec] Q a)
    -> Q a
    -> ReaderT SgEnv (WriterT [DDec] Q) a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Q a -> WriterT [DDec] Q a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift

    instance Quasi SgM where
      qNewName :: String -> SgM Name
    qNewName          = Q Name -> SgM Name
    forall a. Q a -> SgM a
    liftSgM (Q Name -> SgM Name) -> (String -> Q Name) -> String -> SgM Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    `comp1` String -> Q Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName
      qReport :: Bool -> String -> SgM ()
    qReport           = Q () -> SgM ()
    forall a. Q a -> SgM a
    liftSgM (Q () -> SgM ())
    -> (Bool -> String -> Q ()) -> Bool -> String -> SgM ()
    forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
    `comp2` Bool -> String -> Q ()
    forall (m :: * -> *). Quasi m => Bool -> String -> m ()
    qReport
      qLookupName :: Bool -> String -> SgM (Maybe Name)
    qLookupName       = Q (Maybe Name) -> SgM (Maybe Name)
    forall a. Q a -> SgM a
    liftSgM (Q (Maybe Name) -> SgM (Maybe Name))
    -> (Bool -> String -> Q (Maybe Name))
    -> Bool
    -> String
    -> SgM (Maybe Name)
    forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
    `comp2` Bool -> String -> Q (Maybe Name)
    forall (m :: * -> *). Quasi m => Bool -> String -> m (Maybe Name)
    qLookupName
      qReify :: Name -> SgM Info
    qReify            = Q Info -> SgM Info
    forall a. Q a -> SgM a
    liftSgM (Q Info -> SgM Info) -> (Name -> Q Info) -> Name -> SgM Info
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    `comp1` Name -> Q Info
    forall (m :: * -> *). Quasi m => Name -> m Info
    qReify
      qReifyInstances :: Name -> [Type] -> SgM [Dec]
    qReifyInstances   = Q [Dec] -> SgM [Dec]
    forall a. Q a -> SgM a
    liftSgM (Q [Dec] -> SgM [Dec])
    -> (Name -> [Type] -> Q [Dec]) -> Name -> [Type] -> SgM [Dec]
    forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
    `comp2` Name -> [Type] -> Q [Dec]
    forall (m :: * -> *). Quasi m => Name -> [Type] -> m [Dec]
    qReifyInstances
      qLocation :: SgM Loc
    qLocation         = Q Loc -> SgM Loc
    forall a. Q a -> SgM a
    liftSgM Q Loc
    forall (m :: * -> *). Quasi m => m Loc
    qLocation
      qRunIO :: IO a -> SgM a
    qRunIO            = Q a -> SgM a
    forall a. Q a -> SgM a
    liftSgM (Q a -> SgM a) -> (IO a -> Q a) -> IO a -> SgM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    `comp1` IO a -> Q a
    forall (m :: * -> *) a. Quasi m => IO a -> m a
    qRunIO
      qAddDependentFile :: String -> SgM ()
    qAddDependentFile = Q () -> SgM ()
    forall a. Q a -> SgM a
    liftSgM (Q () -> SgM ()) -> (String -> Q ()) -> String -> SgM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    `comp1` String -> Q ()
    forall (m :: * -> *). Quasi m => String -> m ()
    qAddDependentFile
      qReifyRoles :: Name -> SgM [Role]
    qReifyRoles       = Q [Role] -> SgM [Role]
    forall a. Q a -> SgM a
    liftSgM (Q [Role] -> SgM [Role])
    -> (Name -> Q [Role]) -> Name -> SgM [Role]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    `comp1` Name -> Q [Role]
    forall (m :: * -> *). Quasi m => Name -> m [Role]
    qReifyRoles
      qReifyAnnotations :: AnnLookup -> SgM [a]
    qReifyAnnotations = Q [a] -> SgM [a]
    forall a. Q a -> SgM a
    liftSgM (Q [a] -> SgM [a]) -> (AnnLookup -> Q [a]) -> AnnLookup -> SgM [a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    `comp1` AnnLookup -> Q [a]
    forall (m :: * -> *) a. (Quasi m, Data a) => AnnLookup -> m [a]
    qReifyAnnotations
      qReifyModule :: Module -> SgM ModuleInfo
    qReifyModule      = Q ModuleInfo -> SgM ModuleInfo
    forall a. Q a -> SgM a
    liftSgM (Q ModuleInfo -> SgM ModuleInfo)
    -> (Module -> Q ModuleInfo) -> Module -> SgM ModuleInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    `comp1` Module -> Q ModuleInfo
    forall (m :: * -> *). Quasi m => Module -> m ModuleInfo
    qReifyModule
      qAddTopDecls :: [Dec] -> SgM ()
    qAddTopDecls      = Q () -> SgM ()
    forall a. Q a -> SgM a
    liftSgM (Q () -> SgM ()) -> ([Dec] -> Q ()) -> [Dec] -> SgM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    `comp1` [Dec] -> Q ()
    forall (m :: * -> *). Quasi m => [Dec] -> m ()
    qAddTopDecls
      qAddModFinalizer :: Q () -> SgM ()
    qAddModFinalizer  = Q () -> SgM ()
    forall a. Q a -> SgM a
    liftSgM (Q () -> SgM ()) -> (Q () -> Q ()) -> Q () -> SgM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    `comp1` Q () -> Q ()
    forall (m :: * -> *). Quasi m => Q () -> m ()
    qAddModFinalizer
      qGetQ :: SgM (Maybe a)
    qGetQ             = Q (Maybe a) -> SgM (Maybe a)
    forall a. Q a -> SgM a
    liftSgM Q (Maybe a)
    forall (m :: * -> *) a. (Quasi m, Typeable a) => m (Maybe a)
    qGetQ
      qPutQ :: a -> SgM ()
    qPutQ             = Q () -> SgM ()
    forall a. Q a -> SgM a
    liftSgM (Q () -> SgM ()) -> (a -> Q ()) -> a -> SgM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    `comp1` a -> Q ()
    forall (m :: * -> *) a. (Quasi m, Typeable a) => a -> m ()
    qPutQ

      qReifyFixity :: Name -> SgM (Maybe Fixity)
    qReifyFixity        = Q (Maybe Fixity) -> SgM (Maybe Fixity)
    forall a. Q a -> SgM a
    liftSgM (Q (Maybe Fixity) -> SgM (Maybe Fixity))
    -> (Name -> Q (Maybe Fixity)) -> Name -> SgM (Maybe Fixity)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    `comp1` Name -> Q (Maybe Fixity)
    forall (m :: * -> *). Quasi m => Name -> m (Maybe Fixity)
    qReifyFixity
      qReifyConStrictness :: Name -> SgM [DecidedStrictness]
    qReifyConStrictness = Q [DecidedStrictness] -> SgM [DecidedStrictness]
    forall a. Q a -> SgM a
    liftSgM (Q [DecidedStrictness] -> SgM [DecidedStrictness])
    -> (Name -> Q [DecidedStrictness])
    -> Name
    -> SgM [DecidedStrictness]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    `comp1` Name -> Q [DecidedStrictness]
    forall (m :: * -> *). Quasi m => Name -> m [DecidedStrictness]
    qReifyConStrictness
      qIsExtEnabled :: Extension -> SgM Bool
    qIsExtEnabled       = Q Bool -> SgM Bool
    forall a. Q a -> SgM a
    liftSgM (Q Bool -> SgM Bool)
    -> (Extension -> Q Bool) -> Extension -> SgM Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    `comp1` Extension -> Q Bool
    forall (m :: * -> *). Quasi m => Extension -> m Bool
    qIsExtEnabled
      qExtsEnabled :: SgM [Extension]
    qExtsEnabled        = Q [Extension] -> SgM [Extension]
    forall a. Q a -> SgM a
    liftSgM Q [Extension]
    forall (m :: * -> *). Quasi m => m [Extension]
    qExtsEnabled
      qAddForeignFilePath :: ForeignSrcLang -> String -> SgM ()
    qAddForeignFilePath = Q () -> SgM ()
    forall a. Q a -> SgM a
    liftSgM (Q () -> SgM ())
    -> (ForeignSrcLang -> String -> Q ())
    -> ForeignSrcLang
    -> String
    -> SgM ()
    forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
    `comp2` ForeignSrcLang -> String -> Q ()
    forall (m :: * -> *). Quasi m => ForeignSrcLang -> String -> m ()
    qAddForeignFilePath
      qAddTempFile :: String -> SgM String
    qAddTempFile        = Q String -> SgM String
    forall a. Q a -> SgM a
    liftSgM (Q String -> SgM String)
    -> (String -> Q String) -> String -> SgM String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    `comp1` String -> Q String
    forall (m :: * -> *). Quasi m => String -> m String
    qAddTempFile
      qAddCorePlugin :: String -> SgM ()
    qAddCorePlugin      = Q () -> SgM ()
    forall a. Q a -> SgM a
    liftSgM (Q () -> SgM ()) -> (String -> Q ()) -> String -> SgM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    `comp1` String -> Q ()
    forall (m :: * -> *). Quasi m => String -> m ()
    qAddCorePlugin

      qRecover :: SgM a -> SgM a -> SgM a
    qRecover (SgM handler :: ReaderT SgEnv (WriterT [DDec] Q) a
    handler) (SgM body :: ReaderT SgEnv (WriterT [DDec] Q) a
    body) = do
        SgEnv
    env <- SgM SgEnv
    forall r (m :: * -> *). MonadReader r m => m r
    ask
        (result :: a
    result, aux :: [DDec]
    aux) <- Q (a, [DDec]) -> SgM (a, [DDec])
    forall a. Q a -> SgM a
    liftSgM (Q (a, [DDec]) -> SgM (a, [DDec]))
    -> Q (a, [DDec]) -> SgM (a, [DDec])
    forall a b. (a -> b) -> a -> b
    $
                         Q (a, [DDec]) -> Q (a, [DDec]) -> Q (a, [DDec])
    forall (m :: * -> *) a. Quasi m => m a -> m a -> m a
    qRecover (WriterT [DDec] Q a -> Q (a, [DDec])
    forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
    runWriterT (WriterT [DDec] Q a -> Q (a, [DDec]))
    -> WriterT [DDec] Q a -> Q (a, [DDec])
    forall a b. (a -> b) -> a -> b
    $ ReaderT SgEnv (WriterT [DDec] Q) a -> SgEnv -> WriterT [DDec] Q a
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT ReaderT SgEnv (WriterT [DDec] Q) a
    handler SgEnv
    env)
                                  (WriterT [DDec] Q a -> Q (a, [DDec])
    forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
    runWriterT (WriterT [DDec] Q a -> Q (a, [DDec]))
    -> WriterT [DDec] Q a -> Q (a, [DDec])
    forall a b. (a -> b) -> a -> b
    $ ReaderT SgEnv (WriterT [DDec] Q) a -> SgEnv -> WriterT [DDec] Q a
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT ReaderT SgEnv (WriterT [DDec] Q) a
    body SgEnv
    env)
        [DDec] -> SgM ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell [DDec]
    aux
        a -> SgM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    result

    instance DsMonad SgM where
      localDeclarations :: SgM [Dec]
    localDeclarations = (SgEnv -> [Dec]) -> SgM [Dec]
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks SgEnv -> [Dec]
    sg_local_decls

    bindLets :: [(Name, DExp)] -> SgM a -> SgM a
    bindLets :: [(Name, DExp)] -> SgM a -> SgM a
    bindLets lets1 :: [(Name, DExp)]
    lets1 =
      (SgEnv -> SgEnv) -> SgM a -> SgM a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local (\env :: SgEnv
    env@(SgEnv { sg_let_binds :: SgEnv -> Map Name DExp
    sg_let_binds = Map Name DExp
    lets2 }) ->
                   SgEnv
    env { sg_let_binds :: Map Name DExp
    sg_let_binds = ([(Name, DExp)] -> Map Name DExp
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [(Name, DExp)]
    lets1) Map Name DExp -> Map Name DExp -> Map Name DExp
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    `Map.union` Map Name DExp
    lets2 })

    -- Add some constraints to the current type signature context.
    -- See Note [Tracking the current type signature context]
    bindContext :: DCxt -> SgM a -> SgM a
    bindContext :: DCxt -> SgM a -> SgM a
    bindContext ctxt1 :: DCxt
    ctxt1
      = (SgEnv -> SgEnv) -> SgM a -> SgM a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local (\env :: SgEnv
    env@(SgEnv { sg_context :: SgEnv -> DCxt
    sg_context = DCxt
    ctxt2 }) ->
                     SgEnv
    env { sg_context :: DCxt
    sg_context = DCxt
    ctxt1 DCxt -> DCxt -> DCxt
    forall a. [a] -> [a] -> [a]
    ++ DCxt
    ctxt2 })

    -- Retrieve the current type signature context.
    -- See Note [Tracking the current type signature context]
    askContext :: SgM DCxt
    askContext :: SgM DCxt
    askContext = (SgEnv -> DCxt) -> SgM DCxt
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks SgEnv -> DCxt
    sg_context

    lookupVarE :: Name -> SgM DExp
    lookupVarE :: Name -> SgM DExp
    lookupVarE = (Name -> Name) -> (Name -> DExp) -> Name -> SgM DExp
    lookup_var_con Name -> Name
    singValName (Name -> DExp
    DVarE (Name -> DExp) -> (Name -> Name) -> Name -> DExp
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> Name
    singValName)

    lookupConE :: Name -> SgM DExp
    lookupConE :: Name -> SgM DExp
    lookupConE = (Name -> Name) -> (Name -> DExp) -> Name -> SgM DExp
    lookup_var_con Name -> Name
    singDataConName (Name -> DExp
    DConE (Name -> DExp) -> (Name -> Name) -> Name -> DExp
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> Name
    singDataConName)

    lookup_var_con :: (Name -> Name) -> (Name -> DExp) -> Name -> SgM DExp
    lookup_var_con :: (Name -> Name) -> (Name -> DExp) -> Name -> SgM DExp
    lookup_var_con mk_sing_name :: Name -> Name
    mk_sing_name mk_exp :: Name -> DExp
    mk_exp name :: Name
    name = do
      Map Name DExp
    letExpansions <- (SgEnv -> Map Name DExp) -> SgM (Map Name DExp)
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks SgEnv -> Map Name DExp
    sg_let_binds
      Name
    sName <- String -> SgM Name
    forall (m :: * -> *). Quasi m => String -> m Name
    mkDataName (Name -> String
    nameBase (Name -> Name
    mk_sing_name Name
    name)) -- we want *term* names!
      case Name -> Map Name DExp -> Maybe DExp
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    name Map Name DExp
    letExpansions of
        Nothing -> do
          -- try to get it from the global context
          Maybe DInfo
    m_dinfo <- (Maybe DInfo -> Maybe DInfo -> Maybe DInfo)
    -> SgM (Maybe DInfo) -> SgM (Maybe DInfo) -> SgM (Maybe DInfo)
    forall (m :: * -> *) a1 a2 r.
    Monad m =>
    (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
    liftM2 Maybe DInfo -> Maybe DInfo -> Maybe DInfo
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    (<|>) (Name -> SgM (Maybe DInfo)
    forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
    dsReify Name
    sName) (Name -> SgM (Maybe DInfo)
    forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
    dsReify Name
    name)
            -- try the unrefined name too -- it's needed to bootstrap Enum
          case Maybe DInfo
    m_dinfo of
            Just (DVarI _ ty :: DType
    ty _) ->
              let num_args :: Int
    num_args = DType -> Int
    countArgs DType
    ty in
              DExp -> SgM DExp
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DExp -> SgM DExp) -> DExp -> SgM DExp
    forall a b. (a -> b) -> a -> b
    $ Int -> DType -> DExp -> DExp
    wrapSingFun Int
    num_args (Name -> DType
    promoteValRhs Name
    name) (Name -> DExp
    mk_exp Name
    name)
            _ -> DExp -> SgM DExp
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DExp -> SgM DExp) -> DExp -> SgM DExp
    forall a b. (a -> b) -> a -> b
    $ Name -> DExp
    mk_exp Name
    name   -- lambda-bound
        Just exp :: DExp
    exp -> DExp -> SgM DExp
    forall (m :: * -> *) a. Monad m => a -> m a
    return DExp
    exp

    wrapSingFun :: Int -> DType -> DExp -> DExp
    wrapSingFun :: Int -> DType -> DExp -> DExp
    wrapSingFun 0 _  = DExp -> DExp
    forall a. a -> a
    id
    wrapSingFun n :: Int
    n ty :: DType
    ty =
      let wrap_fun :: DExp
    wrap_fun = Name -> DExp
    DVarE (Name -> DExp) -> Name -> DExp
    forall a b. (a -> b) -> a -> b
    $ case Int
    n of
                               1 -> 'singFun1
                               2 -> 'singFun2
                               3 -> 'singFun3
                               4 -> 'singFun4
                               5 -> 'singFun5
                               6 -> 'singFun6
                               7 -> 'singFun7
                               _ -> String -> Name
    forall a. HasCallStack => String -> a
    error "No support for functions of arity > 7."
      in
      (DExp
    wrap_fun DExp -> DType -> DExp
    `DAppTypeE` DType
    ty DExp -> DExp -> DExp
    `DAppE`)

    wrapUnSingFun :: Int -> DType -> DExp -> DExp
    wrapUnSingFun :: Int -> DType -> DExp -> DExp
    wrapUnSingFun 0 _  = DExp -> DExp
    forall a. a -> a
    id
    wrapUnSingFun n :: Int
    n ty :: DType
    ty =
      let unwrap_fun :: DExp
    unwrap_fun = Name -> DExp
    DVarE (Name -> DExp) -> Name -> DExp
    forall a b. (a -> b) -> a -> b
    $ case Int
    n of
                                 1 -> 'unSingFun1
                                 2 -> 'unSingFun2
                                 3 -> 'unSingFun3
                                 4 -> 'unSingFun4
                                 5 -> 'unSingFun5
                                 6 -> 'unSingFun6
                                 7 -> 'unSingFun7
                                 _ -> String -> Name
    forall a. HasCallStack => String -> a
    error "No support for functions of arity > 7."
      in
      (DExp
    unwrap_fun DExp -> DType -> DExp
    `DAppTypeE` DType
    ty DExp -> DExp -> DExp
    `DAppE`)

    singM :: DsMonad q => [Dec] -> SgM a -> q (a, [DDec])
    singM :: [Dec] -> SgM a -> q (a, [DDec])
    singM locals :: [Dec]
    locals (SgM rdr :: ReaderT SgEnv (WriterT [DDec] Q) a
    rdr) = do
      [Dec]
    other_locals <- q [Dec]
    forall (m :: * -> *). DsMonad m => m [Dec]
    localDeclarations
      let wr :: WriterT [DDec] Q a
    wr = ReaderT SgEnv (WriterT [DDec] Q) a -> SgEnv -> WriterT [DDec] Q a
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT ReaderT SgEnv (WriterT [DDec] Q) a
    rdr (SgEnv
    emptySgEnv { sg_local_decls :: [Dec]
    sg_local_decls = [Dec]
    other_locals [Dec] -> [Dec] -> [Dec]
    forall a. [a] -> [a] -> [a]
    ++ [Dec]
    locals })
          q :: Q (a, [DDec])
    q  = WriterT [DDec] Q a -> Q (a, [DDec])
    forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
    runWriterT WriterT [DDec] Q a
    wr
      Q (a, [DDec]) -> q (a, [DDec])
    forall (m :: * -> *) a. Quasi m => Q a -> m a
    runQ Q (a, [DDec])
    q

    singDecsM :: DsMonad q => [Dec] -> SgM [DDec] -> q [DDec]
    singDecsM :: [Dec] -> SgM [DDec] -> q [DDec]
    singDecsM locals :: [Dec]
    locals thing :: SgM [DDec]
    thing = do
      (decs1 :: [DDec]
    decs1, decs2 :: [DDec]
    decs2) <- [Dec] -> SgM [DDec] -> q ([DDec], [DDec])
    forall (q :: * -> *) a.
    DsMonad q =>
    [Dec] -> SgM a -> q (a, [DDec])
    singM [Dec]
    locals SgM [DDec]
    thing
      [DDec] -> q [DDec]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([DDec] -> q [DDec]) -> [DDec] -> q [DDec]
    forall a b. (a -> b) -> a -> b
    $ [DDec]
    decs1 [DDec] -> [DDec] -> [DDec]
    forall a. [a] -> [a] -> [a]
    ++ [DDec]
    decs2

    {-
    Note [Tracking the current type signature context]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Much like we track the let-bound names in scope, we also track the current
    context. For instance, in the following program:

      -- (1)
      f :: forall a. Show a => a -> String -> Bool
      f x y = g (show x) y
        where
          -- (2)
          g :: forall b. Eq b => b -> b -> Bool
          g = h
            where
              -- (3)
              h :: b -> b -> Bool
              h = (==)

    Here is the context at various points:

    (1) ()
    (2) (Show a)
    (3) (Show a, Eq b)

    We track this informating during singling instead of during promotion, as the
    promoted versions of things are often type families, which do not have
    contexts.

    Why do we bother tracking this at all? Ultimately, because singDefuns (from
    Data.Singletons.Single.Defun) needs to know the current context in order to
    generate a correctly typed SingI instance. For instance, if you called
    singDefuns on the class method bar:

      class Foo a where
        bar :: Eq a => a -> Bool

    Then if you only grabbed the context of `bar` itself, then you'd end up
    generating the following SingI instance for BarSym0:

      instance SEq a => SingI (FooSym0 :: a ~> Bool) where ...

    Which is incorrect—there needs to be an (SFoo a) constraint as well! If we
    track the current context when singling Foo, then we will correctly propagate
    this information to singDefuns.
    -}