    {- Data/Singletons/Promote/Monad.hs

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

    This file defines the PrM monad and its operations, for use during promotion.

    The PrM monad allows reading from a PrEnv environment and writing to a list
    of DDec, and is wrapped around a Q.
    -}

    {-# LANGUAGE GeneralizedNewtypeDeriving, FlexibleContexts,
                 TypeFamilies, KindSignatures #-}

    module Data.Singletons.Promote.Monad (
      PrM, promoteM, promoteM_, promoteMDecs, VarPromotions,
      allLocals, emitDecs, emitDecsM,
      lambdaBind, LetBind, letBind, lookupVarE, forallBind, allBoundKindVars
      ) where

    import Control.Monad.Reader
    import Control.Monad.Writer
    import Language.Haskell.TH.Syntax hiding ( lift )
    import Language.Haskell.TH.Desugar
    import qualified Language.Haskell.TH.Desugar.OMap.Strict as OMap
    import Language.Haskell.TH.Desugar.OMap.Strict (OMap)
    import qualified Language.Haskell.TH.Desugar.OSet as OSet
    import Language.Haskell.TH.Desugar.OSet (OSet)
    import Data.Singletons.Names
    import Data.Singletons.Syntax

    type LetExpansions = OMap Name DType  -- from **term-level** name

    -- environment during promotion
    data PrEnv =
      PrEnv { PrEnv -> OMap Name Name
    pr_lambda_bound :: OMap Name Name
            , PrEnv -> LetExpansions
    pr_let_bound    :: LetExpansions
            , PrEnv -> OSet Name
    pr_forall_bound :: OSet Name -- See Note [Explicitly quantifying kinds variables]
            , PrEnv -> [Dec]
    pr_local_decls  :: [Dec]
            }

    emptyPrEnv :: PrEnv
    emptyPrEnv :: PrEnv
    emptyPrEnv = PrEnv :: OMap Name Name -> LetExpansions -> OSet Name -> [Dec] -> PrEnv
    PrEnv { pr_lambda_bound :: OMap Name Name
    pr_lambda_bound = OMap Name Name
    forall k v. OMap k v
    OMap.empty
                       , pr_let_bound :: LetExpansions
    pr_let_bound    = LetExpansions
    forall k v. OMap k v
    OMap.empty
                       , pr_forall_bound :: OSet Name
    pr_forall_bound = OSet Name
    forall a. OSet a
    OSet.empty
                       , pr_local_decls :: [Dec]
    pr_local_decls  = [] }

    -- the promotion monad
    newtype PrM a = PrM (ReaderT PrEnv (WriterT [DDec] Q) a)
      deriving ( a -> PrM b -> PrM a
    (a -> b) -> PrM a -> PrM b
    (forall a b. (a -> b) -> PrM a -> PrM b)
    -> (forall a b. a -> PrM b -> PrM a) -> Functor PrM
    forall a b. a -> PrM b -> PrM a
    forall a b. (a -> b) -> PrM a -> PrM b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: a -> PrM b -> PrM a
    $c<$ :: forall a b. a -> PrM b -> PrM a
    fmap :: (a -> b) -> PrM a -> PrM b
    $cfmap :: forall a b. (a -> b) -> PrM a -> PrM b
    Functor, Functor PrM
    a -> PrM a
    Functor PrM =>
    (forall a. a -> PrM a)
    -> (forall a b. PrM (a -> b) -> PrM a -> PrM b)
    -> (forall a b c. (a -> b -> c) -> PrM a -> PrM b -> PrM c)
    -> (forall a b. PrM a -> PrM b -> PrM b)
    -> (forall a b. PrM a -> PrM b -> PrM a)
    -> Applicative PrM
    PrM a -> PrM b -> PrM b
    PrM a -> PrM b -> PrM a
    PrM (a -> b) -> PrM a -> PrM b
    (a -> b -> c) -> PrM a -> PrM b -> PrM c
    forall a. a -> PrM a
    forall a b. PrM a -> PrM b -> PrM a
    forall a b. PrM a -> PrM b -> PrM b
    forall a b. PrM (a -> b) -> PrM a -> PrM b
    forall a b c. (a -> b -> c) -> PrM a -> PrM b -> PrM 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
    <* :: PrM a -> PrM b -> PrM a
    $c<* :: forall a b. PrM a -> PrM b -> PrM a
    *> :: PrM a -> PrM b -> PrM b
    $c*> :: forall a b. PrM a -> PrM b -> PrM b
    liftA2 :: (a -> b -> c) -> PrM a -> PrM b -> PrM c
    $cliftA2 :: forall a b c. (a -> b -> c) -> PrM a -> PrM b -> PrM c
    <*> :: PrM (a -> b) -> PrM a -> PrM b
    $c<*> :: forall a b. PrM (a -> b) -> PrM a -> PrM b
    pure :: a -> PrM a
    $cpure :: forall a. a -> PrM a
    $cp1Applicative :: Functor PrM
    Applicative, Applicative PrM
    a -> PrM a
    Applicative PrM =>
    (forall a b. PrM a -> (a -> PrM b) -> PrM b)
    -> (forall a b. PrM a -> PrM b -> PrM b)
    -> (forall a. a -> PrM a)
    -> Monad PrM
    PrM a -> (a -> PrM b) -> PrM b
    PrM a -> PrM b -> PrM b
    forall a. a -> PrM a
    forall a b. PrM a -> PrM b -> PrM b
    forall a b. PrM a -> (a -> PrM b) -> PrM 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 -> PrM a
    $creturn :: forall a. a -> PrM a
    >> :: PrM a -> PrM b -> PrM b
    $c>> :: forall a b. PrM a -> PrM b -> PrM b
    >>= :: PrM a -> (a -> PrM b) -> PrM b
    $c>>= :: forall a b. PrM a -> (a -> PrM b) -> PrM b
    $cp1Monad :: Applicative PrM
    Monad, MonadFail PrM
    MonadIO PrM
    PrM [Extension]
    PrM (Maybe a)
    PrM Loc
    a -> PrM ()
    Bool -> String -> PrM (Maybe Name)
    Bool -> String -> PrM ()
    String -> PrM String
    String -> PrM Name
    String -> PrM ()
    [Dec] -> PrM ()
    IO a -> PrM a
    Q () -> PrM ()
    Name -> PrM [Role]
    Name -> PrM [DecidedStrictness]
    Name -> PrM (Maybe Fixity)
    Name -> PrM Info
    Name -> [Type] -> PrM [Dec]
    ForeignSrcLang -> String -> PrM ()
    Extension -> PrM Bool
    AnnLookup -> PrM [a]
    Module -> PrM ModuleInfo
    (MonadIO PrM, MonadFail PrM) =>
    (String -> PrM Name)
    -> (Bool -> String -> PrM ())
    -> (forall a. PrM a -> PrM a -> PrM a)
    -> (Bool -> String -> PrM (Maybe Name))
    -> (Name -> PrM Info)
    -> (Name -> PrM (Maybe Fixity))
    -> (Name -> [Type] -> PrM [Dec])
    -> (Name -> PrM [Role])
    -> (forall a. Data a => AnnLookup -> PrM [a])
    -> (Module -> PrM ModuleInfo)
    -> (Name -> PrM [DecidedStrictness])
    -> PrM Loc
    -> (forall a. IO a -> PrM a)
    -> (String -> PrM ())
    -> (String -> PrM String)
    -> ([Dec] -> PrM ())
    -> (ForeignSrcLang -> String -> PrM ())
    -> (Q () -> PrM ())
    -> (String -> PrM ())
    -> (forall a. Typeable a => PrM (Maybe a))
    -> (forall a. Typeable a => a -> PrM ())
    -> (Extension -> PrM Bool)
    -> PrM [Extension]
    -> Quasi PrM
    PrM a -> PrM a -> PrM a
    forall a. Data a => AnnLookup -> PrM [a]
    forall a. Typeable a => PrM (Maybe a)
    forall a. Typeable a => a -> PrM ()
    forall a. IO a -> PrM a
    forall a. PrM a -> PrM a -> PrM a
    forall (m :: * -> *).
    (MonadIO m, MonadFail m) =>
    (String -> m Name)
    -> (Bool -> String -> m ())
    -> (forall a. m a -> m a -> m a)
    -> (Bool -> String -> m (Maybe Name))
    -> (Name -> m Info)
    -> (Name -> m (Maybe Fixity))
    -> (Name -> [Type] -> m [Dec])
    -> (Name -> m [Role])
    -> (forall a. Data a => AnnLookup -> m [a])
    -> (Module -> m ModuleInfo)
    -> (Name -> m [DecidedStrictness])
    -> m Loc
    -> (forall a. IO a -> m a)
    -> (String -> m ())
    -> (String -> m String)
    -> ([Dec] -> m ())
    -> (ForeignSrcLang -> String -> m ())
    -> (Q () -> m ())
    -> (String -> m ())
    -> (forall a. Typeable a => m (Maybe a))
    -> (forall a. Typeable a => a -> m ())
    -> (Extension -> m Bool)
    -> m [Extension]
    -> Quasi m
    qExtsEnabled :: PrM [Extension]
    $cqExtsEnabled :: PrM [Extension]
    qIsExtEnabled :: Extension -> PrM Bool
    $cqIsExtEnabled :: Extension -> PrM Bool
    qPutQ :: a -> PrM ()
    $cqPutQ :: forall a. Typeable a => a -> PrM ()
    qGetQ :: PrM (Maybe a)
    $cqGetQ :: forall a. Typeable a => PrM (Maybe a)
    qAddCorePlugin :: String -> PrM ()
    $cqAddCorePlugin :: String -> PrM ()
    qAddModFinalizer :: Q () -> PrM ()
    $cqAddModFinalizer :: Q () -> PrM ()
    qAddForeignFilePath :: ForeignSrcLang -> String -> PrM ()
    $cqAddForeignFilePath :: ForeignSrcLang -> String -> PrM ()
    qAddTopDecls :: [Dec] -> PrM ()
    $cqAddTopDecls :: [Dec] -> PrM ()
    qAddTempFile :: String -> PrM String
    $cqAddTempFile :: String -> PrM String
    qAddDependentFile :: String -> PrM ()
    $cqAddDependentFile :: String -> PrM ()
    qRunIO :: IO a -> PrM a
    $cqRunIO :: forall a. IO a -> PrM a
    qLocation :: PrM Loc
    $cqLocation :: PrM Loc
    qReifyConStrictness :: Name -> PrM [DecidedStrictness]
    $cqReifyConStrictness :: Name -> PrM [DecidedStrictness]
    qReifyModule :: Module -> PrM ModuleInfo
    $cqReifyModule :: Module -> PrM ModuleInfo
    qReifyAnnotations :: AnnLookup -> PrM [a]
    $cqReifyAnnotations :: forall a. Data a => AnnLookup -> PrM [a]
    qReifyRoles :: Name -> PrM [Role]
    $cqReifyRoles :: Name -> PrM [Role]
    qReifyInstances :: Name -> [Type] -> PrM [Dec]
    $cqReifyInstances :: Name -> [Type] -> PrM [Dec]
    qReifyFixity :: Name -> PrM (Maybe Fixity)
    $cqReifyFixity :: Name -> PrM (Maybe Fixity)
    qReify :: Name -> PrM Info
    $cqReify :: Name -> PrM Info
    qLookupName :: Bool -> String -> PrM (Maybe Name)
    $cqLookupName :: Bool -> String -> PrM (Maybe Name)
    qRecover :: PrM a -> PrM a -> PrM a
    $cqRecover :: forall a. PrM a -> PrM a -> PrM a
    qReport :: Bool -> String -> PrM ()
    $cqReport :: Bool -> String -> PrM ()
    qNewName :: String -> PrM Name
    $cqNewName :: String -> PrM Name
    $cp2Quasi :: MonadFail PrM
    $cp1Quasi :: MonadIO PrM
    Quasi
               , MonadReader PrEnv, MonadWriter [DDec]
               , Monad PrM
    Monad PrM => (forall a. String -> PrM a) -> MonadFail PrM
    String -> PrM a
    forall a. String -> PrM a
    forall (m :: * -> *).
    Monad m =>
    (forall a. String -> m a) -> MonadFail m
    fail :: String -> PrM a
    $cfail :: forall a. String -> PrM a
    $cp1MonadFail :: Monad PrM
    MonadFail, Monad PrM
    Monad PrM => (forall a. IO a -> PrM a) -> MonadIO PrM
    IO a -> PrM a
    forall a. IO a -> PrM a
    forall (m :: * -> *).
    Monad m =>
    (forall a. IO a -> m a) -> MonadIO m
    liftIO :: IO a -> PrM a
    $cliftIO :: forall a. IO a -> PrM a
    $cp1MonadIO :: Monad PrM
    MonadIO )

    instance DsMonad PrM where
      localDeclarations :: PrM [Dec]
    localDeclarations = (PrEnv -> [Dec]) -> PrM [Dec]
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks PrEnv -> [Dec]
    pr_local_decls

    -- return *type-level* names
    allLocals :: MonadReader PrEnv m => m [Name]
    allLocals :: m [Name]
    allLocals = do
      [(Name, Name)]
    lambdas <- (PrEnv -> [(Name, Name)]) -> m [(Name, Name)]
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (OMap Name Name -> [(Name, Name)]
    forall k v. OMap k v -> [(k, v)]
    OMap.assocs (OMap Name Name -> [(Name, Name)])
    -> (PrEnv -> OMap Name Name) -> PrEnv -> [(Name, Name)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PrEnv -> OMap Name Name
    pr_lambda_bound)
      LetExpansions
    lets    <- (PrEnv -> LetExpansions) -> m LetExpansions
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks PrEnv -> LetExpansions
    pr_let_bound
        -- filter out shadowed variables!
      [Name] -> m [Name]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ Name
    typeName
             | (termName :: Name
    termName, typeName :: Name
    typeName) <- [(Name, Name)]
    lambdas
             , case Name -> LetExpansions -> Maybe DType
    forall k v. Ord k => k -> OMap k v -> Maybe v
    OMap.lookup Name
    termName LetExpansions
    lets of
                 Just (DVarT typeName' :: Name
    typeName') | Name
    typeName' Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    typeName -> Bool
    True
                 _                                              -> Bool
    False ]

    emitDecs :: MonadWriter [DDec] m => [DDec] -> m ()
    emitDecs :: [DDec] -> m ()
    emitDecs = [DDec] -> m ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell

    emitDecsM :: MonadWriter [DDec] m => m [DDec] -> m ()
    emitDecsM :: m [DDec] -> m ()
    emitDecsM action :: m [DDec]
    action = do
      [DDec]
    decs <- m [DDec]
    action
      [DDec] -> m ()
    forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
    emitDecs [DDec]
    decs

    -- when lambda-binding variables, we still need to add the variables
    -- to the let-expansion, because of shadowing. ugh.
    lambdaBind :: VarPromotions -> PrM a -> PrM a
    lambdaBind :: [(Name, Name)] -> PrM a -> PrM a
    lambdaBind binds :: [(Name, Name)]
    binds = (PrEnv -> PrEnv) -> PrM a -> PrM a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local PrEnv -> PrEnv
    add_binds
      where add_binds :: PrEnv -> PrEnv
    add_binds env :: PrEnv
    env@(PrEnv { pr_lambda_bound :: PrEnv -> OMap Name Name
    pr_lambda_bound = OMap Name Name
    lambdas
                                 , pr_let_bound :: PrEnv -> LetExpansions
    pr_let_bound    = LetExpansions
    lets }) =
              let new_lets :: LetExpansions
    new_lets = [(Name, DType)] -> LetExpansions
    forall k v. Ord k => [(k, v)] -> OMap k v
    OMap.fromList [ (Name
    tmN, Name -> DType
    DVarT Name
    tyN) | (tmN :: Name
    tmN, tyN :: Name
    tyN) <- [(Name, Name)]
    binds ] in
              PrEnv
    env { pr_lambda_bound :: OMap Name Name
    pr_lambda_bound = [(Name, Name)] -> OMap Name Name
    forall k v. Ord k => [(k, v)] -> OMap k v
    OMap.fromList [(Name, Name)]
    binds OMap Name Name -> OMap Name Name -> OMap Name Name
    forall k v. Ord k => OMap k v -> OMap k v -> OMap k v
    `OMap.union` OMap Name Name
    lambdas
                  , pr_let_bound :: LetExpansions
    pr_let_bound    = LetExpansions
    new_lets            LetExpansions -> LetExpansions -> LetExpansions
    forall k v. Ord k => OMap k v -> OMap k v -> OMap k v
    `OMap.union` LetExpansions
    lets }

    type LetBind = (Name, DType)
    letBind :: [LetBind] -> PrM a -> PrM a
    letBind :: [(Name, DType)] -> PrM a -> PrM a
    letBind binds :: [(Name, DType)]
    binds = (PrEnv -> PrEnv) -> PrM a -> PrM a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local PrEnv -> PrEnv
    add_binds
      where add_binds :: PrEnv -> PrEnv
    add_binds env :: PrEnv
    env@(PrEnv { pr_let_bound :: PrEnv -> LetExpansions
    pr_let_bound = LetExpansions
    lets }) =
              PrEnv
    env { pr_let_bound :: LetExpansions
    pr_let_bound = [(Name, DType)] -> LetExpansions
    forall k v. Ord k => [(k, v)] -> OMap k v
    OMap.fromList [(Name, DType)]
    binds LetExpansions -> LetExpansions -> LetExpansions
    forall k v. Ord k => OMap k v -> OMap k v -> OMap k v
    `OMap.union` LetExpansions
    lets }

    lookupVarE :: Name -> PrM DType
    lookupVarE :: Name -> PrM DType
    lookupVarE n :: Name
    n = do
      LetExpansions
    lets <- (PrEnv -> LetExpansions) -> PrM LetExpansions
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks PrEnv -> LetExpansions
    pr_let_bound
      case Name -> LetExpansions -> Maybe DType
    forall k v. Ord k => k -> OMap k v -> Maybe v
    OMap.lookup Name
    n LetExpansions
    lets of
        Just ty :: DType
    ty -> DType -> PrM DType
    forall (m :: * -> *) a. Monad m => a -> m a
    return DType
    ty
        Nothing -> DType -> PrM DType
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DType -> PrM DType) -> DType -> PrM DType
    forall a b. (a -> b) -> a -> b
    $ Name -> DType
    promoteValRhs Name
    n

    -- Add to the set of bound kind variables currently in scope.
    -- See Note [Explicitly binding kind variables]
    forallBind :: OSet Name -> PrM a -> PrM a
    forallBind :: OSet Name -> PrM a -> PrM a
    forallBind kvs1 :: OSet Name
    kvs1 =
      (PrEnv -> PrEnv) -> PrM a -> PrM a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local (\env :: PrEnv
    env@(PrEnv { pr_forall_bound :: PrEnv -> OSet Name
    pr_forall_bound = OSet Name
    kvs2 }) ->
        PrEnv
    env { pr_forall_bound :: OSet Name
    pr_forall_bound = OSet Name
    kvs1 OSet Name -> OSet Name -> OSet Name
    forall a. Ord a => OSet a -> OSet a -> OSet a
    `OSet.union` OSet Name
    kvs2 })

    -- Look up the set of bound kind variables currently in scope.
    -- See Note [Explicitly binding kind variables]
    allBoundKindVars :: PrM (OSet Name)
    allBoundKindVars :: PrM (OSet Name)
    allBoundKindVars = (PrEnv -> OSet Name) -> PrM (OSet Name)
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks PrEnv -> OSet Name
    pr_forall_bound

    promoteM :: DsMonad q => [Dec] -> PrM a -> q (a, [DDec])
    promoteM :: [Dec] -> PrM a -> q (a, [DDec])
    promoteM locals :: [Dec]
    locals (PrM rdr :: ReaderT PrEnv (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 PrEnv (WriterT [DDec] Q) a -> PrEnv -> WriterT [DDec] Q a
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT ReaderT PrEnv (WriterT [DDec] Q) a
    rdr (PrEnv
    emptyPrEnv { pr_local_decls :: [Dec]
    pr_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

    promoteM_ :: DsMonad q => [Dec] -> PrM () -> q [DDec]
    promoteM_ :: [Dec] -> PrM () -> q [DDec]
    promoteM_ locals :: [Dec]
    locals thing :: PrM ()
    thing = do
      ((), decs :: [DDec]
    decs) <- [Dec] -> PrM () -> q ((), [DDec])
    forall (q :: * -> *) a.
    DsMonad q =>
    [Dec] -> PrM a -> q (a, [DDec])
    promoteM [Dec]
    locals PrM ()
    thing
      [DDec] -> q [DDec]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [DDec]
    decs

    -- promoteM specialized to [DDec]
    promoteMDecs :: DsMonad q => [Dec] -> PrM [DDec] -> q [DDec]
    promoteMDecs :: [Dec] -> PrM [DDec] -> q [DDec]
    promoteMDecs locals :: [Dec]
    locals thing :: PrM [DDec]
    thing = do
      (decs1 :: [DDec]
    decs1, decs2 :: [DDec]
    decs2) <- [Dec] -> PrM [DDec] -> q ([DDec], [DDec])
    forall (q :: * -> *) a.
    DsMonad q =>
    [Dec] -> PrM a -> q (a, [DDec])
    promoteM [Dec]
    locals PrM [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 [Explicitly binding kind variables]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    We want to ensure that when we single type signatures for functions, we should
    explicitly quantify every kind variable bound by a forall. For example, if we
    were to single the identity function:

      identity :: forall a. a -> a
      identity x = x

    We want the final result to be:

      sIdentity :: forall a (x :: a). Sing x -> Sing (Identity x)
      sIdentity sX = sX

    Accomplishing this takes a bit of care during promotion. When promoting a
    function, we determine what set of kind variables are currently bound at that
    point and store them in an ALetDecEnv (as lde_bound_kvs), which in turn is
    singled. Then, during singling, we extract every kind variable in a singled
    type signature, subtract the lde_bound_kvs, and explicitly bind the variables
    that remain.

    For a top-level function like identity, lde_bound_kvs is the empty set. But
    consider this more complicated example:

      f :: forall a. a -> a
      f = g
        where
          g :: a -> a
          g x = x

    When singling, we would eventually end up in this spot:

      sF :: forall a (x :: a). Sing a -> Sing (F a)
      sF = sG
        where
          sG :: _
          sG x = x

    We must make sure /not/ to fill in the following type for _:

      sF :: forall a (x :: a). Sing a -> Sing (F a)
      sF = sG
        where
          sG :: forall a (y :: a). Sing a -> Sing (G a)
          sG x = x

    This would be incorrect, as the `a` bound by sF /must/ be the same one used in
    sG, as per the scoping of the original `f` function. Thus, we ensure that the
    bound variables from `f` are put into lde_bound_kvs when promoting `g` so
    that we subtract out `a` and are left with the correct result:

      sF :: forall a (x :: a). Sing a -> Sing (F a)
      sF = sG
        where
          sG :: forall (y :: a). Sing a -> Sing (G a)
          sG x = x
    -}